Re: [isabelle] Quantifying over types
Steve W wrote:
> I was wondering why the type of 'func' needs to be be declared in lem1 and
> not in lem2.
> s :: real
> f :: real
> F :: "real => real"
> Y :: "real => real"
> Z :: "real => real"
> 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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and