# [isabelle] surprising behavior of schematic_lemma

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] surprising behavior of schematic_lemma
*From*: Ondřej Kunčar <kuncar at in.tum.de>
*Date*: Mon, 15 Apr 2013 12:21:33 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

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.*