src/HOL/NumberTheory/IntPrimes.thy
changeset 11868 56db9f3a6b3e
parent 11701 3d51fbf81c17
child 13183 c7290200b3f4
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
     1.5      :: int * int * int * int *int * int * int * int => nat)"
     1.6    "xzgcda (m, n, r', r, s', s, t', t) =
     1.7 -    (if r \<le> Numeral0 then (r', s', t')
     1.8 +    (if r \<le> 0 then (r', s', t')
     1.9       else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
    1.10    (hints simp: pos_mod_bound)
    1.11  
    1.12 @@ -38,13 +38,13 @@
    1.13    "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
    1.14  
    1.15  defs
    1.16 -  xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, Numeral1, Numeral0, Numeral0, Numeral1)"
    1.17 -  zprime_def: "zprime == {p. Numeral1 < p \<and> (\<forall>m. m dvd p --> m = Numeral1 \<or> m = p)}"
    1.18 +  xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
    1.19 +  zprime_def: "zprime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
    1.20    zcong_def: "[a = b] (mod m) == m dvd (a - b)"
    1.21  
    1.22  
    1.23  lemma zabs_eq_iff:
    1.24 -    "(abs (z::int) = w) = (z = w \<and> Numeral0 <= z \<or> z = -w \<and> z < Numeral0)"
    1.25 +    "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
    1.26    apply (auto simp add: zabs_def)
    1.27    done
    1.28  
    1.29 @@ -64,17 +64,17 @@
    1.30  
    1.31  subsection {* Divides relation *}
    1.32  
    1.33 -lemma zdvd_0_right [iff]: "(m::int) dvd Numeral0"
    1.34 +lemma zdvd_0_right [iff]: "(m::int) dvd 0"
    1.35    apply (unfold dvd_def)
    1.36    apply (blast intro: zmult_0_right [symmetric])
    1.37    done
    1.38  
    1.39 -lemma zdvd_0_left [iff]: "(Numeral0 dvd (m::int)) = (m = Numeral0)"
    1.40 +lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
    1.41    apply (unfold dvd_def)
    1.42    apply auto
    1.43    done
    1.44  
    1.45 -lemma zdvd_1_left [iff]: "Numeral1 dvd (m::int)"
    1.46 +lemma zdvd_1_left [iff]: "1 dvd (m::int)"
    1.47    apply (unfold dvd_def)
    1.48    apply simp
    1.49    done
    1.50 @@ -104,7 +104,7 @@
    1.51    done
    1.52  
    1.53  lemma zdvd_anti_sym:
    1.54 -    "Numeral0 < m ==> Numeral0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
    1.55 +    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
    1.56    apply (unfold dvd_def)
    1.57    apply auto
    1.58    apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
    1.59 @@ -186,19 +186,19 @@
    1.60    apply (simp add: zdvd_zadd zdvd_zmult2)
    1.61    done
    1.62  
    1.63 -lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = Numeral0)"
    1.64 +lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
    1.65    apply (unfold dvd_def)
    1.66    apply auto
    1.67    done
    1.68  
    1.69 -lemma zdvd_not_zless: "Numeral0 < m ==> m < n ==> \<not> n dvd (m::int)"
    1.70 +lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    1.71    apply (unfold dvd_def)
    1.72    apply auto
    1.73 -  apply (subgoal_tac "Numeral0 < n")
    1.74 +  apply (subgoal_tac "0 < n")
    1.75     prefer 2
    1.76     apply (blast intro: zless_trans)
    1.77    apply (simp add: int_0_less_mult_iff)
    1.78 -  apply (subgoal_tac "n * k < n * Numeral1")
    1.79 +  apply (subgoal_tac "n * k < n * 1")
    1.80     apply (drule zmult_zless_cancel1 [THEN iffD1])
    1.81     apply auto
    1.82    done
    1.83 @@ -221,7 +221,7 @@
    1.84        nat_mult_distrib [symmetric] nat_eq_iff2)
    1.85    done
    1.86  
    1.87 -lemma nat_dvd_iff: "(nat z dvd m) = (if Numeral0 \<le> z then (z dvd int m) else m = 0)"
    1.88 +lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    1.89    apply (auto simp add: dvd_def zmult_int [symmetric])
    1.90    apply (rule_tac x = "nat k" in exI)
    1.91    apply (cut_tac k = m in int_less_0_conv)
    1.92 @@ -245,11 +245,11 @@
    1.93  
    1.94  subsection {* Euclid's Algorithm and GCD *}
    1.95  
    1.96 -lemma zgcd_0 [simp]: "zgcd (m, Numeral0) = abs m"
    1.97 +lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
    1.98    apply (simp add: zgcd_def zabs_def)
    1.99    done
   1.100  
   1.101 -lemma zgcd_0_left [simp]: "zgcd (Numeral0, m) = abs m"
   1.102 +lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m"
   1.103    apply (simp add: zgcd_def zabs_def)
   1.104    done
   1.105  
   1.106 @@ -261,7 +261,7 @@
   1.107    apply (simp add: zgcd_def)
   1.108    done
   1.109  
   1.110 -lemma zgcd_non_0: "Numeral0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   1.111 +lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   1.112    apply (frule_tac b = n and a = m in pos_mod_sign)
   1.113    apply (simp add: zgcd_def zabs_def nat_mod_distrib)
   1.114    apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if)
   1.115 @@ -273,17 +273,17 @@
   1.116    done
   1.117  
   1.118  lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
   1.119 -  apply (tactic {* zdiv_undefined_case_tac "n = Numeral0" 1 *})
   1.120 +  apply (tactic {* zdiv_undefined_case_tac "n = 0" 1 *})
   1.121    apply (auto simp add: linorder_neq_iff zgcd_non_0)
   1.122    apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0)
   1.123     apply auto
   1.124    done
   1.125  
   1.126 -lemma zgcd_1 [simp]: "zgcd (m, Numeral1) = Numeral1"
   1.127 +lemma zgcd_1 [simp]: "zgcd (m, 1) = 1"
   1.128    apply (simp add: zgcd_def zabs_def)
   1.129    done
   1.130  
   1.131 -lemma zgcd_0_1_iff [simp]: "(zgcd (Numeral0, m) = Numeral1) = (abs m = Numeral1)"
   1.132 +lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)"
   1.133    apply (simp add: zgcd_def zabs_def)
   1.134    done
   1.135  
   1.136 @@ -303,7 +303,7 @@
   1.137    apply (simp add: zgcd_def gcd_commute)
   1.138    done
   1.139  
   1.140 -lemma zgcd_1_left [simp]: "zgcd (Numeral1, m) = Numeral1"
   1.141 +lemma zgcd_1_left [simp]: "zgcd (1, m) = 1"
   1.142    apply (simp add: zgcd_def gcd_1_left)
   1.143    done
   1.144  
   1.145 @@ -320,7 +320,7 @@
   1.146  lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
   1.147    -- {* addition is an AC-operator *}
   1.148  
   1.149 -lemma zgcd_zmult_distrib2: "Numeral0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
   1.150 +lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
   1.151    apply (simp del: zmult_zminus_right
   1.152      add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
   1.153      zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   1.154 @@ -330,29 +330,29 @@
   1.155    apply (simp add: zabs_def zgcd_zmult_distrib2)
   1.156    done
   1.157  
   1.158 -lemma zgcd_self [simp]: "Numeral0 \<le> m ==> zgcd (m, m) = m"
   1.159 -  apply (cut_tac k = m and m = "Numeral1" and n = "Numeral1" in zgcd_zmult_distrib2)
   1.160 +lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m"
   1.161 +  apply (cut_tac k = m and m = "1" and n = "1" in zgcd_zmult_distrib2)
   1.162     apply simp_all
   1.163    done
   1.164  
   1.165 -lemma zgcd_zmult_eq_self [simp]: "Numeral0 \<le> k ==> zgcd (k, k * n) = k"
   1.166 -  apply (cut_tac k = k and m = "Numeral1" and n = n in zgcd_zmult_distrib2)
   1.167 +lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k"
   1.168 +  apply (cut_tac k = k and m = "1" and n = n in zgcd_zmult_distrib2)
   1.169     apply simp_all
   1.170    done
   1.171  
   1.172 -lemma zgcd_zmult_eq_self2 [simp]: "Numeral0 \<le> k ==> zgcd (k * n, k) = k"
   1.173 -  apply (cut_tac k = k and m = n and n = "Numeral1" in zgcd_zmult_distrib2)
   1.174 +lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k"
   1.175 +  apply (cut_tac k = k and m = n and n = "1" in zgcd_zmult_distrib2)
   1.176     apply simp_all
   1.177    done
   1.178  
   1.179 -lemma aux: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> Numeral0 \<le> m ==> k dvd m"
   1.180 +lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
   1.181    apply (subgoal_tac "m = zgcd (m * n, m * k)")
   1.182     apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
   1.183     apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
   1.184    done
   1.185  
   1.186 -lemma zrelprime_zdvd_zmult: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> k dvd m"
   1.187 -  apply (case_tac "Numeral0 \<le> m")
   1.188 +lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
   1.189 +  apply (case_tac "0 \<le> m")
   1.190     apply (blast intro: aux)
   1.191    apply (subgoal_tac "k dvd -m")
   1.192     apply (rule_tac [2] aux)
   1.193 @@ -360,20 +360,20 @@
   1.194    done
   1.195  
   1.196  lemma zprime_imp_zrelprime:
   1.197 -    "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = Numeral1"
   1.198 +    "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1"
   1.199    apply (unfold zprime_def)
   1.200    apply auto
   1.201    done
   1.202  
   1.203  lemma zless_zprime_imp_zrelprime:
   1.204 -    "p \<in> zprime ==> Numeral0 < n ==> n < p ==> zgcd (n, p) = Numeral1"
   1.205 +    "p \<in> zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
   1.206    apply (erule zprime_imp_zrelprime)
   1.207    apply (erule zdvd_not_zless)
   1.208    apply assumption
   1.209    done
   1.210  
   1.211  lemma zprime_zdvd_zmult:
   1.212 -    "Numeral0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   1.213 +    "0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   1.214    apply safe
   1.215    apply (rule zrelprime_zdvd_zmult)
   1.216     apply (rule zprime_imp_zrelprime)
   1.217 @@ -392,7 +392,7 @@
   1.218    done
   1.219  
   1.220  lemma zgcd_zmult_zdvd_zgcd:
   1.221 -    "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) dvd zgcd (m, n)"
   1.222 +    "zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)"
   1.223    apply (simp add: zgcd_greatest_iff)
   1.224    apply (rule_tac n = k in zrelprime_zdvd_zmult)
   1.225     prefer 2
   1.226 @@ -402,16 +402,16 @@
   1.227    apply (simp (no_asm) add: zgcd_ac)
   1.228    done
   1.229  
   1.230 -lemma zgcd_zmult_cancel: "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) = zgcd (m, n)"
   1.231 +lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)"
   1.232    apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
   1.233    done
   1.234  
   1.235  lemma zgcd_zgcd_zmult:
   1.236 -    "zgcd (k, m) = Numeral1 ==> zgcd (n, m) = Numeral1 ==> zgcd (k * n, m) = Numeral1"
   1.237 +    "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1"
   1.238    apply (simp (no_asm_simp) add: zgcd_zmult_cancel)
   1.239    done
   1.240  
   1.241 -lemma zdvd_iff_zgcd: "Numeral0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
   1.242 +lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
   1.243    apply safe
   1.244     apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans)
   1.245      apply (rule_tac [3] zgcd_zdvd1)
   1.246 @@ -423,7 +423,7 @@
   1.247  
   1.248  subsection {* Congruences *}
   1.249  
   1.250 -lemma zcong_1 [simp]: "[a = b] (mod Numeral1)"
   1.251 +lemma zcong_1 [simp]: "[a = b] (mod 1)"
   1.252    apply (unfold zcong_def)
   1.253    apply auto
   1.254    done
   1.255 @@ -494,19 +494,19 @@
   1.256    done
   1.257  
   1.258  lemma zcong_square:
   1.259 -  "p \<in> zprime ==> Numeral0 < a ==> [a * a = Numeral1] (mod p)
   1.260 -    ==> [a = Numeral1] (mod p) \<or> [a = p - Numeral1] (mod p)"
   1.261 +  "p \<in> zprime ==> 0 < a ==> [a * a = 1] (mod p)
   1.262 +    ==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)"
   1.263    apply (unfold zcong_def)
   1.264    apply (rule zprime_zdvd_zmult)
   1.265 -    apply (rule_tac [3] s = "a * a - Numeral1 + p * (Numeral1 - a)" in subst)
   1.266 +    apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst)
   1.267       prefer 4
   1.268       apply (simp add: zdvd_reduce)
   1.269      apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2)
   1.270    done
   1.271  
   1.272  lemma zcong_cancel:
   1.273 -  "Numeral0 \<le> m ==>
   1.274 -    zgcd (k, m) = Numeral1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
   1.275 +  "0 \<le> m ==>
   1.276 +    zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
   1.277    apply safe
   1.278     prefer 2
   1.279     apply (blast intro: zcong_scalar)
   1.280 @@ -523,19 +523,19 @@
   1.281    done
   1.282  
   1.283  lemma zcong_cancel2:
   1.284 -  "Numeral0 \<le> m ==>
   1.285 -    zgcd (k, m) = Numeral1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
   1.286 +  "0 \<le> m ==>
   1.287 +    zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
   1.288    apply (simp add: zmult_commute zcong_cancel)
   1.289    done
   1.290  
   1.291  lemma zcong_zgcd_zmult_zmod:
   1.292 -  "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = Numeral1
   1.293 +  "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1
   1.294      ==> [a = b] (mod m * n)"
   1.295    apply (unfold zcong_def dvd_def)
   1.296    apply auto
   1.297    apply (subgoal_tac "m dvd n * ka")
   1.298     apply (subgoal_tac "m dvd ka")
   1.299 -    apply (case_tac [2] "Numeral0 \<le> ka")
   1.300 +    apply (case_tac [2] "0 \<le> ka")
   1.301       prefer 3
   1.302       apply (subst zdvd_zminus_iff [symmetric])
   1.303       apply (rule_tac n = n in zrelprime_zdvd_zmult)
   1.304 @@ -550,8 +550,8 @@
   1.305    done
   1.306  
   1.307  lemma zcong_zless_imp_eq:
   1.308 -  "Numeral0 \<le> a ==>
   1.309 -    a < m ==> Numeral0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
   1.310 +  "0 \<le> a ==>
   1.311 +    a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
   1.312    apply (unfold zcong_def dvd_def)
   1.313    apply auto
   1.314    apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
   1.315 @@ -566,38 +566,38 @@
   1.316    done
   1.317  
   1.318  lemma zcong_square_zless:
   1.319 -  "p \<in> zprime ==> Numeral0 < a ==> a < p ==>
   1.320 -    [a * a = Numeral1] (mod p) ==> a = Numeral1 \<or> a = p - Numeral1"
   1.321 +  "p \<in> zprime ==> 0 < a ==> a < p ==>
   1.322 +    [a * a = 1] (mod p) ==> a = 1 \<or> a = p - 1"
   1.323    apply (cut_tac p = p and a = a in zcong_square)
   1.324       apply (simp add: zprime_def)
   1.325      apply (auto intro: zcong_zless_imp_eq)
   1.326    done
   1.327  
   1.328  lemma zcong_not:
   1.329 -    "Numeral0 < a ==> a < m ==> Numeral0 < b ==> b < a ==> \<not> [a = b] (mod m)"
   1.330 +    "0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)"
   1.331    apply (unfold zcong_def)
   1.332    apply (rule zdvd_not_zless)
   1.333     apply auto
   1.334    done
   1.335  
   1.336  lemma zcong_zless_0:
   1.337 -    "Numeral0 \<le> a ==> a < m ==> [a = Numeral0] (mod m) ==> a = Numeral0"
   1.338 +    "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
   1.339    apply (unfold zcong_def dvd_def)
   1.340    apply auto
   1.341 -  apply (subgoal_tac "Numeral0 < m")
   1.342 +  apply (subgoal_tac "0 < m")
   1.343     apply (rotate_tac -1)
   1.344     apply (simp add: int_0_le_mult_iff)
   1.345 -   apply (subgoal_tac "m * k < m * Numeral1")
   1.346 +   apply (subgoal_tac "m * k < m * 1")
   1.347      apply (drule zmult_zless_cancel1 [THEN iffD1])
   1.348      apply (auto simp add: linorder_neq_iff)
   1.349    done
   1.350  
   1.351  lemma zcong_zless_unique:
   1.352 -    "Numeral0 < m ==> (\<exists>!b. Numeral0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.353 +    "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.354    apply auto
   1.355     apply (subgoal_tac [2] "[b = y] (mod m)")
   1.356 -    apply (case_tac [2] "b = Numeral0")
   1.357 -     apply (case_tac [3] "y = Numeral0")
   1.358 +    apply (case_tac [2] "b = 0")
   1.359 +     apply (case_tac [3] "y = 0")
   1.360        apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le
   1.361          simp add: zcong_sym)
   1.362    apply (unfold zcong_def dvd_def)
   1.363 @@ -616,8 +616,8 @@
   1.364    done
   1.365  
   1.366  lemma zgcd_zcong_zgcd:
   1.367 -  "Numeral0 < m ==>
   1.368 -    zgcd (a, m) = Numeral1 ==> [a = b] (mod m) ==> zgcd (b, m) = Numeral1"
   1.369 +  "0 < m ==>
   1.370 +    zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1"
   1.371    apply (auto simp add: zcong_iff_lin)
   1.372    done
   1.373  
   1.374 @@ -643,7 +643,7 @@
   1.375    apply (simp add: zadd_commute)
   1.376    done
   1.377  
   1.378 -lemma zcong_zmod_eq: "Numeral0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
   1.379 +lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
   1.380    apply auto
   1.381     apply (rule_tac m = m in zcong_zless_imp_eq)
   1.382         prefer 5
   1.383 @@ -659,13 +659,13 @@
   1.384    apply (auto simp add: zcong_def)
   1.385    done
   1.386  
   1.387 -lemma zcong_zero [iff]: "[a = b] (mod Numeral0) = (a = b)"
   1.388 +lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)"
   1.389    apply (auto simp add: zcong_def)
   1.390    done
   1.391  
   1.392  lemma "[a = b] (mod m) = (a mod m = b mod m)"
   1.393 -  apply (tactic {* zdiv_undefined_case_tac "m = Numeral0" 1 *})
   1.394 -  apply (case_tac "Numeral0 < m")
   1.395 +  apply (tactic {* zdiv_undefined_case_tac "m = 0" 1 *})
   1.396 +  apply (case_tac "0 < m")
   1.397     apply (simp add: zcong_zmod_eq)
   1.398    apply (rule_tac t = m in zminus_zminus [THEN subst])
   1.399    apply (subst zcong_zminus)
   1.400 @@ -677,7 +677,7 @@
   1.401  subsection {* Modulo *}
   1.402  
   1.403  lemma zmod_zdvd_zmod:
   1.404 -    "Numeral0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   1.405 +    "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   1.406    apply (unfold dvd_def)
   1.407    apply auto
   1.408    apply (subst zcong_zmod_eq [symmetric])
   1.409 @@ -696,14 +696,14 @@
   1.410  declare xzgcda.simps [simp del]
   1.411  
   1.412  lemma aux1:
   1.413 -  "zgcd (r', r) = k --> Numeral0 < r -->
   1.414 +  "zgcd (r', r) = k --> 0 < r -->
   1.415      (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
   1.416    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   1.417      z = s and aa = t' and ab = t in xzgcda.induct)
   1.418    apply (subst zgcd_eq)
   1.419    apply (subst xzgcda.simps)
   1.420    apply auto
   1.421 -  apply (case_tac "r' mod r = Numeral0")
   1.422 +  apply (case_tac "r' mod r = 0")
   1.423     prefer 2
   1.424     apply (frule_tac a = "r'" in pos_mod_sign)
   1.425     apply auto
   1.426 @@ -716,14 +716,14 @@
   1.427    done
   1.428  
   1.429  lemma aux2:
   1.430 -  "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> Numeral0 < r -->
   1.431 +  "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
   1.432      zgcd (r', r) = k"
   1.433    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   1.434      z = s and aa = t' and ab = t in xzgcda.induct)
   1.435    apply (subst zgcd_eq)
   1.436    apply (subst xzgcda.simps)
   1.437    apply (auto simp add: linorder_not_le)
   1.438 -  apply (case_tac "r' mod r = Numeral0")
   1.439 +  apply (case_tac "r' mod r = 0")
   1.440     prefer 2
   1.441     apply (frule_tac a = "r'" in pos_mod_sign)
   1.442     apply auto
   1.443 @@ -735,7 +735,7 @@
   1.444    done
   1.445  
   1.446  lemma xzgcd_correct:
   1.447 -    "Numeral0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
   1.448 +    "0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
   1.449    apply (unfold xzgcd_def)
   1.450    apply (rule iffI)
   1.451     apply (rule_tac [2] aux2 [THEN mp, THEN mp])
   1.452 @@ -768,17 +768,17 @@
   1.453    by (rule iffD2 [OF order_less_le conjI])
   1.454  
   1.455  lemma xzgcda_linear [rule_format]:
   1.456 -  "Numeral0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
   1.457 +  "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
   1.458      r' = s' * m + t' * n -->  r = s * m + t * n --> rn = sn * m + tn * n"
   1.459    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   1.460      z = s and aa = t' and ab = t in xzgcda.induct)
   1.461    apply (subst xzgcda.simps)
   1.462    apply (simp (no_asm))
   1.463    apply (rule impI)+
   1.464 -  apply (case_tac "r' mod r = Numeral0")
   1.465 +  apply (case_tac "r' mod r = 0")
   1.466     apply (simp add: xzgcda.simps)
   1.467     apply clarify
   1.468 -  apply (subgoal_tac "Numeral0 < r' mod r")
   1.469 +  apply (subgoal_tac "0 < r' mod r")
   1.470     apply (rule_tac [2] order_le_neq_implies_less)
   1.471     apply (rule_tac [2] pos_mod_sign)
   1.472      apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
   1.473 @@ -787,7 +787,7 @@
   1.474    done
   1.475  
   1.476  lemma xzgcd_linear:
   1.477 -    "Numeral0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
   1.478 +    "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
   1.479    apply (unfold xzgcd_def)
   1.480    apply (erule xzgcda_linear)
   1.481      apply assumption
   1.482 @@ -795,7 +795,7 @@
   1.483    done
   1.484  
   1.485  lemma zgcd_ex_linear:
   1.486 -    "Numeral0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
   1.487 +    "0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
   1.488    apply (simp add: xzgcd_correct)
   1.489    apply safe
   1.490    apply (rule exI)+
   1.491 @@ -804,8 +804,8 @@
   1.492    done
   1.493  
   1.494  lemma zcong_lineq_ex:
   1.495 -    "Numeral0 < n ==> zgcd (a, n) = Numeral1 ==> \<exists>x. [a * x = Numeral1] (mod n)"
   1.496 -  apply (cut_tac m = a and n = n and k = "Numeral1" in zgcd_ex_linear)
   1.497 +    "0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)"
   1.498 +  apply (cut_tac m = a and n = n and k = "1" in zgcd_ex_linear)
   1.499      apply safe
   1.500    apply (rule_tac x = s in exI)
   1.501    apply (rule_tac b = "s * a + t * n" in zcong_trans)
   1.502 @@ -816,8 +816,8 @@
   1.503    done
   1.504  
   1.505  lemma zcong_lineq_unique:
   1.506 -  "Numeral0 < n ==>
   1.507 -    zgcd (a, n) = Numeral1 ==> \<exists>!x. Numeral0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   1.508 +  "0 < n ==>
   1.509 +    zgcd (a, n) = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   1.510    apply auto
   1.511     apply (rule_tac [2] zcong_zless_imp_eq)
   1.512         apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
   1.513 @@ -833,7 +833,7 @@
   1.514    apply (subst zcong_zmod)
   1.515    apply (subst zmod_zmult1_eq [symmetric])
   1.516    apply (subst zcong_zmod [symmetric])
   1.517 -  apply (subgoal_tac "[a * x * b = Numeral1 * b] (mod n)")
   1.518 +  apply (subgoal_tac "[a * x * b = 1 * b] (mod n)")
   1.519     apply (rule_tac [2] zcong_zmult)
   1.520      apply (simp_all add: zmult_assoc)
   1.521    done