[isabelle] Implicit typing in lemma



Hi,

Please correct my understanding of this situation. Suppose I have:

consts
a :: real

axioms
ax1: "f a = 0"

lemma lemma1: "EX func arg. func arg = 0"
proof -
  show "g a = 0"
    using ax1
    by auto
qed

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"
proof -
  have "g a = 0"
    using ax1
    by auto
  show ?thesis
    by auto
qed

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.

Steve




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