Theory UnionFind

theory UnionFind
imports Main
    "Collections.Partial_Equivalence_Relation"
begin



section "firstpart of SeprefUF"

  type_synonym 'a per = "('a×'a) set"


  definition "per_init D ≡ {(i,i) | i. i∈D}"
  definition [simp]: "per_compare R a b ≡ (a,b)∈R"

  definition per_init' :: "nat ⇒ nat per" where "per_init' n ≡ {(i,i) |i. i<n}"

  lemma per_init_of_nat_range: "per_init {i. i<N} = per_init' N"
    by (auto simp: per_init_def per_init'_def)

  lemma per_init_per[simp, intro!]:
    "part_equiv (per_init D)"
    unfolding per_init_def
    by (auto simp: part_equiv_def sym_def trans_def)

  lemma per_init_self: "(a,b)∈per_init D ⟹ a=b"
    unfolding per_init_def by simp

  lemma per_union_impl: "(i,j)∈R ⟹ (i,j)∈per_union R a b"
    by (auto simp: per_union_def)

  lemma per_union_related:
    "part_equiv R ⟹ a∈Domain R ⟹ b∈Domain  R ⟹ (a,b)∈per_union R a b"
    unfolding per_union_def
    by (auto simp: part_equiv_refl)

  lemma part_equiv_refl':
    "part_equiv R ⟹ x∈Domain R ⟹ (x,x)∈R"
    using part_equiv_refl[of R x] by blast


  definition per_supset_rel :: "('a per × 'a per) set" where
    "per_supset_rel
      ≡ {(p1,p2). p1 ∩ Domain p2 × Domain p2 = p2 ∧ p1 - (Domain p2 × Domain p2) ⊆ Id}"

  lemma per_supset_rel_dom: "(p1, p2) ∈ per_supset_rel ⟹ Domain p1 ⊇ Domain p2"
    by (auto simp: per_supset_rel_def)
  
  lemma per_supset_compare:
    "(p1, p2) ∈ per_supset_rel ⟹ x1∈Domain p2 ⟹ x2∈Domain p2 ⟹ per_compare p1 x1 x2 ⟷ per_compare p2 x1 x2"
    by (auto simp: per_supset_rel_def)
  
  lemma per_supset_union: "(p1, p2) ∈ per_supset_rel ⟹ x1∈Domain p2 ⟹ x2∈Domain p2 ⟹
    (per_union p1 x1 x2, per_union p2 x1 x2) ∈ per_supset_rel"
    apply (clarsimp simp: per_supset_rel_def per_union_def Domain_unfold )
    apply (intro subsetI conjI)
    apply blast
    apply force
    done



end