theory CSpaceInv_AI

lemma final_cap_at_eq:
  "cte_wp_at (\<lambda>c. is_final_cap' c s) p s =
    (\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> (gen_obj_refs cp \<noteq> {})
       \<and> (\<forall>p'. (cte_at p' s \<and> p' \<noteq> p) \<longrightarrow>
                   cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s))" apply (clarsimp simp: is_final_cap'_def3 cte_wp_at_caps_of_state
                  simp del: split_paired_Ex split_paired_All) apply (rule iffI) apply (clarsimp simp del: split_paired_Ex split_paired_All) apply (rule conjI) apply clarsimp apply (subgoal_tac "(a, b) = p") apply (erule allEI) apply clarsimp apply (erule_tac x=p in allE) apply fastforce apply (clarsimp simp del: split_paired_Ex split_paired_All) apply (rule_tac x=p in exI) apply (clarsimp simp del: split_paired_Ex split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. is_final_cap' c s) p s = (\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. cte_wp_at (\<lambda>_. True) p' s \<and> p' \<noteq> p \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s)) proof (prove)
goal (1 subgoal):
 1. (\<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})))) = (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) proof (prove)
goal (2 subgoals):
 1. \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<Longrightarrow> \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))
 2. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))
 2. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (3 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<noteq> {}
 2. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})
 3. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})
 2. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (3 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}; (a, b) = p\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})
 2. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> (a, b) = p
 3. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (3 subgoals):
 1. \<And>cap a b capa p'. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}; (a, b) = p; (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>capa. caps_of_state s p' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})
 2. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> (a, b) = p
 3. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>cap a b capa. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s (a, b) = Some capa; gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}; (\<exists>cap. caps_of_state s p = Some cap) \<and> p \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s p = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})\<rbrakk> \<Longrightarrow> (a, b) = p
 2. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (1 subgoal):
 1. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cap. caps_of_state s p = Some cap \<and> (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>cp. \<lbrakk>caps_of_state s p = Some cp; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})\<rbrakk> \<Longrightarrow> \<exists>cref. (\<exists>cap. caps_of_state s cref = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>cp. \<lbrakk>caps_of_state s p = Some cp; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal:
No subgoals!