Yet more rules for Lib

lib/Corres_UL.thy

@@ -1176,6 +1176,18 @@ lemma corres_move_asm:
 
 lemmas corres_cross_over_guard = corres_move_asm[rotated]
 
+lemma corres_cross_add_guard:
+  "\<lbrakk>\<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q' s';
+    corres_underlying sr nf nf' r P (P' and Q') f g\<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by (fastforce simp: corres_underlying_def)
+
+lemma corres_cross_add_abs_guard:
+  "\<lbrakk>\<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s;
+    corres_underlying sr nf nf' r (P and Q)  P' f g\<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by (fastforce simp: corres_underlying_def)
+
 lemma corres_either_alternate:
   "\<lbrakk> corres_underlying sr nf nf' r P Pa' a c; corres_underlying sr nf nf' r P Pb' b c \<rbrakk>
    \<Longrightarrow> corres_underlying sr nf nf' r P (Pa' or Pb') (a \<sqinter> b) c"
@@ -1256,6 +1268,18 @@ lemma corres_stateAssert_implied2:
   apply simp
   done
 
+lemma corres_stateAssert_add_assertion:
+  "\<lbrakk> corres_underlying sr nf nf' r P (Q and Q') f (g ());
+     \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; Q s' \<rbrakk> \<Longrightarrow> Q' s' \<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P Q f (stateAssert Q' [] >>= g)"
+  apply (clarsimp simp: bind_assoc stateAssert_def)
+  apply (rule corres_symb_exec_r [OF _ get_sp])
+    apply (rule corres_assume_pre)
+    apply (rule corres_assert_assume)
+     apply (erule corres_guard_imp, clarsimp+)
+   apply (wp | rule no_fail_pre)+
+  done
+
 lemma corres_add_noop_lhs:
   "corres_underlying sr nf nf' r P P' (return () >>= (\<lambda>_. f)) g
       \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"

lib/HaskellLemmaBucket.thy

@@ -127,10 +127,14 @@ lemma empty_fail_stateAssert[intro!, simp]:
   "empty_fail (stateAssert P l)"
   unfolding stateAssert_def by simp
 
-lemma haskell_assert_wp:
+lemma haskell_assert_wp[wp]:
   "\<lbrace>\<lambda>s. Q \<longrightarrow> P s\<rbrace> haskell_assert Q xs \<lbrace>\<lambda>_. P\<rbrace>"
   by simp wp
 
+lemma haskell_assert_inv:
+  "\<lbrace>P\<rbrace> haskell_assert Q l \<lbrace>\<lambda>_. P\<rbrace>"
+  by wpsimp
+
 lemma init_append_last:
   "xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs"
   apply (induct xs rule: rev_induct)

lib/Heap_List.thy

@@ -383,6 +383,14 @@ lemma not_head_prev_not_None:
   using sym_heap_prev_None_is_start heap_path_head
   by fastforce
 
