diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy | 6 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index 2f2d43ef..56aa6e87 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -32,7 +32,7 @@ datatype 'regval event = (* 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_tagv bitU bool + | e_write_tag "bitU list" bitU bool (* Tell the system to dynamically recalculate dependency footprint *) | e_footprint (* Request a memory barrier *) @@ -50,7 +50,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, ' | 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_tagv: "((Write_tagv v k), e_write_tagv 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" @@ -79,7 +79,7 @@ lemma Traces_cases: | (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_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv 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" diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index 746fd315..291157f5 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -274,7 +274,7 @@ lemma no_throw_mem_builtins: "\<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>t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a 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 |