theory Finalise_R

lemma distinct_zombies_n[simp]:
  "distinct_zombies n" using distinct_zombies_m apply (simp add: n_def distinct_zombies_nonCTE_modify_map) apply (subst modify_map_apply[where p=slot]) apply (simp add: modify_map_def slot) apply simp apply (rule distinct_zombies_sameMasterE) apply (simp add: distinct_zombies_nonCTE_modify_map) apply (simp add: modify_map_def slot) apply simp 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 (modify_map (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)))) slot (cteCap_update (\<lambda>_. capability.NullCap))) proof (prove)
goal (2 subgoals):
 1. distinct_zombies m \<Longrightarrow> modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))) slot = Some ?x1
 2. distinct_zombies m \<Longrightarrow> distinct_zombies ((modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))))(slot \<mapsto> cteCap_update (\<lambda>_. capability.NullCap) ?x1)) proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies ((modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))))(slot \<mapsto> cteCap_update (\<lambda>_. capability.NullCap) (CTE s_cap s_node))) proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies ((modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))))(slot \<mapsto> CTE capability.NullCap s_node)) proof (prove)
goal (3 subgoals):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))))
 2. distinct_zombies m \<Longrightarrow> modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))) slot = Some ?cte10
 3. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE capability.NullCap s_node)) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap ?cte10) = capMasterCap (cteCap (CTE capability.NullCap s_node)) proof (prove)
goal (2 subgoals):
 1. distinct_zombies m \<Longrightarrow> modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))) slot = Some ?cte10
 2. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE capability.NullCap s_node)) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap ?cte10) = capMasterCap (cteCap (CTE capability.NullCap s_node)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; capClass (cteCap (CTE capability.NullCap s_node)) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap (CTE s_cap s_node)) = capMasterCap (cteCap (CTE capability.NullCap s_node)) proof (prove)
goal:
No subgoals!