theory CSpaceInv_AI

lemma valid_thread_state_tcb_update:
  "\<lbrakk> tcb_at t s \<rbrakk> \<Longrightarrow>
  valid_tcb_state ts (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = valid_tcb_state ts s" apply (unfold valid_tcb_state_def) apply (case_tac ts) apply (simp_all add: obj_at_tcb_update is_ep_def is_tcb_def is_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> valid_tcb_state ts (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = valid_tcb_state ts s proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>tcb_at t s; ts = Running\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 2. \<lbrakk>tcb_at t s; inactive ts\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 3. \<lbrakk>tcb_at t s; ts = Restart\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 4. \<And>x41 x42. \<lbrakk>tcb_at t s; ts = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 5. \<And>x51 x52. \<lbrakk>tcb_at t s; ts = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 6. \<lbrakk>tcb_at t s; awaiting_reply ts\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 7. \<And>x7. \<lbrakk>tcb_at t s; ts = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)
 8. \<lbrakk>tcb_at t s; idle ts\<rbrakk> \<Longrightarrow> (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnSend ref sp \<Rightarrow> ep_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | BlockedOnNotification ref \<Rightarrow> ntfn_at ref (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) | _ \<Rightarrow> True) = (case ts of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True) proof (prove)
goal:
No subgoals!