*To*: Michel <michel.levy2009 at laposte.net>, Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] isar in PIDE : strange behavior*From*: Makarius <makarius at sketis.net>*Date*: Sat, 4 Mar 2017 16:43:58 +0100*Cc*: Isabelle User <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <7752d53f-bfcd-e6a1-fbb0-46c322550908@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> <1488478407.13177.23.camel@in.tum.de> <7752d53f-bfcd-e6a1-fbb0-46c322550908@laposte.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

On 03/03/17 15:26, Michel via Cl-isabelle-users wrote: > Thank you really much for your examples. I try to write basic proofs if > it possible without automation and with your suggestion it was possible. > I have written a software <http://teachinglogic.liglab.fr/DN/> (a long > time ago) to produce proof in natural deduction. > > This software was originally written in Prolog by Robert StÃrk, who was > assistant at ETH ZÃrich. I try to see if the proofs given by this > software can be translated in Isar. That is the origin of my questions > on Isar. > > Lawrence Paulson has said : Itâs essential to understand that âproofâ by > itself will attempt to use the default proof method. But this default > proof method can lead to an unprovable goal. The main Isar proof scheme is as follows: from facts1 have goal using facts2 proof method1 ... qed method2 The body "..." then consists recursively of sub-proofs, each with a local context: fix parameters assume premises show conclusion <proof> These usually address each sub-goal in turn, but the order is arbitrary. The "next" command may be used to proceed with a fresh local context; alternatively it is always possible to use { ... } to indicate context block structure. The initial refinement of "proof method1" uses facts = facts1 facts2 (appended in that order) and passes that to the proof method. It is "standard" by default; "standard" is a bit more than just "rule", but usually it is sufficient to think of "rule" as the standard step. The terminal method2 has a chance to finish-off remaining sub-goals (it may be omitted). Afterwards there is always an implicit stage to finish everything implicitly by-assumption. Some important abbreviations: proof method1 qed method2 == by method1 method2 .. == by standard . == by this Proof method "standard" applies a standard rule: the facts are put into its premises (in that order), the remaining rule is applied to the goal. Proof method "this" applies all "used" facts directly, without putting a rule in between. To apply these Isar principles in practice, I recommend to take all the Natural Deduction rules for predicate logic as examples, and turn them into canonical Isar proof outlines, e.g. like this for conjunction: have "A â B" proof show A sorry show B sorry qed next assume *: "A â B" then have A .. from * have B .. The double projection is a bit awkward. Better eliminate conjunction simultaneously: assume "A â B" then obtain A B .. Etc. ... Here is http://teachinglogic.liglab.fr/DN/index.php?formula=p+%26+q+%3D%3E+q+%26+p&action=Prove+Formula in Isar: have "A â B â B â A" proof assume "A â B" then obtain B A .. then show "B â A" .. qed You can enclose the above snippets into "notepad begin ... end", to avoid having toplevel theorem statements (which have separate syntax). I also recommend to start Isar without ever writing Pure rule statements in the text: these somehow belong to the "implementation" of logic and are rarely needed in proof texts. > I think the indication above on how to prove a thesis must be written in > the tutorial prog-prove or an another short tutorial on > the manner to write proofs in Isar. After more than 30 years, the situation of Isabelle manuals is very complex. Everything can be found somewhere, but it might take time to find it. Moreover, some old materials needs to be ignored, especially when getting started. Makarius

**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

**Re: [isabelle] isar in PIDE : strange behavior***From:*Peter Lammich

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

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