reversed import dependency between Relation and Finite_Set; and move theorems around

--- a/NEWS	Mon Mar 20 11:13:01 2023 +0100
+++ b/NEWS	Mon Mar 20 15:01:12 2023 +0100
@@ -63,7 +63,13 @@
     Except in "[...]" maps where ":=" would create a clash with
     list update syntax "xs[i := x]".
 
+* Theory "HOL.Finite_Set"
+  - Imported Relation instead of Product_Type, Sum_Type, and Fields.
+    Minor INCOMPATIBILITY.
+
 * Theory "HOL.Relation":
+  - Imported Product_Type, Sum_Type, and Fields instead of Finite_Set.
+    Minor INCOMPATIBILITY.
   - Added predicates irrefl_on and irreflp_on and redefined irrefl and
     irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
     explicitly provided for backward compatibility but their usage is

--- a/src/HOL/Finite_Set.thy	Mon Mar 20 11:13:01 2023 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 20 15:01:12 2023 +0100
@@ -9,7 +9,7 @@
 section \<open>Finite sets\<close>
 
 theory Finite_Set
-  imports Product_Type Sum_Type Fields
+  imports Product_Type Sum_Type Fields Relation
 begin
 
 subsection \<open>Predicate for finite sets\<close>
@@ -581,6 +581,23 @@
   with assms show ?thesis by auto
 qed
 
+lemma finite_converse [iff]: "finite (r\<inverse>) \<longleftrightarrow> finite r"
+  unfolding converse_def conversep_iff
+  using [[simproc add: finite_Collect]]
+  by (auto elim: finite_imageD simp: inj_on_def)
+
+lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
+  by (induct set: finite) auto
+
+lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
+  by (induct set: finite) auto
+
+lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
+  by (simp add: Field_def finite_Domain finite_Range)
+
+lemma finite_Image[simp]: "finite R \<Longrightarrow> finite (R `` A)"
+  by(rule finite_subset[OF _ finite_Range]) auto
+
 
 subsection \<open>Further induction rules on finite sets\<close>
 
@@ -1465,6 +1482,91 @@
 
 end
 
+subsubsection \<open>Expressing relation operations via \<^const>\<open>fold\<close>\<close>
+
+lemma Id_on_fold:
+  assumes "finite A"
+  shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
+proof -
+  interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)"
+    by standard auto
+  from assms show ?thesis
+    unfolding Id_on_def by (induct A) simp_all
+qed
+
+lemma comp_fun_commute_Image_fold:
+  "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
+proof -
+  interpret comp_fun_idem Set.insert
+    by (fact comp_fun_idem_insert)
+  show ?thesis
+    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
+qed
+
+lemma Image_fold:
+  assumes "finite R"
+  shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R"
+proof -
+  interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
+    by (rule comp_fun_commute_Image_fold)
+  have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
+    by (force intro: rev_ImageI)
+  show ?thesis
+    using assms by (induct R) (auto simp: * )
+qed
+
+lemma insert_relcomp_union_fold:
+  assumes "finite S"
+  shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
+proof -
+  interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
+  proof -
+    interpret comp_fun_idem Set.insert
+      by (fact comp_fun_idem_insert)
+    show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
+      by standard (auto simp add: fun_eq_iff split: prod.split)
+  qed
+  have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}"
+    by (auto simp: relcomp_unfold intro!: exI)
+  show ?thesis
+    unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split)
+qed
+
+lemma insert_relcomp_fold:
+  assumes "finite S"
+  shows "Set.insert x R O S =
+    Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
+proof -
+  have "Set.insert x R O S = ({x} O S) \<union> (R O S)"
+    by auto
+  then show ?thesis
+    by (auto simp: insert_relcomp_union_fold [OF assms])
+qed
+
+lemma comp_fun_commute_relcomp_fold:
+  assumes "finite S"
+  shows "comp_fun_commute (\<lambda>(x,y) A.
+    Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
+proof -
+  have *: "\<And>a b A.
+    Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
+    by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
+  show ?thesis
+    by standard (auto simp: * )
+qed
+
+lemma relcomp_fold:
+  assumes "finite R" "finite S"
+  shows "R O S = Finite_Set.fold
+    (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
+proof -
+  interpret commute_relcomp_fold: comp_fun_commute
+    "(\<lambda>(x, y) A. Finite_Set.fold (\<lambda>(w, z) A'. if y = w then insert (x, z) A' else A') A S)"
+    by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>])
+  from assms show ?thesis
+    by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong)
+qed
+
 
 subsection \<open>Locales as mini-packages for fold operations\<close>
 
@@ -2260,6 +2362,20 @@
   by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
       intro: card_image[symmetric, OF subset_inj_on])
 
+lemma card_inverse[simp]: "card (R\<inverse>) = card R"
+proof -
+  have *: "\<And>R. prod.swap ` R = R\<inverse>" by auto
+  {
+    assume "\<not>finite R"
+    hence ?thesis
+      by auto
+  } moreover {
+    assume "finite R"
+    with card_image_le[of R prod.swap] card_image_le[of "R\<inverse>" prod.swap]
+    have ?thesis by (auto simp: * )
+  } ultimately show ?thesis by blast
+qed
+
 subsubsection \<open>Pigeonhole Principles\<close>
 
 lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A "

