From 3af704040f4b0f2b6c8594528b4ed0d6b1fa0cdb Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Wed, 9 Aug 2023 19:38:38 +1000
Subject: [PATCH 1/3] lib/monads: move lifting/splitting section earlier in
 Nondet_VCG

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/nondet/Nondet_VCG.thy | 438 +++++++++++++++----------------
 1 file changed, 219 insertions(+), 219 deletions(-)

diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
index 6cf3fa976e..ca1adeaa25 100644
--- a/lib/Monads/nondet/Nondet_VCG.thy
+++ b/lib/Monads/nondet/Nondet_VCG.thy
@@ -445,6 +445,225 @@ lemma liftE_validE[simp]:
   by (simp add: liftE_liftM validE_def hoare_liftM_subst o_def)
 
 
+subsection \<open>Operator lifting/splitting\<close>
+
+lemma hoare_vcg_if_split:
+  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>"
+  by simp
+
+lemma hoare_vcg_if_splitE:
+  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>"
+  by simp
+
+lemma hoare_vcg_split_case_option:
+ "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow>
+  \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and>(\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
+  case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
+  \<lbrace>R x\<rbrace>"
+  by (cases x; simp)
+
+lemma hoare_vcg_split_case_optionE:
+  "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
+   case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
+   \<lbrace>R x\<rbrace>, \<lbrace>E x\<rbrace>"
+  by (cases x; simp)
+
+lemma hoare_vcg_split_case_sum:
+ "\<lbrakk> \<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace> f x a \<lbrace>R x\<rbrace>; \<And>x b. x = Inr b \<Longrightarrow> \<lbrace>Q x b\<rbrace> g x b \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow>
+  \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P x a s) \<and> (\<forall>b. x = Inr b \<longrightarrow> Q x b s) \<rbrace>
+  case x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b
+  \<lbrace>R x\<rbrace>"
+  by (cases x; simp)
+
+lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
+
+lemmas hoare_seq_ext = seq_ext[rotated]
+lemmas hoare_vcg_seqE = seqE[rotated]
+
+lemma hoare_seq_ext_nobind:
+  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>"
+  by (fastforce simp: valid_def bind_def Let_def split_def)
+
+lemma hoare_seq_ext_nobindE:
+  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
+  by (fastforce simp: validE_def valid_def bindE_def bind_def throwError_def return_def lift_def
+                split: sum.splits)
+
+lemmas hoare_seq_ext_skip' = hoare_seq_ext[where B=C and C=C for C]
+
+lemma hoare_chain:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>rv s. Q rv s \<Longrightarrow> S rv s \<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>"
+  by (wp_pre, rule hoare_post_imp)
+
+lemma validE_weaken: (* FIXME lib: eliminate in favour of hoare_chainE *)
+  "\<lbrakk> \<lbrace>P'\<rbrace> A \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s; \<And>rv s. E' rv s \<Longrightarrow> E rv s \<rbrakk> \<Longrightarrow>
+   \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  by wp_pre (rule hoare_post_impErr)
+
+lemmas hoare_chainE = validE_weaken
+
+lemma hoare_vcg_conj_lift:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
+  unfolding valid_def
+  by fastforce
+
+\<comment> \<open>A variant which works nicely with subgoals that do not contain schematics\<close>
+lemmas hoare_vcg_conj_lift_pre_fix = hoare_vcg_conj_lift[where P=R and P'=R for R, simplified]
+
+lemma hoare_vcg_conj_liftE1:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E\<rbrace>"
+  unfolding valid_def validE_R_def validE_def
+  by (fastforce simp: split_def split: sum.splits)
+
+lemma hoare_vcg_disj_lift:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>"
+  unfolding valid_def
+  by fastforce
+
+lemma hoare_vcg_const_Ball_lift:
+  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>"
+  by (fastforce simp: valid_def)
+
+lemma hoare_vcg_const_Ball_lift_R:
+ "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>,-"
+  unfolding validE_R_def validE_def
+  by (rule hoare_strengthen_post)
+     (fastforce intro!: hoare_vcg_const_Ball_lift split: sum.splits)+
+
+lemma hoare_vcg_all_lift:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
+  by (fastforce simp: valid_def)
+
+lemma hoare_vcg_all_lift_R:
+  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, -"
+  by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified])
+
+lemma hoare_vcg_imp_lift:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
+  by (simp only: imp_conv_disj) (rule hoare_vcg_disj_lift)
+
+lemma hoare_vcg_imp_lift':
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
+  by (wpsimp wp: hoare_vcg_imp_lift)
+
+lemma hoare_vcg_imp_conj_lift[wp_comb]:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
+  by (auto simp: valid_def)
+
+lemmas hoare_vcg_imp_conj_lift'[wp_unsafe] = hoare_vcg_imp_conj_lift[where Q'''="\<top>\<top>", simplified]
+
+lemma hoare_absorb_imp:
+  "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
+  by (erule hoare_post_imp[rotated], blast)
+
+lemma hoare_weaken_imp:
+  "\<lbrakk> \<And>rv s. Q rv s \<Longrightarrow> Q' rv s ;  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> R rv s\<rbrace> \<rbrakk>
+    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
+  by (clarsimp simp: valid_def split_def)
+
+lemma hoare_vcg_const_imp_lift:
+  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
+  by (cases P, simp_all add: hoare_vcg_prop)
+
+lemma hoare_vcg_const_imp_lift_R:
+  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,-) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
+  by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits)
+
+lemma hoare_weak_lift_imp:
+  "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>"
+  by (auto simp add: valid_def split_def)
+
+lemmas hoare_vcg_weaken_imp = hoare_weaken_imp  (* FIXME lib: eliminate *)
+
+lemma hoare_vcg_ex_lift:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
+  by (clarsimp simp: valid_def, blast)
+
+lemma hoare_vcg_ex_lift_R1:
+  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>, -"
+  by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits)
+
+lemma hoare_liftP_ext:
+  assumes "\<And>P x. m \<lbrace>\<lambda>s. P (f s x)\<rbrace>"
+  shows "m \<lbrace>\<lambda>s. P (f s)\<rbrace>"
+  unfolding valid_def
+  apply clarsimp
+  apply (erule subst[rotated, where P=P])
+  apply (rule ext)
+  apply (drule use_valid, rule assms, rule refl)
+  apply simp
+  done
+
+(* for instantiations *)
+lemma hoare_triv:    "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" .
+lemma hoare_trivE:   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .
+lemma hoare_trivE_R: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" .
+lemma hoare_trivR_R: "\<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" .
+
+lemma hoare_vcg_E_conj:
+  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace>"
+  unfolding validE_def validE_E_def
+  by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
+
+lemma hoare_vcg_E_elim:
+  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  by (rule hoare_post_impErr[OF hoare_vcg_E_conj]) (simp add: validE_R_def)+
+
+lemma hoare_vcg_R_conj:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,-"
+  unfolding validE_R_def validE_def
+  by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
+
+lemma hoare_lift_Pf_E_R:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, - \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -"
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
+
+lemma hoare_lift_Pf_E_E:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace> \<rbrakk> \<Longrightarrow>
+  \<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>"
+  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_const_Ball_lift_E_E:
+ "(\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>"
+  unfolding validE_E_def validE_def valid_def
+  by (fastforce split: sum.splits)
+
+lemma hoare_vcg_all_liftE_E:
+  "(\<And>x. \<lbrace>P x\<rbrace> f -, \<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
+  by (rule hoare_vcg_const_Ball_lift_E_E[where S=UNIV, simplified])
+
+lemma hoare_vcg_imp_liftE_E:
+  "\<lbrakk>\<lbrace>P'\<rbrace> f -, \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f -, \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
+  by (auto simp add: valid_def validE_E_def validE_def split_def split: sum.splits)
+
+lemma hoare_vcg_ex_liftE:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
+  by (fastforce simp: validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_ex_liftE_E:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f -,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>"
+  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
+
+lemma hoare_post_imp_R:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
+  unfolding validE_R_def
+  by (erule hoare_post_impErr)
+
+lemma hoare_post_imp_E:
+  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>"
+  unfolding validE_E_def
+  by (rule hoare_post_impErr)
+
+lemma hoare_post_comb_imp_conj:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
+  by (wpsimp wp: hoare_vcg_conj_lift)
+
+
 subsection \<open>Weakest Precondition Rules\<close>
 
 lemma fail_wp:
@@ -705,225 +924,6 @@ lemma select_throwError_wp:
   by (simp add: bind_def throwError_def return_def select_def validE_E_def validE_def valid_def)
 
 
-subsection \<open>Operator lifting/splitting\<close>
-
-lemma hoare_vcg_if_split:
-  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>"
-  by simp
-
-lemma hoare_vcg_if_splitE:
-  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
-   \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>"
-  by simp
-
-lemma hoare_vcg_split_case_option:
- "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and>(\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
-  case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
-  \<lbrace>R x\<rbrace>"
-  by (cases x; simp)
-
-lemma hoare_vcg_split_case_optionE:
-  "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow>
-   \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
-   case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
-   \<lbrace>R x\<rbrace>, \<lbrace>E x\<rbrace>"
-  by (cases x; simp)
-
-lemma hoare_vcg_split_case_sum:
- "\<lbrakk> \<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace> f x a \<lbrace>R x\<rbrace>; \<And>x b. x = Inr b \<Longrightarrow> \<lbrace>Q x b\<rbrace> g x b \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P x a s) \<and> (\<forall>b. x = Inr b \<longrightarrow> Q x b s) \<rbrace>
-  case x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b
-  \<lbrace>R x\<rbrace>"
-  by (cases x; simp)
-
-lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
-
-lemmas hoare_seq_ext = seq_ext[rotated]
-lemmas hoare_vcg_seqE = seqE[rotated]
-
-lemma hoare_seq_ext_nobind:
-  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>"
-  by (fastforce simp: valid_def bind_def Let_def split_def)
-
-lemma hoare_seq_ext_nobindE:
-  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
-  by (fastforce simp: validE_def valid_def bindE_def bind_def throwError_def return_def lift_def
-                split: sum.splits)
-
-lemmas hoare_seq_ext_skip' = hoare_seq_ext[where B=C and C=C for C]
-
-lemma hoare_chain:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>rv s. Q rv s \<Longrightarrow> S rv s \<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>"
-  by (wp_pre, rule hoare_post_imp)
-
-lemma validE_weaken: (* FIXME lib: eliminate in favour of hoare_chainE *)
-  "\<lbrakk> \<lbrace>P'\<rbrace> A \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s; \<And>rv s. E' rv s \<Longrightarrow> E rv s \<rbrakk> \<Longrightarrow>
-   \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
-  by wp_pre (rule hoare_post_impErr)
-
-lemmas hoare_chainE = validE_weaken
-
-lemma hoare_vcg_conj_lift:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
-  unfolding valid_def
-  by fastforce
-
-\<comment> \<open>A variant which works nicely with subgoals that do not contain schematics\<close>
-lemmas hoare_vcg_conj_lift_pre_fix = hoare_vcg_conj_lift[where P=R and P'=R for R, simplified]
-
-lemma hoare_vcg_conj_liftE1:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E\<rbrace>"
-  unfolding valid_def validE_R_def validE_def
-  by (fastforce simp: split_def split: sum.splits)
-
-lemma hoare_vcg_disj_lift:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>"
-  unfolding valid_def
-  by fastforce
-
-lemma hoare_vcg_const_Ball_lift:
-  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>"
-  by (fastforce simp: valid_def)
-
-lemma hoare_vcg_const_Ball_lift_R:
- "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>,-"
-  unfolding validE_R_def validE_def
-  by (rule hoare_strengthen_post)
-     (fastforce intro!: hoare_vcg_const_Ball_lift split: sum.splits)+
-
-lemma hoare_vcg_all_lift:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
-  by (fastforce simp: valid_def)
-
-lemma hoare_vcg_all_lift_R:
-  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, -"
-  by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified])
-
-lemma hoare_vcg_imp_lift:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
-  by (simp only: imp_conv_disj) (rule hoare_vcg_disj_lift)
-
-lemma hoare_vcg_imp_lift':
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
-  by (wpsimp wp: hoare_vcg_imp_lift)
-
-lemma hoare_vcg_imp_conj_lift[wp_comb]:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
-   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
-  by (auto simp: valid_def)
-
-lemmas hoare_vcg_imp_conj_lift'[wp_unsafe] = hoare_vcg_imp_conj_lift[where Q'''="\<top>\<top>", simplified]
-
-lemma hoare_absorb_imp:
-  "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
-  by (erule hoare_post_imp[rotated], blast)
-
-lemma hoare_weaken_imp:
-  "\<lbrakk> \<And>rv s. Q rv s \<Longrightarrow> Q' rv s ;  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> R rv s\<rbrace> \<rbrakk>
-    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
-  by (clarsimp simp: valid_def split_def)
-
-lemma hoare_vcg_const_imp_lift:
-  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
-  by (cases P, simp_all add: hoare_vcg_prop)
-
-lemma hoare_vcg_const_imp_lift_R:
-  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,-) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
-  by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits)
-
-lemma hoare_weak_lift_imp:
-  "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>"
-  by (auto simp add: valid_def split_def)
-
-lemmas hoare_vcg_weaken_imp = hoare_weaken_imp  (* FIXME lib: eliminate *)
-
-lemma hoare_vcg_ex_lift:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
-  by (clarsimp simp: valid_def, blast)
-
-lemma hoare_vcg_ex_lift_R1:
-  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>, -"
-  by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits)
-
-lemma hoare_liftP_ext:
-  assumes "\<And>P x. m \<lbrace>\<lambda>s. P (f s x)\<rbrace>"
-  shows "m \<lbrace>\<lambda>s. P (f s)\<rbrace>"
-  unfolding valid_def
-  apply clarsimp
-  apply (erule subst[rotated, where P=P])
-  apply (rule ext)
-  apply (drule use_valid, rule assms, rule refl)
-  apply simp
-  done
-
-(* for instantiations *)
-lemma hoare_triv:    "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" .
-lemma hoare_trivE:   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .
-lemma hoare_trivE_R: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" .
-lemma hoare_trivR_R: "\<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" .
-
-lemma hoare_vcg_E_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace>"
-  unfolding validE_def validE_E_def
-  by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
-
-lemma hoare_vcg_E_elim:
-  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
-  by (rule hoare_post_impErr[OF hoare_vcg_E_conj]) (simp add: validE_R_def)+
-
-lemma hoare_vcg_R_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,-"
-  unfolding validE_R_def validE_def
-  by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
-
-lemma hoare_lift_Pf_E_R:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, - \<rbrakk> \<Longrightarrow>
-   \<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -"
-  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
-
-lemma hoare_lift_Pf_E_E:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>"
-  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
-
-lemma hoare_vcg_const_Ball_lift_E_E:
- "(\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>"
-  unfolding validE_E_def validE_def valid_def
-  by (fastforce split: sum.splits)
-
-lemma hoare_vcg_all_liftE_E:
-  "(\<And>x. \<lbrace>P x\<rbrace> f -, \<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
-  by (rule hoare_vcg_const_Ball_lift_E_E[where S=UNIV, simplified])
-
-lemma hoare_vcg_imp_liftE_E:
-  "\<lbrakk>\<lbrace>P'\<rbrace> f -, \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow>
-   \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f -, \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
-  by (auto simp add: valid_def validE_E_def validE_def split_def split: sum.splits)
-
-lemma hoare_vcg_ex_liftE:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
-  by (fastforce simp: validE_def valid_def split: sum.splits)
-
-lemma hoare_vcg_ex_liftE_E:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f -,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>"
-  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
-
-lemma hoare_post_imp_R:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
-  unfolding validE_R_def
-  by (erule hoare_post_impErr)
-
-lemma hoare_post_imp_E:
-  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>"
-  unfolding validE_E_def
-  by (rule hoare_post_impErr)
-
-lemma hoare_post_comb_imp_conj:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
-  by (wpsimp wp: hoare_vcg_conj_lift)
-
-
 subsection \<open>Setting up the @{method wp} method\<close>
 
 lemma valid_is_triple:

