Re: [isabelle] Quantifying over types



Steve W wrote:
> Hi,
> 
> I was wondering why the type of 'func' needs to be be declared in lem1 and
> not in lem2.
> 
> consts
> s :: real
> f :: real
> F :: "real => real"
> Y :: "real => real"
> Z :: "real => real"
> 
> axioms
> ax1 : "F t = Y t + Z t"
> ax2 : "Y s = -1"
> ax3 : "Z s = 1"
> ax4 : "Y f = -1"
> ax5 : "Z f = -1"
> 
> lemma lem1: "EX func t. func t = 0"
> proof -
>   have "F s = 0"
>     using ax1 ax2 ax3
>     by auto
>   show ?thesis
>     by auto
> qed

The "F s = 0" refers to type real and contributes nothing to the proof
of ?thesis, which talks about a 0 of some arbitrary type (displayed as
"0::'b"). This thesis is simple enough that auto can solve it (probably
by func = %x. x" and t = 0) but that is more a coincidence.

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

No.

Tobias





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