*To*: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>*Subject*: Re: [isabelle] problem with opening proof*From*: Makarius <makarius at sketis.net>*Date*: Thu, 28 May 2009 20:18:56 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <A56E563B-386D-4270-BD43-D21297A5266E@dsto.defence.gov.au>*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> <A56E563B-386D-4270-BD43-D21297A5266E@dsto.defence.gov.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Mon, 25 May 2009, Dr. Brendan Patrick Mahony wrote:

On 23/05/2009, at 7:13 PM, Makarius wrote:You should be able to ignore the "intro" and "elim" methods most of thetime -- they stem from a very early stage of Isar when structuredproofs were not fully understood yet.Is there any source I can access that describes this full understandingof structured proofs?

Generally, I see the structured proof game as coaxing the proof engineinto returning the particular proof state that I feel best explains thetruth of my proposition to the human reader.

To this end, I find intro and elim necessary quite often, when thedefault reasoning set returns a proof state that is incomprehensible toa human reader.

1997).

Obviously, it is suboptimal to have long convoluted chains of methodsthat result in the "obvious" goal state, since this will tend to makethe reader uneasy about the "formal nonsense" that is meant to bereassuring them about the quality of the proof being offered.

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" ..

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

**Re: [isabelle] problem with opening proof***From:*Dr. Brendan Patrick Mahony

- Previous by Date: [isabelle] ESSLLI 2009 Bordeaux: Program and Call for Participation
- Next by Date: Re: [isabelle] Very strange behaviour of interpretation
- 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