lib+proof+autocorres: update for monad changes

This mostly involved renamed variable names and one lemma being removed
from the simp set.

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

lib/Monad_Lists.thy

@@ -619,7 +619,7 @@ next
   show ?case
     apply (simp add: mapME_Cons)
     apply (wp)
-     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P x s" in hoare_strengthen_postE_R)
+     apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P rv s" in hoare_strengthen_postE_R)
       apply (wp Cons.hyps minvp)
      apply simp
     apply (fold validE_R_def)

proof/access-control/ARM/ArchArch_AC.thy

@@ -830,7 +830,6 @@ lemma decode_arch_invocation_authorised:
           | wpc
           | simp add: authorised_asid_control_inv_def authorised_page_inv_def
                       authorised_page_directory_inv_def
-                 del: hoareE_R_TrueI
                  split del: if_split)+
   apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def
                         neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs)

proof/access-control/ARM/ArchTcb_AC.thy

@@ -37,7 +37,7 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
    apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
                  in hoare_gen_asm)
    apply (simp only: split_def)
-   apply (((simp add: conj_comms del: hoareE_R_TrueI,
+   apply (((simp add: conj_comms,
            strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
           | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
           | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R
@@ -78,7 +78,6 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
                cap_delete_pas_refined'[THEN valid_validE_E] thread_set_cte_wp_at_trivial
           | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
                       emptyable_def a_type_def partial_inv_def
-                 del: hoareE_R_TrueI
           | wpc
           | strengthen invs_mdb use_no_cap_to_obj_asid_strg
                        tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]

proof/access-control/Ipc_AC.thy

@@ -2351,7 +2351,7 @@ lemma send_ipc_integrity_autarch:
           apply (wp set_thread_state_integrity_autarch thread_get_wp'
                     do_ipc_transfer_integrity_autarch
                     hoare_vcg_all_lift hoare_drop_imps set_endpoint_respects
-                 | wpc | simp add: get_thread_state_def split del: if_split del: hoareE_R_TrueI)+
+                 | wpc | simp add: get_thread_state_def split del: if_split)+
    apply (fastforce simp: a_type_def obj_at_def is_ep elim: send_ipc_valid_ep_helper)
   \<comment> \<open>we don't own head of queue\<close>
   apply clarsimp

proof/access-control/RISCV64/ArchTcb_AC.thy

@@ -37,7 +37,7 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
    apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
                  in hoare_gen_asm)
    apply (simp only: split_def)
-  apply (((simp add: conj_comms del: hoareE_R_TrueI,
+  apply (((simp add: conj_comms,
           strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
          | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
          | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R
@@ -78,7 +78,6 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
               cap_delete_pas_refined'[THEN valid_validE_E] thread_set_cte_wp_at_trivial
          | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
                      emptyable_def a_type_def partial_inv_def
-                del: hoareE_R_TrueI
          | wpc
          | strengthen invs_mdb use_no_cap_to_obj_asid_strg
                       tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]

proof/access-control/Syscall_AC.thy

@@ -135,7 +135,7 @@ lemma decode_invocation_authorised:
              decode_arch_invocation_authorised
           | strengthen cnode_eq_strg
           | wpc | simp add: comp_def authorised_invocation_def decode_invocation_def
-                       split del: if_split del: hoareE_R_TrueI
+                       split del: if_split
           | wp (once) hoare_FalseE_R)+
   apply (clarsimp simp: aag_has_Control_iff_owns split_def aag_cap_auth_def)
   apply (cases cap, simp_all)
@@ -279,8 +279,7 @@ lemma handle_invocation_pas_refined:
        | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
        | wpc
        | rule hoare_drop_imps
-       | simp add: if_apply_def2 conj_comms split del: if_split
-              del: hoareE_R_TrueI)+,
+       | simp add: if_apply_def2 conj_comms split del: if_split)+,
       (wp lookup_extra_caps_auth lookup_extra_caps_authorised decode_invocation_authorised
           lookup_cap_and_slot_authorised lookup_cap_and_slot_cur_auth as_user_pas_refined
           lookup_cap_and_slot_valid_fault3 hoare_vcg_const_imp_lift_R

proof/bisim/Syscall_S.thy

@@ -323,12 +323,12 @@ lemma bisim_liftME_same:
   shows "bisim (f \<oplus> (=)) P P' (liftME g m) (liftME g m')"
   unfolding liftME_def
   apply (rule bisim_guard_imp)
-  apply (rule bisim_splitE [OF bs])
-   apply simp
-   apply (rule bisim_returnOk)
-   apply simp
-   apply wp
-  apply simp+
+    apply (rule bisim_splitE [OF bs])
+      apply simp
+      apply (rule bisim_returnOk)
+      apply simp
+     apply wp+
+   apply simp+
   done
 
 lemma bisim_split_if:
@@ -596,7 +596,7 @@ lemma handle_recv_bisim:
                    apply (simp split del: if_split)
                    apply (rule bisim_refl [where P = \<top> and P' = \<top>])
                    apply (case_tac rc, simp_all)[1]
-                   apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del:  hoareE_R_TrueI)+
+                   apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def)+
                    apply (rule handle_fault_bisim)
                    apply (wp get_simple_ko_wp | wpc | simp)+
                    apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_strengthen_postE_R)

proof/capDL-api/IRQ_DP.thy

@@ -341,7 +341,7 @@ shows "\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb  \<and>* (root_t
         apply (rule_tac P = "c=irq_cap" in hoare_gen_asmEx, simp)
         apply (simp add: unify decode_invocation_def)
         apply (wp)
-         apply (rule_tac P = "x = (IrqHandlerSetEndpointIntent)" in hoare_gen_asmE, simp)
+         apply (rule_tac P = "rv = (IrqHandlerSetEndpointIntent)" in hoare_gen_asmE, simp)
          apply (wp decode_invocation_irq_endpoint_rv'[where endpoint_cap=endpoint_cap and endpoint_ptr = endpoint_ptr and xs = "[]"])
         apply (unfold throw_opt_def get_irq_handler_intent_def, simp)
         apply (rule returnOk_wp)

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)
+  apply (wpsimp simp: o_def nonep_invocation_def wp: wp_post_tauts)
   apply (auto simp: ep_related_cap_def)
   done
 

proof/capDL-api/Retype_DP.thy

@@ -252,7 +252,7 @@ lemma reset_untyped_cap_wp:
   apply (rule hoare_pre)
    apply (wp whenE_wp)
       apply (rule_tac P = "\<exists>fr. cap = UntypedCap dev obj_range fr
-          \<and> (\<forall>fr\<in> set x. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range)" in hoare_gen_asmE)
+          \<and> (\<forall>fr\<in> set rv. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range)" in hoare_gen_asmE)
       apply clarsimp
       apply (wp whenE_wp mapME_x_wp)
       apply (rule ballI)
@@ -261,7 +261,7 @@ lemma reset_untyped_cap_wp:
        apply simp
        apply (rule hoare_post_imp[OF _ set_cap_wp])
        apply clarsimp
-       apply (rule_tac x = xa in exI)
+       apply (rule_tac x = x in exI)
         apply ((rule conjI, fastforce)+, sep_solve)
       apply clarsimp
       apply sep_solve

proof/crefine/AARCH64/Refine_C.thy

@@ -192,7 +192,7 @@ lemma handleVMFaultEvent_ccorres:
        apply (clarsimp simp: return_def)
       apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_valid_objs_strengthen invs_pspace_aligned' invs_pspace_distinct')+
-     apply (case_tac x, clarsimp, wp)
+     apply (case_tac rv, clarsimp, wp)
      apply (clarsimp, wp, simp)
     apply wp
    apply (simp add: guard_is_UNIV_def)

proof/crefine/AARCH64/SyscallArgs_C.thy

@@ -656,7 +656,7 @@ lemma getMRs_tcbContext:
   apply (thin_tac "thread = t" for t)
   apply (clarsimp simp add: getMRs_def)
   apply (wp|wpc)+
-    apply (rule_tac P="n < length x" in hoare_gen_asm)
+    apply (rule_tac P="n < length rv" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' hoare_weak_lift_imp)+
     apply simp

proof/crefine/ARM/Refine_C.thy

@@ -171,7 +171,7 @@ lemma handleVMFaultEvent_ccorres:
        apply (clarsimp simp: return_def)
       apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_valid_objs_strengthen invs_pspace_aligned' invs_pspace_distinct')+
-     apply (case_tac x, clarsimp, wp)
+     apply (case_tac rv, clarsimp, wp)
      apply (clarsimp, wp, simp)
     apply wp
    apply (simp add: guard_is_UNIV_def)

proof/crefine/ARM/SyscallArgs_C.thy

@@ -637,7 +637,7 @@ lemma getMRs_tcbContext:
   apply (thin_tac "thread = t" for t)
   apply (clarsimp simp add: getMRs_def)
   apply (wp|wpc)+
-    apply (rule_tac P="n < length x" in hoare_gen_asm)
+    apply (rule_tac P="n < length rv" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' hoare_weak_lift_imp)+
     apply simp

proof/crefine/ARM_HYP/Refine_C.thy

@@ -165,7 +165,7 @@ lemma handleVMFaultEvent_ccorres:
        apply (clarsimp simp: return_def)
       apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_valid_objs_strengthen invs_pspace_aligned' invs_pspace_distinct')+
-     apply (case_tac x, clarsimp, wp)
+     apply (case_tac rv, clarsimp, wp)
      apply (clarsimp, wp, simp)
     apply wp
    apply (simp add: guard_is_UNIV_def)

proof/crefine/ARM_HYP/SyscallArgs_C.thy

@@ -660,7 +660,7 @@ lemma getMRs_tcbContext:
   apply (thin_tac "thread = t" for t)
   apply (clarsimp simp add: getMRs_def)
   apply (wp|wpc)+
-    apply (rule_tac P="n < length x" in hoare_gen_asm)
+    apply (rule_tac P="n < length rv" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' hoare_weak_lift_imp)+
     apply simp

proof/crefine/RISCV64/Finalise_C.thy

@@ -1527,7 +1527,7 @@ lemma unmapPageTable_ccorres:
              apply simp
             apply wp
            apply (simp add: guard_is_UNIV_def)
-          apply (simp add: guard_is_UNIV_def)
+          apply wpsimp
          apply (simp add: guard_is_UNIV_def)
         apply vcg
        apply (vcg spec=modifies)

proof/crefine/RISCV64/Refine_C.thy

@@ -162,7 +162,7 @@ lemma handleVMFaultEvent_ccorres:
        apply (clarsimp simp: return_def)
       apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_valid_objs_strengthen invs_pspace_aligned' invs_pspace_distinct')+
-     apply (case_tac x, clarsimp, wp)
+     apply (case_tac rv, clarsimp, wp)
      apply (clarsimp, wp, simp)
     apply wp
    apply (simp add: guard_is_UNIV_def)

proof/crefine/RISCV64/SyscallArgs_C.thy

@@ -656,7 +656,7 @@ lemma getMRs_tcbContext:
   apply (thin_tac "thread = t" for t)
   apply (clarsimp simp add: getMRs_def)
   apply (wp|wpc)+
-    apply (rule_tac P="n < length x" in hoare_gen_asm)
+    apply (rule_tac P="n < length rv" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' hoare_weak_lift_imp)+
     apply simp

proof/crefine/X64/Refine_C.thy

@@ -162,7 +162,7 @@ lemma handleVMFaultEvent_ccorres:
        apply (clarsimp simp: return_def)
       apply (wp schedule_sch_act_wf schedule_invs'
              | strengthen invs_valid_objs_strengthen invs_pspace_aligned' invs_pspace_distinct')+
-     apply (case_tac x, clarsimp, wp)
+     apply (case_tac rv, clarsimp, wp)
      apply (clarsimp, wp, simp)
     apply wp
    apply (simp add: guard_is_UNIV_def)

proof/crefine/X64/SyscallArgs_C.thy

@@ -662,7 +662,7 @@ lemma getMRs_tcbContext:
   apply (thin_tac "thread = t" for t)
   apply (clarsimp simp add: getMRs_def)
   apply (wp|wpc)+
-    apply (rule_tac P="n < length x" in hoare_gen_asm)
+    apply (rule_tac P="n < length rv" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' hoare_weak_lift_imp)+
     apply simp

proof/crefine/X64/VSpace_C.thy

@@ -1829,7 +1829,7 @@ lemma unmapPage_ccorres:
         apply ccorres_rewrite
         apply (clarsimp simp: liftE_liftM)
         apply (ctac add: invalidateTranslationSingleASID_ccorres)
-       apply clarsimp
+       apply wpsimp
       apply clarsimp
       apply (clarsimp simp: guard_is_UNIV_def conj_comms tcb_cnode_index_defs)
      apply (simp add: throwError_def)

proof/drefine/CNode_DR.thy

@@ -2648,11 +2648,7 @@ lemma decode_cnode_corres:
                         apply simp
                        apply (rule dcorres_returnOk)
                        apply (simp add:translate_cnode_invocation_def)
-                      apply (wp get_cap_wp whenE_wp|clarsimp)+
-         apply (rule hoare_strengthen_postE_R[OF validE_validE_R])
-         apply (rule hoareE_TrueI[where P = \<top>])
-          apply fastforce
-         apply (wp hoare_drop_imp|simp)+
+                      apply (wp get_cap_wp | simp)+
          apply (rule_tac Q'="\<lambda>r. real_cte_at src_slota and valid_objs and
                                 real_cte_at dest_slota and valid_idle and
                                      not_idle_thread (fst src_slota) and

proof/drefine/Finalise_DR.thy

@@ -210,13 +210,14 @@ lemma delete_cap_one_shrink_descendants:
      apply (clarsimp simp add:empty_slot_def)
      apply (wp dxo_wp_weak)
          apply simp
-        apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
-          \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
-          in hoare_weaken_pre)
+        apply (rename_tac slot_p cdt')
+        apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = cdt' \<and> cdt pres = cdt' \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
+                               \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
+                     in hoare_weaken_pre)
          apply (rule_tac Q ="\<lambda>r s. Q r s \<and>  (mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post)
           apply (rule hoare_vcg_conj_lift)
            apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p])
-          apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s ) xa" in hoare_weaken_pre)
+          apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s ) cdt'" in hoare_weaken_pre)
            apply (case_tac slot)
            apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def mdb_cte_at_def)
           apply (assumption)
@@ -245,7 +246,7 @@ lemma delete_cap_one_shrink_descendants:
   apply (drule descendants_not_null_cap)
    apply simp
   apply (clarsimp simp:cte_wp_at_def)
-done
+  done
 
 lemma invs_emptyable_descendants:
   "\<lbrakk>invs s;CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk>
@@ -1402,10 +1403,10 @@ lemma remain_pt_pd_relation:
   apply (subgoal_tac "ptr\<noteq> y")
    apply (simp add: store_pte_def)
    apply wp
-     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
+     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable rv)) (ptr && ~~ mask pt_bits)
                 and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_weaken_pre)
       apply (clarsimp simp: set_pt_def)
