theory CNodeInv_R

lemma cap_relation_removables:
  "\<lbrakk> cap_relation cap cap'; isNullCap cap' \<or> isZombie cap';
      s \<turnstile> cap; cte_at slot s; invs s \<rbrakk>
       \<Longrightarrow> cap_removeable cap slot = capRemovable cap' (cte_map slot)
               \<and> cap_cyclic_zombie cap slot = capCyclicZombie cap' (cte_map slot)" apply (clarsimp simp: capRemovable_def isCap_simps
                        capCyclicZombie_def cap_cyclic_zombie_def
                 split: cap_relation_split_asm arch_cap.split_asm) apply (rule iffD1 [OF conj_commute], rule context_conjI) apply (rule iffI) apply (clarsimp simp: cte_map_replicate) apply clarsimp apply (frule(1) cte_map_inj_eq [rotated, OF _ cte_at_replicate_zbits]) apply clarsimp+ apply (simp add: cte_map_replicate) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; isNullCap cap' \<or> isZombie cap'; s \<turnstile> cap; cte_wp_at (\<lambda>_. True) slot s; invs s\<rbrakk> \<Longrightarrow> cap_removeable cap slot = capRemovable cap' (cte_map slot) \<and> cap_cyclic_zombie cap slot = capCyclicZombie cap' (cte_map slot) proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) \<and> ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111) proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113\<rbrakk> \<Longrightarrow> ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)
 2. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; (x111, replicate (zombie_cte_bits x112) False) = slot\<rbrakk> \<Longrightarrow> cte_map slot = x111
 2. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; cte_map slot = x111\<rbrakk> \<Longrightarrow> (x111, replicate (zombie_cte_bits x112) False) = slot
 3. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; cte_map slot = x111\<rbrakk> \<Longrightarrow> (x111, replicate (zombie_cte_bits x112) False) = slot
 2. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (2 subgoals):
 1. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits x112) False) = slot
 2. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (6 subgoals):
 1. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> pspace_distinct s
 4. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> cte_map slot = cte_map (cte_map slot, replicate (zombie_cte_bits x112) False)
 5. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113; slot = (cte_map slot, replicate (zombie_cte_bits x112) False)\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits x112) False) = slot
 6. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (3 subgoals):
 1. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113\<rbrakk> \<Longrightarrow> cte_map slot = cte_map (cte_map slot, replicate (zombie_cte_bits x112) False)
 2. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113; slot = (cte_map slot, replicate (zombie_cte_bits x112) False)\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits x112) False) = slot
 3. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (2 subgoals):
 1. \<And>x112 x113. \<lbrakk>s \<turnstile> cap.Zombie (cte_map slot) x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie (cte_map slot) x112 x113; cap' = capability.Zombie (cte_map slot) (zbits_map x112) x113; slot = (cte_map slot, replicate (zombie_cte_bits x112) False)\<rbrakk> \<Longrightarrow> (cte_map slot, replicate (zombie_cte_bits x112) False) = slot
 2. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113. \<lbrakk>s \<turnstile> cap.Zombie x111 x112 x113; cte_wp_at (\<lambda>_. True) slot s; invs s; cap = cap.Zombie x111 x112 x113; cap' = capability.Zombie x111 (zbits_map x112) x113; ((x111, replicate (zombie_cte_bits x112) False) = slot) = (cte_map slot = x111)\<rbrakk> \<Longrightarrow> (x113 = 0 \<or> x113 = Suc 0 \<and> (x111, replicate (zombie_cte_bits x112) False) = slot) = (x113 = 0 \<or> x113 = Suc 0 \<and> cte_map slot = x111) proof (prove)
goal:
No subgoals!