# HG changeset patch
# User haftmann
# Date 1641883682 0
# Node ID 4d77dd3019d1237345e8b5ca9f2324a01babc2c9
# Parent  1f30aa91f496e9e15c95d33babb19d251bdedbd2
earlier availability of lifting

diff -r 1f30aa91f496 -r 4d77dd3019d1 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Equiv_Relations.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -5,7 +5,7 @@
 section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
 
 theory Equiv_Relations
-  imports Groups_Big
+  imports BNF_Least_Fixpoint
 begin
 
 subsection \<open>Equivalence relations -- set version\<close>
@@ -348,60 +348,6 @@
     by (auto simp: Union_quotient dest: quotient_disj)
 qed (use assms in blast)
 
-lemma card_quotient_disjoint:
-  assumes "finite A" "inj_on (\<lambda>x. {x} // r) A"
-  shows "card (A//r) = card A"
-proof -
-  have "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> r `` {j} \<noteq> r `` {i}"
-    using assms by (fastforce simp add: quotient_def inj_on_def)
-  with assms show ?thesis
-    by (simp add: quotient_def card_UN_disjoint)
-qed
-
-text \<open>By Jakub Kądziołka:\<close>
-
-lemma sum_fun_comp:
-  assumes "finite S" "finite R" "g ` S \<subseteq> R"
-  shows "(\<Sum>x \<in> S. f (g x)) = (\<Sum>y \<in> R. of_nat (card {x \<in> S. g x = y}) * f y)"
-proof -
-  let ?r = "relation_of (\<lambda>p q. g p = g q) S"
-  have eqv: "equiv S ?r"
-    unfolding relation_of_def by (auto intro: comp_equivI)
-  have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C
-    by (fact finite_equiv_class[OF \<open>finite S\<close> equiv_type[OF \<open>equiv S ?r\<close>]])
-  have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B
-    using eqv quotient_disj by blast
-
-  let ?cls = "\<lambda>y. {x \<in> S. y = g x}"
-  have quot_as_img: "S//?r = ?cls ` g ` S"
-    by (auto simp add: relation_of_def quotient_def)
-  have cls_inj: "inj_on ?cls (g ` S)"
-    by (auto intro: inj_onI)
-
-  have rest_0: "(\<Sum>y \<in> R - g ` S. of_nat (card (?cls y)) * f y) = 0"
-  proof -
-    have "of_nat (card (?cls y)) * f y = 0" if asm: "y \<in> R - g ` S" for y
-    proof -
-      from asm have *: "?cls y = {}" by auto
-      show ?thesis unfolding * by simp
-    qed
-    thus ?thesis by simp
-  qed
-
-  have "(\<Sum>x \<in> S. f (g x)) = (\<Sum>C \<in> S//?r. \<Sum>x \<in> C. f (g x))"
-    using eqv finite disjoint
-    by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient)
-  also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f (g x))"
-    unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj])
-  also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f y)"
-    by auto
-  also have "... = (\<Sum>y \<in> g ` S. of_nat (card (?cls y)) * f y)"
-    by (simp flip: sum_constant)
-  also have "... = (\<Sum>y \<in> R. of_nat (card (?cls y)) * f y)"
-    using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>])
-  finally show ?thesis
-    by (simp add: eq_commute)
-qed
 
 subsection \<open>Projection\<close>
 
diff -r 1f30aa91f496 -r 4d77dd3019d1 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Groups_Big.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -8,7 +8,7 @@
 section \<open>Big sum and product over finite (non-empty) sets\<close>
 
 theory Groups_Big
-  imports Power
+  imports Power Equiv_Relations
 begin
 
 subsection \<open>Generic monoid operation over a set\<close>
@@ -1259,6 +1259,16 @@
     using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) 
 qed auto
 
+lemma card_quotient_disjoint:
+  assumes "finite A" "inj_on (\<lambda>x. {x} // r) A"
+  shows "card (A//r) = card A"
+proof -
+  have "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> r `` {j} \<noteq> r `` {i}"
+    using assms by (fastforce simp add: quotient_def inj_on_def)
+  with assms show ?thesis
+    by (simp add: quotient_def card_UN_disjoint)
+qed
+
 lemma sum_multicount_gen:
   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t"
@@ -1303,6 +1313,52 @@
   qed
 qed simp
 
+text \<open>By Jakub Kądziołka:\<close>
+
+lemma sum_fun_comp:
+  assumes "finite S" "finite R" "g ` S \<subseteq> R"
+  shows "(\<Sum>x \<in> S. f (g x)) = (\<Sum>y \<in> R. of_nat (card {x \<in> S. g x = y}) * f y)"
+proof -
+  let ?r = "relation_of (\<lambda>p q. g p = g q) S"
+  have eqv: "equiv S ?r"
+    unfolding relation_of_def by (auto intro: comp_equivI)
+  have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C
+    by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]])
+  have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B
+    using eqv quotient_disj by blast
+
+  let ?cls = "\<lambda>y. {x \<in> S. y = g x}"
+  have quot_as_img: "S//?r = ?cls ` g ` S"
+    by (auto simp add: relation_of_def quotient_def)
+  have cls_inj: "inj_on ?cls (g ` S)"
+    by (auto intro: inj_onI)
+
+  have rest_0: "(\<Sum>y \<in> R - g ` S. of_nat (card (?cls y)) * f y) = 0"
+  proof -
+    have "of_nat (card (?cls y)) * f y = 0" if asm: "y \<in> R - g ` S" for y
+    proof -
+      from asm have *: "?cls y = {}" by auto
+      show ?thesis unfolding * by simp
+    qed
+    thus ?thesis by simp
+  qed
+
+  have "(\<Sum>x \<in> S. f (g x)) = (\<Sum>C \<in> S//?r. \<Sum>x \<in> C. f (g x))"
+    using eqv finite disjoint
+    by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient)
+  also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f (g x))"
+    unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj])
+  also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f y)"
+    by auto
+  also have "... = (\<Sum>y \<in> g ` S. of_nat (card (?cls y)) * f y)"
+    by (simp flip: sum_constant)
+  also have "... = (\<Sum>y \<in> R. of_nat (card (?cls y)) * f y)"
+    using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>])
+  finally show ?thesis
+    by (simp add: eq_commute)
+qed
+
+
 
 subsubsection \<open>Cardinality of products\<close>
 
diff -r 1f30aa91f496 -r 4d77dd3019d1 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Int.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -6,7 +6,7 @@
 section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
 
 theory Int
-  imports Equiv_Relations Power Quotient Fun_Def
+  imports Quotient Groups_Big Fun_Def
 begin
 
 subsection \<open>Definition of integers as a quotient type\<close>
diff -r 1f30aa91f496 -r 4d77dd3019d1 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Lattices_Big.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -6,7 +6,7 @@
 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
 
 theory Lattices_Big
-  imports Option
+  imports Groups_Big Option
 begin
 
 subsection \<open>Generic lattice operations over a set\<close>
diff -r 1f30aa91f496 -r 4d77dd3019d1 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Lifting_Set.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -5,7 +5,7 @@
 section \<open>Setup for Lifting/Transfer for the set type\<close>
 
 theory Lifting_Set
-imports Lifting
+imports Lifting Groups_Big
 begin
 
 subsection \<open>Relator and predicator properties\<close>