*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Quantifying over locales*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Thu, 22 Sep 2011 20:42:28 +0200*In-reply-to*: <CAP0k5J4xWF+73sMVdxJWWQ+wJ+7GCbV7854bbCU45vQf+=6Dxw@mail.gmail.com>*References*: <CAP0k5J4xWF+73sMVdxJWWQ+wJ+7GCbV7854bbCU45vQf+=6Dxw@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

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:*John Munroe

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

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

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