theory CNodeInv_R

lemma distinct_zombies_switchE:
  "\<lbrakk> distinct_zombies m; m x = Some old_x; m y = Some old_y;
             capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y);
             capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x) \<rbrakk>
       \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y))" apply (cases "x = y") apply clarsimp apply (erule(1) distinct_zombies_sameMasterE) apply simp apply (drule_tac F="\<lambda>cap. (isUntypedCap cap, isZombie cap, isArchPageCap cap,
                             capClass cap, capUntypedPtr cap, capBits cap)"
               in master_eqE,
         simp add: isCap_Master capClass_Master capUntyped_Master capBits_Master)+ apply (simp add: distinct_zombies_def distinct_zombie_caps_def
                    split del: if_split) apply (intro allI) apply (drule_tac x="(id (x := y, y := x)) ptr" in spec) apply (drule_tac x="(id (x := y, y := x)) ptr'" in spec) apply (clarsimp split del: if_split) apply (clarsimp simp: isCap_Master
                        capBits_Master
                        capClass_Master
                        capUntyped_Master
                  split: if_split_asm ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x)\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x); x = y\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y))
 2. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x); x \<noteq> y\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct_zombies m; old_y = old_x; m y = Some old_x; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_x); capMasterCap (cteCap new_y) = capMasterCap (cteCap new_x); x = y\<rbrakk> \<Longrightarrow> distinct_zombies (m(y \<mapsto> new_y))
 2. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x); x \<noteq> y\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>old_y = old_x; m y = Some old_x; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_x); capMasterCap (cteCap new_y) = capMasterCap (cteCap new_x); x = y; capClass (cteCap new_y) = PhysicalClass\<rbrakk> \<Longrightarrow> capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y)
 2. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x); x \<noteq> y\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; capMasterCap (cteCap old_x) = capMasterCap (cteCap new_y); capMasterCap (cteCap old_y) = capMasterCap (cteCap new_x); x \<noteq> y\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some old_x; m y = Some old_y; x \<noteq> y; (isUntypedCap (cteCap old_x), isZombie (cteCap old_x), isArchPageCap (cteCap old_x), capClass (cteCap old_x), global.capUntypedPtr (cteCap old_x), capBits (cteCap old_x)) = (isUntypedCap (cteCap new_y), isZombie (cteCap new_y), isArchPageCap (cteCap new_y), capClass (cteCap new_y), global.capUntypedPtr (cteCap new_y), capBits (cteCap new_y)); (isUntypedCap (cteCap old_y), isZombie (cteCap old_y), isArchPageCap (cteCap old_y), capClass (cteCap old_y), global.capUntypedPtr (cteCap old_y), capBits (cteCap old_y)) = (isUntypedCap (cteCap new_x), isZombie (cteCap new_x), isArchPageCap (cteCap new_x), capClass (cteCap new_x), global.capUntypedPtr (cteCap new_x), capBits (cteCap new_x))\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> new_x, y \<mapsto> new_y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr ptr' cap cap'. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; m x = Some old_x; m y = Some old_y; x \<noteq> y; isUntypedCap (cteCap old_x) = isUntypedCap (cteCap new_y) \<and> isZombie (cteCap old_x) = isZombie (cteCap new_y) \<and> isArchPageCap (cteCap old_x) = isArchPageCap (cteCap new_y) \<and> capClass (cteCap old_x) = capClass (cteCap new_y) \<and> global.capUntypedPtr (cteCap old_x) = global.capUntypedPtr (cteCap new_y) \<and> capBits (cteCap old_x) = capBits (cteCap new_y); isUntypedCap (cteCap old_y) = isUntypedCap (cteCap new_x) \<and> isZombie (cteCap old_y) = isZombie (cteCap new_x) \<and> isArchPageCap (cteCap old_y) = isArchPageCap (cteCap new_x) \<and> capClass (cteCap old_y) = capClass (cteCap new_x) \<and> global.capUntypedPtr (cteCap old_y) = global.capUntypedPtr (cteCap new_x) \<and> capBits (cteCap old_y) = capBits (cteCap new_x)\<rbrakk> \<Longrightarrow> \<forall>ptr ptr' cap cap'. (if ptr = y then Some (cteCap new_y) else if ptr = x then Some (cteCap new_x) else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = y then Some (cteCap new_y) else if ptr' = x then Some (cteCap new_x) else map_option cteCap (m ptr')) = Some cap' \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' cap cap'. \<lbrakk>\<forall>ptr ptr' cap cap'. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; m x = Some old_x; m y = Some old_y; x \<noteq> y; isUntypedCap (cteCap old_x) = isUntypedCap (cteCap new_y) \<and> isZombie (cteCap old_x) = isZombie (cteCap new_y) \<and> isArchPageCap (cteCap old_x) = isArchPageCap (cteCap new_y) \<and> capClass (cteCap old_x) = capClass (cteCap new_y) \<and> global.capUntypedPtr (cteCap old_x) = global.capUntypedPtr (cteCap new_y) \<and> capBits (cteCap old_x) = capBits (cteCap new_y); isUntypedCap (cteCap old_y) = isUntypedCap (cteCap new_x) \<and> isZombie (cteCap old_y) = isZombie (cteCap new_x) \<and> isArchPageCap (cteCap old_y) = isArchPageCap (cteCap new_x) \<and> capClass (cteCap old_y) = capClass (cteCap new_x) \<and> global.capUntypedPtr (cteCap old_y) = global.capUntypedPtr (cteCap new_x) \<and> capBits (cteCap old_y) = capBits (cteCap new_x)\<rbrakk> \<Longrightarrow> (if ptr = y then Some (cteCap new_y) else if ptr = x then Some (cteCap new_x) else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = y then Some (cteCap new_y) else if ptr' = x then Some (cteCap new_x) else map_option cteCap (m ptr')) = Some cap' \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' cap cap'. \<lbrakk>m x = Some old_x; m y = Some old_y; x \<noteq> y; isUntypedCap (cteCap old_x) = isUntypedCap (cteCap new_y) \<and> isZombie (cteCap old_x) = isZombie (cteCap new_y) \<and> isArchPageCap (cteCap old_x) = isArchPageCap (cteCap new_y) \<and> capClass (cteCap old_x) = capClass (cteCap new_y) \<and> global.capUntypedPtr (cteCap old_x) = global.capUntypedPtr (cteCap new_y) \<and> capBits (cteCap old_x) = capBits (cteCap new_y); isUntypedCap (cteCap old_y) = isUntypedCap (cteCap new_x) \<and> isZombie (cteCap old_y) = isZombie (cteCap new_x) \<and> isArchPageCap (cteCap old_y) = isArchPageCap (cteCap new_x) \<and> capClass (cteCap old_y) = capClass (cteCap new_x) \<and> global.capUntypedPtr (cteCap old_y) = global.capUntypedPtr (cteCap new_x) \<and> capBits (cteCap old_y) = capBits (cteCap new_x); \<forall>ptr' cap cap'. (\<exists>z. m ((id(x := y, y := x)) ptr) = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> (id(x := y, y := x)) ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> (if ptr = y then Some (cteCap new_y) else if ptr = x then Some (cteCap new_x) else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = y then Some (cteCap new_y) else if ptr' = x then Some (cteCap new_x) else map_option cteCap (m ptr')) = Some cap' \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' cap cap'. \<lbrakk>m x = Some old_x; m y = Some old_y; x \<noteq> y; isUntypedCap (cteCap old_x) = isUntypedCap (cteCap new_y) \<and> isZombie (cteCap old_x) = isZombie (cteCap new_y) \<and> isArchPageCap (cteCap old_x) = isArchPageCap (cteCap new_y) \<and> capClass (cteCap old_x) = capClass (cteCap new_y) \<and> global.capUntypedPtr (cteCap old_x) = global.capUntypedPtr (cteCap new_y) \<and> capBits (cteCap old_x) = capBits (cteCap new_y); isUntypedCap (cteCap old_y) = isUntypedCap (cteCap new_x) \<and> isZombie (cteCap old_y) = isZombie (cteCap new_x) \<and> isArchPageCap (cteCap old_y) = isArchPageCap (cteCap new_x) \<and> capClass (cteCap old_y) = capClass (cteCap new_x) \<and> global.capUntypedPtr (cteCap old_y) = global.capUntypedPtr (cteCap new_x) \<and> capBits (cteCap old_y) = capBits (cteCap new_x); \<forall>cap cap'. (\<exists>z. m ((id(x := y, y := x)) ptr) = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ((id(x := y, y := x)) ptr') = Some z \<and> cteCap z = cap') \<and> (id(x := y, y := x)) ptr \<noteq> (id(x := y, y := x)) ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> (if ptr = y then Some (cteCap new_y) else if ptr = x then Some (cteCap new_x) else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = y then Some (cteCap new_y) else if ptr' = x then Some (cteCap new_x) else map_option cteCap (m ptr')) = Some cap' \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' cap cap'. \<lbrakk>m x = Some old_x; m y = Some old_y; x \<noteq> y; \<forall>cap cap'. (\<exists>z. m (if ptr = y then x else if ptr = x then y else ptr) = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m (if ptr' = y then x else if ptr' = x then y else ptr') = Some z \<and> cteCap z = cap') \<and> (if ptr = y then x else if ptr = x then y else ptr) \<noteq> (if ptr' = y then x else if ptr' = x then y else ptr') \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; isUntypedCap (cteCap old_x) = isUntypedCap (cteCap new_y); isUntypedCap (cteCap old_y) = isUntypedCap (cteCap new_x); isZombie (cteCap old_x) = isZombie (cteCap new_y); isZombie (cteCap old_y) = isZombie (cteCap new_x); isArchPageCap (cteCap old_x) = isArchPageCap (cteCap new_y); isArchPageCap (cteCap old_y) = isArchPageCap (cteCap new_x); capClass (cteCap old_x) = capClass (cteCap new_y); capClass (cteCap old_y) = capClass (cteCap new_x); global.capUntypedPtr (cteCap old_x) = global.capUntypedPtr (cteCap new_y); capBits (cteCap old_x) = capBits (cteCap new_y); global.capUntypedPtr (cteCap old_y) = global.capUntypedPtr (cteCap new_x); capBits (cteCap old_y) = capBits (cteCap new_x); (if ptr = y then Some (cteCap new_y) else if ptr = x then Some (cteCap new_x) else map_option cteCap (m ptr)) = Some cap; (if ptr' = y then Some (cteCap new_y) else if ptr' = x then Some (cteCap new_x) else map_option cteCap (m ptr')) = Some cap'; ptr \<noteq> ptr'; isZombie cap; capClass cap' = PhysicalClass; \<not> isUntypedCap cap'; \<not> isArchPageCap cap'; capBits cap = capBits cap'; global.capUntypedPtr cap = global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!