Make named theorem collections of state monad more fine-grained

3 files changed, 93 insertions, 78 deletions

diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index a6c2ee3d..9271e2fa 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -42,19 +42,20 @@ lemma PrePost_weaken_post:
   shows "PrePost A f C"
   using assms by (blast intro: PrePost_consequence)
 
-named_theorems PrePost_intro
+named_theorems PrePost_compositeI
+named_theorems PrePost_atomI
 
-lemma PrePost_True_post[PrePost_intro, intro, simp]:
+lemma PrePost_True_post[PrePost_atomI, intro, simp]:
   "PrePost P m (\<lambda>_ _. True)"
   unfolding PrePost_def by auto
 
 lemma PrePost_any: "PrePost (\<lambda>s. \<forall>(r, s') \<in> m s. Q r s') m Q"
   unfolding PrePost_def by auto
 
-lemma PrePost_returnS[intro, PrePost_intro]: "PrePost (P (Value x)) (returnS x) P"
+lemma PrePost_returnS[intro, PrePost_atomI]: "PrePost (P (Value x)) (returnS x) P"
   unfolding PrePost_def returnS_def by auto
 
-lemma PrePost_bindS[intro, PrePost_intro]:
+lemma PrePost_bindS[intro, PrePost_compositeI]:
   assumes f: "\<And>s a s'. (Value a, s') \<in> m s \<Longrightarrow> PrePost (R a) (f a) Q"
     and m: "PrePost P m (\<lambda>r. case r of Value a \<Rightarrow> R a | Ex e \<Rightarrow> Q (Ex e))"
   shows "PrePost P (bindS m f) Q"
@@ -89,10 +90,10 @@ lemma PrePost_bindS_unit:
   shows "PrePost P (bindS m f) Q"
   using assms by auto
 
-lemma PrePost_readS[intro, PrePost_intro]: "PrePost (\<lambda>s. P (Value (f s)) s) (readS f) P"
+lemma PrePost_readS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value (f s)) s) (readS f) P"
   unfolding PrePost_def readS_def returnS_def by auto
 
-lemma PrePost_updateS[intro, PrePost_intro]: "PrePost (\<lambda>s. P (Value ()) (f s)) (updateS f) P"
+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_if:
@@ -100,7 +101,7 @@ lemma PrePost_if:
   shows "PrePost P (if b then f else g) Q"
   using assms by auto
 
-lemma PrePost_if_branch[PrePost_intro]:
+lemma PrePost_if_branch[PrePost_compositeI]:
   assumes "b \<Longrightarrow> PrePost Pf f Q" and "\<not>b \<Longrightarrow> PrePost Pg g Q"
   shows "PrePost (if b then Pf else Pg) (if b then f else g) Q"
   using assms by auto
@@ -115,22 +116,22 @@ lemma PrePost_if_else:
   shows "PrePost P (if b then f else g) Q"
   using assms by auto
 
-lemma PrePost_prod_cases[PrePost_intro]:
+lemma PrePost_prod_cases[PrePost_compositeI]:
   assumes "PrePost P (f (fst x) (snd x)) Q"
   shows "PrePost P (case x of (a, b) \<Rightarrow> f a b) Q"
   using assms by (auto split: prod.splits)
 
-lemma PrePost_option_cases[PrePost_intro]:
+lemma PrePost_option_cases[PrePost_compositeI]:
   assumes "\<And>a. PrePost (PS a) (s a) Q" and "PrePost PN n Q"
   shows "PrePost (case x of Some a \<Rightarrow> PS a | None \<Rightarrow> PN) (case x of Some a \<Rightarrow> s a | None \<Rightarrow> n) Q"
   using assms by (auto split: option.splits)
 
-lemma PrePost_let[intro, PrePost_intro]:
+lemma PrePost_let[intro, PrePost_compositeI]:
   assumes "PrePost P (m y) Q"
   shows "PrePost P (let x = y in m x) Q"
   using assms by auto
 
