Make partiality more explicit in library functions of Lem shallow embedding

Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits.  Undefined
cases can be handled in different ways:

- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
  default so far),
- return an option type,
- raise a failure  in the monad, or
- use a bitstream oracle to resolve undefined bits.

This patch adds different versions of partial functions corresponding to those
options.  The desired behaviour can be selected by choosing a binding in the
Sail prelude.  The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.

4 files changed, 115 insertions, 146 deletions

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 688dfa07..d6bcf9bb 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -23,10 +23,10 @@ Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy
 Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy
+Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy Prompt.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy
+Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy Prompt.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
 Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy
diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy
index 2114d991..df2fc808 100644
--- a/lib/isabelle/Sail_values_lemmas.thy
+++ b/lib/isabelle/Sail_values_lemmas.thy
@@ -2,6 +2,8 @@ theory Sail_values_lemmas
   imports Sail_values
 begin
 
+lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def)
+
 termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def)
 
 termination index_list
@@ -21,32 +23,67 @@ lemma just_list_cases:
         | (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 bitops_bitU_of_bool[simp]:
+  "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<and> y)"
+  "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<or> y)"
+  "xor_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool ((x \<or> y) \<and> \<not>(x \<and> y))"
+  "not_bit (bitU_of_bool x) = bitU_of_bool (\<not>x)"
+  "not_bit \<circ> bitU_of_bool = bitU_of_bool \<circ> Not"
+  by (auto simp: bitU_of_bool_def not_bit_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 bool_of_bitU_bitU_of_bool[simp]:
+  "bool_of_bitU \<circ> bitU_of_bool = Some"
+  "bool_of_bitU \<circ> (bitU_of_bool \<circ> f) = Some \<circ> f"
+  "bool_of_bitU (bitU_of_bool x) = Some x"
+  by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+
+
+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_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_def
+  length_mword_def access_mword_def access_mword_inc_def access_mword_dec_def
+  (*update_mword_def update_mword_inc_def update_mword_dec_def*)
+  subrange_list_def subrange_list_inc_def subrange_list_dec_def
+  update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def
+
+lemma BC_mword_simps[simp]:
+  "unsigned_method BC_mword a = Some (uint a)"
+  "signed_method BC_mword a = Some (sint a)"
+  "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))"
+  by (auto simp: BC_mword_defs word_size)
 
 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])
+  "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))"
+  by (induction acc bs rule: nat_of_bools_aux.induct)
+     (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits)
 
-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 nat_of_bits_bl_to_bin[simp]: "nat_of_bools bs = nat (bl_to_bin bs)"
+  by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux)
 
-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_mword[simp]:
+  "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)"
+  by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_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"
+lemma bits_of_bitU_list[simp]:
+  "bits_of_method BC_bitU_list v = v"
+  "of_bits_method BC_bitU_list v = Some v"
   by (auto simp: BC_bitU_list_def)
 
+lemma access_list_dec_rev_nth:
+  assumes "0 \<le> i" and "nat i < size xs"
+  shows "access_list_dec xs i = rev xs ! (nat i)"
+  using assms
+  by (auto simp: access_list_dec_def access_list_inc_def length_list_def rev_nth
+           intro!: arg_cong2[where f = List.nth])
+
+lemma access_bv_dec_mword[simp]:
+  fixes w :: "('a::len) word"
+  assumes "0 \<le> n" and "nat n < LENGTH('a)"
+  shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))"
+  using assms
+  by (auto simp: access_bv_dec_def access_list_def access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl word_size)
+
 end
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index d8ab5db9..36fb987f 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -26,6 +26,8 @@ lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS (
 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_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def)
+lemma liftState_maybe_fail[simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
+  by (auto simp: maybe_fail_def maybe_failS_def split: option.splits)
 
 lemma liftState_try_catch[simp]:
   "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
@@ -47,19 +49,26 @@ 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]:
+lemma liftState_read_mem_BC:
   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]
+  using assms
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def split: option.splits)
+
+lemma liftState_read_mem[simp]:
+  "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
+  "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz"
+  by (auto simp: liftState_read_mem_BC)
 
 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"
+  shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat 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_write_mem_ea[simp]:
+  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)"
+  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
+  by (auto simp: liftState_write_mem_ea_BC)
 
 lemma liftState_write_mem_val:
   "liftState r (write_mem_val BC v) = write_mem_valS BC v"
