1.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -20,25 +20,25 @@
1.4 wset :: "int * int => int set"
1.5
1.6 defs
1.7 - inv_def: "inv p a == (a^(nat (p - #2))) mod p"
1.8 + inv_def: "inv p a == (a^(nat (p - # 2))) mod p"
1.9
1.10 recdef wset
1.11 "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
1.12 "wset (a, p) =
1.13 - (if #1 < a then
1.14 - let ws = wset (a - #1, p)
1.15 + (if Numeral1 < a then
1.16 + let ws = wset (a - Numeral1, p)
1.17 in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
1.18
1.19
1.20 text {* \medskip @{term [source] inv} *}
1.21
1.22 -lemma aux: "#1 < m ==> Suc (nat (m - #2)) = nat (m - #1)"
1.23 +lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)"
1.24 apply (subst int_int_eq [symmetric])
1.25 apply auto
1.26 done
1.27
1.28 lemma inv_is_inv:
1.29 - "p \<in> zprime \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> [a * inv p a = #1] (mod p)"
1.30 + "p \<in> zprime \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> [a * inv p a = Numeral1] (mod p)"
1.31 apply (unfold inv_def)
1.32 apply (subst zcong_zmod)
1.33 apply (subst zmod_zmult1_eq [symmetric])
1.34 @@ -52,71 +52,71 @@
1.35 done
1.36
1.37 lemma inv_distinct:
1.38 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> a \<noteq> inv p a"
1.39 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> a \<noteq> inv p a"
1.40 apply safe
1.41 apply (cut_tac a = a and p = p in zcong_square)
1.42 apply (cut_tac [3] a = a and p = p in inv_is_inv)
1.43 apply auto
1.44 - apply (subgoal_tac "a = #1")
1.45 + apply (subgoal_tac "a = Numeral1")
1.46 apply (rule_tac [2] m = p in zcong_zless_imp_eq)
1.47 - apply (subgoal_tac [7] "a = p - #1")
1.48 + apply (subgoal_tac [7] "a = p - Numeral1")
1.49 apply (rule_tac [8] m = p in zcong_zless_imp_eq)
1.50 apply auto
1.51 done
1.52
1.53 lemma inv_not_0:
1.54 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #0"
1.55 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> Numeral0"
1.56 apply safe
1.57 apply (cut_tac a = a and p = p in inv_is_inv)
1.58 apply (unfold zcong_def)
1.59 apply auto
1.60 - apply (subgoal_tac "\<not> p dvd #1")
1.61 + apply (subgoal_tac "\<not> p dvd Numeral1")
1.62 apply (rule_tac [2] zdvd_not_zless)
1.63 - apply (subgoal_tac "p dvd #1")
1.64 + apply (subgoal_tac "p dvd Numeral1")
1.65 prefer 2
1.66 apply (subst zdvd_zminus_iff [symmetric])
1.67 apply auto
1.68 done
1.69
1.70 lemma inv_not_1:
1.71 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #1"
1.72 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> Numeral1"
1.73 apply safe
1.74 apply (cut_tac a = a and p = p in inv_is_inv)
1.75 prefer 4
1.76 apply simp
1.77 - apply (subgoal_tac "a = #1")
1.78 + apply (subgoal_tac "a = Numeral1")
1.79 apply (rule_tac [2] zcong_zless_imp_eq)
1.80 apply auto
1.81 done
1.82
1.83 -lemma aux: "[a * (p - #1) = #1] (mod p) = [a = p - #1] (mod p)"
1.84 +lemma aux: "[a * (p - Numeral1) = Numeral1] (mod p) = [a = p - Numeral1] (mod p)"
1.85 apply (unfold zcong_def)
1.86 apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
1.87 - apply (rule_tac s = "p dvd -((a + #1) + (p * -a))" in trans)
1.88 + apply (rule_tac s = "p dvd -((a + Numeral1) + (p * -a))" in trans)
1.89 apply (simp add: zmult_commute zminus_zdiff_eq)
1.90 apply (subst zdvd_zminus_iff)
1.91 apply (subst zdvd_reduce)
1.92 - apply (rule_tac s = "p dvd (a + #1) + (p * -#1)" in trans)
1.93 + apply (rule_tac s = "p dvd (a + Numeral1) + (p * -Numeral1)" in trans)
1.94 apply (subst zdvd_reduce)
1.95 apply auto
1.96 done
1.97
1.98 lemma inv_not_p_minus_1:
1.99 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> p - #1"
1.100 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> p - Numeral1"
1.101 apply safe
1.102 apply (cut_tac a = a and p = p in inv_is_inv)
1.103 apply auto
1.104 apply (simp add: aux)
1.105 - apply (subgoal_tac "a = p - #1")
1.106 + apply (subgoal_tac "a = p - Numeral1")
1.107 apply (rule_tac [2] zcong_zless_imp_eq)
1.108 apply auto
1.109 done
1.110
1.111 lemma inv_g_1:
1.112 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> #1 < inv p a"
1.113 - apply (case_tac "#0\<le> inv p a")
1.114 - apply (subgoal_tac "inv p a \<noteq> #1")
1.115 - apply (subgoal_tac "inv p a \<noteq> #0")
1.116 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> Numeral1 < inv p a"
1.117 + apply (case_tac "Numeral0\<le> inv p a")
1.118 + apply (subgoal_tac "inv p a \<noteq> Numeral1")
1.119 + apply (subgoal_tac "inv p a \<noteq> Numeral0")
1.120 apply (subst order_less_le)
1.121 apply (subst zle_add1_eq_le [symmetric])
1.122 apply (subst order_less_le)
1.123 @@ -128,7 +128,7 @@
1.124 done
1.125
1.126 lemma inv_less_p_minus_1:
1.127 - "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a < p - #1"
1.128 + "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a < p - Numeral1"
1.129 apply (case_tac "inv p a < p")
1.130 apply (subst order_less_le)
1.131 apply (simp add: inv_not_p_minus_1)
1.132 @@ -137,24 +137,24 @@
1.133 apply (simp add: pos_mod_bound)
1.134 done
1.135
1.136 -lemma aux: "#5 \<le> p ==>
1.137 - nat (p - #2) * nat (p - #2) = Suc (nat (p - #1) * nat (p - #3))"
1.138 +lemma aux: "# 5 \<le> p ==>
1.139 + nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))"
1.140 apply (subst int_int_eq [symmetric])
1.141 apply (simp add: zmult_int [symmetric])
1.142 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
1.143 done
1.144
1.145 lemma zcong_zpower_zmult:
1.146 - "[x^y = #1] (mod p) \<Longrightarrow> [x^(y * z) = #1] (mod p)"
1.147 + "[x^y = Numeral1] (mod p) \<Longrightarrow> [x^(y * z) = Numeral1] (mod p)"
1.148 apply (induct z)
1.149 apply (auto simp add: zpower_zadd_distrib)
1.150 - apply (subgoal_tac "zcong (x^y * x^(y * n)) (#1 * #1) p")
1.151 + apply (subgoal_tac "zcong (x^y * x^(y * n)) (Numeral1 * Numeral1) p")
1.152 apply (rule_tac [2] zcong_zmult)
1.153 apply simp_all
1.154 done
1.155
1.156 lemma inv_inv: "p \<in> zprime \<Longrightarrow>
1.157 - #5 \<le> p \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
1.158 + # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
1.159 apply (unfold inv_def)
1.160 apply (subst zpower_zmod)
1.161 apply (subst zpower_zpower)
1.162 @@ -165,7 +165,7 @@
1.163 apply (subst zcong_zmod [symmetric])
1.164 apply (subst aux)
1.165 apply (subgoal_tac [2]
1.166 - "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a * #1) p")
1.167 + "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p")
1.168 apply (rule_tac [3] zcong_zmult)
1.169 apply (rule_tac [4] zcong_zpower_zmult)
1.170 apply (erule_tac [4] Little_Fermat)
1.171 @@ -180,7 +180,7 @@
1.172
1.173 lemma wset_induct:
1.174 "(!!a p. P {} a p) \<Longrightarrow>
1.175 - (!!a p. #1 < (a::int) \<Longrightarrow> P (wset (a - #1, p)) (a - #1) p
1.176 + (!!a p. Numeral1 < (a::int) \<Longrightarrow> P (wset (a - Numeral1, p)) (a - Numeral1) p
1.177 ==> P (wset (a, p)) a p)
1.178 ==> P (wset (u, v)) u v"
1.179 proof -
1.180 @@ -188,7 +188,7 @@
1.181 show ?thesis
1.182 apply (rule wset.induct)
1.183 apply safe
1.184 - apply (case_tac [2] "#1 < a")
1.185 + apply (case_tac [2] "Numeral1 < a")
1.186 apply (rule_tac [2] rule_context)
1.187 apply simp_all
1.188 apply (simp_all add: wset.simps rule_context)
1.189 @@ -196,27 +196,27 @@
1.190 qed
1.191
1.192 lemma wset_mem_imp_or [rule_format]:
1.193 - "#1 < a \<Longrightarrow> b \<notin> wset (a - #1, p)
1.194 + "Numeral1 < a \<Longrightarrow> b \<notin> wset (a - Numeral1, p)
1.195 ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
1.196 apply (subst wset.simps)
1.197 apply (unfold Let_def)
1.198 apply simp
1.199 done
1.200
1.201 -lemma wset_mem_mem [simp]: "#1 < a ==> a \<in> wset (a, p)"
1.202 +lemma wset_mem_mem [simp]: "Numeral1 < a ==> a \<in> wset (a, p)"
1.203 apply (subst wset.simps)
1.204 apply (unfold Let_def)
1.205 apply simp
1.206 done
1.207
1.208 -lemma wset_subset: "#1 < a \<Longrightarrow> b \<in> wset (a - #1, p) ==> b \<in> wset (a, p)"
1.209 +lemma wset_subset: "Numeral1 < a \<Longrightarrow> b \<in> wset (a - Numeral1, p) ==> b \<in> wset (a, p)"
1.210 apply (subst wset.simps)
1.211 apply (unfold Let_def)
1.212 apply auto
1.213 done
1.214
1.215 lemma wset_g_1 [rule_format]:
1.216 - "p \<in> zprime --> a < p - #1 --> b \<in> wset (a, p) --> #1 < b"
1.217 + "p \<in> zprime --> a < p - Numeral1 --> b \<in> wset (a, p) --> Numeral1 < b"
1.218 apply (induct a p rule: wset_induct)
1.219 apply auto
1.220 apply (case_tac "b = a")
1.221 @@ -230,7 +230,7 @@
1.222 done
1.223
1.224 lemma wset_less [rule_format]:
1.225 - "p \<in> zprime --> a < p - #1 --> b \<in> wset (a, p) --> b < p - #1"
1.226 + "p \<in> zprime --> a < p - Numeral1 --> b \<in> wset (a, p) --> b < p - Numeral1"
1.227 apply (induct a p rule: wset_induct)
1.228 apply auto
1.229 apply (case_tac "b = a")
1.230 @@ -245,7 +245,7 @@
1.231
1.232 lemma wset_mem [rule_format]:
1.233 "p \<in> zprime -->
1.234 - a < p - #1 --> #1 < b --> b \<le> a --> b \<in> wset (a, p)"
1.235 + a < p - Numeral1 --> Numeral1 < b --> b \<le> a --> b \<in> wset (a, p)"
1.236 apply (induct a p rule: wset.induct)
1.237 apply auto
1.238 apply (subgoal_tac "b = a")
1.239 @@ -256,7 +256,7 @@
1.240 done
1.241
1.242 lemma wset_mem_inv_mem [rule_format]:
1.243 - "p \<in> zprime --> #5 \<le> p --> a < p - #1 --> b \<in> wset (a, p)
1.244 + "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
1.245 --> inv p b \<in> wset (a, p)"
1.246 apply (induct a p rule: wset_induct)
1.247 apply auto
1.248 @@ -274,7 +274,7 @@
1.249 done
1.250
1.251 lemma wset_inv_mem_mem:
1.252 - "p \<in> zprime \<Longrightarrow> #5 \<le> p \<Longrightarrow> a < p - #1 \<Longrightarrow> #1 < b \<Longrightarrow> b < p - #1
1.253 + "p \<in> zprime \<Longrightarrow> # 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
1.254 \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
1.255 apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
1.256 apply (rule_tac [2] wset_mem_inv_mem)
1.257 @@ -292,7 +292,7 @@
1.258
1.259 lemma wset_zcong_prod_1 [rule_format]:
1.260 "p \<in> zprime -->
1.261 - #5 \<le> p --> a < p - #1 --> [setprod (wset (a, p)) = #1] (mod p)"
1.262 + # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
1.263 apply (induct a p rule: wset_induct)
1.264 prefer 2
1.265 apply (subst wset.simps)
1.266 @@ -301,20 +301,20 @@
1.267 apply (subst setprod_insert)
1.268 apply (tactic {* stac (thm "setprod_insert") 3 *})
1.269 apply (subgoal_tac [5]
1.270 - "zcong (a * inv p a * setprod (wset (a - #1, p))) (#1 * #1) p")
1.271 + "zcong (a * inv p a * setprod (wset (a - Numeral1, p))) (Numeral1 * Numeral1) p")
1.272 prefer 5
1.273 apply (simp add: zmult_assoc)
1.274 apply (rule_tac [5] zcong_zmult)
1.275 apply (rule_tac [5] inv_is_inv)
1.276 apply (tactic "Clarify_tac 4")
1.277 - apply (subgoal_tac [4] "a \<in> wset (a - #1, p)")
1.278 + apply (subgoal_tac [4] "a \<in> wset (a - Numeral1, p)")
1.279 apply (rule_tac [5] wset_inv_mem_mem)
1.280 apply (simp_all add: wset_fin)
1.281 apply (rule inv_distinct)
1.282 apply auto
1.283 done
1.284
1.285 -lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - #2) = wset (p - #2, p)"
1.286 +lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)"
1.287 apply safe
1.288 apply (erule wset_mem)
1.289 apply (rule_tac [2] d22set_g_1)
1.290 @@ -323,7 +323,7 @@
1.291 apply (erule_tac [4] wset_g_1)
1.292 prefer 6
1.293 apply (subst zle_add1_eq_le [symmetric])
1.294 - apply (subgoal_tac "p - #2 + #1 = p - #1")
1.295 + apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1")
1.296 apply (simp (no_asm_simp))
1.297 apply (erule wset_less)
1.298 apply auto
1.299 @@ -332,36 +332,36 @@
1.300
1.301 subsection {* Wilson *}
1.302
1.303 -lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> #2 \<Longrightarrow> p \<noteq> #3 ==> #5 \<le> p"
1.304 +lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p"
1.305 apply (unfold zprime_def dvd_def)
1.306 - apply (case_tac "p = #4")
1.307 + apply (case_tac "p = # 4")
1.308 apply auto
1.309 apply (rule notE)
1.310 prefer 2
1.311 apply assumption
1.312 apply (simp (no_asm))
1.313 - apply (rule_tac x = "#2" in exI)
1.314 + apply (rule_tac x = "# 2" in exI)
1.315 apply safe
1.316 - apply (rule_tac x = "#2" in exI)
1.317 + apply (rule_tac x = "# 2" in exI)
1.318 apply auto
1.319 apply arith
1.320 done
1.321
1.322 theorem Wilson_Russ:
1.323 - "p \<in> zprime ==> [zfact (p - #1) = #-1] (mod p)"
1.324 - apply (subgoal_tac "[(p - #1) * zfact (p - #2) = #-1 * #1] (mod p)")
1.325 + "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
1.326 + apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)")
1.327 apply (rule_tac [2] zcong_zmult)
1.328 apply (simp only: zprime_def)
1.329 apply (subst zfact.simps)
1.330 - apply (rule_tac t = "p - #1 - #1" and s = "p - #2" in subst)
1.331 + apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
1.332 apply auto
1.333 apply (simp only: zcong_def)
1.334 apply (simp (no_asm_simp))
1.335 - apply (case_tac "p = #2")
1.336 + apply (case_tac "p = # 2")
1.337 apply (simp add: zfact.simps)
1.338 - apply (case_tac "p = #3")
1.339 + apply (case_tac "p = # 3")
1.340 apply (simp add: zfact.simps)
1.341 - apply (subgoal_tac "#5 \<le> p")
1.342 + apply (subgoal_tac "# 5 \<le> p")
1.343 apply (erule_tac [2] prime_g_5)
1.344 apply (subst d22set_prod_zfact [symmetric])
1.345 apply (subst d22set_eq_wset)