-lemma PrePost_and_boolS[PrePost_intro]:
+lemma PrePost_and_boolS[PrePost_compositeI]:
   assumes r: "PrePost R r Q"
     and l: "PrePost P l (\<lambda>r. case r of Value True \<Rightarrow> R | _ \<Rightarrow> Q r)"
   shows "PrePost P (and_boolS l r) Q"
@@ -145,7 +146,7 @@ next
     using l by (elim PrePost_weaken_post) (auto split: result.splits)
 qed
 
-lemma PrePost_or_boolS[PrePost_intro]:
+lemma PrePost_or_boolS[PrePost_compositeI]:
   assumes r: "PrePost R r Q"
     and l: "PrePost P l (\<lambda>r. case r of Value False \<Rightarrow> R | _ \<Rightarrow> Q r)"
   shows "PrePost P (or_boolS l r) Q"
@@ -160,20 +161,20 @@ next
     using l by (elim PrePost_weaken_post) (auto split: result.splits)
 qed
 
-lemma PrePost_assert_expS[intro, PrePost_intro]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
+lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
   unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
 
-lemma PrePost_chooseS[intro, PrePost_intro]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
+lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
   by (auto simp: PrePost_def chooseS_def)
 
-lemma PrePost_failS[intro, PrePost_intro]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
+lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
   by (auto simp: PrePost_def failS_def)
 
 lemma case_result_combine[simp]:
   "(case r of Value a \<Rightarrow> Q (Value a) | Ex e \<Rightarrow> Q (Ex e)) = Q r"
   by (auto split: result.splits)
 
-lemma PrePost_foreachS_Nil[intro, simp, PrePost_intro]:
+lemma PrePost_foreachS_Nil[intro, simp, PrePost_atomI]:
   "PrePost (Q (Value vars)) (foreachS [] vars body) Q"
   by auto
 
@@ -249,20 +250,21 @@ lemma PrePostE_weaken_post:
   shows "PrePostE A f C E"
   using assms by (blast intro: PrePostE_consequence)
 
-named_theorems PrePostE_intro
+named_theorems PrePostE_compositeI
+named_theorems PrePostE_atomI
 
-lemma PrePostE_True_post[PrePost_intro, intro, simp]:
+lemma PrePostE_True_post[PrePostE_atomI, intro, simp]:
   "PrePostE P m (\<lambda>_ _. True) (\<lambda>_ _. True)"
   unfolding PrePost_defs by (auto split: result.splits)
 
 lemma PrePostE_any: "PrePostE (\<lambda>s. \<forall>(r, s') \<in> m s. case r of Value a \<Rightarrow> Q a s' | Ex e \<Rightarrow> E e s') m Q E"
   by (intro PrePostE_I) auto
 
-lemma PrePostE_returnS[PrePostE_intro, intro, simp]:
+lemma PrePostE_returnS[PrePostE_atomI, intro, simp]:
   "PrePostE (P x) (returnS x) P Q"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
-lemma PrePostE_bindS[intro, PrePostE_intro]:
+lemma PrePostE_bindS[intro, PrePostE_compositeI]:
   assumes f: "\<And>s a s'. (Value a, s') \<in> m s \<Longrightarrow> PrePostE (R a) (f a) Q E"
     and m: "PrePostE P m R E"
   shows "PrePostE P (bindS m f) Q E"
@@ -282,13 +284,13 @@ lemma PrePostE_bindS_unit:
   shows "PrePostE P (bindS m f) Q E"
   using assms by auto
 
-lemma PrePostE_readS[PrePostE_intro, intro]: "PrePostE (\<lambda>s. Q (f s) s) (readS f) Q E"
+lemma PrePostE_readS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q (f s) s) (readS f) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
-lemma PrePostE_updateS[PrePostE_intro, intro]: "PrePostE (\<lambda>s. Q () (f s)) (updateS f) Q E"
+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_if_branch[PrePostE_intro]:
+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"
   using assms by (auto)
