*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Formal semantics for Isar structured proof language*From*: "Elsa L. Gunter" <egunter at illinois.edu>*Date*: Wed, 18 Feb 2015 20:39:06 -0600*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAAPnxw2eiatdNJ89raCm_iO=ri5x_=PqYrFECj84mtF03Lbaqg@mail.gmail.com>*References*: <54E508FB.6070104@illinois.edu> <CAAPnxw2eiatdNJ89raCm_iO=ri5x_=PqYrFECj84mtF03Lbaqg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear Alfio,

---Elsa On 2/18/15 8:28 PM, Alfio Martini wrote:

Dear Elsa,I have just a working knowledge of Isar and Isabelle. But byexperience tells me thatwhen you use the method "by (rule R)" in a forward way, the premisesof the goal have to matchexactly the premises of the rule. In this case, the rule mp is codedin Isabelle like this:?P-->?Q ==> ?P ==>?QSo, the first premise in you third proof is only "A" and thus does notmatchthe implication of the rule. In such cases, using "simp" will suffice.Anyway, I am sure a more technical and precise answer will follow thismessage.Best!On Wed, Feb 18, 2015 at 7:49 PM, Elsa L. Gunter <egunter at illinois.edu<mailto:egunter at illinois.edu>> wrote:Dear Isabelle Community, Does there exist / where can I find a formal semantics for the Isar structured proof scripting language? The syntax of the Isar proof scripting language is defined fairly formally in Section 6 of The Isabelle / Isar Reference Manual and it is accompanied by an informal and high level English explanation of each construct or group of construct, but I have not yet found a formal description of the language, via, say, something like modular structural operational semantics. I'm not looking for any one particular style of semantics, but I would like something rigorous enough that it could be expressed in Isabelle, and rigorous enough so that it would explain why lemma fixes A and B shows "A â (A â B) â B" proof (rule impI) assume A: "A" show "(A â B) â B" proof (rule impI) assume AB: "A â B" from AB and A show "B" by (rule mp) qed qed and lemma fixes A and B shows "A â (A â B) â B" proof (rule impI) assume A: "A" show "(A â B) â B" proof (rule impI) assume AB: "A â B" from AB and A show "B" by (rule impE) qed qed both succeed, but lemma fixes A and B shows "A â (A â B) â B" proof (rule impI) assume A: "A" show "(A â B) â B" proof (rule impI) assume AB: "A â B" from A and AB show "B" by (rule mp) qed qed fails at by (rule mp). ---Elsa Elsa L Gunter Department of Computer Science University of Illinois at Urbana - Champaign -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio <http://www.inf.pucrs.br/alfio> Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] Formal semantics for Isar structured proof language***From:*Alfio Martini

**References**:**[isabelle] Formal semantics for Isar structured proof language***From:*Elsa L. Gunter

**Re: [isabelle] Formal semantics for Isar structured proof language***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Formal semantics for Isar structured proof language
- Next by Date: Re: [isabelle] Formal semantics for Isar structured proof language
- Previous by Thread: Re: [isabelle] Formal semantics for Isar structured proof language
- Next by Thread: Re: [isabelle] Formal semantics for Isar structured proof language
- Cl-isabelle-users February 2015 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