From 2529f5a65d70dfffe40ead73ae49aaa4d78fefb4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:47:28 +0100
Subject: Add some syntactic sugar for Isabelle

---
 lib/isabelle/Hoare.thy                    | 4 ++--
 lib/isabelle/Sail2_state_monad_lemmas.thy | 3 +++
 src/state.ml                              | 6 +++---
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index afa953be..88807c7c 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -13,7 +13,7 @@ subsection \<open>Hoare triples\<close>
 
 type_synonym 'regs predS = "'regs sequential_state \<Rightarrow> bool"
 
-definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool"
+definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>")
   where "PrePost P f Q \<equiv> (\<forall>s. P s \<longrightarrow> (\<forall>(r, s') \<in> f s. Q r s'))"
 
 lemma PrePostI:
@@ -211,7 +211,7 @@ there is an exception.
 [1] D. Cock, G. Klein, and T. Sewell, ‘Secure Microkernels, State Monads and Scalable Refinement’,
 in Theorem Proving in Higher Order Logics, 2008, pp. 167–182.\<close>
 
-definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool"
+definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_ \<bar> _\<rbrace>")
   where "PrePostE P f Q E \<equiv> PrePost P f (\<lambda>v. case v of Value a \<Rightarrow> Q a | Ex e \<Rightarrow> E e)"
 
 lemmas PrePost_defs = PrePost_def PrePostE_def
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 91e4c17e..3a286c10 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -8,6 +8,9 @@ begin
   notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp]
 begin*)
 
+notation bindS (infixr "\<bind>\<^sub>S" 54)
+notation seqS (infixr "\<then>\<^sub>S" 54)
+
 lemma bindS_ext_cong[fundef_cong]:
   assumes m: "m1 s = m2 s"
     and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
diff --git a/src/state.ml b/src/state.ml
index e788ab6a..245d450c 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -367,15 +367,15 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
     let id' = remove_trailing_underscores id in
     separate_map hardline string [
       "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\"";
+      "  \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\"";
       "  by (auto simp: liftState_read_reg_readS register_defs)";
       "";
       "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
+      "  \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
       "  by (auto simp: liftState_write_reg_updateS register_defs)"
     ]
   in
-  string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
+  string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
   hardline ^^ hardline ^^
   register_defs ^^
   hardline ^^ hardline ^^
-- 
cgit v1.2.3