*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] intro rule for &&&*From*: Makarius <makarius at sketis.net>*Date*: Sat, 22 Dec 2012 12:39:01 +0100 (CET)*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <471B2DE1-DDC9-4526-8248-AFA898FB5B29@cam.ac.uk>*References*: <471B2DE1-DDC9-4526-8248-AFA898FB5B29@cam.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 20 Dec 2012, John Wickerson wrote:

When I type...lemma assumes "A ∧ B" shows "A" "B" using assms apply rule...I obtain the following proof state...goal (2 subgoals): 1. A ⟹ B ⟹ A 2. B... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.goal (2 subgoals): 1. A ⟹ B ⟹ A 2. A ⟹ B ⟹ BBy the way, I know I can solve this lemma via auto; my question ispedagogical rather than practical.

notepad begin assume ab: "A & B" from ab have A and A apply rule apply assumption using ab apply rule apply assumption done from ab obtain A and B .. end General notes on it: * 'notepad' is better for experimentation than old-fashioned 'lemma', because it gives you the full proof language. In top-level theorem statements your possibilities to indicate proof structure are more limited and one has to simulate things, and obscure the main points more than necessary. There is also the initial goal hanging around, but proof is not primarily about goals. * The fact "ab" (or your assms) need to be eliminated twice to work on the two goals "A" and "B". The "rule" method implicitly refers to conjE, but it works on the head goal only. Note that in old-fashioned tactical reasoning, you would simulate a local fact like "ab" via some goal premise "A & B ==> ...", and "apply (erule conjE)" would consume that, and the result would indeed become insoluble as you've said. In proper Isar, the context grows monotonically, and things can be used again as required. * My second proof above via 'obtain' does the elimination of fact "ab" in a single step, saying that it is possible to assume A and B simultaneously thanks to the (implicit) conjE rule. Recall that ".." abbreviates "by rule" (actually "by default", which is a bit more). Formally, there is only one goal behind 'obtain', so it works in a single rule application step, not two. It would be more awkward to prove: from ab have A and B sorry which are two goals again. Since the context of assumptions is commutative, you may swap the obtain result in-place like this: from ab obtain B and A .. Putting it all together, here is my canonical starter proof for Isar: assume "A & B" then obtain B and A .. then have "B & A" .. You can also make implicit rules explicit like this: assume "A & B" then obtain B and A by (rule conjE) then have "B & A" by (rule conjI)

assume ab: "A & B" from ab have a: A by (rule conjD1) from ab have b: B by (rule conjD2) from b and a have "B & A" by (rule conjI)

assume "A & B" then have B .. from `A & B` have A .. with `B` have "B & A" ..

Makarius

**References**:**[isabelle] intro rule for &&&***From:*John Wickerson

- Previous by Date: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Next by Date: Re: [isabelle] intro rule for &&&
- Previous by Thread: Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]
- Next by Thread: [isabelle] Fwd: Isabelle2012 - What distribution?
- Cl-isabelle-users December 2012 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