wp: update the proofs for the new wp/wpc/wpsimp

proof/bisim/Syscall_S.thy

@@ -293,8 +293,7 @@ lemma send_fault_ipc_bisim:
     apply (wp not_empty_lc)
       apply (rule_tac P = "separate_cap xa" in not_empty_gen_asm)
       apply (erule separate_capE, simp_all)[1]
-        apply wp+
-  apply simp
+        apply wpsimp+
   done
 
 lemma handle_fault_bisim:
@@ -690,7 +689,7 @@ lemma handle_event_bisim:
 
       apply (wp separate_state_pres)+
        apply (rule hoare_pre, wps, wp+, simp)
-      apply wp+
+      apply wpsimp+
    apply (simp add: cur_tcb_def)
 
    apply (rule bisim_refl, simp)

proof/capDL-api/Retype_DP.thy

@@ -999,7 +999,6 @@ lemma invoke_untyped_preempt:
         apply (rule mapME_x_inv_wp[where P = P and E = "\<lambda>r. P" for P])
         apply (wp alternative_wp)
          apply simp
-         apply (rule hoare_pre)
          apply (wp hoare_vcg_ex_lift)
           apply (rule hoare_post_imp[OF _ set_cap_wp])
           apply sep_solve
@@ -1008,7 +1007,6 @@ lemma invoke_untyped_preempt:
         apply sep_solve
        apply simp
       apply simp
-     apply sep_solve
     apply (wp select_wp)+
   apply clarsimp
   apply (frule opt_cap_sep_imp)

proof/capDL-api/TCB_DP.thy

@@ -246,9 +246,8 @@ lemma tcb_update_cspace_root_wp:
   apply (wp hoare_whenE_wp tcb_update_thread_slot_wp[sep_wand_side_wpE] get_cap_rv )
    apply (wp get_cap_rv)
   apply (intro hoare_validE_conj)
-    apply (wp tcb_empty_thread_slot_wpE[sep_wand_wpE])
-    apply (clarsimp simp: sep_conj_assoc)
-    apply (sep_cancel+)
+    apply (wpsimp wp: tcb_empty_thread_slot_wpE[sep_wand_wpE] simp: sep_conj_assoc)
+    apply (sep_cancel+, simp)
     apply (wp tcb_empty_thread_slot_wpE[sep_wand_wpE])+
    apply (clarsimp, sep_cancel+)
   apply (rule validE_allI)
@@ -1151,6 +1150,7 @@ shows
         apply (rule_tac P="is_tcb_cap c" in hoare_gen_asmEx )
         apply (rule split_error_validE)
          apply (clarsimp simp: decode_tcb_invocation_simps)
+         including no_pre
          apply (wp)
          apply (clarsimp simp: comp_def)
          apply (wp+)[2]

proof/crefine/Fastpath_C.thy

@@ -984,7 +984,8 @@ lemma armv_contextSwitch_HWASID_fp_rewrite:
   apply (rule monadic_rewrite_imp)
    apply (rule monadic_rewrite_gets_l)
    apply (rule monadic_rewrite_symb_exec_l)
-      apply (wp | simp)+
+      including no_pre
+      apply (wpsimp)+
      apply (simp add: empty_fail_findPDForASID empty_fail_catch)
     apply (rule monadic_rewrite_assert monadic_rewrite_gets_l)+
     apply (rule_tac P="asidMap asid \<noteq> None \<and> fst (the (asidMap asid)) = the (pde_stored_asid v)"

proof/crefine/Ipc_C.thy

@@ -825,7 +825,7 @@ lemma handleFaultReply':
                   fromIntegral_simp1 fromIntegral_simp2 shiftL_word)
     apply (clarsimp simp: mapM_def sequence_def bind_assoc asUser_bind_distrib
                           asUser_return submonad_asUser.fn_stateAssert bit_def)
-   apply wp+
+   apply wpsimp+
   done
 
 end
@@ -2348,7 +2348,7 @@ lemma loadCapTransfer_ctReceiveDepth:
      apply simp
      apply (simp only: word_bits_len_of[symmetric])
      apply (subst unat_lt2p, simp) 
-    apply wp+
+    apply wpsimp+
   done
 
 (* FIXME: move *)
@@ -3482,8 +3482,7 @@ proof -
            apply (rule_tac Q'="\<lambda>rv. no_0_obj' and real_cte_at' rv"
                       in hoare_post_imp_R, wp lsft_real_cte)
            apply (clarsimp simp: cte_wp_at_ctes_of)
