diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
index f68d32c8cf..8db34a1e0c 100644
--- a/lib/Monads/nondet/Nondet_VCG.thy
+++ b/lib/Monads/nondet/Nondet_VCG.thy
@@ -487,6 +487,24 @@ lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
 lemmas hoare_seq_ext = seq_ext[rotated]
 lemmas hoare_vcg_seqE = seqE[rotated]
 
+lemmas hoare_vcg_seqE_R = validE_validE_R[OF hoare_vcg_seqE [OF validE_R_validE validE_R_validE]]
+lemmas hoare_vcg_seqE_E = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
+
+lemma hoare_seq_extE_R:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE_E:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x -,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g -,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_E_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_def)
+  by (wp | assumption)+
+
 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 (erule seq_ext) (clarsimp simp: valid_def)
@@ -1066,8 +1084,7 @@ lemmas all_classic_wp_combs =
   hoare_classic_wp_combs
 
 lemmas hoare_wp_splits[wp_split] =
-  hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
-  validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
+  handleE'_wp handleE_wp
   validE_validE_R [OF handleE'_wp [OF validE_R_validE]]
   validE_validE_R [OF handleE_wp [OF validE_R_validE]]
   catch_wp hoare_vcg_if_split hoare_vcg_if_splitE
@@ -1078,9 +1095,20 @@ lemmas hoare_wp_splits[wp_split] =
 
 lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE  hoare_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   hoare_seq_ext, hoare_vcg_seqE and their variants are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] =
+  hoare_vcg_prop hoare_seq_ext
+  hoare_vcg_seqE_R hoare_vcg_seqE_E hoare_vcg_seqE
+  hoare_seq_extE_R hoare_seq_extE_E hoare_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = hoare_vcg_prop
-              wp_post_taut
+lemmas [wp] = wp_post_taut
               hoare_fun_app_wp
               returnOk_E
               liftE_validE_E
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index baff602f5b..a56cea300b 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -858,6 +858,11 @@ lemma rg_vcg_split_case_sum:
        \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>"
   by (cases x; simp)
 
+lemma rg_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validIE_def)
+  by (wp | assumption)+
+
 lemma bind_twp_nobind:
   "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> do f; g od \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>"
   by (erule bind_twp_fwd) clarsimp
@@ -1409,16 +1414,24 @@ lemmas all_rg_classic_wp_combs =
   rg_classic_wp_combs
 
 lemmas rg_wp_splits[wp_split] =
-  bind_twp bindE_twp handleE'_twp handleE_twp
+  handleE'_twp handleE_twp
   catch_twp rg_vcg_if_split rg_vcg_if_splitE
   liftM_twp liftME_twp whenE_twp unlessE_twp
   validIE_validI
 
 lemmas [wp_comb] = rg_wp_state_combsE rg_wp_combsE rg_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   bind_twp, bindE_twp and rg_seq_extE are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   rg_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] = rg_vcg_prop bind_twp bindE_twp rg_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = rg_vcg_prop
-              twp_post_taut
+lemmas [wp] = twp_post_taut
               twp_post_tautE
               rg_fun_app_twp
               liftE_twp
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index bd68d0cedd..1fc46c6daa 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -520,6 +520,24 @@ lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
 lemmas hoare_seq_ext = seq_ext[rotated]
 lemmas hoare_vcg_seqE = seqE[rotated]
 
+lemmas hoare_vcg_seqE_R = validE_validE_R[OF hoare_vcg_seqE [OF validE_R_validE validE_R_validE]]
+lemmas hoare_vcg_seqE_E = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
+
+lemma hoare_seq_extE_R:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE_E:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x -,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g -,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_E_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_def)
+  by (wp | assumption)+
+
 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 (erule seq_ext) (clarsimp simp: valid_def)
@@ -1102,7 +1120,7 @@ lemmas all_classic_wp_combs =
   hoare_classic_wp_combs
 
 lemmas hoare_wp_splits[wp_split] =
-  hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
+  handleE'_wp handleE_wp
   validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
   validE_validE_R [OF handleE'_wp [OF validE_R_validE]]
   validE_validE_R [OF handleE_wp [OF validE_R_validE]]
@@ -1114,9 +1132,20 @@ lemmas hoare_wp_splits[wp_split] =
 
 lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE  hoare_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   hoare_seq_ext, hoare_vcg_seqE and their variants are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] =
