theory CSpaceInv_AI

lemma is_final_cap'_def3:
  "is_final_cap' cap = (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref s
                                \<and> (\<forall>cref'. (cte_at cref' s \<and> cref' \<noteq> cref)
                                      \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c = {}) cref' s))" apply (clarsimp simp: is_final_cap'_def2
                intro!: ext arg_cong[where f=Ex]) apply (subst iff_conv_conj_imp) apply (clarsimp simp: all_conj_distrib conj_comms) apply (rule rev_conj_cong[OF _ refl]) apply (rule arg_cong[where f=All] ext)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply fastforce done

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