Make Isabelle lemma generation work with grouped regstate

3 files changed, 26 insertions, 10 deletions

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 (\<lambda>s. P (Value (f s))
 lemma PrePost_updateS[intro, PrePost_atomI]: "PrePost (\<lambda>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 (\<lambda>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 (\<lambda>s. P (Value ()) (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) P"
+  unfolding write_regS_def by (rule PrePost_updateS)
+
 lemma PrePost_if:
   assumes "b \<Longrightarrow> PrePost P f Q" and "\<not>b \<Longrightarrow> 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 (\<lambda>s. Q (f s) s) (
 lemma PrePostE_updateS[PrePostE_atomI, intro]: "PrePostE (\<lambda>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 (\<lambda>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 (\<lambda>s. Q () (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) Q E"
+  unfolding write_regS_def by (rule PrePostE_updateS)
+
 lemma PrePostE_if_branch[PrePostE_compositeI]:
   assumes "b \<Longrightarrow> PrePostE Pf f Q E" and "\<not>b \<Longrightarrow> 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 "\<And>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 \<circ> 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 \<equiv> 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 \<circ> 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 "\<And>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 (\<lambda>i x. liftState r (f i x)) xs"
diff --git a/src/state.ml b/src/state.ml
index 478a3fd5..8d487d3e 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -410,12 +410,12 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
     let id' = remove_trailing_underscores id in
     separate_map hardline string [
       "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\"";
-      "  by (auto simp: liftState_read_reg_readS register_defs)";
+      "  \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = read_regS " ^ id ^ "_ref\"";
+      "  by (intro liftState_read_reg) (auto simp: register_defs)";
       "";
       "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
-      "  by (auto simp: liftState_write_reg_updateS register_defs)"
+      "  \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = write_regS " ^ id ^ "_ref v\"";
+      "  by (intro liftState_write_reg) (auto simp: register_defs)"
     ]
   in
   string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^