Re: [isabelle] surprising behavior of schematic_lemma
On 15.04.2013 12:21, Ondřej Kunčar wrote:
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
Not that it helps in your concrete case, but using meta implication in
show will often get you unexpected results and is thus best avoided (by
using assume instead).
This archive was generated by a fusion of
Pipermail (Mailman edition) and