[isabelle] Implicit typing in lemma
Please correct my understanding of this situation. Suppose I have:
a :: real
ax1: "f a = 0"
lemma lemma1: "EX func arg. func arg = 0"
show "g a = 0"
I cannot proceed to the line with the proof goal "g a = 0" because the type
implied by this proof goal is more specific than the lemma.
However, why is the following fine:
lemma lemma2: "EX func arg. func arg = 0"
have "g a = 0"
Are the types of func and arg in lemma2 not also universally quantified? I'm
proving it using ax1, in which f and a have more specific types.
Thanks for any help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and