From 326e97e2ecaafaae75b841999fc94eed34e9a841 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 May 2019 11:01:55 +0100 Subject: Patch up a couple of Isabelle proofs due to memory interface changes --- lib/isabelle/Sail2_state_lemmas.thy | 4 ++-- lib/isabelle/Sail2_state_monad_lemmas.thy | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'lib') 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: "\rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" "\rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s" "\BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" - "\BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s" + "\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" "\BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s" "\BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s" "\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" - "\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" + "\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" "\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" "\s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" -- cgit v1.2.3