*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 23 Nov 2012 10:28:46 +1100*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <04665034-67AE-4672-9101-A05F7AA8C385@cam.ac.uk>*References*: <50921697.9090307@cococo.de> <50921DCB.6050502@rsise.anu.edu.au> <alpine.LNX.2.00.1211162218270.24652@macbroy20.informatik.tu-muenchen.de> <50A728D8.2070105@rsise.anu.edu.au> <E20FDEC0-25AE-4C90-B51B-0510141A586B@cam.ac.uk> <50AABBDD.70700@rsise.anu.edu.au> <98A92B35-BD03-4E31-B0E5-BBD552920CF6@cam.ac.uk> <50AC4179.7070101@rsise.anu.edu.au> <49EAB30D-6FC1-4B09-A576-12094F24F98A@cam.ac.uk> <50AD562E.5090103@rsise.anu.edu.au> <04665034-67AE-4672-9101-A05F7AA8C385@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.13) Gecko/20101209 Fedora/3.1.7-0.35.b3pre.fc14 Thunderbird/3.1.7

On 11/22/2012 10:32 PM, Lawrence Paulson wrote:

You still have the capacity to code your own proof procedures; ML is just one level down. And you get a much more readable proof language.

Larry,

Some years ago, I translated a lot of proofs from HOL to Isabelle. The HOL proofs were opaque blocks of tactics, while in the corresponding structure proof you could see (even if you knew little of the Isar language) which local facts were available for use and what had to be proved. And almost certainly, creating those opaque blocks of tactics required much more effort, because the old ML style (whether in HOL or Isabelle) isn't very good at forward reasoning.

Jeremy

Larry On 21 Nov 2012, at 22:31, Jeremy Dawson<jeremy at rsise.anu.edu.au> wrote:Given that in HOL (as in Isabelle, both pre and post Isar) one can always use proof procedures coded by someone else, this seems to sum up to saying that Isabelle/Isar is like HOL, minus the capacity to code one's own proof procedures, plus -- what ??

**References**:**[isabelle] Length of Proofs***From:*Jens Doll

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Makarius

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: Re: [isabelle] Length of Proofs
- Previous by Thread: Re: [isabelle] Length of Proofs
- Next by Thread: Re: [isabelle] Length of Proofs
- Cl-isabelle-users November 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