Re: [isabelle] Quantifying over locales



Thanks. Sorry, I should have made my question clearer (with a better
example): Suppose I have two different locales

locale T = fixes f c assumes "f c > 0"
locale S = fixes f c assumes "f c = 0"

I want to prove that f c > 0 is indeed provable in T and f c = 0 is
indeed provable in S in a single lemma. Based on your response, I
believe the appropriate formulation would be:

lemma "T f c & S f' c' --> f c > 0 & f' c' = 0"

Am I correct?

But how about

lemma "(T f c --> f c > 0) & (S f' c' --> f' c' = 0)"

Does it not fulfil my purpose as well?

Thanks

John

On Wed, Oct 19, 2011 at 4:40 PM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
> Dear John,
>
> all of your statements essentially involve only the parameters of *one*
> locale, so it is hard to say which is the right one. Also, your original
> question involved only one locale T, now there seems to be another called S.
> I am confused.
>
> Here's an example how I would do it. Maybe this helps.
>
> locale T = fixes f c assumes "f c > 0"
>
> lemma "T f1 c1 & T f2 c2 ==> f1 c1 > 0 & f2 c2 > 0 & ..."
>
> (* or in Isar syntax *)
>
> lemma
>  assumes "T f1 c1" and "T f2 c2"
>  shows "f1 c1 > 0" and "f2 c2 > 0" and "..."
>
> If you have two different locales S and T, it essentially looks the same:
>
> locale T = fixes f c assumes ...
> locale S = fixes a b assumes ...
>
> lemma "T f c & S a b ==> P f c a b"
>
> where P is the property that you wish to prove about the parameters of both
> locales.
>
> If you want to use the convenient locale mechanism, you can also combine
> locales as follows:
>
> locale T_and_S = T + S begin
> lemma "P f c a b"
> <proof>
> end
>
>
> Andreas
>
> Am 19.10.2011 17:29, schrieb John Munroe:
>>
>> 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
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>
>>>
>>>
>>>
>>
>
> --
> Karlsruher Institut für Technologie
> IPD Snelting
>
> Andreas Lochbihler
> wissenschaftlicher Mitarbeiter
> Adenauerring 20a, Geb. 50.41, Raum 031
> 76131 Karlsruhe
>
> Telefon: +49 721 608-47399
> Fax: +49 721 608-48457
> E-Mail: andreas.lochbihler at kit.edu
> http://pp.info.uni-karlsruhe.de
> KIT - Universität des Landes Baden-Württemberg und nationales
> Forschungszentrum in der Helmholtz-Gemeinschaft
>





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