theory CNodeInv_AI

lemma final_zombie_not_live:
  "\<lbrakk> is_final_cap' (cap.Zombie ptr b n) s; cte_wp_at ((=) (cap.Zombie ptr b n)) p s;
     if_live_then_nonz_cap s \<rbrakk>
     \<Longrightarrow> \<not> obj_at live ptr s" apply clarsimp apply (drule(1) if_live_then_nonz_capD, simp) apply (clarsimp simp: ex_nonz_cap_to_def zobj_refs_to_obj_refs) apply (subgoal_tac "(a, ba) \<noteq> p") apply (clarsimp simp: is_final_cap'_def) apply (erule(1) obvious) apply (clarsimp simp: cte_wp_at_def is_zombie_def gen_obj_refs_Int)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; if_live_then_nonz_cap s\<rbrakk> \<Longrightarrow> \<not> obj_at live ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; if_live_then_nonz_cap s; obj_at live ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a ba. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a ba. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s; (a, ba) \<noteq> p\<rbrakk> \<Longrightarrow> False
 2. \<And>a ba. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s\<rbrakk> \<Longrightarrow> (a, ba) \<noteq> p proof (prove)
goal (2 subgoals):
 1. \<And>a ba aa baa. \<lbrakk>cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s; (a, ba) \<noteq> p; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs (Zombie ptr b n) \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, baa)}\<rbrakk> \<Longrightarrow> False
 2. \<And>a ba. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s\<rbrakk> \<Longrightarrow> (a, ba) \<noteq> p proof (prove)
goal (3 subgoals):
 1. \<And>a ba aa baa. \<lbrakk>cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s; (a, ba) \<noteq> p\<rbrakk> \<Longrightarrow> (a, ba) \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs (Zombie ptr b n) \<inter> gen_obj_refs cap' \<noteq> {}}
 2. \<And>a ba aa baa. \<lbrakk>cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s; (a, ba) \<noteq> p\<rbrakk> \<Longrightarrow> p \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs (Zombie ptr b n) \<inter> gen_obj_refs cap' \<noteq> {}}
 3. \<And>a ba. \<lbrakk>is_final_cap' (Zombie ptr b n) s; cte_wp_at ((=) (Zombie ptr b n)) p s; obj_at live ptr s; cte_wp_at (\<lambda>c. ptr \<in> obj_refs c \<and> \<not> is_zombie c) (a, ba) s\<rbrakk> \<Longrightarrow> (a, ba) \<noteq> p proof (prove)
goal:
No subgoals!