theory CNodeInv_AI

lemma not_recursive_set_cap_shrinks:
  "\<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n
      \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s
      \<and> ptr \<in> fst_cte_ptrs cap\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>" apply (rule shrinks_proof[where x=ptr]) apply (rule not_recursive_cspaces_finite) apply (wp set_cap_no_new_recursive) apply simp apply (simp add: not_recursive_cspaces_def) apply (wp set_cap_cte_wp_at_neg) apply (clarsimp elim!: cte_wp_at_weakenE) apply (simp add: not_recursive_cspaces_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. finite (not_recursive_cspaces s)
 2. \<And>x. \<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace>
 3. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. ptr \<notin> not_recursive_cspaces s\<rbrace>
 4. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. x \<notin> not_recursive_cspaces s\<rbrace>
 2. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. ptr \<notin> not_recursive_cspaces s\<rbrace>
 3. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (3 subgoals):
 1. \<And>x s. x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> x \<notin> not_recursive_cspaces s \<and> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s
 2. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. ptr \<notin> not_recursive_cspaces s\<rbrace>
 3. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. ptr \<notin> not_recursive_cspaces s\<rbrace>
 2. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s\<rbrace>
 2. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (2 subgoals):
 1. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> cte_wp_at (\<lambda>_. True) ptr s \<and> (if ptr = ptr then \<not> ptr \<notin> fst_cte_ptrs cap else \<not> cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s)
 2. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>cap. ptr \<notin> fst_cte_ptrs cap) ptr s \<and> ptr \<in> fst_cte_ptrs cap \<Longrightarrow> ptr \<in> not_recursive_cspaces s proof (prove)
goal:
No subgoals!