+lemma heap_ls_neighbour_in_set:
+  "\<lbrakk>heap_ls hp st xs; sym_heap hp hp'; st \<noteq> None \<longrightarrow> hp' (the st) = None; p \<in> set xs\<rbrakk>
+   \<Longrightarrow> \<forall>nbr. (hp p = Some nbr \<longrightarrow> nbr \<in> set xs) \<and> (hp' p = Some nbr \<longrightarrow> nbr \<in> set xs)"
+  apply (intro conjI impI allI)
+   apply (erule (2) heap_ls_next_in_list)
+  apply (fastforce dest: heap_ls_prev_cases[where np=p] sym_heapD2)
+  done
+
 (* more on heap_path *)
 
 lemma heap_ls_next_takeWhile_append:

lib/LemmaBucket.thy

@@ -510,4 +510,12 @@ lemma cases_conj_strg: "A \<and> B \<longrightarrow> (P \<and> A) \<or> (\<not>
 
 lemma and_not_not_or_imp: "(~ A & ~ B | C) = ((A | B) \<longrightarrow> C)" by blast
 
+lemma filter_hd_equals_tl:
+  "\<lbrakk>distinct q; q \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (hd q)) q = tl q"
+  apply (induct q rule: length_induct)
+  apply (rename_tac list)
+  apply (case_tac list; simp)
+  apply (fastforce simp: filter_id_conv)
+  done
+
 end

lib/Lib.thy

@@ -2533,8 +2533,18 @@ next
     by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
 qed
 
-lemma rsubst:
-  "\<lbrakk> P s; s = t \<rbrakk> \<Longrightarrow> P t"
+lemmas rsubst = back_subst[where a=s and b=t for s t]
+
+lemma rsubst2:
+  "\<lbrakk>P a b; a = s; b = t\<rbrakk> \<Longrightarrow> P s t"
+  by simp
+
+lemma rsubst3:
+  "\<lbrakk>P a b c ; a = s; b = t; c = u\<rbrakk> \<Longrightarrow> P s t u"
+  by simp
+
+lemma rsubst4:
+  "\<lbrakk>P a b c d; a = s; b = t; c = u; d = v\<rbrakk> \<Longrightarrow> P s t u v"
   by simp
 
 lemma ex_impE: "((\<exists>x. P x) \<longrightarrow> Q) \<Longrightarrow> P x \<Longrightarrow> Q"

lib/Monads/reader_option/Reader_Option_VCG.thy

@@ -114,6 +114,11 @@ lemma ovalid_if_split:
   "\<lbrakk> P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not>P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot> \<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>"
   by simp
 
+lemma reader_case_option_wp[wp]:
+  "\<lbrakk>\<And>x. \<lblot>P x\<rblot> m x \<lblot>Q\<rblot>; \<lblot>P'\<rblot> m' \<lblot>Q\<rblot>\<rbrakk>
+   \<Longrightarrow> \<lblot>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (\<forall>y. x = Some y \<longrightarrow> P y s)\<rblot> case_option m' m x \<lblot>Q\<rblot>"
+  by (cases x; simp)
+
 lemma ovalid_case_prod[wp]:
   assumes "(\<And>x y. ovalid (P x y) (B x y) Q)"
   shows "ovalid (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q"
@@ -129,7 +134,7 @@ lemma owhile_ovalid[wp]:
    apply auto
   done
 
-lemma assert_opt_ovalid:
+lemma oassert_opt_ovalid[wp]:
   "\<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> oassert_opt x \<lblot>Q\<rblot>"
   unfolding oassert_opt_def
   by (case_tac x; wpsimp)

proof/crefine/AARCH64/Fastpath_C.thy

@@ -585,7 +585,7 @@ lemma getASIDPoolEntry_wp:
    getASIDPoolEntry asid
    \<lbrace>\<lambda>rv s. P rv s \<rbrace>"
   unfolding getASIDPoolEntry_def asid_has_entry_def getPoolPtr_def
-  apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift getASID_wp simp: comp_def)
+  apply (wpsimp wp: haskell_assert_inv getASID_wp)
   apply normalise_obj_at'
   apply (rename_tac pool)
   apply (case_tac "pool (asid AND mask asid_low_bits)"; simp)

proof/refine/AARCH64/Detype_R.thy

@@ -3006,25 +3006,14 @@ lemma curDomain_commute:
 crunch inv[wp]: curDomain P
 
 lemma placeNewObject_tcb_at':