-      apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits)
+      apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable rv)) (ptr && ~~ mask pt_bits)
                    and  pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_weaken_pre)
        apply (clarsimp simp: valid_def set_object_def get_object_def in_monad)
        apply (drule_tac x= y in bspec,simp)
@@ -1426,10 +1427,10 @@ lemma remain_pd_section_relation:
        \<lbrace>\<lambda>r s. pd_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>"
   apply (simp add: store_pde_def)
   apply wp
-    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
+    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory rv)) (ptr && ~~ mask pd_bits)
                   and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_weaken_pre)
      apply (clarsimp simp: set_pd_def)
-     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
+     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory rv)) (ptr && ~~ mask pd_bits)
                 and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_weaken_pre)
       apply (clarsimp simp: valid_def set_object_def get_object_def in_monad)
       apply (clarsimp simp: pd_section_relation_def dest!: ucast_inj_mask | rule conjI)+
@@ -1448,10 +1449,10 @@ lemma remain_pd_super_section_relation:
        \<lbrace>\<lambda>r s. pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>"
   apply (simp add: store_pde_def)
   apply wp
-    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
+    apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory rv)) (ptr && ~~ mask pd_bits)
                and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_weaken_pre)
      apply (clarsimp simp: set_pd_def)
-     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits)
+     apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory rv)) (ptr && ~~ mask pd_bits)
                and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_weaken_pre)
       apply (clarsimp simp: valid_def set_object_def get_object_def in_monad)
       apply (clarsimp simp: pd_super_section_relation_def dest!: ucast_inj_mask | rule conjI)+

