[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
Recently I've experienced a bit odd behavior of schematic_lemma.
Let's consider this minimal example:
"?A ⟹ ?B ⟹ ?C"
fix a1 :: 'a
fix a2 :: 'a
fix A :: "'a set"
show "a1 ∈ A ⟹ a2 ∈ A ⟹ a1 = a1 ∧ a2 = a2" by auto
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and