--- 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 \<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>
--- 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 \<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>
--- 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 \<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>
--- 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 \<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>
--- 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 \<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>
--- 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 *)