refinement proof for AArch64

lib/Corres_UL.thy

@@ -339,6 +339,18 @@ lemma corres_splitEE:
    apply (clarsimp simp: lift_def y)+
   done
 
+lemma corres_splitEE_prod:
+  assumes x: "corres_underlying sr nf nf' (f \<oplus> r') P P' a c"
+  assumes y: "\<And>x y x' y'. r' (x, y) (x', y')
+              \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R x y) (R' x' y') (b x y) (d x' y')"
+  assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>(x, y). R x y \<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>(x, y). R' x y\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
+  shows      "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>(x, y). b x y)) (c >>=E (\<lambda>(x, y). d x y))"
+  using assms
+  apply (unfold bindE_def validE_def)
+  apply (rule corres_split[rotated 2], assumption+)
+  apply (fastforce simp: lift_def y split: sum.splits)
+  done
+
 lemma corres_split_handle:
   assumes    "corres_underlying sr nf nf' (f' \<oplus> r) P P' a c"
   assumes y: "\<And>ft ft'. f' ft ft'
@@ -494,6 +506,8 @@ lemma corres_liftE_rel_sum[simp]:
   corres_underlying sr nf nf' r P P' m m'"
   by (simp add: liftE_liftM o_def)
 
+lemmas corres_liftE_lift = corres_liftE_rel_sum[THEN iffD2]
+
 text \<open>Support for proving correspondence to noop with hoare triples\<close>
 
 lemma corres_noop:
@@ -689,6 +703,17 @@ lemma corres_trivial:
  "corres_underlying sr nf nf' r \<top> \<top> f g \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> f g"
   by assumption
 
+lemma corres_underlying_trivial[corres]:
+  "\<lbrakk> nf' \<Longrightarrow> no_fail P' f \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' (=) \<top> P' f f"
+  by (auto simp add: corres_underlying_def Id_def no_fail_def)
+
+(* Instance of corres_underlying_trivial for unit type with dc instead of (=) as return relation,
+   for nicer return relation instantiation. *)
+lemma corres_underlying_trivial_dc[corres]:
+  "(nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow> corres_underlying Id nf nf' dc (\<lambda>_. True) P' f f"
+  for f :: "('s, unit) nondet_monad"
+  by (fastforce intro: corres_underlying_trivial corres_rrel_pre)
+
 lemma corres_assume_pre:
   assumes R: "\<And>s s'. \<lbrakk> P s; Q s'; (s,s') \<in> sr \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P Q f g"
   shows "corres_underlying sr nf nf' r P Q f g"
@@ -855,6 +880,31 @@ lemma corres_assert_opt_assume:
   by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
                  corres_underlying_def split: option.splits)
 
