theory Tcb_AI

lemma tcb_not_in_state_refs_of_tcb:
  "tcb_at a s \<Longrightarrow> (a, NTFNBound) \<notin> state_refs_of s a" apply (clarsimp simp: tcb_at_def obj_at_def is_tcb_def) apply (case_tac ko) apply simp_all apply (clarsimp simp: state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def) apply (erule disjE) apply (rename_tac tcb_ext) apply (case_tac "tcb_state tcb_ext") apply simp_all apply (simp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at a s \<Longrightarrow> (a, NTFNBound) \<notin> state_refs_of s a proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a; ko = CNode x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x2. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a; ko = TCB x2\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x3. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a; ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x4. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a; ko = Notification x4\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x5. \<lbrakk>kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; (a, NTFNBound) \<in> state_refs_of s a; ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> state_refs_of s a; ko = TCB x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_state x2 of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}) \<or> (a, NTFNBound) \<in> (case tcb_bound_notification x2 of None \<Rightarrow> {} | Some ntfn \<Rightarrow> {(ntfn, TCBBound)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_state x2 of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_bound_notification x2 of None \<Rightarrow> {} | Some ntfn \<Rightarrow> {(ntfn, TCBBound)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_bound_notification x2 of None \<Rightarrow> {} | Some ntfn \<Rightarrow> {(ntfn, TCBBound)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); tcb_state tcb_ext = Running\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); inactive (tcb_state tcb_ext)\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); tcb_state tcb_ext = Restart\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb_ext x41 x42. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); tcb_state tcb_ext = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> False
 5. \<And>tcb_ext x51 x52. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); tcb_state tcb_ext = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> False
 6. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); awaiting_reply (tcb_state tcb_ext)\<rbrakk> \<Longrightarrow> False
 7. \<And>tcb_ext x7. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); tcb_state tcb_ext = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> False
 8. \<And>tcb_ext. \<lbrakk>kheap s a = Some (TCB tcb_ext); (a, NTFNBound) \<in> (case tcb_state tcb_ext of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}); idle (tcb_state tcb_ext)\<rbrakk> \<Longrightarrow> False
 9. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_bound_notification x2 of None \<Rightarrow> {} | Some ntfn \<Rightarrow> {(ntfn, TCBBound)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>kheap s a = Some (TCB x2); (a, NTFNBound) \<in> (case tcb_bound_notification x2 of None \<Rightarrow> {} | Some ntfn \<Rightarrow> {(ntfn, TCBBound)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!