theory CSpace_I

lemma distinct_zombies_init:
  "\<lbrakk> distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte));
        capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte) \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (p \<mapsto> cte))" apply (erule distinct_zombies_seperateE) apply (rename_tac y cte') apply (clarsimp simp: caps_no_overlap'_def) apply (drule_tac x=y in spec)+ apply (case_tac cte') apply (rename_tac capability mdbnode) apply clarsimp apply (subgoal_tac "capRange capability \<noteq> capRange (cteCap cte)") apply (clarsimp simp: capRange_def) apply (drule(1) capAligned_capUntypedPtr)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte)); capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte)\<rbrakk> \<Longrightarrow> distinct_zombies (m(p \<mapsto> cte)) proof (prove)
goal (1 subgoal):
 1. \<And>y ctea. \<lbrakk>caps_no_overlap' m (capRange (cteCap cte)); capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte); m y = Some ctea; p \<noteq> y; \<not> isUntypedCap (cteCap ctea); \<not> isArchPageCap (cteCap ctea); capClass (cteCap ctea) = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap ctea) = global.capUntypedPtr (cteCap cte); capBits (cteCap ctea) = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte'. \<lbrakk>caps_no_overlap' m (capRange (cteCap cte)); capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte); m y = Some cte'; p \<noteq> y; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte'. \<lbrakk>\<forall>p c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange (cteCap cte) = {}; capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte); m y = Some cte'; p \<noteq> y; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte'. \<lbrakk>capAligned (cteCap cte); m y = Some cte'; p \<noteq> y; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); \<forall>c. (\<exists>n. m y = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange (cteCap cte) = {}; \<forall>cte. m y = Some cte \<longrightarrow> capAligned (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte' x1 x2. \<lbrakk>capAligned (cteCap cte); m y = Some cte'; p \<noteq> y; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); \<forall>c. (\<exists>n. m y = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange (cteCap cte) = {}; \<forall>cte. m y = Some cte \<longrightarrow> capAligned (cteCap cte); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cte' capability mdbnode. \<lbrakk>capAligned (cteCap cte); m y = Some cte'; p \<noteq> y; \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); \<forall>c. (\<exists>n. m y = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange (cteCap cte) = {}; \<forall>cte. m y = Some cte \<longrightarrow> capAligned (cteCap cte); cte' = CTE capability mdbnode\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y capability mdbnode. \<lbrakk>capAligned (cteCap cte); m y = Some (CTE capability mdbnode); p \<noteq> y; \<not> isUntypedCap capability; \<not> isArchPageCap capability; capClass capability = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr capability = global.capUntypedPtr (cteCap cte); capBits capability = capBits (cteCap cte); capRange capability \<inter> capRange (cteCap cte) = {}; capAligned capability\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y capability mdbnode. \<lbrakk>capAligned (cteCap cte); m y = Some (CTE capability mdbnode); p \<noteq> y; \<not> isUntypedCap capability; \<not> isArchPageCap capability; capClass capability = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr capability = global.capUntypedPtr (cteCap cte); capBits capability = capBits (cteCap cte); capRange capability \<inter> capRange (cteCap cte) = {}; capAligned capability; capRange capability \<noteq> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>y capability mdbnode. \<lbrakk>capAligned (cteCap cte); m y = Some (CTE capability mdbnode); p \<noteq> y; \<not> isUntypedCap capability; \<not> isArchPageCap capability; capClass capability = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr capability = global.capUntypedPtr (cteCap cte); capBits capability = capBits (cteCap cte); capRange capability \<inter> capRange (cteCap cte) = {}; capAligned capability\<rbrakk> \<Longrightarrow> capRange capability \<noteq> capRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y capability mdbnode. \<lbrakk>capAligned (cteCap cte); m y = Some (CTE capability mdbnode); p \<noteq> y; \<not> isUntypedCap capability; \<not> isArchPageCap capability; capClass capability = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr capability = global.capUntypedPtr (cteCap cte); capBits capability = capBits (cteCap cte); capRange capability \<inter> capRange (cteCap cte) = {}; capAligned capability\<rbrakk> \<Longrightarrow> capRange capability \<noteq> capRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>y capability mdbnode. \<lbrakk>m y = Some (CTE capability mdbnode); p \<noteq> y; \<not> isUntypedCap capability; \<not> isArchPageCap capability; capClass capability = PhysicalClass; capClass (cteCap cte) = PhysicalClass; global.capUntypedPtr capability = global.capUntypedPtr (cteCap cte); capBits capability = capBits (cteCap cte); capRange capability \<inter> capRange (cteCap cte) = {}; global.capUntypedPtr (cteCap cte) \<in> capRange (cteCap cte); global.capUntypedPtr capability \<in> capRange capability\<rbrakk> \<Longrightarrow> capRange capability \<noteq> capRange (cteCap cte) proof (prove)
goal:
No subgoals!