Add/generate Isabelle lemmas about the monad lifting

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

5 files changed, 367 insertions, 30 deletions

diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy
index e93c6052..9d29f5a2 100644
--- a/lib/isabelle/Prompt_monad_extras.thy
+++ b/lib/isabelle/Prompt_monad_extras.thy
@@ -1,5 +1,7 @@
 theory Prompt_monad_extras
-  imports Prompt_monad
+  imports
+    Prompt_monad
+    Sail_values_extras
 begin
 
 lemma All_bind_dom: "bind_dom (m, f)"
@@ -21,14 +23,18 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 datatype 'regval event =
   (* Request to read memory *)
-    e_read_mem read_kind int int "memory_byte list"
+    e_read_mem read_kind "bitU list" nat "memory_byte list"
+  | e_read_tag "bitU list" bitU
   (* Write is imminent, at address lifted, of size nat *)
-  | e_write_ea write_kind int int
+  | e_write_ea write_kind "bitU list" nat
   (* Request the result of store-exclusive *)
   | e_excl_res bool
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
   | e_write_memv "memory_byte list" bool
+  | e_write_tagv bitU bool
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | e_footprint
   (* Request a memory barrier *)
   | e_barrier " barrier_kind "
   (* Request to read register *)
@@ -38,9 +44,12 @@ datatype 'regval event =
 
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
   Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
+| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \<in> T"
 | Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
 | Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
+| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \<in> T"
+| Footprint: "((Footprint k), e_footprint, k) \<in> T"
 | Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
@@ -59,6 +68,29 @@ lemmas Traces_ConsI = T.intros[THEN Step, rotated]
 inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces"
 inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces"
 
+lemma Traces_cases:
+  fixes m :: "('rv, 'a, 'e) monad"
+  assumes Run: "(m, t, m') \<in> Traces"
+  obtains (Nil) a where "m = m'" and "t = []"
+  | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
+  | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv val v # t'" and "(k v, t', m') \<in> Traces"
+  | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces"
+  | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
+  | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = e_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
+  | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
+  | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
+proof (use Run in \<open>cases m t m' set: Traces\<close>)
+  case Nil
+  then show ?thesis by (auto intro: that(1))
+next
+  case (Step e m'' t')
+  from \<open>(m, e, m'') \<in> T\<close> and \<open>t = e # t'\<close> and \<open>(m'', t', m') \<in> Traces\<close>
+  show ?thesis by (cases m e m'' rule: T.cases; elim that; blast)
+qed
+
 abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
   where "Run s t a \<equiv> (s, t, Done a) \<in> Traces"
 
@@ -114,11 +146,6 @@ lemma Run_DoneE:
 lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
   by (auto elim: Run_DoneE)
 
-lemma Run_BarrierE[elim!]:
-  assumes "Run (Barrier bk k) t a"
-  obtains t' where "t = e_barrier bk # t'" and "Run k t' a"
-  using assms by cases (auto elim: T.cases)
-
 lemma bind_cong[fundef_cong]:
   assumes m: "m1 = m2"
     and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a"
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index d826ea08..b07bc807 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -1,7 +1,7 @@
 session "Sail" = "LEM" +
   options [document = false]
   theories
-    Sail_values
+    Sail_values_extras
     Prompt
     State_extras
     Sail_operators_mwords
diff --git a/lib/isabelle/Sail_values_extras.thy b/lib/isabelle/Sail_values_extras.thy
new file mode 100644
index 00000000..66bcba48
--- /dev/null
+++ b/lib/isabelle/Sail_values_extras.thy
@@ -0,0 +1,52 @@
+theory Sail_values_extras
+  imports Sail_values
+begin
+
+termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def)
+
+termination index_list
+  by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto
+
+lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto
+
+lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs"
+  by (induction xs) (auto split: option.splits)
+
+lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys"
+  by (induction xs arbitrary: ys) (auto split: option.splits)
+
+lemma just_list_cases:
+  assumes "just_list xs = y"
+  obtains (None) "None \<in> set xs" and "y = None"
+        | (Some) ys where "xs = map Some ys" and "y = Some ys"
+  using assms by (cases y) auto
+
+abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict"
+lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def
+abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict"
+lemmas BC_mword_def = instance_Sail_values_Bitvector_Machine_word_mword_dict_def
+
+lemma image_bitU_of_bool_B0_B1: "bitU_of_bool ` bs \<subseteq> {B0, B1}"
+  by (auto simp: bitU_of_bool_def split: if_splits)
+
+lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \<circ> bitU_of_bool = id"
+  by (intro ext) (auto simp: bool_of_bitU_def bitU_of_bool_def)
+
+lemma nat_of_bits_aux_bl_to_bin_aux:
+  assumes "set bs \<subseteq> {B0, B1}"
+  shows "nat_of_bits_aux acc bs = nat (bl_to_bin_aux (map bool_of_bitU bs) (int acc))"
+  by (use assms in \<open>induction acc bs rule: nat_of_bits_aux.induct\<close>)
+     (auto simp: Bit_def bool_of_bitU_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux])
+
+lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bits (map bitU_of_bool bs) = nat (bl_to_bin bs)"
+  by (auto simp: nat_of_bits_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux image_bitU_of_bool_B0_B1)
+
+lemma unsigned_bits_of_mword:
+  "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = unsigned_method BC_mword a"
+  by (auto simp: BC_bitU_list_def BC_mword_def unsigned_of_bits_def)
+
+lemma unsigned_bits_of_bitU_list:
+  "unsigned_method BC_bitU_list (bits_of_method BC_bitU_list a) = unsigned_method BC_bitU_list a"
+  by (auto simp: BC_bitU_list_def)
+
+end
diff --git a/lib/isabelle/State_extras.thy b/lib/isabelle/State_extras.thy
index 096fb19b..924861b0 100644
--- a/lib/isabelle/State_extras.thy
+++ b/lib/isabelle/State_extras.thy
@@ -4,32 +4,187 @@ begin
 
 lemma All_liftState_dom: "liftState_dom (r, m)"
   by (induction m) (auto intro: liftState.domintros)
