[isabelle] surprising behavior of schematic_lemma



Hi.
Recently I've experienced a bit odd behavior of schematic_lemma.
Let's consider this minimal example:

schematic_lemma surprise:
"?A ⟹ ?B ⟹ ?C"
proof -
  fix a1 :: 'a
  fix a2 :: 'a
  fix A :: "'a set"
  show "a1 ∈ A ⟹ a2 ∈ A ⟹ a1 = a1 ∧ a2 = a2" by auto
qed

Then what I get as a lemma surprise is the following theorem:
?a1.0 ∈ ?A ⟹ ?B ⟹ ?a1.0 = ?a1.0 ∧ ?a1.0 = ?a1.0

That hints that a2 ∈ A got somehow unified against a1 ∈ A and is not used any more as an assumption. Thus I get a more special theorem than I wanted to have.

I guess I am going to get the canonical answer: "it has never been intended to be used like that" but I am wondering anyway if there is an easy way to make schematic_lemma working for this kind of situations.

Ondrej




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