theory Finalise_AI

lemma zombie_not_ex_cap_to:
  "\<lbrakk> cte_wp_at ((=) (cap.Zombie ptr zbits n)) slot s;
         zombies_final s \<rbrakk>
      \<Longrightarrow> \<not> ex_nonz_cap_to ptr s" apply (clarsimp simp: ex_nonz_cap_to_def ) apply (frule(1) zombies_finalD3[where P="(=) c" and P'="\<lambda>c. x \<in> S c" for c x S]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply assumption apply (rule notI, drule_tac a=ptr in equals0D) apply (clarsimp simp add: zobj_refs_to_obj_refs) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s\<rbrakk> \<Longrightarrow> \<not> ex_nonz_cap_to ptr s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> slot \<noteq> (a, b)
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> zombies_final s
 3. \<And>a b cap cap'. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; Zombie ptr zbits n = cap; ptr \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}
 4. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; cte_wp_at (Not \<circ> is_zombie) slot s \<and> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> zombies_final s
 2. \<And>a b cap cap'. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; Zombie ptr zbits n = cap; ptr \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}
 3. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; cte_wp_at (Not \<circ> is_zombie) slot s \<and> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b cap cap'. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; Zombie ptr zbits n = cap; ptr \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; cte_wp_at (Not \<circ> is_zombie) slot s \<and> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b cap cap'. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; Zombie ptr zbits n = cap; ptr \<in> zobj_refs cap'; ptr \<notin> obj_refs cap \<inter> obj_refs cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; cte_wp_at (Not \<circ> is_zombie) slot s \<and> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) slot s; zombies_final s; cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s; cte_wp_at (Not \<circ> is_zombie) slot s \<and> cte_wp_at (Not \<circ> is_zombie) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!