proof: remove hoare_vcg_precond_imp from wp_comb

This being a `wp_comb` rule is a leftover from before `wp_pre` was
implemented and it is being removed because in some cases it can cause
unintended schematics to appear in the assumptions.

This commit also updates all of the proofs that accidentally
depended on it being a `wp_comb` rule. In many cases this involved
`including classic_wp_pre`, which locally returns the wp attributes to a
state similar to what it was when the proofs were first written. Other
cases required small rewrites, often involving using `wpsimp` instead of
`wp`, and removing some uses of `wp (once)`.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

proof/access-control/ARM/ArchFinalise_AC.thy

@@ -107,7 +107,7 @@ lemma finalise_cap_fst_ret[Finalise_AC_assms]:
   "\<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace>
    finalise_cap cap is_final
    \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (cases cap, simp_all add: arch_finalise_cap_def split del: if_split)
   apply (wp | simp add: comp_def split del: if_split | fastforce)+
   apply (rule hoare_pre)

proof/access-control/ARM/ArchRetype_AC.thy

@@ -98,7 +98,7 @@ lemma copy_global_mappings_integrity:
        \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (simp add: copy_global_mappings_def)
-  apply (wp mapM_x_wp[OF _ subset_refl] store_pde_respects)
+  apply (wp mapM_x_wp[OF _ subset_refl] store_pde_respects)+
     apply (drule subsetD[OF copy_global_mappings_index_subset])
     apply (fastforce simp: pd_shifting')
    apply wpsimp+
@@ -329,8 +329,7 @@ lemma dmo_freeMemory_respects[Retype_AC_assms]:
   apply wp
   apply clarsimp
   apply (erule use_valid)
-   apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch)
-   apply simp
+   apply (wpsimp wp: mol_respects mapM_x_wp' storeWord_integrity_autarch)
    apply (clarsimp simp: word_size_def word_bits_def word_size_bits_def
                          upto_enum_step_shift_red[where us=2, simplified])
    apply (erule bspec)

proof/access-control/DomainSepInv.thy

@@ -452,7 +452,7 @@ lemma finalise_cap_domain_sep_inv_cap:
   "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace>
    finalise_cap cap b
    \<lbrace>\<lambda>rv s :: det_ext state. domain_sep_inv_cap irqs (fst rv)\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (case_tac cap)
              apply (wp | simp add: o_def split del: if_split  split: cap.splits
                        | fastforce split: if_splits simp: domain_sep_inv_cap_def)+
@@ -784,7 +784,7 @@ lemma invoke_control_domain_sep_inv:
   "\<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace>
     invoke_irq_control i
    \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (case_tac i)
    apply (case_tac irqs)
     apply (wp cap_insert_domain_sep_inv' | simp )+

proof/access-control/Finalise_AC.thy

@@ -700,7 +700,7 @@ lemma finalise_cap_auth':
   "\<lbrace>pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
    finalise_cap cap final
    \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>"
-  including no_pre
+  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

proof/access-control/Ipc_AC.thy

@@ -1781,7 +1781,7 @@ lemma cap_insert_ext_integrity_in_ipc_autarch:
    apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
                          tcb_states_of_state_def get_tcb_def
               split del: if_split cong: if_cong)
-   including no_pre
+   including classic_wp_pre
    apply wp
    apply (rule hoare_vcg_conj_lift)
     apply (simp add: list_integ_def del: split_paired_All)
@@ -2655,7 +2655,7 @@ lemma empty_slot_respects_in_ipc_autarch:
   unfolding empty_slot_def post_cap_deletion_def
   apply simp
   apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch)
-       apply (wp empty_slot_extended_list_integ_lift_in_ipc empty_slot_list_integrity')
+       apply (wpsimp wp: empty_slot_extended_list_integ_lift_in_ipc empty_slot_list_integrity')
           apply simp
          apply wp+
       apply (wp set_cdt_empty_slot_respects_in_ipc_autarch)

proof/access-control/RISCV64/ArchFinalise_AC.thy

@@ -280,7 +280,7 @@ lemma finalise_cap_fst_ret[Finalise_AC_assms]:
   "\<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace>
    finalise_cap cap is_final
    \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (cases cap, simp_all add: arch_finalise_cap_def split del: if_split)
   apply (wp | simp add: comp_def split del: if_split | fastforce)+
   apply (rule hoare_pre)

proof/access-control/RISCV64/ArchRetype_AC.thy

@@ -292,8 +292,7 @@ lemma dmo_freeMemory_respects[Retype_AC_assms]:
   apply wp
   apply clarsimp
   apply (erule use_valid)
-   apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch)
-   apply simp
+   apply (wpsimp wp: mol_respects mapM_x_wp' storeWord_integrity_autarch)
    apply (clarsimp simp: word_size_def word_size_bits_def word_bits_def
                          upto_enum_step_shift_red[where us=3, simplified])
    apply (erule bspec)

proof/access-control/Retype_AC.thy

@@ -497,7 +497,7 @@ lemma retype_region_ext_pas_refined:
   "\<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in> set xs. is_subject aag x)\<rbrace>
    retype_region_ext xs ty
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (subst and_assoc[symmetric])
   apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed')
   apply (simp add: retype_region_ext_def, wp)

proof/crefine/AARCH64/Fastpath_Equiv.thy

@@ -755,8 +755,7 @@ lemma fastpath_callKernel_SysCall_corres:
                               apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                              apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                             apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
-                            apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
-                             apply simp
+                            apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
                             apply ((wp assert_inv threadSet_pred_tcb_at_state
                                        cteInsert_obj_at'_not_queued
                                     | wps)+)[1]
@@ -1494,7 +1493,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
      (invs' and ct_in_state' ((=) Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and cnode_caps_gsCNodes')
      (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)"
-  including no_pre
+  including classic_wp_pre
   supply if_cong[cong] option.case_cong[cong]
   supply if_split[split del]
   supply user_getreg_inv[wp] (* FIXME *)

proof/crefine/ARM/Fastpath_Equiv.thy

@@ -661,8 +661,7 @@ lemma fastpath_callKernel_SysCall_corres:
                               apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                              apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                             apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
-                            apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
-                             apply simp
+                            apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
                             apply ((wp assert_inv threadSet_pred_tcb_at_state
                                        cteInsert_obj_at'_not_queued
                                     | wps)+)[1]
@@ -1364,7 +1363,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
      (invs' and ct_in_state' ((=) Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and cnode_caps_gsCNodes')
      (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)"
-  including no_pre
+  including classic_wp_pre
   supply if_cong[cong] option.case_cong[cong]
   supply if_split[split del]
   supply user_getreg_inv[wp] (* FIXME *)

proof/crefine/ARM_HYP/Fastpath_Equiv.thy

@@ -661,8 +661,7 @@ lemma fastpath_callKernel_SysCall_corres:
                               apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                              apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
                             apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1]
-                            apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
-                             apply simp
+                            apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t])
                             apply ((wp assert_inv threadSet_pred_tcb_at_state
                                        cteInsert_obj_at'_not_queued
                                     | wps)+)[1]
@@ -1367,7 +1366,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
      (invs' and ct_in_state' ((=) Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and cnode_caps_gsCNodes')
      (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)"
-  including no_pre
+  including classic_wp_pre
   supply if_cong[cong] option.case_cong[cong]
   supply if_split[split del]
   supply user_getreg_inv[wp] (* FIXME *)

proof/crefine/Move_C.thy

@@ -988,7 +988,7 @@ lemma empty_fail_getIdleThread [simp,intro!]:
 
 lemma setTCB_cur:
   "\<lbrace>cur_tcb'\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_. cur_tcb'\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (wp cur_tcb_lift)
   apply (simp add: setObject_def split_def updateObject_default_def)
   apply wp

proof/drefine/CNode_DR.thy

@@ -244,8 +244,7 @@ lemma insert_cap_sibling_corres:
            cte_wp_at_caps_of_state has_parent_cte_at is_physical_def
            dest!:is_untyped_cap_eqD)
          apply fastforce
-        apply (wp get_cap_wp set_cap_idle | simp)+
-   apply clarsimp
+        apply (wpsimp wp: get_cap_wp set_cap_idle)+
    apply (clarsimp simp: not_idle_thread_def)
    apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state
      transform_cap_def)

proof/drefine/Finalise_DR.thy

@@ -486,7 +486,7 @@ lemma dcorres_deleting_irq_handler:
   apply (rule corres_split[OF dcorres_get_irq_slot])
     apply (simp, rule delete_cap_simple_corres,simp)
     apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"])
-    including no_pre
+    including classic_wp_pre
     apply (wpsimp simp:get_irq_slot_def)+
     apply (rule irq_node_image_not_idle)
     apply (simp add:invs_def valid_state_def)+
@@ -2503,6 +2503,7 @@ lemma dcorres_delete_asid:
               apply (wp | clarsimp)+
          apply simp
         apply (wp | clarsimp)+
+       apply (rule hoare_pre, wp, clarsimp)
       apply (rule hoare_pre, wp)
       apply simp
      apply (wp | clarsimp)+

proof/drefine/Ipc_DR.thy

@@ -702,7 +702,7 @@ lemma tcb_sched_action_tcb_at_not_idle[wp]:
 
 lemma valid_idle_cancel_all_ipc:
   "\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.cancel_all_ipc word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (simp add:cancel_all_ipc_def)
   apply (wp|wpc|simp)+
       apply (rename_tac queue list)
@@ -757,7 +757,7 @@ lemma valid_idle_cancel_all_ipc:
 
 lemma valid_idle_cancel_all_signals:
   "\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.cancel_all_signals word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (simp add:cancel_all_signals_def)
   apply (wp|wpc|simp)+
      apply (rename_tac list)
@@ -1285,10 +1285,9 @@ next
         apply (rule dcorres_set_extra_badge,simp)
        apply (rule Cons.hyps, rule refl, rule refl, simp)
       apply wp[1]
-     apply (simp add: store_word_offs_def set_extra_badge_def
-     not_idle_thread_def ipc_frame_wp_at_def
-     split_def)
-     apply (wp evalMonad_lookup_ipc_buffer_wp)
+     apply (simp add: store_word_offs_def set_extra_badge_def not_idle_thread_def
+                      ipc_frame_wp_at_def split_def)
+     apply (wpsimp wp: evalMonad_lookup_ipc_buffer_wp)
          apply (erule cte_wp_at_weakenE)
          apply (simp add:ipc_buffer_wp_at_def)+
         apply wp

proof/drefine/Schedule_DR.thy

@@ -81,7 +81,7 @@ lemma change_current_domain_and_switch_to_idle_thread_dcorres:
                     Schedule_D.switch_to_thread None
                  od)
                 switch_to_idle_thread"
-  including no_pre
+  including classic_wp_pre
   apply (clarsimp simp: Schedule_D.switch_to_thread_def switch_to_idle_thread_def)
   apply (rule dcorres_symb_exec_r)
     apply (rule corres_guard_imp)

proof/infoflow/ADT_IF.thy

@@ -1665,7 +1665,7 @@ lemma schedule_if_globals_equiv_scheduler[wp]:
    \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>"
   apply (simp add: schedule_if_def)
   apply wp
-    apply (wp globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv)
+    apply (wpsimp wp: globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv)
     apply (simp add: invs_arch_state invs_valid_idle)
    apply (wp | simp)+
   done
@@ -2618,8 +2618,7 @@ lemma perform_invocation_irq_state_inv:
                       invoke_tcb_irq_state_inv invoke_cnode_irq_state_inv[simplified validE_R_def]
                    | clarsimp | simp add: invoke_domain_def)+\<close>)?)
    apply wp
