src/HOL/NumberTheory/IntPrimes.thy
changeset 13833 f8dcb1d9ea68
parent 13788 fd03c4ab89d4
child 13837 8dd150d36c65
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Wed Feb 26 10:48:00 2003 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed Feb 26 13:16:07 2003 +0100
     1.3 @@ -2,6 +2,11 @@
     1.4      ID:         $Id$
     1.5      Author:     Thomas M. Rasmussen
     1.6      Copyright   2000  University of Cambridge
     1.7 +
     1.8 +Changes by Jeremy Avigad, 2003/02/21:
     1.9 +   Repaired definition of zprime_def, added "0 <= m &"
    1.10 +   Added lemma zgcd_geq_zero
    1.11 +   Repaired proof of zprime_imp_zrelprime
    1.12  *)
    1.13  
    1.14  header {* Divisibility and prime numbers (on integers) *}
    1.15 @@ -21,43 +26,43 @@
    1.16  
    1.17  consts
    1.18    xzgcda :: "int * int * int * int * int * int * int * int => int * int * int"
    1.19 -  xzgcd :: "int => int => int * int * int"
    1.20 -  zprime :: "int set"
    1.21 -  zcong :: "int => int => int => bool"    ("(1[_ = _] '(mod _'))")
    1.22  
    1.23  recdef xzgcda
    1.24    "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
    1.25      :: int * int * int * int *int * int * int * int => nat)"
    1.26    "xzgcda (m, n, r', r, s', s, t', t) =
    1.27 -    (if r \<le> 0 then (r', s', t')
    1.28 -     else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
    1.29 +	(if r \<le> 0 then (r', s', t')
    1.30 +	 else xzgcda (m, n, r, r' mod r, 
    1.31 +		      s, s' - (r' div r) * s, 
    1.32 +		      t, t' - (r' div r) * t))"
    1.33  
    1.34  constdefs
    1.35    zgcd :: "int * int => int"
    1.36    "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
    1.37  
    1.38 -defs
    1.39 -  xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
    1.40 -  zprime_def: "zprime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
    1.41 -  zcong_def: "[a = b] (mod m) == m dvd (a - b)"
    1.42 +  zprime :: "int set"
    1.43 +  "zprime == {p. 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)}"
    1.44 +
    1.45 +  xzgcd :: "int => int => int * int * int"
    1.46 +  "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
    1.47 +
    1.48 +  zcong :: "int => int => int => bool"    ("(1[_ = _] '(mod _'))")
    1.49 +  "[a = b] (mod m) == m dvd (a - b)"
    1.50  
    1.51  
    1.52  lemma zabs_eq_iff:
    1.53      "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
    1.54 -  apply (auto simp add: zabs_def)
    1.55 -  done
    1.56 +  by (auto simp add: zabs_def)
    1.57  
    1.58  
    1.59  text {* \medskip @{term gcd} lemmas *}
    1.60  
    1.61  lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)"
    1.62 -  apply (simp add: gcd_commute)
    1.63 -  done
    1.64 +  by (simp add: gcd_commute)
    1.65  
    1.66  lemma gcd_diff2: "m \<le> n ==> gcd (n, n - m) = gcd (n, m)"
    1.67    apply (subgoal_tac "n = m + (n - m)")
    1.68 -   apply (erule ssubst, rule gcd_add1_eq)
    1.69 -  apply simp
    1.70 +   apply (erule ssubst, rule gcd_add1_eq, simp)
    1.71    done
    1.72  
    1.73  
    1.74 @@ -69,14 +74,10 @@
    1.75    done
    1.76  
    1.77  lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
    1.78 -  apply (unfold dvd_def)
    1.79 -  apply auto
    1.80 -  done
    1.81 +  by (unfold dvd_def, auto)
    1.82  
    1.83  lemma zdvd_1_left [iff]: "1 dvd (m::int)"
    1.84 -  apply (unfold dvd_def)
    1.85 -  apply simp
    1.86 -  done
    1.87 +  by (unfold dvd_def, simp)
    1.88  
    1.89  lemma zdvd_refl [simp]: "m dvd (m::int)"
    1.90    apply (unfold dvd_def)
    1.91 @@ -89,23 +90,18 @@
    1.92    done
    1.93  
    1.94  lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
    1.95 -  apply (unfold dvd_def)
    1.96 -  apply auto
    1.97 -   apply (rule_tac [!] x = "-k" in exI)
    1.98 -  apply auto
    1.99 +  apply (unfold dvd_def, auto)
   1.100 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.101    done
   1.102  
   1.103  lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
   1.104 -  apply (unfold dvd_def)
   1.105 -  apply auto
   1.106 -   apply (rule_tac [!] x = "-k" in exI)
   1.107 -  apply auto
   1.108 +  apply (unfold dvd_def, auto)
   1.109 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.110    done
   1.111  
   1.112  lemma zdvd_anti_sym:
   1.113      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   1.114 -  apply (unfold dvd_def)
   1.115 -  apply auto
   1.116 +  apply (unfold dvd_def, auto)
   1.117    apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
   1.118    done
   1.119  
   1.120 @@ -122,8 +118,7 @@
   1.121  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
   1.122    apply (subgoal_tac "m = n + (m - n)")
   1.123     apply (erule ssubst)
   1.124 -   apply (blast intro: zdvd_zadd)
   1.125 -  apply simp
   1.126 +   apply (blast intro: zdvd_zadd, simp)
   1.127    done
   1.128  
   1.129  lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   1.130 @@ -148,19 +143,16 @@
   1.131  
   1.132  lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   1.133    apply (unfold dvd_def)
   1.134 -  apply (simp add: zmult_assoc)
   1.135 -  apply blast
   1.136 +  apply (simp add: zmult_assoc, blast)
   1.137    done
   1.138  
   1.139  lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   1.140    apply (rule zdvd_zmultD2)
   1.141 -  apply (subst zmult_commute)
   1.142 -  apply assumption
   1.143 +  apply (subst zmult_commute, assumption)
   1.144    done
   1.145  
   1.146  lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   1.147 -  apply (unfold dvd_def)
   1.148 -  apply clarify
   1.149 +  apply (unfold dvd_def, clarify)
   1.150    apply (rule_tac x = "k * ka" in exI)
   1.151    apply (simp add: zmult_ac)
   1.152    done
   1.153 @@ -170,8 +162,7 @@
   1.154     apply (erule_tac [2] zdvd_zadd)
   1.155     apply (subgoal_tac "n = (n + k * m) - k * m")
   1.156      apply (erule ssubst)
   1.157 -    apply (erule zdvd_zdiff)
   1.158 -    apply simp_all
   1.159 +    apply (erule zdvd_zdiff, simp_all)
   1.160    done
   1.161  
   1.162  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   1.163 @@ -186,20 +177,16 @@
   1.164    done
   1.165  
   1.166  lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
   1.167 -  apply (unfold dvd_def)
   1.168 -  apply auto
   1.169 -  done
   1.170 +  by (unfold dvd_def, auto)
   1.171  
   1.172  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   1.173 -  apply (unfold dvd_def)
   1.174 -  apply auto
   1.175 +  apply (unfold dvd_def, auto)
   1.176    apply (subgoal_tac "0 < n")
   1.177     prefer 2
   1.178     apply (blast intro: zless_trans)
   1.179    apply (simp add: int_0_less_mult_iff)
   1.180    apply (subgoal_tac "n * k < n * 1")
   1.181 -   apply (drule zmult_zless_cancel1 [THEN iffD1])
   1.182 -   apply auto
   1.183 +   apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
   1.184    done
   1.185  
   1.186  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   1.187 @@ -230,82 +217,67 @@
   1.188  
   1.189  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   1.190    apply (auto simp add: dvd_def)
   1.191 -   apply (rule_tac [!] x = "-k" in exI)
   1.192 -   apply auto
   1.193 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.194    done
   1.195  
   1.196  lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   1.197    apply (auto simp add: dvd_def)
   1.198     apply (drule zminus_equation [THEN iffD1])
   1.199 -   apply (rule_tac [!] x = "-k" in exI)
   1.200 -   apply auto
   1.201 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.202    done
   1.203  
   1.204  
   1.205  subsection {* Euclid's Algorithm and GCD *}
   1.206  
   1.207  lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
   1.208 -  apply (simp add: zgcd_def zabs_def)
   1.209 -  done
   1.210 +  by (simp add: zgcd_def zabs_def)
   1.211  
   1.212  lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m"
   1.213 -  apply (simp add: zgcd_def zabs_def)
   1.214 -  done
   1.215 +  by (simp add: zgcd_def zabs_def)
   1.216  
   1.217  lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)"
   1.218 -  apply (simp add: zgcd_def)
   1.219 -  done
   1.220 +  by (simp add: zgcd_def)
   1.221  
   1.222  lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)"
   1.223 -  apply (simp add: zgcd_def)
   1.224 -  done
   1.225 +  by (simp add: zgcd_def)
   1.226  
   1.227  lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   1.228    apply (frule_tac b = n and a = m in pos_mod_sign)
   1.229 -  apply (simp add: zgcd_def zabs_def nat_mod_distrib del:pos_mod_sign)
   1.230 +  apply (simp del: pos_mod_sign add: zgcd_def zabs_def nat_mod_distrib)
   1.231    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   1.232    apply (frule_tac a = m in pos_mod_bound)
   1.233 -  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle del:pos_mod_bound)
   1.234 +  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
   1.235    done
   1.236  
   1.237  lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
   1.238    apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
   1.239    apply (auto simp add: linorder_neq_iff zgcd_non_0)
   1.240 -  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0)
   1.241 -   apply auto
   1.242 +  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
   1.243    done
   1.244  
   1.245  lemma zgcd_1 [simp]: "zgcd (m, 1) = 1"
   1.246 -  apply (simp add: zgcd_def zabs_def)
   1.247 -  done
   1.248 +  by (simp add: zgcd_def zabs_def)
   1.249  
   1.250  lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)"
   1.251 -  apply (simp add: zgcd_def zabs_def)
   1.252 -  done
   1.253 +  by (simp add: zgcd_def zabs_def)
   1.254  
   1.255  lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m"
   1.256 -  apply (simp add: zgcd_def zabs_def int_dvd_iff)
   1.257 -  done
   1.258 +  by (simp add: zgcd_def zabs_def int_dvd_iff)
   1.259  
   1.260  lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n"
   1.261 -  apply (simp add: zgcd_def zabs_def int_dvd_iff)
   1.262 -  done
   1.263 +  by (simp add: zgcd_def zabs_def int_dvd_iff)
   1.264  
   1.265  lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)"
   1.266 -  apply (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff)
   1.267 -  done
   1.268 +  by (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff)
   1.269  
   1.270  lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)"
   1.271 -  apply (simp add: zgcd_def gcd_commute)
   1.272 -  done
   1.273 +  by (simp add: zgcd_def gcd_commute)
   1.274  
   1.275  lemma zgcd_1_left [simp]: "zgcd (1, m) = 1"
   1.276 -  apply (simp add: zgcd_def gcd_1_left)
   1.277 -  done
   1.278 +  by (simp add: zgcd_def gcd_1_left)
   1.279  
   1.280  lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))"
   1.281 -  apply (simp add: zgcd_def gcd_assoc)
   1.282 -  done
   1.283 +  by (simp add: zgcd_def gcd_assoc)
   1.284  
   1.285  lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))"
   1.286    apply (rule zgcd_commute [THEN trans])
   1.287 @@ -317,31 +289,24 @@
   1.288    -- {* addition is an AC-operator *}
   1.289  
   1.290  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
   1.291 -  apply (simp del: zmult_zminus_right
   1.292 -    add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
   1.293 -    zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   1.294 -  done
   1.295 +  by (simp del: zmult_zminus_right
   1.296 +      add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
   1.297 +          zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   1.298  
   1.299  lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
   1.300 -  apply (simp add: zabs_def zgcd_zmult_distrib2)
   1.301 -  done
   1.302 +  by (simp add: zabs_def zgcd_zmult_distrib2)
   1.303  
   1.304  lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m"
   1.305 -  apply (cut_tac k = m and m = "1" and n = "1" in zgcd_zmult_distrib2)
   1.306 -   apply simp_all
   1.307 -  done
   1.308 +  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
   1.309  
   1.310  lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k"
   1.311 -  apply (cut_tac k = k and m = "1" and n = n in zgcd_zmult_distrib2)
   1.312 -   apply simp_all
   1.313 -  done
   1.314 +  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
   1.315  
   1.316  lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k"
   1.317 -  apply (cut_tac k = k and m = n and n = "1" in zgcd_zmult_distrib2)
   1.318 -   apply simp_all
   1.319 -  done
   1.320 +  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
   1.321  
   1.322 -lemma zrelprime_zdvd_zmult_aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
   1.323 +lemma zrelprime_zdvd_zmult_aux:
   1.324 +     "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
   1.325    apply (subgoal_tac "m = zgcd (m * n, m * k)")
   1.326     apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
   1.327     apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
   1.328 @@ -351,29 +316,31 @@
   1.329    apply (case_tac "0 \<le> m")
   1.330     apply (blast intro: zrelprime_zdvd_zmult_aux)
   1.331    apply (subgoal_tac "k dvd -m")
   1.332 -   apply (rule_tac [2] zrelprime_zdvd_zmult_aux)
   1.333 -     apply auto
   1.334 +   apply (rule_tac [2] zrelprime_zdvd_zmult_aux, auto)
   1.335    done
   1.336  
   1.337 +lemma zgcd_geq_zero: "0 <= zgcd(x,y)"
   1.338 +  by (auto simp add: zgcd_def)
   1.339 +
   1.340  lemma zprime_imp_zrelprime:
   1.341      "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1"
   1.342 -  apply (unfold zprime_def)
   1.343 -  apply auto
   1.344 +  apply (auto simp add: zprime_def)
   1.345 +  apply (drule_tac x = "zgcd(n, p)" in allE)
   1.346 +  apply (auto simp add: zgcd_zdvd2 [of n p] zgcd_geq_zero)
   1.347 +  apply (insert zgcd_zdvd1 [of n p], auto)
   1.348    done
   1.349  
   1.350  lemma zless_zprime_imp_zrelprime:
   1.351      "p \<in> zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
   1.352    apply (erule zprime_imp_zrelprime)
   1.353 -  apply (erule zdvd_not_zless)
   1.354 -  apply assumption
   1.355 +  apply (erule zdvd_not_zless, assumption)
   1.356    done
   1.357  
   1.358  lemma zprime_zdvd_zmult:
   1.359      "0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   1.360    apply safe
   1.361    apply (rule zrelprime_zdvd_zmult)
   1.362 -   apply (rule zprime_imp_zrelprime)
   1.363 -    apply auto
   1.364 +   apply (rule zprime_imp_zrelprime, auto)
   1.365    done
   1.366  
   1.367  lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)"
   1.368 @@ -399,63 +366,50 @@
   1.369    done
   1.370  
   1.371  lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)"
   1.372 -  apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
   1.373 -  done
   1.374 +  by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
   1.375  
   1.376  lemma zgcd_zgcd_zmult:
   1.377      "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1"
   1.378 -  apply (simp (no_asm_simp) add: zgcd_zmult_cancel)
   1.379 -  done
   1.380 +  by (simp add: zgcd_zmult_cancel)
   1.381  
   1.382  lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
   1.383    apply safe
   1.384     apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans)
   1.385 -    apply (rule_tac [3] zgcd_zdvd1)
   1.386 -   apply simp_all
   1.387 -  apply (unfold dvd_def)
   1.388 -  apply auto
   1.389 +    apply (rule_tac [3] zgcd_zdvd1, simp_all)
   1.390 +  apply (unfold dvd_def, auto)
   1.391    done
   1.392  
   1.393  
   1.394  subsection {* Congruences *}
   1.395  
   1.396  lemma zcong_1 [simp]: "[a = b] (mod 1)"
   1.397 -  apply (unfold zcong_def)
   1.398 -  apply auto
   1.399 -  done
   1.400 +  by (unfold zcong_def, auto)
   1.401  
   1.402  lemma zcong_refl [simp]: "[k = k] (mod m)"
   1.403 -  apply (unfold zcong_def)
   1.404 -  apply auto
   1.405 -  done
   1.406 +  by (unfold zcong_def, auto)
   1.407  
   1.408  lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
   1.409 -  apply (unfold zcong_def dvd_def)
   1.410 -  apply auto
   1.411 -   apply (rule_tac [!] x = "-k" in exI)
   1.412 -   apply auto
   1.413 +  apply (unfold zcong_def dvd_def, auto)
   1.414 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.415    done
   1.416  
   1.417  lemma zcong_zadd:
   1.418      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
   1.419    apply (unfold zcong_def)
   1.420    apply (rule_tac s = "(a - b) + (c - d)" in subst)
   1.421 -   apply (rule_tac [2] zdvd_zadd)
   1.422 -    apply auto
   1.423 +   apply (rule_tac [2] zdvd_zadd, auto)
   1.424    done
   1.425  
   1.426  lemma zcong_zdiff:
   1.427      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
   1.428    apply (unfold zcong_def)
   1.429    apply (rule_tac s = "(a - b) - (c - d)" in subst)
   1.430 -   apply (rule_tac [2] zdvd_zdiff)
   1.431 -    apply auto
   1.432 +   apply (rule_tac [2] zdvd_zdiff, auto)
   1.433    done
   1.434  
   1.435  lemma zcong_trans:
   1.436      "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
   1.437 -  apply (unfold zcong_def dvd_def)
   1.438 -  apply auto
   1.439 +  apply (unfold zcong_def dvd_def, auto)
   1.440    apply (rule_tac x = "k + ka" in exI)
   1.441    apply (simp add: zadd_ac zadd_zmult_distrib2)
   1.442    done
   1.443 @@ -474,23 +428,18 @@
   1.444    done
   1.445  
   1.446  lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
   1.447 -  apply (rule zcong_zmult)
   1.448 -  apply simp_all
   1.449 -  done
   1.450 +  by (rule zcong_zmult, simp_all)
   1.451  
   1.452  lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)"
   1.453 -  apply (rule zcong_zmult)
   1.454 -  apply simp_all
   1.455 -  done
   1.456 +  by (rule zcong_zmult, simp_all)
   1.457  
   1.458  lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
   1.459    apply (unfold zcong_def)
   1.460 -  apply (rule zdvd_zdiff)
   1.461 -   apply simp_all
   1.462 +  apply (rule zdvd_zdiff, simp_all)
   1.463    done
   1.464  
   1.465  lemma zcong_square:
   1.466 -  "p \<in> zprime ==> 0 < a ==> [a * a = 1] (mod p)
   1.467 +   "[|p \<in> zprime;  0 < a;  [a * a = 1] (mod p)|]
   1.468      ==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)"
   1.469    apply (unfold zcong_def)
   1.470    apply (rule zprime_zdvd_zmult)
   1.471 @@ -514,21 +463,18 @@
   1.472       apply (simp_all add: zdiff_zmult_distrib)
   1.473    apply (subgoal_tac "m dvd (-(a * k - b * k))")
   1.474     apply (simp add: zminus_zdiff_eq)
   1.475 -  apply (subst zdvd_zminus_iff)
   1.476 -  apply assumption
   1.477 +  apply (subst zdvd_zminus_iff, assumption)
   1.478    done
   1.479  
   1.480  lemma zcong_cancel2:
   1.481    "0 \<le> m ==>
   1.482      zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
   1.483 -  apply (simp add: zmult_commute zcong_cancel)
   1.484 -  done
   1.485 +  by (simp add: zmult_commute zcong_cancel)
   1.486  
   1.487  lemma zcong_zgcd_zmult_zmod:
   1.488    "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1
   1.489      ==> [a = b] (mod m * n)"
   1.490 -  apply (unfold zcong_def dvd_def)
   1.491 -  apply auto
   1.492 +  apply (unfold zcong_def dvd_def, auto)
   1.493    apply (subgoal_tac "m dvd n * ka")
   1.494     apply (subgoal_tac "m dvd ka")
   1.495      apply (case_tac [2] "0 \<le> ka")
   1.496 @@ -547,17 +493,13 @@
   1.497  lemma zcong_zless_imp_eq:
   1.498    "0 \<le> a ==>
   1.499      a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
   1.500 -  apply (unfold zcong_def dvd_def)
   1.501 -  apply auto
   1.502 +  apply (unfold zcong_def dvd_def, auto)
   1.503    apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
   1.504 -  apply (cut_tac z = a and w = b in zless_linear)
   1.505 -  apply auto
   1.506 +  apply (cut_tac z = a and w = b in zless_linear, auto)
   1.507     apply (subgoal_tac [2] "(a - b) mod m = a - b")
   1.508 -    apply (rule_tac [3] mod_pos_pos_trivial)
   1.509 -     apply auto
   1.510 +    apply (rule_tac [3] mod_pos_pos_trivial, auto)
   1.511    apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")
   1.512 -   apply (rule_tac [2] mod_pos_pos_trivial)
   1.513 -    apply auto
   1.514 +   apply (rule_tac [2] mod_pos_pos_trivial, auto)
   1.515    done
   1.516  
   1.517  lemma zcong_square_zless:
   1.518 @@ -571,14 +513,12 @@
   1.519  lemma zcong_not:
   1.520      "0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)"
   1.521    apply (unfold zcong_def)
   1.522 -  apply (rule zdvd_not_zless)
   1.523 -   apply auto
   1.524 +  apply (rule zdvd_not_zless, auto)
   1.525    done
   1.526  
   1.527  lemma zcong_zless_0:
   1.528      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
   1.529 -  apply (unfold zcong_def dvd_def)
   1.530 -  apply auto
   1.531 +  apply (unfold zcong_def dvd_def, auto)
   1.532    apply (subgoal_tac "0 < m")
   1.533     apply (simp add: int_0_le_mult_iff)
   1.534     apply (subgoal_tac "m * k < m * 1")
   1.535 @@ -595,32 +535,29 @@
   1.536        apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le
   1.537          simp add: zcong_sym)
   1.538    apply (unfold zcong_def dvd_def)
   1.539 -  apply (rule_tac x = "a mod m" in exI)
   1.540 -  apply (auto)
   1.541 +  apply (rule_tac x = "a mod m" in exI, auto)
   1.542    apply (rule_tac x = "-(a div m)" in exI)
   1.543    apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
   1.544    done
   1.545  
   1.546  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
   1.547 -  apply (unfold zcong_def dvd_def)
   1.548 -  apply auto
   1.549 -   apply (rule_tac [!] x = "-k" in exI)
   1.550 -   apply auto
   1.551 +  apply (unfold zcong_def dvd_def, auto)
   1.552 +   apply (rule_tac [!] x = "-k" in exI, auto)
   1.553    done
   1.554  
   1.555  lemma zgcd_zcong_zgcd:
   1.556    "0 < m ==>
   1.557      zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1"
   1.558 -  apply (auto simp add: zcong_iff_lin)
   1.559 -  done
   1.560 +  by (auto simp add: zcong_iff_lin)
   1.561  
   1.562 -lemma zcong_zmod_aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   1.563 -by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
   1.564 +lemma zcong_zmod_aux:
   1.565 +     "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   1.566 +  by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
   1.567  
   1.568  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   1.569    apply (unfold zcong_def)
   1.570    apply (rule_tac t = "a - b" in ssubst)
   1.571 -  apply (rule_tac "m" = "m" in zcong_zmod_aux)
   1.572 +  apply (rule_tac "m" = m in zcong_zmod_aux)
   1.573    apply (rule trans)
   1.574     apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   1.575    apply (simp add: zadd_commute)
   1.576 @@ -630,21 +567,17 @@
   1.577    apply auto
   1.578     apply (rule_tac m = m in zcong_zless_imp_eq)
   1.579         prefer 5
   1.580 -       apply (subst zcong_zmod [symmetric])
   1.581 -       apply (simp_all)
   1.582 +       apply (subst zcong_zmod [symmetric], simp_all)
   1.583    apply (unfold zcong_def dvd_def)
   1.584    apply (rule_tac x = "a div m - b div m" in exI)
   1.585 -  apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
   1.586 -  apply auto
   1.587 +  apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans], auto)
   1.588    done
   1.589  
   1.590  lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)"
   1.591 -  apply (auto simp add: zcong_def)
   1.592 -  done
   1.593 +  by (auto simp add: zcong_def)
   1.594  
   1.595  lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)"
   1.596 -  apply (auto simp add: zcong_def)
   1.597 -  done
   1.598 +  by (auto simp add: zcong_def)
   1.599  
   1.600  lemma "[a = b] (mod m) = (a mod m = b mod m)"
   1.601    apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO)
   1.602 @@ -654,8 +587,7 @@
   1.603    txt{*Remainding case: @{term "m<0"}*}
   1.604    apply (rule_tac t = m in zminus_zminus [THEN subst])
   1.605    apply (subst zcong_zminus)
   1.606 -  apply (subst zcong_zmod_eq)
   1.607 -   apply arith
   1.608 +  apply (subst zcong_zmod_eq, arith)
   1.609    apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
   1.610    apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
   1.611    done
   1.612 @@ -664,14 +596,12 @@
   1.613  
   1.614  lemma zmod_zdvd_zmod:
   1.615      "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   1.616 -  apply (unfold dvd_def)
   1.617 -  apply auto
   1.618 +  apply (unfold dvd_def, auto)
   1.619    apply (subst zcong_zmod_eq [symmetric])
   1.620     prefer 2
   1.621     apply (subst zcong_iff_lin)
   1.622     apply (rule_tac x = "k * (a div (m * k))" in exI)
   1.623 -   apply(simp add:zmult_assoc [symmetric])
   1.624 -  apply assumption
   1.625 +   apply (simp add:zmult_assoc [symmetric], assumption)
   1.626    done
   1.627  
   1.628  
   1.629 @@ -685,16 +615,13 @@
   1.630    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   1.631      z = s and aa = t' and ab = t in xzgcda.induct)
   1.632    apply (subst zgcd_eq)
   1.633 -  apply (subst xzgcda.simps)
   1.634 -  apply auto
   1.635 +  apply (subst xzgcda.simps, auto)
   1.636    apply (case_tac "r' mod r = 0")
   1.637     prefer 2
   1.638 -   apply (frule_tac a = "r'" in pos_mod_sign)
   1.639 -   apply auto
   1.640 +   apply (frule_tac a = "r'" in pos_mod_sign, auto)
   1.641    apply (rule exI)
   1.642    apply (rule exI)
   1.643 -  apply (subst xzgcda.simps)
   1.644 -  apply auto
   1.645 +  apply (subst xzgcda.simps, auto)
   1.646    apply (simp add: zabs_def)
   1.647    done
   1.648  
   1.649 @@ -708,11 +635,9 @@
   1.650    apply (auto simp add: linorder_not_le)
   1.651    apply (case_tac "r' mod r = 0")
   1.652     prefer 2
   1.653 -   apply (frule_tac a = "r'" in pos_mod_sign)
   1.654 -   apply auto
   1.655 +   apply (frule_tac a = "r'" in pos_mod_sign, auto)
   1.656    apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   1.657 -  apply (subst xzgcda.simps)
   1.658 -  apply auto
   1.659 +  apply (subst xzgcda.simps, auto)
   1.660    apply (simp add: zabs_def)
   1.661    done
   1.662  
   1.663 @@ -721,8 +646,7 @@
   1.664    apply (unfold xzgcd_def)
   1.665    apply (rule iffI)
   1.666     apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
   1.667 -    apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp])
   1.668 -     apply auto
   1.669 +    apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp], auto)
   1.670    done
   1.671  
   1.672  
   1.673 @@ -730,9 +654,8 @@
   1.674  
   1.675  lemma xzgcda_linear_aux1:
   1.676    "(a - r * b) * m + (c - r * d) * (n::int) =
   1.677 -    (a * m + c * n) - r * (b * m + d * n)"
   1.678 -  apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
   1.679 -  done
   1.680 +   (a * m + c * n) - r * (b * m + d * n)"
   1.681 +  by (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
   1.682  
   1.683  lemma xzgcda_linear_aux2:
   1.684    "r' = s' * m + t' * n ==> r = s * m + t * n
   1.685 @@ -754,37 +677,31 @@
   1.686    apply (simp (no_asm))
   1.687    apply (rule impI)+
   1.688    apply (case_tac "r' mod r = 0")
   1.689 -   apply (simp add: xzgcda.simps)
   1.690 -   apply clarify
   1.691 +   apply (simp add: xzgcda.simps, clarify)
   1.692    apply (subgoal_tac "0 < r' mod r")
   1.693     apply (rule_tac [2] order_le_neq_implies_less)
   1.694     apply (rule_tac [2] pos_mod_sign)
   1.695      apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
   1.696 -      s = s and t' = t' and t = t in xzgcda_linear_aux2)
   1.697 -      apply auto
   1.698 +      s = s and t' = t' and t = t in xzgcda_linear_aux2, auto)
   1.699    done
   1.700  
   1.701  lemma xzgcd_linear:
   1.702      "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
   1.703    apply (unfold xzgcd_def)
   1.704 -  apply (erule xzgcda_linear)
   1.705 -    apply assumption
   1.706 +  apply (erule xzgcda_linear, assumption)
   1.707     apply auto
   1.708    done
   1.709  
   1.710  lemma zgcd_ex_linear:
   1.711      "0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
   1.712 -  apply (simp add: xzgcd_correct)
   1.713 -  apply safe
   1.714 +  apply (simp add: xzgcd_correct, safe)
   1.715    apply (rule exI)+
   1.716 -  apply (erule xzgcd_linear)
   1.717 -  apply auto
   1.718 +  apply (erule xzgcd_linear, auto)
   1.719    done
   1.720  
   1.721  lemma zcong_lineq_ex:
   1.722      "0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)"
   1.723 -  apply (cut_tac m = a and n = n and k = "1" in zgcd_ex_linear)
   1.724 -    apply safe
   1.725 +  apply (cut_tac m = a and n = n and k = 1 in zgcd_ex_linear, safe)
   1.726    apply (rule_tac x = s in exI)
   1.727    apply (rule_tac b = "s * a + t * n" in zcong_trans)
   1.728     prefer 2
   1.729 @@ -803,10 +720,8 @@
   1.730            apply (simp_all (no_asm_simp))
   1.731     prefer 2
   1.732     apply (simp add: zcong_sym)
   1.733 -  apply (cut_tac a = a and n = n in zcong_lineq_ex)
   1.734 -    apply auto
   1.735 -  apply (rule_tac x = "x * b mod n" in exI)
   1.736 -  apply safe
   1.737 +  apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
   1.738 +  apply (rule_tac x = "x * b mod n" in exI, safe)
   1.739      apply (simp_all (no_asm_simp))
   1.740    apply (subst zcong_zmod)
   1.741    apply (subst zmod_zmult1_eq [symmetric])