# Re: [isabelle] Quantifying over locales

• 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
• 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?
>>>>
>>>>
>>>> John
>>>>
>>>>
>>>
>>>
>>>
>>
>
>
>
>

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.