From 9a877c9bdd2d61b8d7e8c182541613a530d9b270 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Wed, 9 Aug 2023 19:44:37 +1000
Subject: [PATCH 2/3] lib/monads: minor cleanup and restyle in nondet monad

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/nondet/Nondet_More_VCG.thy |  8 --------
 lib/Monads/nondet/Nondet_VCG.thy      | 27 ++++++++++++---------------
 2 files changed, 12 insertions(+), 23 deletions(-)

diff --git a/lib/Monads/nondet/Nondet_More_VCG.thy b/lib/Monads/nondet/Nondet_More_VCG.thy
index 1c351cb303..eb4b261020 100644
--- a/lib/Monads/nondet/Nondet_More_VCG.thy
+++ b/lib/Monads/nondet/Nondet_More_VCG.thy
@@ -36,14 +36,6 @@ lemma hoare_pre_addE:
   apply (subst iff_conv_conj_imp)
   by(intro conjI impI; rule hoare_weaken_preE, assumption, clarsimp)
 
-lemma hoare_disjI1:
-  "\<lbrace>R\<rbrace> f \<lbrace>P\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>r s. P r s \<or> Q r s\<rbrace>"
-  by (erule hoare_post_imp [rotated]) simp
-
-lemma hoare_disjI2:
-  "\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>r s. P r s \<or> Q r s \<rbrace>"
-  by (rule hoare_post_imp [OF _ hoare_disjI1, where P1=Q], auto)
-
 lemma hoare_name_pre_state:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (clarsimp simp: valid_def)
diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
index ca1adeaa25..81be633ba4 100644
--- a/lib/Monads/nondet/Nondet_VCG.thy
+++ b/lib/Monads/nondet/Nondet_VCG.thy
@@ -31,16 +31,15 @@ text \<open>This section defines a Hoare logic for partial correctness for
   the monad satisfy the postcondition. Note that if the computation returns
   the empty set, the triple is trivially valid. This means @{term "assert P"}
   does not require us to prove that @{term P} holds, but rather allows us
-  to assume @{term P}! Proving non-failure is done via separate predicate and
-  calculus (see below).
-\<close>
+  to assume @{term P}! Proving non-failure is done via a separate predicate and
+  calculus (see Nondet_No_Fail).\<close>
 definition valid ::
   "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> fst (f s). Q r s')"
 
 text \<open>
   We often reason about invariant predicates. The following provides shorthand syntax
-  that avoids repeating potentially long predicates. \<close>
+  that avoids repeating potentially long predicates.\<close>
 abbreviation (input) invariant ::
   "('s,'a) nondet_monad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) where
   "invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
@@ -60,7 +59,7 @@ lemma validE_def2:
 
 text \<open>
   The following two instantiations are convenient to separate reasoning for exceptional and
-  normal case. \<close>
+  normal case.\<close>
 (* Narrator: they are in fact not convenient, and are now considered a mistake that should have
              been an abbreviation instead. *)
 definition validE_R :: (* FIXME lib: this should be an abbreviation *)
