*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] isar in PIDE : strange behavior*From*: Peter Lammich <lammich at in.tum.de>*Date*: Thu, 02 Mar 2017 19:13:27 +0100*In-reply-to*: <dc11bfee-3eab-cb9c-c8a6-6c60d6d955e7@laposte.net>*References*: <c80a975f-0be4-4777-7748-228789b9afc2@laposte.net> <245FCB71-E0D5-4E7B-8918-6BE6B39F3255@cam.ac.uk> <dc11bfee-3eab-cb9c-c8a6-6c60d6d955e7@laposte.net>

Just note that this highly nested proof structure is very unusual in practice.Â The parenthesis structure of your goal is a bit misleading. TryÂ Â term "(p â (q â r)) â (q â (p â r))"ÂÂ to see how it looks with only necessary parenthesis: Â "(p â q â r) â q â p â r" Chains of implications are a very common thing in HOL, and usually you handle them all at once by repeated implication introduction ... there is no need to open a new nesting level for every single impI: Â ÂÂ Â lemma "(p â (q â r)) â (q â (p â r))"ÂÂ Â proof (intro impI) having done this, the proof is almost as easy as you would write it down on paper. You have several stylistic possibilities here. You could number your assumptions: ÂÂÂÂassume 1: "p â (q â r)" and 2: "q" and 3: "p" ÂÂÂÂfrom 1 have "qâr" using 3 by (rule mp) ÂÂÂÂthen show "r" using 2 by (rule mp) Â qedÂÂÂÂÂÂ ÂÂÂÂ or you could refer to the short assumptions explicitly by fact antiquotations (note that you have to assume them anyway): Â lemma "(p â (q â r)) â (q â (p â r))"ÂÂ Â proof (intro impI) ÂÂÂÂassume "q" "p" ÂÂÂÂassume "p â (q â r)"Â ÂÂÂÂthen have "qâr" using âpâ by (rule mp) ÂÂÂÂthen show "r" using âqâ by (rule mp) Â qed Â Â Â I posted this email because I feel that this thread has the potential to scare new Isabelle users and leave them with the impression they need deeply nested lengthy proofs to handle simple chains of implications ... Note to more advanced beginners: Usually, you never state top-level implications on the HOL level, but you use the meta-level directly, e.g., you would write: Â lemma "(p â (q â r)) â q â p â r" or, equivalently: Â lemma "â(p â (q â r)); q; pâ â r"Â Â proof - ÂÂÂÂassume "q" "p" ÂÂÂÂassume "p â (q â r)"Â ÂÂÂÂthen have "qâr" using âpâ by (rule mp) ÂÂÂÂthen show "r" using âqâ by (rule mp) Â qedÂÂÂÂÂÂ (whether to use brackets or chains of implications is a matter of taste, and actually, brackets are just syntactic sugar for chains of implication. I, personally, find brackets easier to read.) Even more likely, you would use the long-goal format, which saves you from re-stating the assumptions in the proof: Â lemmaÂ ÂÂÂÂassumes 1: "(p â (q â r))" and "q" "p"Â ÂÂÂÂshows "r"ÂÂ Â proof - ÂÂÂÂfrom 1 have "qâr" using âpâ by (rule mp) ÂÂÂÂthen show "r" using âqâ by (rule mp) Â qed Â Â Â -- Â Peter On Do, 2017-03-02 at 18:21 +0100, Michel via Cl-isabelle-users wrote: > To understand Isar, I try to write proofs without automation. > I have understood that after the word "proof", PIDE try to apply the > implicit rule of the formula to prove and with "r", such a rule does > not exists. > But with show "r" using 1, it's worst. > > Intuitively, the proof of "r" is simple. > 4: "q --> r" by mp (modus ponens) on 1, 3 > "r" by mp on 4, 2 > Why it's impossible to write this in Isar ? > How to avoid the implicit use of rules? > > lemma trivial3isar : "(p â (q â r)) â (q â (p â r))" > Â proof > ÂÂÂÂassume 1: "p â (q â r)" > ÂÂÂÂshow "q â (p â r)" > ÂÂÂÂproof > ÂÂÂÂÂÂassume 2: "q" > ÂÂÂÂÂÂshow "p â r" > ÂÂÂÂÂÂproof > ÂÂÂÂÂÂÂÂassumeÂÂ3: "p" > ÂÂÂÂÂÂÂÂshow "r" > ÂÂÂÂÂÂÂÂÂÂusing 1 > ÂÂÂÂÂÂÂÂproof > > With show "r" using 1,ÂÂthe last proof gives two unsolvable goals > 1 (q --> r)==> r > 2 p --> (q --> r) ==> p > > > Le 02/03/2017 Ã 16:41, Lawrence Paulson a Ãcrit : > > > > > > > > On 2 Mar 2017, at 15:03, Michel via Cl-isabelle-users <cl-isabell > > > e-users at lists.cam.ac.uk> wrote: > > > > > > As a beginner, I tried another elementary proof with jedit. > > > > > > But during the proof, I have strange messages in the output > > > window and 4 proof and only 3 qed. > > > > > > lemma trivial3isar : "(p â (q â r)) â (q â (p â r))" > > > Â proof > > > ÂÂÂÂassume "p â (q â r)" > > > ÂÂÂÂshow "q â (p â r)" > > > ÂÂÂÂproof > > > ÂÂÂÂÂÂassume "q" > > > ÂÂÂÂÂÂshow "p â r" > > > ÂÂÂÂÂÂproof > > > ÂÂÂÂÂÂÂÂassumeÂÂ"p" > > > ÂÂÂÂÂÂÂÂshow "r" > > > ÂÂÂÂÂÂÂÂproof > > Itâs essential to understand that âproofâ by itself will attempt to > > use the default proof method, but there is none for the formula r. > > > > At this stage, you have two alternatives. One is to continue in > > this single-step style by feeding in one of your previous > > assumptions; the other is finally to use a little automation. So > > possibly this (note the introduced label): > > > > Â lemma trivial3isar : "(p â (q â r)) â (q â (p â r))" > > Â proof > > ÂÂÂÂassume 1: "p â (q â r)" > > ÂÂÂÂshow "q â (p â r)" > > ÂÂÂÂproof > > ÂÂÂÂÂÂassume "q" > > ÂÂÂÂÂÂshow "p â r" > > ÂÂÂÂÂÂproof > > ÂÂÂÂÂÂÂÂassumeÂÂ"p" > > ÂÂÂÂÂÂÂÂshow "r" > > ÂÂÂÂÂÂÂÂÂÂusing 1 > > ÂÂÂÂÂÂÂÂproof > > > > Alternatively, this: > > > > ÂÂÂÂÂÂÂÂshow "r" > > ÂÂÂÂÂÂÂÂÂÂby (simp add: "1" âpâ âqâ) > > > > Larry Paulson > >

**Follow-Ups**:**Re: [isabelle] isar in PIDE : strange behavior***From:*Lawrence Paulson

**Re: [isabelle] isar in PIDE : strange behavior***From:*Michel via Cl-isabelle-users

**References**:**[isabelle] isar in jedit : strange behavior***From:*Michel via Cl-isabelle-users

**Re: [isabelle] isar in jedit : strange behavior***From:*Lawrence Paulson

**Re: [isabelle] isar in PIDE : strange behavior***From:*Michel via Cl-isabelle-users

- Previous by Date: Re: [isabelle] isar in PIDE : strange behavior
- Next by Date: Re: [isabelle] Cancellation simprocs
- Previous by Thread: Re: [isabelle] isar in PIDE : strange behavior
- Next by Thread: Re: [isabelle] isar in PIDE : strange behavior
- Cl-isabelle-users March 2017 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