@@ -308,44 +310,44 @@ lemma PrePostE_if_else:
   shows "PrePostE P (if b then f else g) Q E"
   using assms by auto
 
-lemma PrePostE_prod_cases[PrePostE_intro]:
+lemma PrePostE_prod_cases[PrePostE_compositeI]:
   assumes "PrePostE P (f (fst x) (snd x)) Q E"
   shows "PrePostE P (case x of (a, b) \<Rightarrow> f a b) Q E"
   using assms by (auto split: prod.splits)
 
-lemma PrePostE_option_cases[PrePostE_intro]:
+lemma PrePostE_option_cases[PrePostE_compositeI]:
   assumes "\<And>a. PrePostE (PS a) (s a) Q E" and "PrePostE PN n Q E"
   shows "PrePostE (case x of Some a \<Rightarrow> PS a | None \<Rightarrow> PN) (case x of Some a \<Rightarrow> s a | None \<Rightarrow> n) Q E"
   using assms by (auto split: option.splits)
 
-lemma PrePostE_let[PrePostE_intro]:
+lemma PrePostE_let[PrePostE_compositeI]:
   assumes "PrePostE P (m y) Q E"
   shows "PrePostE P (let x = y in m x) Q E"
   using assms by auto
 
-lemma PrePostE_and_boolS[PrePostE_intro]:
+lemma PrePostE_and_boolS[PrePostE_compositeI]:
   assumes r: "PrePostE R r Q E"
     and l: "PrePostE P l (\<lambda>r. if r then R else Q False) E"
   shows "PrePostE P (and_boolS l r) Q E"
   using assms unfolding PrePostE_def
   by (intro PrePost_and_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits)
 
-lemma PrePostE_or_boolS[PrePostE_intro]:
+lemma PrePostE_or_boolS[PrePostE_compositeI]:
   assumes r: "PrePostE R r Q E"
     and l: "PrePostE P l (\<lambda>r. if r then Q True else R) E"
   shows "PrePostE P (or_boolS l r) Q E"
   using assms unfolding PrePostE_def
   by (intro PrePost_or_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits)
 
-lemma PrePostE_assert_expS[PrePostE_intro, intro]:
+lemma PrePostE_assert_expS[PrePostE_atomI, intro]:
   "PrePostE (if c then P () else Q (Failure m)) (assert_expS c m) P Q"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
-lemma PrePostE_failS[PrePost_intro, intro]:
+lemma PrePostE_failS[PrePostE_atomI, intro]:
   "PrePostE (E (Failure msg)) (failS msg) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
-lemma PrePostE_chooseS[intro, PrePostE_intro]:
+lemma PrePostE_chooseS[intro, PrePostE_atomI]:
   "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index f7c171a8..cf5e4dbf 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -6,11 +6,13 @@ lemma All_liftState_dom: "liftState_dom (r, m)"
   by (induction m) (auto intro: liftState.domintros)
 termination liftState using All_liftState_dom by auto
 
-lemma liftState_bind[simp]:
+named_theorems liftState_simp
+
+lemma liftState_bind[liftState_simp]:
   "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
   by (induction m f rule: bind.induct) auto
 
-lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def)
+lemma liftState_return[liftState_simp]: "liftState r (return a) = returnS a" by (auto simp: return_def)
 
 lemma Value_liftState_Run:
   assumes "(Value a, s') \<in> liftState r m s"
@@ -19,51 +21,58 @@ lemma Value_liftState_Run:
       auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
       blast elim: Value_bindS_elim)
 