+lemma corres_assert_opt[corres]:
+  "r x x' \<Longrightarrow>
+  corres_underlying sr nf nf' (\<lambda>x x'. r (Some x) x') (\<lambda>s. x \<noteq> None) \<top> (assert_opt x) (return x')"
+  unfolding corres_underlying_def
+  by (clarsimp simp: assert_opt_def return_def split: option.splits)
+
+lemma assert_opt_assert_corres[corres]:
+  "(x = None) = (x' = None) \<Longrightarrow>
+   corres_underlying sr nf nf' (\<lambda>y _. x = Some y) (K (x \<noteq> None)) \<top>
+                     (assert_opt x) (assert (\<exists>y. x' = Some y))"
+  by (simp add: corres_underlying_def assert_opt_def return_def split: option.splits)
+
+lemma corres_assert_opt_l:
+  assumes "\<And>x. P' = Some x \<Longrightarrow> corres_underlying sr nf nf' r (P x) Q (f x) g"
+  shows "corres_underlying sr nf nf' r (\<lambda>s. \<exists>x. P' = Some x \<and> P x s) Q (assert_opt P' >>= f) g"
+  using assms
+  by (auto simp: bind_def assert_opt_def assert_def fail_def return_def corres_underlying_def
+           split: option.splits)
+
+lemma corres_gets_the_gets:
+  "corres_underlying sr False nf' r P P' (gets_the f) f' \<Longrightarrow>
+   corres_underlying sr nf nf' (\<lambda>x x'. x \<noteq> None \<and> r (the x) x') P P' (gets f) f'"
+  apply (simp add: gets_the_def bind_def simpler_gets_def assert_opt_def)
+  apply (fastforce simp: corres_underlying_def in_monad split: option.splits)
+  done
 
 text \<open>Support for proving correspondance by decomposing the state relation\<close>
 

lib/ExtraCorres.thy

@@ -93,6 +93,8 @@ lemma corres_mapM_x:
            apply (simp | wp)+
   done
 
+lemmas corres_mapM_x' = corres_mapM_x[OF _ _ _ _ order_refl]
+
 (* FIXME: see comment for mapM rule. Same applies for lemma strength *)
 lemma corres_mapME:
   assumes x: "r [] []"

lib/LemmaBucket.thy

@@ -11,10 +11,6 @@ imports
   SubMonadLib
 begin
 
-lemma corres_underlying_trivial:
-  "\<lbrakk> nf' \<Longrightarrow> no_fail P' f \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' (=) \<top> P' f f"
-  by (auto simp add: corres_underlying_def Id_def no_fail_def)
-
 lemma hoare_spec_gen_asm:
   "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f \<lbrace>Q\<rbrace>"
   "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"

lib/Lib.thy

@@ -2522,6 +2522,14 @@ lemma if_option_None_eq:
   "((if P then Some x else None) = None) = (\<not>P)"
   by simp+
 
+lemma option_case_all_conv:
+  "(case x of None \<Rightarrow> True | Some v \<Rightarrow> P v) = (\<forall>v. x = Some v \<longrightarrow> P v)"
+  by (auto split: option.split)
+
+lemma prod_o_comp:
+  "(case x of (a, b) \<Rightarrow> f a b) \<circ> g = (case x of (a, b) \<Rightarrow> f a b \<circ> g)"
+  by (auto simp: split_def)
+
 lemma lhs_sym_eq:
   "(a = b) = x \<longleftrightarrow> (b = a) = x"
   by auto

lib/MonadicRewrite.thy

@@ -653,6 +653,13 @@ lemma monadic_rewrite_gets_the_gets:
   apply (auto simp: simpler_gets_def return_def)
   done
 
+lemma gets_oapply_liftM_rewrite:
+  "monadic_rewrite False True (\<lambda>s. f s p \<noteq> None)
+                   (gets (oapply p \<circ> f)) (liftM Some (gets_map f p))"
+  unfolding monadic_rewrite_def
+  by (simp add: liftM_def simpler_gets_def bind_def gets_map_def assert_opt_def return_def
+           split: option.splits)
+
 text \<open>Option cases\<close>
 
 lemma monadic_rewrite_case_option:

lib/Monads/nondet/Nondet_Monad_Equations.thy

@@ -384,6 +384,14 @@ lemma gets_fold_into_modify:
   by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
                     exec_get exec_put)
 
+lemma gets_return_gets_eq:
+  "gets f >>= (\<lambda>g. return (h g)) = gets (\<lambda>s. h (f s))"
+  by (simp add: simpler_gets_def bind_def return_def)
+
+lemma gets_prod_comp:
+  "gets (case x of (a, b) \<Rightarrow> f a b) = (case x of (a, b) \<Rightarrow> gets (f a b))"
+  by (auto simp: split_def)
+
 lemma bind_assoc2:
   "(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)"
   by (simp add: bind_assoc)

lib/Monads/nondet/Nondet_More_VCG.thy

@@ -48,14 +48,6 @@ lemma valid_prove_more: (* FIXME: duplicate *)
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
   by (rule hoare_post_add)
 
-lemma hoare_vcg_if_lift:
-  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
-
-  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
-  by (auto simp: valid_def split_def)
-
 lemma hoare_vcg_if_lift_strong:
   "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
    \<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then Q rv s else R rv s\<rbrace>"
@@ -248,13 +240,6 @@ lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *
   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
   by (auto simp: valid_def validE_R_def validE_def split_def)
 
-lemma hoare_vcg_imp_liftE:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<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>, \<lbrace>A\<rbrace>"
-  apply (simp only: imp_conv_disj)
-  apply (clarsimp simp: validE_def valid_def split_def sum.case_eq_if)
-  done
-
 lemma hoare_list_all_lift:
   "(\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>)
    \<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>"
@@ -419,13 +404,6 @@ lemma hoare_vcg_const_imp_lift_R:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. F \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. F \<longrightarrow> Q rv s\<rbrace>,-"
   by (cases F, simp_all)
 
-lemma hoare_vcg_disj_lift_R:
-  assumes x: "\<lbrace>P\<rbrace>  f \<lbrace>Q\<rbrace>,-"
-  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
-  shows      "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
-  using assms
-  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
-
 lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def]
 
 lemma valid_case_option_post_wp:
@@ -592,10 +570,6 @@ lemma hoare_const_imp_R:
   "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
   by (cases P, simp_all)
 
-lemma hoare_vcg_imp_lift_R:
-  "\<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 (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
-
 lemma hoare_disj_division:
   "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
      \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"

lib/Monads/nondet/Nondet_VCG.thy

@@ -516,6 +516,15 @@ lemma hoare_vcg_conj_liftE1:
   unfolding valid_def validE_R_def validE_def
   by (fastforce simp: split_def split: sum.splits)
 
+lemma hoare_vcg_conj_liftE_weaker:
+  assumes "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
+  assumes "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>"
+  shows "\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>"
+  apply (rule hoare_pre)
+   apply (fastforce intro: assms hoare_vcg_conj_liftE1 validE_validE_R hoare_post_impErr)
+  apply simp
+  done
+
 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
@@ -547,6 +556,19 @@ 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_liftE:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<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>, \<lbrace>A\<rbrace>"
+  by (fastforce simp: validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_imp_lift_R:
+  "\<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 (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
+
+lemma hoare_vcg_imp_lift_R':
+  "\<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_R_def validE_def split_def split: sum.splits)
+
 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>"
@@ -567,6 +589,10 @@ 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_E:
+  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f -, \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f -, \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
+  by (fastforce simp: validE_E_def validE_def valid_def split_def split: sum.splits)
+
 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)
