*To*: Clemens Ballarin <ballarin at in.tum.de>*Subject*: Re: [isabelle] Quantifying over locales*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 19 Oct 2011 16:29:43 +0100*Cc*: Steve Wong <s.wong.731 at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20110927213334.20121lj04832phxq@mailbroy.in.tum.de>*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>

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 >>>> >>>> >>> >>> >>> >> > > > >

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

- Previous by Date: Re: [isabelle] Custom Isar Commands
- Next by Date: Re: [isabelle] Quantifying over locales
- Previous by Thread: Re: [isabelle] Custom Isar Commands
- 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