theory CSpace_R

lemma distinct_zombies[simp]:
  "distinct_zombies n'" using distinct_zombies_m apply (simp add: n'_def distinct_zombies_nonCTE_modify_map) apply (simp add: n_def modify_map_apply src dest) apply (rule distinct_zombies_sameE[rotated]) apply (simp add: src) apply simp+ apply (cases "isUntypedCap src_cap") apply (erule distinct_zombies_seperateE) apply (case_tac "y = src") apply (clarsimp simp add: src) apply (frule(3) untyped_rangefree) apply (simp add: capRange_def) apply (rule sameRegionAsE [OF sameRegion_src], simp_all) apply (erule distinct_zombies_copyMasterE, rule src) apply simp apply (simp add: notZomb) apply (simp add: notArchPage) apply (erule distinct_zombies_sameMasterE, rule dest) apply (clarsimp simp: isCap_simps) 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(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))), src \<mapsto> CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) proof (prove)
goal (8 subgoals):
 1. distinct_zombies m \<Longrightarrow> (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) src = Some ?cte8
 2. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> isZombie (cteCap ?cte8) = isZombie (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 3. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass; isUntypedCap (cteCap ?cte8)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 4. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass; isArchPageCap (cteCap ?cte8)\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 5. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = capBits (cteCap ?cte8)
 6. distinct_zombies m \<Longrightarrow> capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass \<longrightarrow> capClass (cteCap ?cte8) = PhysicalClass
 7. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = global.capUntypedPtr (cteCap ?cte8)
 8. distinct_zombies m \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> isZombie (cteCap (CTE src_cap src_node)) = isZombie (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 2. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass; isUntypedCap (cteCap (CTE src_cap src_node))\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 3. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass; isArchPageCap (cteCap (CTE src_cap src_node))\<rbrakk> \<Longrightarrow> isArchPageCap (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node)))
 4. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> capBits (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = capBits (cteCap (CTE src_cap src_node))
 5. distinct_zombies m \<Longrightarrow> capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass \<longrightarrow> capClass (cteCap (CTE src_cap src_node)) = PhysicalClass
 6. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap (CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) = global.capUntypedPtr (cteCap (CTE src_cap src_node))
 7. distinct_zombies m \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>isUntypedCap src_cap; m y = Some cte; dest \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); capBits (cteCap cte) = capBits (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (3 subgoals):
 1. \<And>y cte. \<lbrakk>isUntypedCap src_cap; m y = Some cte; dest \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); capBits (cteCap cte) = capBits (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); y = src\<rbrakk> \<Longrightarrow> False
 2. \<And>y cte. \<lbrakk>isUntypedCap src_cap; m y = Some cte; dest \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); capBits (cteCap cte) = capBits (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); y \<noteq> src\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>isUntypedCap src_cap; m y = Some cte; dest \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); capBits (cteCap cte) = capBits (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); y \<noteq> src\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (2 subgoals):
 1. \<And>y cte. \<lbrakk>isUntypedCap src_cap; m y = Some cte; dest \<noteq> y; \<not> isUntypedCap (cteCap cte); \<not> isArchPageCap (cteCap cte); capClass (cteCap cte) = PhysicalClass; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); capBits (cteCap cte) = capBits (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))); y \<noteq> src; capRange (cteCap cte) \<noteq> capRange c'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>distinct_zombies m; capMasterCap src_cap = capMasterCap c'; src_cap \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; capRange c' \<noteq> {}; capRange c' \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 3. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>capMasterCap src_cap = capMasterCap c'; src_cap \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap (CTE src_cap src_node)) = capMasterCap (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 2. \<lbrakk>capMasterCap src_cap = capMasterCap c'; src_cap \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap; isZombie (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))\<rbrakk> \<Longrightarrow> src = dest
 3. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; capRange c' \<noteq> {}; capRange c' \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 4. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>capMasterCap src_cap = capMasterCap c'; src_cap \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap; isZombie (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))\<rbrakk> \<Longrightarrow> src = dest
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; capRange c' \<noteq> {}; capRange c' \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 3. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; capRange c' \<noteq> {}; capRange c' \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))))
 2. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; \<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'\<rbrakk> \<Longrightarrow> distinct_zombies (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isUntypedCap src_cap; isIRQControlCap src_cap; isIRQHandlerCap c'; capClass (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap (CTE dest_cap dest_node)) = capMasterCap (cteCap (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))) proof (prove)
goal:
No subgoals!