Re: [isabelle] Formal semantics for Isar structured proof language



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.