diff options
Diffstat (limited to 'lib/isabelle/Sail2_prompt_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 500d260d..3658296b 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -35,6 +35,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, ' | 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 k), E_write_mem wk addr sz v 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" @@ -63,6 +64,7 @@ lemma Traces_cases: 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_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_mem) wk addr sz val k v t' where "m = Write_mem wk addr sz val k" and "t = E_write_mem wk addr sz val v # t'" and "(k v, 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" |