+  hoare_vcg_prop hoare_seq_ext
+  hoare_vcg_seqE_R hoare_vcg_seqE_E hoare_vcg_seqE
+  hoare_seq_extE_R hoare_seq_extE_E hoare_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = hoare_vcg_prop
-              wp_post_taut
+lemmas [wp] = wp_post_taut
               hoare_fun_app_wp
               returnOk_E
               liftE_validE_E
diff --git a/proof/access-control/ARM/ArchInterrupt_AC.thy b/proof/access-control/ARM/ArchInterrupt_AC.thy
index a58fc92270..e7a833797f 100644
--- a/proof/access-control/ARM/ArchInterrupt_AC.thy
+++ b/proof/access-control/ARM/ArchInterrupt_AC.thy
@@ -87,17 +87,12 @@ lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    arch_decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
+  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def Let_def
             authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen  aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)
diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy
index aa92c68dd3..b97a3eaef1 100644
--- a/proof/access-control/Finalise_AC.thy
+++ b/proof/access-control/Finalise_AC.thy
@@ -958,18 +958,11 @@ lemma rec_del_respects_CTEDelete_transferable':
    apply (wp rec_del_respects'')
    apply (solves \<open>simp\<close>)
   apply (subst rec_del.simps[abs_def])
-  apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
-                 rec_del_Finalise_transferable
-            del: wp_not_transferable
-         | wpc)+
+  apply (wpsimp wp: wp_transferable hoare_weak_lift_imp)
     apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
-     apply simp apply (elim conjE) apply simp apply simp
-   apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
-                  rec_del_Finalise_transferable
-             del: wp_not_transferable
-          | wpc)+
+     apply simp apply simp
    apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
-    apply simp apply (elim conjE) apply simp apply simp
+    apply simp apply simp
   apply (clarsimp)
   apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb])
   by (safe; simp)
diff --git a/proof/access-control/Interrupt_AC.thy b/proof/access-control/Interrupt_AC.thy
index f85af98fb9..7fc6003aab 100644
--- a/proof/access-control/Interrupt_AC.thy
+++ b/proof/access-control/Interrupt_AC.thy
@@ -152,17 +152,11 @@ lemma decode_irq_control_invocation_authorised [wp]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x s. authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def authorised_irq_ctl_inv_def
+  unfolding decode_irq_control_invocation_def authorised_irq_ctl_inv_def Let_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp arch_decode_irq_control_invocation_authorised
-             whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen  aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp arch_decode_irq_control_invocation_authorised simp: o_def)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)
diff --git a/proof/access-control/RISCV64/ArchInterrupt_AC.thy b/proof/access-control/RISCV64/ArchInterrupt_AC.thy
index 6aec17f88b..cf742b0c30 100644
--- a/proof/access-control/RISCV64/ArchInterrupt_AC.thy
+++ b/proof/access-control/RISCV64/ArchInterrupt_AC.thy
@@ -87,17 +87,12 @@ lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    arch_decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
+  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def Let_def
             authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)
diff --git a/proof/capDL-api/Invocation_DP.thy b/proof/capDL-api/Invocation_DP.thy
index d1736068d1..858ad14021 100644
--- a/proof/capDL-api/Invocation_DP.thy
+++ b/proof/capDL-api/Invocation_DP.thy
@@ -294,7 +294,7 @@ lemma decode_invocation_nonep:
    decode_invocation cap cap_ref extra_caps intent
    \<lbrace>\<lambda>rv s. nonep_invocation rv\<rbrace>, -"
   apply (simp add: decode_invocation_def)
-  apply (wpsimp simp: o_def nonep_invocation_def simp_del: hoare_True_E_R)
+  apply (wpsimp simp: o_def nonep_invocation_def)
   apply (auto simp: ep_related_cap_def)
   done
 
@@ -578,9 +578,7 @@ lemma call_kernel_with_intent_no_fault_helper:
                 | Inr rv \<Rightarrow> Q (Inr rv) s" and Q=Q for Q, rotated])
          apply (case_tac r, simp_all)[1]
         apply (simp add: validE_def[symmetric])
