# HG changeset patch # User desharna # Date 1642001587 -3600 # Node ID a10873b3c7d45bb3fddbe5fe45838177bc0b707d # Parent 10df7a627ab6e96fa2f54be37b195fdef8530ab2# Parent 4d77dd3019d1237345e8b5ca9f2324a01babc2c9 merged diff -r 10df7a627ab6 -r a10873b3c7d4 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Tue Jan 11 22:07:04 2022 +0100 +++ b/src/HOL/Equiv_Relations.thy Wed Jan 12 16:33:07 2022 +0100 @@ -5,7 +5,7 @@ section \Equivalence Relations in Higher-Order Set Theory\ theory Equiv_Relations - imports Groups_Big + imports BNF_Least_Fixpoint begin subsection \Equivalence relations -- set version\ @@ -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 (\x. {x} // r) A" - shows "card (A//r) = card A" -proof - - have "\i\A. \j\A. i \ j \ r `` {j} \ 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 \By Jakub Kądziołka:\ - -lemma sum_fun_comp: - assumes "finite S" "finite R" "g ` S \ R" - shows "(\x \ S. f (g x)) = (\y \ R. of_nat (card {x \ S. g x = y}) * f y)" -proof - - let ?r = "relation_of (\p q. g p = g q) S" - have eqv: "equiv S ?r" - unfolding relation_of_def by (auto intro: comp_equivI) - have finite: "C \ S//?r \ finite C" for C - by (fact finite_equiv_class[OF \finite S\ equiv_type[OF \equiv S ?r\]]) - have disjoint: "A \ S//?r \ B \ S//?r \ A \ B \ A \ B = {}" for A B - using eqv quotient_disj by blast - - let ?cls = "\y. {x \ 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: "(\y \ R - g ` S. of_nat (card (?cls y)) * f y) = 0" - proof - - have "of_nat (card (?cls y)) * f y = 0" if asm: "y \ 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 "(\x \ S. f (g x)) = (\C \ S//?r. \x \ C. f (g x))" - using eqv finite disjoint - by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient) - also have "... = (\y \ g ` S. \x \ ?cls y. f (g x))" - unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj]) - also have "... = (\y \ g ` S. \x \ ?cls y. f y)" - by auto - also have "... = (\y \ g ` S. of_nat (card (?cls y)) * f y)" - by (simp flip: sum_constant) - also have "... = (\y \ R. of_nat (card (?cls y)) * f y)" - using rest_0 by (simp add: sum.subset_diff[OF \g ` S \ R\ \finite R\]) - finally show ?thesis - by (simp add: eq_commute) -qed subsection \Projection\ diff -r 10df7a627ab6 -r a10873b3c7d4 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Tue Jan 11 22:07:04 2022 +0100 +++ b/src/HOL/Groups_Big.thy Wed Jan 12 16:33:07 2022 +0100 @@ -8,7 +8,7 @@ section \Big sum and product over finite (non-empty) sets\ theory Groups_Big - imports Power + imports Power Equiv_Relations begin subsection \Generic monoid operation over a set\ @@ -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 (\x. {x} // r) A" + shows "card (A//r) = card A" +proof - + have "\i\A. \j\A. i \ j \ r `` {j} \ 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" "\j\t. (card {i\s. R i j} = k j)" shows "sum (\i. (card {j\t. R i j})) s = sum k t" @@ -1303,6 +1313,52 @@ qed qed simp +text \By Jakub Kądziołka:\ + +lemma sum_fun_comp: + assumes "finite S" "finite R" "g ` S \ R" + shows "(\x \ S. f (g x)) = (\y \ R. of_nat (card {x \ S. g x = y}) * f y)" +proof - + let ?r = "relation_of (\p q. g p = g q) S" + have eqv: "equiv S ?r" + unfolding relation_of_def by (auto intro: comp_equivI) + have finite: "C \ S//?r \ finite C" for C + by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]]) + have disjoint: "A \ S//?r \ B \ S//?r \ A \ B \ A \ B = {}" for A B + using eqv quotient_disj by blast + + let ?cls = "\y. {x \ 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: "(\y \ R - g ` S. of_nat (card (?cls y)) * f y) = 0" + proof - + have "of_nat (card (?cls y)) * f y = 0" if asm: "y \ 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 "(\x \ S. f (g x)) = (\C \ S//?r. \x \ C. f (g x))" + using eqv finite disjoint + by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient) + also have "... = (\y \ g ` S. \x \ ?cls y. f (g x))" + unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj]) + also have "... = (\y \ g ` S. \x \ ?cls y. f y)" + by auto + also have "... = (\y \ g ` S. of_nat (card (?cls y)) * f y)" + by (simp flip: sum_constant) + also have "... = (\y \ R. of_nat (card (?cls y)) * f y)" + using rest_0 by (simp add: sum.subset_diff[OF \g ` S \ R\ \finite R\]) + finally show ?thesis + by (simp add: eq_commute) +qed + + subsubsection \Cardinality of products\ diff -r 10df7a627ab6 -r a10873b3c7d4 src/HOL/Int.thy --- a/src/HOL/Int.thy Tue Jan 11 22:07:04 2022 +0100 +++ b/src/HOL/Int.thy Wed Jan 12 16:33:07 2022 +0100 @@ -6,7 +6,7 @@ section \The Integers as Equivalence Classes over Pairs of Natural Numbers\ theory Int - imports Equiv_Relations Power Quotient Fun_Def + imports Quotient Groups_Big Fun_Def begin subsection \Definition of integers as a quotient type\ diff -r 10df7a627ab6 -r a10873b3c7d4 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Tue Jan 11 22:07:04 2022 +0100 +++ b/src/HOL/Lattices_Big.thy Wed Jan 12 16:33:07 2022 +0100 @@ -6,7 +6,7 @@ section \Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\ theory Lattices_Big - imports Option + imports Groups_Big Option begin subsection \Generic lattice operations over a set\ diff -r 10df7a627ab6 -r a10873b3c7d4 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Tue Jan 11 22:07:04 2022 +0100 +++ b/src/HOL/Lifting_Set.thy Wed Jan 12 16:33:07 2022 +0100 @@ -5,7 +5,7 @@ section \Setup for Lifting/Transfer for the set type\ theory Lifting_Set -imports Lifting +imports Lifting Groups_Big begin subsection \Relator and predicator properties\ diff -r 10df7a627ab6 -r a10873b3c7d4 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jan 11 22:07:04 2022 +0100 +++ b/src/Pure/Isar/code.ML Wed Jan 12 16:33:07 2022 +0100 @@ -1112,12 +1112,7 @@ fun rewrite_eqn conv ctxt = singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt) -fun preprocess conv ctxt = - Thm.transfer' ctxt - #> rewrite_eqn conv ctxt - #> Axclass.unoverload ctxt; - -fun cert_of_eqns_preprocess ctxt functrans c = +fun apply_functrans ctxt functrans = let fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns); @@ -1126,19 +1121,25 @@ tap (tracing "before function transformation") #> (perhaps o perhaps_loop o perhaps_apply) functrans #> tap (tracing "after function transformation") - #> (map o apfst) (preprocess eqn_conv ctxt) - #> cert_of_eqns ctxt c end; +fun preprocess conv ctxt = + rewrite_eqn conv ctxt + #> Axclass.unoverload ctxt; + fun get_cert ctxt functrans c = case lookup_proper_fun_spec (specs_of (Proof_Context.theory_of ctxt)) c of NONE => nothing_cert ctxt c | SOME (Eqns (_, eqns)) => eqns - |> cert_of_eqns_preprocess ctxt functrans c + |> (map o apfst) (Thm.transfer' ctxt) + |> apply_functrans ctxt functrans + |> (map o apfst) (preprocess eqn_conv ctxt) + |> cert_of_eqns ctxt c | SOME (Proj (_, (tyco, _))) => cert_of_proj ctxt c tyco | SOME (Abstr (abs_thm, (tyco, _))) => abs_thm - |> preprocess Conv.arg_conv ctxt - |> cert_of_abs ctxt tyco c; + |> Thm.transfer' ctxt + |> preprocess Conv.arg_conv ctxt + |> cert_of_abs ctxt tyco c; (* case certificates *)