lib+proof+autocorres: update for monad changes

This mostly involved some renamed bound variables and the following lemma renamings: hoare_post_taut -> hoare_TrueI hoare_TrueI[where P=\<top>] -> wp_post_taut hoare_post_imp_R -> hoare_strengthen_postE_R hoare_seq_ext -> bind_wp bind_wp[rotated] -> bind_wp_fwd hoare_vcg_precond_imp -> hoare_weaken_pre hoare_vcg_precond_impE -> hoare_weaken_preE hoare_vcg_precond_impE_R -> hoare_weaken_preE_R hoare_vcg_seqE -> bindE_wp bindE_wp[rotated] -> bindE_wp_fwd validE_weaken -> hoare_chainE seqE -> bindE_wp_fwd bindE_wp_fwd[rotated] -> bindE_wp hoare_True_E_R -> hoareE_R_TrueI hoareE_R_TrueI[where P=\<top>] -> wp_post_tautE_R hoare_post_impErr -> hoare_strengthen_postE hoare_vcg_all_lift_R -> hoare_vcg_all_liftE_R hoare_seq_ext_skip -> bind_wp_fwd_skip Signed-off-by: Corey Lewis <[email protected]>
seL4 · May 30, 2024 · 644b3e0 · 644b3e0
1 parent 3f37636
commit 644b3e0
Show file tree

Hide file tree

Showing 272 changed files with 1,931 additions and 1,984 deletions.
diff --git a/lib/CorresK_Method.thy b/lib/CorresK_Method.thy
@@ -969,9 +969,9 @@ method corresKwp uses wp =
       \<open>use in \<open>wp add: wp | wpc\<close>\<close>))\<close>)
 
 lemmas [corresKwp_wp_comb_del] =
-  hoare_vcg_precond_imp
-  hoare_vcg_precond_impE
-  hoare_vcg_precond_impE_R
+  hoare_weaken_pre
+  hoare_weaken_preE
+  hoare_weaken_preE_R
 
 lemma corres_inst_conj_lift[corresKwp_wp_comb]:
   "\<lbrakk>\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. corres_inst_eq (R s) (P s)\<rbrakk> \<Longrightarrow>

diff --git a/lib/EquivValid.thy b/lib/EquivValid.thy
@@ -513,7 +513,7 @@ lemma liftME_ev:
   shows "equiv_valid_inv I A P (liftME f g)"
   apply(simp add: liftME_def)
   apply (rule bindE_ev_pre[OF returnOk_ev reads_res])
-  apply (rule hoare_True_E_R)
+  apply (rule hoareE_R_TrueI)
   apply fast
   done
 
@@ -645,7 +645,7 @@ lemma mapME_ev_pre:
    apply(subst mapME_Cons)
    apply wp
    apply fastforce
-   apply (rule hoare_True_E_R[where P="\<top>"])
+   apply (rule wp_post_tautE_R)
    apply fastforce+
   done
 

diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy
@@ -72,7 +72,7 @@ next
   show ?case
     apply (simp add: mapM_Cons)
     apply (rule corres_underlying_split [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]])
-    apply (rule corres_underlying_split [OF Cons(3) _ hoare_post_taut hoare_post_taut])
+    apply (rule corres_underlying_split [OF Cons(3) _ hoare_TrueI hoare_TrueI])
     apply (simp add: rc)
     apply (rule Cons.hyps)+
     done

diff --git a/lib/HaskellLemmaBucket.thy b/lib/HaskellLemmaBucket.thy
@@ -225,15 +225,15 @@ lemma findM_on_outcome':
 lemma findM_on_outcome:
   assumes x: "\<And>x ys. x \<in> set xs \<Longrightarrow> \<lbrace>Q None and I\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrace>"
   shows      "\<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace>"