-        apply (rule hoare_pre, wp)
-          apply (simp add: validE_def, (wp | simp add: validE_def[symmetric])+)
-          apply (wp handle_pending_interrupts_no_ntf_cap)
+        apply (wp handle_pending_interrupts_no_ntf_cap)
          apply (rule handle_event_syscall_no_decode_exception
                    [where cur_thread = root_tcb_id
                       and intent_op = intent_op
@@ -1071,10 +1069,7 @@ lemma call_kernel_with_intent_allow_error_helper:
                 | Inr rv \<Rightarrow> Q (Inr rv) s" and Q=Q for Q, rotated])
          apply (case_tac r, simp_all)[1]
         apply (simp add: validE_def[symmetric])
-        apply (rule hoare_pre, wp)
-          apply (simp add: validE_def, (wp | simp add: validE_def[symmetric])+)
-          apply (wp handle_pending_interrupts_no_ntf_cap)
-
+        apply (wp handle_pending_interrupts_no_ntf_cap)
          apply (rule handle_event_syscall_allow_error
                        [where cur_thread = root_tcb_id
                           and intent_op = intent_op
diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy
index 7ac7351dd6..de960019ad 100644
--- a/proof/drefine/Arch_DR.thy
+++ b/proof/drefine/Arch_DR.thy
@@ -963,7 +963,7 @@ next
         apply (simp add: pd_shifting_dual ucast_nat_def shiftr_20_less triple_shift_fun
                          le_shiftr linorder_not_le)
        apply (rule hoare_pre, wp, auto)[1]
-      apply (wp | simp)+
+      apply (wp weak_if_wp | simp)+
     apply (clarsimp simp: is_final_cap'_def
       is_final_cap_def split:list.splits)
     apply (simp add: liftE_bindE is_final_cap_def corres_symb_exec_in_gets
diff --git a/proof/drefine/Corres_D.thy b/proof/drefine/Corres_D.thy
index db947dae27..ba11d6b38f 100644
--- a/proof/drefine/Corres_D.thy
+++ b/proof/drefine/Corres_D.thy
@@ -633,6 +633,7 @@ lemma dcorres_rhs_noop_above: "\<lbrakk> dcorres anyrel P P' (return ()) m; dcor
 lemmas dcorres_rhs_noop_below_True = dcorres_rhs_noop_below[OF _ _ hoare_TrueI hoare_TrueI]
 lemmas dcorres_rhs_noop_above_True = dcorres_rhs_noop_above[OF _ _ hoare_TrueI hoare_TrueI]
 
+\<comment> \<open>FIXME: remove\<close>
 declare hoare_TrueI[simp]
 
 lemma dcorres_dc_rhs_noop_below_gen:
diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy
index 0e1a3b35c1..3858afc91d 100644
--- a/proof/drefine/Syscall_DR.thy
+++ b/proof/drefine/Syscall_DR.thy
@@ -1325,21 +1325,12 @@ lemma handle_invocation_corres:
           apply (simp add: not_idle_thread_def)
           apply (strengthen invs_valid_idle)
           apply wp+
-        apply (simp add:conj_comms not_idle_thread_def split_def)
+        \<comment> \<open>The following proof is quite fragile. If clarsimp is used, either on its own or as part
+            of wpsimp, then it rewrites pairs and necessary rules no longer match.\<close>
+        apply (simp add: not_idle_thread_def split_def)
         apply (wp sts_Restart_invs set_thread_state_ct_active)+
-       apply (simp add:conj_comms split_def msg_from_syscall_error_simp)
-       apply (wp | simp add:split_def)+
-      apply (rule_tac Q'="\<lambda>r s. s = s'a \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_invocation r s \<and>
-                                invocation_duplicates_valid r s"
-                      in hoare_post_imp_R)
-       apply (simp add:split_def liftE_bindE[symmetric])
-       apply (wp decode_inv_wf)
-      apply (clarsimp simp:ct_in_state_def st_tcb_at_def obj_at_def not_idle_thread_def)+
-     apply (rule wp_post_tautE)
-    apply clarsimp
-    apply wp
-       apply (simp add:split_def liftE_bindE[symmetric])
-       apply (wp | simp add: split_def liftE_bindE[symmetric])+
+       apply (simp add: split_def msg_from_syscall_error_simp)
+       apply (wp | simp add: split_def)+
       apply (rule_tac Q="\<lambda>r s. s = s'a \<and>
                                evalMonad (lookup_ipc_buffer False (cur_thread s'a)) s'a = Some r \<and>
                                cte_wp_at (Not \<circ> is_master_reply_cap) (snd x) s \<and>
@@ -1351,12 +1342,12 @@ lemma handle_invocation_corres:
                                (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to \<top> r s)"
                       in hoare_strengthen_post)
        apply (wp evalMonad_wp)
-         apply (simp add: empty_when_fail_lookup_ipc_buffer  weak_det_spec_lookup_ipc_buffer)+
+         apply (simp add: empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+
        apply wp
       apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_idle_def st_tcb_ex_cap
                             ct_in_state_def pred_tcb_at_def not_idle_thread_def obj_at_def
                      dest!: get_tcb_SomeD)
-     apply (wp)+
+     apply wp+
     apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def pred_tcb_at_def obj_at_def)
    apply simp_all
   done
diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy
index 6effc4ba93..d9c3987751 100644
--- a/proof/drefine/Tcb_DR.thy
+++ b/proof/drefine/Tcb_DR.thy
@@ -1117,8 +1117,7 @@ lemma dcorres_tcb_update_ipc_buffer:
              apply wp
             apply wpsimp
            apply (wp when_wp)+
-          apply (rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top>]],clarsimp+)
-        apply (wp wp_post_taut hoare_drop_imp get_cap_weak_wp)+
+        apply (wpsimp wp: wp_post_taut hoare_drop_imp get_cap_weak_wp simp_del: hoare_TrueI)+
       apply (clarsimp simp:conj_comms)
       apply (wp thread_set_global_refs_triv thread_set_valid_idle)
        apply (clarsimp simp:tcb_cap_cases_def)
diff --git a/proof/infoflow/ARM/ArchRetype_IF.thy b/proof/infoflow/ARM/ArchRetype_IF.thy
index d30498d5a1..02a14a160e 100644
--- a/proof/infoflow/ARM/ArchRetype_IF.thy
+++ b/proof/infoflow/ARM/ArchRetype_IF.thy
@@ -471,30 +471,31 @@ lemma reset_untyped_cap_reads_respects_g:
         apply (frule(1) caps_of_state_valid)
         apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                               free_index_of_def invs_valid_global_objs)
-        apply (simp add: aligned_add_aligned is_aligned_shiftl)
-        apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
+       apply (simp add: aligned_add_aligned is_aligned_shiftl)
+       apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
        apply (rule hoare_pre)
         apply (wp preemption_point_inv' set_untyped_cap_invs_simple set_cap_cte_wp_at
                   set_cap_no_overlap only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
+                  irq_state_independent_A_conjI
                | simp)+
         apply (strengthen empty_descendants_range_in)
-         apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
-                | simp | wp (once) dmo_wp)+
-        apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
-        apply (frule(1) caps_of_state_valid)
-        apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
-       apply (wp | simp)+
-       apply (wp delete_objects_reads_respects_g)
-      apply (simp add: if_apply_def2)
-      apply (strengthen invs_valid_global_objs)
-      apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
-                     delete_objects_pspace_no_overlap_again
-                     delete_objects_valid_arch_state
-                     only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
-                del: Untyped_AI.delete_objects_pspace_no_overlap
-             | simp)+
-     apply (rule get_cap_reads_respects_g)
-    apply (wp get_cap_wp)
+        apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
+               | simp | wp (once) dmo_wp)+
+       apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
+       apply (frule(1) caps_of_state_valid)
+       apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
+      apply (wp | simp)+
+      apply (wp delete_objects_reads_respects_g)
+     apply (simp add: if_apply_def2)
+     apply (strengthen invs_valid_global_objs)
+     apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
+                    delete_objects_pspace_no_overlap_again
+                    delete_objects_valid_arch_state
+                    only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
+               del: Untyped_AI.delete_objects_pspace_no_overlap
+            | simp)+
+    apply (rule get_cap_reads_respects_g)
+   apply (wp get_cap_wp)
   apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
   apply (frule(1) caps_of_state_valid)
   apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
