[isabelle] Quantifying over types



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

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.