# HG changeset patch
# User wenzelm
# Date 1608753991 -3600
# Node ID b1be35908165959e4b25e3e3382589a49ddbdd8d
# Parent  d231d71d27b4621e141a39447eb12ae5888b2b54
clarified modules: avoid multiple uses of the same ML file;
clarified concrete vs. abstract syntax;

diff -r d231d71d27b4 -r b1be35908165 NEWS
--- 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 ***
 
diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Logic.thy
--- 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]
diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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
diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Syntax.thy
--- /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
diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/hoare_syntax.ML
--- 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;
-