diff --git a/proof/infoflow/RISCV64/ArchRetype_IF.thy b/proof/infoflow/RISCV64/ArchRetype_IF.thy
index 749c1de80d..7674bc01c7 100644
--- a/proof/infoflow/RISCV64/ArchRetype_IF.thy
+++ b/proof/infoflow/RISCV64/ArchRetype_IF.thy
@@ -413,30 +413,31 @@ lemma reset_untyped_cap_reads_respects_g:
         apply (frule(1) caps_of_state_valid)
         apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                               free_index_of_def invs_valid_global_objs)
-        apply (simp add: aligned_add_aligned is_aligned_shiftl)
-        apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
+       apply (simp add: aligned_add_aligned is_aligned_shiftl)
+       apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
        apply (rule hoare_pre)
         apply (wp preemption_point_inv' set_untyped_cap_invs_simple set_cap_cte_wp_at
                   set_cap_no_overlap only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
+                  irq_state_independent_A_conjI
                | simp)+
         apply (strengthen empty_descendants_range_in)
-         apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
-                | simp | wp (once) dmo_wp)+
-        apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
-        apply (frule(1) caps_of_state_valid)
-        apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
-       apply (wp | simp)+
-       apply (wp delete_objects_reads_respects_g)
-      apply (simp add: if_apply_def2)
-      apply (strengthen invs_valid_global_objs)
-      apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
-                     delete_objects_pspace_no_overlap_again
-                     only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
-                     delete_objects_valid_arch_state
-                del: Untyped_AI.delete_objects_pspace_no_overlap
-             | simp)+
-     apply (rule get_cap_reads_respects_g)
-    apply (wp get_cap_wp)
+        apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
+               | simp | wp (once) dmo_wp)+
+       apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
+       apply (frule(1) caps_of_state_valid)
+       apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
+      apply (wp | simp)+
+      apply (wp delete_objects_reads_respects_g)
+     apply (simp add: if_apply_def2)
+     apply (strengthen invs_valid_global_objs)
+     apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
+                    delete_objects_pspace_no_overlap_again
+                    only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
+                    delete_objects_valid_arch_state
+               del: Untyped_AI.delete_objects_pspace_no_overlap
+            | simp)+
+    apply (rule get_cap_reads_respects_g)
+   apply (wp get_cap_wp)
   apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
   apply (frule(1) caps_of_state_valid)
   apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy
index 4c66515e52..3b5e6c0e65 100644
--- a/proof/invariant-abstract/Syscall_AI.thy
+++ b/proof/invariant-abstract/Syscall_AI.thy
@@ -1146,8 +1146,6 @@ lemma hy_inv: "(\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace
   apply (wp | simp)+
   done
 
-declare hoare_seq_ext[wp]
-
 lemma ct_active_simple [elim!]:
   "ct_active s \<Longrightarrow> st_tcb_at simple (cur_thread s) s"
   by (fastforce simp: ct_in_state_def elim!: pred_tcb_weakenE)
diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy
index d151843ac8..5d1f8f2d2f 100644
--- a/proof/refine/AARCH64/TcbAcc_R.thy
+++ b/proof/refine/AARCH64/TcbAcc_R.thy
@@ -1027,20 +1027,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done
diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy
index 9c25603b95..f9f1c3c180 100644
--- a/proof/refine/AARCH64/Tcb_R.thy
+++ b/proof/refine/AARCH64/Tcb_R.thy
@@ -1465,6 +1465,10 @@ proof -
     out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
     checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])
diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy
index 75692b7624..33e79a0476 100644
--- a/proof/refine/ARM/Arch_R.thy
+++ b/proof/refine/ARM/Arch_R.thy
@@ -1522,9 +1522,9 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
   apply (clarsimp simp:createMappingEntries_def)
   apply (rule hoare_pre)
    apply (wpc | wp lookupPTSlot_page_table_at'
-     | simp add: slots_duplicated_ensured_def)+
-     apply (rule_tac Q' = "\<lambda>p s.  is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s"
-       in  hoare_post_imp_R)
+          | simp add: slots_duplicated_ensured_def)+
+     apply (rule_tac Q' = "\<lambda>p s. is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s"
+                  in hoare_post_imp_R)
       apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at')
      apply (rename_tac rv s)
      apply (rule_tac x = rv in exI)
