theory Finalise_R

lemma finaliseCap_zombie_cap[wp]:
  "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>
     finaliseCap cap fin flag
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>" apply (simp add: finaliseCap_def Let_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp suspend_cte_wp_at'
             deletingIRQHandler_cte_preserved
                 | clarsimp simp: finaliseCap_def isCap_simps | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte)) sl\<rbrace> if isEndpointCap cap then do y <- when fin (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when fin (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if flag then fail else if isCNodeCap cap \<and> fin then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> fin then do cte_ptr <- getThreadCSpaceRoot (capTCBPtr cap);
y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- Arch.prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> fin then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) fin else if isIRQHandlerCap cap \<and> fin then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> fin then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte)) sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q26\<rbrace> if isEndpointCap cap then do y <- when fin (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when fin (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if flag then fail else if isCNodeCap cap \<and> fin then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> fin then do cte_ptr <- getThreadCSpaceRoot (capTCBPtr cap);
y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- Arch.prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> fin then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) fin else if isIRQHandlerCap cap \<and> fin then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> fin then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte)) sl\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> isZombie (cteCap cte)) sl s \<Longrightarrow> ?Q26 s proof (prove)
goal:
No subgoals!