Theory HOL-Library.Disjoint_FSets

(*  Author:     Lars Hupel, TU München
*)

section ‹Disjoint FSets›

theory Disjoint_FSets
  imports
    "HOL-Library.Finite_Map"
    Disjoint_Sets
begin

context
  includes fset.lifting
begin

lift_definition fdisjnt :: "'a fset ⇒ 'a fset ⇒ bool" is disjnt .

lemma fdisjnt_alt_def: "fdisjnt M N ⟷ (M |∩| N = {||})"
by transfer (simp add: disjnt_def)

lemma fdisjnt_insert: "x |∉| N ⟹ fdisjnt M N ⟹ fdisjnt (finsert x M) N"
by transfer' (rule disjnt_insert)

lemma fdisjnt_subset_right: "N' |⊆| N ⟹ fdisjnt M N ⟹ fdisjnt M N'"
unfolding fdisjnt_alt_def by auto

lemma fdisjnt_subset_left: "N' |⊆| N ⟹ fdisjnt N M ⟹ fdisjnt N' M"
unfolding fdisjnt_alt_def by auto

lemma fdisjnt_union_right: "fdisjnt M A ⟹ fdisjnt M B ⟹ fdisjnt M (A |∪| B)"
unfolding fdisjnt_alt_def by auto

lemma fdisjnt_union_left: "fdisjnt A M ⟹ fdisjnt B M ⟹ fdisjnt (A |∪| B) M"
unfolding fdisjnt_alt_def by auto

lemma fdisjnt_swap: "fdisjnt M N ⟹ fdisjnt N M"
including fset.lifting by transfer' (auto simp: disjnt_def)

lemma distinct_append_fset:
  assumes "distinct xs" "distinct ys" "fdisjnt (fset_of_list xs) (fset_of_list ys)"
  shows "distinct (xs @ ys)"
using assms
by transfer' (simp add: disjnt_def)

lemma fdisjnt_contrI:
  assumes "⋀x. x |∈| M ⟹ x |∈| N ⟹ False"
  shows "fdisjnt M N"
using assms
by transfer' (auto simp: disjnt_def)

lemma fdisjnt_Union_left: "fdisjnt (ffUnion S) T ⟷ fBall S (λS. fdisjnt S T)"
by transfer' (auto simp: disjnt_def)

lemma fdisjnt_Union_right: "fdisjnt T (ffUnion S) ⟷ fBall S (λS. fdisjnt T S)"
by transfer' (auto simp: disjnt_def)

lemma fdisjnt_ge_max: "fBall X (λx. x > fMax Y) ⟹ fdisjnt X Y"
by transfer (auto intro: disjnt_ge_max)

end

(* FIXME should be provable without lifting *)
lemma fmadd_disjnt: "fdisjnt (fmdom m) (fmdom n) ⟹ m ++⇩f n = n ++⇩f m"
unfolding fdisjnt_alt_def
including fset.lifting fmap.lifting
apply transfer
apply (rule ext)
apply (auto simp: map_add_def split: option.splits)
done

end