-  apply (rule hoare_vcg_precond_imp)
+  apply (rule hoare_weaken_pre)
    apply (rule findM_on_outcome' [where fn="\<lambda>s. if I s then set xs else {}"])
    apply (case_tac "x \<notin> set xs")
     apply simp
    apply (simp cong: rev_conj_cong)
    apply (case_tac "\<not> set xsa \<subseteq> set xs")
     apply simp
    apply simp
-   apply (rule hoare_vcg_precond_imp)
+   apply (rule hoare_weaken_pre)
     apply (rule hoare_post_imp [OF _ x])
      apply clarsimp
     apply assumption

diff --git a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy
@@ -31,10 +31,10 @@ lemma hoare_eq_post: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace
   by (rule hoare_strengthen_post, assumption, clarsimp)
 
 lemma hoare_eq_postE: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>E\<rbrace>"
-  by (metis (full_types) hoare_post_impErr')
+  by (metis (full_types) hoare_strengthen_postE)
 
 lemma hoare_eq_postE_R: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, -"
-  by (metis hoare_post_imp_R)
+  by (metis hoare_strengthen_postE_R)
 
 ML \<open>
 val sep_select_post_method =  sep_select_generic_method false [@{thm hoare_eq_post},

diff --git a/lib/Monad_Lists.thy b/lib/Monad_Lists.thy
@@ -469,8 +469,8 @@ lemma filterM_distinct1:
   apply (rule rev_induct [where xs=xs])
    apply (clarsimp | wp)+
   apply (simp add: filterM_append)
-  apply (erule hoare_seq_ext[rotated])
-  apply (rule hoare_seq_ext[rotated], rule hoare_vcg_prop)
+  apply (erule bind_wp_fwd)
+  apply (rule bind_wp_fwd, rule hoare_vcg_prop)
   apply (wp, clarsimp)
   apply blast
   done
@@ -601,15 +601,15 @@ lemma mapME_set:
   and     invp: "\<And>x y. \<lbrace>R and P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>, -"
   and     invr: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>\<lambda>_. R\<rbrace>, -"
   shows "\<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>, -"
-proof (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs)
+proof (rule hoare_strengthen_postE_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs)
   case Nil
   thus ?case by (simp add: mapME_Nil | wp returnOKE_R_wp)+
 next
   case (Cons y ys)
 
   have minvp: "\<And>x. \<lbrace>R and P x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, -"
     apply (rule hoare_pre)
-     apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_post_imp_R)
+     apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_strengthen_postE_R)
       apply (wp mapME_wp' invr invp)+
       apply simp
      apply simp
@@ -619,7 +619,7 @@ next
   show ?case
     apply (simp add: mapME_Cons)
     apply (wp)
-     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P x s" in hoare_post_imp_R)
+     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P rv s" in hoare_strengthen_postE_R)
       apply (wp Cons.hyps minvp)
      apply simp
     apply (fold validE_R_def)

diff --git a/lib/SpecValid_R.thy b/lib/SpecValid_R.thy
@@ -46,14 +46,14 @@ lemma drop_equalled_validE:
 lemma drop_spec_valid[wp_split]:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (simp add: spec_valid_def)
-  apply (erule hoare_vcg_precond_imp)
+  apply (erule hoare_weaken_pre)
   apply clarsimp
   done
 
 lemma drop_spec_validE[wp_split]:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   apply (simp add: spec_validE_def)
-  apply (erule hoare_vcg_precond_impE)
+  apply (erule hoare_weaken_preE)
   apply clarsimp
   done
 

diff --git a/lib/SubMonadLib.thy b/lib/SubMonadLib.thy
@@ -343,13 +343,13 @@ lemma corres_submonad:
    apply (fastforce simp: corres_underlying_def stateAssert_def get_def
                          assert_def return_def bind_def)
   apply (rule corres_underlying_split [where r'="\<lambda>x y. (x, y) \<in> ssr",
-                             OF _ _ hoare_post_taut hoare_post_taut])
+                             OF _ _ hoare_TrueI hoare_TrueI])
    apply clarsimp
   apply (rule corres_underlying_split [where r'="\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr",
-                             OF _ _ hoare_post_taut hoare_post_taut])
+                             OF _ _ hoare_TrueI hoare_TrueI])
    defer
    apply clarsimp
