diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 10 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 10 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 6 |
3 files changed, 13 insertions, 13 deletions
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 54f58fad..500d260d 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -32,10 +32,10 @@ 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" +| Read_memt: "((Read_memt rk addr sz k), E_read_memt 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" +| Write_memt: "((Write_memt wk addr sz v t k), E_write_memt 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" @@ -62,8 +62,8 @@ lemma Traces_cases: 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_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" + | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces" + | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt 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" @@ -81,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_tagged_mem rk addr sz k v) + case (Read_memt 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 d99dfc85..05ae99ee 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -83,9 +83,9 @@ 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_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 +lemma liftState_read_memt[liftState_simp]: + shows "liftState r (read_memt BCa BCb rk a sz) = read_memtS BCa BCb rk a sz" + by (auto simp: read_memt_def read_memt_bytes_def maybe_failS_def read_memtS_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) @@ -93,7 +93,7 @@ lemma liftState_read_tagged_mem[liftState_simp]: lemma liftState_read_mem[liftState_simp]: 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 + read_memtS_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) @@ -422,7 +422,7 @@ lemma emitEventS_update_cases: assumes "emitEventS ra e s = Some s'" obtains (Write_mem) wk addr sz v tag r - where "e = E_write_mem wk addr sz v tag r" + where "e = E_write_memt wk addr sz v tag r" and "s' = put_mem_bytes addr sz v tag s" | (Write_reg) r v rs' where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'" diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index ca7e5751..d870c4a8 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -212,15 +212,15 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in lemma no_throw_mem_builtins: "\<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>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_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>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS 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>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_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def + unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_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 |