theory CNodeInv_AI

lemma zombies_final_helper:
  "\<lbrakk> cte_wp_at (\<lambda>c. c = cap) p s; \<not> is_zombie cap; zombies_final s \<rbrakk>
     \<Longrightarrow> (\<forall>r\<in>obj_refs cap. \<forall>a b.
            cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s)" apply (clarsimp simp: cte_wp_at_def) apply (case_tac "p = (a, b)") apply simp apply (drule(2) zombies_finalD2) apply clarsimp apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. c = cap) p s; \<not> is_zombie cap; zombies_final s\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs cap. \<forall>a b. cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>r a b capa. \<lbrakk>fst (get_cap p s) = {(cap, s)}; \<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r a b capa. \<lbrakk>fst (get_cap p s) = {(cap, s)}; \<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p = (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>r a b capa. \<lbrakk>fst (get_cap p s) = {(cap, s)}; \<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r a b capa. \<lbrakk>fst (get_cap p s) = {(cap, s)}; \<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> zombies_final s
 2. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs capa \<noteq> {}
 3. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b); \<not> is_zombie cap \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b)\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs capa \<noteq> {}
 2. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b); \<not> is_zombie cap \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r a b capa. \<lbrakk>\<not> is_zombie cap; zombies_final s; r \<in> obj_refs cap; fst (get_cap (a, b) s) = {(capa, s)}; r \<in> obj_refs capa; is_zombie capa; p \<noteq> (a, b); \<not> is_zombie cap \<and> \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!