-          apply (wp | simp)+
-         apply (rule hoare_pre, (wp | simp)+)
+          apply (wpsimp)+
         apply (clarsimp simp: guard_is_UNIV_def
                        elim!: inl_inrE)
        apply (rule hoare_pre, (wp mapM_wp' | simp)+)
@@ -3519,9 +3518,7 @@ lemma lookupExtraCaps_excaps_in_mem[wp]:
   apply (simp add: excaps_in_mem_def lookupExtraCaps_def lookupCapAndSlot_def
                    split_def)
   apply (wp mapME_set)
-      apply (wp getSlotCap_slotcap_in_mem | simp)+
-    apply (rule hoare_pre, wp, simp)
-   apply (simp add:hoare_TrueI)+
+      apply (wpsimp wp: getSlotCap_slotcap_in_mem)+
   done
 
 lemma doNormalTransfer_ccorres [corres]:

proof/crefine/Retype_C.thy

@@ -8094,6 +8094,7 @@ shows  "ccorres dc xfdc
          apply (rule is_aligned_shiftl_self)
         apply (simp)
        apply (simp add: range_cover_one[OF _  range_cover.sz(2) range_cover.sz(1)])
+       including no_pre
        apply (wp insertNewCap_invs' insertNewCap_valid_pspace' insertNewCap_caps_overlap_reserved'
                  insertNewCap_pspace_no_overlap' insertNewCap_caps_no_overlap'' insertNewCap_descendants_range_in'
                  insertNewCap_untypedRange hoare_vcg_all_lift insertNewCap_cte_at static_imp_wp)

proof/crefine/Syscall_C.thy

@@ -404,8 +404,6 @@ lemma lookupExtraCaps_excaps_in_mem[wp]:
                    split_def)
   apply (wp mapME_set)
       apply (wp getSlotCap_slotcap_in_mem | simp)+
-    apply (rule hoare_pre, wp, simp)
-   apply (simp add:hoare_TrueI)+
   done
 
 lemma getCurThread_ccorres:

proof/crefine/Tcb_C.thy

@@ -464,7 +464,7 @@ lemma setPriority_ccorres:
       apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits)
      apply (wp threadSet_tcbDomain_triv)
      apply simp