-   apply (rule corres_underlying_split [where r'=dc, OF _ _ hoare_post_taut hoare_post_taut])
+   apply (rule corres_underlying_split [where r'=dc, OF _ _ hoare_TrueI hoare_TrueI])
     apply (simp add: corres_modify')
    apply clarsimp
   apply (rule corres_select_f_stronger)

diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy
@@ -1222,7 +1222,7 @@ lemmas prefix_refinement_bind_isr = prefix_refinement_bind[where isr=isr and int
 lemmas pfx_refn_bind =
   prefix_refinement_bind_v[where sr=sr and isr=sr and osr=sr and intsr=sr for sr]
 lemmas pfx_refn_bindT =
-  pfx_refn_bind[where P'="\<top>" and Q'="\<lambda>_ _. True", OF _ _ hoare_post_taut twp_post_taut,
+  pfx_refn_bind[where P'="\<top>" and Q'="\<lambda>_ _. True", OF _ _ hoare_TrueI twp_post_taut,
                 simplified pred_conj_def, simplified]
 
 \<comment> \<open>FIXME: these are copied from Corres_UL.thy, move somewhere that they can be shared\<close>

diff --git a/proof/access-control/ARM/ArchArch_AC.thy b/proof/access-control/ARM/ArchArch_AC.thy
@@ -159,7 +159,7 @@ lemma unmap_page_table_respects:
   apply (rule hoare_gen_asm)
   apply (simp add: unmap_page_table_def page_table_mapped_def )
   apply (rule hoare_pre)
-   apply (wpsimp wp: store_pde_respects page_table_mapped_wp_weak get_pde_wp hoare_vcg_all_lift_R
+   apply (wpsimp wp: store_pde_respects page_table_mapped_wp_weak get_pde_wp hoare_vcg_all_liftE_R
                simp: cleanByVA_PoU_def
           | wp (once) hoare_drop_imps)+
   apply auto
@@ -372,7 +372,7 @@ lemma lookup_pt_slot_authorised3:
    \<lbrace>\<lambda>rv _.  \<forall>x\<in>set [rv, rv + 4 .e. rv + 0x3C]. is_subject aag (x && ~~ mask pt_bits)\<rbrace>, -"
   apply (rule_tac Q'="\<lambda>rv s. is_aligned rv 6 \<and> (\<forall>x\<in>set [0, 4 .e. 0x3C].
                                                   is_subject aag (x + rv && ~~ mask pt_bits))"
-               in hoare_post_imp_R)
+               in hoare_strengthen_postE_R)
   apply (rule hoare_pre)
   apply (wp lookup_pt_slot_is_aligned_6 lookup_pt_slot_authorised2)
    apply (fastforce simp: vmsz_aligned_def pd_bits_def pageBits_def)
@@ -830,7 +830,6 @@ lemma decode_arch_invocation_authorised:
           | wpc
           | simp add: authorised_asid_control_inv_def authorised_page_inv_def
                       authorised_page_directory_inv_def
-                 del: hoare_True_E_R
                  split del: if_split)+
   apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def
                         neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs)

diff --git a/proof/access-control/ARM/ArchFinalise_AC.thy b/proof/access-control/ARM/ArchFinalise_AC.thy
@@ -28,7 +28,7 @@ lemma sbn_st_vrefs[Finalise_AC_assms, wp]:
 lemma arch_finalise_cap_auth'[Finalise_AC_assms]:
    "\<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace>"
   unfolding arch_finalise_cap_def
-  by (wp | wpc | simp add: comp_def hoare_post_taut[where P = \<top>] split del: if_split)+
+  by (wp | wpc | simp add: comp_def hoare_TrueI[where P = \<top>] split del: if_split)+
 
 lemma arch_finalise_cap_obj_refs[Finalise_AC_assms]:
   "\<lbrace>\<lambda>s. \<forall>x \<in> aobj_ref' acap. P x\<rbrace>

diff --git a/proof/access-control/ARM/ArchRetype_AC.thy b/proof/access-control/ARM/ArchRetype_AC.thy
@@ -174,7 +174,7 @@ lemma copy_global_mappings_pas_refined:
                                valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s)"
                  in hoare_strengthen_post)
      apply (rule mapM_x_wp[OF _ subset_refl])
-     apply (rule hoare_seq_ext)
+     apply (rule bind_wp)
       apply (unfold o_def)
     (* Use [1] so wp doesn't filter out the global_pd condition *)
       apply (wp store_pde_pas_refined store_pde_valid_kernel_mappings_map_global)[1]

diff --git a/proof/access-control/ARM/ArchTcb_AC.thy b/proof/access-control/ARM/ArchTcb_AC.thy
@@ -33,14 +33,14 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
   apply (subst invoke_tcb.simps)
   apply (subst option_update_thread_def)
   apply (subst set_priority_extended.dxo_eq)
-  apply (rule hoare_vcg_precond_imp)
+  apply (rule hoare_weaken_pre)
    apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
                  in hoare_gen_asm)
    apply (simp only: split_def)
-   apply (((simp add: conj_comms del: hoare_True_E_R,
+   apply (((simp add: conj_comms,
            strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
           | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
-          | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_lift_R
+          | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R
                  hoare_vcg_E_elim hoare_vcg_const_imp_lift_R hoare_vcg_R_conj
           | wp restart_integrity_autarch set_mcpriority_integrity_autarch
                as_user_integrity_autarch thread_set_integrity_autarch
@@ -54,7 +54,7 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
                out_invs_trivial case_option_wpE cap_delete_deletes
                cap_delete_valid_cap cap_insert_valid_cap out_cte_at
                cap_insert_cte_at cap_delete_cte_at out_valid_cap out_tcb_valid
-               hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
+               hoare_vcg_const_imp_lift_R hoare_vcg_all_liftE_R
                thread_set_tcb_ipc_buffer_cap_cleared_invs
                thread_set_invs_trivial[OF ball_tcb_cap_casesI]
                hoare_vcg_all_lift thread_set_valid_cap out_emptyable
@@ -78,7 +78,6 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
                cap_delete_pas_refined'[THEN valid_validE_E] thread_set_cte_wp_at_trivial
           | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
                       emptyable_def a_type_def partial_inv_def
-                 del: hoare_True_E_R
           | wpc
           | strengthen invs_mdb use_no_cap_to_obj_asid_strg
                        tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]

diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy
@@ -211,7 +211,7 @@ lemma lookup_slot_for_cnode_op_authorised[wp]:
   apply (simp add: lookup_slot_for_cnode_op_def split del: if_split)
   apply (wp whenE_throwError_wp hoare_drop_imps
             resolve_address_bits_authorised
-              [THEN hoare_post_imp_R[where Q'="\<lambda>x s. is_subject aag (fst (fst x))"]]
+              [THEN hoare_strengthen_postE_R[where Q'="\<lambda>x s. is_subject aag (fst (fst x))"]]
          | wpc | fastforce)+
   done
 
@@ -246,7 +246,7 @@ lemma decode_cnode_inv_authorised:
   apply (simp add: authorised_cnode_inv_def decode_cnode_invocation_def
                    split_def whenE_def unlessE_def set_eq_iff
              cong: if_cong Invocations_A.cnode_invocation.case_cong split del: if_split)
-  apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R lsfco_cte_at
+  apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift_R hoare_vcg_all_liftE_R lsfco_cte_at
          | wp (once) get_cap_cur_auth)+
   apply (subgoal_tac "\<forall>n. n < length excaps
                           \<longrightarrow> (is_cnode_cap (excaps ! n)

diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy
@@ -902,8 +902,8 @@ lemma receive_ipc_domain_sep_inv:
    \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>"
   unfolding receive_ipc_def
   apply (simp add: receive_ipc_def split: cap.splits, clarsimp)
-  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
-  apply (rule hoare_seq_ext[OF _ gbn_sp])
+  apply (rule bind_wp[OF _ get_simple_ko_sp])
+  apply (rule bind_wp[OF _ gbn_sp])
   apply (case_tac ntfnptr, simp)
    apply (wp receive_ipc_base_domain_sep_inv get_simple_ko_wp | simp split: if_split option.splits)+
   done
@@ -1040,7 +1040,7 @@ lemma invoke_tcb_domain_sep_inv:
     apply (case_tac option)
      apply  ((wp | simp)+)[1]
     apply (simp add: split_def cong: option.case_cong)
-    apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_lift_R hoare_vcg_all_lift
+    apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_liftE_R hoare_vcg_all_lift
               hoare_vcg_const_imp_lift_R cap_delete_domain_sep_inv cap_delete_deletes
               dxo_wp_weak cap_delete_valid_cap cap_delete_cte_at hoare_weak_lift_imp
            | wpc | strengthen
@@ -1080,11 +1080,11 @@ lemma handle_invocation_domain_sep_inv:
          | simp split del: if_split)+
         apply (rule_tac E="\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of
                                                        and valid_mdb and (\<lambda>y. valid_fault ft)"
-                    and R="Q" and Q=Q for Q in hoare_post_impErr)
+                    and R="Q" and Q=Q for Q in hoare_strengthen_postE)
          apply (wp | simp | clarsimp)+
       apply (rule_tac E="\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and
                               valid_mdb and (\<lambda>y. valid_fault (CapFault x False ft))"
-                  and R="Q" and Q=Q for Q in hoare_post_impErr)
+                  and R="Q" and Q=Q for Q in hoare_strengthen_postE)
         apply (wp lcs_ex_cap_to2 | clarsimp)+
   apply (auto intro: st_tcb_ex_cap simp: ct_in_state_def)
   done
@@ -1150,7 +1150,7 @@ lemma handle_recv_domain_sep_inv:
          | (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. cur_thread s = thread)" in hoare_strengthen_post, wp,
             clarsimp simp: invs_valid_objs invs_sym_refs))+
      apply (rule_tac Q'="\<lambda>r s. domain_sep_inv irqs st s \<and> invs s \<and>
-                               tcb_at thread s \<and> thread = cur_thread s" in hoare_post_imp_R)
+                               tcb_at thread s \<and> thread = cur_thread s" in hoare_strengthen_postE_R)
       apply wp
      apply ((clarsimp simp add: invs_valid_objs invs_sym_refs
              | intro impI allI conjI
@@ -1174,7 +1174,7 @@ lemma handle_event_domain_sep_inv:
                          handle_recv_domain_sep_inv handle_reply_domain_sep_inv hy_inv
               | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def)+
      apply (rule_tac E="\<lambda>rv s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state) \<and>
-                               invs s \<and> valid_fault rv" and R="Q" and Q=Q for Q in hoare_post_impErr)
+                               invs s \<and> valid_fault rv" and R="Q" and Q=Q for Q in hoare_strengthen_postE)
      apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def | auto)+
   done
 

diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy
@@ -163,7 +163,7 @@ lemma cancel_badged_sends_respects[wp]:
                      and Q="P" and I="P" for P])
       apply simp
      apply (simp add: bind_assoc)
-     apply (rule hoare_seq_ext[OF _ gts_sp])
+     apply (rule bind_wp[OF _ gts_sp])
      apply (rule hoare_pre)
       apply (wp sts_respects_restart_ep hoare_vcg_const_Ball_lift sts_st_tcb_at_neq)
      apply clarsimp
@@ -391,7 +391,7 @@ lemma cancel_all_signals_respects[wp]:
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (clarsimp simp add: cancel_all_signals_def)
-  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp], rule hoare_pre)
+  apply (rule bind_wp[OF _ get_simple_ko_sp], rule hoare_pre)
    apply (wp mapM_x_inv_wp2
              [where I="integrity aag X st"
                 and V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"]
@@ -444,7 +444,7 @@ lemma unbind_notification_respects:
    unbind_notification t
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (clarsimp simp: unbind_notification_def)
-  apply (rule hoare_seq_ext[OF _ gbn_sp])
+  apply (rule bind_wp[OF _ gbn_sp])
   apply (wp set_ntfn_respects hoare_vcg_ex_lift gbn_wp | wpc | simp)+
   apply (clarsimp simp: pred_tcb_at_def obj_at_def split: option.splits)
   apply blast
@@ -549,7 +549,7 @@ lemma cancel_signal_respects[wp]:
    cancel_signal t ntfnptr
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: cancel_signal_def)
-  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
+  apply (rule bind_wp[OF _ get_simple_ko_sp])
   apply (rule hoare_pre)
    apply (wp set_thread_state_integrity_autarch set_ntfn_respects | wpc | fastforce)+
   done
@@ -559,7 +559,7 @@ lemma cancel_ipc_respects[wp]:
    cancel_ipc t
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: cancel_ipc_def)
-  apply (rule hoare_seq_ext[OF _ gts_sp])
+  apply (rule bind_wp[OF _ gts_sp])
   apply (rule hoare_pre)
    apply (wp set_thread_state_integrity_autarch set_endpoint_respects get_simple_ko_wp
           | wpc
@@ -703,7 +703,7 @@ lemma finalise_cap_auth':
   including classic_wp_pre
   apply (rule hoare_gen_asm)
   apply (cases cap, simp_all split del: if_split)
-             apply (wp | simp add: comp_def hoare_post_taut[where P = \<top>] split del: if_split
+             apply (wp | simp add: comp_def hoare_TrueI[where P = \<top>] split del: if_split
                        | fastforce simp: aag_cap_auth_Zombie aag_cap_auth_CNode aag_cap_auth_Thread)+
     apply (rule hoare_pre)
      apply (wp | simp)+
@@ -959,9 +959,9 @@ lemma rec_del_respects_CTEDelete_transferable':
    apply (solves \<open>simp\<close>)
   apply (subst rec_del.simps[abs_def])
   apply (wpsimp wp: wp_transferable hoare_weak_lift_imp)
-    apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
+    apply (rule hoare_strengthen_postE,rule rec_del_Finalise_transferable)
      apply simp apply simp
-   apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
+   apply (rule hoare_strengthen_postE,rule rec_del_Finalise_transferable)
     apply simp apply simp
   apply (clarsimp)
   apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb])