theory CSpace1_R

lemma pspace_relation_cte_wp_at:
  "\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
    cte_wp_at ((=) c) (cref, oref) s; pspace_aligned' s';
     pspace_distinct' s' \<rbrakk>
  \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'" apply (simp add: cte_wp_at_cases) apply (erule disjE) apply clarsimp apply (drule(1) pspace_relation_absD) apply (simp add: unpleasant_helper) apply (drule spec, drule mp, erule domI) apply (clarsimp simp: cte_relation_def) apply (drule(2) aligned_distinct_obj_atI'[where 'a=cte]) apply simp apply (drule ko_at_imp_cte_wp_at') apply (clarsimp elim!: cte_wp_at_weakenE') apply clarsimp apply (drule(1) pspace_relation_absD) apply (clarsimp simp: other_obj_relation_def) apply (simp split: kernel_object.split_asm) apply (drule(2) aligned_distinct_obj_atI'[where 'a=tcb]) apply simp apply (drule tcb_cases_related) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (erule(2) cte_wp_at_tcbI') apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cte_wp_at ((=) c) (cref, oref) s; pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); (\<exists>sz fun. kheap s cref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun oref = Some c) \<or> (\<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)); pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>sz fun. kheap s cref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun oref = Some c\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; kheap s cref = Some (CNode sz fun); well_formed_cnode_n sz fun; fun oref = Some c\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; \<forall>(x', P)\<in>obj_relation_cuts (CNode sz fun) cref. \<exists>z. ksPSpace s' x' = Some z \<and> P (CNode sz fun) z\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; \<forall>y. y \<in> dom fun \<longrightarrow> (\<exists>z. ksPSpace s' (cte_map (cref, y)) = Some z \<and> cte_relation y (CNode sz fun) z)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; \<exists>z. ksPSpace s' (cte_map (cref, oref)) = Some z \<and> cte_relation oref (CNode sz fun) z\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; ksPSpace s' (cte_map (cref, oref)) = Some (KOCTE cte); cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (3 subgoals):
 1. \<And>sz fun cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> KOCTE cte = injectKO (?v27 sz fun cte)
 2. \<And>sz fun cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; cap_relation c (cteCap cte); ko_at' (?v27 sz fun cte) (cte_map (cref, oref)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; cap_relation c (cteCap cte); ko_at' cte (cte_map (cref, oref)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; well_formed_cnode_n sz fun; fun oref = Some c; cap_relation c (cteCap cte); cte_wp_at' (\<lambda>ctea. ctea = cte) (cte_map (cref, oref)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; \<exists>tcb. kheap s cref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases oref = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; kheap s cref = Some (TCB tcb); c = get tcb; tcb_cap_cases oref = Some (get, set, restr)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); \<forall>(x', P)\<in>obj_relation_cuts (TCB tcb) cref. \<exists>z. ksPSpace s' x' = Some z \<and> P (TCB tcb) z\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr z. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); ksPSpace s' cref = Some z; case z of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr z x6. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); ksPSpace s' cref = Some (KOTCB x6); z = KOTCB x6; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>tcb get set restr z x6. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); z = KOTCB x6; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> KOTCB x6 = injectKO (?v86 tcb get set restr z x6)
 2. \<And>tcb get set restr z x6. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); z = KOTCB x6; tcb_relation tcb x6; ko_at' (?v86 tcb get set restr z x6) cref s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr z x6. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_cap_cases oref = Some (get, set, restr); z = KOTCB x6; tcb_relation tcb x6; ko_at' x6 cref s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr z x6. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; z = KOTCB x6; tcb_relation tcb x6; ko_at' x6 cref s'; \<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, oref) - x) = Some (getF', setF')) \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (get tcb) (cteCap (getF' tcb')))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (1 subgoal):
 1. \<And>tcb get x6 getF' setF'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_relation tcb x6; ksPSpace s' cref = Some (KOTCB x6); \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (get tcb) (cteCap (getF' tcb')); \<forall>x. tcb_cte_cases (cte_map (x, oref) - x) = Some (getF', setF'); is_aligned cref tcbBlockSizeBits; ps_clear cref tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation (get tcb) (cteCap cte)) (cte_map (cref, oref)) s' proof (prove)
goal (2 subgoals):
 1. \<And>tcb get x6 getF' setF'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_relation tcb x6; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (get tcb) (cteCap (getF' tcb')); \<forall>x. tcb_cte_cases (cte_map (x, oref) - x) = Some (getF', setF'); is_aligned cref tcbBlockSizeBits; ps_clear cref tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> tcb_cte_cases (cte_map (cref, oref) - cref) = Some (?getF100 tcb get x6 getF' setF', ?setF100 tcb get x6 getF' setF')
 2. \<And>tcb get x6 getF' setF'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_relation tcb x6; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (get tcb) (cteCap (getF' tcb')); \<forall>x. tcb_cte_cases (cte_map (x, oref) - x) = Some (getF', setF'); is_aligned cref tcbBlockSizeBits; ps_clear cref tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> cap_relation (get tcb) (cteCap (?getF100 tcb get x6 getF' setF' x6)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb get x6 getF' setF'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; c = get tcb; tcb_relation tcb x6; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (get tcb) (cteCap (getF' tcb')); \<forall>x. tcb_cte_cases (cte_map (x, oref) - x) = Some (getF', setF'); is_aligned cref tcbBlockSizeBits; ps_clear cref tcbBlockSizeBits s'\<rbrakk> \<Longrightarrow> cap_relation (get tcb) (cteCap (getF' x6)) proof (prove)
goal:
No subgoals!