diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy
index 7e5b471f12..297fae9382 100644
--- a/lib/Monads/nondet/Nondet_Reader_Option.thy
+++ b/lib/Monads/nondet/Nondet_Reader_Option.thy
@@ -70,7 +70,11 @@ lemma gets_the_obind:
   "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))"
   by (rule ext) (simp add: monad_simps obind_def split: option.splits)
 
-lemma gets_the_Some_get[simp]:
+lemma gets_the_Some_return:
+  "gets_the (\<lambda>_. Some x) = return x"
+  by (simp add: gets_the_def assert_opt_Some)
+
+lemma gets_the_Some_get:
   "gets_the Some = get"
   by (clarsimp simp: gets_the_def gets_def assert_opt_Some)
 
@@ -115,10 +119,6 @@ lemma gets_the_oapply_comp:
   "gets_the (oapply x \<circ> f) = gets_map f x"
   by (fastforce simp: gets_map_def gets_the_def o_def gets_def)
 
-lemma gets_the_Some:
-  "gets_the (\<lambda>_. Some x) = return x"
-  by (simp add: gets_the_def assert_opt_Some)
-
 lemma gets_the_oapply2_comp:
   "gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x"
   by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)
@@ -136,7 +136,7 @@ lemma fst_assert_opt:
 lemmas omonad_simps [simp] =
   gets_the_opt_map assert_opt_Some gets_the_obind
   gets_the_return gets_the_fail gets_the_returnOk
-  gets_the_throwError gets_the_assert gets_the_Some
+  gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get
   gets_the_oapply_comp
 
 
diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
index 9e0a7199d7..1ebd4a18f2 100644
--- a/lib/Monads/nondet/Nondet_VCG.thy
+++ b/lib/Monads/nondet/Nondet_VCG.thy
@@ -227,11 +227,11 @@ lemma return_inv[iff]:
 
 lemma hoare_modifyE_var:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
-  by(simp add: valid_def modify_def put_def get_def bind_def)
+  by (simp add: valid_def modify_def put_def get_def bind_def)
 
 lemma hoare_if:
   "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if P' then f else g \<lbrace>Q\<rbrace>"
-  by (simp add: valid_def)
+  by simp
 
 lemma hoare_pre_subst:
   "\<lbrakk> P = P'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
diff --git a/lib/Monads/trace/Trace_More_RG.thy b/lib/Monads/trace/Trace_More_RG.thy
index d75e92433e..1a8a3c4074 100644
--- a/lib/Monads/trace/Trace_More_RG.thy
+++ b/lib/Monads/trace/Trace_More_RG.thy
@@ -138,6 +138,20 @@ lemma assertE_tsp:
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assertE Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q \<and> P s0 s\<rbrace>,\<lbrace>E\<rbrace>"
   by (wpsimp wp: assertE_wp)
 
+lemma select_inv_rg:
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> select S \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
+  by wpsimp
+
+lemma assert_inv_rg:
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assert Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
+  unfolding assert_def
+  by (cases Q) wpsimp+
+
+lemma assert_opt_inv_rg:
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assert_opt Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
+  unfolding assert_opt_def
+  by (cases Q) (wp | simp)+
+
 lemma case_options_weak_twp:
   "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index 42889d9236..aedda7f671 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -362,6 +362,22 @@ lemma rg_FalseE[simp]:
   "\<lbrace>\<bottom>\<bottom>\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = prefix_closed f"
   by (simp add: validI_def validIE_def)
 
+lemma rg_modifyE_var:
+  "\<lbrakk> \<And>s0 s. P s0 s \<Longrightarrow> Q s0 (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> modify f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
+  by (simp add: validI_def modify_def put_def get_def bind_def prefix_closed_def rely_def)
+
+lemma rg_if:
+  "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> if P' then f else g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
+  by simp
+
+lemma rg_pre_subst:
+  "\<lbrakk> P = P'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
+  by (erule subst)
+
+lemma rg_post_subst:
+  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>"
+  by (erule subst)
+
 lemma rg_post_imp:
   "\<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   by (simp add: validI_def)
diff --git a/lib/Monads/trace/Trace_Reader_Option.thy b/lib/Monads/trace/Trace_Reader_Option.thy
index 27f59281d0..b493ce65fc 100644
--- a/lib/Monads/trace/Trace_Reader_Option.thy
+++ b/lib/Monads/trace/Trace_Reader_Option.thy
@@ -70,6 +70,14 @@ lemma gets_the_obind:
   "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))"
   by (rule ext) (simp add: monad_simps obind_def split: option.splits)
 
+lemma gets_the_Some_return:
+  "gets_the (\<lambda>_. Some x) = return x"
+  by (simp add: gets_the_def assert_opt_Some)
+
+lemma gets_the_Some_get:
+  "gets_the Some = get"
+  by (clarsimp simp: gets_the_def gets_def assert_opt_Some)
+
 lemma gets_the_return:
   "gets_the (oreturn x) = return x"
   by (simp add: monad_simps oreturn_def)
@@ -94,6 +102,11 @@ lemma gets_the_assert:
   "gets_the (oassert P) = assert P"
   by (simp add: oassert_def assert_def gets_the_fail gets_the_return)
 
+lemma gets_the_ostate_assert:
+  "gets_the (ostate_assert P) = state_assert P"
+  by (clarsimp simp: ostate_assert_def state_assert_def gets_the_obind gets_the_Some_get
+                     gets_the_assert)
+
 lemma gets_the_assert_opt:
   "gets_the (oassert_opt P) = assert_opt P"
   by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)
@@ -106,10 +119,6 @@ lemma gets_the_oapply_comp:
   "gets_the (oapply x \<circ> f) = gets_map f x"
   by (fastforce simp: gets_map_def gets_the_def o_def gets_def)
 
-lemma gets_the_Some:
-  "gets_the (\<lambda>_. Some x) = return x"
-  by (simp add: gets_the_def assert_opt_Some)
-
 lemma gets_the_oapply2_comp:
   "gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x"
   by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)
@@ -127,7 +136,7 @@ lemma mres_assert_opt:
 lemmas omonad_simps [simp] =
   gets_the_opt_map assert_opt_Some gets_the_obind
   gets_the_return gets_the_fail gets_the_returnOk
-  gets_the_throwError gets_the_assert gets_the_Some
+  gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get
   gets_the_oapply_comp
 
 
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index 4b8170b5d3..268cca5e68 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -223,11 +223,11 @@ lemma return_inv[iff]:
 
 lemma hoare_modifyE_var:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
-  by(simp add: valid_def modify_def put_def get_def bind_def mres_def)
+  by (simp add: valid_def modify_def put_def get_def bind_def mres_def)
 
 lemma hoare_if:
   "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if P' then f else g \<lbrace>Q\<rbrace>"
-  by (simp add: valid_def)
+  by simp
 
 lemma hoare_pre_subst:
   "\<lbrakk> P = P'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"