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 ++\<^sub>f n = n ++\<^sub>f m" unfolding fdisjnt_alt_def
including fset.lifting and fmap.lifting apply transfer apply (rule ext) apply (auto simp: map_add_def split: option.splits) done
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