@@ -662,6 +688,58 @@ 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)
 
+lemma hoare_vcg_if_lift:
+  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
+
+  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
+  by (auto simp: valid_def split_def)
+
+lemma hoare_vcg_disj_lift_R:
+  assumes x: "\<lbrace>P\<rbrace>  f \<lbrace>Q\<rbrace>,-"
+  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
+  shows      "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
+  using assms
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_all_liftE:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
+  by (fastforce simp: validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_const_Ball_liftE:
+  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>E\<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>,\<lbrace>E\<rbrace>"
+  by (fastforce simp: validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_split_lift[wp]:
+  "\<lbrace>P\<rbrace> f x y \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> case (x, y) of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>"
+  by simp
+
+named_theorems hoare_vcg_op_lift
+lemmas [hoare_vcg_op_lift] =
+  hoare_vcg_const_imp_lift
+  hoare_vcg_const_imp_lift_E
+  hoare_vcg_const_imp_lift_R
+  (* leaving out hoare_vcg_conj_lift*, because that is built into wp *)
+  hoare_vcg_disj_lift
+  hoare_vcg_disj_lift_R
+  hoare_vcg_ex_lift
+  hoare_vcg_ex_liftE
+  hoare_vcg_ex_liftE_E
+  hoare_vcg_all_lift
+  hoare_vcg_all_liftE
+  hoare_vcg_all_liftE_E
+  hoare_vcg_all_lift_R
+  hoare_vcg_const_Ball_lift
+  hoare_vcg_const_Ball_lift_R
+  hoare_vcg_const_Ball_lift_E_E
+  hoare_vcg_split_lift
+  hoare_vcg_if_lift
+  hoare_vcg_imp_lift'
+  hoare_vcg_imp_liftE
+  hoare_vcg_imp_lift_R
+  hoare_vcg_imp_liftE_E
+
 
 subsection \<open>Weakest Precondition Rules\<close>
 

lib/Monads/reader_option/Reader_Option_ND.thy

@@ -118,6 +118,15 @@ 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)
+
+lemma gets_obind_bind_eq:
+  "(gets (f |>> (\<lambda>x. g x))) =
+   (gets f >>= (\<lambda>x. case x of None \<Rightarrow> return None | Some y \<Rightarrow> gets (g y)))"
+  by (auto simp: simpler_gets_def bind_def obind_def return_def split: option.splits)
+
 lemma fst_assert_opt:
   "fst (assert_opt opt s) = (if opt = None then {} else {(the opt,s)})"
   by (clarsimp simp: assert_opt_def fail_def return_def split: option.split)

lib/Monads/wp/WPBang.thy

@@ -20,7 +20,7 @@ ML \<open>
 structure WP_Safe = struct
 
 fun check_has_frees_tac Ps (_ : int) thm = let
-    val fs = Term.add_frees (Thm.prop_of thm) [] |> filter (member (=) Ps)
+    val fs = Term.add_frees (Thm.prop_of thm) [] |> filter (member (op =) Ps)
   in if null fs then Seq.empty else Seq.single thm end
 
 fun wp_bang wp_safe_rules ctxt = let

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -738,4 +738,11 @@ lemma aligned_mask_le_mask_minus:
   by (metis and_mask_less' is_aligned_after_mask is_aligned_neg_mask_eq'
            mask_2pm1 mask_sub neg_mask_mono_le word_less_sub_le)
 
+lemma shiftr_anti_mono:
+  "m \<le> n \<Longrightarrow> w >> n \<le> w >> m" for w :: "'a::len word"
+  apply transfer
+  apply (simp add: take_bit_drop_bit)
+  apply (simp add: drop_bit_eq_div zdiv_mono2)
+  done
+
 end

proof/access-control/RISCV64/ArchArch_AC.thy

@@ -915,7 +915,7 @@ lemma unmap_page_table_respects:
    unmap_page_table asid vaddr pt
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: unmap_page_table_def sfence_def)
-  apply (wpsimp wp: pt_lookup_from_level_is_subject dmo_mol_respects hoare_vcg_conj_liftE
+  apply (wpsimp wp: pt_lookup_from_level_is_subject dmo_mol_respects hoare_vcg_conj_liftE_weaker
                     store_pte_respects pt_lookup_from_level_wrp[where Q="\<lambda>_. integrity aag X st"]
          | wp (once) hoare_drop_imps hoare_vcg_E_elim)+
   apply (intro conjI; clarsimp)

proof/infoflow/Syscall_IF.thy

@@ -705,7 +705,6 @@ lemma handle_recv_reads_respects_f:
                       simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)[1]
         apply (wp reads_respects_f[OF handle_fault_reads_respects,where st=st])
        apply (wpsimp wp: get_simple_ko_wp get_cap_wp)+
-        apply (rule VSpaceEntries_AI.hoare_vcg_all_liftE)
         apply (rule_tac Q="\<lambda>r s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and>
                                  tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and>
                                  is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst r))"