-lemmas liftState_if_distrib[simp] = if_distrib[where f = "liftState ra" for ra]
-
-lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def)
-lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def)
-lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def)
-lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def)
-lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def)
-lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def)
-lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def)
-lemma liftState_maybe_fail[simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
-  by (auto simp: maybe_fail_def maybe_failS_def split: option.splits)
-lemma liftState_and_boolM[simp]:
+lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
+
+lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e"
+  by (auto simp: throw_def)
+lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg"
+  by (auto simp: assert_exp_def assert_expS_def)
+lemma liftState_exit[liftState_simp]: "liftState r (exit0 ()) = exitS ()"
+  by (auto simp: exit0_def exitS_def)
+lemma liftState_exclResult[liftState_simp]: "liftState r (excl_result ()) = excl_resultS ()"
+  by (auto simp: excl_result_def liftState_simp)
+lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()"
+  by (auto simp: barrier_def)
+lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()"
+  by (auto simp: footprint_def)
+lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()"
+  by (auto simp: undefined_bool_def liftState_simp)
+lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
+  by (auto simp: maybe_fail_def maybe_failS_def liftState_simp split: option.splits)
+lemma liftState_and_boolM[liftState_simp]:
   "liftState r (and_boolM x y) = and_boolS (liftState r x) (liftState r y)"
-  by (auto simp: and_boolM_def and_boolS_def cong: bindS_cong if_cong)
-lemma liftState_or_boolM[simp]:
+  by (auto simp: and_boolM_def and_boolS_def liftState_simp cong: bindS_cong if_cong)
+lemma liftState_or_boolM[liftState_simp]:
   "liftState r (or_boolM x y) = or_boolS (liftState r x) (liftState r y)"
-  by (auto simp: or_boolM_def or_boolS_def cong: bindS_cong if_cong)
+  by (auto simp: or_boolM_def or_boolS_def liftState_simp cong: bindS_cong if_cong)
 
-lemma liftState_try_catch[simp]:
+lemma liftState_try_catch[liftState_simp]:
   "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
   by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw)
 
-lemma liftState_early_return[simp]:
+lemma liftState_early_return[liftState_simp]:
   "liftState r (early_return r) = early_returnS r"
-  by (auto simp: early_return_def early_returnS_def)
+  by (auto simp: early_return_def early_returnS_def liftState_simp)
 
-lemma liftState_catch_early_return[simp]:
+lemma liftState_catch_early_return[liftState_simp]:
   "liftState r (catch_early_return m) = catch_early_returnS (liftState r m)"
-  by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong)
+  by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib liftState_simp cong: sum.case_cong)
 
-lemma liftState_liftR[simp]:
+lemma liftState_liftR[liftState_simp]:
   "liftState r (liftR m) = liftRS (liftState r m)"
-  by (auto simp: liftR_def liftRS_def)
+  by (auto simp: liftR_def liftRS_def liftState_simp)
 
-lemma liftState_try_catchR[simp]:
+lemma liftState_try_catchR[liftState_simp]:
   "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)"
-  by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib cong: sum.case_cong)
+  by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong)
 
 lemma liftState_read_mem_BC:
   assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
   shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
   using assms
-  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def split: option.splits)
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits)
 
-lemma liftState_read_mem[simp]:
+lemma liftState_read_mem[liftState_simp]:
   "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
   "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz"
   by (auto simp: liftState_read_mem_BC)
@@ -73,14 +82,14 @@ lemma liftState_write_mem_ea_BC:
   shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)"
   using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
 
-lemma liftState_write_mem_ea[simp]:
+lemma liftState_write_mem_ea[liftState_simp]:
   "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)"
   "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
   by (auto simp: liftState_write_mem_ea_BC)
 
 lemma liftState_write_mem_val:
   "liftState r (write_mem_val BC v) = write_mem_valS BC v"
-  by (auto simp: write_mem_val_def write_mem_valS_def split: option.splits)
+  by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
 
 lemma liftState_read_reg_readS:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
@@ -99,22 +108,23 @@ lemma liftState_write_reg_updateS:
   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)
 