-
 termination liftState using All_liftState_dom by auto
 
+lemma liftState_bind[simp]:
+  "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
+  by (induction m f rule: bind.induct) auto
+
 lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def)
+
+lemma Value_liftState_Run:
+  assumes "(Value a, s') \<in> set (liftState r m s)"
+  obtains t where "Run m t a"
+  by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>;
+      auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
+      blast elim: Value_bindS_elim)
+
 lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def)
 lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def)
+lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def)
+lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def)
+lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def)
+lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def)
 
-lemma liftState_bind[simp]:
-  "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
-  by (induction m f rule: bind.induct) auto
+lemma liftState_try_catch[simp]:
+  "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
+  by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw)
+
+lemma liftState_early_return[simp]:
+  "liftState r (early_return r) = early_returnS r"
+  by (auto simp: early_return_def early_returnS_def)
+
+lemma liftState_catch_early_return[simp]:
+  "liftState r (catch_early_return m) = catch_early_returnS (liftState r m)"
+  by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong)
+
+lemma liftState_liftR[simp]:
+  "liftState r (liftR m) = liftSR (liftState r m)"
+  by (auto simp: liftR_def liftSR_def)
+
+lemma liftState_try_catchR[simp]:
+  "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)"
+  by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong)
+
+lemma liftState_read_mem_BC[simp]:
+  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
+  shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
+  using assms by (auto simp: read_mem_def read_memS_def read_mem_bytesS_def)
+lemmas liftState_read_mem[simp] =
+  liftState_read_mem_BC[OF unsigned_bits_of_mword] liftState_read_mem_BC[OF unsigned_bits_of_bitU_list]
+
+lemma liftState_write_mem_ea_BC:
+  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
+  shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a sz"
+  using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+lemmas liftState_write_mem_ea[simp] =
+  liftState_write_mem_ea_BC[OF unsigned_bits_of_mword] liftState_write_mem_ea_BC[OF unsigned_bits_of_bitU_list]
 
