# HG changeset patch
# User haftmann
# Date 1614543187 0
# Node ID 7a88313895d57696a6f4d1593f6f8a88f8d75d38
# Parent  a89f56ab26863844d640938259ebee12905eca2b
dissolve theory with duplicated name from afp

diff -r a89f56ab2686 -r 7a88313895d5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Feb 28 21:31:35 2021 +0100
+++ b/src/HOL/Fun.thy	Sun Feb 28 20:13:07 2021 +0000
@@ -468,6 +468,38 @@
   with that show thesis by blast
 qed
 
+lemma bij_iff: \<^marker>\<open>contributor \<open>Amine Chaieb\<close>\<close>
+  \<open>bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)\<close>  (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?P
+  then have \<open>inj f\<close> \<open>surj f\<close>
+    by (simp_all add: bij_def)
+  show ?Q
+  proof
+    fix y
+    from \<open>surj f\<close> obtain x where \<open>y = f x\<close>
+      by (auto simp add: surj_def)
+    with \<open>inj f\<close> show \<open>\<exists>!x. f x = y\<close>
+      by (auto simp add: inj_def)
+  qed
+next
+  assume ?Q
+  then have \<open>inj f\<close>
+    by (auto simp add: inj_def)
+  moreover have \<open>\<exists>x. y = f x\<close> for y
+  proof -
+    from \<open>?Q\<close> obtain x where \<open>f x = y\<close>
+      by blast
+    then have \<open>y = f x\<close>
+      by simp
+    then show ?thesis ..
+  qed
+  then have \<open>surj f\<close>
+    by (auto simp add: surj_def)
+  ultimately show ?P
+    by (rule bijI)
+qed
+
 lemma surj_image_vimage_eq: "surj f \<Longrightarrow> f ` (f -` A) = A"
   by simp
 
diff -r a89f56ab2686 -r 7a88313895d5 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun Feb 28 21:31:35 2021 +0100
+++ b/src/HOL/Lattices_Big.thy	Sun Feb 28 20:13:07 2021 +0000
@@ -872,6 +872,10 @@
 
 end
 
+lemma disjnt_ge_max: \<^marker>\<open>contributor \<open>Lars Hupel\<close>\<close>
+  \<open>disjnt X Y\<close> if \<open>finite Y\<close> \<open>\<And>x. x \<in> X \<Longrightarrow> x > Max Y\<close>
+  using that by (auto simp add: disjnt_def) (use Max_less_iff in blast)
+
 
 subsection \<open>Arg Min\<close>
 
diff -r a89f56ab2686 -r 7a88313895d5 src/HOL/Library/Disjoint_FSets.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Disjoint_FSets.thy	Sun Feb 28 20:13:07 2021 +0000
@@ -0,0 +1,72 @@
+(*  Title:      HOL/Library/Disjoint_FSets.thy
+    Author:     Lars Hupel, TU München
+*)
+
+section \<open>Disjoint FSets\<close>
+
+theory Disjoint_FSets
+  imports
+    "HOL-Library.Finite_Map"
+    "HOL-Library.Disjoint_Sets"
+begin
+
+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
diff -r a89f56ab2686 -r 7a88313895d5 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sun Feb 28 21:31:35 2021 +0100
+++ b/src/HOL/Library/Library.thy	Sun Feb 28 20:13:07 2021 +0000
@@ -24,6 +24,7 @@
   Diagonal_Subsequence
   Discrete
   Disjoint_Sets
+  Disjoint_FSets
   Dlist
   Dual_Ordered_Lattice
   Equipollence
diff -r a89f56ab2686 -r 7a88313895d5 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Feb 28 21:31:35 2021 +0100
+++ b/src/HOL/Set.thy	Sun Feb 28 20:13:07 2021 +0000
@@ -1949,6 +1949,10 @@
 lemma pairwise_disjnt_iff: "pairwise disjnt \<A> \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1 X. X \<in> \<A> \<and> x \<in> X)"
   by (auto simp: Uniq_def disjnt_iff pairwise_def)
 
+lemma disjnt_insert: \<^marker>\<open>contributor \<open>Lars Hupel\<close>\<close>
+  \<open>disjnt (insert x M) N\<close> if \<open>x \<notin> N\<close> \<open>disjnt M N\<close>
+  using that by (simp add: disjnt_def)
+
 lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
   by blast