diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index e8148597..8be5cc6b 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -91,7 +91,7 @@ lemma liftState_read_memt[liftState_simp]: split: option.splits intro: bindS_cong) lemma liftState_read_mem[liftState_simp]: - shows "liftState r (read_mem BCa BCb rk asz a sz) = read_memS BCa BCb rk a sz" + shows "liftState r (read_mem BCa BCb rk asz a sz) = read_memS BCa BCb rk asz a sz" by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def read_memtS_def prod.case_distrib option.case_distrib[where h = "liftState r"] @@ -118,7 +118,7 @@ lemma liftState_write_memt[liftState_simp]: by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits) lemma liftState_write_mem[liftState_simp]: - "liftState r (write_mem BCa BCv wk addrsize addr sz v) = write_memS BCa BCv wk addr sz v" + "liftState r (write_mem BCa BCv wk addrsize addr sz v) = write_memS BCa BCv wk addrsize addr sz v" by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp split: option.splits) diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 1e9f50cc..2fbd7a56 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -214,11 +214,11 @@ 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_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 asz a sz s. ignore_throw (read_memS BCa BCv rk asz a sz) s = read_memS BCa BCv rk asz 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 s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s" "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s" - "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s" + "\<And>BCa BCv wk asz addr sz v s. ignore_throw (write_memS BCa BCv wk asz addr sz v) s = write_memS BCa BCv wk asz addr sz v s" "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS 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" |