author | wenzelm |
Tue, 13 Dec 2005 19:32:05 +0100 | |
changeset 18398 | 5d63a8b35688 |
parent 18369 | 694ea14ab4f2 |
child 19670 | 2e4a143c73c5 |
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 |
9 |
imports IntFact |
|
10 |
begin |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
11 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
12 |
text{*These are useful for combinatorial and number-theoretic counting |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
13 |
arguments.*} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
14 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
15 |
text{*Note. This theory is being revised. See the web page |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
16 |
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
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 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
19 |
(* *) |
15392 | 20 |
(* Useful properties of sums and products *) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
21 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
22 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
23 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
24 |
subsection {* Useful properties of sums and products *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
25 |
|
18369 | 26 |
lemma setsum_same_function_zcong: |
15392 | 27 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
28 |
shows "[setsum f S = setsum g S] (mod m)" |
|
29 |
proof cases |
|
30 |
assume "finite S" |
|
31 |
thus ?thesis using a by induct (simp_all add: zcong_zadd) |
|
32 |
next |
|
33 |
assume "infinite S" thus ?thesis by(simp add:setsum_def) |
|
34 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
35 |
|
15392 | 36 |
lemma setprod_same_function_zcong: |
37 |
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)" |
|
38 |
shows "[setprod f S = setprod g S] (mod m)" |
|
39 |
proof cases |
|
40 |
assume "finite S" |
|
41 |
thus ?thesis using a by induct (simp_all add: zcong_zmult) |
|
42 |
next |
|
43 |
assume "infinite S" thus ?thesis by(simp add:setprod_def) |
|
44 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
45 |
|
15392 | 46 |
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
47 |
apply (induct set: Finites) |
15047 | 48 |
apply (auto simp add: left_distrib right_distrib int_eq_of_nat) |
49 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
50 |
|
18369 | 51 |
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = |
15392 | 52 |
int(c) * int(card X)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
53 |
apply (induct set: Finites) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
54 |
apply (auto simp add: zadd_zmult_distrib2) |
18369 | 55 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
56 |
|
18369 | 57 |
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = |
15392 | 58 |
c * setsum f A" |
18369 | 59 |
by (induct set: Finites) (auto simp add: zadd_zmult_distrib2) |
60 |
||
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
61 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
62 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
63 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
64 |
(* Cardinality of some explicit finite sets *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
65 |
(* *) |
15392 | 66 |
(******************************************************************) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
67 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
68 |
subsection {* Cardinality of explicit finite sets *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
69 |
|
15392 | 70 |
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B" |
18369 | 71 |
by (simp add: finite_subset finite_imageI) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
72 |
|
18369 | 73 |
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}" |
74 |
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
|
75 |
|
18369 | 76 |
lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}" |
77 |
proof - |
|
78 |
have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto |
|
79 |
then show ?thesis by (auto simp add: bdd_nat_set_l_finite) |
|
80 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
81 |
|
18369 | 82 |
lemma bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}" |
83 |
apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> |
|
15392 | 84 |
int ` {(x :: nat). x < nat n}") |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
85 |
apply (erule finite_surjI) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
86 |
apply (auto simp add: bdd_nat_set_l_finite image_def) |
18369 | 87 |
apply (rule_tac x = "nat x" in exI, simp) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
88 |
done |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
89 |
|
15392 | 90 |
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
91 |
apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
92 |
apply (erule ssubst) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
93 |
apply (rule bdd_int_set_l_finite) |
18369 | 94 |
apply auto |
95 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
96 |
|
15392 | 97 |
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}" |
18369 | 98 |
proof - |
99 |
have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}" |
|
100 |
by auto |
|
101 |
then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset) |
|
102 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
103 |
|
15392 | 104 |
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}" |
18369 | 105 |
proof - |
106 |
have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}" |
|
107 |
by auto |
|
108 |
then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset) |
|
109 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
110 |
|
15392 | 111 |
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x" |
18369 | 112 |
proof (induct x) |
113 |
show "card {y::nat . y < 0} = 0" by simp |
|
114 |
next |
|
15392 | 115 |
fix n::nat |
18369 | 116 |
assume "card {y. y < n} = n" |
15392 | 117 |
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
|
118 |
by auto |
15392 | 119 |
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
|
120 |
by auto |
15392 | 121 |
also have "... = Suc (card {y. y < n})" |
18369 | 122 |
by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite) |
123 |
finally show "card {y. y < Suc n} = Suc n" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
124 |
by (simp add: prems) |
15392 | 125 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
126 |
|
15392 | 127 |
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x" |
18369 | 128 |
proof - |
129 |
have "{y::nat. y \<le> x} = { y::nat. y < Suc x}" |
|
130 |
by auto |
|
131 |
then show ?thesis by (auto simp add: card_bdd_nat_set_l) |
|
132 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
133 |
|
15392 | 134 |
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n" |
135 |
proof - |
|
136 |
assume "0 \<le> n" |
|
15402 | 137 |
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
|
138 |
by (auto simp add: inj_on_def) |
15402 | 139 |
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
|
140 |
by (rule card_image) |
15392 | 141 |
also from prems 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
|
142 |
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
|
143 |
apply (rule_tac x = "nat x" in exI) |
18369 | 144 |
apply (auto simp add: nat_0_le) |
145 |
done |
|
146 |
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
|
147 |
by (rule card_bdd_nat_set_l) |
15392 | 148 |
finally show "card {y. 0 \<le> y & y < n} = nat n" . |
149 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
150 |
|
18369 | 151 |
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = |
15392 | 152 |
nat n + 1" |
18369 | 153 |
proof - |
154 |
assume "0 \<le> n" |
|
155 |
moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto |
|
156 |
ultimately show ?thesis |
|
157 |
using card_bdd_int_set_l [of "n + 1"] |
|
158 |
by (auto simp add: nat_add_distrib) |
|
159 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
160 |
|
18369 | 161 |
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> |
15392 | 162 |
card {x. 0 < x & x \<le> n} = nat n" |
163 |
proof - |
|
164 |
assume "0 \<le> n" |
|
15402 | 165 |
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
|
166 |
by (auto simp add: inj_on_def) |
18369 | 167 |
hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = |
15392 | 168 |
card {x. 0 \<le> x & x < n}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
169 |
by (rule card_image) |
18369 | 170 |
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
|
171 |
by (rule card_bdd_int_set_l) |
15392 | 172 |
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
|
173 |
apply (auto simp add: image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
174 |
apply (rule_tac x = "x - 1" in exI) |
18369 | 175 |
apply arith |
176 |
done |
|
177 |
finally show "card {x. 0 < x & x \<le> n} = nat n" . |
|
15392 | 178 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
179 |
|
18369 | 180 |
lemma card_bdd_int_set_l_l: "0 < (n::int) ==> |
181 |
card {x. 0 < x & x < n} = nat n - 1" |
|
182 |
proof - |
|
183 |
assume "0 < n" |
|
184 |
moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}" |
|
185 |
by simp |
|
186 |
ultimately show ?thesis |
|
187 |
using insert card_bdd_int_set_l_le [of "n - 1"] |
|
188 |
by (auto simp add: nat_diff_distrib) |
|
189 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
190 |
|
18369 | 191 |
lemma int_card_bdd_int_set_l_l: "0 < n ==> |
15392 | 192 |
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
|
193 |
apply (auto simp add: card_bdd_int_set_l_l) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
194 |
apply (subgoal_tac "Suc 0 \<le> nat n") |
18369 | 195 |
apply (auto simp add: zdiff_int [symmetric]) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
196 |
apply (subgoal_tac "0 < nat n", arith) |
18369 | 197 |
apply (simp add: zero_less_nat_eq) |
198 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
199 |
|
18369 | 200 |
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> |
15392 | 201 |
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
|
202 |
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
|
203 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
204 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
205 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
206 |
(* Cartesian products of finite sets *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
207 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
208 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
209 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
210 |
subsection {* Cardinality of finite cartesian products *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
211 |
|
15402 | 212 |
(* FIXME could be useful in general but not needed here |
213 |
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
|
214 |
by blast |
15402 | 215 |
*) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
216 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
217 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
218 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
(* Sums and products over finite sets *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
220 |
(* *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
221 |
(******************************************************************) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
222 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
223 |
subsection {* Lemmas for counting arguments *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
224 |
|
18369 | 225 |
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
15392 | 226 |
g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A" |
227 |
apply (frule_tac h = g and f = f in setsum_reindex) |
|
228 |
apply (subgoal_tac "setsum g B = setsum g (f ` A)") |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
229 |
apply (simp add: inj_on_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
230 |
apply (subgoal_tac "card A = card B") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
231 |
apply (drule_tac A = "f ` A" and B = B in card_seteq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
232 |
apply (auto simp add: card_image) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
233 |
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
234 |
apply (frule_tac A = B and B = A and f = g in card_inj_on_le) |
18369 | 235 |
apply auto |
236 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
237 |
|
18369 | 238 |
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; |
15392 | 239 |
g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A" |
240 |
apply (frule_tac h = g and f = f in setprod_reindex) |
|
18369 | 241 |
apply (subgoal_tac "setprod g B = setprod g (f ` A)") |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
242 |
apply (simp add: inj_on_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
243 |
apply (subgoal_tac "card A = card B") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
244 |
apply (drule_tac A = "f ` A" and B = B in card_seteq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
245 |
apply (auto simp add: card_image) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
246 |
apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) |
18369 | 247 |
apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) |
248 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
249 |
|
18369 | 250 |
end |