[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"
have "F s = 0"
using ax1 ax2 ax3
That's fine (even without declaring the types of func in the lemma). But
lemma lem2: "EX func t. func t =/ 0"
have "F f =/ 0"
using ax1 ax4 ax5
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and