[isabelle] Quantifying over types


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

That's fine (even without declaring the types of func in the lemma). But

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?


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