theory CSpace_I

lemma distinct_zombies_unzombieE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
        isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte);
        isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte');
        isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte');
        capClass (cteCap cte') = capClass (cteCap cte);
        capBits (cteCap cte') = capBits (cteCap cte);
        capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
          \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte'))" apply (simp add: distinct_zombies_def distinct_zombie_caps_def
                     split del: if_split) apply (erule allEI, erule allEI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_zombies m; m x = Some cte; isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte)\<rbrakk> \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte')) 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 cte; isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte)\<rbrakk> \<Longrightarrow> \<forall>ptr ptr' cap cap'. (if ptr = x then Some (cteCap cte') else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = x then Some (cteCap cte') 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'. \<lbrakk>m x = Some cte; isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); capClass (cteCap cte') = capClass (cteCap cte); capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<forall>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'\<rbrakk> \<Longrightarrow> \<forall>cap cap'. (if ptr = x then Some (cteCap cte') else map_option cteCap (m ptr)) = Some cap \<and> (if ptr' = x then Some (cteCap cte') 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:
No subgoals!