proof/drefine/Ipc_DR.thy

@@ -72,7 +72,7 @@ lemma handle_reply_cur_thread_idle_thread:
                apply ((wps|wp cap_delete_one_it)+)[1]
               apply (wp do_ipc_transfer_cur_thread_idle_thread dxo_wp_weak)+
                     apply (clarsimp simp: trans_state_def)
-                   apply (case_tac xf)
+                   apply (case_tac rvf)
                    apply (simp | wp set_thread_state_cur_thread_idle_thread
                                     thread_set_cur_thread_idle_thread)+
                  apply ((wps | wp)+)[1]
@@ -1333,8 +1333,8 @@ next
              apply (rule cap_insert_weak_cte_wp_at_not_null)
              apply clarsimp+
            apply (wp cap_insert_idle valid_irq_node_typ hoare_vcg_ball_lift cap_insert_cte_wp_at)+
-       apply (simp add: if_apply_def2)
-       apply wp
+        apply (wpsimp simp: if_apply_def2)
+       apply (wpsimp simp: if_apply_def2)
       apply (simp add: if_apply_def2)
       apply (rule validE_R_validE)
       apply (simp add:conj_comms ball_conj_distrib split del:if_split)
@@ -1593,7 +1593,7 @@ lemma transfer_caps_loop_None:
 lemma get_rs_length [wp]:
   "\<lbrace>\<top>\<rbrace> get_receive_slots rcv buffer \<lbrace>\<lambda>slots s. length slots \<le> 1\<rbrace>"
   apply (cases buffer)
-   apply (simp del: hoareE_R_TrueI|wp)+
+   apply (simp|wp)+
   done
 
 lemma transfer_caps_dcorres: