theory CSpaceInv_AI

lemma set_cap_cap_to:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p'\<notin>(zobj_refs cap' - zobj_refs cap)) p s
         \<and> ex_nonz_cap_to p' s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p'\<rbrace>" apply (simp add: ex_nonz_cap_to_def cte_wp_at_caps_of_state) apply wp apply simp apply (elim conjE exE) apply (case_tac "(a, b) = p") apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. p' \<notin> zobj_refs cap' - zobj_refs cap) p s \<and> ex_nonz_cap_to p' s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. ex_nonz_cap_to p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>capa. caps_of_state s p = Some capa \<and> (p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap)) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s p = Some capa \<and> (p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap)) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap) \<Longrightarrow> \<exists>a b capa. ((caps_of_state s)(p \<mapsto> cap)) (a, b) = Some capa \<and> p' \<in> zobj_refs capa proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s p = Some capa \<and> (p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap)) \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap) \<Longrightarrow> \<exists>a b. ((a, b) = p \<longrightarrow> p' \<in> zobj_refs cap) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s p = Some capa; p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap; caps_of_state s (a, b) = Some capaa; p' \<in> zobj_refs capaa\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = p \<longrightarrow> p' \<in> zobj_refs cap) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s p = Some capa; p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap; caps_of_state s (a, b) = Some capaa; p' \<in> zobj_refs capaa; (a, b) = p\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = p \<longrightarrow> p' \<in> zobj_refs cap) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap))
 2. \<And>s capa a b capaa. \<lbrakk>caps_of_state s p = Some capa; p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap; caps_of_state s (a, b) = Some capaa; p' \<in> zobj_refs capaa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = p \<longrightarrow> p' \<in> zobj_refs cap) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s p = Some capa; p' \<in> zobj_refs capa \<longrightarrow> p' \<in> zobj_refs cap; caps_of_state s (a, b) = Some capaa; p' \<in> zobj_refs capaa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = p \<longrightarrow> p' \<in> zobj_refs cap) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> zobj_refs cap)) proof (prove)
goal:
No subgoals!