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> wrote:
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

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
current behavior.

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,
- Brian

OK, this really sheds light on what happens there.
Thanks Brian.


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