-    apply (wp irq_state_inv_triv' invoke_irq_control_irq_masks)
-    apply clarsimp
+    apply (wpsimp wp: irq_state_inv_triv' invoke_irq_control_irq_masks)
     apply assumption
    apply auto[1]
   apply wp

proof/infoflow/ARM/ArchRetype_IF.thy

@@ -278,7 +278,7 @@ lemma copy_global_mappings_globals_equiv:
   "\<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace>
    copy_global_mappings x
    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
-  unfolding copy_global_mappings_def including no_pre
+  unfolding copy_global_mappings_def including classic_wp_pre
   apply simp
   apply wp
    apply (rule_tac Q="\<lambda>_. globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and>

proof/infoflow/ARM/ArchScheduler_IF.thy

@@ -186,7 +186,7 @@ lemma globals_equiv_scheduler_inv'[Scheduler_IF_assms]:
 
 lemma clearExMonitor_globals_equiv_scheduler[wp]:
   "do_machine_op clearExMonitor \<lbrace>globals_equiv_scheduler sta\<rbrace>"
-  unfolding clearExMonitor_def including no_pre
+  unfolding clearExMonitor_def including classic_wp_pre
   apply (wp dmo_no_mem_globals_equiv_scheduler)
    apply simp
   apply (simp add: simpler_modify_def valid_def)

proof/infoflow/Decode_IF.thy

@@ -110,8 +110,8 @@ lemma slot_cap_long_running_delete_reads_respects_f:
          apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+
       apply (wp is_final_cap_reads_respects[where st=st])[1]
      apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+
-    apply (wp reads_respects_f[OF get_cap_rev, where Q="\<top>" and st=st], blast)
-   apply (wp get_cap_wp | simp)+
+    apply (wpsimp wp: reads_respects_f[OF get_cap_rev, where Q="\<top>" and st=st])
+   apply (wp get_cap_wp)
   apply (fastforce intro!: cte_wp_valid_cap aag_has_auth_to_obj_refs_of_owned_cap simp: is_zombie_def
                      dest: silc_inv_not_subject)
   done
@@ -227,14 +227,14 @@ lemma decode_tcb_invocation_reads_respects_f:
   apply (simp add: unlessE_def[symmetric] unlessE_whenE split del: if_split
              cong: gen_invocation_labels.case_cong)
   apply (rule equiv_valid_guard_imp)
-   apply (wp (once) requiv_cur_thread_eq range_check_ev respects_f[OF derive_cap_rev]
-                    derive_cap_inv slot_cap_long_running_delete_reads_respects_f[where st=st]
-                    respects_f[OF check_valid_ipc_buffer_rev] check_valid_ipc_buffer_inv
-                    respects_f[OF decode_set_priority_rev] respects_f[OF decode_set_mcpriority_rev]
-                    respects_f[OF decode_set_sched_params_rev]
-                    respects_f[OF get_simple_ko_reads_respects]
-                    respects_f[OF get_bound_notification_reads_respects']
-          | wp (once) whenE_throwError_wp
+   apply (wp requiv_cur_thread_eq range_check_ev respects_f[OF derive_cap_rev]
+             derive_cap_inv slot_cap_long_running_delete_reads_respects_f[where st=st]
+             respects_f[OF check_valid_ipc_buffer_rev] check_valid_ipc_buffer_inv
+             respects_f[OF decode_set_priority_rev] respects_f[OF decode_set_mcpriority_rev]
+             respects_f[OF decode_set_sched_params_rev]
+             respects_f[OF get_simple_ko_reads_respects]
+             respects_f[OF get_bound_notification_reads_respects']
+             whenE_throwError_wp
           | wp (once) hoare_drop_imps
           | wpc
           | simp add: if_apply_def2 split del: if_split add: o_def split_def)+

proof/infoflow/FinalCaps.thy

@@ -1441,7 +1441,7 @@ lemma finalise_cap_ret_is_subject:
    finalise_cap cap is_final
    \<lbrace>\<lambda>rv _ :: det_state. case (fst rv) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv))
                                                        | _ \<Rightarrow> True\<rbrace>"
-  including no_pre
+  including classic_wp_pre
   apply (case_tac cap, simp_all add: is_zombie_def)
              apply (wp | simp add: comp_def | rule impI | rule conjI)+
   apply (fastforce simp: valid_def dest: arch_finalise_cap_ret)
@@ -2400,7 +2400,7 @@ lemma transfer_caps_silc_inv:
   apply (simp add: transfer_caps_def)
   apply (wpc | wp)+
     apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm)
-    apply (wp transfer_caps_loop_pres_dest cap_insert_silc_inv)
+    apply (wpsimp wp: transfer_caps_loop_pres_dest cap_insert_silc_inv)
      apply (fastforce simp: silc_inv_def)
     apply (wp get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+
   apply (fastforce elim: cte_wp_at_weakenE)

proof/infoflow/Finalise_IF.thy

@@ -570,10 +570,10 @@ lemma tcb_sched_action_reads_respects:
    apply (force intro: domtcbs simp: get_etcb_def)
   apply (simp add: equiv_valid_def2 ethread_get_def)
   apply (rule equiv_valid_rv_bind)
-    apply (wp equiv_valid_rv_trivial', simp)
+    apply (wpsimp wp: equiv_valid_rv_trivial')
    apply (rule equiv_valid_2_bind)
       prefer 2
-      apply (wp equiv_valid_rv_trivial, simp)
+      apply (wpsimp wp: equiv_valid_rv_trivial)
      apply (rule equiv_valid_2_bind)
         apply (rule_tac P=\<top> and P'=\<top> and L="{pasObjectAbs aag t}" and L'="{pasObjectAbs aag t}"
                      in ev2_invisible[OF domains_distinct])

proof/infoflow/Ipc_IF.thy

@@ -601,6 +601,9 @@ lemma send_signal_reads_respects:
                         set_thread_state_runnable_equiv_but_for_labels get_simple_ko_wp
                         gts_wp update_waiting_ntfn_equiv_but_for_labels
                         blocked_cancel_ipc_nosts_equiv_but_for_labels
+            \<comment> \<open>FIXME: The following line is working around the fact that wp (once) doesn't invoke
+                      wp_pre. If that is changed then it could be removed.\<close>
+            | wp_pre0
             | wpc
             | wps)+
     apply (elim conjE)
@@ -1717,7 +1720,7 @@ lemma copy_mrs_globals_equiv:
   "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
    copy_mrs sender sbuf receiver rbuf n
    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
-  unfolding copy_mrs_def including no_pre
+  unfolding copy_mrs_def including classic_wp_pre
   apply (wp | wpc)+
     apply (rule_tac Q="\<lambda>_. globals_equiv s" in hoare_strengthen_post)
      apply (wp mapM_wp' | wpc)+

proof/infoflow/Noninterference.thy

@@ -381,8 +381,7 @@ lemma kernel_entry_if_globals_equiv_scheduler:
                                and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
    kernel_entry_if e tc
    \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>"
-  apply (wp globals_equiv_scheduler_inv' kernel_entry_if_globals_equiv)
-   apply (clarsimp)
+  apply (wpsimp wp: globals_equiv_scheduler_inv' kernel_entry_if_globals_equiv)
    apply assumption
   apply clarsimp
   done
@@ -2090,10 +2089,10 @@ lemma tcb_sched_action_reads_respects_g':
    apply (force intro: domtcbs simp: get_etcb_def)
   apply (simp add: equiv_valid_def2 ethread_get_def)
   apply (rule equiv_valid_rv_bind)
-    apply (wp equiv_valid_rv_trivial', simp)
+    apply (wpsimp wp: equiv_valid_rv_trivial')
    apply (rule equiv_valid_2_bind)
       prefer 2
-      apply (wp equiv_valid_rv_trivial, simp)
+      apply (wpsimp wp: equiv_valid_rv_trivial)
      apply (rule equiv_valid_2_bind)
         apply (rule_tac P="\<top>" and P'="\<top>" and L="{pasObjectAbs aag thread}" and
                                               L'="{pasObjectAbs aag thread}" in ev2_invisible')