@@ -1533,24 +1533,21 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
       apply simp
      apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
      apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc)
-     apply simp
-    apply wp+
-   apply (intro conjI impI)
-            apply ((clarsimp simp: vmsz_aligned_def pageBitsForSize_def
-              slots_duplicated_ensured_def
-              split:vmpage_size.splits)+)[8]
-   apply clarsimp
-   apply (drule lookup_pd_slot_aligned_6)
-    apply (simp add:pdBits_def pageBits_def pdeBits_def)
-   apply (clarsimp simp:slots_duplicated_ensured_def)
-   apply (rule_tac x = "(lookup_pd_slot pd vptr)" in exI)
-   apply clarsimp
-   apply (frule is_aligned_no_wrap'[where off = "0x3c" and sz = 6])
     apply simp
-   apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
-   apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc
-                         superSectionPDEOffsets_def pdeBits_def)
-   done
+    apply wp+
+  apply (intro conjI impI; clarsimp)
+    apply ((clarsimp simp: vmsz_aligned_def slots_duplicated_ensured_def)+)[2]
+  apply (drule lookup_pd_slot_aligned_6)
+   apply (simp add: pdBits_def pageBits_def pdeBits_def)
+  apply (clarsimp simp: slots_duplicated_ensured_def)
+  apply (rule_tac x = "(lookup_pd_slot pd vptr)" in exI)
+  apply clarsimp
+  apply (frule is_aligned_no_wrap'[where off = "0x3c" and sz = 6])
+   apply simp
+  apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified])
+  apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc
+                        superSectionPDEOffsets_def pdeBits_def)
+  done
 
 lemma arch_decodeARMPageFlush_wf:
   "ARM_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy
index eaa2abc417..5dc688b212 100644
--- a/proof/refine/ARM/TcbAcc_R.thy
+++ b/proof/refine/ARM/TcbAcc_R.thy
@@ -977,20 +977,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done
diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy
index bbe4e0ad88..6e158808df 100644
--- a/proof/refine/ARM/Tcb_R.thy
+++ b/proof/refine/ARM/Tcb_R.thy
@@ -1548,6 +1548,10 @@ proof -
     out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
     checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])
diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy
index d0a22a7ab3..8a1d041ee0 100644
--- a/proof/refine/ARM_HYP/Arch_R.thy
+++ b/proof/refine/ARM_HYP/Arch_R.thy
@@ -1752,11 +1752,11 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
   apply (clarsimp simp:createMappingEntries_def)
   apply (rule hoare_pre)
    apply (wpc | wp lookupPTSlot_page_table_at'
-     | simp add: slots_duplicated_ensured_def)+
-     apply (rule_tac Q' = "\<lambda>p s.  is_aligned p 7 \<and> page_table_at' (p && ~~ mask pt_bits) s"
-       in  hoare_post_imp_R)
+          | simp add: slots_duplicated_ensured_def)+
+     apply (rule_tac Q' = "\<lambda>p s. is_aligned p 7 \<and> page_table_at' (p && ~~ mask pt_bits) s"
+                  in hoare_post_imp_R)
       apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at'
-           | simp add: vspace_bits_defs largePagePTEOffsets_def superSectionPDEOffsets_def)+
+             | simp add: vspace_bits_defs largePagePTEOffsets_def superSectionPDEOffsets_def)+
      apply (rename_tac rv s)
      apply (rule_tac x = rv in exI)
      apply clarsimp
@@ -1765,21 +1765,18 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
      apply (drule upto_enum_step_shift[where n = 7 and m = 3,simplified])
      apply (clarsimp simp:mask_def add.commute upto_enum_step_def)
     apply wp+
