theory CSpaceInv_AI

lemma valid_cap_tcb_update [simp]:
  "tcb_at t s \<Longrightarrow> (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) \<turnstile> cap = s \<turnstile> cap" apply (clarsimp simp: is_tcb elim!: obj_atE) apply (subgoal_tac "a_type (TCB tcba) = a_type (TCB tcb)") apply (rule iffI) apply (drule(1) valid_cap_same_type[where p=t]) apply simp apply (simp add: fun_upd_idem) apply (erule(2) valid_cap_same_type[OF _ sym]) apply (simp add: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap = s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap = s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb)\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap = s \<turnstile> cap
 2. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal (3 subgoals):
 1. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap
 3. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal (4 subgoals):
 1. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb)\<rbrakk> \<Longrightarrow> kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) t = Some (TCB tcb)
 2. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb), kheap := (kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>))(t \<mapsto> TCB tcba)\<rparr> \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 3. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap
 4. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal (3 subgoals):
 1. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb), kheap := (kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>))(t \<mapsto> TCB tcba)\<rparr> \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap
 3. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal (2 subgoals):
 1. \<And>tcba. \<lbrakk>kheap s t = Some (TCB tcba); a_type (TCB tcba) = a_type (TCB tcb); s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr> \<turnstile> cap
 2. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcba. kheap s t = Some (TCB tcba) \<Longrightarrow> a_type (TCB tcba) = a_type (TCB tcb) proof (prove)
goal:
No subgoals!