unified curried gcd, lcm, zgcd, zlcm
authorhaftmann
Mon Jul 14 11:04:42 2008 +0200 (2008-07-14)
changeset 27556292098f2efdf
parent 27555 dfda3192dec2
child 27557 151731493264
unified curried gcd, lcm, zgcd, zlcm
NEWS
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Complex/ex/Sqrt.thy
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Primes.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/NEWS	Fri Jul 11 23:17:25 2008 +0200
     1.2 +++ b/NEWS	Mon Jul 14 11:04:42 2008 +0200
     1.3 @@ -41,7 +41,20 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL-Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
     1.8 +* HOL/Library/GCD:  Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int);
     1.9 +carried together from various gcd/lcm developements in the HOL Distribution.
    1.10 +zgcd and zlcm replace former igcd and ilcm;  corresponding theorems renamed
    1.11 +accordingly.  INCOMPATIBILY.  To recover tupled syntax, use syntax declarations like:
    1.12 +
    1.13 +    hide (open) const gcd
    1.14 +    abbreviation gcd where
    1.15 +      "gcd == (%(a, b). GCD.gcd a b)"
    1.16 +    notation (output)
    1.17 +      GCD.gcd ("gcd '(_, _')")
    1.18 +
    1.19 +(analogously for lcm, zgcd, zlcm).
    1.20 +
    1.21 +* HOL/Real/Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
    1.22  
    1.23  * Integrated image HOL-Complex with HOL.  Entry points Main.thy and
    1.24  Complex_Main.thy remain as they are.
     2.1 --- a/src/HOL/Complex/ex/MIR.thy	Fri Jul 11 23:17:25 2008 +0200
     2.2 +++ b/src/HOL/Complex/ex/MIR.thy	Mon Jul 14 11:04:42 2008 +0200
     2.3 @@ -642,9 +642,9 @@
     2.4    done
     2.5  
     2.6  recdef numgcdh "measure size"
     2.7 -  "numgcdh (C i) = (\<lambda>g. igcd i g)"
     2.8 -  "numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
     2.9 -  "numgcdh (CF c s t) = (\<lambda>g. igcd c (numgcdh t g))"
    2.10 +  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
    2.11 +  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
    2.12 +  "numgcdh (CF c s t) = (\<lambda>g. zgcd c (numgcdh t g))"
    2.13    "numgcdh t = (\<lambda>g. 1)"
    2.14  
    2.15  definition
    2.16 @@ -687,13 +687,13 @@
    2.17    shows "Inum bs t = 0"
    2.18  proof-
    2.19    have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0"
    2.20 -    by (induct t rule: numgcdh.induct, auto simp add: igcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    2.21 +    by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    2.22    thus ?thesis using g0[simplified numgcd_def] by blast
    2.23  qed
    2.24  
    2.25  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    2.26    using gp
    2.27 -  by (induct t rule: numgcdh.induct, auto simp add: igcd_def)
    2.28 +  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
    2.29  
    2.30  lemma numgcd_pos: "numgcd t \<ge>0"
    2.31    by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
    2.32 @@ -738,8 +738,8 @@
    2.33    from ismaxcoeff_mono[OF H1 thh1] show ?case by (simp add: le_maxI1)
    2.34  qed simp_all
    2.35  
    2.36 -lemma igcd_gt1: "igcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
    2.37 -  apply (unfold igcd_def)
    2.38 +lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
    2.39 +  apply (unfold zgcd_def)
    2.40    apply (cases "i = 0", simp_all)
    2.41    apply (cases "j = 0", simp_all)
    2.42    apply (cases "abs i = 1", simp_all)
    2.43 @@ -747,7 +747,7 @@
    2.44    apply auto
    2.45    done
    2.46  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    2.47 -  by (induct t rule: numgcdh.induct, auto simp add:igcd0)
    2.48 +  by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
    2.49  
    2.50  lemma dvdnumcoeff_aux:
    2.51    assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
    2.52 @@ -756,17 +756,17 @@
    2.53  proof(induct t rule: numgcdh.induct)
    2.54    case (2 n c t) 
    2.55    let ?g = "numgcdh t m"
    2.56 -  from prems have th:"igcd c ?g > 1" by simp
    2.57 -  from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.58 +  from prems have th:"zgcd c ?g > 1" by simp
    2.59 +  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.60    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    2.61    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    2.62      have th: "dvdnumcoeff t ?g" by simp
    2.63 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    2.64 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
    2.65 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    2.66 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
    2.67    moreover {assume "abs c = 0 \<and> ?g > 1"
    2.68      with prems have th: "dvdnumcoeff t ?g" by simp
    2.69 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    2.70 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
    2.71 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    2.72 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
    2.73      hence ?case by simp }
    2.74    moreover {assume "abs c > 1" and g0:"?g = 0" 
    2.75      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    2.76 @@ -774,22 +774,22 @@
    2.77  next
    2.78    case (3 c s t) 
    2.79    let ?g = "numgcdh t m"
    2.80 -  from prems have th:"igcd c ?g > 1" by simp
    2.81 -  from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.82 +  from prems have th:"zgcd c ?g > 1" by simp
    2.83 +  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.84    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    2.85    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    2.86      have th: "dvdnumcoeff t ?g" by simp
    2.87 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    2.88 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
    2.89 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    2.90 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
    2.91    moreover {assume "abs c = 0 \<and> ?g > 1"
    2.92      with prems have th: "dvdnumcoeff t ?g" by simp
    2.93 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    2.94 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
    2.95 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    2.96 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
    2.97      hence ?case by simp }
    2.98    moreover {assume "abs c > 1" and g0:"?g = 0" 
    2.99      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   2.100    ultimately show ?case by blast
   2.101 -qed(auto simp add: igcd_dvd1)
   2.102 +qed(auto simp add: zgcd_dvd1)
   2.103  
   2.104  lemma dvdnumcoeff_aux2:
   2.105    assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
   2.106 @@ -1041,7 +1041,7 @@
   2.107  constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
   2.108    "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
   2.109     (let t' = simpnum t ; g = numgcd t' in 
   2.110 -      if g > 1 then (let g' = igcd n g in 
   2.111 +      if g > 1 then (let g' = zgcd n g in 
   2.112          if g' = 1 then (t',n) 
   2.113          else (reducecoeffh t' g', n div g')) 
   2.114        else (t',n))))"
   2.115 @@ -1052,23 +1052,23 @@
   2.116  proof-
   2.117    let ?t' = "simpnum t"
   2.118    let ?g = "numgcd ?t'"
   2.119 -  let ?g' = "igcd n ?g"
   2.120 +  let ?g' = "zgcd n ?g"
   2.121    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.122    moreover
   2.123    { assume nnz: "n \<noteq> 0"
   2.124      {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.125      moreover
   2.126      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.127 -      from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.128 -      hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.129 +      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.130 +      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.131        hence "?g'= 1 \<or> ?g' > 1" by arith
   2.132        moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.133        moreover {assume g'1:"?g'>1"
   2.134  	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
   2.135  	let ?tt = "reducecoeffh ?t' ?g'"
   2.136  	let ?t = "Inum bs ?tt"
   2.137 -	have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
   2.138 -	have gpdd: "?g' dvd n" by (simp add: igcd_dvd1) 
   2.139 +	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
   2.140 +	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
   2.141  	have gpdgp: "?g' dvd ?g'" by simp
   2.142  	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   2.143  	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   2.144 @@ -1088,21 +1088,21 @@
   2.145  proof-
   2.146      let ?t' = "simpnum t"
   2.147    let ?g = "numgcd ?t'"
   2.148 -  let ?g' = "igcd n ?g"
   2.149 +  let ?g' = "zgcd n ?g"
   2.150    {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   2.151    moreover
   2.152    { assume nnz: "n \<noteq> 0"
   2.153      {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}
   2.154      moreover
   2.155      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.156 -      from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.157 -      hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.158 +      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.159 +      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.160        hence "?g'= 1 \<or> ?g' > 1" by arith
   2.161        moreover {assume "?g'=1" hence ?thesis using prems 
   2.162  	  by (auto simp add: Let_def simp_num_pair_def)}
   2.163        moreover {assume g'1:"?g'>1"
   2.164 -	have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
   2.165 -	have gpdd: "?g' dvd n" by (simp add: igcd_dvd1) 
   2.166 +	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
   2.167 +	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
   2.168  	have gpdgp: "?g' dvd ?g'" by simp
   2.169  	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   2.170  	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
   2.171 @@ -1219,7 +1219,7 @@
   2.172  constdefs simpdvd:: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)"
   2.173    "simpdvd d t \<equiv> 
   2.174     (let g = numgcd t in 
   2.175 -      if g > 1 then (let g' = igcd d g in 
   2.176 +      if g > 1 then (let g' = zgcd d g in 
   2.177          if g' = 1 then (d, t) 
   2.178          else (d div g',reducecoeffh t g')) 
   2.179        else (d, t))"
   2.180 @@ -1228,20 +1228,20 @@
   2.181    shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)"
   2.182  proof-
   2.183    let ?g = "numgcd t"
   2.184 -  let ?g' = "igcd d ?g"
   2.185 +  let ?g' = "zgcd d ?g"
   2.186    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)}
   2.187    moreover
   2.188    {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.189 -    from igcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
   2.190 -    hence g'p: "?g' > 0" using igcd_pos[where i="d" and j="numgcd t"] by arith
   2.191 +    from zgcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
   2.192 +    hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="numgcd t"] by arith
   2.193      hence "?g'= 1 \<or> ?g' > 1" by arith
   2.194      moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}
   2.195      moreover {assume g'1:"?g'>1"
   2.196        from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
   2.197        let ?tt = "reducecoeffh t ?g'"
   2.198        let ?t = "Inum bs ?tt"
   2.199 -      have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
   2.200 -      have gpdd: "?g' dvd d" by (simp add: igcd_dvd1) 
   2.201 +      have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
   2.202 +      have gpdd: "?g' dvd d" by (simp add: zgcd_dvd1) 
   2.203        have gpdgp: "?g' dvd ?g'" by simp
   2.204        from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   2.205        have th2:"real ?g' * ?t = Inum bs t" by simp
   2.206 @@ -2093,8 +2093,8 @@
   2.207    "plusinf p = p"
   2.208  
   2.209  recdef \<delta> "measure size"
   2.210 -  "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)" 
   2.211 -  "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)" 
   2.212 +  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
   2.213 +  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
   2.214    "\<delta> (Dvd i (CN 0 c e)) = i"
   2.215    "\<delta> (NDvd i (CN 0 c e)) = i"
   2.216    "\<delta> p = 1"
   2.217 @@ -2126,20 +2126,20 @@
   2.218  proof (induct p rule: iszlfm.induct)
   2.219    case (1 p q) 
   2.220    let ?d = "\<delta> (And p q)"
   2.221 -  from prems ilcm_pos have dp: "?d >0" by simp
   2.222 +  from prems zlcm_pos have dp: "?d >0" by simp
   2.223    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
   2.224     hence th: "d\<delta> p ?d" 
   2.225 -     using delta_mono prems by (auto simp del: dvd_ilcm_self1)
   2.226 +     using delta_mono prems by (auto simp del: dvd_zlcm_self1)
   2.227    have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 
   2.228 -  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2)
   2.229 +  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_zlcm_self2)
   2.230    from th th' dp show ?case by simp 
   2.231  next
   2.232    case (2 p q)  
   2.233    let ?d = "\<delta> (And p q)"
   2.234 -  from prems ilcm_pos have dp: "?d >0" by simp
   2.235 +  from prems zlcm_pos have dp: "?d >0" by simp
   2.236    have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
   2.237 -    by (auto simp del: dvd_ilcm_self1)
   2.238 -  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2)
   2.239 +    by (auto simp del: dvd_zlcm_self1)
   2.240 +  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_zlcm_self2)
   2.241    from th th' dp show ?case by simp 
   2.242  qed simp_all
   2.243  
   2.244 @@ -2388,8 +2388,8 @@
   2.245    "d\<beta> p = (\<lambda> k. True)"
   2.246  
   2.247  recdef \<zeta> "measure size"
   2.248 -  "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)" 
   2.249 -  "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)" 
   2.250 +  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   2.251 +  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   2.252    "\<zeta> (Eq  (CN 0 c e)) = c"
   2.253    "\<zeta> (NEq (CN 0 c e)) = c"
   2.254    "\<zeta> (Lt  (CN 0 c e)) = c"
   2.255 @@ -2510,19 +2510,19 @@
   2.256  using linp
   2.257  proof(induct p rule: iszlfm.induct)
   2.258    case (1 p q)
   2.259 -  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   2.260 -  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   2.261 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   2.262 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   2.263 -    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
   2.264 +  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.265 +  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.266 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.267 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.268 +    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   2.269  next
   2.270    case (2 p q)
   2.271 -  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   2.272 -  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   2.273 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   2.274 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   2.275 -    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
   2.276 -qed (auto simp add: ilcm_pos)
   2.277 +  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.278 +  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.279 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.280 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.281 +    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   2.282 +qed (auto simp add: zlcm_pos)
   2.283  
   2.284  lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
   2.285    shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"
   2.286 @@ -4171,9 +4171,9 @@
   2.287  
   2.288  lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
   2.289    by (induct p rule: isrlfm.induct, auto)
   2.290 -lemma igcd_le1: assumes ip: "0 < i" shows "igcd i j \<le> i"
   2.291 +lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
   2.292  proof-
   2.293 -  from igcd_dvd1 have th: "igcd i j dvd i" by blast
   2.294 +  from zgcd_dvd1 have th: "zgcd i j dvd i" by blast
   2.295    from zdvd_imp_le[OF th ip] show ?thesis .
   2.296  qed
   2.297  
   2.298 @@ -4195,7 +4195,7 @@
   2.299        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.300        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.301        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.302 -	by (simp add: numgcd_def igcd_le1)
   2.303 +	by (simp add: numgcd_def zgcd_le1)
   2.304        from prems have th': "c\<noteq>0" by auto
   2.305        from prems have cp: "c \<ge> 0" by simp
   2.306        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.307 @@ -4220,7 +4220,7 @@
   2.308        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.309        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.310        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.311 -	by (simp add: numgcd_def igcd_le1)
   2.312 +	by (simp add: numgcd_def zgcd_le1)
   2.313        from prems have th': "c\<noteq>0" by auto
   2.314        from prems have cp: "c \<ge> 0" by simp
   2.315        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.316 @@ -4245,7 +4245,7 @@
   2.317        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.318        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.319        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.320 -	by (simp add: numgcd_def igcd_le1)
   2.321 +	by (simp add: numgcd_def zgcd_le1)
   2.322        from prems have th': "c\<noteq>0" by auto
   2.323        from prems have cp: "c \<ge> 0" by simp
   2.324        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.325 @@ -4270,7 +4270,7 @@
   2.326        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.327        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.328        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.329 -	by (simp add: numgcd_def igcd_le1)
   2.330 +	by (simp add: numgcd_def zgcd_le1)
   2.331        from prems have th': "c\<noteq>0" by auto
   2.332        from prems have cp: "c \<ge> 0" by simp
   2.333        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.334 @@ -4295,7 +4295,7 @@
   2.335        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.336        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.337        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.338 -	by (simp add: numgcd_def igcd_le1)
   2.339 +	by (simp add: numgcd_def zgcd_le1)
   2.340        from prems have th': "c\<noteq>0" by auto
   2.341        from prems have cp: "c \<ge> 0" by simp
   2.342        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.343 @@ -4320,7 +4320,7 @@
   2.344        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   2.345        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   2.346        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   2.347 -	by (simp add: numgcd_def igcd_le1)
   2.348 +	by (simp add: numgcd_def zgcd_le1)
   2.349        from prems have th': "c\<noteq>0" by auto
   2.350        from prems have cp: "c \<ge> 0" by simp
   2.351        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   2.352 @@ -5117,9 +5117,9 @@
   2.353    let ?M = "?I x (minusinf ?rq)"
   2.354    let ?P = "?I x (plusinf ?rq)"
   2.355    have MF: "?M = False"
   2.356 -    apply (simp add: Let_def reducecoeff_def numgcd_def igcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.357 +    apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.358      by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
   2.359 -  have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def igcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.360 +  have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.361      by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
   2.362    have "(\<exists> x. ?I x ?q ) = 
   2.363      ((?I x (minusinf ?rq)) \<or> (?I x (plusinf ?rq )) \<or> (\<exists> (t,n) \<in> set (\<Upsilon> ?rq). \<exists> (s,m) \<in> set (\<Upsilon> ?rq ). ?I x (\<upsilon> ?rq (Add (Mul m t) (Mul n s), 2*n*m))))"
   2.364 @@ -5284,7 +5284,7 @@
   2.365    let ?F = "\<lambda> p. \<exists> a \<in> set (\<Upsilon> p). \<exists> b \<in> set (\<Upsilon> p). ?I x (\<upsilon> p (?g(a,b)))"
   2.366    let ?ep = "evaldjf (\<upsilon> ?q) ?Y"
   2.367    from rlfm_l[OF qf] have lq: "isrlfm ?q" 
   2.368 -    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def igcd_def)
   2.369 +    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def zgcd_def)
   2.370    from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   2.371    from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   2.372    from U_l UpU 
     3.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Jul 11 23:17:25 2008 +0200
     3.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Jul 14 11:04:42 2008 +0200
     3.3 @@ -478,8 +478,8 @@
     3.4    by (induct t rule: maxcoeff.induct, auto)
     3.5  
     3.6  recdef numgcdh "measure size"
     3.7 -  "numgcdh (C i) = (\<lambda>g. igcd i g)"
     3.8 -  "numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
     3.9 +  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
    3.10 +  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
    3.11    "numgcdh t = (\<lambda>g. 1)"
    3.12  defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
    3.13  
    3.14 @@ -512,11 +512,11 @@
    3.15    assumes g0: "numgcd t = 0"
    3.16    shows "Inum bs t = 0"
    3.17    using g0[simplified numgcd_def] 
    3.18 -  by (induct t rule: numgcdh.induct, auto simp add: igcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    3.19 +  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    3.20  
    3.21  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    3.22    using gp
    3.23 -  by (induct t rule: numgcdh.induct, auto simp add: igcd_def)
    3.24 +  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
    3.25  
    3.26  lemma numgcd_pos: "numgcd t \<ge>0"
    3.27    by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
    3.28 @@ -551,15 +551,15 @@
    3.29    from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
    3.30  qed simp_all
    3.31  
    3.32 -lemma igcd_gt1: "igcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
    3.33 -  apply (cases "abs i = 0", simp_all add: igcd_def)
    3.34 +lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
    3.35 +  apply (cases "abs i = 0", simp_all add: zgcd_def)
    3.36    apply (cases "abs j = 0", simp_all)
    3.37    apply (cases "abs i = 1", simp_all)
    3.38    apply (cases "abs j = 1", simp_all)
    3.39    apply auto
    3.40    done
    3.41  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    3.42 -  by (induct t rule: numgcdh.induct, auto simp add:igcd0)
    3.43 +  by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
    3.44  
    3.45  lemma dvdnumcoeff_aux:
    3.46    assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
    3.47 @@ -568,22 +568,22 @@
    3.48  proof(induct t rule: numgcdh.induct)
    3.49    case (2 n c t) 
    3.50    let ?g = "numgcdh t m"
    3.51 -  from prems have th:"igcd c ?g > 1" by simp
    3.52 -  from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    3.53 +  from prems have th:"zgcd c ?g > 1" by simp
    3.54 +  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    3.55    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    3.56    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    3.57      have th: "dvdnumcoeff t ?g" by simp
    3.58 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    3.59 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
    3.60 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    3.61 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
    3.62    moreover {assume "abs c = 0 \<and> ?g > 1"
    3.63      with prems have th: "dvdnumcoeff t ?g" by simp
    3.64 -    have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
    3.65 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
    3.66 +    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
    3.67 +    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
    3.68      hence ?case by simp }
    3.69    moreover {assume "abs c > 1" and g0:"?g = 0" 
    3.70      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    3.71    ultimately show ?case by blast
    3.72 -qed(auto simp add: igcd_dvd1)
    3.73 +qed(auto simp add: zgcd_dvd1)
    3.74  
    3.75  lemma dvdnumcoeff_aux2:
    3.76    assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
    3.77 @@ -727,7 +727,7 @@
    3.78  constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
    3.79    "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
    3.80     (let t' = simpnum t ; g = numgcd t' in 
    3.81 -      if g > 1 then (let g' = igcd n g in 
    3.82 +      if g > 1 then (let g' = zgcd n g in 
    3.83          if g' = 1 then (t',n) 
    3.84          else (reducecoeffh t' g', n div g')) 
    3.85        else (t',n))))"
    3.86 @@ -738,23 +738,23 @@
    3.87  proof-
    3.88    let ?t' = "simpnum t"
    3.89    let ?g = "numgcd ?t'"
    3.90 -  let ?g' = "igcd n ?g"
    3.91 +  let ?g' = "zgcd n ?g"
    3.92    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
    3.93    moreover
    3.94    { assume nnz: "n \<noteq> 0"
    3.95      {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
    3.96      moreover
    3.97      {assume g1:"?g>1" hence g0: "?g > 0" by simp
    3.98 -      from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
    3.99 -      hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith 
   3.100 +      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   3.101 +      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith 
   3.102        hence "?g'= 1 \<or> ?g' > 1" by arith
   3.103        moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
   3.104        moreover {assume g'1:"?g'>1"
   3.105  	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
   3.106  	let ?tt = "reducecoeffh ?t' ?g'"
   3.107  	let ?t = "Inum bs ?tt"
   3.108 -	have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
   3.109 -	have gpdd: "?g' dvd n" by (simp add: igcd_dvd1) 
   3.110 +	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
   3.111 +	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
   3.112  	have gpdgp: "?g' dvd ?g'" by simp
   3.113  	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   3.114  	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   3.115 @@ -774,21 +774,21 @@
   3.116  proof-
   3.117      let ?t' = "simpnum t"
   3.118    let ?g = "numgcd ?t'"
   3.119 -  let ?g' = "igcd n ?g"
   3.120 +  let ?g' = "zgcd n ?g"
   3.121    {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   3.122    moreover
   3.123    { assume nnz: "n \<noteq> 0"
   3.124      {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   3.125      moreover
   3.126      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   3.127 -      from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   3.128 -      hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
   3.129 +      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   3.130 +      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   3.131        hence "?g'= 1 \<or> ?g' > 1" by arith
   3.132        moreover {assume "?g'=1" hence ?thesis using prems 
   3.133  	  by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   3.134        moreover {assume g'1:"?g'>1"
   3.135 -	have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
   3.136 -	have gpdd: "?g' dvd n" by (simp add: igcd_dvd1) 
   3.137 +	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
   3.138 +	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
   3.139  	have gpdgp: "?g' dvd ?g'" by simp
   3.140  	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   3.141  	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
     4.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Fri Jul 11 23:17:25 2008 +0200
     4.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Mon Jul 14 11:04:42 2008 +0200
     4.3 @@ -23,16 +23,16 @@
     4.4  
     4.5  theorem rationals_rep [elim?]:
     4.6    assumes "x \<in> \<rat>"
     4.7 -  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1"
     4.8 +  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
     4.9  proof -
    4.10    from `x \<in> \<rat>` obtain m n :: nat where
    4.11        n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
    4.12      unfolding rationals_def by blast
    4.13 -  let ?gcd = "gcd (m, n)"
    4.14 +  let ?gcd = "gcd m n"
    4.15    from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    4.16    let ?k = "m div ?gcd"
    4.17    let ?l = "n div ?gcd"
    4.18 -  let ?gcd' = "gcd (?k, ?l)"
    4.19 +  let ?gcd' = "gcd ?k ?l"
    4.20    have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
    4.21      by (rule dvd_mult_div_cancel)
    4.22    have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
    4.23 @@ -52,7 +52,7 @@
    4.24    moreover
    4.25    have "?gcd' = 1"
    4.26    proof -
    4.27 -    have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
    4.28 +    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
    4.29        by (rule gcd_mult_distrib2)
    4.30      with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    4.31      with gcd show ?thesis by simp
    4.32 @@ -76,7 +76,7 @@
    4.33    assume "sqrt (real p) \<in> \<rat>"
    4.34    then obtain m n where
    4.35        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    4.36 -    and gcd: "gcd (m, n) = 1" ..
    4.37 +    and gcd: "gcd m n = 1" ..
    4.38    have eq: "m\<twosuperior> = p * n\<twosuperior>"
    4.39    proof -
    4.40      from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    4.41 @@ -96,7 +96,7 @@
    4.42      then have "p dvd n\<twosuperior>" ..
    4.43      with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
    4.44    qed
    4.45 -  then have "p dvd gcd (m, n)" ..
    4.46 +  then have "p dvd gcd m n" ..
    4.47    with gcd have "p dvd 1" by simp
    4.48    then have "p \<le> 1" by (simp add: dvd_imp_le)
    4.49    with p show False by simp
    4.50 @@ -122,7 +122,7 @@
    4.51    assume "sqrt (real p) \<in> \<rat>"
    4.52    then obtain m n where
    4.53        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    4.54 -    and gcd: "gcd (m, n) = 1" ..
    4.55 +    and gcd: "gcd m n = 1" ..
    4.56    from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    4.57    then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    4.58      by (auto simp add: power2_eq_square)
    4.59 @@ -136,7 +136,7 @@
    4.60    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
    4.61    then have "p dvd n\<twosuperior>" ..
    4.62    with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
    4.63 -  with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
    4.64 +  with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
    4.65    with gcd have "p dvd 1" by simp
    4.66    then have "p \<le> 1" by (simp add: dvd_imp_le)
    4.67    with p show False by simp
     5.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Fri Jul 11 23:17:25 2008 +0200
     5.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Jul 14 11:04:42 2008 +0200
     5.3 @@ -70,55 +70,55 @@
     5.4    finally show "?P (n + 2)" .
     5.5  qed
     5.6  
     5.7 -lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
     5.8 +lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
     5.9  proof (induct n rule: fib_induct)
    5.10    show "?P 0" by simp
    5.11    show "?P 1" by simp
    5.12    fix n
    5.13    have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
    5.14      by simp
    5.15 -  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
    5.16 +  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
    5.17      by (simp only: gcd_add2')
    5.18 -  also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
    5.19 +  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
    5.20      by (simp add: gcd_commute)
    5.21    also assume "... = 1"
    5.22    finally show "?P (n + 2)" .
    5.23  qed
    5.24  
    5.25 -lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
    5.26 +lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n"
    5.27  proof -
    5.28    assume "0 < n"
    5.29 -  then have "gcd (n * k + m, n) = gcd (n, m mod n)"
    5.30 +  then have "gcd (n * k + m) n = gcd n (m mod n)"
    5.31      by (simp add: gcd_non_0 add_commute)
    5.32 -  also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0)
    5.33 +  also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)
    5.34    finally show ?thesis .
    5.35  qed
    5.36  
    5.37 -lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
    5.38 +lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
    5.39  proof (cases m)
    5.40    case 0
    5.41    then show ?thesis by simp
    5.42  next
    5.43    case (Suc k)
    5.44 -  then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
    5.45 +  then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
    5.46      by (simp add: gcd_commute)
    5.47    also have "fib (n + k + 1)
    5.48      = fib (k + 1) * fib (n + 1) + fib k * fib n"
    5.49      by (rule fib_add)
    5.50 -  also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
    5.51 +  also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
    5.52      by (simp add: gcd_mult_add)
    5.53 -  also have "... = gcd (fib n, fib (k + 1))"
    5.54 +  also have "... = gcd (fib n) (fib (k + 1))"
    5.55      by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
    5.56 -  also have "... = gcd (fib m, fib n)"
    5.57 +  also have "... = gcd (fib m) (fib n)"
    5.58      using Suc by (simp add: gcd_commute)
    5.59    finally show ?thesis .
    5.60  qed
    5.61  
    5.62  lemma gcd_fib_diff:
    5.63    assumes "m <= n"
    5.64 -  shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
    5.65 +  shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
    5.66  proof -
    5.67 -  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
    5.68 +  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
    5.69      by (simp add: gcd_fib_add)
    5.70    also from `m <= n` have "n - m + m = n" by simp
    5.71    finally show ?thesis .
    5.72 @@ -126,25 +126,25 @@
    5.73  
    5.74  lemma gcd_fib_mod:
    5.75    assumes "0 < m"
    5.76 -  shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    5.77 +  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
    5.78  proof (induct n rule: nat_less_induct)
    5.79    case (1 n) note hyp = this
    5.80    show ?case
    5.81    proof -
    5.82      have "n mod m = (if n < m then n else (n - m) mod m)"
    5.83        by (rule mod_if)
    5.84 -    also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
    5.85 +    also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
    5.86      proof (cases "n < m")
    5.87        case True then show ?thesis by simp
    5.88      next
    5.89        case False then have "m <= n" by simp
    5.90        from `0 < m` and False have "n - m < n" by simp
    5.91 -      with hyp have "gcd (fib m, fib ((n - m) mod m))
    5.92 -        = gcd (fib m, fib (n - m))" by simp
    5.93 -      also have "... = gcd (fib m, fib n)"
    5.94 +      with hyp have "gcd (fib m) (fib ((n - m) mod m))
    5.95 +        = gcd (fib m) (fib (n - m))" by simp
    5.96 +      also have "... = gcd (fib m) (fib n)"
    5.97          using `m <= n` by (rule gcd_fib_diff)
    5.98 -      finally have "gcd (fib m, fib ((n - m) mod m)) =
    5.99 -        gcd (fib m, fib n)" .
   5.100 +      finally have "gcd (fib m) (fib ((n - m) mod m)) =
   5.101 +        gcd (fib m) (fib n)" .
   5.102        with False show ?thesis by simp
   5.103      qed
   5.104      finally show ?thesis .
   5.105 @@ -152,15 +152,15 @@
   5.106  qed
   5.107  
   5.108  
   5.109 -theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
   5.110 +theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
   5.111  proof (induct m n rule: gcd_induct)
   5.112 -  fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
   5.113 +  fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
   5.114    fix n :: nat assume n: "0 < n"
   5.115 -  then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
   5.116 -  also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
   5.117 -  also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
   5.118 -  also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
   5.119 -  finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
   5.120 +  then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0)
   5.121 +  also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
   5.122 +  also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
   5.123 +  also have "... = gcd (fib m) (fib n)" by (rule gcd_commute)
   5.124 +  finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
   5.125  qed
   5.126  
   5.127  end
     6.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Jul 11 23:17:25 2008 +0200
     6.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Jul 14 11:04:42 2008 +0200
     6.3 @@ -22,13 +22,13 @@
     6.4  definition
     6.5    isnormNum :: "Num \<Rightarrow> bool"
     6.6  where
     6.7 -  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))"
     6.8 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> zgcd a b = 1))"
     6.9  
    6.10  definition
    6.11    normNum :: "Num \<Rightarrow> Num"
    6.12  where
    6.13    "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    6.14 -  (let g = igcd a b 
    6.15 +  (let g = zgcd a b 
    6.16     in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    6.17  
    6.18  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    6.19 @@ -38,19 +38,19 @@
    6.20    {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    6.21    moreover
    6.22    {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    6.23 -    let ?g = "igcd a b"
    6.24 +    let ?g = "zgcd a b"
    6.25      let ?a' = "a div ?g"
    6.26      let ?b' = "b div ?g"
    6.27 -    let ?g' = "igcd ?a' ?b'"
    6.28 -    from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b] 
    6.29 +    let ?g' = "zgcd ?a' ?b'"
    6.30 +    from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
    6.31      have gpos: "?g > 0"  by arith
    6.32 -    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
    6.33 +    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
    6.34      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    6.35      anz bnz
    6.36      have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    6.37 -      by - (rule notI,simp add:igcd_def)+
    6.38 +      by - (rule notI,simp add:zgcd_def)+
    6.39      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
    6.40 -    from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
    6.41 +    from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
    6.42      from bnz have "b < 0 \<or> b > 0" by arith
    6.43      moreover
    6.44      {assume b: "b > 0"
    6.45 @@ -84,7 +84,7 @@
    6.46  definition
    6.47    Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    6.48  where
    6.49 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b') 
    6.50 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b') 
    6.51      in (a*a' div g, b*b' div g))"
    6.52  
    6.53  definition
    6.54 @@ -120,11 +120,11 @@
    6.55    then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
    6.56    {assume "a = 0"
    6.57      hence ?thesis using xn ab ab'
    6.58 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
    6.59 +      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    6.60    moreover
    6.61    {assume "a' = 0"
    6.62      hence ?thesis using yn ab ab' 
    6.63 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
    6.64 +      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    6.65    moreover
    6.66    {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
    6.67      hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
    6.68 @@ -136,11 +136,11 @@
    6.69  
    6.70  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    6.71    by (simp add: Ninv_def isnormNum_def split_def)
    6.72 -    (cases "fst x = 0", auto simp add: igcd_commute)
    6.73 +    (cases "fst x = 0", auto simp add: zgcd_commute)
    6.74  
    6.75  lemma isnormNum_int[simp]: 
    6.76    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    6.77 -  by (simp_all add: isnormNum_def igcd_def)
    6.78 +  by (simp_all add: isnormNum_def zgcd_def)
    6.79  
    6.80  
    6.81  text {* Relations over Num *}
    6.82 @@ -201,8 +201,8 @@
    6.83      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    6.84      from prems have eq:"a * b' = a'*b" 
    6.85        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    6.86 -    from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"       
    6.87 -      by (simp_all add: isnormNum_def add: igcd_commute)
    6.88 +    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
    6.89 +      by (simp_all add: isnormNum_def add: zgcd_commute)
    6.90      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
    6.91        apply(unfold dvd_def)
    6.92        apply (rule_tac x="b'" in exI, simp add: mult_ac)
    6.93 @@ -257,7 +257,7 @@
    6.94        by (simp add: INum_def normNum_def split_def Let_def)}
    6.95    moreover 
    6.96    {assume a: "a\<noteq>0" and b: "b\<noteq>0"
    6.97 -    let ?g = "igcd a b"
    6.98 +    let ?g = "zgcd a b"
    6.99      from a b have g: "?g \<noteq> 0"by simp
   6.100      from of_int_div[OF g, where ?'a = 'a]
   6.101      have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
   6.102 @@ -293,13 +293,13 @@
   6.103        from z aa' bb' have ?thesis 
   6.104  	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   6.105      moreover {assume z: "a * b' + b * a' \<noteq> 0"
   6.106 -      let ?g = "igcd (a * b' + b * a') (b*b')"
   6.107 +      let ?g = "zgcd (a * b' + b * a') (b*b')"
   6.108        have gz: "?g \<noteq> 0" using z by simp
   6.109        have ?thesis using aa' bb' z gz
   6.110  	of_int_div[where ?'a = 'a, 
   6.111 -	OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
   6.112 +	OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
   6.113  	of_int_div[where ?'a = 'a,
   6.114 -	OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
   6.115 +	OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
   6.116  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   6.117      ultimately have ?thesis using aa' bb' 
   6.118        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   6.119 @@ -318,10 +318,10 @@
   6.120        done }
   6.121    moreover
   6.122    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   6.123 -    let ?g="igcd (a*a') (b*b')"
   6.124 +    let ?g="zgcd (a*a') (b*b')"
   6.125      have gz: "?g \<noteq> 0" using z by simp
   6.126 -    from z of_int_div[where ?'a = 'a, OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]] 
   6.127 -      of_int_div[where ?'a = 'a , OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]] 
   6.128 +    from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]] 
   6.129 +      of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]] 
   6.130      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   6.131    ultimately show ?thesis by blast
   6.132  qed
   6.133 @@ -456,7 +456,7 @@
   6.134  qed
   6.135  
   6.136  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   6.137 -  by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
   6.138 +  by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
   6.139  
   6.140  lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   6.141    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
     7.1 --- a/src/HOL/Library/GCD.thy	Fri Jul 11 23:17:25 2008 +0200
     7.2 +++ b/src/HOL/Library/GCD.thy	Mon Jul 14 11:04:42 2008 +0200
     7.3 @@ -18,64 +18,62 @@
     7.4  
     7.5  definition
     7.6    is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
     7.7 -  [code func del]: "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     7.8 +  [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     7.9      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    7.10  
    7.11  text {* Uniqueness *}
    7.12  
    7.13 -lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
    7.14 +lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
    7.15    by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
    7.16  
    7.17  text {* Connection to divides relation *}
    7.18  
    7.19 -lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
    7.20 +lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
    7.21    by (auto simp add: is_gcd_def)
    7.22  
    7.23  text {* Commutativity *}
    7.24  
    7.25 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
    7.26 +lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
    7.27    by (auto simp add: is_gcd_def)
    7.28  
    7.29  
    7.30  subsection {* GCD on nat by Euclid's algorithm *}
    7.31  
    7.32 -fun
    7.33 -  gcd  :: "nat \<times> nat => nat"
    7.34 -where
    7.35 -  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    7.36 +fun gcd  :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    7.37 +  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
    7.38  
    7.39 -lemma gcd_induct:
    7.40 +thm gcd.induct
    7.41 +
    7.42 +lemma gcd_induct [case_names "0" rec]:
    7.43    fixes m n :: nat
    7.44    assumes "\<And>m. P m 0"
    7.45      and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
    7.46    shows "P m n"
    7.47 -apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
    7.48 -apply (case_tac "n = 0")
    7.49 -apply simp_all
    7.50 -using assms apply simp_all
    7.51 -done
    7.52 +proof (induct m n rule: gcd.induct)
    7.53 +  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
    7.54 +qed
    7.55  
    7.56 -lemma gcd_0 [simp]: "gcd (m, 0) = m"
    7.57 +lemma gcd_0 [simp]: "gcd m 0 = m"
    7.58    by simp
    7.59  
    7.60 -lemma gcd_0_left [simp]: "gcd (0, m) = m"
    7.61 +lemma gcd_0_left [simp]: "gcd 0 m = m"
    7.62    by simp
    7.63  
    7.64 -lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
    7.65 +lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
    7.66    by simp
    7.67  
    7.68 -lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    7.69 +lemma gcd_1 [simp]: "gcd m (Suc 0) = 1"
    7.70    by simp
    7.71  
    7.72  declare gcd.simps [simp del]
    7.73  
    7.74  text {*
    7.75 -  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    7.76 +  \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
    7.77    conjunctions don't seem provable separately.
    7.78  *}
    7.79  
    7.80 -lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
    7.81 -  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
    7.82 +lemma gcd_dvd1 [iff]: "gcd m n dvd m"
    7.83 +  and gcd_dvd2 [iff]: "gcd m n dvd n"
    7.84    apply (induct m n rule: gcd_induct)
    7.85       apply (simp_all add: gcd_non_0)
    7.86    apply (blast dest: dvd_mod_imp_dvd)
    7.87 @@ -84,50 +82,50 @@
    7.88  text {*
    7.89    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    7.90    naturals, if @{term k} divides @{term m} and @{term k} divides
    7.91 -  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    7.92 +  @{term n} then @{term k} divides @{term "gcd m n"}.
    7.93  *}
    7.94  
    7.95 -lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
    7.96 +lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    7.97    by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
    7.98  
    7.99  text {*
   7.100    \medskip Function gcd yields the Greatest Common Divisor.
   7.101  *}
   7.102  
   7.103 -lemma is_gcd: "is_gcd (gcd (m, n)) m n"
   7.104 +lemma is_gcd: "is_gcd m n (gcd m n) "
   7.105    by (simp add: is_gcd_def gcd_greatest)
   7.106  
   7.107  
   7.108  subsection {* Derived laws for GCD *}
   7.109  
   7.110 -lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
   7.111 +lemma gcd_greatest_iff [iff]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   7.112    by (blast intro!: gcd_greatest intro: dvd_trans)
   7.113  
   7.114 -lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   7.115 +lemma gcd_zero: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   7.116    by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   7.117  
   7.118 -lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   7.119 +lemma gcd_commute: "gcd m n = gcd n m"
   7.120    apply (rule is_gcd_unique)
   7.121     apply (rule is_gcd)
   7.122    apply (subst is_gcd_commute)
   7.123    apply (simp add: is_gcd)
   7.124    done
   7.125  
   7.126 -lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   7.127 +lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
   7.128    apply (rule is_gcd_unique)
   7.129     apply (rule is_gcd)
   7.130    apply (simp add: is_gcd_def)
   7.131    apply (blast intro: dvd_trans)
   7.132    done
   7.133  
   7.134 -lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
   7.135 +lemma gcd_1_left [simp]: "gcd (Suc 0) m = 1"
   7.136    by (simp add: gcd_commute)
   7.137  
   7.138  text {*
   7.139    \medskip Multiplication laws
   7.140  *}
   7.141  
   7.142 -lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   7.143 +lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
   7.144      -- {* \cite[page 27]{davenport92} *}
   7.145    apply (induct m n rule: gcd_induct)
   7.146     apply simp
   7.147 @@ -135,26 +133,26 @@
   7.148     apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   7.149    done
   7.150  
   7.151 -lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   7.152 +lemma gcd_mult [simp]: "gcd k (k * n) = k"
   7.153    apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   7.154    done
   7.155  
   7.156 -lemma gcd_self [simp]: "gcd (k, k) = k"
   7.157 +lemma gcd_self [simp]: "gcd k k = k"
   7.158    apply (rule gcd_mult [of k 1, simplified])
   7.159    done
   7.160  
   7.161 -lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   7.162 +lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
   7.163    apply (insert gcd_mult_distrib2 [of m k n])
   7.164    apply simp
   7.165    apply (erule_tac t = m in ssubst)
   7.166    apply simp
   7.167    done
   7.168  
   7.169 -lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   7.170 +lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
   7.171    apply (blast intro: relprime_dvd_mult dvd_trans)
   7.172    done
   7.173  
   7.174 -lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   7.175 +lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   7.176    apply (rule dvd_anti_sym)
   7.177     apply (rule gcd_greatest)
   7.178      apply (rule_tac n = k in relprime_dvd_mult)
   7.179 @@ -167,29 +165,29 @@
   7.180  
   7.181  text {* \medskip Addition laws *}
   7.182  
   7.183 -lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   7.184 +lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   7.185    apply (case_tac "n = 0")
   7.186     apply (simp_all add: gcd_non_0)
   7.187    done
   7.188  
   7.189 -lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   7.190 +lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
   7.191  proof -
   7.192 -  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
   7.193 -  also have "... = gcd (n + m, m)" by (simp add: add_commute)
   7.194 -  also have "... = gcd (n, m)" by simp
   7.195 -  also have  "... = gcd (m, n)" by (rule gcd_commute)
   7.196 +  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
   7.197 +  also have "... = gcd (n + m) m" by (simp add: add_commute)
   7.198 +  also have "... = gcd n m" by simp
   7.199 +  also have  "... = gcd m n" by (rule gcd_commute)
   7.200    finally show ?thesis .
   7.201  qed
   7.202  
   7.203 -lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   7.204 +lemma gcd_add2' [simp]: "gcd m (n + m) = gcd m n"
   7.205    apply (subst add_commute)
   7.206    apply (rule gcd_add2)
   7.207    done
   7.208  
   7.209 -lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   7.210 +lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   7.211    by (induct k) (simp_all add: add_assoc)
   7.212  
   7.213 -lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
   7.214 +lemma gcd_dvd_prod: "gcd m n dvd m * n"
   7.215    using mult_dvd_mono [of 1] by auto
   7.216  
   7.217  text {*
   7.218 @@ -198,12 +196,12 @@
   7.219  
   7.220  lemma div_gcd_relprime:
   7.221    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   7.222 -  shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1"
   7.223 +  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
   7.224  proof -
   7.225 -  let ?g = "gcd (a, b)"
   7.226 +  let ?g = "gcd a b"
   7.227    let ?a' = "a div ?g"
   7.228    let ?b' = "b div ?g"
   7.229 -  let ?g' = "gcd (?a', ?b')"
   7.230 +  let ?g' = "gcd ?a' ?b'"
   7.231    have dvdg: "?g dvd a" "?g dvd b" by simp_all
   7.232    have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   7.233    from dvdg dvdg' obtain ka kb ka' kb' where
   7.234 @@ -222,28 +220,28 @@
   7.235  subsection {* LCM defined by GCD *}
   7.236  
   7.237  definition
   7.238 -  lcm :: "nat \<times> nat \<Rightarrow> nat"
   7.239 +  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   7.240  where
   7.241 -  lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
   7.242 +  lcm_prim_def: "lcm m n = m * n div gcd m n"
   7.243  
   7.244  lemma lcm_def:
   7.245 -  "lcm (m, n) = m * n div gcd (m, n)"
   7.246 +  "lcm m n = m * n div gcd m n"
   7.247    unfolding lcm_prim_def by simp
   7.248  
   7.249  lemma prod_gcd_lcm:
   7.250 -  "m * n = gcd (m, n) * lcm (m, n)"
   7.251 +  "m * n = gcd m n * lcm m n"
   7.252    unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
   7.253  
   7.254 -lemma lcm_0 [simp]: "lcm (m, 0) = 0"
   7.255 +lemma lcm_0 [simp]: "lcm m 0 = 0"
   7.256    unfolding lcm_def by simp
   7.257  
   7.258 -lemma lcm_1 [simp]: "lcm (m, 1) = m"
   7.259 +lemma lcm_1 [simp]: "lcm m 1 = m"
   7.260    unfolding lcm_def by simp
   7.261  
   7.262 -lemma lcm_0_left [simp]: "lcm (0, n) = 0"
   7.263 +lemma lcm_0_left [simp]: "lcm 0 n = 0"
   7.264    unfolding lcm_def by simp
   7.265  
   7.266 -lemma lcm_1_left [simp]: "lcm (1, m) = m"
   7.267 +lemma lcm_1_left [simp]: "lcm 1 m = m"
   7.268    unfolding lcm_def by simp
   7.269  
   7.270  lemma dvd_pos:
   7.271 @@ -254,38 +252,38 @@
   7.272  
   7.273  lemma lcm_least:
   7.274    assumes "m dvd k" and "n dvd k"
   7.275 -  shows "lcm (m, n) dvd k"
   7.276 +  shows "lcm m n dvd k"
   7.277  proof (cases k)
   7.278    case 0 then show ?thesis by auto
   7.279  next
   7.280    case (Suc _) then have pos_k: "k > 0" by auto
   7.281    from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
   7.282 -  with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
   7.283 +  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
   7.284    from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   7.285    from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   7.286    from pos_k k_m have pos_p: "p > 0" by auto
   7.287    from pos_k k_n have pos_q: "q > 0" by auto
   7.288 -  have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
   7.289 +  have "k * k * gcd q p = k * gcd (k * q) (k * p)"
   7.290      by (simp add: mult_ac gcd_mult_distrib2)
   7.291 -  also have "\<dots> = k * gcd (m * p * q, n * q * p)"
   7.292 +  also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
   7.293      by (simp add: k_m [symmetric] k_n [symmetric])
   7.294 -  also have "\<dots> = k * p * q * gcd (m, n)"
   7.295 +  also have "\<dots> = k * p * q * gcd m n"
   7.296      by (simp add: mult_ac gcd_mult_distrib2)
   7.297 -  finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
   7.298 +  finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
   7.299      by (simp only: k_m [symmetric] k_n [symmetric])
   7.300 -  then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
   7.301 +  then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
   7.302      by (simp add: mult_ac)
   7.303 -  with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
   7.304 +  with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
   7.305      by simp
   7.306    with prod_gcd_lcm [of m n]
   7.307 -  have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
   7.308 +  have "lcm m n * gcd q p * gcd m n = k * gcd m n"
   7.309      by (simp add: mult_ac)
   7.310 -  with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
   7.311 +  with pos_gcd have "lcm m n * gcd q p = k" by simp
   7.312    then show ?thesis using dvd_def by auto
   7.313  qed
   7.314  
   7.315  lemma lcm_dvd1 [iff]:
   7.316 -  "m dvd lcm (m, n)"
   7.317 +  "m dvd lcm m n"
   7.318  proof (cases m)
   7.319    case 0 then show ?thesis by simp
   7.320  next
   7.321 @@ -297,16 +295,16 @@
   7.322    next
   7.323      case (Suc _)
   7.324      then have npos: "n > 0" by simp
   7.325 -    have "gcd (m, n) dvd n" by simp
   7.326 -    then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
   7.327 -    then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
   7.328 +    have "gcd m n dvd n" by simp
   7.329 +    then obtain k where "n = gcd m n * k" using dvd_def by auto
   7.330 +    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
   7.331      also have "\<dots> = m * k" using mpos npos gcd_zero by simp
   7.332      finally show ?thesis by (simp add: lcm_def)
   7.333    qed
   7.334  qed
   7.335  
   7.336  lemma lcm_dvd2 [iff]: 
   7.337 -  "n dvd lcm (m, n)"
   7.338 +  "n dvd lcm m n"
   7.339  proof (cases n)
   7.340    case 0 then show ?thesis by simp
   7.341  next
   7.342 @@ -318,9 +316,9 @@
   7.343    next
   7.344      case (Suc _)
   7.345      then have mpos: "m > 0" by simp
   7.346 -    have "gcd (m, n) dvd m" by simp
   7.347 -    then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
   7.348 -    then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
   7.349 +    have "gcd m n dvd m" by simp
   7.350 +    then obtain k where "m = gcd m n * k" using dvd_def by auto
   7.351 +    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
   7.352      also have "\<dots> = n * k" using mpos npos gcd_zero by simp
   7.353      finally show ?thesis by (simp add: lcm_def)
   7.354    qed
   7.355 @@ -330,35 +328,35 @@
   7.356  subsection {* GCD and LCM on integers *}
   7.357  
   7.358  definition
   7.359 -  igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   7.360 -  "igcd i j = int (gcd (nat (abs i), nat (abs j)))"
   7.361 +  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   7.362 +  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
   7.363  
   7.364 -lemma igcd_dvd1 [simp]: "igcd i j dvd i"
   7.365 -  by (simp add: igcd_def int_dvd_iff)
   7.366 +lemma zgcd_dvd1 [simp]: "zgcd i j dvd i"
   7.367 +  by (simp add: zgcd_def int_dvd_iff)
   7.368  
   7.369 -lemma igcd_dvd2 [simp]: "igcd i j dvd j"
   7.370 -  by (simp add: igcd_def int_dvd_iff)
   7.371 +lemma zgcd_dvd2 [simp]: "zgcd i j dvd j"
   7.372 +  by (simp add: zgcd_def int_dvd_iff)
   7.373  
   7.374 -lemma igcd_pos: "igcd i j \<ge> 0"
   7.375 -  by (simp add: igcd_def)
   7.376 +lemma zgcd_pos: "zgcd i j \<ge> 0"
   7.377 +  by (simp add: zgcd_def)
   7.378  
   7.379 -lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
   7.380 -  by (simp add: igcd_def gcd_zero) arith
   7.381 +lemma zgcd0 [simp]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
   7.382 +  by (simp add: zgcd_def gcd_zero) arith
   7.383  
   7.384 -lemma igcd_commute: "igcd i j = igcd j i"
   7.385 -  unfolding igcd_def by (simp add: gcd_commute)
   7.386 +lemma zgcd_commute: "zgcd i j = zgcd j i"
   7.387 +  unfolding zgcd_def by (simp add: gcd_commute)
   7.388  
   7.389 -lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j"
   7.390 -  unfolding igcd_def by simp
   7.391 +lemma zgcd_neg1 [simp]: "zgcd (- i) j = zgcd i j"
   7.392 +  unfolding zgcd_def by simp
   7.393  
   7.394 -lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j"
   7.395 -  unfolding igcd_def by simp
   7.396 +lemma zgcd_neg2 [simp]: "zgcd i (- j) = zgcd i j"
   7.397 +  unfolding zgcd_def by simp
   7.398  
   7.399 -lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   7.400 -  unfolding igcd_def
   7.401 +lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   7.402 +  unfolding zgcd_def
   7.403  proof -
   7.404 -  assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   7.405 -  then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
   7.406 +  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   7.407 +  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
   7.408    from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
   7.409    have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
   7.410      unfolding dvd_def
   7.411 @@ -375,34 +373,34 @@
   7.412      done
   7.413  qed
   7.414  
   7.415 -lemma int_nat_abs: "int (nat (abs x)) = abs x"  by arith
   7.416 +lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
   7.417  
   7.418 -lemma igcd_greatest:
   7.419 +lemma zgcd_greatest:
   7.420    assumes "k dvd m" and "k dvd n"
   7.421 -  shows "k dvd igcd m n"
   7.422 +  shows "k dvd zgcd m n"
   7.423  proof -
   7.424    let ?k' = "nat \<bar>k\<bar>"
   7.425    let ?m' = "nat \<bar>m\<bar>"
   7.426    let ?n' = "nat \<bar>n\<bar>"
   7.427    from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
   7.428      unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
   7.429 -  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
   7.430 -    unfolding igcd_def by (simp only: zdvd_int)
   7.431 -  then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
   7.432 -  then show "k dvd igcd m n" by (simp add: zdvd_abs1)
   7.433 +  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
   7.434 +    unfolding zgcd_def by (simp only: zdvd_int)
   7.435 +  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
   7.436 +  then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
   7.437  qed
   7.438  
   7.439 -lemma div_igcd_relprime:
   7.440 +lemma div_zgcd_relprime:
   7.441    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   7.442 -  shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
   7.443 +  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
   7.444  proof -
   7.445    from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
   7.446 -  let ?g = "igcd a b"
   7.447 +  let ?g = "zgcd a b"
   7.448    let ?a' = "a div ?g"
   7.449    let ?b' = "b div ?g"
   7.450 -  let ?g' = "igcd ?a' ?b'"
   7.451 -  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
   7.452 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2)
   7.453 +  let ?g' = "zgcd ?a' ?b'"
   7.454 +  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
   7.455 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
   7.456    from dvdg dvdg' obtain ka kb ka' kb' where
   7.457     kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
   7.458      unfolding dvd_def by blast
   7.459 @@ -411,35 +409,36 @@
   7.460      by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
   7.461        zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   7.462    have "?g \<noteq> 0" using nz by simp
   7.463 -  then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
   7.464 -  from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   7.465 +  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
   7.466 +  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   7.467    with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
   7.468 -  with igcd_pos show "?g' = 1" by simp
   7.469 +  with zgcd_pos show "?g' = 1" by simp
   7.470  qed
   7.471  
   7.472 -definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
   7.473 +definition zlcm :: "int \<Rightarrow> int \<Rightarrow> int" where
   7.474 +  "zlcm i j = int (lcm (nat (abs i)) (nat (abs j)))"
   7.475  
   7.476 -lemma dvd_ilcm_self1[simp]: "i dvd ilcm i j"
   7.477 -by(simp add:ilcm_def dvd_int_iff)
   7.478 +lemma dvd_zlcm_self1[simp]: "i dvd zlcm i j"
   7.479 +by(simp add:zlcm_def dvd_int_iff)
   7.480  
   7.481 -lemma dvd_ilcm_self2[simp]: "j dvd ilcm i j"
   7.482 -by(simp add:ilcm_def dvd_int_iff)
   7.483 +lemma dvd_zlcm_self2[simp]: "j dvd zlcm i j"
   7.484 +by(simp add:zlcm_def dvd_int_iff)
   7.485  
   7.486  
   7.487 -lemma dvd_imp_dvd_ilcm1:
   7.488 -  assumes "k dvd i" shows "k dvd (ilcm i j)"
   7.489 +lemma dvd_imp_dvd_zlcm1:
   7.490 +  assumes "k dvd i" shows "k dvd (zlcm i j)"
   7.491  proof -
   7.492    have "nat(abs k) dvd nat(abs i)" using `k dvd i`
   7.493      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
   7.494 -  thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
   7.495 +  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   7.496  qed
   7.497  
   7.498 -lemma dvd_imp_dvd_ilcm2:
   7.499 -  assumes "k dvd j" shows "k dvd (ilcm i j)"
   7.500 +lemma dvd_imp_dvd_zlcm2:
   7.501 +  assumes "k dvd j" shows "k dvd (zlcm i j)"
   7.502  proof -
   7.503    have "nat(abs k) dvd nat(abs j)" using `k dvd j`
   7.504      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
   7.505 -  thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
   7.506 +  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   7.507  qed
   7.508  
   7.509  
   7.510 @@ -453,35 +452,35 @@
   7.511  
   7.512  lemma lcm_pos: 
   7.513    assumes mpos: "m > 0"
   7.514 -  and npos: "n>0"
   7.515 -  shows "lcm (m,n) > 0"
   7.516 +  and npos: "n > 0"
   7.517 +  shows "lcm m n > 0"
   7.518  proof(rule ccontr, simp add: lcm_def gcd_zero)
   7.519 -assume h:"m*n div gcd(m,n) = 0"
   7.520 -from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
   7.521 -hence gcdp: "gcd(m,n) > 0" by simp
   7.522 +assume h:"m * n div gcd m n = 0"
   7.523 +from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
   7.524 +hence gcdp: "gcd m n > 0" by simp
   7.525  with h
   7.526 -have "m*n < gcd(m,n)"
   7.527 -  by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
   7.528 +have "m*n < gcd m n"
   7.529 +  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
   7.530  moreover 
   7.531 -have "gcd(m,n) dvd m" by simp
   7.532 - with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
   7.533 - with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
   7.534 - have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
   7.535 - with t1 have "gcd(m,n) \<le> m*n" by arith
   7.536 +have "gcd m n dvd m" by simp
   7.537 + with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
   7.538 + with npos have t1:"gcd m n*n \<le> m*n" by simp
   7.539 + have "gcd m n \<le> gcd m n*n" using npos by simp
   7.540 + with t1 have "gcd m n \<le> m*n" by arith
   7.541  ultimately show "False" by simp
   7.542  qed
   7.543  
   7.544 -lemma ilcm_pos: 
   7.545 +lemma zlcm_pos: 
   7.546    assumes anz: "a \<noteq> 0"
   7.547    and bnz: "b \<noteq> 0" 
   7.548 -  shows "0 < ilcm a b"
   7.549 +  shows "0 < zlcm a b"
   7.550  proof-
   7.551    let ?na = "nat (abs a)"
   7.552    let ?nb = "nat (abs b)"
   7.553    have nap: "?na >0" using anz by simp
   7.554    have nbp: "?nb >0" using bnz by simp
   7.555 -  have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
   7.556 -  thus ?thesis by (simp add: ilcm_def)
   7.557 +  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
   7.558 +  thus ?thesis by (simp add: zlcm_def)
   7.559  qed
   7.560  
   7.561  end
     8.1 --- a/src/HOL/Library/Primes.thy	Fri Jul 11 23:17:25 2008 +0200
     8.2 +++ b/src/HOL/Library/Primes.thy	Mon Jul 14 11:04:42 2008 +0200
     8.3 @@ -12,7 +12,7 @@
     8.4  
     8.5  definition
     8.6    coprime :: "nat => nat => bool" where
     8.7 -  "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)"
     8.8 +  "coprime m n \<longleftrightarrow> (gcd m n = 1)"
     8.9  
    8.10  definition
    8.11    prime :: "nat \<Rightarrow> bool" where
    8.12 @@ -25,7 +25,7 @@
    8.13     apply (auto dest!: dvd_imp_le)
    8.14    done
    8.15  
    8.16 -lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
    8.17 +lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
    8.18    apply (auto simp add: prime_def)
    8.19    apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
    8.20    done
    8.21 @@ -309,24 +309,24 @@
    8.22  qed
    8.23  
    8.24  text {* Greatest common divisor. *}
    8.25 -lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd(a,b)"
    8.26 +lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    8.27  proof(auto)
    8.28    assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
    8.29    from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
    8.30 -  have th: "gcd (a,b) dvd d" by blast
    8.31 -  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd (a,b)" by blast 
    8.32 +  have th: "gcd a b dvd d" by blast
    8.33 +  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d =gcd a b" by blast 
    8.34  qed
    8.35  
    8.36  lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
    8.37 -  shows "gcd (x,y) = gcd(u,v)"
    8.38 +  shows "gcd x y = gcd u v"
    8.39  proof-
    8.40 -  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd (u,v)" by simp
    8.41 -  with gcd_unique[of "gcd(u,v)" x y]  show ?thesis by auto
    8.42 +  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
    8.43 +  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
    8.44  qed
    8.45  
    8.46 -lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd(a,b) \<or> b * x - a * y = gcd(a,b)"
    8.47 +lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
    8.48  proof-
    8.49 -  let ?g = "gcd (a,b)"
    8.50 +  let ?g = "gcd a b"
    8.51    from bezout[of a b] obtain d x y where d: "d dvd a" "d dvd b" "a * x - b * y = d \<or> b * x - a * y = d" by blast
    8.52    from d(1,2) have "d dvd ?g" by simp
    8.53    then obtain k where k: "?g = d*k" unfolding dvd_def by blast
    8.54 @@ -339,9 +339,9 @@
    8.55  qed
    8.56  
    8.57  lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
    8.58 -  shows "\<exists>x y. a * x = b * y + gcd(a,b)"
    8.59 +  shows "\<exists>x y. a * x = b * y + gcd a b"
    8.60  proof-
    8.61 -  let ?g = "gcd (a,b)"
    8.62 +  let ?g = "gcd a b"
    8.63    from bezout_add_strong[OF a, of b]
    8.64    obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
    8.65    from d(1,2) have "d dvd ?g" by simp
    8.66 @@ -351,13 +351,13 @@
    8.67    thus ?thesis by blast
    8.68  qed
    8.69  
    8.70 -lemma gcd_mult_distrib: "gcd(a * c, b * c) = c * gcd(a,b)"
    8.71 +lemma gcd_mult_distrib: "gcd (a * c) (b * c) = c * gcd a b"
    8.72  by(simp add: gcd_mult_distrib2 mult_commute)
    8.73  
    8.74 -lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd(a,b) dvd d"
    8.75 +lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
    8.76    (is "?lhs \<longleftrightarrow> ?rhs")
    8.77  proof-
    8.78 -  let ?g = "gcd (a,b)"
    8.79 +  let ?g = "gcd a b"
    8.80    {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
    8.81      from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
    8.82        by blast
    8.83 @@ -376,34 +376,34 @@
    8.84    ultimately show ?thesis by blast
    8.85  qed
    8.86  
    8.87 -lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd(a,b) dvd d"
    8.88 +lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
    8.89  proof-
    8.90 -  let ?g = "gcd (a,b)"
    8.91 +  let ?g = "gcd a b"
    8.92      have dv: "?g dvd a*x" "?g dvd b * y" 
    8.93        using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
    8.94      from dvd_add[OF dv] H
    8.95      show ?thesis by auto
    8.96  qed
    8.97  
    8.98 -lemma gcd_mult': "gcd(b,a * b) = b"
    8.99 +lemma gcd_mult': "gcd b (a * b) = b"
   8.100  by (simp add: gcd_mult mult_commute[of a b]) 
   8.101  
   8.102 -lemma gcd_add: "gcd(a + b,b) = gcd(a,b)" "gcd(b + a,b) = gcd(a,b)" "gcd(a,a + b) = gcd(a,b)" "gcd(a,b + a) = gcd(a,b)"
   8.103 +lemma gcd_add: "gcd (a + b) b = gcd a b" "gcd (b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
   8.104  apply (simp_all add: gcd_add1)
   8.105  by (simp add: gcd_commute gcd_add1)
   8.106  
   8.107 -lemma gcd_sub: "b <= a ==> gcd(a - b,b) = gcd(a,b)" "a <= b ==> gcd(a,b - a) = gcd(a,b)"
   8.108 +lemma gcd_sub: "b <= a ==> gcd (a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
   8.109  proof-
   8.110    {fix a b assume H: "b \<le> (a::nat)"
   8.111      hence th: "a - b + b = a" by arith
   8.112 -    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b,b) = gcd(a,b)" by simp}
   8.113 +    from gcd_add(1)[of "a - b" b] th  have "gcd (a - b) b = gcd a b" by simp}
   8.114    note th = this
   8.115  {
   8.116    assume ab: "b \<le> a"
   8.117 -  from th[OF ab] show "gcd (a - b, b) = gcd (a, b)" by blast
   8.118 +  from th[OF ab] show "gcd (a - b) b = gcd a b" by blast
   8.119  next
   8.120    assume ab: "a \<le> b"
   8.121 -  from th[OF ab] show "gcd (a,b - a) = gcd (a, b)" 
   8.122 +  from th[OF ab] show "gcd a (b - a) = gcd a b" 
   8.123      by (simp add: gcd_commute)}
   8.124  qed
   8.125  
   8.126 @@ -425,10 +425,10 @@
   8.127  lemma coprime_Suc0'[simp]: "coprime (Suc 0) a" by (simp add: coprime_def)
   8.128  
   8.129  lemma gcd_coprime: 
   8.130 -  assumes z: "gcd(a,b) \<noteq> 0" and a: "a = a' * gcd(a,b)" and b: "b = b' * gcd(a,b)" 
   8.131 +  assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" 
   8.132    shows    "coprime a' b'"
   8.133  proof-
   8.134 -  let ?g = "gcd(a,b)"
   8.135 +  let ?g = "gcd a b"
   8.136    {assume bz: "a = 0" from b bz z a have ?thesis by (simp add: gcd_zero coprime_def)}
   8.137    moreover 
   8.138    {assume az: "a\<noteq> 0" 
   8.139 @@ -447,8 +447,8 @@
   8.140  lemma coprime_mul: assumes da: "coprime d a" and db: "coprime d b"
   8.141    shows "coprime d (a * b)"
   8.142  proof-
   8.143 -  from da have th: "gcd(a, d) = 1" by (simp add: coprime_def gcd_commute)
   8.144 -  from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd (d, a*b) = 1"
   8.145 +  from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute)
   8.146 +  from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a * b) = 1"
   8.147      by (simp add: gcd_commute)
   8.148    thus ?thesis unfolding coprime_def .
   8.149  qed
   8.150 @@ -480,10 +480,10 @@
   8.151    by blast
   8.152  
   8.153  lemma gcd_coprime_exists:
   8.154 -  assumes nz: "gcd(a,b) \<noteq> 0" 
   8.155 -  shows "\<exists>a' b'. a = a' * gcd(a,b) \<and> b = b' * gcd(a,b) \<and> coprime a' b'"
   8.156 +  assumes nz: "gcd a b \<noteq> 0" 
   8.157 +  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   8.158  proof-
   8.159 -  let ?g = "gcd (a,b)"
   8.160 +  let ?g = "gcd a b"
   8.161    from gcd_dvd1[of a b] gcd_dvd2[of a b] 
   8.162    obtain a' b' where "a = ?g*a'"  "b = ?g*b'" unfolding dvd_def by blast
   8.163    hence ab': "a = a'*?g" "b = b'*?g" by algebra+
   8.164 @@ -505,9 +505,9 @@
   8.165  lemma coprime_minus1: "n \<noteq> 0 ==> coprime (n - 1) n"
   8.166    using coprime_plus1[of "n - 1"] coprime_commute[of "n - 1" n] by auto
   8.167  
   8.168 -lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd(a,b) ^ n \<or> b ^ n * x - a ^ n * y = gcd(a,b) ^ n"
   8.169 +lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd a b ^ n \<or> b ^ n * x - a ^ n * y = gcd a b ^ n"
   8.170  proof-
   8.171 -  let ?g = "gcd (a,b)"
   8.172 +  let ?g = "gcd a b"
   8.173    {assume z: "?g = 0" hence ?thesis 
   8.174        apply (cases n, simp)
   8.175        apply arith
   8.176 @@ -530,16 +530,16 @@
   8.177      hence  ?thesis by blast }
   8.178    ultimately show ?thesis by blast
   8.179  qed
   8.180 -lemma gcd_exp: "gcd (a^n, b^n) = gcd(a,b)^n"
   8.181 +lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b ^ n"
   8.182  proof-
   8.183 -  let ?g = "gcd(a^n,b^n)"
   8.184 -  let ?gn = "gcd(a,b)^n"
   8.185 +  let ?g = "gcd (a^n) (b^n)"
   8.186 +  let ?gn = "gcd a b ^ n"
   8.187    {fix e assume H: "e dvd a^n" "e dvd b^n"
   8.188      from bezout_gcd_pow[of a n b] obtain x y 
   8.189        where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
   8.190      from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
   8.191        dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
   8.192 -    have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd (a, b) ^ n", simp_all)}
   8.193 +    have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
   8.194    hence th:  "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
   8.195    from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
   8.196      gcd_unique have "?gn = ?g" by blast thus ?thesis by simp 
   8.197 @@ -551,7 +551,7 @@
   8.198  lemma division_decomp: assumes dc: "(a::nat) dvd b * c"
   8.199    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   8.200  proof-
   8.201 -  let ?g = "gcd (a,b)"
   8.202 +  let ?g = "gcd a b"
   8.203    {assume "?g = 0" with dc have ?thesis apply (simp add: gcd_zero)
   8.204        apply (rule exI[where x="0"])
   8.205        by (rule exI[where x="c"], simp)}
   8.206 @@ -575,7 +575,7 @@
   8.207  
   8.208  lemma divides_rev: assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" shows "a dvd b"
   8.209  proof-
   8.210 -  let ?g = "gcd (a,b)"
   8.211 +  let ?g = "gcd a b"
   8.212    from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   8.213    {assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)}
   8.214    moreover
     9.1 --- a/src/HOL/NumberTheory/Chinese.thy	Fri Jul 11 23:17:25 2008 +0200
     9.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Jul 14 11:04:42 2008 +0200
     9.3 @@ -6,7 +6,9 @@
     9.4  
     9.5  header {* The Chinese Remainder Theorem *}
     9.6  
     9.7 -theory Chinese imports IntPrimes begin
     9.8 +theory Chinese 
     9.9 +imports IntPrimes
    9.10 +begin
    9.11  
    9.12  text {*
    9.13    The Chinese Remainder Theorem for an arbitrary finite number of
    9.14 @@ -35,11 +37,11 @@
    9.15    m_cond :: "nat => (nat => int) => bool" where
    9.16    "m_cond n mf =
    9.17      ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
    9.18 -      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
    9.19 +      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i) (mf j) = 1))"
    9.20  
    9.21  definition
    9.22    km_cond :: "nat => (nat => int) => (nat => int) => bool" where
    9.23 -  "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
    9.24 +  "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i) (mf i) = 1)"
    9.25  
    9.26  definition
    9.27    lincong_sol ::
    9.28 @@ -75,8 +77,8 @@
    9.29    done
    9.30  
    9.31  lemma funprod_zgcd [rule_format (no_asm)]:
    9.32 -  "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
    9.33 -    zgcd (funprod mf k l, mf m) = 1"
    9.34 +  "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
    9.35 +    zgcd (funprod mf k l) (mf m) = 1"
    9.36    apply (induct l)
    9.37     apply simp_all
    9.38    apply (rule impI)+
    10.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Jul 11 23:17:25 2008 +0200
    10.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Mon Jul 14 11:04:42 2008 +0200
    10.3 @@ -6,7 +6,9 @@
    10.4  
    10.5  header {* Fermat's Little Theorem extended to Euler's Totient function *}
    10.6  
    10.7 -theory EulerFermat imports BijectionRel IntFact begin
    10.8 +theory EulerFermat
    10.9 +imports BijectionRel IntFact
   10.10 +begin
   10.11  
   10.12  text {*
   10.13    Fermat's Little Theorem extended to Euler's Totient function. More
   10.14 @@ -22,7 +24,7 @@
   10.15    for m :: int
   10.16    where
   10.17      empty [simp]: "{} \<in> RsetR m"
   10.18 -  | insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
   10.19 +  | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
   10.20        \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
   10.21  
   10.22  consts
   10.23 @@ -33,7 +35,7 @@
   10.24    "BnorRset (a, m) =
   10.25     (if 0 < a then
   10.26      let na = BnorRset (a - 1, m)
   10.27 -    in (if zgcd (a, m) = 1 then insert a na else na)
   10.28 +    in (if zgcd a m = 1 then insert a na else na)
   10.29      else {})"
   10.30  
   10.31  definition
   10.32 @@ -103,7 +105,7 @@
   10.33    done
   10.34  
   10.35  lemma Bnor_mem_if [rule_format]:
   10.36 -    "zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
   10.37 +    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
   10.38    apply (induct a m rule: BnorRset.induct, auto)
   10.39     apply (subst BnorRset.simps)
   10.40     defer
   10.41 @@ -137,7 +139,7 @@
   10.42  
   10.43  lemma norR_mem_unique:
   10.44    "1 < m ==>
   10.45 -    zgcd (a, m) = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   10.46 +    zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   10.47    apply (unfold norRRset_def)
   10.48    apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
   10.49     apply (rule_tac [2] m = m in zcong_zless_imp_eq)
   10.50 @@ -149,7 +151,7 @@
   10.51       apply (auto intro: order_less_le [THEN iffD2])
   10.52     prefer 2
   10.53     apply (simp only: zcong_def)
   10.54 -   apply (subgoal_tac "zgcd (a, m) = m")
   10.55 +   apply (subgoal_tac "zgcd a m = m")
   10.56      prefer 2
   10.57      apply (subst zdvd_iff_zgcd [symmetric])
   10.58       apply (rule_tac [4] zgcd_zcong_zgcd)
   10.59 @@ -160,14 +162,14 @@
   10.60  text {* \medskip @{term noXRRset} *}
   10.61  
   10.62  lemma RRset_gcd [rule_format]:
   10.63 -    "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
   10.64 +    "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
   10.65    apply (unfold is_RRset_def)
   10.66 -  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd (a, m) = 1"], auto)
   10.67 +  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
   10.68    done
   10.69  
   10.70  lemma RsetR_zmult_mono:
   10.71    "A \<in> RsetR m ==>
   10.72 -    0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   10.73 +    0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   10.74    apply (erule RsetR.induct, simp_all)
   10.75    apply (rule RsetR.insert, auto)
   10.76     apply (blast intro: zgcd_zgcd_zmult)
   10.77 @@ -176,7 +178,7 @@
   10.78  
   10.79  lemma card_nor_eq_noX:
   10.80    "0 < m ==>
   10.81 -    zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)"
   10.82 +    zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)"
   10.83    apply (unfold norRRset_def noXRRset_def)
   10.84    apply (rule card_image)
   10.85     apply (auto simp add: inj_on_def Bnor_fin)
   10.86 @@ -184,7 +186,7 @@
   10.87    done
   10.88  
   10.89  lemma noX_is_RRset:
   10.90 -    "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m"
   10.91 +    "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m"
   10.92    apply (unfold is_RRset_def phi_def)
   10.93    apply (auto simp add: card_nor_eq_noX)
   10.94    apply (unfold noXRRset_def norRRset_def)
   10.95 @@ -284,7 +286,7 @@
   10.96    done
   10.97  
   10.98  lemma Bnor_prod_zgcd [rule_format]:
   10.99 -    "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
  10.100 +    "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
  10.101    apply (induct a m rule: BnorRset_induct)
  10.102     prefer 2
  10.103     apply (subst BnorRset.simps)
  10.104 @@ -294,7 +296,7 @@
  10.105    done
  10.106  
  10.107  theorem Euler_Fermat:
  10.108 -    "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)"
  10.109 +    "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
  10.110    apply (unfold norRRset_def phi_def)
  10.111    apply (case_tac "x = 0")
  10.112     apply (case_tac [2] "m = 1")
    11.1 --- a/src/HOL/NumberTheory/Fib.thy	Fri Jul 11 23:17:25 2008 +0200
    11.2 +++ b/src/HOL/NumberTheory/Fib.thy	Mon Jul 14 11:04:42 2008 +0200
    11.3 @@ -5,7 +5,9 @@
    11.4  
    11.5  header {* The Fibonacci function *}
    11.6  
    11.7 -theory Fib imports Primes begin
    11.8 +theory Fib
    11.9 +imports Primes
   11.10 +begin
   11.11  
   11.12  text {*
   11.13    Fibonacci numbers: proofs of laws taken from:
   11.14 @@ -92,14 +94,14 @@
   11.15  
   11.16  text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
   11.17  
   11.18 -lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0"
   11.19 +lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0"
   11.20    apply (induct n rule: fib.induct)
   11.21      prefer 3
   11.22      apply (simp add: gcd_commute fib_Suc3)
   11.23     apply (simp_all add: fib_2)
   11.24    done
   11.25  
   11.26 -lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
   11.27 +lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
   11.28    apply (simp add: gcd_commute [of "fib m"])
   11.29    apply (case_tac m)
   11.30     apply simp 
   11.31 @@ -109,31 +111,31 @@
   11.32    apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
   11.33    done
   11.34  
   11.35 -lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
   11.36 +lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   11.37    by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) 
   11.38  
   11.39 -lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
   11.40 +lemma gcd_fib_mod: "0 < m ==> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   11.41  proof (induct n rule: less_induct)
   11.42    case (less n)
   11.43    from less.prems have pos_m: "0 < m" .
   11.44 -  show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
   11.45 +  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   11.46    proof (cases "m < n")
   11.47      case True note m_n = True
   11.48      then have m_n': "m \<le> n" by auto
   11.49      with pos_m have pos_n: "0 < n" by auto
   11.50      with pos_m m_n have diff: "n - m < n" by auto
   11.51 -    have "gcd (fib m, fib (n mod m)) = gcd (fib m, fib ((n - m) mod m))"
   11.52 +    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
   11.53      by (simp add: mod_if [of n]) (insert m_n, auto)
   11.54 -    also have "\<dots> = gcd (fib m, fib (n - m))" by (simp add: less.hyps diff pos_m)
   11.55 -    also have "\<dots> = gcd (fib m, fib n)" by (simp add: gcd_fib_diff m_n')
   11.56 -    finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
   11.57 +    also have "\<dots> = gcd (fib m) (fib (n - m))" by (simp add: less.hyps diff pos_m)
   11.58 +    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff m_n')
   11.59 +    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   11.60    next
   11.61 -    case False then show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
   11.62 +    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   11.63      by (cases "m = n") auto
   11.64    qed
   11.65  qed
   11.66  
   11.67 -lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}
   11.68 +lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  -- {* Law 6.111 *}
   11.69    apply (induct m n rule: gcd_induct)
   11.70    apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
   11.71    done
    12.1 --- a/src/HOL/NumberTheory/Gauss.thy	Fri Jul 11 23:17:25 2008 +0200
    12.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Mon Jul 14 11:04:42 2008 +0200
    12.3 @@ -5,7 +5,9 @@
    12.4  
    12.5  header {* Gauss' Lemma *}
    12.6  
    12.7 -theory Gauss imports Euler begin
    12.8 +theory Gauss
    12.9 +imports Euler
   12.10 +begin
   12.11  
   12.12  locale GAUSS =
   12.13    fixes p :: "int"
   12.14 @@ -284,10 +286,10 @@
   12.15      using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   12.16  qed
   12.17  
   12.18 -lemma all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   12.19 +lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
   12.20    using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   12.21  
   12.22 -lemma A_prod_relprime: "zgcd((setprod id A),p) = 1"
   12.23 +lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
   12.24    using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
   12.25  
   12.26  
    13.1 --- a/src/HOL/NumberTheory/Int2.thy	Fri Jul 11 23:17:25 2008 +0200
    13.2 +++ b/src/HOL/NumberTheory/Int2.thy	Mon Jul 14 11:04:42 2008 +0200
    13.3 @@ -5,7 +5,9 @@
    13.4  
    13.5  header {*Integers: Divisibility and Congruences*}
    13.6  
    13.7 -theory Int2 imports Finite2 WilsonRuss begin
    13.8 +theory Int2
    13.9 +imports Finite2 WilsonRuss
   13.10 +begin
   13.11  
   13.12  definition
   13.13    MultInv :: "int => int => int" where
   13.14 @@ -167,8 +169,8 @@
   13.15    apply auto
   13.16    done
   13.17  
   13.18 -lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
   13.19 -    ==> zgcd (setprod id A,y) = 1"
   13.20 +lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |]
   13.21 +    ==> zgcd (setprod id A) y = 1"
   13.22    by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
   13.23  
   13.24  
    14.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Jul 11 23:17:25 2008 +0200
    14.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Jul 14 11:04:42 2008 +0200
    14.3 @@ -34,10 +34,6 @@
    14.4  		      t, t' - (r' div r) * t))"
    14.5  
    14.6  definition
    14.7 -  zgcd :: "int * int => int" where
    14.8 -  "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))"
    14.9 -
   14.10 -definition
   14.11    zprime :: "int \<Rightarrow> bool" where
   14.12    "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
   14.13  
   14.14 @@ -53,10 +49,10 @@
   14.15  
   14.16  text {* \medskip @{term gcd} lemmas *}
   14.17  
   14.18 -lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)"
   14.19 +lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
   14.20    by (simp add: gcd_commute)
   14.21  
   14.22 -lemma gcd_diff2: "m \<le> n ==> gcd (n, n - m) = gcd (n, m)"
   14.23 +lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
   14.24    apply (subgoal_tac "n = m + (n - m)")
   14.25     apply (erule ssubst, rule gcd_add1_eq, simp)
   14.26    done
   14.27 @@ -64,19 +60,19 @@
   14.28  
   14.29  subsection {* Euclid's Algorithm and GCD *}
   14.30  
   14.31 -lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
   14.32 +lemma zgcd_0 [simp]: "zgcd m 0 = abs m"
   14.33    by (simp add: zgcd_def abs_if)
   14.34  
   14.35 -lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m"
   14.36 +lemma zgcd_0_left [simp]: "zgcd 0 m = abs m"
   14.37    by (simp add: zgcd_def abs_if)
   14.38  
   14.39 -lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)"
   14.40 +lemma zgcd_zminus [simp]: "zgcd (-m) n = zgcd m n"
   14.41    by (simp add: zgcd_def)
   14.42  
   14.43 -lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)"
   14.44 +lemma zgcd_zminus2 [simp]: "zgcd m (-n) = zgcd m n"
   14.45    by (simp add: zgcd_def)
   14.46  
   14.47 -lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   14.48 +lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
   14.49    apply (frule_tac b = n and a = m in pos_mod_sign)
   14.50    apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
   14.51    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   14.52 @@ -84,37 +80,37 @@
   14.53    apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
   14.54    done
   14.55  
   14.56 -lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
   14.57 +lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
   14.58    apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
   14.59    apply (auto simp add: linorder_neq_iff zgcd_non_0)
   14.60    apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
   14.61    done
   14.62  
   14.63 -lemma zgcd_1 [simp]: "zgcd (m, 1) = 1"
   14.64 +lemma zgcd_1 [simp]: "zgcd m 1 = 1"
   14.65    by (simp add: zgcd_def abs_if)
   14.66  
   14.67 -lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)"
   14.68 +lemma zgcd_0_1_iff [simp]: "zgcd 0 m = 1 \<longleftrightarrow> abs m = 1"
   14.69    by (simp add: zgcd_def abs_if)
   14.70  
   14.71 -lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m"
   14.72 +lemma zgcd_zdvd1 [iff]: "zgcd m n dvd m"
   14.73    by (simp add: zgcd_def abs_if int_dvd_iff)
   14.74  
   14.75 -lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n"
   14.76 +lemma zgcd_zdvd2 [iff]: "zgcd m n dvd n"
   14.77    by (simp add: zgcd_def abs_if int_dvd_iff)
   14.78  
   14.79 -lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)"
   14.80 +lemma zgcd_greatest_iff: "k dvd zgcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   14.81    by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
   14.82  
   14.83 -lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)"
   14.84 +lemma zgcd_commute: "zgcd m n = zgcd n m"
   14.85    by (simp add: zgcd_def gcd_commute)
   14.86  
   14.87 -lemma zgcd_1_left [simp]: "zgcd (1, m) = 1"
   14.88 +lemma zgcd_1_left [simp]: "zgcd 1 m = 1"
   14.89    by (simp add: zgcd_def gcd_1_left)
   14.90  
   14.91 -lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))"
   14.92 +lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
   14.93    by (simp add: zgcd_def gcd_assoc)
   14.94  
   14.95 -lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))"
   14.96 +lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
   14.97    apply (rule zgcd_commute [THEN trans])
   14.98    apply (rule zgcd_assoc [THEN trans])
   14.99    apply (rule zgcd_commute [THEN arg_cong])
  14.100 @@ -123,35 +119,35 @@
  14.101  lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
  14.102    -- {* addition is an AC-operator *}
  14.103  
  14.104 -lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
  14.105 +lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
  14.106    by (simp del: minus_mult_right [symmetric]
  14.107        add: minus_mult_right nat_mult_distrib zgcd_def abs_if
  14.108            mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
  14.109  
  14.110 -lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
  14.111 +lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
  14.112    by (simp add: abs_if zgcd_zmult_distrib2)
  14.113  
  14.114 -lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m"
  14.115 +lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
  14.116    by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
  14.117  
  14.118 -lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k"
  14.119 +lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
  14.120    by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
  14.121  
  14.122 -lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k"
  14.123 +lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
  14.124    by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
  14.125  
  14.126  lemma zrelprime_zdvd_zmult_aux:
  14.127 -     "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
  14.128 +     "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
  14.129    by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
  14.130  
  14.131 -lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
  14.132 +lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
  14.133    apply (case_tac "0 \<le> m")
  14.134     apply (blast intro: zrelprime_zdvd_zmult_aux)
  14.135    apply (subgoal_tac "k dvd -m")
  14.136     apply (rule_tac [2] zrelprime_zdvd_zmult_aux, auto)
  14.137    done
  14.138  
  14.139 -lemma zgcd_geq_zero: "0 <= zgcd(x,y)"
  14.140 +lemma zgcd_geq_zero: "0 <= zgcd x y"
  14.141    by (auto simp add: zgcd_def)
  14.142  
  14.143  text{*This is merely a sanity check on zprime, since the previous version
  14.144 @@ -163,34 +159,34 @@
  14.145    done
  14.146  
  14.147  lemma zprime_imp_zrelprime:
  14.148 -    "zprime p ==> \<not> p dvd n ==> zgcd (n, p) = 1"
  14.149 +    "zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
  14.150    apply (auto simp add: zprime_def)
  14.151    apply (metis zgcd_commute zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
  14.152    done
  14.153  
  14.154  lemma zless_zprime_imp_zrelprime:
  14.155 -    "zprime p ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
  14.156 +    "zprime p ==> 0 < n ==> n < p ==> zgcd n p = 1"
  14.157    apply (erule zprime_imp_zrelprime)
  14.158    apply (erule zdvd_not_zless, assumption)
  14.159    done
  14.160  
  14.161  lemma zprime_zdvd_zmult:
  14.162      "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
  14.163 -  by (metis igcd_dvd1 igcd_dvd2 igcd_pos zprime_def zrelprime_dvd_mult)
  14.164 +  by (metis zgcd_dvd1 zgcd_dvd2 zgcd_pos zprime_def zrelprime_dvd_mult)
  14.165  
  14.166 -lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)"
  14.167 +lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
  14.168    apply (rule zgcd_eq [THEN trans])
  14.169    apply (simp add: zmod_zadd1_eq)
  14.170    apply (rule zgcd_eq [symmetric])
  14.171    done
  14.172  
  14.173 -lemma zgcd_zdvd_zgcd_zmult: "zgcd (m, n) dvd zgcd (k * m, n)"
  14.174 +lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
  14.175    apply (simp add: zgcd_greatest_iff)
  14.176    apply (blast intro: zdvd_trans)
  14.177    done
  14.178  
  14.179  lemma zgcd_zmult_zdvd_zgcd:
  14.180 -    "zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)"
  14.181 +  "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
  14.182    apply (simp add: zgcd_greatest_iff)
  14.183    apply (rule_tac n = k in zrelprime_zdvd_zmult)
  14.184     prefer 2
  14.185 @@ -198,14 +194,14 @@
  14.186    apply (metis zgcd_1 zgcd_commute zgcd_left_commute)
  14.187    done
  14.188  
  14.189 -lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)"
  14.190 +lemma zgcd_zmult_cancel: "zgcd k n = 1 ==> zgcd (k * m) n = zgcd m n"
  14.191    by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
  14.192  
  14.193  lemma zgcd_zgcd_zmult:
  14.194 -    "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1"
  14.195 +  "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1"
  14.196    by (simp add: zgcd_zmult_cancel)
  14.197  
  14.198 -lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
  14.199 +lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
  14.200    by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
  14.201  
  14.202  
  14.203 @@ -276,7 +272,7 @@
  14.204  
  14.205  lemma zcong_cancel:
  14.206    "0 \<le> m ==>
  14.207 -    zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
  14.208 +    zgcd k m = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
  14.209    apply safe
  14.210     prefer 2
  14.211     apply (blast intro: zcong_scalar)
  14.212 @@ -293,11 +289,11 @@
  14.213  
  14.214  lemma zcong_cancel2:
  14.215    "0 \<le> m ==>
  14.216 -    zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
  14.217 +    zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
  14.218    by (simp add: zmult_commute zcong_cancel)
  14.219  
  14.220  lemma zcong_zgcd_zmult_zmod:
  14.221 -  "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1
  14.222 +  "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
  14.223      ==> [a = b] (mod m * n)"
  14.224    apply (unfold zcong_def dvd_def, auto)
  14.225    apply (subgoal_tac "m dvd n * ka")
  14.226 @@ -353,7 +349,7 @@
  14.227  
  14.228  lemma zgcd_zcong_zgcd:
  14.229    "0 < m ==>
  14.230 -    zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1"
  14.231 +    zgcd a m = 1 ==> [a = b] (mod m) ==> zgcd b m = 1"
  14.232    by (auto simp add: zcong_iff_lin)
  14.233  
  14.234  lemma zcong_zmod_aux:
  14.235 @@ -412,7 +408,7 @@
  14.236  declare xzgcda.simps [simp del]
  14.237  
  14.238  lemma xzgcd_correct_aux1:
  14.239 -  "zgcd (r', r) = k --> 0 < r -->
  14.240 +  "zgcd r' r = k --> 0 < r -->
  14.241      (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
  14.242    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
  14.243      z = s and aa = t' and ab = t in xzgcda.induct)
  14.244 @@ -428,7 +424,7 @@
  14.245  
  14.246  lemma xzgcd_correct_aux2:
  14.247    "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
  14.248 -    zgcd (r', r) = k"
  14.249 +    zgcd r' r = k"
  14.250    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
  14.251      z = s and aa = t' and ab = t in xzgcda.induct)
  14.252    apply (subst zgcd_eq)
  14.253 @@ -441,7 +437,7 @@
  14.254    done
  14.255  
  14.256  lemma xzgcd_correct:
  14.257 -    "0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
  14.258 +    "0 < n ==> zgcd m n = k \<longleftrightarrow> (\<exists>s t. xzgcd m n = (k, s, t))"
  14.259    apply (unfold xzgcd_def)
  14.260    apply (rule iffI)
  14.261     apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
  14.262 @@ -491,14 +487,14 @@
  14.263    done
  14.264  
  14.265  lemma zgcd_ex_linear:
  14.266 -    "0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
  14.267 +    "0 < n ==> zgcd m n = k ==> (\<exists>s t. k = s * m + t * n)"
  14.268    apply (simp add: xzgcd_correct, safe)
  14.269    apply (rule exI)+
  14.270    apply (erule xzgcd_linear, auto)
  14.271    done
  14.272  
  14.273  lemma zcong_lineq_ex:
  14.274 -    "0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)"
  14.275 +    "0 < n ==> zgcd a n = 1 ==> \<exists>x. [a * x = 1] (mod n)"
  14.276    apply (cut_tac m = a and n = n and k = 1 in zgcd_ex_linear, safe)
  14.277    apply (rule_tac x = s in exI)
  14.278    apply (rule_tac b = "s * a + t * n" in zcong_trans)
  14.279 @@ -510,7 +506,7 @@
  14.280  
  14.281  lemma zcong_lineq_unique:
  14.282    "0 < n ==>
  14.283 -    zgcd (a, n) = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
  14.284 +    zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
  14.285    apply auto
  14.286     apply (rule_tac [2] zcong_zless_imp_eq)
  14.287         apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
    15.1 --- a/src/HOL/ex/LocaleTest2.thy	Fri Jul 11 23:17:25 2008 +0200
    15.2 +++ b/src/HOL/ex/LocaleTest2.thy	Mon Jul 14 11:04:42 2008 +0200
    15.3 @@ -592,26 +592,26 @@
    15.4  qed
    15.5  
    15.6  interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
    15.7 -  where "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
    15.8 -    and "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
    15.9 +  where "dlat.meet (op dvd) (x::nat) y = gcd x y"
   15.10 +    and "dlat.join (op dvd) (x::nat) y = lcm x y"
   15.11  proof -
   15.12    show "dlat (op dvd :: [nat, nat] => bool)"
   15.13      apply unfold_locales
   15.14      apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
   15.15 -    apply (rule_tac x = "gcd (x, y)" in exI)
   15.16 +    apply (rule_tac x = "gcd x y" in exI)
   15.17      apply auto [1]
   15.18 -    apply (rule_tac x = "lcm (x, y)" in exI)
   15.19 +    apply (rule_tac x = "lcm x y" in exI)
   15.20      apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
   15.21      done
   15.22    then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
   15.23    txt {* Interpretation to ease use of definitions, which are
   15.24      conditional in general but unconditional after interpretation. *}
   15.25 -  show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
   15.26 +  show "dlat.meet (op dvd) (x::nat) y = gcd x y"
   15.27      apply (unfold nat_dvd.meet_def)
   15.28      apply (rule the_equality)
   15.29      apply (unfold nat_dvd.is_inf_def)
   15.30      by auto
   15.31 -  show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
   15.32 +  show "dlat.join (op dvd) (x::nat) y = lcm x y"
   15.33      apply (unfold nat_dvd.join_def)
   15.34      apply (rule the_equality)
   15.35      apply (unfold nat_dvd.is_sup_def)
   15.36 @@ -624,7 +624,7 @@
   15.37  lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
   15.38    apply (rule nat_dvd.less_def) done
   15.39  thm nat_dvd.meet_left text {* from dlat *}
   15.40 -lemma "gcd (x, y) dvd x"
   15.41 +lemma "gcd x y dvd x"
   15.42    apply (rule nat_dvd.meet_left) done
   15.43  
   15.44  print_interps dpo
    16.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jul 11 23:17:25 2008 +0200
    16.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jul 14 11:04:42 2008 +0200
    16.3 @@ -1077,8 +1077,8 @@
    16.4    "plusinf p = p"
    16.5  
    16.6  recdef \<delta> "measure size"
    16.7 -  "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)" 
    16.8 -  "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)" 
    16.9 +  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
   16.10 +  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
   16.11    "\<delta> (Dvd i (CN 0 c e)) = i"
   16.12    "\<delta> (NDvd i (CN 0 c e)) = i"
   16.13    "\<delta> p = 1"
   16.14 @@ -1110,20 +1110,20 @@
   16.15  proof (induct p rule: iszlfm.induct)
   16.16    case (1 p q) 
   16.17    let ?d = "\<delta> (And p q)"
   16.18 -  from prems ilcm_pos have dp: "?d >0" by simp
   16.19 +  from prems zlcm_pos have dp: "?d >0" by simp
   16.20    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
   16.21 -  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1)
   16.22 +  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_zlcm_self1)
   16.23    have "\<delta> q dvd \<delta> (And p q)" using prems by simp
   16.24 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
   16.25 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
   16.26    from th th' dp show ?case by simp
   16.27  next
   16.28    case (2 p q)  
   16.29    let ?d = "\<delta> (And p q)"
   16.30 -  from prems ilcm_pos have dp: "?d >0" by simp
   16.31 +  from prems zlcm_pos have dp: "?d >0" by simp
   16.32    have "\<delta> p dvd \<delta> (And p q)" using prems by simp
   16.33 -  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1)
   16.34 +  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_zlcm_self1)
   16.35    have "\<delta> q dvd \<delta> (And p q)" using prems by simp
   16.36 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
   16.37 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
   16.38    from th th' dp show ?case by simp
   16.39  qed simp_all
   16.40  
   16.41 @@ -1162,8 +1162,8 @@
   16.42    "d\<beta> p = (\<lambda> k. True)"
   16.43  
   16.44  recdef \<zeta> "measure size"
   16.45 -  "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)" 
   16.46 -  "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)" 
   16.47 +  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   16.48 +  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   16.49    "\<zeta> (Eq  (CN 0 c e)) = c"
   16.50    "\<zeta> (NEq (CN 0 c e)) = c"
   16.51    "\<zeta> (Lt  (CN 0 c e)) = c"
   16.52 @@ -1412,19 +1412,19 @@
   16.53  using linp
   16.54  proof(induct p rule: iszlfm.induct)
   16.55    case (1 p q)
   16.56 -  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   16.57 -  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)"  by simp
   16.58 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   16.59 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   16.60 -    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
   16.61 +  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   16.62 +  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)"  by simp
   16.63 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   16.64 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   16.65 +    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   16.66  next
   16.67    case (2 p q)
   16.68 -  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   16.69 -  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
   16.70 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   16.71 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"] 
   16.72 -    dl1 dl2 show ?case by (auto simp add: ilcm_pos)
   16.73 -qed (auto simp add: ilcm_pos)
   16.74 +  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   16.75 +  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   16.76 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   16.77 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   16.78 +    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   16.79 +qed (auto simp add: zlcm_pos)
   16.80  
   16.81  lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
   16.82    shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"