clarified modules: avoid multiple uses of the same ML file;
clarified concrete vs. abstract syntax;
--- a/NEWS Wed Dec 23 20:49:05 2020 +0100
+++ b/NEWS Wed Dec 23 21:06:31 2020 +0100
@@ -103,8 +103,6 @@
*** HOL ***
-* Session "Hoare" now provides a total correctness logic as well.
-
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
@@ -213,6 +211,11 @@
* Syntax for reflected term syntax is organized in bundle term_syntax,
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
+* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
+abstract language constructors.
+
+* Session "HOL-Hoare": now provides a total correctness logic as well.
+
*** FOL ***
--- a/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 20:49:05 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 21:06:31 2020 +0100
@@ -2,15 +2,18 @@
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 1998 TUM
Author: Walter Guttmann (extension to total-correctness proofs)
-
-Sugared semantic embedding of Hoare logic.
-Strictly speaking a shallow embedding (as implemented by Norbert Galm
-following Mike Gordon) would suffice. Maybe the datatype com comes in useful
-later.
*)
+section \<open>Sugared semantic embedding of Hoare logic\<close>
+
+text \<open>
+ Strictly speaking a shallow embedding (as implemented by Norbert Galm
+ following Mike Gordon) would suffice. Maybe the datatype com comes in useful
+ later.
+\<close>
+
theory Hoare_Logic
-imports Hoare_Tac
+imports Hoare_Syntax Hoare_Tac
begin
type_synonym 'a bexp = "'a set"
@@ -19,14 +22,9 @@
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
-| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
-| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
-
-syntax
- "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-translations
- "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+| Seq "'a com" "'a com"
+| Cond "'a bexp" "'a com" "'a com"
+| While "'a bexp" "'a assn" "'a var" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -35,16 +33,22 @@
inductive Sem :: "'a com \<Rightarrow> 'a sem"
where
"Sem (Basic f) s (f s)"
-| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
-| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
-| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
| "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
Sem (While b x y c) s s'"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
+
+definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "ValidTC p c q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
+
inductive_cases [elim!]:
- "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
- "Sem (IF b THEN c1 ELSE c2 FI) s s'"
+ "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
+ "Sem (Cond b c1 c2) s s'"
lemma Sem_deterministic:
assumes "Sem c s s1"
@@ -57,12 +61,6 @@
using assms by simp
qed
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
-
-definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c s t \<and> t \<in> q)"
-
lemma tc_implies_pc:
"ValidTC p c q \<Longrightarrow> Valid p c q"
by (metis Sem_deterministic Valid_def ValidTC_def)
@@ -71,30 +69,6 @@
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (metis ValidTC_def)
-syntax
- "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
-
-syntax
- "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax (output)
- "_hoare" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
-
-ML_file \<open>hoare_syntax.ML\<close>
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
-
-syntax
- "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax (output)
- "_hoare_tc" :: "['a assn,'a com,'a assn] => bool"
- ("[_] // _ // [_]" [0,55,0] 50)
-
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close>
-
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
@@ -102,7 +76,7 @@
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
by (auto simp:Valid_def)
lemma CondRule:
@@ -111,11 +85,11 @@
by (auto simp:Valid_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
+ assumes "Sem (While b i v c) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
using assms
- by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
+ by (induct "While b i v c" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
@@ -139,7 +113,7 @@
lemma SeqRuleTC:
assumes "ValidTC p c1 q"
and "ValidTC q c2 r"
- shows "ValidTC p (c1;c2) r"
+ shows "ValidTC p (Seq c1 c2) r"
by (meson assms Sem.intros(2) ValidTC_def)
lemma CondRuleTC:
@@ -193,6 +167,22 @@
qed
+subsection \<open>Concrete syntax\<close>
+
+setup \<open>
+ Hoare_Syntax.setup
+ {Basic = \<^const_syntax>\<open>Basic\<close>,
+ Skip = \<^const_syntax>\<open>annskip\<close>,
+ Seq = \<^const_syntax>\<open>Seq\<close>,
+ Cond = \<^const_syntax>\<open>Cond\<close>,
+ While = \<^const_syntax>\<open>While\<close>,
+ Valid = \<^const_syntax>\<open>Valid\<close>,
+ ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
+\<close>
+
+
+subsection \<open>Proof methods: VCG\<close>
+
declare BasicRule [Hoare_Tac.BasicRule]
and SkipRule [Hoare_Tac.SkipRule]
and SeqRule [Hoare_Tac.SeqRule]
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 20:49:05 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 21:06:31 2020 +0100
@@ -2,12 +2,12 @@
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 2003 TUM
Author: Walter Guttmann (extension to total-correctness proofs)
-
-Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors.
*)
+section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
+
theory Hoare_Logic_Abort
-imports Hoare_Tac
+imports Hoare_Syntax Hoare_Tac
begin
type_synonym 'a bexp = "'a set"
@@ -17,14 +17,9 @@
datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Abort
-| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
-| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
-
-syntax
- "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-translations
- "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+| Seq "'a com" "'a com"
+| Cond "'a bexp" "'a com" "'a com"
+| While "'a bexp" "'a assn" "'a var" "'a com"
abbreviation annskip ("SKIP") where "SKIP == Basic id"
@@ -35,18 +30,18 @@
"Sem (Basic f) None None"
| "Sem (Basic f) (Some s) (Some (f s))"
| "Sem Abort s None"
-| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
-| "Sem (IF b THEN c1 ELSE c2 FI) None None"
-| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
-| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
+| "Sem (Cond b c1 c2) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
| "Sem (While b x y c) None None"
| "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
Sem (While b x y c) (Some s) s'"
inductive_cases [elim!]:
- "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
- "Sem (IF b THEN c1 ELSE c2 FI) s s'"
+ "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
+ "Sem (Cond b c1 c2) s s'"
lemma Sem_deterministic:
assumes "Sem c s s1"
@@ -73,30 +68,6 @@
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
by (meson ValidTC_def)
-syntax
- "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
-
-syntax
- "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax (output)
- "_hoare_abort" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
-
-ML_file \<open>hoare_syntax.ML\<close>
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
-
-syntax
- "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax (output)
- "_hoare_abort_tc" :: "['a assn,'a com,'a assn] => bool"
- ("[_] // _ // [_]" [0,55,0] 50)
-
-parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
-print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>
-
text \<open>The proof rules for partial correctness\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
@@ -105,7 +76,7 @@
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
by (auto simp:Valid_def)
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
by (auto simp:Valid_def)
lemma CondRule:
@@ -114,11 +85,11 @@
by (fastforce simp:Valid_def image_def)
lemma While_aux:
- assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
+ assumes "Sem (While b i v c) s s'"
shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
using assms
- by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
+ by (induct "While b i v c" s s') auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
@@ -147,7 +118,7 @@
lemma SeqRuleTC:
assumes "ValidTC p c1 q"
and "ValidTC q c2 r"
- shows "ValidTC p (c1;c2) r"
+ shows "ValidTC p (Seq c1 c2) r"
by (meson assms Sem.intros(4) ValidTC_def)
lemma CondRuleTC:
@@ -201,7 +172,35 @@
qed
-subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
+subsection \<open>Concrete syntax\<close>
+
+setup \<open>
+ Hoare_Syntax.setup
+ {Basic = \<^const_syntax>\<open>Basic\<close>,
+ Skip = \<^const_syntax>\<open>annskip\<close>,
+ Seq = \<^const_syntax>\<open>Seq\<close>,
+ Cond = \<^const_syntax>\<open>Cond\<close>,
+ While = \<^const_syntax>\<open>While\<close>,
+ Valid = \<^const_syntax>\<open>Valid\<close>,
+ ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
+\<close>
+
+\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
+syntax
+ "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
+ "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
+translations
+ "P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI"
+ "a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
+ \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
+
+text \<open>
+ Note: there is no special syntax for guarded array access. Thus
+ you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
+\<close>
+
+
+subsection \<open>Proof methods: VCG\<close>
declare BasicRule [Hoare_Tac.BasicRule]
and SkipRule [Hoare_Tac.SkipRule]
@@ -234,18 +233,4 @@
SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
"verification condition generator plus simplification"
-\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
-syntax
- "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
- "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
-translations
- "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
- "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
- \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
-
-text \<open>
- Note: there is no special syntax for guarded array access. Thus
- you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
-\<close>
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare_Syntax.thy Wed Dec 23 21:06:31 2020 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/Hoare/Hoare_Syntax.thy
+ Author: Leonor Prensa Nieto & Tobias Nipkow
+ Author: Walter Guttmann (extension to total-correctness proofs)
+
+Concrete syntax for Hoare logic, with translations for variables.
+*)
+
+theory Hoare_Syntax
+ imports Main
+begin
+
+syntax
+ "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" ("(2_ :=/ _)" [70, 65] 61)
+ "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(_;/ _)" [61,60] 60)
+ "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
+ "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+
+syntax
+ "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
+translations
+ "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
+
+syntax
+ "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+ "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
+syntax (output)
+ "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50)
+ "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50)
+
+ML_file \<open>hoare_syntax.ML\<close>
+
+end
--- a/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 20:49:05 2020 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 21:06:31 2020 +0100
@@ -7,14 +7,41 @@
signature HOARE_SYNTAX =
sig
- val hoare_vars_tr: term list -> term
- val hoare_tc_vars_tr: term list -> term
- val spec_tr': string -> term list -> term
+ val hoare_vars_tr: Proof.context -> term list -> term
+ val hoare_tc_vars_tr: Proof.context -> term list -> term
+ val spec_tr': string -> Proof.context -> term list -> term
+ val setup:
+ {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
+ Valid: string, ValidTC: string} -> theory -> theory
end;
structure Hoare_Syntax: HOARE_SYNTAX =
struct
+(** theory data **)
+
+structure Data = Theory_Data
+(
+ type T =
+ {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
+ Valid: string, ValidTC: string} option;
+ val empty: T = NONE;
+ val extend = I;
+ fun merge (data1, data2) =
+ if is_some data1 andalso is_some data2 andalso data1 <> data2 then
+ error "Cannot merge syntax from different Hoare Logics"
+ else merge_options (data1, data2);
+);
+
+fun const_syntax ctxt which =
+ (case Data.get (Proof_Context.theory_of ctxt) of
+ SOME consts => which consts
+ | NONE => error "Undefined Hoare syntax consts");
+
+val syntax_const = Syntax.const oo const_syntax;
+
+
+
(** parse translation **)
local
@@ -54,35 +81,33 @@
(* com_tr *)
-fun com_tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
- Syntax.const \<^const_syntax>\<open>Basic\<close> $ mk_fexp x e xs
- | com_tr (Const (\<^const_syntax>\<open>Basic\<close>,_) $ f) _ = Syntax.const \<^const_syntax>\<open>Basic\<close> $ f
- | com_tr (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) xs =
- Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs =
- Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ V $ c) xs =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs
- | com_tr t _ = t;
+fun com_tr ctxt =
+ let
+ fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
+ syntax_const ctxt #Basic $ mk_fexp x e xs
+ | tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
+ syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs
+ | tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
+ syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs
+ | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ I $ V $ c) xs =
+ syntax_const ctxt #While $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ tr c xs
+ | tr t _ = t;
+ in tr end;
fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
| vars_tr t = [t];
in
-fun hoare_vars_tr [vars, pre, prg, post] =
+fun hoare_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const \<^const_syntax>\<open>Valid\<close> $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+ in syntax_const ctxt #Valid $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);
-fun hoare_tc_vars_tr [vars, pre, prg, post] =
+fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const \<^const_syntax>\<open>ValidTC\<close> $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts);
+ in syntax_const ctxt #ValidTC $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end
+ | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);
end;
@@ -139,32 +164,55 @@
(* com_tr' *)
-fun mk_assign f =
+fun mk_assign ctxt f =
let
val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+ val (ch, (a, b)) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
in
if ch
- then Syntax.const \<^syntax_const>\<open>_assign\<close> $ fst which $ snd which
- else Syntax.const \<^const_syntax>\<open>annskip\<close>
+ then Syntax.const \<^syntax_const>\<open>_assign\<close> $ a $ b
+ else syntax_const ctxt #Skip
end;
-fun com_tr' (Const (\<^const_syntax>\<open>Basic\<close>, _) $ f) =
- if is_f f then mk_assign f
- else Syntax.const \<^const_syntax>\<open>Basic\<close> $ f
- | com_tr' (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) =
- Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) =
- Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ V $ c) =
- Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c
- | com_tr' t = t;
+fun com_tr' ctxt t =
+ let
+ val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
+ fun arg k = nth args (k - 1);
+ val n = length args;
+ in
+ (case head of
+ NONE => t
+ | SOME c =>
+ if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
+ mk_assign ctxt (arg 1)
+ else if c = const_syntax ctxt #Seq andalso n = 2 then
+ Syntax.const \<^syntax_const>\<open>_Seq\<close> $ com_tr' ctxt (arg 1) $ com_tr' ctxt (arg 2)
+ else if c = const_syntax ctxt #Cond andalso n = 3 then
+ Syntax.const \<^syntax_const>\<open>_Cond\<close> $
+ bexp_tr' (arg 1) $ com_tr' ctxt (arg 2) $ com_tr' ctxt (arg 3)
+ else if c = const_syntax ctxt #While andalso n = 4 then
+ Syntax.const \<^syntax_const>\<open>_While\<close> $
+ bexp_tr' (arg 1) $ assn_tr' (arg 2) $ var_tr' (arg 3) $ com_tr' ctxt (arg 4)
+ else t)
+ end;
in
-fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q;
+fun spec_tr' syn ctxt [p, c, q] =
+ Syntax.const syn $ assn_tr' p $ com_tr' ctxt c $ assn_tr' q;
end;
+
+(** setup **)
+
+fun setup consts =
+ Data.put (SOME consts) #>
+ Sign.parse_translation
+ [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
+ (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)] #>
+ Sign.print_translation
+ [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
+ (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
+
end;
-