Re: [isabelle] surprising behavior of schematic_lemma
On 04/15/2013 10:51 PM, Brian Huffman wrote:
On Mon, Apr 15, 2013 at 3:21 AM, Ondřej Kunčar <kuncar at in.tum.de> 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
I don't have any workaround to offer, but I think I can explain the
Step 1: When you prove the goal using "show", this proposition is
immediately generalized over a1, a2 and A (i.e. it is "exported"). You
can see the exported result in the goals buffer:
Successful attempt to solve goal by exported rule:
?a1.2 ∈ ?A2 ⟹ ?a2.2 ∈ ?A2 ⟹ ?a1.2 = ?a1.2 ∧ ?a2.2 = ?a2.2
Step 2: The exported rule is applied to the first matching goal in the
current proof state. The new proof state is not shown by default, but
you can see it by inserting a "next" before the "qed":
goal (2 subgoals):
1. ⟦?A; ?B⟧ ⟹ ?a1.8 ∈ ?A8
2. ⟦?A; ?B⟧ ⟹ ?a2.8 ∈ ?A8
Applying the exported rule usually discharges a goal, but in this case
it has introduced two new ones! This is what happens when you use
meta-implication with "show", as has been discussed several times
Step 3: Processing "qed" causes all remaining subgoals to be solved by
assumption. Solving goal 1 unifies ?A with "?a1.8 ∈ ?A8", leaving goal
2 looking something like this:
⟦?a1.8 ∈ ?A8; ?B⟧ ⟹ ?a2.8 ∈ ?A8
Now it unifies the conclusion with the first matching assumption, so
?a1.8 gets unified to ?a2.8. Finally this results in the surprising
theorem you found.
Hope this helps,
OK, this really sheds light on what happens there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and