author | hoelzl |
Thu, 12 Nov 2009 17:21:43 +0100 | |
changeset 33638 | 548a34929e98 |
parent 32479 | 521cc9bf2958 |
child 38159 | e9b4835a54ee |
permissions | -rw-r--r-- |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Quadratic_Reciprocity/Finite2.thy |
14981 | 2 |
ID: $Id$ |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
3 |
Authors: Jeremy Avigad, David Gray, and Adam Kramer |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
4 |
*) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
5 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
6 |
header {*Finite Sets and Finite Sums*} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
7 |
|
15392 | 8 |
theory Finite2 |
25592 | 9 |
imports Main IntFact Infinite_Set |
15392 | 10 |
begin |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
11 |
|
19670 | 12 |
text{* |
13 |
These are useful for combinatorial and number-theoretic counting |
|
14 |
arguments. |
|
15 |
*} |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
16 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
17 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
18 |
subsection {* Useful properties of sums and products *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
19 |
|
18369 | 20 |
lemma setsum_same_function_zcong: |
19670 | 21 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
22 |
shows "[setsum f S = setsum g S] (mod m)" |
|
15392 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
29 |
|
15392 | 30 |
lemma setprod_same_function_zcong: |
19670 | 31 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
32 |
shows "[setprod f S = setprod g S] (mod m)" |
|
15392 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
39 |
|
15392 | 40 |
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" |
22274 | 41 |
apply (induct set: finite) |
15047 | 42 |
apply (auto simp add: left_distrib right_distrib int_eq_of_nat) |
43 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
44 |
|
18369 | 45 |
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = |
15392 | 46 |
int(c) * int(card X)" |
22274 | 47 |
apply (induct set: finite) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
48 |
apply (auto simp add: zadd_zmult_distrib2) |
18369 | 49 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
50 |
|
18369 | 51 |
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = |
15392 | 52 |
c * setsum f A" |
22274 | 53 |
by (induct set: finite) (auto simp add: zadd_zmult_distrib2) |
18369 | 54 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
55 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
56 |
subsection {* Cardinality of explicit finite sets *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
57 |
|
15392 | 58 |
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B" |
18369 | 59 |
by (simp add: finite_subset finite_imageI) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
60 |
|
18369 | 61 |
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}" |
62 |
by (rule bounded_nat_set_is_finite) blast |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
63 |
|
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
69 |
|
18369 | 70 |
lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}" |
19670 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
77 |
|
15392 | 78 |
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}" |
19670 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
84 |
|
15392 | 85 |
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}" |
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
91 |
|
15392 | 92 |
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}" |
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
98 |
|
15392 | 99 |
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x" |
18369 | 100 |
proof (induct x) |
20369 | 101 |
case 0 |
18369 | 102 |
show "card {y::nat . y < 0} = 0" by simp |
103 |
next |
|
20369 | 104 |
case (Suc n) |
15392 | 105 |
have "{y. y < Suc n} = insert n {y. y < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
106 |
by auto |
15392 | 107 |
then have "card {y. y < Suc n} = card (insert n {y. y < n})" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
108 |
by auto |
15392 | 109 |
also have "... = Suc (card {y. y < n})" |
18369 | 110 |
by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite) |
111 |
finally show "card {y. y < Suc n} = Suc n" |
|
20369 | 112 |
using `card {y. y < n} = n` by simp |
15392 | 113 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
114 |
|
15392 | 115 |
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x" |
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
121 |
|
15392 | 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" |
|
15402 | 125 |
have "inj_on (%y. int y) {y. y < nat n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
126 |
by (auto simp add: inj_on_def) |
15402 | 127 |
hence "card (int ` {y. y < nat n}) = card {y. y < nat n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
128 |
by (rule card_image) |
20369 | 129 |
also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
130 |
apply (auto simp add: zless_nat_eq_int_zless image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
131 |
apply (rule_tac x = "nat x" in exI) |
18369 | 132 |
apply (auto simp add: nat_0_le) |
133 |
done |
|
134 |
also have "card {y. y < nat n} = nat n" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
135 |
by (rule card_bdd_nat_set_l) |
15392 | 136 |
finally show "card {y. 0 \<le> y & y < n} = nat n" . |
137 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
138 |
|
18369 | 139 |
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = |
15392 | 140 |
nat n + 1" |
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
148 |
|
18369 | 149 |
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> |
15392 | 150 |
card {x. 0 < x & x \<le> n} = nat n" |
151 |
proof - |
|
152 |
assume "0 \<le> n" |
|
15402 | 153 |
have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
154 |
by (auto simp add: inj_on_def) |
18369 | 155 |
hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = |
15392 | 156 |
card {x. 0 \<le> x & x < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
157 |
by (rule card_image) |
18369 | 158 |
also from `0 \<le> n` have "... = nat n" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
159 |
by (rule card_bdd_int_set_l) |
15392 | 160 |
also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
161 |
apply (auto simp add: image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
162 |
apply (rule_tac x = "x - 1" in exI) |
18369 | 163 |
apply arith |
164 |
done |
|
165 |
finally show "card {x. 0 < x & x \<le> n} = nat n" . |
|
15392 | 166 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
167 |
|
18369 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
178 |
|
18369 | 179 |
lemma int_card_bdd_int_set_l_l: "0 < n ==> |
15392 | 180 |
int(card {x. 0 < x & x < n}) = n - 1" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
181 |
apply (auto simp add: card_bdd_int_set_l_l) |
18369 | 182 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
183 |
|
18369 | 184 |
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> |
15392 | 185 |
int(card {x. 0 < x & x \<le> n}) = n" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
186 |
by (auto simp add: card_bdd_int_set_l_le) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
187 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
188 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
189 |
subsection {* Cardinality of finite cartesian products *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
190 |
|
15402 | 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)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
193 |
by blast |
15402 | 194 |
*) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
195 |
|
19670 | 196 |
text {* Lemmas for counting arguments. *} |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
197 |
|
18369 | 198 |
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
15392 | 199 |
g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A" |
19670 | 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 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
210 |
|
18369 | 211 |
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
15392 | 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) |
|
18369 | 214 |
apply (subgoal_tac "setprod g B = setprod g (f ` A)") |
19670 | 215 |
apply (simp add: inj_on_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
216 |
apply (subgoal_tac "card A = card B") |
19670 | 217 |
apply (drule_tac A = "f ` A" and B = B in card_seteq) |
218 |
apply (auto simp add: card_image) |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) |
18369 | 220 |
apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) |
221 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
222 |
|
18369 | 223 |
end |