theory Finalise_AI

lemma suspend_final_cap:
  "\<lbrace>\<lambda>s. is_final_cap' cap s \<and> \<not> can_fast_finalise cap
            \<and> cte_wp_at ((=) cap) sl s\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv s. is_final_cap' cap s\<rbrace>" apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state
              del: split_paired_Ex split_paired_All) apply (wp suspend_caps_of_state) apply (clarsimp simp del: split_paired_Ex split_paired_All) apply (rule_tac x=sl in exI) apply (intro allI impI conjI) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (subgoal_tac "(aa, ba) = sl") apply clarsimp apply (frule_tac x="(aa, ba)" in spec) apply (drule_tac x=sl in spec) apply clarsimp done

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