-lemma liftState_read_reg[intro]:
+lemma liftState_write_mem_val:
+  "liftState r (write_mem_val BC v) = write_mem_valS BC v"
+  by (auto simp: write_mem_val_def write_mem_valS_def split: option.splits)
+
+lemma liftState_read_reg_readS:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
-  shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg"
+  shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \<circ> regstate)"
 proof
   fix s :: "'a sequential_state"
   obtain rv v where "get_regval' (name reg) (regstate s) = Some rv"
-    and "of_regval reg rv = Some v" and "read_from reg (regstate s) = v"
+    and "of_regval reg rv \<equiv> Some v" and "read_from reg (regstate s) = v"
     using assms unfolding bind_eq_Some_conv by blast
-  then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s"
-    by (auto simp: read_reg_def bindS_def returnS_def read_regS_def)
+  then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \<circ> regstate) s"
+    by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def)
+qed
+
+lemma liftState_write_reg_updateS:
+  assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)"
+  shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))"
+  using assms by (auto simp: write_reg_def bindS_readS updateS_def returnS_def)
+
+lemma liftState_iter_aux[simp]:
+  shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs"
+  by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto cong: bindS_cong)
+
+lemma liftState_iteri[simp]:
+  "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs"
+  by (auto simp: iteri_def iteriS_def)
+
+lemma liftState_iter[simp]:
+  "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs"
+  by (auto simp: iter_def iterS_def)
+
+lemma liftState_foreachM[simp]:
+  "liftState r (foreachM xs vars body) = foreachS xs vars (\<lambda>x vars. liftState r (body x vars))"
+  by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
+     (auto cong: bindS_cong)
+
+lemma whileS_dom_step:
+  assumes "whileS_dom (vars, cond, body, s)"
+    and "(Value True, s') \<in> set (cond vars s)"
+    and "(Value vars', s'') \<in> set (body vars s')"
+  shows "whileS_dom (vars', cond, body, s'')"
+  by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>)
+     (auto intro: whileS.domintros)
+
+lemma whileM_dom_step:
+  assumes "whileM_dom (vars, cond, body)"
+    and "Run (cond vars) t True"
+    and "Run (body vars) t' vars'"
+  shows "whileM_dom (vars', cond, body)"
+  by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\<close>)
+     (auto intro: whileM.domintros)
+
+lemma whileM_dom_ex_step:
+  assumes "whileM_dom (vars, cond, body)"
+    and "\<exists>t. Run (cond vars) t True"
+    and "\<exists>t'. Run (body vars) t' vars'"
+  shows "whileM_dom (vars', cond, body)"
+  using assms by (blast intro: whileM_dom_step)
+
+lemmas whileS_pinduct = whileS.pinduct[case_names Step]
+
+lemma liftState_whileM:
+  assumes "whileS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)"
+    and "whileM_dom (vars, cond, body)"
+  shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \<circ> cond) (liftState r \<circ> body) s"
+proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: whileS.pinduct\<close>)
+  case Step: (1 vars s)
+  note domS = Step(1) and IH = Step(2) and domM = Step(3)
+  show ?case unfolding whileS.psimps[OF domS] whileM.psimps[OF domM] liftState_bind
+  proof (intro bindS_ext_cong, goal_cases cond while)
+    case (while a s')
+    have "bindS (liftState r (body vars)) (liftState r \<circ> (\<lambda>vars. whileM vars cond body)) s' =
+          bindS (liftState r (body vars)) (\<lambda>vars. whileS vars (liftState r \<circ> cond) (liftState r \<circ> body)) s'"
+      if "a"
+    proof (intro bindS_ext_cong, goal_cases body while')
+      case (while' vars' s'')
+      have "whileM_dom (vars', cond, body)" proof (rule whileM_dom_ex_step[OF domM])
+        show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run)
+        show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run)
+      qed
+      then show ?case using while while' that by (auto intro: IH)
+    qed auto
+    then show ?case by auto
+  qed auto
 qed
 
