*To*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Case names qualified by locale*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 10 Sep 2015 15:15:03 +0200*In-reply-to*: <55E83A3B.7030606@in.tum.de>*Organization*: TU Munich*References*: <55E81EF1.5040401@yozora.eu> <55E83A3B.7030606@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

>> I like how I can use a named case for coinduction, where P is a >> coinductive predicate: >> >> lemma "P n" >> proof (coinduction rule: P.coinduct) >> case P show ?case sorry >> qed >> >> This works fine. >> >> However, suppose P is inside a locale L. Sometimes I need coinduction >> over L.P: >> >> lemma "L.P n" >> proof (coinduction rule: L.P.coinduct) >> case P show ?case sorry >> qed > > I don't know why the case names are lost here The case names are not ÂlostÂ. L.P is a opaque foundational constant, and the corresponding declarations are applied only in resulting contexts, i. e. in the context of the locale itself or due to interpretation. You might consider wrapping up you matter in something like context begin interpretation prefix!: L â <proof> lemma â proof (coinduction rule: prefix.P.coinduct) case P â qed end which will give you the full declarations from L inside a certain block. Hope this helps. Florian but you should be able to > use the names by using > > L.P.coinduct[case_names P Q R] > > or maybe > > L.P.coinduct[consumes 1, case_names P Q R] > > as a workaround. > > -- Lars > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Case names qualified by locale***From:*Christoph Dittmann

**Re: [isabelle] Case names qualified by locale***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Code setup for Fraction_Field
- Next by Date: Re: [isabelle] Creating ML data is slow. No sharing/caching?
- Previous by Thread: Re: [isabelle] Case names qualified by locale
- Next by Thread: Re: [isabelle] citation autocompletion
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list