-   apply (intro conjI impI)
-            apply ((clarsimp simp: vmsz_aligned_def pageBitsForSize_def
-              slots_duplicated_ensured_def
-              split:vmpage_size.splits)+)[9]
-   apply clarsimp
-   apply (drule lookup_pd_slot_aligned_6)
-    apply (simp add:pdBits_def pageBits_def pd_bits_def pde_bits_def)
-   apply (clarsimp simp:slots_duplicated_ensured_def)
-   apply (rule_tac x = "(lookup_pd_slot pd vptr)" in exI)
-   apply (clarsimp simp: superSectionPDEOffsets_def Let_def pde_bits_def)
-   apply (frule is_aligned_no_wrap'[where off = "0x78" and sz = 7])
-    apply simp
-   apply (drule upto_enum_step_shift[where n = 7 and m = 3,simplified])
-   apply (clarsimp simp:mask_def add.commute upto_enum_step_def)
-   done
+  apply (intro conjI impI; clarsimp)
+    apply ((clarsimp simp: vmsz_aligned_def slots_duplicated_ensured_def)+)[2]
+  apply (drule lookup_pd_slot_aligned_6)
+   apply (simp add:pdBits_def pageBits_def pd_bits_def pde_bits_def)
+  apply (clarsimp simp:slots_duplicated_ensured_def)
+  apply (rule_tac x = "(lookup_pd_slot pd vptr)" in exI)
+  apply (clarsimp simp: superSectionPDEOffsets_def Let_def pde_bits_def)
+  apply (frule is_aligned_no_wrap'[where off = "0x78" and sz = 7])
+   apply simp
+  apply (drule upto_enum_step_shift[where n = 7 and m = 3,simplified])
+  apply (clarsimp simp:mask_def add.commute upto_enum_step_def)
+  done
 
 lemma arch_decodeARMPageFlush_wf:
   "ARM_HYP_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy
index 80957947dc..b0cc124095 100644
--- a/proof/refine/ARM_HYP/TcbAcc_R.thy
+++ b/proof/refine/ARM_HYP/TcbAcc_R.thy
@@ -1005,20 +1005,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done
diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy
index 5d0255421d..e8091f932d 100644
--- a/proof/refine/ARM_HYP/Tcb_R.thy
+++ b/proof/refine/ARM_HYP/Tcb_R.thy
@@ -1523,6 +1523,10 @@ proof -
                out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
                checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])
diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy
index c8aa05c7e3..f2d9fbb4e4 100644
--- a/proof/refine/RISCV64/TcbAcc_R.thy
+++ b/proof/refine/RISCV64/TcbAcc_R.thy
@@ -1012,20 +1012,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done
diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy
index 3854a619f4..101d292c3a 100644
--- a/proof/refine/RISCV64/Tcb_R.thy
+++ b/proof/refine/RISCV64/Tcb_R.thy
@@ -1457,6 +1457,10 @@ proof -
     out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
     checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])
diff --git a/proof/refine/RISCV64/VSpace_R.thy b/proof/refine/RISCV64/VSpace_R.thy
index 1c6ce35bf0..67c56baa2f 100644
--- a/proof/refine/RISCV64/VSpace_R.thy
+++ b/proof/refine/RISCV64/VSpace_R.thy
@@ -121,7 +121,7 @@ proof -
          apply (case_tac acap; clarsimp simp: isCap_simps catch_throwError intro!: global)
          apply (rename_tac m)
          apply (case_tac m; clarsimp simp: isCap_simps catch_throwError intro!: global)
-         apply (corres simp: lookup_failure_map_def)
+         apply (corres simp: lookup_failure_map_def wp: hoare_vcg_if_lift_ER)
           apply (frule (1) cte_wp_at_valid_objs_valid_cap)
           apply (clarsimp simp: valid_cap_def mask_def wellformed_mapdata_def)
          apply (wpsimp wp: get_cap_wp simp: getThreadVSpaceRoot_def)+
diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy
index 99e9ebc658..d34682ed73 100644
--- a/proof/refine/X64/TcbAcc_R.thy
+++ b/proof/refine/X64/TcbAcc_R.thy
@@ -1002,20 +1002,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done
diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy
index a5802efd31..9c02ebcce4 100644
--- a/proof/refine/X64/Tcb_R.thy
+++ b/proof/refine/X64/Tcb_R.thy
@@ -1483,6 +1483,10 @@ proof -
     out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
     checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])