arm crefine: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

proof/crefine/ARM/Arch_C.thy

@@ -2018,12 +2018,10 @@ lemma ivc_label_flush_case:
   by (auto split: invocation_label.split arch_invocation_label.split)
 
 lemma injection_handler_whenE:
-  "injection_handler Inl (whenE a b)
+  "injection_handler Inl (whenE a b) = (if a then injection_handler Inl b else returnOk ())"
-   = (if a then (injection_handler Inl b)
-      else (returnOk ()))"
   apply (subst injection_handler_returnOk[symmetric])
-  apply (clarsimp simp:whenE_def injection_handler_def)
+  apply (clarsimp simp: whenE_def injection_handler_def cong: if_cong)
-  apply (fastforce simp:split:if_splits)
+  apply (fastforce split: if_splits)
   done
 
 lemma injection_handler_if_returnOk:
@@ -2215,6 +2213,7 @@ lemma decodeARMFrameInvocation_ccorres:
        (decodeARMMMUInvocation label args cptr slot cp extraCaps
               >>= invocationCatch thread isBlocking isCall InvokeArchObject)
        (Call decodeARMFrameInvocation_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   apply (clarsimp simp only: isCap_simps)
   apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' excaps_' cap_' buffer_'
                 simp: decodeARMMMUInvocation_def decodeARMPageFlush_def)
@@ -2753,7 +2752,7 @@ proof -
     using assms
     apply (subst AND_NOT_mask_plus_AND_mask_eq
       [where w = start,symmetric,where n = "pageBitsForSize a"])
-    apply (simp add:sign_simps page_base_def)
+    apply (simp add: page_base_def)
     apply (drule word_le_minus_mono_left[where x= "start && ~~ mask (pageBitsForSize a)"])
      apply (rule word_and_le2)
     apply (simp(no_asm_use), simp)

proof/crefine/ARM/CSpace_C.thy

@@ -826,6 +826,7 @@ lemma update_freeIndex':
       using order_trans[OF i'_bound power_increasing[OF sz_bound], simplified]
       by (simp add: word_of_nat_le untypedBits_defs)
     show ?thesis
+      supply if_cong[cong]
       apply (cinit lift: cap_ptr_' v32_')
        apply (rule ccorres_pre_getCTE)
        apply (rule_tac P="\<lambda>s. ctes_of s srcSlot = Some rv \<and> (\<exists>i. cteCap rv = UntypedCap d p sz i)"
@@ -1893,7 +1894,7 @@ lemma heap_list_zero_Ball_intvl:
 lemma untypedZeroRange_not_device:
   "untypedZeroRange cap = Some r
     \<Longrightarrow> \<not> capIsDevice cap"
-  by (clarsimp simp: untypedZeroRange_def)
+  by (clarsimp simp: untypedZeroRange_def cong: if_cong)
 
 lemma updateTrackedFreeIndex_noop_ccorres:
   "ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
@@ -2054,6 +2055,7 @@ lemma emptySlot_ccorres:
           []
           (emptySlot slot info)
           (Call emptySlot_'proc)"
+  supply if_cong[cong]
   apply (cinit lift: slot_' cleanupInfo_' simp: case_Null_If)
 
   \<comment> \<open>--- handle the clearUntypedFreeIndex\<close>
@@ -2291,6 +2293,7 @@ lemma Arch_sameRegionAs_spec:
                  ccap_relation (ArchObjectCap capb) \<acute>cap_b  \<rbrace>
   Call Arch_sameRegionAs_'proc
   \<lbrace>  \<acute>ret__unsigned_long = from_bool (Arch.sameRegionAs capa capb) \<rbrace>"
+  supply if_cong[cong]
   apply vcg
   apply clarsimp
 
@@ -2679,7 +2682,7 @@ lemma ccap_relation_get_capSizeBits_physical:
         defer 4 (* arch caps last *)
         apply ((frule cap_get_tag_isCap_unfolded_H_cap,
                      clarsimp simp: unfolds
-                             split: if_split_asm)+)[5] (* SOMEONE FIX SUBGOAL PLZ *)
+                             split: if_split_asm)+)[5]
    apply (frule cap_get_tag_isCap_unfolded_H_cap)
    apply (clarsimp simp: unfolds split: if_split_asm)
    apply (rule arg_cong [OF less_mask_eq[where n=5, unfolded mask_def, simplified]])
@@ -3221,6 +3224,7 @@ lemma isMDBParentOf_spec:
             (\<exists>s. s \<turnstile>' (cteCap ctea)) }
    Call isMDBParentOf_'proc
    \<lbrace> \<acute>ret__unsigned_long = from_bool (isMDBParentOf ctea cteb) \<rbrace>"
+  supply if_cong[cong]
   apply (intro allI, rule conseqPre)
    apply vcg
   apply (clarsimp simp: isMDBParentOf_def)
@@ -3309,6 +3313,7 @@ lemma updateCapData_spec:
   "\<forall>cap. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<and> preserve = to_bool (\<acute>preserve) \<and> newData = \<acute>newData\<rbrace>
   Call updateCapData_'proc
   \<lbrace>  ccap_relation (updateCapData preserve newData cap) \<acute>ret__struct_cap_C \<rbrace>"
+  supply if_cong[cong]
   apply (rule allI, rule conseqPre)
   apply vcg
   apply (clarsimp simp: if_1_0_0)

proof/crefine/ARM/CSpace_RAB_C.thy

@@ -390,6 +390,7 @@ next
     note if_cong[cong]
     show ?case
       using ind.prems
+      supply option.case_cong[cong]
       apply -
       apply (rule iffD1 [OF ccorres_expand_while_iff])
       apply (subst resolveAddressBits.simps)

proof/crefine/ARM/Delete_C.thy

@@ -138,6 +138,7 @@ lemma capRemovable_spec:
   "\<forall>cap s.  \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> (isZombie cap \<or> cap = NullCap) \<and> capAligned cap\<rbrace>
      Call capRemovable_'proc
       {s'. ret__unsigned_long_' s' = from_bool (capRemovable cap (ptr_val (slot_' s)))}"
