From 7ad3ef3b3ec41f6998fab752740ad70d3a607612 Mon Sep 17 00:00:00 2001 From: Miki Tanaka Date: Tue, 14 Mar 2017 03:37:32 +1100 Subject: [PATCH] wp: update the proofs for the new wp/wpc/wpsimp --- proof/bisim/Syscall_S.thy | 5 ++--- proof/capDL-api/Retype_DP.thy | 2 -- proof/capDL-api/TCB_DP.thy | 6 +++--- proof/crefine/Fastpath_C.thy | 3 ++- proof/crefine/Ipc_C.thy | 11 ++++------- proof/crefine/Retype_C.thy | 1 + proof/crefine/Syscall_C.thy | 2 -- proof/crefine/Tcb_C.thy | 2 +- proof/drefine/Arch_DR.thy | 1 + proof/drefine/Finalise_DR.thy | 6 ++++-- proof/drefine/Schedule_DR.thy | 2 +- proof/drefine/Tcb_DR.thy | 1 - proof/infoflow/ADT_IF.thy | 2 +- proof/infoflow/Arch_IF.thy | 10 ++++------ proof/infoflow/FinalCaps.thy | 13 +++++-------- proof/infoflow/Finalise_IF.thy | 2 +- proof/infoflow/Ipc_IF.thy | 1 + proof/infoflow/Syscall_IF.thy | 4 +--- proof/refine/ARM/ArchAcc_R.thy | 4 +--- proof/refine/ARM/Detype_R.thy | 2 +- proof/refine/ARM/Finalise_R.thy | 2 -- proof/refine/ARM/IpcCancel_R.thy | 5 ++--- proof/refine/ARM/Ipc_R.thy | 2 +- proof/refine/ARM/Orphanage.thy | 2 +- proof/refine/ARM/PageTableDuplicates.thy | 4 ---- proof/refine/ARM/Refine.thy | 2 +- proof/refine/ARM/TcbAcc_R.thy | 5 +---- proof/refine/ARM/VSpace_R.thy | 2 -- sys-init/InitCSpace_SI.thy | 3 ++- 29 files changed, 42 insertions(+), 65 deletions(-) diff --git a/proof/bisim/Syscall_S.thy b/proof/bisim/Syscall_S.thy index d0ed55712..64cea78b9 100644 --- a/proof/bisim/Syscall_S.thy +++ b/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) diff --git a/proof/capDL-api/Retype_DP.thy b/proof/capDL-api/Retype_DP.thy index a02832005..75e355fa2 100644 --- a/proof/capDL-api/Retype_DP.thy +++ b/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 = "\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) diff --git a/proof/capDL-api/TCB_DP.thy b/proof/capDL-api/TCB_DP.thy index 58d4e152c..82d3ddcd7 100644 --- a/proof/capDL-api/TCB_DP.thy +++ b/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] diff --git a/proof/crefine/Fastpath_C.thy b/proof/crefine/Fastpath_C.thy index 0e69610c8..d5567b9eb 100644 --- a/proof/crefine/Fastpath_C.thy +++ b/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 \ None \ fst (the (asidMap asid)) = the (pde_stored_asid v)" diff --git a/proof/crefine/Ipc_C.thy b/proof/crefine/Ipc_C.thy index ad70f874b..2dddaa8c5 100644 --- a/proof/crefine/Ipc_C.thy +++ b/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'="\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]: diff --git a/proof/crefine/Retype_C.thy b/proof/crefine/Retype_C.thy index e806d58c4..a1d95e5fa 100644 --- a/proof/crefine/Retype_C.thy +++ b/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) diff --git a/proof/crefine/Syscall_C.thy b/proof/crefine/Syscall_C.thy index 6580facdb..9c5d3639a 100644 --- a/proof/crefine/Syscall_C.thy +++ b/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: diff --git a/proof/crefine/Tcb_C.thy b/proof/crefine/Tcb_C.thy index d964dc896..63d70125a 100644 --- a/proof/crefine/Tcb_C.thy +++ b/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, diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index b3b280118..aa11d938f 100644 --- a/proof/drefine/Arch_DR.thy +++ b/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)+ diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index 405c8db96..248630f6f 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/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 diff --git a/proof/drefine/Schedule_DR.thy b/proof/drefine/Schedule_DR.thy index 35b7b309b..d071be14b 100644 --- a/proof/drefine/Schedule_DR.thy +++ b/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 diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy index 4a47d0704..b8d905bc6 100644 --- a/proof/drefine/Tcb_DR.thy +++ b/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 diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index ed003c7b8..67f989df9 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/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: diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy index e37a7fe87..108177365 100644 --- a/proof/infoflow/Arch_IF.thy +++ b/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="\\" 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'="\\" 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="\\" and Q="\ rv s. is_subject aag pool_ptr \ 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]) diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index bc83159bf..58f16bf3c 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -548,8 +548,7 @@ lemma set_cap_slots_holding_overlapping_caps_other: set_cap cap slot \ \ rv s. x \ slots_holding_overlapping_caps capa s \" 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 = {} \ cap_irqs capa = {}") apply(clarsimp simp: slots_holding_overlapping_caps_def) apply(subgoal_tac "fst x \ 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: "\\\ set_cap cap slot \\_. cte_wp_at (op = cap) slot\" 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 diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 8267fb6fc..23b38dee2 100644 --- a/proof/infoflow/Finalise_IF.thy +++ b/proof/infoflow/Finalise_IF.thy @@ -466,7 +466,7 @@ lemma get_endpoint_revrv: unfolding get_endpoint_def apply(rule_tac Q="\ rv. ko_at rv epptr and pas_refined aag and valid_objs and sym_refs \ state_refs_of and (K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \ 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 "\ ep. rv = Endpoint ep") apply(case_tac "\ ep. rv' = Endpoint ep") apply (clarsimp split: kernel_object.splits) diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy index 62a5bbd0b..e179c350e 100644 --- a/proof/infoflow/Ipc_IF.thy +++ b/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: diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index 8340e9690..f0701d8e4 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/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="\r s. silc_inv aag st s \ einvs s \ pas_refined aag s \ tcb_at rv s \ pas_cur_domain aag s \ diff --git a/proof/refine/ARM/ArchAcc_R.thy b/proof/refine/ARM/ArchAcc_R.thy index 1f2d7f28c..a1249b7d7 100644 --- a/proof/refine/ARM/ArchAcc_R.thy +++ b/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)+ diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy index 7bca93983..ad732ab1e 100644 --- a/proof/refine/ARM/Detype_R.thy +++ b/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 = "\r s. r = (ksCurDomain s) \ pspace_aligned' s \ pspace_distinct' s \ diff --git a/proof/refine/ARM/Finalise_R.thy b/proof/refine/ARM/Finalise_R.thy index 0e122740c..e1d24ccf7 100644 --- a/proof/refine/ARM/Finalise_R.thy +++ b/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) diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index 3dc834006..89e348106 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/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="\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="\rv. ?PRE" in hoare_post_imp, fastforce) apply (wp cteDeleteOne_tcb_at_runnable' threadSet_pred_tcb_no_state diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 8f6155962..8ca5eeaae 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/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: diff --git a/proof/refine/ARM/Orphanage.thy b/proof/refine/ARM/Orphanage.thy index 6731571a4..53b71756c 100644 --- a/proof/refine/ARM/Orphanage.thy +++ b/proof/refine/ARM/Orphanage.thy @@ -1065,7 +1065,7 @@ lemma sendIPC_valid_queues' [wp]: sendIPC blocking call badge canGrant thread epptr \ \rv s. valid_queues' s \" 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="\rv. valid_queues' and valid_objs' and ko_at' rv epptr diff --git a/proof/refine/ARM/PageTableDuplicates.thy b/proof/refine/ARM/PageTableDuplicates.thy index 163155116..e2cc4b0e5 100644 --- a/proof/refine/ARM/PageTableDuplicates.thy +++ b/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]: diff --git a/proof/refine/ARM/Refine.thy b/proof/refine/ARM/Refine.thy index a7d3b6e28..fd2878787 100644 --- a/proof/refine/ARM/Refine.thy +++ b/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="\_. \" and E="\_. 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) diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index a3ec2c09e..12cefb286 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -389,10 +389,7 @@ proof - apply (rule y) apply (rule e) apply (rule corres_noop [where P=\ and P'=\]) - 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 diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index f7028e1e3..10d9cbc90 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/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 diff --git a/sys-init/InitCSpace_SI.thy b/sys-init/InitCSpace_SI.thy index 9340b8bd7..950c2c956 100644 --- a/sys-init/InitCSpace_SI.thy +++ b/sys-init/InitCSpace_SI.thy @@ -1265,8 +1265,9 @@ lemma init_cnode_slots_move_sep: si_objects \* 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