-    apply (simp add: guard_is_UNIV_def)
+    apply (simp add: guard_is_UNIV_def)+
    apply (simp add: inQ_def pred_conj_def conj_comms)
    apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues)
     apply (rule hoare_strengthen_post,

proof/drefine/Arch_DR.thy

@@ -1006,6 +1006,7 @@ next
          apply (wp valid_validE[OF whenE_inv] |  clarsimp split: option.splits | safe)+
       apply (rule validE_cases_valid, rule hoare_pre, wp)
 
+      including no_pre
       apply (wp resolve_vaddr_inv |  clarsimp simp: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
       in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
         apply (wp valid_validE[OF whenE_inv] |  clarsimp split: option.splits | safe)+

proof/drefine/Finalise_DR.thy

@@ -453,7 +453,8 @@ lemma finalise_cancel_ipc:
              apply (rule corres_split[OF _ dcorres_revoke_cap_unnecessary])
                unfolding K_bind_def
                apply (rule set_thread_state_corres)
-              apply (wp set_ntfn_valid_objs | clarsimp simp:not_idle_thread_def)+
+              including no_pre
+              apply (wpsimp wp: set_ntfn_valid_objs simp:not_idle_thread_def)+
            apply (clarsimp simp:valid_def fail_def return_def split:Structures_A.ntfn.splits)+
            apply (clarsimp simp:invs_def)
            apply (frule(1) valid_tcb_if_valid_state)
@@ -487,7 +488,8 @@ 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"])
-    apply (wp |clarsimp simp:get_irq_slot_def)+
+    including no_pre
+    apply (wpsimp simp:get_irq_slot_def)+
     apply (rule irq_node_image_not_idle)
     apply (simp add:invs_def valid_state_def)+
 done

proof/drefine/Schedule_DR.thy

@@ -658,7 +658,7 @@ lemma activate_thread_corres:
            apply (rule dcorres_symb_exec_r)
              apply (rule set_thread_state_corres[unfolded tcb_pending_op_slot_def])
             apply simp
-            apply (wp dcorres_to_wp[OF as_user_setNextPC_corres,simplified])+
+            apply (wpsimp wp: dcorres_to_wp[OF as_user_setNextPC_corres,simplified])+
        apply (simp add:invs_mdb pred_tcb_at_def obj_at_def invs_valid_idle
          generates_pending_def not_idle_thread_def)
       apply (clarsimp simp:infer_tcb_pending_op_def arch_activate_idle_thread_def

proof/drefine/Tcb_DR.thy

@@ -614,7 +614,6 @@ lemma invoke_tcb_corres_read_regs:
            apply (rule dcorres_idempotent_as_user)
            apply (rule hoare_mapM_idempotent)
            apply wp+
-        apply simp
        apply (rule suspend_corres, simp)
       apply wp
     apply simp

proof/infoflow/ADT_IF.thy

@@ -2046,7 +2046,7 @@ lemma kernel_entry_if_was_not_Interrupt:
    apply wp
      apply simp
      apply(rule handle_event_was_not_Interrupt[simplified validE_E_def validE_def])
-    apply wp+
+    apply wpsimp+
   done
 
 lemma ct_idle_lift:

proof/infoflow/Arch_IF.thy

@@ -113,8 +113,7 @@ lemma get_object_revrv:
       apply(simp)
      apply(rule assert_ev2)
      apply(simp)
-    apply(wp)+
-  apply fastforce
+    apply(wpsimp)+
   done
 
 lemma get_object_revrv':
@@ -131,8 +130,7 @@ lemma get_object_revrv':
       apply(simp)
      apply(rule assert_ev2)
      apply(simp add: equiv_for_def)
-    apply(wp)+
-  apply fastforce
+    apply(wpsimp)+
   done
 
 lemma get_asid_pool_revrv':
@@ -1020,7 +1018,7 @@ lemma equiv_valid_get_assert:
   apply(rule_tac W="\<top>\<top>" in equiv_valid_rv_bind)
     apply(rule equiv_valid_rv_guard_imp)
      apply(rule equiv_valid_rv_trivial)
-     apply wp+
+     apply wpsimp+
    apply(rule_tac R'="\<top>\<top>" in equiv_valid_2_bind)
       apply(simp add: equiv_valid_def2)
      apply(rule assert_ev2)
@@ -1101,7 +1099,7 @@ lemma arm_asid_table_update_reads_respects:
   apply(simp add: equiv_valid_def2)
   apply(rule_tac W="\<top>\<top>" and Q="\<lambda> rv s. is_subject aag pool_ptr \<and> rv = arm_asid_table (arch_state s)" in equiv_valid_rv_bind)
     apply(rule equiv_valid_rv_guard_imp[OF equiv_valid_rv_trivial])
-     apply wp+
+     apply wpsimp+
    apply(rule modify_ev2)
    apply clarsimp
    apply (drule(1) is_subject_kheap_eq[rotated])

proof/infoflow/FinalCaps.thy

@@ -548,8 +548,7 @@ lemma set_cap_slots_holding_overlapping_caps_other:
     set_cap cap slot
    \<lbrace> \<lambda> rv s. x \<in> slots_holding_overlapping_caps capa s \<rbrace>"
   unfolding set_cap_def
-  apply (wp set_object_wp get_object_wp | wpc | simp add: split_def)+
-  apply clarsimp
+  apply (wpsimp wp: set_object_wp get_object_wp)+
   apply(case_tac "Structures_A.obj_refs capa = {} \<and> cap_irqs capa = {}")
    apply(clarsimp simp: slots_holding_overlapping_caps_def)
   apply(subgoal_tac "fst x \<noteq> fst slot")
@@ -561,7 +560,8 @@ lemma set_cap_slots_holding_overlapping_caps_other:
         apply(rule upd_other_cte_wp_at)
          apply(simp add: cte_wp_at_def)
         apply assumption
-       apply(auto intro: set_cap_slots_holding_overlapping_caps_helper)
+       apply((drule set_cap_slots_holding_overlapping_caps_helper[where slot=slot], simp+)+)[5]
+  apply clarsimp
   done
 
 
@@ -569,15 +569,12 @@ lemma set_cap_cte_wp_at_triv:
   "\<lbrace>\<top>\<rbrace> set_cap cap slot 
    \<lbrace>\<lambda>_. cte_wp_at (op = cap) slot\<rbrace>"
   unfolding set_cap_def
-  apply (wp set_object_wp get_object_wp | wpc | simp add: split_def)+
-  apply clarsimp
+  apply (wpsimp wp: set_object_wp get_object_wp)
   apply(intro impI conjI allI)
        apply(rule cte_wp_at_cteI)
           apply fastforce
          apply clarsimp
-         apply(erule (1) set_cap_well_formed_cnode_helper)
-        apply simp
-       apply(rule refl)
+         apply(drule set_cap_well_formed_cnode_helper[where slot=slot], simp+)
       apply(fastforce intro: cte_wp_at_tcbI simp: tcb_cap_cases_def)+
   done
 

proof/infoflow/Finalise_IF.thy

@@ -466,7 +466,7 @@ lemma get_endpoint_revrv:
   unfolding get_endpoint_def
   apply(rule_tac Q="\<lambda> rv. ko_at rv epptr and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag))" in equiv_valid_rv_bind)
     apply(rule equiv_valid_rv_guard_imp[OF equiv_valid_rv_trivial])
-     apply wp+
+     apply wpsimp+
    apply(case_tac "\<exists> ep. rv = Endpoint ep")
     apply(case_tac "\<exists> ep. rv' = Endpoint ep")
      apply (clarsimp split: kernel_object.splits)

proof/infoflow/Ipc_IF.thy

@@ -934,6 +934,7 @@ lemma get_extra_cptrs_rev:
   apply(case_tac buffer, simp_all add: return_ev_pre)
   apply (wp mapM_ev equiv_valid_guard_imp[OF load_word_offs_rev]
        | erule (2) aag_has_auth_to_read_cptrs)+
+  apply wpsimp+
   done
 
 lemma lookup_extra_caps_rev:

proof/infoflow/Syscall_IF.thy

@@ -701,9 +701,7 @@ lemma handle_recv_reads_respects_f:
              apply(rule reads_ep[where auth=Receive])
               apply(fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)+
         apply(wp reads_respects_f[OF handle_fault_reads_respects,where st=st])
-        apply (wp get_ntfn_wp get_cap_wp | wpc)+
-       apply simp
-       apply(rule hoare_pre)
+        apply (wpsimp wp: get_ntfn_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>                                     

proof/refine/ARM/ArchAcc_R.thy

@@ -1417,9 +1417,7 @@ lemma find_pd_for_asid_corres'':
                 split: option.split)
       apply (clarsimp simp:checkPDAt_def stateAssert_def liftE_bindE bind_assoc)
       apply (rule corres_noop)
-       apply (simp add:validE_def returnOk_def | wp)+
-      apply (rule no_fail_pre, wp)
-      apply clarsimp
+       apply (wpsimp simp:validE_def returnOk_def)+
       apply (erule page_directory_at_state_relation)
         apply simp+
      apply (wp getObject_inv loadObject_default_inv | simp)+

proof/refine/ARM/Detype_R.thy

@@ -5086,7 +5086,7 @@ proof -
               apply simp
              apply (subst monad_commute_simple[symmetric])
               apply (rule commute_commute[OF curDomain_commute])
-              apply wp+
+              apply (wpsimp+)[2]
              apply (rule_tac Q = "\<lambda>r s. r = (ksCurDomain s) \<and>
                pspace_aligned' s \<and>
                pspace_distinct' s \<and>

proof/refine/ARM/Finalise_R.thy

@@ -3505,8 +3505,6 @@ lemma (in delete_one) deleting_irq_corres:
           apply (auto simp: cte_wp_at_caps_of_state is_cap_simps can_fast_finalise_def)[1]
          apply (clarsimp simp: cte_wp_at_ctes_of)
         apply (wp getCTE_wp' | simp add: getSlotCap_def)+
-      apply (rule no_fail_pre, wp)
-      apply (clarsimp simp: cte_wp_at_ctes_of)
      apply (wp | simp add: get_irq_slot_def getIRQSlot_def
                            locateSlot_conv getInterruptState_def)+
    apply (clarsimp simp: ex_cte_cap_wp_to_def interrupt_cap_null_or_ntfn)

proof/refine/ARM/IpcCancel_R.thy

@@ -1014,9 +1014,8 @@ lemma (in delete_one_conc_pre) cancelIPC_tcb_at_runnable':
   apply (case_tac "t'=t")
    apply (rule_tac B="\<lambda>st. st_tcb_at' runnable' t and K (runnable' st)"
             in hoare_seq_ext)
-    apply(case_tac x; wpsimp)
-   apply (wp sts_pred_tcb_neq' | simp | wpc)+
-           apply (clarsimp)
+    apply(case_tac x; simp)
+   apply (wpsimp wp: sts_pred_tcb_neq')+
            apply (rule_tac Q="\<lambda>rv. ?PRE" in hoare_post_imp, fastforce)
            apply (wp cteDeleteOne_tcb_at_runnable'
                     threadSet_pred_tcb_no_state

proof/refine/ARM/Ipc_R.thy

@@ -1502,7 +1502,7 @@ lemma getMessageInfo_msgExtraCaps[wp]:
      apply (simp add: word_bits_def msgExtraCapBits_def)
     apply (rule and_mask_less'[unfolded mask_2pm1])
     apply (simp add: msgExtraCapBits_def)
-   apply wp+
+   apply wpsimp+
   done
 
 lemma lcs_corres:  

proof/refine/ARM/Orphanage.thy

@@ -1065,7 +1065,7 @@ lemma sendIPC_valid_queues' [wp]:
    sendIPC blocking call badge canGrant thread epptr
    \<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>"
   unfolding sendIPC_def
-  apply (wp hoare_drop_imps | wpc | clarsimp)+
+  apply (wp hoare_drop_imps | wpsimp)+
           apply (wp_once sts_st_tcb', clarsimp)
          apply (wp)+
   apply (rule_tac Q="\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr

proof/refine/ARM/PageTableDuplicates.thy

@@ -1824,13 +1824,9 @@ lemma archFinaliseCap_valid_duplicates'[wp]:
   apply (case_tac arch_cap,simp_all add:ARM_H.finaliseCap_def)
       apply (rule hoare_pre)
        apply (wp|wpc|simp)+
-    apply (rule hoare_pre)
-     apply (wp|wpc|simp)+
     apply (clarsimp simp:valid_cap'_def)
    apply (rule hoare_pre)
     apply (wp|wpc|simp)+
-  apply (rule hoare_pre)
-   apply (wp|wpc|simp)+
   done
 
 lemma finaliseCap_valid_duplicates'[wp]:

proof/refine/ARM/Refine.thy

@@ -610,7 +610,7 @@ lemma kernel_corres:
           apply simp
          apply (wp doMachineOp_getActiveIRQ_IRQ_active handle_event_valid_sched | simp)+
        apply (rule_tac Q="\<lambda>_. \<top>" and E="\<lambda>_. invs'" in hoare_post_impErr)
-         apply wp+
+         apply wpsimp+
        apply (simp add: invs'_def valid_state'_def)
       apply (rule corres_split [OF _ schedule_corres])
         apply (rule activate_corres)

proof/refine/ARM/TcbAcc_R.thy

@@ -389,10 +389,7 @@ proof -
            apply (rule y)
           apply (rule e)
          apply (rule corres_noop [where P=\<top> and P'=\<top>])
-          apply simp
-         apply (rule no_fail_pre, wp)[1]
-        apply wp+
-      apply simp
+          apply wpsimp+
       apply (erule pspace_relation_tcb_at[rotated])
       apply clarsimp
      apply simp

proof/refine/ARM/VSpace_R.thy

@@ -2577,8 +2577,6 @@ lemma perform_page_table_corres:
      apply (rule hoare_lift_Pf2[where f=caps_of_state])
       apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
                 mapM_x_wp' | simp split del: if_split)+
-     apply (rule hoare_pre)
-      apply (wp mapM_x_wp' | simp split del: if_split)+
    apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state
                          is_arch_diminished_def
                          cap_master_cap_simps

sys-init/InitCSpace_SI.thy

@@ -1265,8 +1265,9 @@ lemma init_cnode_slots_move_sep:
                   si_objects \<and>* object_empty_slots_initialised spec t obj_id" and
                xs="slots_of_list spec obj_id",
                simplified sep_conj_assoc], clarsimp+)
-     apply (wp init_cnode_slot_move_sep, simp+)
+     apply (wpsimp wp: init_cnode_slot_move_sep)
      apply fastforce
+    apply simp
    apply (subst sep.prod.distrib)+
    apply (clarsimp simp: sep_conj_assoc fun_eq_iff)
    apply sep_solve