*To*: Steve Wong <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Quantifying over locales*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 27 Sep 2011 21:33:34 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAFU+7wO8Y_nj0bDmT-EDKjp8EaNSWNDABMZ0aEuWL8E4Q17bbg@mail.gmail.com>*References*: <CAP0k5J4xWF+73sMVdxJWWQ+wJ+7GCbV7854bbCU45vQf+=6Dxw@mail.gmail.com> <20110922204228.29761t2hkq0ui6xg@mailbroy.in.tum.de> <CAFU+7wO8Y_nj0bDmT-EDKjp8EaNSWNDABMZ0aEuWL8E4Q17bbg@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

Hi Steve,

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

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

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

**Re: [isabelle] Quantifying over locales***From:*Steve Wong

- Previous by Date: Re: [isabelle] 3 new AFP entries
- Next by Date: [isabelle] conditional equations and code generation
- Previous by Thread: Re: [isabelle] Quantifying over locales
- Next by Thread: [isabelle] IJCAR 2012: Call for Papers
- 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