[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.