*To*: "Elsa L. Gunter" <egunter at illinois.edu>*Subject*: Re: [isabelle] Formal semantics for Isar structured proof language*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Thu, 19 Feb 2015 00:28:00 -0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <54E508FB.6070104@illinois.edu>*References*: <54E508FB.6070104@illinois.edu>*Sender*: alfio.martini at gmail.com

Dear Elsa, I have just a working knowledge of Isar and Isabelle. But by experience tells me that when you use the method "by (rule R)" in a forward way, the premises of the goal have to match exactly the premises of the rule. In this case, the rule mp is coded in Isabelle like this: ?P-->?Q ==> ?P ==>?Q So, the first premise in you third proof is only "A" and thus does not match the implication of the rule. In such cases, using "simp" will suffice. Anyway, I am sure a more technical and precise answer will follow this message. Best! On Wed, Feb 18, 2015 at 7:49 PM, Elsa L. Gunter <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 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:*Elsa L. Gunter

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

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