*To*: Clemens Ballarin <ballarin at in.tum.de>*Subject*: Re: [isabelle] Quantifying over locales*From*: Steve Wong <s.wong.731 at gmail.com>*Date*: Tue, 27 Sep 2011 14:13:05 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20110922204228.29761t2hkq0ui6xg@mailbroy.in.tum.de>*References*: <CAP0k5J4xWF+73sMVdxJWWQ+wJ+7GCbV7854bbCU45vQf+=6Dxw@mail.gmail.com> <20110922204228.29761t2hkq0ui6xg@mailbroy.in.tum.de>

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:*Clemens Ballarin

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

**Re: [isabelle] Quantifying over locales***From:*Clemens Ballarin

- Previous by Date: [isabelle] CfP for 9th International Workshop on Formal Engineering approaches to Software Components and Architectures at ETAPS2012, Tallinn, Estonia
- Next by Date: [isabelle] On the use of the rule HOL.refl(exive)
- Previous by Thread: Re: [isabelle] Quantifying over locales
- Next by Thread: Re: [isabelle] Quantifying over locales
- Cl-isabelle-users September 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