@@ -80,7 +89,7 @@ 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)
+  using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS)
 
 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"
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index 291157f5..e7286fcf 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -4,23 +4,15 @@ theory State_monad_lemmas
     Sail_values_lemmas
 begin
 
-context
+(*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> \<Union>(bindS_aux f ` ms)"
+begin*)
 
 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'"
   shows "bindS m1 f1 s = bindS m2 f2 s"
   using assms unfolding bindS_def by (auto split: result.splits)
-(* proof -
-  have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2"
-    using f by (auto split: result.splits)
-  then show ?thesis using m by (auto simp: bindS_def)
-qed *)
 
 lemma bindS_cong[fundef_cong]:
   assumes m: "m1 = m2"
@@ -29,21 +21,16 @@ lemma bindS_cong[fundef_cong]:
   using assms by (intro ext bindS_ext_cong; blast)
 
 lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x"
-  by (auto simp add: bindS_def)
+  by (auto simp add: bindS_def returnS_def)
 
 lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)"
-  by (intro ext) (auto simp: bindS_def split: result.splits)
-(* 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 *)
+  by (intro ext) (auto simp: bindS_def returnS_def split: result.splits)
 
 lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)"
-  by (auto simp: bindS_def)
+  by (auto simp: bindS_def readS_def returnS_def)
 
 lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
-  by (auto simp: bindS_def)
+  by (auto simp: bindS_def updateS_def returnS_def)
 
 
 lemma result_cases:
@@ -84,17 +71,6 @@ lemma monadS_eqI:
   shows "m = m'"
   using assms by (intro ext monadS_ext_eqI)
 
-lemma
-  assumes "(Value a, s') \<in> bindS m f s"
-  obtains a' s'' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''"
-  using assms by (auto simp: bindS_def split: result.splits)
-
-lemma
-  assumes "(Ex e, s') \<in> bindS m f s"
-  obtains (Left) "(Ex e, s') \<in> m s"
-  | (Right) a s'' where "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''"
-  using assms by (auto simp: bindS_def split: result.splits)
-
 lemma bindS_cases:
   assumes "(r, s') \<in> bindS m f s"
   obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''"
@@ -110,15 +86,9 @@ lemma bindS_intros:
 
 lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)"
   by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI)
-(*proof -
-  have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) =
-        List.concat (map (bindS_aux (\<lambda>x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs
-    by (induction xs) (auto split: result.splits)
-  then show ?thesis unfolding bindS_def by auto
-qed*)
-
-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)
+
+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)
 declare seqS_def[simp]
 
 lemma Value_bindS_elim:
@@ -132,18 +102,10 @@ lemma Ex_bindS_elim:
   | (Right) s'' a' where "(Value a', s'') \<in> m s" and "(Ex e, s') \<in> f a' s''"
   using assms by (auto elim: bindS_cases)
 
-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> \<Union>(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: try_catchS_def)
+  by (auto simp: try_catchS_def returnS_def failS_def throwS_def)
 
 lemma try_catchS_cong[cong]:
   assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s"
@@ -155,13 +117,14 @@ lemma try_catchS_cases:
   obtains (Value) a where "r = Value a" and "(Value a, s') \<in> m s"
   | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \<in> m s"
   | (h) e s'' where "(Ex (Throw e), s'') \<in> m s" and "(r, s') \<in> h e s''"
-  using assms by (cases r rule: result_cases) (auto simp: try_catchS_def split: result.splits ex.splits)
+  using assms
+  by (cases r rule: result_cases) (auto simp: try_catchS_def returnS_def split: result.splits ex.splits)
 
 lemma try_catchS_intros:
   "\<And>m h s a s'. (Value a, s') \<in> m s \<Longrightarrow> (Value a, s') \<in> try_catchS m h s"
   "\<And>m h s msg s'. (Ex (Failure msg), s') \<in> m s \<Longrightarrow> (Ex (Failure msg), s') \<in> try_catchS m h s"
   "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s"
-  by (auto simp: try_catchS_def intro: bexI[rotated])
+  by (auto simp: try_catchS_def returnS_def intro: bexI[rotated])
 
 fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where
   "ignore_throw_aux (Value a, s') = {(Value a, s')}"
@@ -169,42 +132,23 @@ fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2)
 | "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}"
 definition "ignore_throw m s \<equiv> \<Union>(ignore_throw_aux ` m s)"
 
-(*fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) list" where
-  "ignore_throw_aux 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')})"
-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 [simp]:
+lemma ignore_throw_cong:
+  assumes "\<And>s. m1 s = m2 s"
+  shows "ignore_throw m1 = ignore_throw m2"
+  using assms by (auto simp: ignore_throw_def)
+
+lemma ignore_throw_aux_member_simps[simp]:
   "(Value a, s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Value a, s')"
   "(Ex (Throw e), s') \<in> ignore_throw_aux ms \<longleftrightarrow> False"
   "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')"
   by (cases ms rule: result_state_cases; auto)+
 
-(*lemma [simp]: "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s"
+lemma ignore_throw_member_simps[simp]:
+  "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s"
   "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s"
   "(Ex (Throw e), s') \<in> ignore_throw m s \<longleftrightarrow> False"
-  "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')"
-  by (auto simp: ignore_throw_def)*)
+  "(Ex (Failure msg), s') \<in> ignore_throw m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m s"
+  by (auto simp: ignore_throw_def)
 
 lemma ignore_throw_cases:
   assumes no_throw: "ignore_throw m s = m s"
@@ -232,43 +176,21 @@ proof
   also have "\<dots> = bindS m2 (\<lambda>a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto
   finally show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" .
 qed
-(*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_throwI:
-  fixes m1 :: "('regs, 'a, 'e1) monadS" and m2 :: "('regs, 'a, 'e2) monadS"
-  assumes "\<And>a s'. (Value a, s') \<in> m1 s \<longleftrightarrow> (Value a, s') \<in> m2 s"
-    and "\<And>msg s'. (Ex (Failure msg), s') \<in> m1 s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m2 s"
-    and "\<And>e s'. (Ex (Throw e), s') \<notin> m1 s"
-    and "\<And>e s'. (Ex (Throw e), s') \<notin> m2 s"
-  shows "ignore_throw m1 s = m2 s"
-  using assms by (intro monadS_ext_eqI) (auto simp: ignore_throw_def)*)
-
-(*lemma no_throw_bindSI:
-  assumes "ignore_throw m1 s = m2 s"
-and "\<And>a s'. (Value a, s') \<in> m2 s \<Longrightarrow> ignore_throw (f1 a) s' = f2 a s'"
-shows "ignore_throw (bindS m1 f1) s = bindS m2 f2 s"
-  using assms unfolding ignore_throw_bindS apply (intro monadS_ext_eqI) apply auto apply (auto elim!: bindS_cases intro: bindS_intros)
-   defer thm bindS_intros
-   apply (intro bindS_intros(3)) apply auto
-  apply (intro bindS_intros(3)) apply auto
-  done
-
-lemma
-  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
-  unfolding read_mem_bytesS_def Let_def seqS_def
-  apply (intro no_throw_bindSI)
-  oops*)
+
+lemma no_throw_basic_builtins[simp]:
+  "ignore_throw (returnS a) = returnS a"
+  "\<And>f. ignore_throw (readS f) = readS f"
+  "\<And>f. ignore_throw (updateS f) = updateS f"
+  "ignore_throw (chooseS xs) = chooseS xs"
+  "ignore_throw (failS msg) = failS msg"
+  "ignore_throw (maybe_failS msg x) = maybe_failS msg x"
+  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def
+  by (intro ext; auto split: option.splits)+
+
+lemmas ignore_throw_option_case_distrib =
+  option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s]
 
 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"
@@ -280,20 +202,21 @@ lemma no_throw_mem_builtins:
   unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def
   unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def
   unfolding excl_resultS_def undefined_boolS_def
-  by (auto simp: ignore_throw_def bindS_def chooseS_def Let_def split: option.splits prod.splits)
+  by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
+           simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def)
 
 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_ext_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: ignore_throw_def bindS_def split: option.splits)
+  by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
 
 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: ignore_throw_def bindS_def split: option.splits)
+  by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
 
-lemmas no_throw_builtins[simp, intro] =
+lemmas no_throw_builtins[simp] =
   no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
 
-end
+(* end *)
 
 end