Fix Isabelle library

3 files changed, 55 insertions, 66 deletions

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 25eb9f52..406b5871 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -30,42 +30,17 @@ lemma All_try_catch_dom: "try_catch_dom (m, h)"
 termination try_catch using All_try_catch_dom by auto
 lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct
 
-datatype 'regval event =
-  (* Request to read memory *)
-    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 "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_tag "bitU list" bitU bool
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | e_footprint
-  (* Request a memory barrier *)
-  | e_barrier " barrier_kind "
-  (* Request to read register *)
-  | e_read_reg string 'regval
-  (* Request to write register *)
-  | e_write_reg string 'regval
-  | e_undefined bool
-  | e_print string
-
 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_tag: "((Write_tag a v k), e_write_tag a 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"
-| Undefined: "((Undefined k), e_undefined v, k v) \<in> T"
-| Print: "((Print msg k), e_print msg, k) \<in> T"
+  Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz 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_mem: "((Write_mem wk addr sz v t k), E_write_mem wk addr sz v t 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"
+| Undefined: "((Undefined k), E_undefined v, k v) \<in> T"
+| Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -85,25 +60,28 @@ 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_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a 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"
-  | (Undefined) xs v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
-  | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
+  | (Read_mem) rk addr s k t' v tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag 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"
+  | (Undefined) xs v k t' where "m = Undefined k" and "t = E_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # 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)
+  note t = \<open>t = e # t'\<close>
+  note m' = \<open>(m'', t', m') \<in> Traces\<close>
+  from \<open>(m, e, m'') \<in> T\<close> and t and m'
+  show ?thesis proof (cases m e m'' rule: T.cases)
+    case (Read_mem rk addr sz k v)
+    then show ?thesis using t m' by (cases v; elim that; blast)
+  qed (elim that; blast)+
 qed
 
 abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index ba69d0d8..25d4edea 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -18,7 +18,7 @@ lemma Value_liftState_Run:
   assumes "(Value a, s') \<in> 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;
+      simp add: failS_def throwS_def returnS_def del: read_regvalS.simps;
       blast elim: Value_bindS_elim)
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
@@ -82,7 +82,10 @@ 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_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits)
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+                 prod.case_distrib option.case_distrib[where h = "liftState r"]
+                 option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+           cong: option.case_cong)
 
 lemma liftState_read_mem[liftState_simp]:
   "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
@@ -91,17 +94,22 @@ lemma liftState_read_mem[liftState_simp]:
 
 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 (nat sz)"
-  using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+  shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
+  using assms by (auto simp: write_mem_ea_def)
 
 lemma liftState_write_mem_ea[liftState_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)"
+  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()"
+  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()"
   by (auto simp: liftState_write_mem_ea_BC)
 
+lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+  "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t =
+   write_mem_bytesS BC_mword wk addr sz v t"
+  by (auto simp: write_mem_bytesS_def)
+
 lemma liftState_write_mem_val[liftState_simp]:
-  "liftState r (write_mem_val BC v) = write_mem_valS BC v"
-  by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
+  "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
+  by (auto simp: write_mem_def write_memS_def liftState_simp 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)"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 3a286c10..b2fde7ba 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -205,24 +205,27 @@ lemma no_throw_basic_builtins[simp]:
 
 lemmas ignore_throw_option_case_distrib =
   option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s]
+  option.case_distrib[where h = "\<lambda>c. ignore_throw c" and option = "c" for c]
+
+lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in ignore_throw (f x))"
+  by auto
 
 lemma no_throw_mem_builtins:
   "\<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>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t s"
+  "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  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
+  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_memS_def
+  unfolding write_mem_bytesS_def
+  unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
+  unfolding ignore_throw_bindS
   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)
+           simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_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)
+  by (auto simp: read_memS_def no_throw_mem_builtins prod.case_distrib comp_def 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: option.case_distrib cong: bindS_cong option.case_cong)