theory CSpaceInv_AI

lemma set_cap_zombies':
  "\<lbrace>\<lambda>s. zombies_final s
         \<and> cte_wp_at (\<lambda>cap'. \<forall>p' cap''. (cte_wp_at ((=) cap'') p' s \<and> p \<noteq> p'
                            \<and> (obj_refs cap \<inter> obj_refs cap'' \<noteq> {})
                             \<longrightarrow> (\<not> is_zombie cap \<and> \<not> is_zombie cap''))) p s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: zombies_final_def2 cte_wp_at_caps_of_state) apply (rule hoare_pre, wp) apply clarsimp apply (metis Int_commute prod.inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>p' cap''. cte_wp_at ((=) cap'') p' s \<and> p \<noteq> p' \<and> obj_refs cap \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'') p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>a b aa ba cap cap'. caps_of_state s (a, b) = Some cap \<and> caps_of_state s (aa, ba) = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') \<and> (\<exists>cap. caps_of_state s p = Some cap) \<and> (\<forall>a b cap''. caps_of_state s (a, b) = Some cap'' \<and> p \<noteq> (a, b) \<and> obj_refs cap \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'')\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<forall>a b aa ba cap cap'. caps_of_state s (a, b) = Some cap \<and> caps_of_state s (aa, ba) = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b aa ba cap cap'. caps_of_state s (a, b) = Some cap \<and> caps_of_state s (aa, ba) = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') \<and> (\<exists>cap. caps_of_state s p = Some cap) \<and> (\<forall>a b cap''. caps_of_state s (a, b) = Some cap'' \<and> p \<noteq> (a, b) \<and> obj_refs cap \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'') \<Longrightarrow> \<forall>a b aa ba capa cap'. ((caps_of_state s)(p \<mapsto> cap)) (a, b) = Some capa \<and> ((caps_of_state s)(p \<mapsto> cap)) (aa, ba) = Some cap' \<and> obj_refs capa \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa. \<lbrakk>\<forall>a b aa ba cap cap'. caps_of_state s (a, b) = Some cap \<and> caps_of_state s (aa, ba) = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; \<forall>a b cap''. caps_of_state s (a, b) = Some cap'' \<and> p \<noteq> (a, b) \<and> obj_refs cap \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap''; caps_of_state s p = Some capa\<rbrakk> \<Longrightarrow> ((a, b) = p \<longrightarrow> (\<forall>aa ba. ((aa, ba) = p \<longrightarrow> obj_refs cap \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap) \<and> ((aa, ba) \<noteq> p \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap')))) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<forall>aa ba. (aa, ba) = p \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa \<inter> obj_refs cap \<noteq> {} \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap))) proof (prove)
goal:
No subgoals!