-lemma liftState_iter_aux[simp]:
+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"
-  by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto cong: bindS_cong)
+  by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct)
+     (auto simp: liftState_simp cong: bindS_cong)
 
-lemma liftState_iteri[simp]:
+lemma liftState_iteri[liftState_simp]:
   "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs"
-  by (auto simp: iteri_def iteriS_def)
+  by (auto simp: iteri_def iteriS_def liftState_simp)
 
-lemma liftState_iter[simp]:
+lemma liftState_iter[liftState_simp]:
   "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs"
-  by (auto simp: iter_def iterS_def)
+  by (auto simp: iter_def iterS_def liftState_simp)
 
-lemma liftState_foreachM[simp]:
+lemma liftState_foreachM[liftState_simp]:
   "liftState r (foreachM xs vars body) = foreachS xs vars (\<lambda>x vars. liftState r (body x vars))"
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
-     (auto cong: bindS_cong)
+     (auto simp: liftState_simp cong: bindS_cong)
 
 lemma whileS_dom_step:
   assumes "whileS_dom (vars, cond, body, s)"
@@ -162,7 +172,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
       qed
       then show ?case using while while' that IH by auto
     qed auto
-    then show ?case by auto
+    then show ?case by (auto simp: liftState_simp)
   qed auto
 qed
 
@@ -200,7 +210,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
         show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run)
         show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run)
       qed
-      then show ?case using k until IH by (auto simp: comp_def)
+      then show ?case using k until IH by (auto simp: comp_def liftState_simp)
     qed auto
   qed auto
 qed
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index 51591531..0c83ebea 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -412,7 +412,9 @@ case, defined as
 @{thm [display, names_short] PrePostE_def}
 The theory includes standard proof rules for both of these variants, in particular rules
 giving weakest preconditions of the predefined primitives of the monad, collected under the names
-@{attribute PrePost_intro} and @{attribute PrePostE_intro}, respectively.
+@{attribute PrePost_atomI} for atoms such as @{term return} and @{attribute PrePost_compositeI}
+for composites such as @{term bind} (or @{attribute PrePostE_atomI} and
+@{attribute PrePostE_compositeI}, respectively, for the quadruple variant).
 
 The instruction we are considering is defined as
 @{thm [display] execute_ITYPE.simps[of _ rs for rs]}
@@ -448,16 +450,17 @@ lemma
   shows "PrePostE pre (liftS instr) post (\<lambda>_ _. False)"
 
   unfolding pre_def instr_def post_def
-  by (simp add: rX_def wX_def cong: bindS_cong if_cong split del: if_split)
-     (rule PrePostE_strengthen_pre, (rule PrePostE_intro)+, auto simp: uint_0_iff)
+  by (simp add: rX_def wX_def liftState_simp cong: bindS_cong if_cong split del: if_split)
+     (rule PrePostE_strengthen_pre, (rule PrePostE_atomI PrePostE_compositeI)+, auto simp: uint_0_iff)
 
 text \<open>The proof begins with a simplification step, which not only unfolds the definitions of the
 auxiliary functions @{term rX} and @{term wX}, but also performs the lifting from the free monad
 to the state monad.  We apply the rule @{thm [source] PrePostE_strengthen_pre} (in a
-backward manner) to allow a weaker precondition, then use the rules in @{attribute PrePostE_intro}
-to derive a weakest precondition, and then use @{method auto} to show that it is implied by
-the given precondition.  For more serious proofs, one will want to set up specialised proof
-tactics.  This example uses only basic proof methods, to make the reasoning steps more explicit.\<close>
+backward manner) to allow a weaker precondition, then use the rules in
+@{attribute PrePostE_compositeI} and @{attribute PrePostE_atomI} to derive a weakest precondition,
+and then use @{method auto} to show that it is implied by the given precondition.  For more serious
+proofs, one will want to set up specialised proof tactics.  This example uses only basic proof
+methods, to make the reasoning steps more explicit.\<close>
 
 (*<*)
 end