--- a/src/HOL/Relation.thy	Mon Mar 20 11:13:01 2023 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 20 15:01:12 2023 +0100
@@ -7,7 +7,7 @@
 section \<open>Relations -- as sets of pairs, and binary predicates\<close>
 
 theory Relation
-  imports Finite_Set
+  imports Product_Type Sum_Type Fields
 begin
 
 text \<open>A preliminary: classical rules for reasoning on predicates\<close>
@@ -1198,24 +1198,6 @@
 lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
   by (rule total_on_converse[to_pred])
 
-lemma finite_converse [iff]: "finite (r\<inverse>) = finite r"
-unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
-by (auto elim: finite_imageD simp: inj_on_def)
-
-lemma card_inverse[simp]: "card (R\<inverse>) = card R"
-proof -
-  have *: "\<And>R. prod.swap ` R = R\<inverse>" by auto
-  {
-    assume "\<not>finite R"
-    hence ?thesis
-      by auto
-  } moreover {
-    assume "finite R"
-    with card_image_le[of R prod.swap] card_image_le[of "R\<inverse>" prod.swap]
-    have ?thesis by (auto simp: *)
-  } ultimately show ?thesis by blast
-qed  
-
 lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)"
   by (auto simp add: fun_eq_iff)
 
@@ -1361,15 +1343,6 @@
 lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \<exists>x. P x y}"
   by auto
 
-lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
-  by (induct set: finite) auto
-
-lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
-  by (induct set: finite) auto
-
-lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
-  by (simp add: Field_def finite_Domain finite_Range)
-
 lemma Domain_mono: "r \<subseteq> s \<Longrightarrow> Domain r \<subseteq> Domain s"
   by blast
 
@@ -1480,9 +1453,6 @@
 lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
   by auto
 
-lemma finite_Image[simp]: assumes "finite R" shows "finite (R `` A)"
-by(rule finite_subset[OF _ finite_Range[OF assms]]) auto
-
 
 subsubsection \<open>Inverse image\<close>
 
@@ -1528,90 +1498,4 @@
 
 lemmas Powp_mono [mono] = Pow_mono [to_pred]
 
-
-subsubsection \<open>Expressing relation operations via \<^const>\<open>Finite_Set.fold\<close>\<close>
-
-lemma Id_on_fold:
-  assumes "finite A"
-  shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
-proof -
-  interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)"
-    by standard auto
-  from assms show ?thesis
-    unfolding Id_on_def by (induct A) simp_all
-qed
-
-lemma comp_fun_commute_Image_fold:
-  "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
-proof -
-  interpret comp_fun_idem Set.insert
-    by (fact comp_fun_idem_insert)
-  show ?thesis
-    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
-qed
-
-lemma Image_fold:
-  assumes "finite R"
-  shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R"
-proof -
-  interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
-    by (rule comp_fun_commute_Image_fold)
-  have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
-    by (force intro: rev_ImageI)
-  show ?thesis
-    using assms by (induct R) (auto simp: *)
-qed
-
-lemma insert_relcomp_union_fold:
-  assumes "finite S"
-  shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
-proof -
-  interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
-  proof -
-    interpret comp_fun_idem Set.insert
-      by (fact comp_fun_idem_insert)
-    show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
-      by standard (auto simp add: fun_eq_iff split: prod.split)
-  qed
-  have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}"
-    by (auto simp: relcomp_unfold intro!: exI)
-  show ?thesis
-    unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split)
-qed
-
-lemma insert_relcomp_fold:
-  assumes "finite S"
-  shows "Set.insert x R O S =
-    Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
-proof -
-  have "Set.insert x R O S = ({x} O S) \<union> (R O S)"
-    by auto
-  then show ?thesis
-    by (auto simp: insert_relcomp_union_fold [OF assms])
-qed
-
-lemma comp_fun_commute_relcomp_fold:
-  assumes "finite S"
-  shows "comp_fun_commute (\<lambda>(x,y) A.
-    Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
-proof -
-  have *: "\<And>a b A.
-    Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
-    by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
-  show ?thesis
-    by standard (auto simp: *)
-qed
-
-lemma relcomp_fold:
-  assumes "finite R" "finite S"
-  shows "R O S = Finite_Set.fold
-    (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
-proof -
-  interpret commute_relcomp_fold: comp_fun_commute
-    "(\<lambda>(x, y) A. Finite_Set.fold (\<lambda>(w, z) A'. if y = w then insert (x, z) A' else A') A S)"
-    by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>])
-  from assms show ?thesis
-    by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong)
-qed
-
 end

--- a/src/HOL/Transitive_Closure.thy	Mon Mar 20 11:13:01 2023 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Mar 20 15:01:12 2023 +0100
@@ -6,7 +6,7 @@
 section \<open>Reflexive and Transitive closure of a relation\<close>
 
 theory Transitive_Closure
-  imports Relation
+  imports Finite_Set
   abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*"
     and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+"
     and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="