theory CNodeInv_AI

lemma final_cap_duplicate_obj_ref:
  "\<lbrakk> fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; is_final_cap' cap1 s;
     x \<in> obj_refs cap1; p1 \<noteq> p2 \<rbrakk> \<Longrightarrow> x \<notin> obj_refs cap2" apply (clarsimp simp: is_final_cap'_def gen_obj_refs_def) apply (subgoal_tac "{p1, p2} \<subseteq> {(a, b)}") apply simp apply (drule sym[where s="Collect p" for p], simp) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; is_final_cap' cap1 s; x \<in> obj_refs cap1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> x \<notin> obj_refs cap2 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; x \<in> obj_refs cap1; p1 \<noteq> p2; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') \<noteq> {}} = {(a, b)}; x \<in> obj_refs cap2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; x \<in> obj_refs cap1; p1 \<noteq> p2; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') \<noteq> {}} = {(a, b)}; x \<in> obj_refs cap2; {p1, p2} \<subseteq> {(a, b)}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; x \<in> obj_refs cap1; p1 \<noteq> p2; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') \<noteq> {}} = {(a, b)}; x \<in> obj_refs cap2\<rbrakk> \<Longrightarrow> {p1, p2} \<subseteq> {(a, b)} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; x \<in> obj_refs cap1; p1 \<noteq> p2; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') \<noteq> {}} = {(a, b)}; x \<in> obj_refs cap2\<rbrakk> \<Longrightarrow> {p1, p2} \<subseteq> {(a, b)} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (get_cap p1 s) = {(cap1, s)}; fst (get_cap p2 s) = {(cap2, s)}; x \<in> obj_refs cap1; p1 \<noteq> p2; x \<in> obj_refs cap2; {(a, b)} = {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') \<noteq> {}}\<rbrakk> \<Longrightarrow> (cap_irqs cap1 = {} \<longrightarrow> obj_refs cap1 = {} \<longrightarrow> arch_gen_refs cap1 \<noteq> {}) \<and> (ObjRef ` obj_refs cap1 \<union> IRQRef ` cap_irqs cap1 \<union> ArchRef ` arch_gen_refs cap1) \<inter> (ObjRef ` obj_refs cap2 \<union> IRQRef ` cap_irqs cap2 \<union> ArchRef ` arch_gen_refs cap2) \<noteq> {} proof (prove)
goal:
No subgoals!