Re: [isabelle] Quantifying over locales



But what if I want to show that there is a binary predicate/locale in the
theory such that applying the first param to the second is greater than 0
instead? Basically T f c will be the witness. How should the lemma be
formulated?

Thank you.

John

On Thursday, September 22, 2011, 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
>>
>
>
>
>




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