+  supply if_cong[cong]
   apply vcg
   apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]])
   apply (simp add: capRemovable_def from_bool_def[where b=True] true_def)
@@ -157,6 +158,7 @@ lemma capCyclicZombie_spec:
   "\<forall>cap s.  \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace>
      Call capCyclicZombie_'proc
       {s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}"
+  supply if_cong[cong]
   apply vcg
   apply (clarsimp simp: from_bool_0)
   apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp)

proof/crefine/ARM/DetWP.thy

@@ -60,7 +60,7 @@ lemma det_wp_getTCB [wp]:
   apply (rule det_wp_pre)
    apply (wp|wpc)+
   apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps
-                      cong: conj_cong)
+                      cong: conj_cong option.case_cong)
   apply (simp add: lookupAround2_known1)
   apply (rule ps_clear_lookupAround2, assumption+)
     apply simp

proof/crefine/ARM/Fastpath_C.thy

@@ -398,9 +398,10 @@ lemma lookup_fp_ccorres':
 
     have cap_get_tag_update_1:
       "\<And>f cap. cap_get_tag (cap_C.words_C_update (\<lambda>w. Arrays.update w (Suc 0) (f w)) cap) = cap_get_tag cap"
-      by (simp add: cap_get_tag_def)
+      by (simp add: cap_get_tag_def cong: if_cong)
 
     show ?case
+    supply if_cong[cong] option.case_cong[cong]
     apply (cinitlift cap_' bits_')
     apply (rename_tac cbits ccap)
     apply (elim conjE)
@@ -1881,6 +1882,7 @@ proof -
   (* FIXME indentation is wonky in this proof, fix will come in a future patch, hopefully when
      automatic indentation is improved *)
   show ?thesis
+  supply if_cong[cong] option.case_cong[cong]
   apply (cinit lift: cptr_' msgInfo_')
      apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
                       unifyFailure_catch_If catch_liftE
@@ -2699,6 +2701,7 @@ lemma fastpath_reply_recv_ccorres:
   show ?thesis
   using [[goals_limit = 1]]
   supply option.case_cong_weak[cong del]
+  supply if_cong[cong]
   apply (cinit lift: cptr_' msgInfo_')
      apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
                       unifyFailure_catch_If catch_liftE
