theory ADT_H

lemma absEkheap_correct:
assumes pspace_relation: "pspace_relation (kheap s) (ksPSpace s')"
assumes ekheap_relation: "ekheap_relation (ekheap s) (ksPSpace s')"
assumes vetcbs: "valid_etcbs s"
shows
  "absEkheap (ksPSpace s') = ekheap s" apply (rule ext) apply (clarsimp simp: absEkheap_def split: option.splits Structures_H.kernel_object.splits) apply (subgoal_tac "\<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) =
                          (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb'))") using vetcbs ekheap_relation apply (clarsimp simp: valid_etcbs_def is_etcb_at_def dom_def ekheap_relation_def st_tcb_at_def obj_at_def) apply (erule_tac x=x in allE)+ apply (rule conjI, force) apply clarsimp apply (rule conjI, clarsimp simp: EtcbMap_def etcb_relation_def)+ apply clarsimp using pspace_relation apply (clarsimp simp add: pspace_relation_def pspace_dom_def UNION_eq
                              dom_def Collect_eq) apply (rule iffI) apply (erule_tac x=x in allE)+ apply (case_tac "ksPSpace s' x", clarsimp) apply (erule_tac x=x in allE, clarsimp) apply clarsimp apply (case_tac a, simp_all add: other_obj_relation_def) apply (insert pspace_relation) apply (clarsimp simp: obj_at'_def projectKOs) apply (erule(1) pspace_dom_relatedE) apply (erule(1) obj_relation_cutsE) apply (clarsimp simp: other_obj_relation_def
                 split: Structures_A.kernel_object.split_asm  if_split_asm
                        ARM_A.arch_kernel_obj.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absEkheap (ksPSpace s') = ekheap s proof (prove)
goal (1 subgoal):
 1. \<And>x. absEkheap (ksPSpace s') x = ekheap s x proof (prove)
goal (1 subgoal):
 1. \<And>x. (ksPSpace s' x = None \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) \<Longrightarrow> (ksPSpace s' x = None \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x))
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
using this:
valid_etcbs s
ekheap_relation (ekheap s) (ksPSpace s')

goal (2 subgoals):
 1. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) \<Longrightarrow> (ksPSpace s' x = None \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x))
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')); \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); \<forall>x. (\<exists>y. ekheap s x = Some y) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb')\<rbrakk> \<Longrightarrow> (ksPSpace s' x = None \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x))
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y); (\<exists>y. ekheap s x = Some y) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb')\<rbrakk> \<Longrightarrow> (ksPSpace s' x = None \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x))
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y); (\<exists>y. ekheap s x = Some y) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb')\<rbrakk> \<Longrightarrow> \<forall>x2. (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x)
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>(\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y); (\<exists>y. ekheap s x = Some y) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb')\<rbrakk> \<Longrightarrow> (\<forall>x1. x2 = KOEndpoint x1 \<longrightarrow> ksPSpace s' x = Some (KOEndpoint x1) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x2a. x2 = KONotification x2a \<longrightarrow> ksPSpace s' x = Some (KONotification x2a) \<longrightarrow> None = ekheap s x) \<and> (x2 = KOKernelData \<longrightarrow> ksPSpace s' x = Some KOKernelData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserData \<longrightarrow> ksPSpace s' x = Some KOUserData \<longrightarrow> None = ekheap s x) \<and> (x2 = KOUserDataDevice \<longrightarrow> ksPSpace s' x = Some KOUserDataDevice \<longrightarrow> None = ekheap s x) \<and> (\<forall>x6. x2 = KOTCB x6 \<longrightarrow> ksPSpace s' x = Some (KOTCB x6) \<longrightarrow> Some (EtcbMap x6) = ekheap s x) \<and> (\<forall>x7. x2 = KOCTE x7 \<longrightarrow> ksPSpace s' x = Some (KOCTE x7) \<longrightarrow> None = ekheap s x) \<and> (\<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x)
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>(\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y); (\<exists>y. ekheap s x = Some y) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb')\<rbrakk> \<Longrightarrow> \<forall>x8. x2 = KOArch x8 \<longrightarrow> ksPSpace s' x = Some (KOArch x8) \<longrightarrow> None = ekheap s x
 2. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. \<And>x. \<forall>x. (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)))\<rbrakk> \<Longrightarrow> (\<exists>tcb. kheap s x = Some (TCB tcb)) = (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb. kheap s x = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')
 2. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<exists>tcb. kheap s x = Some (TCB tcb); (\<exists>xa. (\<exists>y. kheap s xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) = (\<exists>y. ksPSpace s' x = Some y); (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)))\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')
 2. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb. \<lbrakk>\<forall>xa. kheap s xa = None \<or> x \<notin> fst ` obj_relation_cuts (the (kheap s xa)) xa; other_obj_relation (TCB tcb) (the None); ksPSpace s' x = None; kheap s x = Some (TCB tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. \<lbrakk>\<exists>tcb. kheap s x = Some (TCB tcb); (\<exists>xa. (\<exists>y. kheap s xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) = (\<exists>y. ksPSpace s' x = Some y); (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); ksPSpace s' x = Some a\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')
 3. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>\<exists>tcb. kheap s x = Some (TCB tcb); (\<exists>xa. (\<exists>y. kheap s xa = Some y) \<and> x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) = (\<exists>y. ksPSpace s' x = Some y); (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); ksPSpace s' x = Some a\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')
 2. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (2 subgoals):
 1. \<And>a tcb xa aa b y. \<lbrakk>other_obj_relation (TCB tcb) a; ksPSpace s' aa = Some a; kheap s aa = Some (TCB tcb); (aa, b) \<in> obj_relation_cuts y xa; kheap s xa = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb'. a = KOTCB tcb'
 2. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x tcb'. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x tcb' y ko P. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko (KOTCB tcb')\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal (5 subgoals):
 1. \<And>x tcb' y ko P sz cs z cap cte. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; P ko (KOTCB tcb'); ko = CNode sz cs; well_formed_cnode_n sz cs; x = cte_map (y, z); KOTCB tcb' = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)
 2. \<And>x tcb' y ko P pt z pte'. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; P ko (KOTCB tcb'); ko = ArchObj (PageTable pt); x = y + (UCAST(8 \<rightarrow> 32) z << 2); KOTCB tcb' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte'\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)
 3. \<And>x tcb' y ko P pd z pde'. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; P ko (KOTCB tcb'); ko = ArchObj (PageDirectory pd); x = y + (UCAST(12 \<rightarrow> 32) z << 2); KOTCB tcb' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde'\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)
 4. \<And>x tcb' y ko P sz dev n. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; P ko (KOTCB tcb'); ko = ArchObj (DataPage dev sz); KOTCB tcb' = (if dev then KOUserDataDevice else KOUserData); x = y + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)
 5. \<And>x tcb' y ko P. \<lbrakk>\<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))); pspace_relation (kheap s) (ksPSpace s'); kheap s y = Some ko; P ko (KOTCB tcb'); x = y; other_obj_relation ko (KOTCB tcb'); is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb) proof (prove)
goal:
No subgoals!