Re: [isabelle] Quantifying over types



> 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.