diff -r ea509b0bfc80 -r 93531ba2c784 src/HOL/Finite_Set.thy
--- 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 "