diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 12 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 25d4edea..edcd9593 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -93,19 +93,19 @@ lemma liftState_read_mem[liftState_simp]: by (auto simp: liftState_read_mem_BC) lemma liftState_write_mem_ea_BC: - assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" + assumes "unsigned_method BCa a = Some a'" shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()" - using assms by (auto simp: write_mem_ea_def) + using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def) -lemma liftState_write_mem_ea[liftState_simp]: +(*lemma liftState_write_mem_ea[liftState_simp]: "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()" "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()" - by (auto simp: liftState_write_mem_ea_BC) + by (auto simp: liftState_write_mem_ea_BC)*) -lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]: +(*lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]: "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t = write_mem_bytesS BC_mword wk addr sz v t" - by (auto simp: write_mem_bytesS_def) + by (auto simp: write_mem_bytesS_def)*) lemma liftState_write_mem_val[liftState_simp]: "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t" diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index b2fde7ba..6fb5e7ef 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -211,9 +211,9 @@ 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 BC rk a sz) s = read_mem_bytesS BC rk a sz s" + "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" - "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t 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>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" |