author | wenzelm |
Fri, 29 Jul 2016 20:34:07 +0200 | |
changeset 63566 | e5abbdee461a |
parent 63534 | 523b488b15c9 |
child 63633 | 2accfb71e33b |
permissions | -rw-r--r-- |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1 |
(* Authors: Jeremy Avigad, David Gray, and Adam Kramer |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
Ported by lcp but unfinished |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
*) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
|
60526 | 6 |
section \<open>Gauss' Lemma\<close> |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
theory Gauss |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
imports Residues |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
begin |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
lemma cong_prime_prod_zero_nat: |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
fixes a::nat |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
by (auto simp add: cong_altdef_nat) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
lemma cong_prime_prod_zero_int: |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
fixes a::int |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
by (auto simp add: cong_altdef_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
locale GAUSS = |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
fixes p :: "nat" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
fixes a :: "int" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
assumes p_prime: "prime p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
assumes p_ge_2: "2 < p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
assumes p_a_relprime: "[a \<noteq> 0](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
assumes a_nonzero: "0 < a" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
begin |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
definition "A = {0::int <.. ((int p - 1) div 2)}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
definition "B = (\<lambda>x. x * a) ` A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
definition "C = (\<lambda>x. x mod p) ` B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
definition "D = C \<inter> {.. (int p - 1) div 2}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
definition "E = C \<inter> {(int p - 1) div 2 <..}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
definition "F = (\<lambda>x. (int p - x)) ` E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
|
60526 | 41 |
subsection \<open>Basic properties of p\<close> |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
lemma odd_p: "odd p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
by (metis p_prime p_ge_2 prime_odd_nat) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
lemma p_minus_one_l: "(int p - 1) div 2 < p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
have "(p - 1) div 2 \<le> (p - 1) div 1" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
by (metis div_by_1 div_le_dividend) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
also have "\<dots> = p - 1" by simp |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
finally show ?thesis using p_ge_2 by arith |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"] |
58834 | 56 |
by simp |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
using odd_p p_ge_2 |
58645 | 60 |
by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
|
60526 | 63 |
subsection \<open>Basic Properties of the Gauss Sets\<close> |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
lemma finite_A: "finite (A)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
by (auto simp add: A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
lemma finite_B: "finite (B)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
by (auto simp add: B_def finite_A) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
lemma finite_C: "finite (C)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
by (auto simp add: C_def finite_B) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
lemma finite_D: "finite (D)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
by (auto simp add: D_def finite_C) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
lemma finite_E: "finite (E)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
by (auto simp add: E_def finite_C) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
lemma finite_F: "finite (F)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
by (auto simp add: F_def finite_E) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
lemma C_eq: "C = D \<union> E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
by (auto simp add: C_def D_def E_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
lemma A_card_eq: "card A = nat ((int p - 1) div 2)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
by (auto simp add: A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
using a_nonzero by (simp add: A_def inj_on_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
definition ResSet :: "int => int set => bool" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
lemma ResSet_image: |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
"\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow> |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
ResSet m (f ` A)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
by (auto simp add: ResSet_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
lemma A_res: "ResSet p A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
using p_ge_2 |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
lemma B_res: "ResSet p B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
{fix x fix y |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
assume a: "[x * a = y * a] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
assume b: "0 < x" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
assume c: "x \<le> (int p - 1) div 2" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
assume d: "0 < y" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
assume e: "y \<le> (int p - 1) div 2" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
112 |
from p_a_relprime have "\<not>p dvd a" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
113 |
by (simp add: cong_altdef_int) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
114 |
with p_prime have "coprime a (int p)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
115 |
by (subst gcd.commute, intro is_prime_imp_coprime) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
116 |
with a cong_mult_rcancel_int [of a "int p" x y] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
117 |
have "[x = y] (mod p)" by simp |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
118 |
with cong_less_imp_eq_int [of x y p] p_minus_one_l |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
order_le_less_trans [of x "(int p - 1) div 2" p] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
order_le_less_trans [of y "(int p - 1) div 2" p] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
have "x = y" |
62348 | 122 |
by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
} note xy = this |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
apply (insert p_ge_2 p_a_relprime p_minus_one_l) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
apply (auto simp add: B_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
apply (rule ResSet_image) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
apply (auto simp add: A_res) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
apply (auto simp add: A_def xy) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
{ fix x fix y |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
assume a: "x * a mod p = y * a mod p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
assume b: "0 < x" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
assume c: "x \<le> (int p - 1) div 2" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
assume d: "0 < y" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
assume e: "y \<le> (int p - 1) div 2" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
assume f: "x \<noteq> y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
142 |
from a have a': "[x * a = y * a](mod p)" |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
by (metis cong_int_def) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
144 |
from p_a_relprime have "\<not>p dvd a" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
145 |
by (simp add: cong_altdef_int) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
146 |
with p_prime have "coprime a (int p)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
147 |
by (subst gcd.commute, intro is_prime_imp_coprime) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
148 |
with a' cong_mult_rcancel_int [of a "int p" x y] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
149 |
have "[x = y] (mod p)" by simp |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
with cong_less_imp_eq_int [of x y p] p_minus_one_l |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
order_le_less_trans [of x "(int p - 1) div 2" p] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
order_le_less_trans [of y "(int p - 1) div 2" p] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
have "x = y" |
62348 | 154 |
by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
then have False |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
by (simp add: f)} |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
then show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
by (auto simp add: B_def inj_on_def A_def) metis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
160 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
162 |
apply (auto simp add: E_def C_def B_def A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
apply (rule_tac g = "(op - (int p))" in inj_on_inverseI) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
apply auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
lemma nonzero_mod_p: |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)" |
59545
12a6088ed195
explicit equivalence for strict order on lattices
haftmann
parents:
58889
diff
changeset
|
169 |
by (simp add: cong_int_def) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
by (rule nonzero_mod_p) (auto simp add: A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
173 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
by (auto simp add: A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
177 |
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
178 |
by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x" |
56544 | 181 |
using a_nonzero by (auto simp add: B_def A_greater_zero) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
182 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
proof (auto simp add: C_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
fix x :: int |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
assume a1: "x \<in> B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
thus "0 < x mod int p" using a1 f2 |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
apply (auto simp add: F_def E_def C_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
apply (auto intro: p_odd_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
by (auto simp add: D_def C_greater_zero) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
203 |
by (auto simp add: F_def E_def D_def C_def B_def A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
by (auto simp add: D_def C_def B_def A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
using p_prime A_ncong_p [OF assms] |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
210 |
by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
211 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
lemma A_prod_relprime: "gcd (setprod id A) p = 1" |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62348
diff
changeset
|
213 |
by (metis id_def all_A_relprime setprod_coprime) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
|
60526 | 216 |
subsection \<open>Relationships Between Gauss Sets\<close> |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
by (auto simp add: ResSet_def inj_on_def cong_int_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
lemma B_card_eq_A: "card B = card A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
lemma B_card_eq: "card B = nat ((int p - 1) div 2)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
by (simp add: B_card_eq_A A_card_eq) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
lemma F_card_eq_E: "card F = card E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
using finite_E |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
by (simp add: F_def inj_on_pminusx_E card_image) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
230 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
lemma C_card_eq_B: "card C = card B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
232 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
have "inj_on (\<lambda>x. x mod p) B" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
by (metis SR_B_inj) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
then show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
by (metis C_def card_image) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
239 |
lemma D_E_disj: "D \<inter> E = {}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
by (auto simp add: D_def E_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
lemma C_card_eq_D_plus_E: "card C = card D + card E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
243 |
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" |
57418 | 246 |
by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
apply (auto simp add: C_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
apply (insert finite_B SR_B_inj) |
57418 | 251 |
apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id]) |
252 |
apply auto |
|
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
253 |
apply (rule cong_setprod_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
apply (auto simp add: cong_int_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset]) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
apply (auto simp add: A_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
262 |
lemma F_D_disj: "(F \<inter> D) = {}" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
proof (auto simp add: F_eq D_eq) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
264 |
fix y::int and z::int |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
265 |
assume "p - (y*a) mod p = (z*a) mod p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
267 |
by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
moreover have "[y * a = (y*a) mod p] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
by (metis cong_int_def mod_mod_trivial) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
ultimately have "[a * (y + z) = 0] (mod p)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
271 |
by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1)) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
with p_prime a_nonzero p_a_relprime |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
273 |
have a: "[y + z = 0] (mod p)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
274 |
by (auto dest!: cong_prime_prod_zero_int) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
275 |
assume b: "y \<in> A" and c: "z \<in> A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
with A_def have "0 < y + z" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
277 |
by auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
moreover from b c p_eq2 A_def have "y + z < p" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
279 |
by auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
ultimately show False |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
by (metis a nonzero_mod_p) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
283 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
have "card (F \<union> D) = card E + card D" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
then have "card (F \<union> D) = card C" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
by (simp add: C_card_eq_D_plus_E) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
then show "card (F \<union> D) = nat ((p - 1) div 2)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
291 |
by (simp add: C_card_eq_B B_card_eq) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
292 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
293 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
294 |
lemma F_Un_D_eq_A: "F \<union> D = A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
295 |
using finite_A F_Un_D_subset A_card_eq F_Un_D_card |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
296 |
by (auto simp add: card_seteq) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
298 |
lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" |
57418 | 299 |
by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
300 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
301 |
lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
302 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
have FE: "setprod id F = setprod (op - p) E" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
304 |
apply (auto simp add: F_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
305 |
apply (insert finite_E inj_on_pminusx_E) |
57418 | 306 |
apply (drule setprod.reindex, auto) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
309 |
by (metis cong_int_def minus_mod_self1 mod_mod_trivial) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
310 |
then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
using finite_E p_ge_2 |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
by auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
then have two: "[setprod id F = setprod (uminus) E](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
316 |
have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
317 |
using finite_E by (induct set: finite) auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
318 |
with two show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
by simp |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
320 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
|
60526 | 323 |
subsection \<open>Gauss' Lemma\<close> |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
324 |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58288
diff
changeset
|
325 |
lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
326 |
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
theorem pre_gauss_lemma: |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
329 |
"[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
330 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
have "[setprod id A = setprod id F * setprod id D](mod p)" |
63566 | 332 |
by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
333 |
then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
apply (rule cong_trans_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
apply (metis cong_scalar_int prod_F_zcong) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
336 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
337 |
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
338 |
by (metis C_prod_eq_D_times_E mult.commute mult.left_commute) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
340 |
by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
341 |
then have "[setprod id A = ((-1)^(card E) * |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
342 |
(setprod id ((\<lambda>x. x * a) ` A)))] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
343 |
by (simp add: B_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
344 |
then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))] |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
(mod p)" |
57418 | 346 |
by (simp add: inj_on_xa_A setprod.reindex) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
moreover have "setprod (\<lambda>x. x * a) A = |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
348 |
setprod (\<lambda>x. a) A * setprod id A" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
using finite_A by (induct set: finite) auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
350 |
ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A * |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
351 |
setprod id A))] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
352 |
by simp |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
353 |
then have "[setprod id A = ((-1)^(card E) * a^(card A) * |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
354 |
setprod id A)](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
355 |
apply (rule cong_trans_int) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
356 |
apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
357 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
358 |
then have a: "[setprod id A * (-1)^(card E) = |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
359 |
((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
360 |
by (rule cong_scalar_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
361 |
then have "[setprod id A * (-1)^(card E) = setprod id A * |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
362 |
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
363 |
apply (rule cong_trans_int) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
364 |
apply (simp add: a mult.commute mult.left_commute) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
365 |
done |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
366 |
then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
367 |
apply (rule cong_trans_int) |
63566 | 368 |
apply (simp add: aux cong del: setprod.strong_cong) |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
369 |
done |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58288
diff
changeset
|
370 |
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
371 |
by (metis cong_mult_lcancel_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
372 |
then show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
373 |
by (simp add: A_card_eq cong_sym_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
374 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
376 |
(*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
377 |
quite a mess and should better be completely redone. |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
379 |
theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
380 |
proof - |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
381 |
from Euler_Criterion p_prime p_ge_2 have |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
382 |
"[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
383 |
by auto |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
384 |
moreover note pre_gauss_lemma |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
385 |
ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
386 |
by (rule cong_trans_int) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
387 |
moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
388 |
by (auto simp add: Legendre_def) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
389 |
moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1" |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
390 |
by (rule neg_one_power) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
391 |
ultimately show ?thesis |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
392 |
by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
393 |
qed |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
394 |
*) |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
395 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
396 |
end |
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
397 |
|
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
398 |
end |