theory Ipc_AI

lemma get_cap_zombies_helper:
  "\<lbrace>zombies_final\<rbrace>
     get_cap p
   \<lbrace>\<lambda>rv s. \<not> is_zombie rv
     \<longrightarrow> (\<forall>r\<in>obj_refs rv. \<forall>p'.
           cte_wp_at (\<lambda>c. r \<in> obj_refs c) p' s
             \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s)\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_def) apply (subgoal_tac "p \<noteq> (a, b)") apply (drule(3) zombies_finalD2) apply blast apply simp apply clarsimp done

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