author  huffman 
Sun, 13 Nov 2011 19:26:53 +0100  
changeset 45480  a39bb6d42ace 
parent 44766  d4d33a4d7548 
child 45605  a89b4bc311a5 
permissions  rwrr 
38159  1 
(* Title: HOL/Old_Number_Theory/EulerFermat.thy 
2 
Author: Thomas M. Rasmussen 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

3 
Copyright 2000 University of Cambridge 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

4 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

5 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

6 
header {* Fermat's Little Theorem extended to Euler's Totient function *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

7 

27556  8 
theory EulerFermat 
9 
imports BijectionRel IntFact 

10 
begin 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

11 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

12 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

13 
Fermat's Little Theorem extended to Euler's Totient function. More 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

14 
abstract approach than BoyerMoore (which seems necessary to achieve 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

15 
the extended version). 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

16 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

17 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

18 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

19 
subsection {* Definitions and lemmas *} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

20 

38159  21 
inductive_set RsetR :: "int => int set set" for m :: int 
22 
where 

23 
empty [simp]: "{} \<in> RsetR m" 

24 
 insert: "A \<in> RsetR m ==> zgcd a m = 1 ==> 

25 
\<forall>a'. a' \<in> A > \<not> zcong a a' m ==> insert a A \<in> RsetR m" 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

26 

38159  27 
fun BnorRset :: "int \<Rightarrow> int => int set" where 
35440  28 
"BnorRset a m = 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

29 
(if 0 < a then 
35440  30 
let na = BnorRset (a  1) m 
27556  31 
in (if zgcd a m = 1 then insert a na else na) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

32 
else {})" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

33 

38159  34 
definition norRRset :: "int => int set" 
35 
where "norRRset m = BnorRset (m  1) m" 

19670  36 

38159  37 
definition noXRRset :: "int => int => int set" 
38 
where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m" 

19670  39 

38159  40 
definition phi :: "int => nat" 
41 
where "phi m = card (norRRset m)" 

19670  42 

38159  43 
definition is_RRset :: "int set => int => bool" 
44 
where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)" 

19670  45 

38159  46 
definition RRset2norRR :: "int set => int => int => int" 
47 
where 

48 
"RRset2norRR A m a = 

49 
(if 1 < m \<and> is_RRset A m \<and> a \<in> A then 

50 
SOME b. zcong a b m \<and> b \<in> norRRset m 

51 
else 0)" 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

52 

38159  53 
definition zcongm :: "int => int => int => bool" 
54 
where "zcongm m = (\<lambda>a b. zcong a b m)" 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

55 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

56 
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = 1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

57 
 {* LCP: not sure why this lemma is needed now *} 
18369  58 
by (auto simp add: abs_if) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

59 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

60 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

61 
text {* \medskip @{text norRRset} *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

62 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

63 
declare BnorRset.simps [simp del] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

64 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

65 
lemma BnorRset_induct: 
18369  66 
assumes "!!a m. P {} a m" 
35440  67 
and "!!a m :: int. 0 < a ==> P (BnorRset (a  1) m) (a  1) m 
68 
==> P (BnorRset a m) a m" 

69 
shows "P (BnorRset u v) u v" 

18369  70 
apply (rule BnorRset.induct) 
35440  71 
apply (case_tac "0 < a") 
72 
apply (rule_tac assms) 

18369  73 
apply simp_all 
35440  74 
apply (simp_all add: BnorRset.simps assms) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

75 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

76 

35440  77 
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

78 
apply (induct a m rule: BnorRset_induct) 
18369  79 
apply simp 
80 
apply (subst BnorRset.simps) 

13833  81 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

82 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

83 

35440  84 
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m" 
18369  85 
by (auto dest: Bnor_mem_zle) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

86 

35440  87 
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m > 0 < b" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

88 
apply (induct a m rule: BnorRset_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

89 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

90 
apply (subst BnorRset.simps) 
13833  91 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

92 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

93 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

94 
lemma Bnor_mem_if [rule_format]: 
35440  95 
"zgcd b m = 1 > 0 < b > b \<le> a > b \<in> BnorRset a m" 
13833  96 
apply (induct a m rule: BnorRset.induct, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

97 
apply (subst BnorRset.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

98 
defer 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

99 
apply (subst BnorRset.simps) 
13833  100 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

101 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

102 

35440  103 
lemma Bnor_in_RsetR [rule_format]: "a < m > BnorRset a m \<in> RsetR m" 
13833  104 
apply (induct a m rule: BnorRset_induct, simp) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

105 
apply (subst BnorRset.simps) 
13833  106 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

107 
apply (rule RsetR.insert) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

108 
apply (rule_tac [3] allI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

109 
apply (rule_tac [3] impI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

110 
apply (rule_tac [3] zcong_not) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

111 
apply (subgoal_tac [6] "a' \<le> a  1") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

112 
apply (rule_tac [7] Bnor_mem_zle) 
13833  113 
apply (rule_tac [5] Bnor_mem_zg, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

114 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

115 

35440  116 
lemma Bnor_fin: "finite (BnorRset a m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

117 
apply (induct a m rule: BnorRset_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

118 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

119 
apply (subst BnorRset.simps) 
13833  120 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

121 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

122 

13524  123 
lemma norR_mem_unique_aux: "a \<le> b  1 ==> a < (b::int)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

124 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

125 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

126 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

127 
lemma norR_mem_unique: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

128 
"1 < m ==> 
27556  129 
zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

130 
apply (unfold norRRset_def) 
13833  131 
apply (cut_tac a = a and m = m in zcong_zless_unique, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

132 
apply (rule_tac [2] m = m in zcong_zless_imp_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

133 
apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

134 
order_less_imp_le norR_mem_unique_aux simp add: zcong_sym) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13833
diff
changeset

135 
apply (rule_tac x = b in exI, safe) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

136 
apply (rule Bnor_mem_if) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

137 
apply (case_tac [2] "b = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

138 
apply (auto intro: order_less_le [THEN iffD2]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

139 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

140 
apply (simp only: zcong_def) 
27556  141 
apply (subgoal_tac "zgcd a m = m") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

142 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

143 
apply (subst zdvd_iff_zgcd [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

144 
apply (rule_tac [4] zgcd_zcong_zgcd) 
45480
a39bb6d42ace
remove unnecessary numberrepresentationspecific rules from metis calls;
huffman
parents:
44766
diff
changeset

145 
apply (simp_all (no_asm_use) add: zcong_sym) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

146 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

147 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

148 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

149 
text {* \medskip @{term noXRRset} *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

150 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

151 
lemma RRset_gcd [rule_format]: 
27556  152 
"is_RRset A m ==> a \<in> A > zgcd a m = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

153 
apply (unfold is_RRset_def) 
27556  154 
apply (rule RsetR.induct [where P="%A. a \<in> A > zgcd a m = 1"], auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

155 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

156 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

157 
lemma RsetR_zmult_mono: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

158 
"A \<in> RsetR m ==> 
27556  159 
0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m" 
13833  160 
apply (erule RsetR.induct, simp_all) 
161 
apply (rule RsetR.insert, auto) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

162 
apply (blast intro: zgcd_zgcd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

163 
apply (simp add: zcong_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

164 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

165 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

166 
lemma card_nor_eq_noX: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

167 
"0 < m ==> 
27556  168 
zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

169 
apply (unfold norRRset_def noXRRset_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

170 
apply (rule card_image) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

171 
apply (auto simp add: inj_on_def Bnor_fin) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

172 
apply (simp add: BnorRset.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

173 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

174 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

175 
lemma noX_is_RRset: 
27556  176 
"0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

177 
apply (unfold is_RRset_def phi_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

178 
apply (auto simp add: card_nor_eq_noX) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

179 
apply (unfold noXRRset_def norRRset_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

180 
apply (rule RsetR_zmult_mono) 
13833  181 
apply (rule Bnor_in_RsetR, simp_all) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

182 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

183 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

184 
lemma aux_some: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

185 
"1 < m ==> is_RRset A m ==> a \<in> A 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

186 
==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and> 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

187 
(SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

188 
apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) 
13833  189 
apply (rule_tac [2] RRset_gcd, simp_all) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

190 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

191 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

192 
lemma RRset2norRR_correct: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

193 
"1 < m ==> is_RRset A m ==> a \<in> A ==> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

194 
[a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m" 
13833  195 
apply (unfold RRset2norRR_def, simp) 
196 
apply (rule aux_some, simp_all) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

197 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

198 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

199 
lemmas RRset2norRR_correct1 = 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

200 
RRset2norRR_correct [THEN conjunct1, standard] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

201 
lemmas RRset2norRR_correct2 = 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

202 
RRset2norRR_correct [THEN conjunct2, standard] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

203 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

204 
lemma RsetR_fin: "A \<in> RsetR m ==> finite A" 
18369  205 
by (induct set: RsetR) auto 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

206 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

207 
lemma RRset_zcong_eq [rule_format]: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

208 
"1 < m ==> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

209 
is_RRset A m ==> [a = b] (mod m) ==> a \<in> A > b \<in> A > a = b" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

210 
apply (unfold is_RRset_def) 
26793
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
23755
diff
changeset

211 
apply (rule RsetR.induct [where P="%A. a \<in> A > b \<in> A > a = b"]) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

212 
apply (auto simp add: zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

213 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

214 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

215 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

216 
"P (SOME a. P a) ==> Q (SOME a. Q a) ==> 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

217 
(SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

218 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

219 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

220 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

221 
lemma RRset2norRR_inj: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

222 
"1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" 
13833  223 
apply (unfold RRset2norRR_def inj_on_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

224 
apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and> 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

225 
([y = b] (mod m) \<and> b \<in> norRRset m)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

226 
apply (rule_tac [2] aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

227 
apply (rule_tac [3] aux_some) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

228 
apply (rule_tac [2] aux_some) 
13833  229 
apply (rule RRset_zcong_eq, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

230 
apply (rule_tac b = b in zcong_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

231 
apply (simp_all add: zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

232 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

233 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

234 
lemma RRset2norRR_eq_norR: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

235 
"1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

236 
apply (rule card_seteq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

237 
prefer 3 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

238 
apply (subst card_image) 
15402  239 
apply (rule_tac RRset2norRR_inj, auto) 
240 
apply (rule_tac [3] RRset2norRR_correct2, auto) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

241 
apply (unfold is_RRset_def phi_def norRRset_def) 
15402  242 
apply (auto simp add: Bnor_fin) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

243 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

244 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

245 

13524  246 
lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" 
13833  247 
by (unfold inj_on_def, auto) 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

248 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

249 
lemma Bnor_prod_power [rule_format]: 
35440  250 
"x \<noteq> 0 ==> a < m > \<Prod>((\<lambda>a. a * x) ` BnorRset a m) = 
251 
\<Prod>(BnorRset a m) * x^card (BnorRset a m)" 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

252 
apply (induct a m rule: BnorRset_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

253 
prefer 2 
15481  254 
apply (simplesubst BnorRset.simps) {*multiple redexes*} 
13833  255 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

256 
apply (simp add: Bnor_fin Bnor_mem_zle_swap) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

257 
apply (subst setprod_insert) 
13524  258 
apply (rule_tac [2] Bnor_prod_power_aux) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

259 
apply (unfold inj_on_def) 
44766  260 
apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

261 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

262 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

263 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

264 
subsection {* Fermat *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

265 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

266 
lemma bijzcong_zcong_prod: 
15392  267 
"(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

268 
apply (unfold zcongm_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

269 
apply (erule bijR.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

270 
apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

271 
apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

272 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

273 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

274 
lemma Bnor_prod_zgcd [rule_format]: 
35440  275 
"a < m > zgcd (\<Prod>(BnorRset a m)) m = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

276 
apply (induct a m rule: BnorRset_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

277 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

278 
apply (subst BnorRset.simps) 
13833  279 
apply (unfold Let_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

280 
apply (simp add: Bnor_fin Bnor_mem_zle_swap) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

281 
apply (blast intro: zgcd_zgcd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

282 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

283 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

284 
theorem Euler_Fermat: 
27556  285 
"0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

286 
apply (unfold norRRset_def phi_def) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

287 
apply (case_tac "x = 0") 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset

288 
apply (case_tac [2] "m = 1") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

289 
apply (rule_tac [3] iffD1) 
35440  290 
apply (rule_tac [3] k = "\<Prod>(BnorRset (m  1) m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

291 
in zcong_cancel2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

292 
prefer 5 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

293 
apply (subst Bnor_prod_power [symmetric]) 
13833  294 
apply (rule_tac [7] Bnor_prod_zgcd, simp_all) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

295 
apply (rule bijzcong_zcong_prod) 
35440  296 
apply (fold norRRset_def, fold noXRRset_def) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

297 
apply (subst RRset2norRR_eq_norR [symmetric]) 
13833  298 
apply (rule_tac [3] inj_func_bijR, auto) 
13187  299 
apply (unfold zcongm_def) 
300 
apply (rule_tac [2] RRset2norRR_correct1) 

301 
apply (rule_tac [5] RRset2norRR_inj) 

302 
apply (auto intro: order_less_le [THEN iffD2] 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

303 
simp add: noX_is_RRset) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

304 
apply (unfold noXRRset_def norRRset_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

305 
apply (rule finite_imageI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

306 
apply (rule Bnor_fin) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

307 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

308 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16663
diff
changeset

309 
lemma Bnor_prime: 
35440  310 
"\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

311 
apply (induct a p rule: BnorRset.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

312 
apply (subst BnorRset.simps) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16663
diff
changeset

313 
apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime) 
35440  314 
apply (subgoal_tac "finite (BnorRset (a  1) m)") 
315 
apply (subgoal_tac "a ~: BnorRset (a  1) m") 

13833  316 
apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) 
317 
apply (frule Bnor_mem_zle, arith) 

318 
apply (frule Bnor_fin) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

319 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

320 

16663  321 
lemma phi_prime: "zprime p ==> phi p = nat (p  1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

322 
apply (unfold phi_def norRRset_def) 
13833  323 
apply (rule Bnor_prime, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

324 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

325 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

326 
theorem Little_Fermat: 
16663  327 
"zprime p ==> \<not> p dvd x ==> [x^(nat (p  1)) = 1] (mod p)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

328 
apply (subst phi_prime [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

329 
apply (rule_tac [2] Euler_Fermat) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

330 
apply (erule_tac [3] zprime_imp_zrelprime) 
13833  331 
apply (unfold zprime_def, auto) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10834
diff
changeset

332 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

333 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

334 
end 