# [isabelle] Formal semantics for Isar structured proof language

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

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