theory Untyped_R

lemma dist_z [simp]:
  "distinct_zombies n'" using dist_z_m apply (simp add: n'_def distinct_zombies_nonCTE_modify_map) apply (simp add: n_def distinct_zombies_nonCTE_modify_map
                   fun_upd_def[symmetric]) apply (erule distinct_zombies_seperateE, simp) apply (case_tac cte, clarsimp) apply (rename_tac cap node) apply (subgoal_tac "capRange cap \<inter> capRange c' \<noteq> {}") apply (frule untyped_mdbD' [OF _ _ _ _ _ untyped_mdb, OF parent]) apply (simp add: is_untyped) apply (clarsimp simp add: untypedCapRange[OF is_untyped, symmetric]) apply (drule disjoint_subset2 [OF capRange_c']) apply simp apply simp apply (simp add: descendants_of'_def) apply (drule(1) rangeD) apply simp apply (drule capAligned_capUntypedPtr [OF capAligned_c']) apply (frule valid_capAligned [OF valid_capI']) apply (drule(1) capAligned_capUntypedPtr) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_zombies n' proof (prove)
using this:
distinct_zombies m

goal (1 subgoal):
 1. distinct_zombies n' proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies n proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies (m(site \<mapsto> CTE c' (MDB (mdbNext parent_node) parent True True))) proof (prove)
goal (1 subgoal):
 1. \<And>y cte. \<lbrakk>m y = Some cte; site \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr c'; capBits (cteCap cte) = capBits c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y x1 x2. \<lbrakk>m y = Some (CTE x1 x2); site \<noteq> y; \<not> isUntypedCap x1; \<not> isArchPageCap x1; capClass x1 = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr x1 = global.capUntypedPtr c'; capBits x1 = capBits c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (5 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE parent_cap parent_node))
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap (CTE parent_cap parent_node)) \<noteq> {}
 3. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 4. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 5. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (4 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap (CTE parent_cap parent_node)) \<noteq> {}
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 3. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 4. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (4 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; capRange cap \<inter> capRange parent_cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 3. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 4. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (4 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; capRange cap \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 3. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 4. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 3. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; y \<in> descendants_of' parent m\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; m \<turnstile> parent \<rightarrow> y\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; capRange cap \<inter> capRange c' \<noteq> {}; capRange cap \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; capClass c' = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; global.capUntypedPtr c' \<in> capRange c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; global.capUntypedPtr c' \<in> capRange c'; capAligned cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>y cap node. \<lbrakk>m y = Some (CTE cap node); site \<noteq> y; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capClass cap = PhysicalClass; global.capUntypedPtr cap = global.capUntypedPtr c'; capBits cap = capBits c'; global.capUntypedPtr c' \<in> capRange c'; global.capUntypedPtr cap \<in> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' \<noteq> {} proof (prove)
goal:
No subgoals!