Commit 474d6dd9 authored by haftmann's avatar haftmann

dissolve theory with duplicated name from afp

parent 59274460849c
theory Disjoint_Sets
imports
"HOL-Library.Finite_Map"
begin
lemma disjnt_insert: "x \<notin> N \<Longrightarrow> disjnt M N \<Longrightarrow> disjnt (insert x M) N"
unfolding disjnt_def by simp
lemma disjnt_ge_max:
assumes "finite Y" "\<And>x. x \<in> X \<Longrightarrow> x > Max Y"
shows "disjnt X Y"
unfolding disjnt_def
by (meson Int_emptyI Max.coboundedI assms(1) assms(2) leD)
context
includes fset.lifting
begin
lift_definition fdisjnt :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is disjnt .
lemma fdisjnt_alt_def: "fdisjnt M N \<longleftrightarrow> (M |\<inter>| N = {||})"
by transfer (simp add: disjnt_def)
lemma fdisjnt_insert: "x |\<notin>| N \<Longrightarrow> fdisjnt M N \<Longrightarrow> fdisjnt (finsert x M) N"
by transfer' (rule disjnt_insert)
lemma fdisjnt_subset_right: "N' |\<subseteq>| N \<Longrightarrow> fdisjnt M N \<Longrightarrow> fdisjnt M N'"
unfolding fdisjnt_alt_def by auto
lemma fdisjnt_subset_left: "N' |\<subseteq>| N \<Longrightarrow> fdisjnt N M \<Longrightarrow> fdisjnt N' M"
unfolding fdisjnt_alt_def by auto
lemma fdisjnt_union_right: "fdisjnt M A \<Longrightarrow> fdisjnt M B \<Longrightarrow> fdisjnt M (A |\<union>| B)"
unfolding fdisjnt_alt_def by auto
lemma fdisjnt_union_left: "fdisjnt A M \<Longrightarrow> fdisjnt B M \<Longrightarrow> fdisjnt (A |\<union>| B) M"
unfolding fdisjnt_alt_def by auto
lemma fdisjnt_swap: "fdisjnt M N \<Longrightarrow> 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 "\<And>x. x |\<in>| M \<Longrightarrow> x |\<in>| N \<Longrightarrow> False"
shows "fdisjnt M N"
using assms
by transfer' (auto simp: disjnt_def)
lemma fdisjnt_Union_left: "fdisjnt (ffUnion S) T \<longleftrightarrow> fBall S (\<lambda>S. fdisjnt S T)"
by transfer' (auto simp: disjnt_def)
lemma fdisjnt_Union_right: "fdisjnt T (ffUnion S) \<longleftrightarrow> fBall S (\<lambda>S. fdisjnt T S)"
by transfer' (auto simp: disjnt_def)
lemma fdisjnt_ge_max: "fBall X (\<lambda>x. x > fMax Y) \<Longrightarrow> 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) \<Longrightarrow> m ++\<^sub>f n = n ++\<^sub>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
\ No newline at end of file
......@@ -9,7 +9,6 @@ session Higher_Order_Terms (AFP) = HOL +
"HOL-ex"
theories [document = false]
Term_Utils
Disjoint_Sets
Find_First
theories
Name
......
......@@ -5,7 +5,7 @@ imports
Datatype_Order_Generator.Order_Generator
Name
Term_Utils
Disjoint_Sets
"HOL-Library.Disjoint_FSets"
begin
hide_type (open) "term"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment