Re: [isabelle] Quantifying over types



My apologies - I meant to write the "not true" comment under lem2, not lem1.

Tobias

Tobias Nipkow wrote:
>> lemma lem1: "EX func t. func t = 0"
> 
> This lemma is not true because the the result type of func could be a
> one-lement type. The "refute" command finds that counterexample.
> 
> Tobias
> 
>> proof -
>>   have "F s = 0"
>>     using ax1 ax2 ax3
>>     by auto
>>   show ?thesis
>>     by auto
>> qed
>>
>> That's fine (even without declaring the types of func in the lemma). But
>> with:
>>
>> lemma lem2: "EX func t. func t =/ 0"
>> proof -
>>   have "F f =/ 0"
>>     using ax1 ax4 ax5
>>     by auto
>>   show ?thesis
>>     by auto
>>
>> Auto cannot solve ?thesis with "F f =/ 0" in lem2 while it can solve the
>> thesis in lem1 with "F s = 0". It works in lem2 if the lemma was "EX
>> (func::real=>real) t. func t =/ 0". How come the type of func needs to be
>> declared in lem2 but not in lem1? Can type be existentially quantified in
>> some way?
>>
>> Thanks
>> Steve
> 






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