From 336522767a1c3b564fd4798851993afef9f629ed Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 9 May 2020 22:10:49 +0100 Subject: Make Isabelle lemma generation work with grouped regstate --- lib/isabelle/Hoare.thy | 16 ++++++++++++++++ lib/isabelle/Sail2_state_lemmas.thy | 12 ++++++------ 2 files changed, 22 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 98b7d077..848cd042 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -96,6 +96,14 @@ lemma PrePost_readS[intro, PrePost_atomI]: "PrePost (\s. P (Value (f s)) lemma PrePost_updateS[intro, PrePost_atomI]: "PrePost (\s. P (Value ()) (f s)) (updateS f) P" unfolding PrePost_def updateS_def returnS_def by auto +lemma PrePost_read_regS[intro, PrePost_atomI]: + "PrePost (\s. P (Value (read_from reg (regstate s))) s) (read_regS reg) P" + unfolding read_regS_def by (rule PrePost_readS) + +lemma PrePost_write_regS[intro, PrePost_atomI]: + "PrePost (\s. P (Value ()) (s\regstate := write_to reg v (regstate s)\)) (write_regS reg v) P" + unfolding write_regS_def by (rule PrePost_updateS) + lemma PrePost_if: assumes "b \ PrePost P f Q" and "\b \ PrePost P g Q" shows "PrePost P (if b then f else g) Q" @@ -311,6 +319,14 @@ lemma PrePostE_readS[PrePostE_atomI, intro]: "PrePostE (\s. Q (f s) s) ( lemma PrePostE_updateS[PrePostE_atomI, intro]: "PrePostE (\s. Q () (f s)) (updateS f) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_read_regS[PrePostE_atomI, intro]: + "PrePostE (\s. Q (read_from reg (regstate s)) s) (read_regS reg) Q E" + unfolding read_regS_def by (rule PrePostE_readS) + +lemma PrePostE_write_regS[PrePostE_atomI, intro]: + "PrePostE (\s. Q () (s\regstate := write_to reg v (regstate s)\)) (write_regS reg v) Q E" + unfolding write_regS_def by (rule PrePostE_updateS) + lemma PrePostE_if_branch[PrePostE_compositeI]: assumes "b \ PrePostE Pf f Q E" and "\b \ PrePostE Pg g Q E" shows "PrePostE (if b then Pf else Pg) (if b then f else g) Q E" diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 8be5cc6b..8fbcf093 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -122,22 +122,22 @@ lemma liftState_write_mem[liftState_simp]: by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp split: option.splits) -lemma liftState_read_reg_readS: +lemma liftState_read_reg: assumes "\s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)" - shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \ regstate)" + shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg" proof fix s :: "'a sequential_state" obtain rv v where "get_regval' (name reg) (regstate s) = Some rv" and "of_regval reg rv \ Some v" and "read_from reg (regstate s) = v" using assms unfolding bind_eq_Some_conv by blast - then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \ regstate) s" + then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s" by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def) qed -lemma liftState_write_reg_updateS: +lemma liftState_write_reg: assumes "\s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)" - shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))" - using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS) + shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v" + using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS write_regS_def) lemma liftState_iter_aux[liftState_simp]: shows "liftState r (iter_aux i f xs) = iterS_aux i (\i x. liftState r (f i x)) xs" -- cgit v1.2.3