author | paulson <lp15@cam.ac.uk> |
Wed, 30 Sep 2015 17:09:12 +0100 | |
changeset 61286 | dcf7be51bf5d |
parent 58889 | 5b7a9633cfa8 |
child 61382 | efac889fccbc |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/Finite2.thy |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
2 |
Authors: Jeremy Avigad, David Gray, and Adam Kramer |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
3 |
*) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
4 |
|
58889 | 5 |
section {*Finite Sets and Finite Sums*} |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
6 |
|
15392 | 7 |
theory Finite2 |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40786
diff
changeset
|
8 |
imports IntFact "~~/src/HOL/Library/Infinite_Set" |
15392 | 9 |
begin |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
10 |
|
19670 | 11 |
text{* |
12 |
These are useful for combinatorial and number-theoretic counting |
|
13 |
arguments. |
|
14 |
*} |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
15 |
|
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 |
subsection {* Useful properties of sums and products *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
18 |
|
18369 | 19 |
lemma setsum_same_function_zcong: |
19670 | 20 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
21 |
shows "[setsum f S = setsum g S] (mod m)" |
|
15392 | 22 |
proof cases |
23 |
assume "finite S" |
|
24 |
thus ?thesis using a by induct (simp_all add: zcong_zadd) |
|
25 |
next |
|
51489 | 26 |
assume "infinite S" thus ?thesis by simp |
15392 | 27 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
28 |
|
15392 | 29 |
lemma setprod_same_function_zcong: |
19670 | 30 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
31 |
shows "[setprod f S = setprod g S] (mod m)" |
|
15392 | 32 |
proof cases |
33 |
assume "finite S" |
|
34 |
thus ?thesis using a by induct (simp_all add: zcong_zmult) |
|
35 |
next |
|
51489 | 36 |
assume "infinite S" thus ?thesis by simp |
15392 | 37 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
38 |
|
15392 | 39 |
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" |
61286 | 40 |
by (simp add: of_nat_mult) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
41 |
|
18369 | 42 |
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = |
15392 | 43 |
int(c) * int(card X)" |
61286 | 44 |
by (simp add: of_nat_mult) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
45 |
|
18369 | 46 |
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = |
15392 | 47 |
c * setsum f A" |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44766
diff
changeset
|
48 |
by (induct set: finite) (auto simp add: distrib_left) |
18369 | 49 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
50 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
51 |
subsection {* Cardinality of explicit finite sets *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
52 |
|
15392 | 53 |
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B" |
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset
|
54 |
by (simp add: finite_subset) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
55 |
|
18369 | 56 |
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}" |
57 |
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
|
58 |
|
18369 | 59 |
lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}" |
60 |
proof - |
|
61 |
have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto |
|
62 |
then show ?thesis by (auto simp add: bdd_nat_set_l_finite) |
|
63 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
64 |
|
18369 | 65 |
lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}" |
19670 | 66 |
apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> |
67 |
int ` {(x :: nat). x < nat n}") |
|
68 |
apply (erule finite_surjI) |
|
69 |
apply (auto simp add: bdd_nat_set_l_finite image_def) |
|
70 |
apply (rule_tac x = "nat x" in exI, simp) |
|
71 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
72 |
|
15392 | 73 |
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}" |
19670 | 74 |
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}") |
75 |
apply (erule ssubst) |
|
76 |
apply (rule bdd_int_set_l_finite) |
|
77 |
apply auto |
|
78 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
79 |
|
15392 | 80 |
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}" |
18369 | 81 |
proof - |
82 |
have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}" |
|
83 |
by auto |
|
84 |
then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset) |
|
85 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
86 |
|
15392 | 87 |
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}" |
18369 | 88 |
proof - |
89 |
have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}" |
|
90 |
by auto |
|
91 |
then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset) |
|
92 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
93 |
|
15392 | 94 |
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x" |
18369 | 95 |
proof (induct x) |
20369 | 96 |
case 0 |
18369 | 97 |
show "card {y::nat . y < 0} = 0" by simp |
98 |
next |
|
20369 | 99 |
case (Suc n) |
15392 | 100 |
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
|
101 |
by auto |
15392 | 102 |
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
|
103 |
by auto |
15392 | 104 |
also have "... = Suc (card {y. y < n})" |
18369 | 105 |
by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite) |
106 |
finally show "card {y. y < Suc n} = Suc n" |
|
20369 | 107 |
using `card {y. y < n} = n` by simp |
15392 | 108 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
109 |
|
15392 | 110 |
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x" |
18369 | 111 |
proof - |
112 |
have "{y::nat. y \<le> x} = { y::nat. y < Suc x}" |
|
113 |
by auto |
|
114 |
then show ?thesis by (auto simp add: card_bdd_nat_set_l) |
|
115 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
116 |
|
15392 | 117 |
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n" |
118 |
proof - |
|
119 |
assume "0 \<le> n" |
|
15402 | 120 |
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
|
121 |
by (auto simp add: inj_on_def) |
15402 | 122 |
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
|
123 |
by (rule card_image) |
20369 | 124 |
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
|
125 |
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
|
126 |
apply (rule_tac x = "nat x" in exI) |
18369 | 127 |
apply (auto simp add: nat_0_le) |
128 |
done |
|
129 |
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
|
130 |
by (rule card_bdd_nat_set_l) |
15392 | 131 |
finally show "card {y. 0 \<le> y & y < n} = nat n" . |
132 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
133 |
|
18369 | 134 |
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = |
15392 | 135 |
nat n + 1" |
18369 | 136 |
proof - |
137 |
assume "0 \<le> n" |
|
138 |
moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto |
|
139 |
ultimately show ?thesis |
|
140 |
using card_bdd_int_set_l [of "n + 1"] |
|
141 |
by (auto simp add: nat_add_distrib) |
|
142 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
143 |
|
18369 | 144 |
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> |
15392 | 145 |
card {x. 0 < x & x \<le> n} = nat n" |
146 |
proof - |
|
147 |
assume "0 \<le> n" |
|
15402 | 148 |
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
|
149 |
by (auto simp add: inj_on_def) |
18369 | 150 |
hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = |
15392 | 151 |
card {x. 0 \<le> x & x < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
152 |
by (rule card_image) |
18369 | 153 |
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
|
154 |
by (rule card_bdd_int_set_l) |
15392 | 155 |
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
|
156 |
apply (auto simp add: image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
157 |
apply (rule_tac x = "x - 1" in exI) |
18369 | 158 |
apply arith |
159 |
done |
|
160 |
finally show "card {x. 0 < x & x \<le> n} = nat n" . |
|
15392 | 161 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
162 |
|
18369 | 163 |
lemma card_bdd_int_set_l_l: "0 < (n::int) ==> |
164 |
card {x. 0 < x & x < n} = nat n - 1" |
|
165 |
proof - |
|
166 |
assume "0 < n" |
|
167 |
moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}" |
|
168 |
by simp |
|
169 |
ultimately show ?thesis |
|
170 |
using insert card_bdd_int_set_l_le [of "n - 1"] |
|
171 |
by (auto simp add: nat_diff_distrib) |
|
172 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
173 |
|
18369 | 174 |
lemma int_card_bdd_int_set_l_l: "0 < n ==> |
15392 | 175 |
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
|
176 |
apply (auto simp add: card_bdd_int_set_l_l) |
18369 | 177 |
done |
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_le: "0 \<le> n ==> |
15392 | 180 |
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
|
181 |
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
|
182 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
183 |
|
18369 | 184 |
end |