author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58889  5b7a9633cfa8 
child 59545  12a6088ed195 
permissions  rwrr 
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 

58889  6 
section {* Gauss' Lemma *} 
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 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

41 
subsection {* Basic properties of p *} 
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 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

63 
subsection {* Basic Properties of the Gauss Sets *} 
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" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

112 
from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y] 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

113 
have "[x = y](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

114 
by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

115 
cong_mult_self_int gcd_int.commute prime_imp_coprime_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

116 
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

117 
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

118 
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

119 
have "x = y" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

120 
by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

121 
} note xy = this 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

122 
show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

123 
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

124 
apply (auto simp add: B_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

125 
apply (rule ResSet_image) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

126 
apply (auto simp add: A_res) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

127 
apply (auto simp add: A_def xy) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

128 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

129 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

130 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

131 
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

132 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

133 
{ fix x fix y 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

134 
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

135 
assume b: "0 < x" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

136 
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

137 
assume d: "0 < y" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

138 
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

139 
assume f: "x \<noteq> y" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

140 
from a have "[x * a = y * a](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

141 
by (metis cong_int_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

142 
with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y] 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

143 
have "[x = y](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

144 
by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

145 
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

146 
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

147 
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

148 
have "x = y" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

149 
by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

150 
then have False 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

151 
by (simp add: f)} 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

152 
then show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

153 
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

154 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

155 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

156 
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

157 
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

158 
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

159 
apply auto 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

160 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

161 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

162 
lemma nonzero_mod_p: 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

163 
fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

164 
by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

165 
inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int) 
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 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

168 
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

169 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

170 
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

171 
by (auto simp add: A_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

172 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

173 
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

174 
by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

175 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

176 
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x" 
56544  177 
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

178 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

179 
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

180 
proof (auto simp add: C_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

181 
fix x :: int 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

182 
assume a1: "x \<in> B" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

183 
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

184 
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

185 
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

186 
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

187 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

188 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

189 
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

190 
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

191 
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

192 
apply (auto intro: p_odd_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

193 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

194 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

195 
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

196 
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

197 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

198 
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

199 
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

200 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

201 
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

202 
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

203 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

204 
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

205 
using p_prime A_ncong_p [OF assms] 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

206 
by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int) 
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 A_prod_relprime: "gcd (setprod id A) p = 1" 
58288  209 
by (metis id_def all_A_relprime setprod_coprime_int) 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

210 

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 
subsection {* Relationships Between Gauss Sets *} 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

213 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

214 
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

215 
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

216 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

217 
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

218 
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

219 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

220 
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

221 
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

222 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

223 
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

224 
using finite_E 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

225 
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

226 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

227 
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

228 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

229 
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

230 
by (metis SR_B_inj) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

231 
then show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

232 
by (metis C_def card_image) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

233 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

234 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

235 
lemma D_E_disj: "D \<inter> E = {}" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

236 
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

237 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

238 
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

239 
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

240 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

241 
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" 
57418  242 
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

243 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

244 
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

245 
apply (auto simp add: C_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

246 
apply (insert finite_B SR_B_inj) 
57418  247 
apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id]) 
248 
apply auto 

55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

249 
apply (rule cong_setprod_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

250 
apply (auto simp add: cong_int_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

251 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

252 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

253 
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

254 
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

255 
apply (auto simp add: A_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

256 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

257 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

258 
lemma F_D_disj: "(F \<inter> D) = {}" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

259 
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

260 
fix y::int and z::int 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

261 
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

262 
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

263 
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

264 
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

265 
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

266 
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

267 
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

268 
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

269 
have a: "[y + z = 0] (mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

270 
by (metis cong_prime_prod_zero_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

271 
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

272 
with A_def have "0 < y + z" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

273 
by auto 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

274 
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

275 
by auto 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

276 
ultimately show False 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

277 
by (metis a nonzero_mod_p) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

278 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

279 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

280 
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

281 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

282 
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

283 
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

284 
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

285 
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

286 
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

287 
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

288 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

289 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

290 
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

291 
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

292 
by (auto simp add: card_seteq) 
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 prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" 
57418  295 
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

296 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

297 
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

298 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

299 
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

300 
apply (auto simp add: F_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

301 
apply (insert finite_E inj_on_pminusx_E) 
57418  302 
apply (drule setprod.reindex, auto) 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

303 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

304 
then have "\<forall>x \<in> E. [(px) mod p =  x](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

305 
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

306 
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

307 
using finite_E p_ge_2 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

308 
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

309 
by auto 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

310 
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

311 
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

312 
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

313 
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

314 
with two show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

315 
by simp 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

316 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

317 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

318 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

319 
subsection {* Gauss' Lemma *} 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

320 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58288
diff
changeset

321 
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

322 
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

323 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

324 
theorem pre_gauss_lemma: 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

325 
"[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

326 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

327 
have "[setprod id A = setprod id F * setprod id D](mod p)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

328 
by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong) 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

329 
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

330 
apply (rule cong_trans_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

331 
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

332 
done 
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 C)] (mod p)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

334 
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

335 
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

336 
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

337 
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

338 
(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

339 
by (simp add: B_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

340 
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

341 
(mod p)" 
57418  342 
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

343 
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

344 
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

345 
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

346 
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

347 
setprod id A))] (mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

348 
by simp 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

349 
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

350 
setprod id A)](mod p)" 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

351 
apply (rule cong_trans_int) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

352 
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

353 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

354 
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

355 
((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

356 
by (rule cong_scalar_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

357 
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

358 
(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

359 
apply (rule cong_trans_int) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

360 
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

361 
done 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

362 
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

363 
apply (rule cong_trans_int) 
57418  364 
apply (simp add: aux cong del:setprod.cong) 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

365 
done 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58288
diff
changeset

366 
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

367 
by (metis cong_mult_lcancel_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

368 
then show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

369 
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

370 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

371 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

372 
(*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

373 
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

374 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

375 
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

376 
proof  
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

377 
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

378 
"[(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

379 
by auto 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

380 
moreover note pre_gauss_lemma 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

381 
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

382 
by (rule cong_trans_int) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

383 
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

384 
by (auto simp add: Legendre_def) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

385 
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

386 
by (rule neg_one_power) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

387 
ultimately show ?thesis 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

388 
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

389 
qed 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

390 
*) 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

391 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

392 
end 
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

393 

97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

394 
end 