author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 13871  26e5f5e624f6 
child 15392  290bc97038c7 
permissions  rwrr 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

1 
(* Title: HOL/Quadratic_Reciprocity/Residues.thy 
14981  2 
ID: $Id$ 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

3 
Authors: Jeremy Avigad, David Gray, and Adam Kramer 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

4 
*) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

5 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

6 
header {* Residue Sets *} 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

7 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

8 
theory Residues = Int2:; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

9 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

10 
text{*Note. This theory is being revised. See the web page 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

11 
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

12 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

13 
(*****************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

14 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

15 
(* Define the residue of a set, the standard residue, quadratic *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

16 
(* residues, and prove some basic properties. *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

17 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

18 
(*****************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

19 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

20 
constdefs 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

21 
ResSet :: "int => int set => bool" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

22 
"ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) > 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

23 
y1 = y2)" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

24 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

25 
StandardRes :: "int => int => int" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

26 
"StandardRes m x == x mod m" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

27 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

28 
QuadRes :: "int => int => bool" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

29 
"QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

30 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

31 
Legendre :: "int => int => int" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

32 
"Legendre a p == (if ([a = 0] (mod p)) then 0 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

33 
else if (QuadRes p a) then 1 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

34 
else 1)" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

35 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

36 
SR :: "int => int set" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

37 
"SR p == {x. (0 \<le> x) & (x < p)}" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

38 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

39 
SRStar :: "int => int set" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

40 
"SRStar p == {x. (0 < x) & (x < p)}"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

41 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

42 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

43 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

44 
(* Some useful properties of StandardRes *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

45 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

46 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

47 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

48 
subsection {* Properties of StandardRes *} 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

49 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

50 
lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

51 
by (auto simp add: StandardRes_def zcong_zmod) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

52 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

53 
lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

54 
= ([x1 = x2] (mod m))"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

55 
by (auto simp add: StandardRes_def zcong_zmod_eq) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

56 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

57 
lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

58 
by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

59 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

60 
lemma StandardRes_prop4: "2 < m 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

61 
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

62 
by (auto simp add: StandardRes_def zcong_zmod_eq 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

63 
zmod_zmult_distrib [of x y m]) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

64 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

65 
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

66 
by (auto simp add: StandardRes_def pos_mod_sign) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

67 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

68 
lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

69 
by (auto simp add: StandardRes_def pos_mod_bound) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

70 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

71 
lemma StandardRes_eq_zcong: 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

72 
"(StandardRes m x = 0) = ([x = 0](mod m))"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

73 
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

74 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

75 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

76 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

77 
(* Some useful stuff relating StandardRes and SRStar and SR *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

78 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

79 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

80 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

81 
subsection {* Relations between StandardRes, SRStar, and SR *} 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

82 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

83 
lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

84 
by (auto simp add: SRStar_def SR_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

85 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

86 
lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

87 
by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

88 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

89 
lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

90 
= (~[x = 0] (mod p))"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

91 
apply (auto simp add: StandardRes_prop3 StandardRes_def 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

92 
SRStar_def pos_mod_bound) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

93 
apply (subgoal_tac "0 < p") 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

94 
by (drule_tac a = x in pos_mod_sign, arith, simp) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

95 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

96 
lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

97 
by (auto simp add: SRStar_def zcong_def zdvd_not_zless) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

98 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

99 
lemma StandardRes_SRStar_prop2: "[ 2 < p; p \<in> zprime; x \<in> SRStar p ] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

100 
==> StandardRes p (MultInv p x) \<in> SRStar p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

101 
apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp); 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

102 
apply (rule MultInv_prop3) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

103 
apply (auto simp add: SRStar_def zcong_def zdvd_not_zless) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

104 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

105 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

106 
lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

107 
by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

108 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

109 
lemma StandardRes_SRStar_prop4: "[ p \<in> zprime; 2 < p; x \<in> SRStar p ] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

110 
==> StandardRes p x \<in> SRStar p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

111 
by (frule StandardRes_SRStar_prop3, auto) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

112 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

113 
lemma SRStar_mult_prop1: "[ p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

114 
==> (StandardRes p (x * y)):SRStar p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

115 
apply (frule_tac x = x in StandardRes_SRStar_prop4, auto) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

116 
apply (frule_tac x = y in StandardRes_SRStar_prop4, auto) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

117 
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

118 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

119 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

120 
lemma SRStar_mult_prop2: "[ p \<in> zprime; 2 < p; ~([a = 0](mod p)); 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

121 
x \<in> SRStar p ] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

122 
==> StandardRes p (a * MultInv p x) \<in> SRStar p"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

123 
apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

124 
apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

125 
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

126 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

127 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

128 
lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p  1"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

129 
by (auto simp add: SRStar_def int_card_bdd_int_set_l_l) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

130 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

131 
lemma SRStar_finite: "2 < p ==> finite( SRStar p)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

132 
by (auto simp add: SRStar_def bdd_int_set_l_l_finite) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

133 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

134 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

135 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

136 
(* Some useful stuff about ResSet and StandardRes *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

137 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

138 
(******************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

139 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

140 
subsection {* Properties relating ResSets with StandardRes *} 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

141 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

142 
lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

143 
apply (subgoal_tac "x = y ==> [x = y](mod m)"); 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

144 
apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)"); 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

145 
apply (auto simp add: zcong_zmod [of x y m]) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

146 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

147 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

148 
lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

149 
apply (auto simp add: ResSet_def StandardRes_def inj_on_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

150 
apply (drule_tac m = m in aux, auto) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

151 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

152 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

153 
lemma StandardRes_Sum: "[ finite X; 0 < m ] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

154 
==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

155 
apply (rule_tac F = X in finite_induct) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

156 
apply (auto intro!: zcong_zadd simp add: StandardRes_prop1) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

157 
done 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

158 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

159 
lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

160 
by (auto simp add: StandardRes_ubound StandardRes_lbound) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

161 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

162 
lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

163 
apply (rule_tac f = "StandardRes m" in finite_imageD) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

164 
apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset); 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

165 
by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

166 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

167 
lemma mod_mod_is_mod: "[x = x mod m](mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

168 
by (auto simp add: zcong_zmod) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

169 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

170 
lemma StandardRes_prod: "[ finite X; 0 < m ] 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

171 
==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

172 
apply (rule_tac F = X in finite_induct) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

173 
by (auto intro!: zcong_zmult simp add: StandardRes_prop1) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

174 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

175 
lemma ResSet_image: "[ 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) > x = y) ] ==> ResSet m (f ` A)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

176 
by (auto simp add: ResSet_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

177 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

178 
(****************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

179 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

180 
(* Property for SRStar *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

181 
(* *) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

182 
(****************************************************************) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

183 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

184 
lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"; 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

185 
by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

186 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

187 
end; 