theory ArchVSpace_AI

lemma is_final_cap_caps_of_state_2D:
  "\<lbrakk> caps_of_state s p = Some cap; caps_of_state s p' = Some cap';
     is_final_cap' cap'' s; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {};
     gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {} \<rbrakk>
       \<Longrightarrow> p = p'" apply (clarsimp simp: is_final_cap'_def3) apply (frule_tac x="fst p" in spec) apply (drule_tac x="snd p" in spec) apply (drule_tac x="fst p'" in spec) apply (drule_tac x="snd p'" in spec) apply (clarsimp simp: cte_wp_at_caps_of_state Int_commute
                        prod_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; is_final_cap' cap'' s; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}; cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c \<noteq> {}) (a, b) s; \<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\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}; cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c \<noteq> {}) (a, b) s; \<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; \<forall>ba. cte_wp_at (\<lambda>_. True) (fst p, ba) s \<and> (fst p = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p, ba) s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}; cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c \<noteq> {}) (a, b) s; \<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; cte_wp_at (\<lambda>_. True) (fst p, snd p) s \<and> (fst p = a \<longrightarrow> snd p \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p, snd p) s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}; cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>_. True) (fst p, snd p) s \<and> (fst p = a \<longrightarrow> snd p \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p, snd p) s; \<forall>ba. cte_wp_at (\<lambda>_. True) (fst p', ba) s \<and> (fst p' = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p', ba) s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {}; cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>_. True) (fst p, snd p) s \<and> (fst p = a \<longrightarrow> snd p \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p, snd p) s; cte_wp_at (\<lambda>_. True) (fst p', snd p') s \<and> (fst p' = a \<longrightarrow> snd p' \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cap'' \<inter> gen_obj_refs c = {}) (fst p', snd p') s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal:
No subgoals!