theory IpcCancel_R

lemma (in delete_one_conc_pre) finaliseCap_tcb_at_runnable':
  "\<lbrace>st_tcb_at' runnable' t\<rbrace> finaliseCap cap final True \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>" apply (clarsimp simp add: finaliseCap_def Let_def) apply (rule conjI | clarsimp | wp cancelAllIPC_tcb_at_runnable' getObject_ntfn_inv
                                    cancelAllSignals_tcb_at_runnable'
       | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' runnable' t\<rbrace> global.finaliseCap cap final True \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. (cap = capability.DomainCap \<longrightarrow> (isNotificationCap capability.DomainCap \<longrightarrow> (isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>) \<and> (\<not> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.DomainCap);
cancelAllSignals (capNtfnPtr capability.DomainCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>)) \<and> (\<not> isNotificationCap capability.DomainCap \<longrightarrow> isEndpointCap capability.DomainCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.DomainCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>)) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> (isNotificationCap capability.NullCap \<longrightarrow> (isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>) \<and> (\<not> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr capability.NullCap);
cancelAllSignals (capNtfnPtr capability.NullCap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>)) \<and> (\<not> isNotificationCap capability.NullCap \<longrightarrow> isEndpointCap capability.NullCap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr capability.NullCap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (isEndpointCap cap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>) \<and> (\<not> isEndpointCap cap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>)) \<and> (\<not> isNotificationCap cap \<longrightarrow> isEndpointCap cap \<longrightarrow> \<lbrace>st_tcb_at' runnable' t\<rbrace> do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>))) proof (prove)
goal:
No subgoals!