*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] surprising behavior of schematic_lemma*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Tue, 16 Apr 2013 11:09:45 +0200*In-reply-to*: <CAAMXsiZBYPqaVuGjb3fjzxNgj73xUvqYQr3Wmpcqe5NkPza2+w@mail.gmail.com>*References*: <516BD4AD.8060509@in.tum.de> <CAAMXsiZBYPqaVuGjb3fjzxNgj73xUvqYQr3Wmpcqe5NkPza2+w@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

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: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.0I 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 before: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-April/msg00052.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-September/msg00044.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-December/msg00043.html https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00022.html 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. Ondrej

**References**:**[isabelle] surprising behavior of schematic_lemma***From:*Ondřej Kunčar

**Re: [isabelle] surprising behavior of schematic_lemma***From:*Brian Huffman

- Previous by Date: [isabelle] 2nd CFP: SCSS 2013
- Next by Date: Re: [isabelle] VDM maps and map comprehension in Isabelle
- Previous by Thread: Re: [isabelle] surprising behavior of schematic_lemma
- Next by Thread: [isabelle] Two PhD Positions in Multicore Computing at the UPMARC Center of Excellence, Uppsala University
- Cl-isabelle-users April 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list