@@ -3494,9 +3497,13 @@ lemma setCTE_obj_at'_tcbIPCBuffer:
   unfolding setCTE_def
   by (rule setObject_cte_obj_at_tcb', simp+)
 
+context
+notes if_cong[cong]
+begin
 crunches cteInsert, asUser
   for obj_at'_tcbIPCBuffer[wp]: "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
   (wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest)
+end
 
 crunch ksReadyQueues_inv[wp]: cteInsert "\<lambda>s. P (ksReadyQueues s)"
   (wp: hoare_drop_imps)
@@ -3524,6 +3531,7 @@ lemma fastpath_callKernel_SysCall_corres:
                 and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
                 and (\<lambda>s. ksDomainTime s \<noteq> 0))
      (callKernel (SyscallEvent SysCall)) (fastpaths SysCall)"
+  supply if_cong[cong]
   apply (rule monadic_rewrite_introduce_alternative)
    apply (simp add: callKernel_def)
   apply (rule monadic_rewrite_imp)
@@ -4439,24 +4447,19 @@ lemma tcbSchedEnqueue_tcbIPCBuffer:
 crunch obj_at'_tcbIPCBuffer[wp]: rescheduleRequired "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
   (wp: crunch_wps tcbSchedEnqueue_tcbIPCBuffer simp: rescheduleRequired_def)
 
