theory CSpaceInv_AI

lemma valid_objs_tcb_update:
  "\<lbrakk>tcb_at t s; valid_tcb t tcb s; valid_objs s \<rbrakk>
  \<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)" apply (clarsimp simp: valid_objs_def dom_def
                 elim!: obj_atE) apply (intro conjI impI) apply (rule valid_obj_same_type) apply (simp add: valid_obj_def)+ apply (clarsimp simp: a_type_def is_tcb) apply clarsimp apply (rule valid_obj_same_type) apply (drule_tac x=ptr in spec, simp) apply (simp add: valid_obj_def) apply assumption apply (clarsimp simp add: a_type_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; valid_tcb t tcb s; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> (ptr = t \<longrightarrow> valid_obj t (TCB tcb) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)) \<and> (ptr \<noteq> t \<longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> valid_obj t (TCB tcb) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)
 2. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; \<exists>y. kheap s ptr = Some y\<rbrakk> \<Longrightarrow> \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> valid_obj t (TCB tcb) s
 2. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> valid_obj t (TCB tcb) s
 3. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> kheap s t = Some (?ko21 ko ptr)
 4. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> a_type (TCB tcb) = a_type (?ko21 ko ptr)
 5. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; \<exists>y. kheap s ptr = Some y\<rbrakk> \<Longrightarrow> \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)); kheap s t = Some ko; is_tcb ko; ptr = t\<rbrakk> \<Longrightarrow> ATCB = a_type ko
 2. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; \<exists>y. kheap s ptr = Some y\<rbrakk> \<Longrightarrow> \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko ptr. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; \<exists>y. kheap s ptr = Some y\<rbrakk> \<Longrightarrow> \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> valid_obj ptr y (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> valid_obj ptr y s
 2. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> valid_obj t (TCB tcb) s
 3. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> kheap s t = Some (?ko33 ko ptr y)
 4. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> a_type (TCB tcb) = a_type (?ko33 ko ptr y) proof (prove)
goal (3 subgoals):
 1. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> valid_obj t (TCB tcb) s
 2. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> kheap s t = Some (?ko33 ko ptr y)
 3. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> a_type (TCB tcb) = a_type (?ko33 ko ptr y) proof (prove)
goal (2 subgoals):
 1. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> kheap s t = Some (?ko33 ko ptr y)
 2. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> a_type (TCB tcb) = a_type (?ko33 ko ptr y) proof (prove)
goal (1 subgoal):
 1. \<And>ko ptr y. \<lbrakk>valid_tcb t tcb s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s t = Some ko; is_tcb ko; ptr \<noteq> t; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> a_type (TCB tcb) = a_type ko proof (prove)
goal:
No subgoals!