theory CNodeInv_AI

lemma set_zombie_not_recursive:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (cap.Zombie p zb n)) slot s
     \<and> P (not_recursive_cspaces s)\<rbrace>
     set_cap (cap.Zombie p zb n) slot
   \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace>" apply (simp add: not_recursive_cspaces_def) apply (rule set_preserved_proof[where P=P]) apply simp_all apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_cap_cte_wp_at) apply (fastforce simp: cte_wp_at_def fst_cte_ptrs_def) apply (simp only: cte_wp_at_neg imp_conv_disj de_Morgan_conj simp_thms) apply (wp hoare_vcg_ex_lift valid_cte_at_neg_typ[OF set_cap_typ_at]
            hoare_vcg_disj_lift set_cap_cte_wp_at) apply (fastforce simp: fst_cte_ptrs_def cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> P (not_recursive_cspaces s)\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> P {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. P {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> x \<in> {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. x \<in> {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> x \<notin> {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. x \<notin> {ptr. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s \<Longrightarrow> ((\<lambda>s. if x = slot then x \<notin> fst_cte_ptrs (Zombie p zb n) else cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s) and cte_wp_at (\<lambda>_. True) slot) s
 2. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. x \<notin> fst_cte_ptrs cap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> (\<not> cte_wp_at (\<lambda>_. True) x s \<or> cte_wp_at (\<lambda>cap. x \<in> fst_cte_ptrs cap) x s)\<rbrace> set_cap (Zombie p zb n) slot \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>_. True) x s \<or> cte_wp_at (\<lambda>cap. x \<in> fst_cte_ptrs cap) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. cte_wp_at (\<lambda>c. fst_cte_ptrs c = fst_cte_ptrs (Zombie p zb n)) slot s \<and> (\<not> cte_wp_at (\<lambda>_. True) x s \<or> cte_wp_at (\<lambda>cap. x \<in> fst_cte_ptrs cap) x s) \<Longrightarrow> \<not> cte_wp_at (\<lambda>_. True) x s \<or> ((\<lambda>s. if x = slot then x \<in> fst_cte_ptrs (Zombie p zb n) else cte_wp_at (\<lambda>cap. x \<in> fst_cte_ptrs cap) x s) and cte_wp_at (\<lambda>_. True) slot) s proof (prove)
goal:
No subgoals!