*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] problem with opening proof*From*: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>*Date*: Mon, 25 May 2009 11:09:18 +0930*In-reply-to*: <alpine.LNX.1.10.0905231133180.20537@atbroy100.informatik.tu-muenchen.de>*References*: <737b61f30905212054n968f86di25c0c6e0bcb9308@mail.gmail.com> <4A1652EC.5050500@informatik.tu-muenchen.de> <737b61f30905221631s604eeffbu37010699ec4b5369@mail.gmail.com> <alpine.LNX.1.10.0905231133180.20537@atbroy100.informatik.tu-muenchen.de>

On 23/05/2009, at 7:13 PM, Makarius wrote: > You should be able to ignore the "intro" and "elim" methods most of > the time -- they stem from a very early stage of Isar when > structured proofs were not fully understood yet. Is there any source I can access that describes this full understanding of structured proofs? Generally, I see the structured proof game as coaxing the proof engine into returning the particular proof state that I feel best explains the truth of my proposition to the human reader. To this end, I find intro and elim necessary quite often, when the default reasoning set returns a proof state that is incomprehensible to a human reader. Since it is very hard to massage the default set into a manageable shape it is easiest to use a number of intro, elim and simp methods to get the desired proof state. Obviously, it is suboptimal to have long convoluted chains of methods that result in the "obvious" goal state, since this will tend to make the reader uneasy about the "formal nonsense" that is meant to be reassuring them about the quality of the proof being offered. However, it is certainly better than having a short chain of methods that result it an unintuitive or incomprehensible or even unexpectedly non-existent proof state. I still must say, that I can't follow the reasoning behind the way default/rule is implemented. My confusion is well described by the following examples, the first of which is a valid proof lemma assumes a1: "A" and a2: "B" shows "A & B" using a1 a2 .. lemma assumes a1: "A" and a2: "B" shows "A & B" using a2 a1 .. and the second of which is not. This can be seriously annoying when trying to chain facts assume b1: "B" have b2: "A" -- proof with b1 show "A & B" .. IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.

**Follow-Ups**:**Re: [isabelle] problem with opening proof***From:*Makarius

**References**:**[isabelle] problem with opening proof***From:*Chris Capel

**Re: [isabelle] problem with opening proof***From:*Florian Haftmann

**Re: [isabelle] problem with opening proof***From:*Chris Capel

**Re: [isabelle] problem with opening proof***From:*Makarius

- Previous by Date: [isabelle] 2nd Cfp: PCC09
- Next by Date: [isabelle] Interpretation with special cases
- Previous by Thread: Re: [isabelle] problem with opening proof
- Next by Thread: Re: [isabelle] problem with opening proof
- Cl-isabelle-users May 2009 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