-lemma liftState_write_reg[intro]:
-  assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg s v)"
-  shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v"
-  using assms by (auto simp: write_reg_def bindS_def returnS_def write_regS_def)
+
+lemma untilM_dom_step:
+  assumes "untilM_dom (vars, cond, body)"
+    and "Run (body vars) t vars'"
+    and "Run (cond vars') t' False"
+  shows "untilM_dom (vars', cond, body)"
+  by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\<close>)
+     (auto intro: untilM.domintros)
+
+lemma untilM_dom_ex_step:
+  assumes "untilM_dom (vars, cond, body)"
+    and "\<exists>t. Run (body vars) t vars'"
+    and "\<exists>t'. Run (cond vars') t' False"
+  shows "untilM_dom (vars', cond, body)"
+  using assms by (blast intro: untilM_dom_step)
+
+lemma liftState_untilM:
+  assumes "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)"
+    and "untilM_dom (vars, cond, body)"
+  shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s"
+proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: untilS.pinduct\<close>)
+  case Step: (1 vars s)
+  note domS = Step(1) and IH = Step(2) and domM = Step(3)
+  show ?case unfolding untilS.psimps[OF domS] untilM.psimps[OF domM] liftState_bind
+  proof (intro bindS_ext_cong, goal_cases body k)
+    case (k vars' s')
+    show ?case unfolding comp_def liftState_bind
+    proof (intro bindS_ext_cong, goal_cases cond until)
+      case (until a s'')
+      have "untilM_dom (vars', cond, body)" if "\<not>a"
+      proof (rule untilM_dom_ex_step[OF domM])
+        show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run)
+        show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run)
+      qed
+      then show ?case using k until IH by (auto simp: comp_def)
+    qed auto
+  qed auto
+qed
 
 end
diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy
index eb8ed678..406aec79 100644
--- a/lib/isabelle/State_monad_extras.thy
+++ b/lib/isabelle/State_monad_extras.thy
@@ -1,15 +1,22 @@
 theory State_monad_extras
-  imports State_monad
+  imports
+    State_monad
+    Sail_values_extras
+begin
+
+context
+  notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp]
 begin
 
 abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> [(Ex e, s')])"
+abbreviation "bindS_app ms f \<equiv> List.concat (List.map (bindS_aux f) ms)"
 
 lemma bindS_ext_cong[fundef_cong]:
   assumes m: "m1 s = m2 s"
     and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
-  shows "(bindS m1 f1) s = (bindS m2 f2) s"
+  shows "bindS m1 f1 s = bindS m2 f2 s"
 proof -
-  have "List.concat (map (bindS_aux f1) (m2 s)) = List.concat (map (bindS_aux f2) (m2 s))"
+  have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2"
     using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits)
   then show ?thesis using m by (auto simp: bindS_def)
 qed
@@ -20,8 +27,21 @@ lemma bindS_cong[fundef_cong]:
   shows "bindS m1 f1 = bindS m2 f2"
   using assms by (blast intro: bindS_ext_cong)
 
-lemma bindS_returnS[simp]: "bindS (returnS x) m = m x"
-  by (auto simp add: bindS_def returnS_def)
+lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x"
+  by (auto simp add: bindS_def)
+
+lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)"
+proof -
+  have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list"
+    by (induction ms) (auto split: result.splits)
+  then show ?thesis unfolding bindS_def by blast
+qed
+
+lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)"
+  by (auto simp: bindS_def)
+
+lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
+  by (auto simp: bindS_def)
 
 lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)"
 proof -
