*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Calling sublocale A < B in A’s context?*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 21 Oct 2013 14:32:06 +0200

Hi, I have a pattern in my theories where I have a series of locales, each refining the previous, e.g. locale A = fixes param :: bool begin lemma A_lem: "param = param".. end locale B = A + assumes "param = True" and then in a different locale, I instantiate the initial locale and step-for-step work through the assumptions of the following locales. So what I’d like to do is something like locale C = fixes n :: nat begin (* ... *) interpretation A "n = 0". (* ... *) lemma n: "n = 0" sorry interpretation B "n = 0" by (unfold_locales, simp add: n) (* ... *) end but (as documented, and quite correctly) now the results from locales A and B are not available when interpreting C, or even when opening "context C" again later. So what I have to do instead is: locale C = fixes n :: nat begin (* ... *) end sublocale C < A "n = 0". context C begin (* ... *) lemma n: "n = 0" sorry end sublocale C < B "n = 0" by (unfold_locales, simp add: n) context C begin (* ... *) end which I find a bit ugly. Is there a way to declare a sublocale relationship for the current locale form within that locale? Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Calling sublocale A < B in A’s context?***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Recursion through Types
- Next by Date: Re: [isabelle] Calling sublocale A < B in A’s context?
- Previous by Thread: Re: [isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE
- Next by Thread: Re: [isabelle] Calling sublocale A < B in A’s context?
- Cl-isabelle-users October 2013 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