+context
+notes if_cong[cong]
+begin
 crunch obj_at'_tcbIPCBuffer[wp]: setThreadState "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
   (wp: crunch_wps threadSet_obj_at'_really_strongest)
 
-crunch obj_at'_tcbIPCBuffer[wp]: getCTE "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
-  (wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest)
-
-crunch obj_at'_tcbIPCBuffer[wp]: emptySlot "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
-  (wp: crunch_wps)
-
-crunch obj_at'_tcbIPCBuffer[wp]: transferCapsToSlots "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
-  (wp: crunch_wps transferCapsToSlots_pres1 simp: crunch_simps ignore: constOnFailure)
-
-crunch obj_at'_tcbIPCBuffer[wp]: asUser "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
-  (wp: crunch_wps)
-
 crunch obj_at'_tcbIPCBuffer[wp]: handleFault "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
   (wp: crunch_wps constOnFailure_wp tcbSchedEnqueue_tcbIPCBuffer threadSet_obj_at'_really_strongest
    simp: zipWithM_x_mapM)
+end
+
+crunch obj_at'_tcbIPCBuffer[wp]: emptySlot "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
+  (wp: crunch_wps)
 
 lemma fastpath_callKernel_SysReplyRecv_corres:
   "monadic_rewrite True False
@@ -4465,6 +4468,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
      (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)"
   including no_pre
   supply option.case_cong_weak[cong del]
+  supply if_cong[cong]
   apply (rule monadic_rewrite_introduce_alternative)
    apply (simp add: callKernel_def)
   apply (rule monadic_rewrite_imp)

proof/crefine/ARM/Finalise_C.thy

@@ -757,6 +757,7 @@ lemma unbindNotification_ccorres:
   "ccorres dc xfdc
     (invs') (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) []
     (unbindNotification tcb) (Call unbindNotification_'proc)"
+  supply option.case_cong[cong]
   apply (cinit lift: tcb_')
    apply (rule_tac xf'=ntfnPtr_'
                     and r'="\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0"
@@ -790,6 +791,7 @@ lemma unbindNotification_ccorres:
 lemma unbindMaybeNotification_ccorres:
   "ccorres dc xfdc (invs') (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) []
         (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)"
+  supply option.case_cong[cong]
   apply (cinit lift: ntfnPtr_')
    apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification])
     apply (rule ccorres_rhs_assoc2)
@@ -1435,6 +1437,7 @@ lemma Arch_finaliseCap_ccorres:
    (UNIV \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
                         \<inter> {s. final_' s = from_bool is_final}) []
    (Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)"
+  supply if_cong[cong]
   apply (cinit lift: cap_' final_' cong: call_ignore_cong)
    apply csymbr
    apply (simp add: ARM_H.finaliseCap_def cap_get_tag_isCap_ArchObject)

proof/crefine/ARM/Invoke_C.thy

@@ -568,6 +568,7 @@ lemma decodeCNodeInvocation_ccorres:
        (decodeCNodeInvocation lab args cp (map fst extraCaps)
            >>= invocationCatch thread isBlocking isCall InvokeCNode)
   (Call decodeCNodeInvocation_'proc)"
+  supply if_cong[cong]
   apply (cases "\<not>isCNodeCap cp")
    apply (simp add: decodeCNodeInvocation_def
               cong: conj_cong)
@@ -1690,6 +1691,7 @@ lemma resetUntypedCap_ccorres:
      (resetUntypedCap slot)
      (Call resetUntypedCap_'proc)"
   using [[ceqv_simpl_sequence = true]]
+  supply if_cong[cong] option.case_cong[cong]
   apply (cinit lift: srcSlot_')
    apply (simp add: liftE_bindE getSlotCap_def
                     Collect_True extra_sle_sless_unfolds)
@@ -2533,9 +2535,10 @@ lemma checkFreeIndex_ccorres:
      apply (rule context_conjI)
       apply (clarsimp simp:cap_get_tag_isCap)
       apply assumption
-     apply (clarsimp simp:ccap_relation_def isCap_simps cap_untyped_cap_lift_def
+     apply (clarsimp simp: ccap_relation_def isCap_simps cap_untyped_cap_lift_def cap_lift_def
-            cap_lift_def cap_to_H_def
+                           cap_to_H_def
-            split:if_splits)
+                     split: if_splits
+                     cong: if_cong)
     apply (rule ensureNoChildren_wp[where P = dc])
    apply clarsimp
    apply (vcg exspec=ensureNoChildren_modifies)
@@ -2648,6 +2651,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
            liftE (stateAssert (valid_untyped_inv' uinv) []); returnOk uinv odE)
            >>= invocationCatch thread isBlocking isCall InvokeUntyped)
   (Call decodeUntypedInvocation_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   apply (rule ccorres_name_pre)
   apply (cinit' lift: invLabel_' length___unsigned_long_' cap_' slot_' excaps_' call_' buffer_'
                 simp: decodeUntypedInvocation_def list_case_If2

proof/crefine/ARM/IpcCancel_C.thy

@@ -2123,8 +2123,8 @@ lemma possibleSwitchTo_ccorres:
   supply dc_simp [simp del]
   supply prio_and_dom_limit_helpers[simp]
   (* FIXME: these should likely be in simpset for CRefine, or even in general *)
-  supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp]
+  supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp]
-         ccorres_IF_True[simp]
+         ccorres_IF_True[simp] if_cong[cong]
   apply (cinit lift: target_')
    apply (rule ccorres_move_c_guard_tcb)
    apply (rule ccorres_pre_curDomain, rename_tac curDom)
@@ -2175,7 +2175,7 @@ lemma scheduleTCB_ccorres':
        rescheduleRequired
   od)
   (Call scheduleTCB_'proc)"
-  apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
+  apply (cinit' lift: tptr_')
    apply (rule ccorres_rhs_assoc2)+
    apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
        defer
@@ -2196,7 +2196,7 @@ lemma scheduleTCB_ccorres':
                                  \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)"
                            and P'=UNIV in ccorres_from_vcg)
            apply (rule allI, rule conseqPre, vcg)
-           apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
+           apply (clarsimp simp: return_def split del: if_split)
            apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
            apply (rule conjI)
             apply (clarsimp simp: st_tcb_at'_def)

proof/crefine/ARM/Ipc_C.thy

@@ -26,10 +26,6 @@ lemma replyFromKernel_success_empty:
   unfolding replyFromKernel_def replyFromKernel_success_empty_def
   by (simp add: setMRs_Nil submonad_asUser.fn_stateAssert)
 
-crunch valid_queues[wp]: handleFaultReply valid_queues
-
-crunch valid_queues'[wp]: handleFaultReply valid_queues'
-
 crunch sch_act_wf: handleFaultReply "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
 
 crunch valid_ipc_buffer_ptr' [wp]: copyMRs "valid_ipc_buffer_ptr' p"
@@ -1228,7 +1224,7 @@ lemma asUser_tcbFault_obj_at:
    \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
   apply (simp add: asUser_def split_def)
   apply (wp threadGet_wp)
-  apply simp
+  apply (simp cong: if_cong)
   done
 
 lemma asUser_atcbContext_obj_at:
@@ -3732,6 +3728,7 @@ lemma handleFaultReply_ccorres [corres]:
               msg \<leftarrow> getMRs s sb tag;
               handleFaultReply f r (msgLabel tag) msg
             od) (Call handleFaultReply_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   apply (unfold K_def, rule ccorres_gen_asm)
   apply (rule monadic_rewrite_ccorres_assemble_nodrop[OF _ handleFaultReply',rotated], simp)
   apply (cinit lift: sender_' receiver_' simp: whileAnno_def)
@@ -3843,6 +3840,9 @@ lemma handleFaultReply_ccorres [corres]:
   apply (fastforce simp: seL4_Faults seL4_Arch_Faults)
   done
 
+context
+notes if_cong[cong]
+begin
 crunch tcbFault: emptySlot, tcbSchedEnqueue, rescheduleRequired
           "obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
   (wp: threadSet_obj_at'_strongish crunch_wps
@@ -3851,13 +3851,14 @@ crunch tcbFault: emptySlot, tcbSchedEnqueue, rescheduleRequired
 crunch tcbFault: setThreadState, cancelAllIPC, cancelAllSignals
           "obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
   (wp: threadSet_obj_at'_strongish crunch_wps)
+end
 
 lemma sbn_tcbFault:
   "\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
   setBoundNotification st t'
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
   apply (simp add: setBoundNotification_def)
-  apply (wp threadSet_obj_at' | simp)+
+  apply (wp threadSet_obj_at' | simp cong: if_cong)+
   done
 
 crunch tcbFault: unbindNotification, unbindMaybeNotification "obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
@@ -3890,7 +3891,7 @@ proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots)
 next
   case (Cons cp cps)
   show ?case using Cons.prems
-    by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak)
+    by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak cong: if_cong)
 qed
 
 lemma transferCaps_local_slots:
@@ -6192,6 +6193,7 @@ lemma receiveSignal_ccorres [corres]:
      (receiveSignal thread cap is_blocking)
      (Call receiveSignal_'proc)"
   unfolding K_def
+  supply if_cong[cong] option.case_cong[cong]
   apply (rule ccorres_gen_asm)
   apply (cinit lift: thread_' cap_' isBlocking_')
    apply (rule ccorres_pre_getNotification, rename_tac ntfn)

proof/crefine/ARM/IsolatedThreadAction.thy

@@ -743,6 +743,7 @@ lemma doIPCTransfer_simple_rewrite:
          y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
          asUser rcvr (setRegister ARM_H.badgeRegister badge)
       od)"
+  supply if_cong[cong]
   apply (rule monadic_rewrite_gen_asm)
   apply (simp add: doIPCTransfer_def bind_assoc doNormalTransfer_def
                    getMessageInfo_def
@@ -930,7 +931,11 @@ crunch obj_at_prio[wp]: cteDeleteOne "obj_at' (\<lambda>tcb. P (tcbPriority tcb)
        setThreadState_obj_at_unchanged setNotification_tcb setBoundNotification_obj_at_unchanged
         simp: crunch_simps unless_def)
 
+context
+notes if_cong[cong]
+begin
 crunch obj_at_dom[wp]: rescheduleRequired "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
+end
 
 context kernel_m begin
 
@@ -1144,6 +1149,7 @@ lemma assert_isolatable:
 
 lemma cteInsert_isolatable:
   "thread_actions_isolatable idx (cteInsert cap src dest)"
+  supply if_cong[cong]
   apply (simp add: cteInsert_def updateCap_def updateMDB_def
                    Let_def setUntypedCapAsFull_def)
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@@ -1435,6 +1441,7 @@ lemma updateMDB_isolatable:
 
 lemma clearUntypedFreeIndex_isolatable:
   "thread_actions_isolatable idx (clearUntypedFreeIndex slot)"
+  supply option.case_cong[cong]
   apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
   apply (rule thread_actions_isolatable_bind)
     apply (rule getCTE_isolatable)
@@ -1472,6 +1479,7 @@ lemmas fastpath_isolate_rewrites
 
 lemma lookupIPCBuffer_isolatable:
   "thread_actions_isolatable idx (lookupIPCBuffer w t)"
+  supply if_cong[cong]
   apply (simp add: lookupIPCBuffer_def)
   apply (rule thread_actions_isolatable_bind)
   apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable

proof/crefine/ARM/Refine_C.thy

@@ -22,14 +22,11 @@ declare liftE_handle [simp]
 
 lemma schedule_sch_act_wf:
   "\<lbrace>invs'\<rbrace> schedule \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
-apply (rule hoare_post_imp)
+  apply (rule hoare_post_imp)
- apply (erule invs_sch_act_wf')
+   apply (erule invs_sch_act_wf')
-apply (rule schedule_invs')
+  apply (rule schedule_invs')
-done
+  done
 
-(* FIXME: This is cheating since ucast from 10 to 16 will never give us 0xFFFF.
-          However type of 10 word is from irq oracle so it is the oracle that matters not this lemma.
-   (Xin) *)
 lemma ucast_not_helper_cheating:
   fixes a:: "10 word"
   assumes a: "ucast a \<noteq> (0xFFFF :: word16)"

proof/crefine/ARM/Retype_C.thy

@@ -720,6 +720,7 @@ lemma clift_ptr_retyps_gen_memset_same:
          = (\<lambda>y. if y \<in> (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) o of_nat) ` {k. k < n}
                 then Some (from_bytes (replicate (size_of TYPE('a  :: mem_type)) 0)) else clift hrs y)"
   using sz
+  supply if_cong[cong]
   apply (simp add: nb liftt_if[folded hrs_mem_def hrs_htd_def]
                    hrs_htd_update hrs_mem_update
                    h_t_valid_ptr_retyps_gen_same[OF guard cleared not_byte]
@@ -766,7 +767,8 @@ lemma clift_ptr_retyps_gen_other:
   apply (cases p)
   apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def]
                    h_t_valid_def hrs_htd_update
-                   ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz])
+                   ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz]
+              cong: if_cong)
   done
 
 lemma clift_heap_list_update_no_heap_other:
@@ -1701,18 +1703,19 @@ proof (intro impI allI)
   have relrl:
     "cpte_relation makeObject (from_bytes (replicate (size_of TYPE(pte_C)) 0))"
     unfolding cpte_relation_def
+    supply if_cong[cong]
     apply (simp add: Let_def makeObject_pte size_of_def pte_lift_def)
     apply (simp add: from_bytes_def)
     apply (simp add: typ_info_simps pte_C_tag_def pte_lift_def pte_get_tag_def
-      size_td_lt_final_pad size_td_lt_ti_typ_pad_combine Let_def size_of_def)
+                     size_td_lt_final_pad size_td_lt_ti_typ_pad_combine Let_def size_of_def)
-    apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine Let_def
+    apply (simp add: final_pad_def size_td_lt_ti_typ_pad_combine Let_def
-      size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
+                     size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
-      ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def)
+                     ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def)
     apply (simp add: typ_info_array array_tag_def eval_nat_numeral)
     apply (simp add: array_tag_n.simps)
-    apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine Let_def
+    apply (simp add: final_pad_def size_td_lt_ti_typ_pad_combine Let_def
-      size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
+                     size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
-      ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def)
+                     ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def)
     apply (simp add: update_ti_t_word32_0s pte_tag_defs)
     done
 
@@ -2355,6 +2358,7 @@ lemma insertNewCap_ccorres1:
        \<inter> {s. slot_' s = Ptr slot}) []
      (insertNewCap parent slot cap)
      (Call insertNewCap_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   apply (cinit (no_ignore_call) lift: cap_' parent_' slot_')
   apply (rule ccorres_liftM_getCTE_cte_at)
    apply (rule ccorres_move_c_guard_cte)
@@ -3231,7 +3235,7 @@ lemma zero_ranges_are_zero_update_zero[simp]:
     \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update_list ptr (replicate n 0)) hrs)"
   apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update)
   apply (drule(1) bspec)
-  apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq)
+  apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq cong: if_cong)
   done
 
 lemma rf_sr_rep0:
@@ -4360,6 +4364,7 @@ proof (intro impI allI)
   hence "cpspace_relation ?ks (underlying_memory (ksMachineState \<sigma>)) ?ks'"
     unfolding cpspace_relation_def
     using empty rc' szo
+    supply if_cong[cong]
     apply -
     apply (clarsimp simp: rl' tag_disj_via_td_name cte_C_size ht_rl
                           clift_ptr_retyps_gen_other
@@ -6825,6 +6830,7 @@ shows  "ccorres dc xfdc
      ) []
      (createNewObjects newType srcSlot destSlots ptr userSize isdev)
      (Call createNewObjects_'proc)"
+  supply if_cong[cong]
   apply (rule ccorres_gen_asm_state)
   apply clarsimp
   apply (subgoal_tac "unat (of_nat (getObjectSize newType userSize)) = getObjectSize newType userSize")

proof/crefine/ARM/SyscallArgs_C.thy

@@ -984,6 +984,7 @@ lemma getMRs_user_word:
       \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
   getMRs thread (Some buffer) info
   \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>"
+  supply if_cong[cong]
   apply (rule hoare_assume_pre)
   apply (elim conjE)
   apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y)

proof/crefine/ARM/Syscall_C.thy

@@ -548,6 +548,7 @@ lemma sendFaultIPC_ccorres:
             \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
       [] (sendFaultIPC tptr fault)
          (Call sendFaultIPC_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   supply Collect_const[simp del]
   apply (cinit lift: tptr_' cong: call_ignore_cong)
    apply (simp add: liftE_bindE del:Collect_const cong:call_ignore_cong)
@@ -722,6 +723,7 @@ lemma getMRs_length:
   "\<lbrace>\<lambda>s. msgLength mi \<le> 120\<rbrace> getMRs thread buffer mi
   \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi))
             else length args = unat (msgLength mi)\<rbrace>"
+  supply if_cong[cong]
   apply (cases buffer)
    apply (simp add: getMRs_def)
    apply (rule hoare_pre, wp)
@@ -1164,6 +1166,7 @@ lemma handleRecv_ccorres:
        []
        (handleRecv isBlocking)
        (Call handleRecv_'proc)"
+  supply if_cong[cong] option.case_cong[cong]
   apply (cinit lift: isBlocking_')
    apply (rule ccorres_pre_getCurThread)
    apply (ctac)

proof/crefine/ARM/VSpace_C.thy

@@ -555,8 +555,9 @@ lemma generic_frame_cap_get_capFIsMapped_spec:
        Call generic_frame_cap_get_capFIsMapped_'proc
        \<lbrace>\<acute>ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \<noteq> 0 then 1 else 0)\<rbrace>"
   apply vcg
-  apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast])
+  apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast]
-done
+                  cong: if_cong)
+  done
 
 
 
@@ -1997,6 +1998,7 @@ lemma ccorres_return_void_C':
 lemma is_aligned_cache_preconds:
   "\<lbrakk>is_aligned rva n; n \<ge> 6\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F \<and>
           addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5"
+  supply if_cong[cong]
   apply (drule is_aligned_weaken, simp)
   apply (rule conjI)
    apply (drule is_aligned_no_overflow, simp, unat_arith)[1]
@@ -2752,6 +2754,7 @@ lemma makeUserPDE_spec:
        C_CL = 0,
        B_CL = iwb_from_cacheable  \<^bsup>s\<^esup>cacheable
     \<rparr>) \<rbrace>"
+  supply if_cong[cong]
   apply (rule allI, rule conseqPre, vcg)
   apply (clarsimp simp:ap_from_vm_rights_mask split:if_splits)
   apply (intro conjI impI allI | clarsimp )+

proof/crefine/lib/AutoCorres_C.thy

@@ -34,11 +34,11 @@ The following setup restores the ordering from @{theory CRefine.Corres_C} for th
 the end of the @{attribute wp_comb} set.
 
 To ensure that we only have to do this once, we are careful to ensure that there is only
-one theory merge between AutoCorres and CRefine. We import @{theory CRefine.L4VerifiedLinks} into
+one theory merge between AutoCorres and CRefine. We import @{theory CBaseRefine.L4VerifiedLinks} into
 @{theory CRefine.AutoCorresModifiesProofs}, and import the latter here. This satisfies the
 dependencies from @{theory CRefine.AutoCorresModifiesProofs} to @{theory AutoCorres.AutoCorres}, and from
-this theory to @{theory CRefine.L4VerifiedLinks} and @{theory CRefine.Corres_C}, without duplicating
+this theory to @{theory CBaseRefine.L4VerifiedLinks} and @{theory CRefine.Corres_C}, without duplicating
-theory merges. Finally, we list @{theory CRefine.L4VerifiedLinks} as a top-level theory in the
+theory merges. Finally, we list @{theory CBaseRefine.L4VerifiedLinks} as a top-level theory in the
 CBaseRefine session, so that @{theory AutoCorres.AutoCorres} need not be processed in a CRefine
 session, but do not import @{theory AutoCorres.AutoCorres} into @{text CBaseRefine.Include_C}, since that would
 cause a redundant theory merge.