*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Quantifying over locales*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 19 Oct 2011 16:47:16 +0100*Cc*: Clemens Ballarin <ballarin at in.tum.de>, Steve Wong <s.wong.731 at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4E9EEF5B.4080404@kit.edu>*References*: <CAP0k5J4xWF+73sMVdxJWWQ+wJ+7GCbV7854bbCU45vQf+=6Dxw@mail.gmail.com> <20110922204228.29761t2hkq0ui6xg@mailbroy.in.tum.de> <CAFU+7wO8Y_nj0bDmT-EDKjp8EaNSWNDABMZ0aEuWL8E4Q17bbg@mail.gmail.com> <20110927213334.20121lj04832phxq@mailbroy.in.tum.de> <CAP0k5J4MrtP6VGC1KpWj4dAzvawqnDrWYupOwfFnAA7irSZHaA@mail.gmail.com> <4E9EEF5B.4080404@kit.edu>

Thanks. Sorry, I should have made my question clearer (with a better example): Suppose I have two different locales locale T = fixes f c assumes "f c > 0" locale S = fixes f c assumes "f c = 0" I want to prove that f c > 0 is indeed provable in T and f c = 0 is indeed provable in S in a single lemma. Based on your response, I believe the appropriate formulation would be: lemma "T f c & S f' c' --> f c > 0 & f' c' = 0" Am I correct? But how about lemma "(T f c --> f c > 0) & (S f' c' --> f' c' = 0)" Does it not fulfil my purpose as well? Thanks John On Wed, Oct 19, 2011 at 4:40 PM, Andreas Lochbihler <andreas.lochbihler at kit.edu> wrote: > Dear John, > > all of your statements essentially involve only the parameters of *one* > locale, so it is hard to say which is the right one. Also, your original > question involved only one locale T, now there seems to be another called S. > I am confused. > > Here's an example how I would do it. Maybe this helps. > > locale T = fixes f c assumes "f c > 0" > > lemma "T f1 c1 & T f2 c2 ==> f1 c1 > 0 & f2 c2 > 0 & ..." > > (* or in Isar syntax *) > > lemma > assumes "T f1 c1" and "T f2 c2" > shows "f1 c1 > 0" and "f2 c2 > 0" and "..." > > If you have two different locales S and T, it essentially looks the same: > > locale T = fixes f c assumes ... > locale S = fixes a b assumes ... > > lemma "T f c & S a b ==> P f c a b" > > where P is the property that you wish to prove about the parameters of both > locales. > > If you want to use the convenient locale mechanism, you can also combine > locales as follows: > > locale T_and_S = T + S begin > lemma "P f c a b" > <proof> > end > > > Andreas > > Am 19.10.2011 17:29, schrieb John Munroe: >> >> Digging up a slightly old post: So if I want to have a lemma that >> speaks about 2 locales, T f c and S a b, which of the following is >> correct? >> >> lemma "(T f c --> f c> 0)& (S a b --> a b> 0)" >> >> or >> >> lemma "T f c& S a b --> f c> 0& a b> 0" >> >> Thanks >> >> John >> >> On Tue, Sep 27, 2011 at 8:33 PM, Clemens Ballarin<ballarin at in.tum.de> >> wrote: >>> >>> Hi Steve, >>> >>> I think this is correct. You'll need some knowledge about nat in the >>> proof, >>> of course. >>> >>> Clemens >>> >>> >>> Quoting Steve Wong<s.wong.731 at gmail.com>: >>> >>>> Just to confirm my understanding: >>>> >>>> EX f c. T f c& f c> 0 can be proved with the fact T_def. >>>> >>>> ALL f c. T f c --> f c> 0 can also be proved with the fact T.ax. >>>> Alternatively T f c --> f c> 0 can be proved the same way because free >>>> variables are implicitly quantified. >>>> >>>> Am I right here? >>>> >>>> Steve >>>> >>>> On Thu, Sep 22, 2011 at 7:42 PM, Clemens Ballarin >>>> <ballarin at in.tum.de>wrote: >>>> >>>>> A locale is a predicate and its existence is trivial. What you >>>>> probably >>>>> wanted to show is that there is an instance of T for which f c> 0: >>>>> >>>>> EX f c. T f c& f c> 0 >>>>> >>>>> If you get the locale predicate (T in your case) involved, types are >>>>> inferred. >>>>> >>>>> Clemens >>>>> >>>>> >>>>> >>>>> Quoting John Munroe<munddr at gmail.com>: >>>>> >>>>> Hi, >>>>>> >>>>>> I'm trying to see how one could quantify over locales. For example, if >>>>>> I >>>>>> have: >>>>>> >>>>>> locale T = >>>>>> fixes f :: "nat => nat" >>>>>> and c :: nat >>>>>> assumes ax: "f c = 1" >>>>>> >>>>>> and if I want to prove that there exists a locale taking 2 parameters >>>>>> such that applying the first parameter to the second is equal to 0 >>>>>> (essentially T): >>>>>> >>>>>> lemma "EX P. P (f::real=>real) (c::real) --> f c> 0" >>>>>> >>>>>> but that would be a trivial lemma since P f c can simply be False. So >>>>>> how should one properly formulate the lemma? Is there a way of doing >>>>>> so without specifying on the type that each parameter should take? >>>>>> >>>>>> Thanks in advance. >>>>>> >>>>>> John >>>>>> >>>>>> >>>>> >>>>> >>>>> >>>> >>> >>> >>> >>> >> > > -- > Karlsruher Institut für Technologie > IPD Snelting > > Andreas Lochbihler > wissenschaftlicher Mitarbeiter > Adenauerring 20a, Geb. 50.41, Raum 031 > 76131 Karlsruhe > > Telefon: +49 721 608-47399 > Fax: +49 721 608-48457 > E-Mail: andreas.lochbihler at kit.edu > http://pp.info.uni-karlsruhe.de > KIT - Universität des Landes Baden-Württemberg und nationales > Forschungszentrum in der Helmholtz-Gemeinschaft >

**Follow-Ups**:**Re: [isabelle] Quantifying over locales***From:*Andreas Lochbihler

**References**:**Re: [isabelle] Quantifying over locales***From:*John Munroe

**Re: [isabelle] Quantifying over locales***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Quantifying over locales
- Next by Date: [isabelle] Schematic type variable
- Previous by Thread: Re: [isabelle] Quantifying over locales
- Next by Thread: Re: [isabelle] Quantifying over locales
- Cl-isabelle-users October 2011 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