theory Retype_R

lemma dist_z_n: "distinct_zombies n" using dist_z_m apply (simp add: n_def distinct_zombies_def
                   distinct_zombie_caps_def
               split del: if_split) apply (erule allEI, erule allEI) apply (clarsimp split del: if_split) apply (clarsimp split: if_split_asm simp: makeObject_cte) 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. \<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' \<Longrightarrow> \<forall>ptr ptr' cap cap'. (\<exists>z. (if P ptr then Some makeObject else m ptr) = Some z \<and> cteCap z = cap) \<and> (\<exists>z. (if P ptr' then Some makeObject else 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' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr'. \<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' \<Longrightarrow> \<forall>cap cap'. (\<exists>z. (if P ptr then Some makeObject else m ptr) = Some z \<and> cteCap z = cap) \<and> (\<exists>z. (if P ptr' then Some makeObject else 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' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' z za. \<lbrakk>\<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> 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'; (if P ptr then Some makeObject else m ptr) = Some z; ptr \<noteq> ptr'; (if P ptr' then Some makeObject else m ptr') = Some za; isZombie (cteCap z); capClass (cteCap za) = PhysicalClass; \<not> isUntypedCap (cteCap za); \<not> isArchPageCap (cteCap za); capBits (cteCap z) = capBits (cteCap za); global.capUntypedPtr (cteCap z) = global.capUntypedPtr (cteCap za)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' za. \<lbrakk>isZombie capability.NullCap; capClass (cteCap za) = PhysicalClass; \<not> isUntypedCap (cteCap za); \<not> isArchPageCap (cteCap za); capBits (cteCap za) = 0; global.capUntypedPtr capability.NullCap = global.capUntypedPtr (cteCap za); \<forall>cap. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> isZombie cap \<and> capBits cap = 0 \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr (cteCap za); P ptr; ptr \<noteq> ptr'; \<not> P ptr'; m ptr' = Some za\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!