theory Finalise_AI

lemma cap_delete_one_final_cap:
  "\<lbrace>\<lambda>s. cte_wp_at ((=) cap) slot s
        \<and> \<not> can_fast_finalise cap
        \<and> is_final_cap' cap s\<rbrace>
     cap_delete_one slot'
   \<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_All split_paired_Ex) apply (wp cap_delete_one_caps_of_state) apply (clarsimp simp: cte_wp_at_caps_of_state
              simp del: split_paired_Ex split_paired_All) apply (subgoal_tac "slot = (a, b)") apply (rule_tac x=slot in exI) apply clarsimp apply (frule_tac x=slot in spec) apply (drule_tac x="(a, b)" in spec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at ((=) cap) slot s \<and> \<not> can_fast_finalise cap \<and> is_final_cap' cap s\<rbrace> cap_delete_one slot' \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_of_state s slot = Some cap \<and> \<not> can_fast_finalise cap \<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))\<rbrace> cap_delete_one slot' \<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. caps_of_state s slot = Some cap \<and> \<not> can_fast_finalise cap \<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)) \<Longrightarrow> cte_wp_at can_fast_finalise slot' s \<longrightarrow> (\<exists>cref. \<forall>cref'. (\<exists>capa. ((caps_of_state s)(slot' \<mapsto> NullCap)) 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 capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> \<exists>cref. \<forall>cref'. (cref' = slot' \<longrightarrow> slot' \<noteq> cref) \<and> (cref' \<noteq> slot' \<longrightarrow> (cref' = (a, b)) = (cref' = cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>cref. \<forall>cref'. (cref' = slot' \<longrightarrow> slot' \<noteq> cref) \<and> (cref' \<noteq> slot' \<longrightarrow> (cref' = (a, b)) = (cref' = cref))
 2. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> slot = (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa; slot = (a, b)\<rbrakk> \<Longrightarrow> \<forall>cref'. (cref' = slot' \<longrightarrow> slot' \<noteq> slot) \<and> (cref' \<noteq> slot' \<longrightarrow> (cref' = (a, b)) = (cref' = slot))
 2. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> slot = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> slot = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; \<forall>cref'. (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (cref' = (a, b)); caps_of_state s slot' = Some capa; can_fast_finalise capa; (\<exists>capa. caps_of_state s slot = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (slot = (a, b))\<rbrakk> \<Longrightarrow> slot = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s slot = Some cap; \<not> can_fast_finalise cap; caps_of_state s slot' = Some capa; can_fast_finalise capa; (\<exists>capa. caps_of_state s slot = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (slot = (a, b)); (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = ((a, b) = (a, b))\<rbrakk> \<Longrightarrow> slot = (a, b) proof (prove)
goal:
No subgoals!