diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 6 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 27 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 14 |
3 files changed, 27 insertions, 20 deletions
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 406b5871..c59fc62f 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -32,6 +32,7 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr 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_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_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" @@ -60,7 +61,8 @@ 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 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" + | (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_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_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" @@ -79,7 +81,7 @@ next 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) + case (Read_tagged_mem rk addr sz k v) then show ?thesis using t m' by (cases v; elim that; blast) qed (elim that; blast)+ qed diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index c7d55d31..77f4ac5a 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -80,19 +80,20 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]: "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b" by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_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_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def +lemma liftState_read_tagged_mem[liftState_simp]: + shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz" + by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_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) + split: option.splits intro: bindS_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" - "\<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) + shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" + by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def + read_tagged_memS_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 + split: option.splits intro: bindS_cong) lemma liftState_write_mem_ea_BC: assumes "unsigned_method BCa a = Some a'" @@ -399,7 +400,10 @@ text \<open>Event traces\<close> lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" unfolding bind_eq_Some_conv[symmetric] by auto -lemma if_then_Some_eq_Some: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" +lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)" by auto lemma emitEventS_update_cases: @@ -413,7 +417,8 @@ lemma emitEventS_update_cases: and "s' = s\<lparr>regstate := rs'\<rparr>" | (Read) "s' = s" using assms - by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some) + by (elim emitEventS.elims) + (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff) lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" by (cases "emitEventS ra e s"; auto) diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 6fb5e7ef..12452ca4 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -211,22 +211,22 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in by auto lemma no_throw_mem_builtins: - "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" + "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" + "\<And>rk a sz s. ignore_throw (read_tagged_mem_bytesS rk a sz) s = read_tagged_mem_bytesS rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_tagged_memS BCa BCv rk a sz) s = read_tagged_memS BCa BCv rk a sz s" "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS 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>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv 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_memS_def + unfolding read_mem_bytesS_def read_tagged_mem_bytesS_def read_tagged_memS_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: 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 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) @@ -234,7 +234,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) lemmas no_throw_builtins[simp] = - no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS + no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS (* end *) |