@@ -31,13 +51,96 @@ proof -
   then show ?thesis unfolding bindS_def by auto
 qed
 
-lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def)
-lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def)
+lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def)
+lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def)
 declare seqS_def[simp]
 
+lemma Value_bindS_elim:
+  assumes "(Value a, s') \<in> set (bindS m f s)"
+  obtains s'' a' where "(Value a', s'') \<in> set (m s)" and "(Value a, s') \<in> set (f a' s'')"
+  using assms by (auto simp: bindS_def; split result.splits; auto)
+
+abbreviation
+  "try_catchS_aux h r \<equiv>
+    (case r of
+       (Value a, s') => returnS a s'
+     | (Ex (Throw e), s') => h e s'
+     | (Ex (Failure msg), s') => [(Ex (Failure msg), s')])"
+abbreviation "try_catchS_app ms h \<equiv> List.concat (List.map (try_catchS_aux h) ms)"
+
 lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a"
   and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg"
   and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e"
-  by (auto simp: returnS_def failS_def throwS_def try_catchS_def)
+  by (auto simp: try_catchS_def)
+
+lemma try_catchS_cong[cong]:
+  assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s"
+  shows "try_catchS m1 h1 = try_catchS m2 h2"
+  using assms by (intro arg_cong2[where f = try_catchS] ext) auto
+
+fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where
+  "ignore_throw_app [] = []"
+| "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms"
+| "ignore_throw_app ((Ex (Failure msg), s) # ms) = (Ex (Failure msg), s) # ignore_throw_app ms"
+| "ignore_throw_app ((Ex (Throw e), s) # ms) = ignore_throw_app ms"
+abbreviation ignore_throw :: "('r, 'a, 'e1) monadS \<Rightarrow> ('r, 'a, 'e2) monadS" where
+  "ignore_throw m \<equiv> \<lambda>s. ignore_throw_app (m s)"
+
+lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \<longleftrightarrow> False"
+  by (induction ms rule: ignore_throw_app.induct) auto
+
+lemma ignore_throw_app_append[simp]:
+  "ignore_throw_app (ms1 @ ms2) = ignore_throw_app ms1 @ ignore_throw_app ms2"
+  by (induction ms1 rule: ignore_throw_app.induct) auto
+
+lemma ignore_throw_app_bindS_app[simp]:
+  "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)"
+  by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)
+
+lemma ignore_throw_bindS[simp]:
+  "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \<circ> f)"
+  "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \<circ> f) s"
+  unfolding bindS_def by auto
+
+lemma try_catchS_bindS_no_throw:
+  fixes m1 :: "('r, 'a, 'e1) monadS" and m2 :: "('r, 'a, 'e2) monadS"
+  assumes m1: "\<And>s. ignore_throw m1 s = m1 s"
+    and m2: "\<And>s. ignore_throw m1 s = m2 s"
+  shows "try_catchS (bindS m1 f) h = bindS m2 (\<lambda>a. try_catchS (f a) h)"
+proof
+  fix s
+  have 1: "try_catchS_app (bindS_app ms f) h =
+        bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)"
+    if "ignore_throw_app ms = ms" for ms
+    using that by (induction ms rule: ignore_throw_app.induct) auto
+  then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s"
+    using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast
+qed
+
+lemma no_throw_mem_builtins:
+  "\<And>a. ignore_throw (returnS a) = returnS a"
+  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
+  "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
+  "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
+  "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
+  "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
+  "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s"
+  "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
+  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def write_mem_valS_def write_mem_bytesS_def write_tagS_def excl_resultS_def
+  by (auto simp: bindS_def chooseS_def Let_def split: option.splits)+
+
+lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
+  by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_cong)
+
+lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
+  by (cases r) (auto simp: bindS_def split: option.splits)
+
+lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s"
+  by (cases r) (auto simp: bindS_def split: option.splits)
+
+lemmas no_throw_builtins[simp, intro] =
+  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
+
+end
 
 end