1 (* Title: HOL/Quadratic_Reciprocity/Finite2.thy |
|
2 ID: $Id$ |
|
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
|
4 *) |
|
5 |
|
6 header {*Finite Sets and Finite Sums*} |
|
7 |
|
8 theory Finite2 |
|
9 imports Main IntFact Infinite_Set |
|
10 begin |
|
11 |
|
12 text{* |
|
13 These are useful for combinatorial and number-theoretic counting |
|
14 arguments. |
|
15 *} |
|
16 |
|
17 |
|
18 subsection {* Useful properties of sums and products *} |
|
19 |
|
20 lemma setsum_same_function_zcong: |
|
21 assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
|
22 shows "[setsum f S = setsum g S] (mod m)" |
|
23 proof cases |
|
24 assume "finite S" |
|
25 thus ?thesis using a by induct (simp_all add: zcong_zadd) |
|
26 next |
|
27 assume "infinite S" thus ?thesis by(simp add:setsum_def) |
|
28 qed |
|
29 |
|
30 lemma setprod_same_function_zcong: |
|
31 assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
|
32 shows "[setprod f S = setprod g S] (mod m)" |
|
33 proof cases |
|
34 assume "finite S" |
|
35 thus ?thesis using a by induct (simp_all add: zcong_zmult) |
|
36 next |
|
37 assume "infinite S" thus ?thesis by(simp add:setprod_def) |
|
38 qed |
|
39 |
|
40 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" |
|
41 apply (induct set: finite) |
|
42 apply (auto simp add: left_distrib right_distrib int_eq_of_nat) |
|
43 done |
|
44 |
|
45 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = |
|
46 int(c) * int(card X)" |
|
47 apply (induct set: finite) |
|
48 apply (auto simp add: zadd_zmult_distrib2) |
|
49 done |
|
50 |
|
51 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = |
|
52 c * setsum f A" |
|
53 by (induct set: finite) (auto simp add: zadd_zmult_distrib2) |
|
54 |
|
55 |
|
56 subsection {* Cardinality of explicit finite sets *} |
|
57 |
|
58 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B" |
|
59 by (simp add: finite_subset finite_imageI) |
|
60 |
|
61 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}" |
|
62 by (rule bounded_nat_set_is_finite) blast |
|
63 |
|
64 lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}" |
|
65 proof - |
|
66 have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto |
|
67 then show ?thesis by (auto simp add: bdd_nat_set_l_finite) |
|
68 qed |
|
69 |
|
70 lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}" |
|
71 apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> |
|
72 int ` {(x :: nat). x < nat n}") |
|
73 apply (erule finite_surjI) |
|
74 apply (auto simp add: bdd_nat_set_l_finite image_def) |
|
75 apply (rule_tac x = "nat x" in exI, simp) |
|
76 done |
|
77 |
|
78 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}" |
|
79 apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}") |
|
80 apply (erule ssubst) |
|
81 apply (rule bdd_int_set_l_finite) |
|
82 apply auto |
|
83 done |
|
84 |
|
85 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}" |
|
86 proof - |
|
87 have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}" |
|
88 by auto |
|
89 then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset) |
|
90 qed |
|
91 |
|
92 lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}" |
|
93 proof - |
|
94 have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}" |
|
95 by auto |
|
96 then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset) |
|
97 qed |
|
98 |
|
99 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x" |
|
100 proof (induct x) |
|
101 case 0 |
|
102 show "card {y::nat . y < 0} = 0" by simp |
|
103 next |
|
104 case (Suc n) |
|
105 have "{y. y < Suc n} = insert n {y. y < n}" |
|
106 by auto |
|
107 then have "card {y. y < Suc n} = card (insert n {y. y < n})" |
|
108 by auto |
|
109 also have "... = Suc (card {y. y < n})" |
|
110 by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite) |
|
111 finally show "card {y. y < Suc n} = Suc n" |
|
112 using `card {y. y < n} = n` by simp |
|
113 qed |
|
114 |
|
115 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x" |
|
116 proof - |
|
117 have "{y::nat. y \<le> x} = { y::nat. y < Suc x}" |
|
118 by auto |
|
119 then show ?thesis by (auto simp add: card_bdd_nat_set_l) |
|
120 qed |
|
121 |
|
122 lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n" |
|
123 proof - |
|
124 assume "0 \<le> n" |
|
125 have "inj_on (%y. int y) {y. y < nat n}" |
|
126 by (auto simp add: inj_on_def) |
|
127 hence "card (int ` {y. y < nat n}) = card {y. y < nat n}" |
|
128 by (rule card_image) |
|
129 also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}" |
|
130 apply (auto simp add: zless_nat_eq_int_zless image_def) |
|
131 apply (rule_tac x = "nat x" in exI) |
|
132 apply (auto simp add: nat_0_le) |
|
133 done |
|
134 also have "card {y. y < nat n} = nat n" |
|
135 by (rule card_bdd_nat_set_l) |
|
136 finally show "card {y. 0 \<le> y & y < n} = nat n" . |
|
137 qed |
|
138 |
|
139 lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = |
|
140 nat n + 1" |
|
141 proof - |
|
142 assume "0 \<le> n" |
|
143 moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto |
|
144 ultimately show ?thesis |
|
145 using card_bdd_int_set_l [of "n + 1"] |
|
146 by (auto simp add: nat_add_distrib) |
|
147 qed |
|
148 |
|
149 lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> |
|
150 card {x. 0 < x & x \<le> n} = nat n" |
|
151 proof - |
|
152 assume "0 \<le> n" |
|
153 have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}" |
|
154 by (auto simp add: inj_on_def) |
|
155 hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = |
|
156 card {x. 0 \<le> x & x < n}" |
|
157 by (rule card_image) |
|
158 also from `0 \<le> n` have "... = nat n" |
|
159 by (rule card_bdd_int_set_l) |
|
160 also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}" |
|
161 apply (auto simp add: image_def) |
|
162 apply (rule_tac x = "x - 1" in exI) |
|
163 apply arith |
|
164 done |
|
165 finally show "card {x. 0 < x & x \<le> n} = nat n" . |
|
166 qed |
|
167 |
|
168 lemma card_bdd_int_set_l_l: "0 < (n::int) ==> |
|
169 card {x. 0 < x & x < n} = nat n - 1" |
|
170 proof - |
|
171 assume "0 < n" |
|
172 moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}" |
|
173 by simp |
|
174 ultimately show ?thesis |
|
175 using insert card_bdd_int_set_l_le [of "n - 1"] |
|
176 by (auto simp add: nat_diff_distrib) |
|
177 qed |
|
178 |
|
179 lemma int_card_bdd_int_set_l_l: "0 < n ==> |
|
180 int(card {x. 0 < x & x < n}) = n - 1" |
|
181 apply (auto simp add: card_bdd_int_set_l_l) |
|
182 done |
|
183 |
|
184 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> |
|
185 int(card {x. 0 < x & x \<le> n}) = n" |
|
186 by (auto simp add: card_bdd_int_set_l_le) |
|
187 |
|
188 |
|
189 subsection {* Cardinality of finite cartesian products *} |
|
190 |
|
191 (* FIXME could be useful in general but not needed here |
|
192 lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)" |
|
193 by blast |
|
194 *) |
|
195 |
|
196 text {* Lemmas for counting arguments. *} |
|
197 |
|
198 lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
|
199 g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A" |
|
200 apply (frule_tac h = g and f = f in setsum_reindex) |
|
201 apply (subgoal_tac "setsum g B = setsum g (f ` A)") |
|
202 apply (simp add: inj_on_def) |
|
203 apply (subgoal_tac "card A = card B") |
|
204 apply (drule_tac A = "f ` A" and B = B in card_seteq) |
|
205 apply (auto simp add: card_image) |
|
206 apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) |
|
207 apply (frule_tac A = B and B = A and f = g in card_inj_on_le) |
|
208 apply auto |
|
209 done |
|
210 |
|
211 lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
|
212 g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A" |
|
213 apply (frule_tac h = g and f = f in setprod_reindex) |
|
214 apply (subgoal_tac "setprod g B = setprod g (f ` A)") |
|
215 apply (simp add: inj_on_def) |
|
216 apply (subgoal_tac "card A = card B") |
|
217 apply (drule_tac A = "f ` A" and B = B in card_seteq) |
|
218 apply (auto simp add: card_image) |
|
219 apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) |
|
220 apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) |
|
221 done |
|
222 |
|
223 end |
|