-  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
-          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
-          atLeastAtMost_iff
-  shows
-  "\<lbrace>pspace_aligned' and pspace_distinct'
-    and pspace_no_overlap' ptr (objBits (makeObject::tcb))
-    and  K(is_aligned ptr  (objBits (makeObject::tcb)))
-   \<rbrace> placeNewObject ptr (makeObject::tcb) 0
-       \<lbrace>\<lambda>rv s. tcb_at' ptr s \<rbrace>"
-  apply (simp add:placeNewObject_def placeNewObject'_def split_def alignError_def)
+  "\<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits (makeObject::tcb))
+    and K (is_aligned ptr  (objBits (makeObject::tcb)))\<rbrace>
+   placeNewObject ptr (makeObject::tcb) 0
+   \<lbrace>\<lambda>_ s. tcb_at' ptr s \<rbrace>"
+  apply (simp add: placeNewObject_def placeNewObject'_def split_def alignError_def)
   apply wpsimp
-  apply (clarsimp simp: obj_at'_def lookupAround2_None1 objBits_simps
-                        lookupAround2_char1 field_simps projectKO_opt_tcb return_def ps_clear_def
-                  simp flip: is_aligned_mask)
-  apply (drule (1) pspace_no_overlap_disjoint')
-  apply (clarsimp intro!: set_eqI;
-         drule_tac m = "ksPSpace s" in domI,
-         erule in_emptyE,
-         fastforce elim!: in_emptyE simp:objBits_simps mask_def add_diff_eq)
+  apply (clarsimp simp: obj_at'_def objBits_simps ps_clear_def)
+  apply (fastforce intro!: set_eqI dest: pspace_no_overlap_disjoint' simp: add_mask_fold)
   done
 
 lemma monad_commute_if_weak_r:

proof/refine/AARCH64/Syscall_R.thy

@@ -1332,6 +1332,7 @@ lemma hinv_invs'[wp]:
   done
 
 crunch typ_at'[wp]: handleFault "\<lambda>s. P (typ_at' T p s)"
+  (wp: crunch_wps)
 
 lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at']
 
@@ -1761,14 +1762,13 @@ lemma hr_ct_active'[wp]:
   "\<lbrace>invs' and ct_active'\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active'\<rbrace>"
   apply (simp add: handleReply_def getSlotCap_def getCurThread_def
                    getThreadCallerSlot_def locateSlot_conv)
-  apply (rule hoare_seq_ext)
-   apply (rule ct_in_state'_decomp)
-    apply ((wp hoare_drop_imps | wpc | simp)+)[1]
-   apply (subst haskell_assert_def)
-   apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active
-        | wpc | simp)+
+  apply (rule hoare_seq_ext, rename_tac cur_thread)
+   apply (rule_tac t=cur_thread in ct_in_state'_decomp)
+    apply (wpsimp wp: getCTE_wp)
+    apply (fastforce simp: cte_wp_at_ctes_of)
+   apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+
   apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def
-                  dest: ctes_of_valid')
+                   dest: ctes_of_valid')
   done
 
 lemma handleCall_corres:
@@ -2086,7 +2086,7 @@ crunches handleVMFault
 
 crunches handleHypervisorFault
   for ksit[wp]: "\<lambda>s. P (ksIdleThread s)"
-  (wp: undefined_valid simp: isFpuEnable_def)
+  (wp: undefined_valid haskell_assert_inv simp: isFpuEnable_def)
 
 lemma hh_invs'[wp]:
   "\<lbrace>invs' and sch_act_not p and (\<lambda>s. \<forall>a b. p \<notin> set (ksReadyQueues s (a, b))) and

proof/refine/AARCH64/VSpace_R.thy

@@ -1335,6 +1335,7 @@ lemma vcpuDisable_invs'[wp]:
              getSCTLR_def get_gic_vcpu_ctrl_hcr_def dsb_def vgicUpdate_def vcpuUpdate_def
              vcpuSaveReg_def enableFpuEL01_def
   by (wpsimp wp: dmo'_gets_wp setVCPU_vgic_invs' setVCPU_regs_invs' dmo_maskInterrupt_True
+                 hoare_drop_imps
              simp: doMachineOp_bind empty_fail_cond)
 
 lemma vcpuInvalidateActive_invs'[wp]:
@@ -1398,7 +1399,7 @@ crunches loadVMID
 lemma updateASIDPoolEntry_valid_arch_state'[wp]:
   "updateASIDPoolEntry f asid \<lbrace>valid_arch_state'\<rbrace>"
   unfolding updateASIDPoolEntry_def
-  by (wpsimp wp: getObject_inv simp: loadObject_default_def)
+  by (wpsimp wp: getObject_inv hoare_drop_imps simp: loadObject_default_def)
 
 lemma invalidateVMIDEntry_valid_arch_state'[wp]:
   "invalidateVMIDEntry vmid \<lbrace>valid_arch_state'\<rbrace>"

proof/refine/AARCH64/orphanage/Orphanage.thy

@@ -1275,15 +1275,15 @@ lemma setupCallerCap_no_orphans [wp]:
    setupCallerCap sender receiver gr
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding setupCallerCap_def
-  by (wpsimp wp: setThreadState_not_active_no_orphans
+  by (wpsimp wp: setThreadState_not_active_no_orphans hoare_drop_imps
              simp: is_active_thread_state_def isRestart_def isRunning_def)
 
 lemma setupCallerCap_almost_no_orphans [wp]:
   "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and> valid_queues' s \<rbrace>
    setupCallerCap sender receiver gr
    \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>"
   unfolding setupCallerCap_def
-  by (wpsimp wp: setThreadState_not_active_almost_no_orphans
+  by (wpsimp wp: setThreadState_not_active_almost_no_orphans hoare_drop_imps
              simp: is_active_thread_state_def isRestart_def isRunning_def)
 
 crunches doIPCTransfer, setMRs
@@ -1332,7 +1332,7 @@ lemma sendIPC_valid_queues' [wp]:
    \<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>"
   unfolding sendIPC_def
   apply (wpsimp wp: hoare_drop_imps)
-        apply (wpsimp | wp (once) sts_st_tcb')+
+        apply (wpsimp | wp (once) sts_st_tcb' hoare_drop_imps)+
   apply (rule_tac Q="\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr
                           and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp)
    apply (clarsimp)
@@ -1586,7 +1586,7 @@ lemma cteDeleteOne_no_orphans [wp]:
    cteDeleteOne slot
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding cteDeleteOne_def
-  by (wpsimp wp: assert_inv isFinalCapability_inv weak_if_wp)
+  by (wpsimp wp: assert_inv haskell_assert_inv isFinalCapability_inv weak_if_wp)
 
 crunch valid_objs' [wp]: getThreadReplySlot "valid_objs'"
 
@@ -1752,7 +1752,7 @@ lemma deletingIRQHandler_no_orphans [wp]:
    deletingIRQHandler irq
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding deletingIRQHandler_def
-  by wp auto
+  by (wpsimp wp: hoare_drop_imps) auto
 
 lemma finaliseCap_no_orphans [wp]:
   "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> valid_cap' cap s \<rbrace>
@@ -2184,7 +2184,7 @@ lemma deleteCallerCap_no_orphans [wp]:
    deleteCallerCap receiver
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding deleteCallerCap_def
-  by wpsimp auto
+  by (wpsimp wp: hoare_drop_imps) auto
 
 lemma remove_neg_strg:
   "(A \<and> B) \<longrightarrow> ((x \<longrightarrow> A) \<and> (\<not> x \<longrightarrow> B))"

proof/refine/ARM/PageTableDuplicates.thy

@@ -2169,14 +2169,15 @@ crunch valid_duplicates'[wp]:
 
 crunch valid_duplicates'[wp]:
   receiveIPC "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
-(wp: getNotification_wp gbn_wp')
+  (wp: getNotification_wp gbn_wp' crunch_wps)
 
 crunch valid_duplicates'[wp]:
   deleteCallerCap "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
   (wp: crunch_wps)
 
 crunch valid_duplicates'[wp]:
   handleReply "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
+  (wp: crunch_wps)
 
 crunch valid_duplicates'[wp]:
   handleYield "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"

proof/refine/ARM/Syscall_R.thy

@@ -1362,6 +1362,7 @@ lemma hinv_invs'[wp]:
   done
 
 crunch typ_at'[wp]: handleFault "\<lambda>s. P (typ_at' T p s)"
+  (wp: crunch_wps)
 
 lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at']
 
@@ -1793,14 +1794,13 @@ lemma hr_ct_active'[wp]:
   "\<lbrace>invs' and ct_active'\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active'\<rbrace>"
   apply (simp add: handleReply_def getSlotCap_def getCurThread_def
                    getThreadCallerSlot_def locateSlot_conv)
-  apply (rule hoare_seq_ext)
-   apply (rule_tac t=thread in ct_in_state'_decomp)
-    apply ((wp hoare_drop_imps | wpc | simp)+)[1]
-   apply (subst haskell_assert_def)
-   apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active
-        | wpc | simp)+
+  apply (rule hoare_seq_ext, rename_tac cur_thread)
+   apply (rule_tac t=cur_thread in ct_in_state'_decomp)
+    apply (wpsimp wp: getCTE_wp)
+    apply (fastforce simp: cte_wp_at_ctes_of)
+   apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+
   apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def
-                  dest: ctes_of_valid')
+                   dest: ctes_of_valid')
   done
 
 lemma handleCall_corres:

proof/refine/ARM/orphanage/Orphanage.thy

@@ -1255,7 +1255,7 @@ lemma setupCallerCap_no_orphans [wp]:
    setupCallerCap sender receiver gr
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding setupCallerCap_def
-  apply (wp setThreadState_not_active_no_orphans
+  apply (wp setThreadState_not_active_no_orphans hoare_drop_imps
          | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+
   done
 
@@ -1264,7 +1264,7 @@ lemma setupCallerCap_almost_no_orphans [wp]:
    setupCallerCap sender receiver gr
    \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>"
   unfolding setupCallerCap_def
-  apply (wp setThreadState_not_active_almost_no_orphans
+  apply (wp setThreadState_not_active_almost_no_orphans hoare_drop_imps
          | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+
   done
 
@@ -1311,7 +1311,7 @@ lemma sendIPC_valid_queues' [wp]:
    \<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>"
   unfolding sendIPC_def
   apply (wpsimp wp: hoare_drop_imps)
-        apply (wpsimp | wp (once) sts_st_tcb')+
+        apply (wpsimp | wp (once) sts_st_tcb' hoare_drop_imps)+
   apply (rule_tac Q="\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr
                           and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp)
    apply (clarsimp)
@@ -1815,7 +1815,7 @@ lemma deletingIRQHandler_no_orphans [wp]:
    deletingIRQHandler irq
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding deletingIRQHandler_def
-  apply (wp, auto)
+  apply (wp hoare_drop_imps, auto)
   done
 
 lemma finaliseCap_no_orphans [wp]:
@@ -2340,7 +2340,7 @@ lemma deleteCallerCap_no_orphans [wp]:
    deleteCallerCap receiver
    \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
   unfolding deleteCallerCap_def
-  by wpsimp auto
+  by (wpsimp wp: hoare_drop_imps) auto
 
 lemma remove_neg_strg:
   "(A \<and> B) \<longrightarrow> ((x \<longrightarrow> A) \<and> (\<not> x \<longrightarrow> B))"

proof/refine/ARM_HYP/PageTableDuplicates.thy

@@ -2102,14 +2102,15 @@ crunch valid_duplicates'[wp]:
 
 crunch valid_duplicates'[wp]:
   receiveIPC "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
-(wp: getNotification_wp gbn_wp')
+  (wp: getNotification_wp gbn_wp' crunch_wps)
 
 crunch valid_duplicates'[wp]:
   deleteCallerCap "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
   (wp: crunch_wps)
 
 crunch valid_duplicates'[wp]:
   handleReply "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
+  (wp: crunch_wps)
 
 crunch valid_duplicates'[wp]:
   handleYield "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"