@@ -96,7 +95,7 @@ lemma hoare_pre_imp:
 lemmas hoare_weaken_pre = hoare_pre_imp[rotated]
 
 lemma hoare_vcg_precond_impE: (* FIXME lib: eliminate in favour of hoare_weaken_preE *)
- "\<lbrakk> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrakk> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>"
   by (fastforce simp add:validE_def2)
 
 lemmas hoare_weaken_preE = hoare_vcg_precond_impE
@@ -420,11 +419,11 @@ lemma validE_R_validE:
   by (simp add: validE_R_def)
 
 lemma validE_validE_E:
-  "\<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>"
+  "\<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>"
   by (simp add: validE_E_def)
 
 lemma validE_E_validE:
-  "\<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>, \<lbrace>E\<rbrace>"
   by (simp add: validE_E_def)
 
 
@@ -458,7 +457,7 @@ lemma hoare_vcg_if_splitE:
 
 lemma hoare_vcg_split_case_option:
  "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and>(\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
+  \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace>
   case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
   \<lbrace>R x\<rbrace>"
   by (cases x; simp)
@@ -498,8 +497,8 @@ lemma hoare_chain:
   by (wp_pre, rule hoare_post_imp)
 
 lemma validE_weaken: (* FIXME lib: eliminate in favour of hoare_chainE *)
-  "\<lbrakk> \<lbrace>P'\<rbrace> A \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s; \<And>rv s. E' rv s \<Longrightarrow> E rv s \<rbrakk> \<Longrightarrow>
-   \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrakk> \<lbrace>P'\<rbrace> A \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s; \<And>rv s. E' rv s \<Longrightarrow> E rv s \<rbrakk>
+   \<Longrightarrow> \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   by wp_pre (rule hoare_post_impErr)
 
 lemmas hoare_chainE = validE_weaken
@@ -708,7 +707,7 @@ lemma returnOKE_R_wp:
 
 lemma liftE_wp:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
-  by (clarsimp simp:valid_def validE_def2 liftE_def split_def Let_def bind_def return_def)
+  by simp
 
 lemma catch_wp:
   "\<lbrakk> \<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> catch f handler \<lbrace>Q\<rbrace>"
@@ -759,8 +758,6 @@ lemma alternative_wp:
   using post_by_hoare[OF x] post_by_hoare[OF y]
   by fastforce
 
-lemmas alternative_valid = alternative_wp[where P=P and P'=P for P, simplified]
-
 lemma alternativeE_wp:
   assumes "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   assumes "\<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
@@ -791,7 +788,7 @@ lemma state_select_wp:
   by (clarsimp simp: state_select_def valid_def)
 
 lemma condition_wp:
-  "\<lbrakk> \<lbrace>Q\<rbrace> A \<lbrace>P\<rbrace>;  \<lbrace>R\<rbrace> B \<lbrace>P\<rbrace>  \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>"
+  "\<lbrakk> \<lbrace>Q\<rbrace> A \<lbrace>P\<rbrace>;  \<lbrace>R\<rbrace> B \<lbrace>P\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>"
   by (clarsimp simp: condition_def valid_def)
 
 lemma conditionE_wp:

From b54525d8b40af754caedd73aacb40db6bfb19e87 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Mon, 14 Aug 2023 21:08:23 +1000
Subject: [PATCH 3/3] refine: update for changes to nondet monad

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 proof/refine/AARCH64/Schedule_R.thy | 2 +-
 proof/refine/ARM/Schedule_R.thy     | 2 +-
 proof/refine/ARM_HYP/Schedule_R.thy | 2 +-
 proof/refine/RISCV64/Schedule_R.thy | 2 +-
 proof/refine/X64/Schedule_R.thy     | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy
index 0ade5d66ca..ff63a9b42a 100644
--- a/proof/refine/AARCH64/Schedule_R.thy
+++ b/proof/refine/AARCH64/Schedule_R.thy
@@ -2314,7 +2314,7 @@ lemma schedule_invs':
     apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                       chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                       switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
-           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
+           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
            | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
            | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
            | strengthen invs'_invs_no_cicd
diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy
index 02921fc419..8622fbfcf9 100644
--- a/proof/refine/ARM/Schedule_R.thy
+++ b/proof/refine/ARM/Schedule_R.thy
@@ -2153,7 +2153,7 @@ lemma schedule_invs':
     apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                       chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                       switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
-           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
+           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
            | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
            | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
            | strengthen invs'_invs_no_cicd
diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy
index 9076942689..8be4b8e1e1 100644
--- a/proof/refine/ARM_HYP/Schedule_R.thy
+++ b/proof/refine/ARM_HYP/Schedule_R.thy
@@ -2279,7 +2279,7 @@ lemma schedule_invs':
     apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                       chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                       switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
-           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
+           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
            | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
            | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
            | strengthen invs'_invs_no_cicd
diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
index 4bc496808b..800d5399b9 100644
--- a/proof/refine/RISCV64/Schedule_R.thy
+++ b/proof/refine/RISCV64/Schedule_R.thy
@@ -2141,7 +2141,7 @@ lemma schedule_invs':
     apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                       chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                       switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
-           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
+           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
            | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
            | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
            | strengthen invs'_invs_no_cicd
diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy
index a248f01710..b1eb3a6820 100644
--- a/proof/refine/X64/Schedule_R.thy
+++ b/proof/refine/X64/Schedule_R.thy
@@ -2144,7 +2144,7 @@ lemma schedule_invs':
     apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                       chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                       switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
-           | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
+           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
            | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
            | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
            | strengthen invs'_invs_no_cicd