theory CNodeInv_AI

lemma suspend_not_recursive:
  "\<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace>
     IpcCancel_A.suspend t
   \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace>" apply (simp add: not_recursive_cspaces_def cte_wp_at_caps_of_state) apply (wp suspend_caps_of_state) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule rsubst[where P=P]) apply (intro set_eqI iffI) apply (clarsimp simp: fst_cte_ptrs_def) apply clarsimp apply (clarsimp simp: fst_cte_ptrs_def can_fast_finalise_def
                 split: cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> suspend t \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> suspend t \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap} \<Longrightarrow> (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P {ptr. \<exists>cap. ((caps_of_state s)(p \<mapsto> NullCap)) ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}) \<and> P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}; caps_of_state s (a, b) = Some cap; can_fast_finalise cap\<rbrakk> \<Longrightarrow> P {ptr. (ptr = (a, b) \<longrightarrow> (a, b) \<notin> fst_cte_ptrs NullCap) \<and> (ptr \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap))} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; can_fast_finalise cap\<rbrakk> \<Longrightarrow> {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap} = {ptr. (ptr = (a, b) \<longrightarrow> (a, b) \<notin> fst_cte_ptrs NullCap) \<and> (ptr \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap))} proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap x. \<lbrakk>caps_of_state s (a, b) = Some cap; can_fast_finalise cap; x \<in> {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrakk> \<Longrightarrow> x \<in> {ptr. (ptr = (a, b) \<longrightarrow> (a, b) \<notin> fst_cte_ptrs NullCap) \<and> (ptr \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap))}
 2. \<And>s a b cap x. \<lbrakk>caps_of_state s (a, b) = Some cap; can_fast_finalise cap; x \<in> {ptr. (ptr = (a, b) \<longrightarrow> (a, b) \<notin> fst_cte_ptrs NullCap) \<and> (ptr \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap))}\<rbrakk> \<Longrightarrow> x \<in> {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap x. \<lbrakk>caps_of_state s (a, b) = Some cap; can_fast_finalise cap; x \<in> {ptr. (ptr = (a, b) \<longrightarrow> (a, b) \<notin> fst_cte_ptrs NullCap) \<and> (ptr \<noteq> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap))}\<rbrakk> \<Longrightarrow> x \<in> {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap} proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; can_fast_finalise cap; (a, b) \<notin> fst_cte_ptrs NullCap; (a, b) \<in> fst_cte_ptrs cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!