new GCD library, courtesy of Jeremy Avigad
authorhuffman
Wed Jun 17 16:55:01 2009 -0700 (2009-06-17)
changeset 317061db0c8f235fb
parent 31664 ee3c9e31e029
child 31707 678d294a563c
new GCD library, courtesy of Jeremy Avigad
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/GCD.thy
src/HOL/IsaMakefile
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Legacy_GCD.thy
src/HOL/Library/Primes.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/Tools/transfer_data.ML
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Jun 16 22:07:39 2009 -0700
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Jun 17 16:55:01 2009 -0700
     1.3 @@ -478,8 +478,8 @@
     1.4    by (induct t rule: maxcoeff.induct, auto)
     1.5  
     1.6  recdef numgcdh "measure size"
     1.7 -  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
     1.8 -  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
     1.9 +  "numgcdh (C i) = (\<lambda>g. gcd i g)"
    1.10 +  "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
    1.11    "numgcdh t = (\<lambda>g. 1)"
    1.12  defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
    1.13  
    1.14 @@ -512,11 +512,11 @@
    1.15    assumes g0: "numgcd t = 0"
    1.16    shows "Inum bs t = 0"
    1.17    using g0[simplified numgcd_def] 
    1.18 -  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    1.19 +  by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
    1.20  
    1.21  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    1.22    using gp
    1.23 -  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
    1.24 +  by (induct t rule: numgcdh.induct, auto)
    1.25  
    1.26  lemma numgcd_pos: "numgcd t \<ge>0"
    1.27    by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
    1.28 @@ -551,15 +551,15 @@
    1.29    from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
    1.30  qed simp_all
    1.31  
    1.32 -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))"
    1.33 -  apply (cases "abs i = 0", simp_all add: zgcd_def)
    1.34 +lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
    1.35 +  apply (cases "abs i = 0", simp_all add: gcd_int_def)
    1.36    apply (cases "abs j = 0", simp_all)
    1.37    apply (cases "abs i = 1", simp_all)
    1.38    apply (cases "abs j = 1", simp_all)
    1.39    apply auto
    1.40    done
    1.41  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    1.42 -  by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
    1.43 +  by (induct t rule: numgcdh.induct, auto)
    1.44  
    1.45  lemma dvdnumcoeff_aux:
    1.46    assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
    1.47 @@ -568,22 +568,22 @@
    1.48  proof(induct t rule: numgcdh.induct)
    1.49    case (2 n c t) 
    1.50    let ?g = "numgcdh t m"
    1.51 -  from prems have th:"zgcd c ?g > 1" by simp
    1.52 +  from prems have th:"gcd c ?g > 1" by simp
    1.53    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    1.54    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    1.55    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    1.56      have th: "dvdnumcoeff t ?g" by simp
    1.57 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    1.58 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
    1.59 +    have th': "gcd c ?g dvd ?g" by simp
    1.60 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    1.61    moreover {assume "abs c = 0 \<and> ?g > 1"
    1.62      with prems have th: "dvdnumcoeff t ?g" by simp
    1.63 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    1.64 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
    1.65 +    have th': "gcd c ?g dvd ?g" by simp
    1.66 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp
    1.67      hence ?case by simp }
    1.68    moreover {assume "abs c > 1" and g0:"?g = 0" 
    1.69      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    1.70    ultimately show ?case by blast
    1.71 -qed(auto simp add: zgcd_zdvd1)
    1.72 +qed auto
    1.73  
    1.74  lemma dvdnumcoeff_aux2:
    1.75    assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
    1.76 @@ -727,7 +727,7 @@
    1.77  constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
    1.78    "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
    1.79     (let t' = simpnum t ; g = numgcd t' in 
    1.80 -      if g > 1 then (let g' = zgcd n g in 
    1.81 +      if g > 1 then (let g' = gcd n g in 
    1.82          if g' = 1 then (t',n) 
    1.83          else (reducecoeffh t' g', n div g')) 
    1.84        else (t',n))))"
    1.85 @@ -738,23 +738,23 @@
    1.86  proof-
    1.87    let ?t' = "simpnum t"
    1.88    let ?g = "numgcd ?t'"
    1.89 -  let ?g' = "zgcd n ?g"
    1.90 +  let ?g' = "gcd n ?g"
    1.91    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
    1.92    moreover
    1.93    { assume nnz: "n \<noteq> 0"
    1.94      {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
    1.95      moreover
    1.96      {assume g1:"?g>1" hence g0: "?g > 0" by simp
    1.97 -      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
    1.98 -      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith 
    1.99 +      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   1.100 +      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith 
   1.101        hence "?g'= 1 \<or> ?g' > 1" by arith
   1.102        moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
   1.103        moreover {assume g'1:"?g'>1"
   1.104  	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
   1.105  	let ?tt = "reducecoeffh ?t' ?g'"
   1.106  	let ?t = "Inum bs ?tt"
   1.107 -	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
   1.108 -	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
   1.109 +	have gpdg: "?g' dvd ?g" by simp
   1.110 +	have gpdd: "?g' dvd n" by simp 
   1.111  	have gpdgp: "?g' dvd ?g'" by simp
   1.112  	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   1.113  	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   1.114 @@ -774,21 +774,21 @@
   1.115  proof-
   1.116      let ?t' = "simpnum t"
   1.117    let ?g = "numgcd ?t'"
   1.118 -  let ?g' = "zgcd n ?g"
   1.119 +  let ?g' = "gcd n ?g"
   1.120    {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   1.121    moreover
   1.122    { assume nnz: "n \<noteq> 0"
   1.123      {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   1.124      moreover
   1.125      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   1.126 -      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   1.127 -      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   1.128 +      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   1.129 +      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
   1.130        hence "?g'= 1 \<or> ?g' > 1" by arith
   1.131        moreover {assume "?g'=1" hence ?thesis using prems 
   1.132  	  by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
   1.133        moreover {assume g'1:"?g'>1"
   1.134 -	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
   1.135 -	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
   1.136 +	have gpdg: "?g' dvd ?g" by simp
   1.137 +	have gpdd: "?g' dvd n" by simp 
   1.138  	have gpdgp: "?g' dvd ?g'" by simp
   1.139  	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   1.140  	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Jun 16 22:07:39 2009 -0700
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Jun 17 16:55:01 2009 -0700
     2.3 @@ -642,9 +642,9 @@
     2.4    done
     2.5  
     2.6  recdef numgcdh "measure size"
     2.7 -  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
     2.8 -  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
     2.9 -  "numgcdh (CF c s t) = (\<lambda>g. zgcd c (numgcdh t g))"
    2.10 +  "numgcdh (C i) = (\<lambda>g. gcd i g)"
    2.11 +  "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
    2.12 +  "numgcdh (CF c s t) = (\<lambda>g. gcd 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: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
    2.21 +    by (induct t rule: numgcdh.induct, auto)
    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: zgcd_def)
    2.28 +  by (induct t rule: numgcdh.induct, auto)
    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 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.37 -  apply (unfold zgcd_def)
    2.38 +lemma zgcd_gt1: "gcd i j > (1::int) \<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 gcd_int_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:zgcd0)
    2.48 +  by (induct t rule: numgcdh.induct, auto)
    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:"zgcd c ?g > 1" by simp
    2.57 +  from prems have th:"gcd c ?g > 1" by simp
    2.58    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.59    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    2.60    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    2.61      have th: "dvdnumcoeff t ?g" by simp
    2.62 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    2.63 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
    2.64 +    have th': "gcd c ?g dvd ?g" by simp
    2.65 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    2.66    moreover {assume "abs c = 0 \<and> ?g > 1"
    2.67      with prems have th: "dvdnumcoeff t ?g" by simp
    2.68 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    2.69 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
    2.70 +    have th': "gcd c ?g dvd ?g" by simp
    2.71 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp
    2.72      hence ?case by simp }
    2.73    moreover {assume "abs c > 1" and g0:"?g = 0" 
    2.74      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    2.75 @@ -774,22 +774,22 @@
    2.76  next
    2.77    case (3 c s t) 
    2.78    let ?g = "numgcdh t m"
    2.79 -  from prems have th:"zgcd c ?g > 1" by simp
    2.80 +  from prems have th:"gcd c ?g > 1" by simp
    2.81    from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
    2.82    have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
    2.83    moreover {assume "abs c > 1" and gp: "?g > 1" with prems
    2.84      have th: "dvdnumcoeff t ?g" by simp
    2.85 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    2.86 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
    2.87 +    have th': "gcd c ?g dvd ?g" by simp
    2.88 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
    2.89    moreover {assume "abs c = 0 \<and> ?g > 1"
    2.90      with prems have th: "dvdnumcoeff t ?g" by simp
    2.91 -    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
    2.92 -    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
    2.93 +    have th': "gcd c ?g dvd ?g" by simp
    2.94 +    from dvdnumcoeff_trans[OF th' th] have ?case by simp
    2.95      hence ?case by simp }
    2.96    moreover {assume "abs c > 1" and g0:"?g = 0" 
    2.97      from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
    2.98    ultimately show ?case by blast
    2.99 -qed(auto simp add: zgcd_zdvd1)
   2.100 +qed auto
   2.101  
   2.102  lemma dvdnumcoeff_aux2:
   2.103    assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
   2.104 @@ -1041,7 +1041,7 @@
   2.105  constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
   2.106    "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
   2.107     (let t' = simpnum t ; g = numgcd t' in 
   2.108 -      if g > 1 then (let g' = zgcd n g in 
   2.109 +      if g > 1 then (let g' = gcd n g in 
   2.110          if g' = 1 then (t',n) 
   2.111          else (reducecoeffh t' g', n div g')) 
   2.112        else (t',n))))"
   2.113 @@ -1052,23 +1052,23 @@
   2.114  proof-
   2.115    let ?t' = "simpnum t"
   2.116    let ?g = "numgcd ?t'"
   2.117 -  let ?g' = "zgcd n ?g"
   2.118 +  let ?g' = "gcd n ?g"
   2.119    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.120    moreover
   2.121    { assume nnz: "n \<noteq> 0"
   2.122      {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.123      moreover
   2.124      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.125 -      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.126 -      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.127 +      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.128 +      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
   2.129        hence "?g'= 1 \<or> ?g' > 1" by arith
   2.130        moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   2.131        moreover {assume g'1:"?g'>1"
   2.132  	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
   2.133  	let ?tt = "reducecoeffh ?t' ?g'"
   2.134  	let ?t = "Inum bs ?tt"
   2.135 -	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
   2.136 -	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
   2.137 +	have gpdg: "?g' dvd ?g" by simp
   2.138 +	have gpdd: "?g' dvd n" by simp
   2.139  	have gpdgp: "?g' dvd ?g'" by simp
   2.140  	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   2.141  	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
   2.142 @@ -1088,21 +1088,21 @@
   2.143  proof-
   2.144      let ?t' = "simpnum t"
   2.145    let ?g = "numgcd ?t'"
   2.146 -  let ?g' = "zgcd n ?g"
   2.147 +  let ?g' = "gcd n ?g"
   2.148    {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   2.149    moreover
   2.150    { assume nnz: "n \<noteq> 0"
   2.151      {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}
   2.152      moreover
   2.153      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.154 -      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.155 -      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
   2.156 +      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   2.157 +      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
   2.158        hence "?g'= 1 \<or> ?g' > 1" by arith
   2.159        moreover {assume "?g'=1" hence ?thesis using prems 
   2.160  	  by (auto simp add: Let_def simp_num_pair_def)}
   2.161        moreover {assume g'1:"?g'>1"
   2.162 -	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
   2.163 -	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
   2.164 +	have gpdg: "?g' dvd ?g" by simp
   2.165 +	have gpdd: "?g' dvd n" by simp
   2.166  	have gpdgp: "?g' dvd ?g'" by simp
   2.167  	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
   2.168  	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
   2.169 @@ -1219,7 +1219,7 @@
   2.170  constdefs simpdvd:: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)"
   2.171    "simpdvd d t \<equiv> 
   2.172     (let g = numgcd t in 
   2.173 -      if g > 1 then (let g' = zgcd d g in 
   2.174 +      if g > 1 then (let g' = gcd d g in 
   2.175          if g' = 1 then (d, t) 
   2.176          else (d div g',reducecoeffh t g')) 
   2.177        else (d, t))"
   2.178 @@ -1228,20 +1228,20 @@
   2.179    shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)"
   2.180  proof-
   2.181    let ?g = "numgcd t"
   2.182 -  let ?g' = "zgcd d ?g"
   2.183 +  let ?g' = "gcd d ?g"
   2.184    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)}
   2.185    moreover
   2.186    {assume g1:"?g>1" hence g0: "?g > 0" by simp
   2.187 -    from zgcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
   2.188 -    hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="numgcd t"] by arith
   2.189 +    from g1 dnz have gp0: "?g' \<noteq> 0" by simp
   2.190 +    hence g'p: "?g' > 0" using int_gcd_ge_0[where x="d" and y="numgcd t"] by arith
   2.191      hence "?g'= 1 \<or> ?g' > 1" by arith
   2.192      moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}
   2.193      moreover {assume g'1:"?g'>1"
   2.194        from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
   2.195        let ?tt = "reducecoeffh t ?g'"
   2.196        let ?t = "Inum bs ?tt"
   2.197 -      have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
   2.198 -      have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1) 
   2.199 +      have gpdg: "?g' dvd ?g" by simp
   2.200 +      have gpdd: "?g' dvd d" by simp
   2.201        have gpdgp: "?g' dvd ?g'" by simp
   2.202        from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
   2.203        have th2:"real ?g' * ?t = Inum bs t" by simp
   2.204 @@ -2093,8 +2093,8 @@
   2.205    "plusinf p = p"
   2.206  
   2.207  recdef \<delta> "measure size"
   2.208 -  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
   2.209 -  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
   2.210 +  "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 
   2.211 +  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
   2.212    "\<delta> (Dvd i (CN 0 c e)) = i"
   2.213    "\<delta> (NDvd i (CN 0 c e)) = i"
   2.214    "\<delta> p = 1"
   2.215 @@ -2126,20 +2126,20 @@
   2.216  proof (induct p rule: iszlfm.induct)
   2.217    case (1 p q) 
   2.218    let ?d = "\<delta> (And p q)"
   2.219 -  from prems zlcm_pos have dp: "?d >0" by simp
   2.220 +  from prems int_lcm_pos have dp: "?d >0" by simp
   2.221    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
   2.222     hence th: "d\<delta> p ?d" 
   2.223 -     using delta_mono prems by (auto simp del: dvd_zlcm_self1)
   2.224 +     using delta_mono prems by (auto simp del: int_lcm_dvd1)
   2.225    have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 
   2.226 -  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_zlcm_self2)
   2.227 +  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
   2.228    from th th' dp show ?case by simp 
   2.229  next
   2.230    case (2 p q)  
   2.231    let ?d = "\<delta> (And p q)"
   2.232 -  from prems zlcm_pos have dp: "?d >0" by simp
   2.233 +  from prems int_lcm_pos have dp: "?d >0" by simp
   2.234    have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
   2.235 -    by (auto simp del: dvd_zlcm_self1)
   2.236 -  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.237 +    by (auto simp del: int_lcm_dvd1)
   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: int_lcm_dvd2)
   2.239    from th th' dp show ?case by simp 
   2.240  qed simp_all
   2.241  
   2.242 @@ -2388,8 +2388,8 @@
   2.243    "d\<beta> p = (\<lambda> k. True)"
   2.244  
   2.245  recdef \<zeta> "measure size"
   2.246 -  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   2.247 -  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
   2.248 +  "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
   2.249 +  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" 
   2.250    "\<zeta> (Eq  (CN 0 c e)) = c"
   2.251    "\<zeta> (NEq (CN 0 c e)) = c"
   2.252    "\<zeta> (Lt  (CN 0 c e)) = c"
   2.253 @@ -2510,19 +2510,19 @@
   2.254  using linp
   2.255  proof(induct p rule: iszlfm.induct)
   2.256    case (1 p q)
   2.257 -  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.258 -  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.259 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.260 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.261 -    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   2.262 +  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   2.263 +  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   2.264 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   2.265 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   2.266 +    dl1 dl2 show ?case by (auto simp add: int_lcm_pos)
   2.267  next
   2.268    case (2 p q)
   2.269 -  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.270 -  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
   2.271 -  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.272 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
   2.273 -    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
   2.274 -qed (auto simp add: zlcm_pos)
   2.275 +  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   2.276 +  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   2.277 +  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   2.278 +    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
   2.279 +    dl1 dl2 show ?case by (auto simp add: int_lcm_pos)
   2.280 +qed (auto simp add: int_lcm_pos)
   2.281  
   2.282  lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
   2.283    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.284 @@ -4173,9 +4173,9 @@
   2.285  
   2.286  lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
   2.287    by (induct p rule: isrlfm.induct, auto)
   2.288 -lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
   2.289 +lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \<le> i"
   2.290  proof-
   2.291 -  from zgcd_zdvd1 have th: "zgcd i j dvd i" by blast
   2.292 +  from int_gcd_dvd1 have th: "gcd i j dvd i" by blast
   2.293    from zdvd_imp_le[OF th ip] show ?thesis .
   2.294  qed
   2.295  
   2.296 @@ -5119,9 +5119,9 @@
   2.297    let ?M = "?I x (minusinf ?rq)"
   2.298    let ?P = "?I x (plusinf ?rq)"
   2.299    have MF: "?M = False"
   2.300 -    apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.301 +    apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.302      by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
   2.303 -  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.304 +  have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
   2.305      by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
   2.306    have "(\<exists> x. ?I x ?q ) = 
   2.307      ((?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.308 @@ -5286,7 +5286,7 @@
   2.309    let ?F = "\<lambda> p. \<exists> a \<in> set (\<Upsilon> p). \<exists> b \<in> set (\<Upsilon> p). ?I x (\<upsilon> p (?g(a,b)))"
   2.310    let ?ep = "evaldjf (\<upsilon> ?q) ?Y"
   2.311    from rlfm_l[OF qf] have lq: "isrlfm ?q" 
   2.312 -    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def zgcd_def)
   2.313 +    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def)
   2.314    from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   2.315    from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   2.316    from U_l UpU 
     3.1 --- a/src/HOL/GCD.thy	Tue Jun 16 22:07:39 2009 -0700
     3.2 +++ b/src/HOL/GCD.thy	Wed Jun 17 16:55:01 2009 -0700
     3.3 @@ -1,202 +1,563 @@
     3.4 -(*  Title:      HOL/GCD.thy
     3.5 -    Author:     Christophe Tabacznyj and Lawrence C Paulson
     3.6 -    Copyright   1996  University of Cambridge
     3.7 +(*  Title:      GCD.thy
     3.8 +    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     3.9 +                Thomas M. Rasmussen, Jeremy Avigad
    3.10 +
    3.11 +
    3.12 +This file deals with the functions gcd and lcm, and properties of
    3.13 +primes. Definitions and lemmas are proved uniformly for the natural
    3.14 +numbers and integers.
    3.15 +
    3.16 +This file combines and revises a number of prior developments.
    3.17 +
    3.18 +The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    3.19 +and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    3.20 +gcd, lcm, and prime for the natural numbers.
    3.21 +
    3.22 +The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    3.23 +extended gcd, lcm, primes to the integers. Amine Chaieb provided
    3.24 +another extension of the notions to the integers, and added a number
    3.25 +of results to "Primes" and "GCD". IntPrimes also defined and developed
    3.26 +the congruence relations on the integers. The notion was extended to
    3.27 +the natural numbers by Chiaeb.
    3.28 +
    3.29  *)
    3.30  
    3.31 -header {* The Greatest Common Divisor *}
    3.32 +
    3.33 +header {* GCD *}
    3.34  
    3.35  theory GCD
    3.36 -imports Main
    3.37 +imports NatTransfer
    3.38 +begin
    3.39 +
    3.40 +declare One_nat_def [simp del]
    3.41 +
    3.42 +subsection {* gcd *}
    3.43 +
    3.44 +class gcd = one +
    3.45 +
    3.46 +fixes
    3.47 +  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    3.48 +  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    3.49 +
    3.50  begin
    3.51  
    3.52 -text {*
    3.53 -  See \cite{davenport92}. \bigskip
    3.54 -*}
    3.55 +abbreviation
    3.56 +  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.57 +where
    3.58 +  "coprime x y == (gcd x y = 1)"
    3.59 +
    3.60 +end
    3.61 +
    3.62 +class prime = one +
    3.63 +
    3.64 +fixes
    3.65 +  prime :: "'a \<Rightarrow> bool"
    3.66 +
    3.67 +
    3.68 +(* definitions for the natural numbers *)
    3.69 +
    3.70 +instantiation nat :: gcd
    3.71 +
    3.72 +begin
    3.73  
    3.74 -subsection {* Specification of GCD on nats *}
    3.75 +fun
    3.76 +  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    3.77 +where
    3.78 +  "gcd_nat x y =
    3.79 +   (if y = 0 then x else gcd y (x mod y))"
    3.80 +
    3.81 +definition
    3.82 +  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    3.83 +where
    3.84 +  "lcm_nat x y = x * y div (gcd x y)"
    3.85 +
    3.86 +instance proof qed
    3.87 +
    3.88 +end
    3.89 +
    3.90 +
    3.91 +instantiation nat :: prime
    3.92 +
    3.93 +begin
    3.94  
    3.95  definition
    3.96 -  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    3.97 -  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    3.98 -    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    3.99 +  prime_nat :: "nat \<Rightarrow> bool"
   3.100 +where
   3.101 +  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
   3.102 +
   3.103 +instance proof qed
   3.104  
   3.105 -text {* Uniqueness *}
   3.106 +end
   3.107 +
   3.108  
   3.109 -lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
   3.110 -  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
   3.111 +(* definitions for the integers *)
   3.112 +
   3.113 +instantiation int :: gcd
   3.114  
   3.115 -text {* Connection to divides relation *}
   3.116 +begin
   3.117  
   3.118 -lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
   3.119 -  by (auto simp add: is_gcd_def)
   3.120 +definition
   3.121 +  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   3.122 +where
   3.123 +  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
   3.124  
   3.125 -text {* Commutativity *}
   3.126 +definition
   3.127 +  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   3.128 +where
   3.129 +  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
   3.130  
   3.131 -lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
   3.132 -  by (auto simp add: is_gcd_def)
   3.133 +instance proof qed
   3.134 +
   3.135 +end
   3.136  
   3.137  
   3.138 -subsection {* GCD on nat by Euclid's algorithm *}
   3.139 +instantiation int :: prime
   3.140 +
   3.141 +begin
   3.142 +
   3.143 +definition
   3.144 +  prime_int :: "int \<Rightarrow> bool"
   3.145 +where
   3.146 +  "prime_int p = prime (nat p)"
   3.147 +
   3.148 +instance proof qed
   3.149 +
   3.150 +end
   3.151 +
   3.152 +
   3.153 +subsection {* Set up Transfer *}
   3.154 +
   3.155 +
   3.156 +lemma transfer_nat_int_gcd:
   3.157 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   3.158 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   3.159 +  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   3.160 +  unfolding gcd_int_def lcm_int_def prime_int_def
   3.161 +  by auto
   3.162  
   3.163 -fun
   3.164 -  gcd  :: "nat => nat => nat"
   3.165 -where
   3.166 -  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
   3.167 -lemma gcd_induct [case_names "0" rec]:
   3.168 +lemma transfer_nat_int_gcd_closures:
   3.169 +  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   3.170 +  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   3.171 +  by (auto simp add: gcd_int_def lcm_int_def)
   3.172 +
   3.173 +declare TransferMorphism_nat_int[transfer add return:
   3.174 +    transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   3.175 +
   3.176 +lemma transfer_int_nat_gcd:
   3.177 +  "gcd (int x) (int y) = int (gcd x y)"
   3.178 +  "lcm (int x) (int y) = int (lcm x y)"
   3.179 +  "prime (int x) = prime x"
   3.180 +  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
   3.181 +
   3.182 +lemma transfer_int_nat_gcd_closures:
   3.183 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   3.184 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   3.185 +  by (auto simp add: gcd_int_def lcm_int_def)
   3.186 +
   3.187 +declare TransferMorphism_int_nat[transfer add return:
   3.188 +    transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   3.189 +
   3.190 +
   3.191 +
   3.192 +subsection {* GCD *}
   3.193 +
   3.194 +(* was gcd_induct *)
   3.195 +lemma nat_gcd_induct:
   3.196    fixes m n :: nat
   3.197    assumes "\<And>m. P m 0"
   3.198      and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   3.199    shows "P m n"
   3.200 -proof (induct m n rule: gcd.induct)
   3.201 -  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
   3.202 -qed
   3.203 +  apply (rule gcd_nat.induct)
   3.204 +  apply (case_tac "y = 0")
   3.205 +  using assms apply simp_all
   3.206 +done
   3.207 +
   3.208 +(* specific to int *)
   3.209 +
   3.210 +lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
   3.211 +  by (simp add: gcd_int_def)
   3.212 +
   3.213 +lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
   3.214 +  by (simp add: gcd_int_def)
   3.215 +
   3.216 +lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
   3.217 +  by (simp add: gcd_int_def)
   3.218 +
   3.219 +lemma int_gcd_cases:
   3.220 +  fixes x :: int and y
   3.221 +  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   3.222 +      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   3.223 +      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   3.224 +      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   3.225 +  shows "P (gcd x y)"
   3.226 +by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
   3.227  
   3.228 -lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
   3.229 -  by simp
   3.230 +lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
   3.231 +  by (simp add: gcd_int_def)
   3.232 +
   3.233 +lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
   3.234 +  by (simp add: lcm_int_def)
   3.235 +
   3.236 +lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
   3.237 +  by (simp add: lcm_int_def)
   3.238 +
   3.239 +lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
   3.240 +  by (simp add: lcm_int_def)
   3.241  
   3.242 -lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
   3.243 +lemma int_lcm_cases:
   3.244 +  fixes x :: int and y
   3.245 +  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   3.246 +      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   3.247 +      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   3.248 +      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   3.249 +  shows "P (lcm x y)"
   3.250 +by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
   3.251 +
   3.252 +lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
   3.253 +  by (simp add: lcm_int_def)
   3.254 +
   3.255 +(* was gcd_0, etc. *)
   3.256 +lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
   3.257    by simp
   3.258  
   3.259 -lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
   3.260 +(* was igcd_0, etc. *)
   3.261 +lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
   3.262 +  by (unfold gcd_int_def, auto)
   3.263 +
   3.264 +lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
   3.265    by simp
   3.266  
   3.267 -lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
   3.268 +lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
   3.269 +  by (unfold gcd_int_def, auto)
   3.270 +
   3.271 +lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
   3.272 +  by (case_tac "y = 0", auto)
   3.273 +
   3.274 +(* weaker, but useful for the simplifier *)
   3.275 +
   3.276 +lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   3.277 +  by simp
   3.278 +
   3.279 +lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   3.280    by simp
   3.281  
   3.282 -lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
   3.283 -  unfolding One_nat_def by (rule gcd_1)
   3.284 +lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   3.285 +  by (simp add: One_nat_def)
   3.286 +
   3.287 +lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
   3.288 +  by (simp add: gcd_int_def)
   3.289  
   3.290 -declare gcd.simps [simp del]
   3.291 +lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
   3.292 +  by simp
   3.293 +
   3.294 +lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
   3.295 +  by (subst int_gcd_abs, auto simp add: gcd_int_def)
   3.296 +
   3.297 +declare gcd_nat.simps [simp del]
   3.298  
   3.299  text {*
   3.300    \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   3.301    conjunctions don't seem provable separately.
   3.302  *}
   3.303  
   3.304 -lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
   3.305 -  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
   3.306 -  apply (induct m n rule: gcd_induct)
   3.307 -     apply (simp_all add: gcd_non_0)
   3.308 +lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
   3.309 +  and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
   3.310 +  apply (induct m n rule: nat_gcd_induct)
   3.311 +  apply (simp_all add: nat_gcd_non_0)
   3.312    apply (blast dest: dvd_mod_imp_dvd)
   3.313 -  done
   3.314 +done
   3.315 +
   3.316 +thm nat_gcd_dvd1 [transferred]
   3.317 +
   3.318 +lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
   3.319 +  apply (subst int_gcd_abs)
   3.320 +  apply (rule dvd_trans)
   3.321 +  apply (rule nat_gcd_dvd1 [transferred])
   3.322 +  apply auto
   3.323 +done
   3.324  
   3.325 -text {*
   3.326 -  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   3.327 -  naturals, if @{term k} divides @{term m} and @{term k} divides
   3.328 -  @{term n} then @{term k} divides @{term "gcd m n"}.
   3.329 -*}
   3.330 +lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
   3.331 +  apply (subst int_gcd_abs)
   3.332 +  apply (rule dvd_trans)
   3.333 +  apply (rule nat_gcd_dvd2 [transferred])
   3.334 +  apply auto
   3.335 +done
   3.336 +
   3.337 +lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   3.338 +  by (rule dvd_imp_le, auto)
   3.339 +
   3.340 +lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   3.341 +  by (rule dvd_imp_le, auto)
   3.342 +
   3.343 +lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   3.344 +  by (rule zdvd_imp_le, auto)
   3.345  
   3.346 -lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   3.347 -  by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
   3.348 +lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   3.349 +  by (rule zdvd_imp_le, auto)
   3.350 +
   3.351 +lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   3.352 +  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
   3.353 +
   3.354 +lemma int_gcd_greatest:
   3.355 +  assumes "(k::int) dvd m" and "k dvd n"
   3.356 +  shows "k dvd gcd m n"
   3.357 +
   3.358 +  apply (subst int_gcd_abs)
   3.359 +  apply (subst abs_dvd_iff [symmetric])
   3.360 +  apply (rule nat_gcd_greatest [transferred])
   3.361 +  using prems apply auto
   3.362 +done
   3.363  
   3.364 -text {*
   3.365 -  \medskip Function gcd yields the Greatest Common Divisor.
   3.366 -*}
   3.367 +lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
   3.368 +    (k dvd m & k dvd n)"
   3.369 +  by (blast intro!: nat_gcd_greatest intro: dvd_trans)
   3.370 +
   3.371 +lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   3.372 +  by (blast intro!: int_gcd_greatest intro: dvd_trans)
   3.373  
   3.374 -lemma is_gcd: "is_gcd m n (gcd m n) "
   3.375 -  by (simp add: is_gcd_def gcd_greatest)
   3.376 +lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   3.377 +  by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
   3.378  
   3.379 +lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   3.380 +  by (auto simp add: gcd_int_def)
   3.381  
   3.382 -subsection {* Derived laws for GCD *}
   3.383 +lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   3.384 +  by (insert nat_gcd_zero [of m n], arith)
   3.385  
   3.386 -lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   3.387 -  by (blast intro!: gcd_greatest intro: dvd_trans)
   3.388 +lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   3.389 +  by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
   3.390 +
   3.391 +lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
   3.392 +  by (rule dvd_anti_sym, auto)
   3.393  
   3.394 -lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   3.395 -  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   3.396 +lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
   3.397 +  by (auto simp add: gcd_int_def nat_gcd_commute)
   3.398 +
   3.399 +lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   3.400 +  apply (rule dvd_anti_sym)
   3.401 +  apply (blast intro: dvd_trans)+
   3.402 +done
   3.403  
   3.404 -lemma gcd_commute: "gcd m n = gcd n m"
   3.405 -  apply (rule is_gcd_unique)
   3.406 -   apply (rule is_gcd)
   3.407 -  apply (subst is_gcd_commute)
   3.408 -  apply (simp add: is_gcd)
   3.409 -  done
   3.410 +lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   3.411 +  by (auto simp add: gcd_int_def nat_gcd_assoc)
   3.412 +
   3.413 +lemma nat_gcd_left_commute: "gcd (k::nat) (gcd m n) = gcd m (gcd k n)"
   3.414 +  apply (rule nat_gcd_commute [THEN trans])
   3.415 +  apply (rule nat_gcd_assoc [THEN trans])
   3.416 +  apply (rule nat_gcd_commute [THEN arg_cong])
   3.417 +done
   3.418 +
   3.419 +lemma int_gcd_left_commute: "gcd (k::int) (gcd m n) = gcd m (gcd k n)"
   3.420 +  apply (rule int_gcd_commute [THEN trans])
   3.421 +  apply (rule int_gcd_assoc [THEN trans])
   3.422 +  apply (rule int_gcd_commute [THEN arg_cong])
   3.423 +done
   3.424 +
   3.425 +lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
   3.426 +  -- {* gcd is an AC-operator *}
   3.427  
   3.428 -lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
   3.429 -  apply (rule is_gcd_unique)
   3.430 -   apply (rule is_gcd)
   3.431 -  apply (simp add: is_gcd_def)
   3.432 -  apply (blast intro: dvd_trans)
   3.433 -  done
   3.434 +lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
   3.435 +
   3.436 +lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
   3.437 +  by (subst nat_gcd_commute, simp)
   3.438 +
   3.439 +lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
   3.440 +  by (subst nat_gcd_commute, simp add: One_nat_def)
   3.441 +
   3.442 +lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
   3.443 +  by (subst int_gcd_commute, simp)
   3.444  
   3.445 -lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
   3.446 -  by (simp add: gcd_commute)
   3.447 +lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
   3.448 +    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   3.449 +  apply auto
   3.450 +  apply (rule dvd_anti_sym)
   3.451 +  apply (erule (1) nat_gcd_greatest)
   3.452 +  apply auto
   3.453 +done
   3.454  
   3.455 -lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
   3.456 -  unfolding One_nat_def by (rule gcd_1_left)
   3.457 +lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   3.458 +    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   3.459 +  apply (case_tac "d = 0")
   3.460 +  apply force
   3.461 +  apply (rule iffI)
   3.462 +  apply (rule zdvd_anti_sym)
   3.463 +  apply arith
   3.464 +  apply (subst int_gcd_pos)
   3.465 +  apply clarsimp
   3.466 +  apply (drule_tac x = "d + 1" in spec)
   3.467 +  apply (frule zdvd_imp_le)
   3.468 +  apply (auto intro: int_gcd_greatest)
   3.469 +done
   3.470  
   3.471  text {*
   3.472    \medskip Multiplication laws
   3.473  *}
   3.474  
   3.475 -lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
   3.476 +lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   3.477      -- {* \cite[page 27]{davenport92} *}
   3.478 -  apply (induct m n rule: gcd_induct)
   3.479 -   apply simp
   3.480 +  apply (induct m n rule: nat_gcd_induct)
   3.481 +  apply simp
   3.482    apply (case_tac "k = 0")
   3.483 -   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   3.484 -  done
   3.485 +  apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
   3.486 +done
   3.487  
   3.488 -lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
   3.489 -  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   3.490 -  done
   3.491 +lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   3.492 +  apply (subst (1 2) int_gcd_abs)
   3.493 +  apply (simp add: abs_mult)
   3.494 +  apply (rule nat_gcd_mult_distrib [transferred])
   3.495 +  apply auto
   3.496 +done
   3.497  
   3.498 -lemma gcd_self [simp, algebra]: "gcd k k = k"
   3.499 -  apply (rule gcd_mult [of k 1, simplified])
   3.500 -  done
   3.501 +lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
   3.502 +  by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
   3.503  
   3.504 -lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
   3.505 -  apply (insert gcd_mult_distrib2 [of m k n])
   3.506 +lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
   3.507 +  by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
   3.508 +
   3.509 +lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   3.510 +  apply (insert nat_gcd_mult_distrib [of m k n])
   3.511    apply simp
   3.512    apply (erule_tac t = m in ssubst)
   3.513    apply simp
   3.514    done
   3.515  
   3.516 -lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
   3.517 -  by (auto intro: relprime_dvd_mult dvd_mult2)
   3.518 +lemma int_coprime_dvd_mult:
   3.519 +  assumes "coprime (k::int) n" and "k dvd m * n"
   3.520 +  shows "k dvd m"
   3.521  
   3.522 -lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   3.523 +  using prems
   3.524 +  apply (subst abs_dvd_iff [symmetric])
   3.525 +  apply (subst dvd_abs_iff [symmetric])
   3.526 +  apply (subst (asm) int_gcd_abs)
   3.527 +  apply (rule nat_coprime_dvd_mult [transferred])
   3.528 +  apply auto
   3.529 +  apply (subst abs_mult [symmetric], auto)
   3.530 +done
   3.531 +
   3.532 +lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   3.533 +    (k dvd m * n) = (k dvd m)"
   3.534 +  by (auto intro: nat_coprime_dvd_mult)
   3.535 +
   3.536 +lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
   3.537 +    (k dvd m * n) = (k dvd m)"
   3.538 +  by (auto intro: int_coprime_dvd_mult)
   3.539 +
   3.540 +lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   3.541    apply (rule dvd_anti_sym)
   3.542 -   apply (rule gcd_greatest)
   3.543 -    apply (rule_tac n = k in relprime_dvd_mult)
   3.544 -     apply (simp add: gcd_assoc)
   3.545 -     apply (simp add: gcd_commute)
   3.546 -    apply (simp_all add: mult_commute)
   3.547 -  done
   3.548 +  apply (rule nat_gcd_greatest)
   3.549 +  apply (rule_tac n = k in nat_coprime_dvd_mult)
   3.550 +  apply (simp add: nat_gcd_assoc)
   3.551 +  apply (simp add: nat_gcd_commute)
   3.552 +  apply (simp_all add: mult_commute)
   3.553 +done
   3.554  
   3.555 +lemma int_gcd_mult_cancel:
   3.556 +  assumes "coprime (k::int) n"
   3.557 +  shows "gcd (k * m) n = gcd m n"
   3.558 +
   3.559 +  using prems
   3.560 +  apply (subst (1 2) int_gcd_abs)
   3.561 +  apply (subst abs_mult)
   3.562 +  apply (rule nat_gcd_mult_cancel [transferred])
   3.563 +  apply (auto simp add: int_gcd_abs [symmetric])
   3.564 +done
   3.565  
   3.566  text {* \medskip Addition laws *}
   3.567  
   3.568 -lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
   3.569 -  by (cases "n = 0") (auto simp add: gcd_non_0)
   3.570 +lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
   3.571 +  apply (case_tac "n = 0")
   3.572 +  apply (simp_all add: nat_gcd_non_0)
   3.573 +done
   3.574 +
   3.575 +lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
   3.576 +  apply (subst (1 2) nat_gcd_commute)
   3.577 +  apply (subst add_commute)
   3.578 +  apply simp
   3.579 +done
   3.580 +
   3.581 +(* to do: add the other variations? *)
   3.582 +
   3.583 +lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   3.584 +  by (subst nat_gcd_add1 [symmetric], auto)
   3.585 +
   3.586 +lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   3.587 +  apply (subst nat_gcd_commute)
   3.588 +  apply (subst nat_gcd_diff1 [symmetric])
   3.589 +  apply auto
   3.590 +  apply (subst nat_gcd_commute)
   3.591 +  apply (subst nat_gcd_diff1)
   3.592 +  apply assumption
   3.593 +  apply (rule nat_gcd_commute)
   3.594 +done
   3.595 +
   3.596 +lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   3.597 +  apply (frule_tac b = y and a = x in pos_mod_sign)
   3.598 +  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   3.599 +  apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
   3.600 +    zmod_zminus1_eq_if)
   3.601 +  apply (frule_tac a = x in pos_mod_bound)
   3.602 +  apply (subst (1 2) nat_gcd_commute)
   3.603 +  apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
   3.604 +    nat_le_eq_zle)
   3.605 +done
   3.606  
   3.607 -lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
   3.608 -proof -
   3.609 -  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
   3.610 -  also have "... = gcd (n + m) m" by (simp add: add_commute)
   3.611 -  also have "... = gcd n m" by simp
   3.612 -  also have  "... = gcd m n" by (rule gcd_commute)
   3.613 -  finally show ?thesis .
   3.614 -qed
   3.615 +lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
   3.616 +  apply (case_tac "y = 0")
   3.617 +  apply force
   3.618 +  apply (case_tac "y > 0")
   3.619 +  apply (subst int_gcd_non_0, auto)
   3.620 +  apply (insert int_gcd_non_0 [of "-y" "-x"])
   3.621 +  apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
   3.622 +done
   3.623 +
   3.624 +lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   3.625 +  apply (case_tac "n = 0", force)
   3.626 +  apply (subst (1 2) int_gcd_red)
   3.627 +  apply auto
   3.628 +done
   3.629 +
   3.630 +lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   3.631 +  apply (subst int_gcd_commute)
   3.632 +  apply (subst add_commute)
   3.633 +  apply (subst int_gcd_add1)
   3.634 +  apply (subst int_gcd_commute)
   3.635 +  apply (rule refl)
   3.636 +done
   3.637  
   3.638 -lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
   3.639 -  apply (subst add_commute)
   3.640 -  apply (rule gcd_add2)
   3.641 -  done
   3.642 +lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   3.643 +  by (induct k, simp_all add: ring_simps)
   3.644  
   3.645 -lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
   3.646 -  by (induct k) (simp_all add: add_assoc)
   3.647 +lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   3.648 +  apply (subgoal_tac "ALL s. ALL m. ALL n.
   3.649 +      gcd m (int (s::nat) * m + n) = gcd m n")
   3.650 +  apply (case_tac "k >= 0")
   3.651 +  apply (drule_tac x = "nat k" in spec, force)
   3.652 +  apply (subst (1 2) int_gcd_neg2 [symmetric])
   3.653 +  apply (drule_tac x = "nat (- k)" in spec)
   3.654 +  apply (drule_tac x = "m" in spec)
   3.655 +  apply (drule_tac x = "-n" in spec)
   3.656 +  apply auto
   3.657 +  apply (rule nat_induct)
   3.658 +  apply auto
   3.659 +  apply (auto simp add: left_distrib)
   3.660 +  apply (subst add_assoc)
   3.661 +  apply simp
   3.662 +done
   3.663  
   3.664 -lemma gcd_dvd_prod: "gcd m n dvd m * n" 
   3.665 +(* to do: differences, and all variations of addition rules
   3.666 +    as simplification rules for nat and int *)
   3.667 +
   3.668 +lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   3.669    using mult_dvd_mono [of 1] by auto
   3.670  
   3.671 -text {*
   3.672 -  \medskip Division by gcd yields rrelatively primes.
   3.673 -*}
   3.674 +(* to do: add the three variations of these, and for ints? *)
   3.675 +
   3.676  
   3.677 -lemma div_gcd_relprime:
   3.678 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   3.679 -  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
   3.680 +subsection {* Coprimality *}
   3.681 +
   3.682 +lemma nat_div_gcd_coprime [intro]:
   3.683 +  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   3.684 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   3.685  proof -
   3.686    let ?g = "gcd a b"
   3.687    let ?a' = "a div ?g"
   3.688 @@ -207,42 +568,551 @@
   3.689    from dvdg dvdg' obtain ka kb ka' kb' where
   3.690        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   3.691      unfolding dvd_def by blast
   3.692 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
   3.693 +  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   3.694 +    by simp_all
   3.695    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   3.696      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   3.697        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   3.698 -  have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
   3.699 -  then have gp: "?g > 0" by simp
   3.700 -  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   3.701 +  have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
   3.702 +  then have gp: "?g > 0" by arith
   3.703 +  from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   3.704    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   3.705  qed
   3.706  
   3.707 +lemma int_div_gcd_coprime [intro]:
   3.708 +  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   3.709 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   3.710  
   3.711 -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"
   3.712 -proof(auto)
   3.713 -  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   3.714 -  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   3.715 -  have th: "gcd a b dvd d" by blast
   3.716 -  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   3.717 +  apply (subst (1 2 3) int_gcd_abs)
   3.718 +  apply (subst (1 2) abs_div)
   3.719 +  apply auto
   3.720 +  prefer 3
   3.721 +  apply (rule nat_div_gcd_coprime [transferred])
   3.722 +  using nz apply (auto simp add: int_gcd_abs [symmetric])
   3.723 +done
   3.724 +
   3.725 +lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   3.726 +  using nat_gcd_unique[of 1 a b, simplified] by auto
   3.727 +
   3.728 +lemma nat_coprime_Suc_0:
   3.729 +    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   3.730 +  using nat_coprime by (simp add: One_nat_def)
   3.731 +
   3.732 +lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
   3.733 +    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   3.734 +  using int_gcd_unique [of 1 a b]
   3.735 +  apply clarsimp
   3.736 +  apply (erule subst)
   3.737 +  apply (rule iffI)
   3.738 +  apply force
   3.739 +  apply (drule_tac x = "abs e" in exI)
   3.740 +  apply (case_tac "e >= 0")
   3.741 +  apply force
   3.742 +  apply force
   3.743 +done
   3.744 +
   3.745 +lemma nat_gcd_coprime:
   3.746 +  assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   3.747 +    b: "b = b' * gcd a b"
   3.748 +  shows    "coprime a' b'"
   3.749 +
   3.750 +  apply (subgoal_tac "a' = a div gcd a b")
   3.751 +  apply (erule ssubst)
   3.752 +  apply (subgoal_tac "b' = b div gcd a b")
   3.753 +  apply (erule ssubst)
   3.754 +  apply (rule nat_div_gcd_coprime)
   3.755 +  using prems
   3.756 +  apply force
   3.757 +  apply (subst (1) b)
   3.758 +  using z apply force
   3.759 +  apply (subst (1) a)
   3.760 +  using z apply force
   3.761 +done
   3.762 +
   3.763 +lemma int_gcd_coprime:
   3.764 +  assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   3.765 +    b: "b = b' * gcd a b"
   3.766 +  shows    "coprime a' b'"
   3.767 +
   3.768 +  apply (subgoal_tac "a' = a div gcd a b")
   3.769 +  apply (erule ssubst)
   3.770 +  apply (subgoal_tac "b' = b div gcd a b")
   3.771 +  apply (erule ssubst)
   3.772 +  apply (rule int_div_gcd_coprime)
   3.773 +  using prems
   3.774 +  apply force
   3.775 +  apply (subst (1) b)
   3.776 +  using z apply force
   3.777 +  apply (subst (1) a)
   3.778 +  using z apply force
   3.779 +done
   3.780 +
   3.781 +lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   3.782 +    shows "coprime d (a * b)"
   3.783 +  apply (subst nat_gcd_commute)
   3.784 +  using da apply (subst nat_gcd_mult_cancel)
   3.785 +  apply (subst nat_gcd_commute, assumption)
   3.786 +  apply (subst nat_gcd_commute, rule db)
   3.787 +done
   3.788 +
   3.789 +lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
   3.790 +    shows "coprime d (a * b)"
   3.791 +  apply (subst int_gcd_commute)
   3.792 +  using da apply (subst int_gcd_mult_cancel)
   3.793 +  apply (subst int_gcd_commute, assumption)
   3.794 +  apply (subst int_gcd_commute, rule db)
   3.795 +done
   3.796 +
   3.797 +lemma nat_coprime_lmult:
   3.798 +  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   3.799 +proof -
   3.800 +  have "gcd d a dvd gcd d (a * b)"
   3.801 +    by (rule nat_gcd_greatest, auto)
   3.802 +  with dab show ?thesis
   3.803 +    by auto
   3.804 +qed
   3.805 +
   3.806 +lemma int_coprime_lmult:
   3.807 +  assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
   3.808 +proof -
   3.809 +  have "gcd d a dvd gcd d (a * b)"
   3.810 +    by (rule int_gcd_greatest, auto)
   3.811 +  with dab show ?thesis
   3.812 +    by auto
   3.813 +qed
   3.814 +
   3.815 +lemma nat_coprime_rmult:
   3.816 +  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
   3.817 +proof -
   3.818 +  have "gcd d b dvd gcd d (a * b)"
   3.819 +    by (rule nat_gcd_greatest, auto intro: dvd_mult)
   3.820 +  with dab show ?thesis
   3.821 +    by auto
   3.822 +qed
   3.823 +
   3.824 +lemma int_coprime_rmult:
   3.825 +  assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   3.826 +proof -
   3.827 +  have "gcd d b dvd gcd d (a * b)"
   3.828 +    by (rule int_gcd_greatest, auto intro: dvd_mult)
   3.829 +  with dab show ?thesis
   3.830 +    by auto
   3.831 +qed
   3.832 +
   3.833 +lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
   3.834 +    coprime d a \<and>  coprime d b"
   3.835 +  using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
   3.836 +    nat_coprime_mult[of d a b]
   3.837 +  by blast
   3.838 +
   3.839 +lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
   3.840 +    coprime d a \<and>  coprime d b"
   3.841 +  using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
   3.842 +    int_coprime_mult[of d a b]
   3.843 +  by blast
   3.844 +
   3.845 +lemma nat_gcd_coprime_exists:
   3.846 +    assumes nz: "gcd (a::nat) b \<noteq> 0"
   3.847 +    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   3.848 +  apply (rule_tac x = "a div gcd a b" in exI)
   3.849 +  apply (rule_tac x = "b div gcd a b" in exI)
   3.850 +  using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
   3.851 +done
   3.852 +
   3.853 +lemma int_gcd_coprime_exists:
   3.854 +    assumes nz: "gcd (a::int) b \<noteq> 0"
   3.855 +    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   3.856 +  apply (rule_tac x = "a div gcd a b" in exI)
   3.857 +  apply (rule_tac x = "b div gcd a b" in exI)
   3.858 +  using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
   3.859 +done
   3.860 +
   3.861 +lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   3.862 +  by (induct n, simp_all add: nat_coprime_mult)
   3.863 +
   3.864 +lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   3.865 +  by (induct n, simp_all add: int_coprime_mult)
   3.866 +
   3.867 +lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   3.868 +  apply (rule nat_coprime_exp)
   3.869 +  apply (subst nat_gcd_commute)
   3.870 +  apply (rule nat_coprime_exp)
   3.871 +  apply (subst nat_gcd_commute, assumption)
   3.872 +done
   3.873 +
   3.874 +lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   3.875 +  apply (rule int_coprime_exp)
   3.876 +  apply (subst int_gcd_commute)
   3.877 +  apply (rule int_coprime_exp)
   3.878 +  apply (subst int_gcd_commute, assumption)
   3.879 +done
   3.880 +
   3.881 +lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   3.882 +proof (cases)
   3.883 +  assume "a = 0 & b = 0"
   3.884 +  thus ?thesis by simp
   3.885 +  next assume "~(a = 0 & b = 0)"
   3.886 +  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   3.887 +    by auto
   3.888 +  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   3.889 +      ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   3.890 +    apply (subst (1 2) mult_commute)
   3.891 +    apply (subst nat_gcd_mult_distrib [symmetric])
   3.892 +    apply simp
   3.893 +    done
   3.894 +  also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   3.895 +    apply (subst div_power)
   3.896 +    apply auto
   3.897 +    apply (rule dvd_div_mult_self)
   3.898 +    apply (rule dvd_power_same)
   3.899 +    apply auto
   3.900 +    done
   3.901 +  also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   3.902 +    apply (subst div_power)
   3.903 +    apply auto
   3.904 +    apply (rule dvd_div_mult_self)
   3.905 +    apply (rule dvd_power_same)
   3.906 +    apply auto
   3.907 +    done
   3.908 +  finally show ?thesis .
   3.909 +qed
   3.910 +
   3.911 +lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   3.912 +  apply (subst (1 2) int_gcd_abs)
   3.913 +  apply (subst (1 2) power_abs)
   3.914 +  apply (rule nat_gcd_exp [where n = n, transferred])
   3.915 +  apply auto
   3.916 +done
   3.917 +
   3.918 +lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   3.919 +  using nat_coprime_dvd_mult_iff[of d a b]
   3.920 +  by (auto simp add: mult_commute)
   3.921 +
   3.922 +lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   3.923 +  using int_coprime_dvd_mult_iff[of d a b]
   3.924 +  by (auto simp add: mult_commute)
   3.925 +
   3.926 +lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
   3.927 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   3.928 +proof-
   3.929 +  let ?g = "gcd a b"
   3.930 +  {assume "?g = 0" with dc have ?thesis by auto}
   3.931 +  moreover
   3.932 +  {assume z: "?g \<noteq> 0"
   3.933 +    from nat_gcd_coprime_exists[OF z]
   3.934 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   3.935 +      by blast
   3.936 +    have thb: "?g dvd b" by auto
   3.937 +    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   3.938 +    with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   3.939 +    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   3.940 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   3.941 +    with z have th_1: "a' dvd b' * c" by auto
   3.942 +    from nat_coprime_dvd_mult[OF ab'(3)] th_1
   3.943 +    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   3.944 +    from ab' have "a = ?g*a'" by algebra
   3.945 +    with thb thc have ?thesis by blast }
   3.946 +  ultimately show ?thesis by blast
   3.947 +qed
   3.948 +
   3.949 +lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
   3.950 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   3.951 +proof-
   3.952 +  let ?g = "gcd a b"
   3.953 +  {assume "?g = 0" with dc have ?thesis by auto}
   3.954 +  moreover
   3.955 +  {assume z: "?g \<noteq> 0"
   3.956 +    from int_gcd_coprime_exists[OF z]
   3.957 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   3.958 +      by blast
   3.959 +    have thb: "?g dvd b" by auto
   3.960 +    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   3.961 +    with dc have th0: "a' dvd b*c"
   3.962 +      using dvd_trans[of a' a "b*c"] by simp
   3.963 +    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   3.964 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   3.965 +    with z have th_1: "a' dvd b' * c" by auto
   3.966 +    from int_coprime_dvd_mult[OF ab'(3)] th_1
   3.967 +    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   3.968 +    from ab' have "a = ?g*a'" by algebra
   3.969 +    with thb thc have ?thesis by blast }
   3.970 +  ultimately show ?thesis by blast
   3.971  qed
   3.972  
   3.973 -lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
   3.974 -  shows "gcd x y = gcd u v"
   3.975 +lemma nat_pow_divides_pow:
   3.976 +  assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   3.977 +  shows "a dvd b"
   3.978 +proof-
   3.979 +  let ?g = "gcd a b"
   3.980 +  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   3.981 +  {assume "?g = 0" with ab n have ?thesis by auto }
   3.982 +  moreover
   3.983 +  {assume z: "?g \<noteq> 0"
   3.984 +    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   3.985 +    from nat_gcd_coprime_exists[OF z]
   3.986 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   3.987 +      by blast
   3.988 +    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   3.989 +      by (simp add: ab'(1,2)[symmetric])
   3.990 +    hence "?g^n*a'^n dvd ?g^n *b'^n"
   3.991 +      by (simp only: power_mult_distrib mult_commute)
   3.992 +    with zn z n have th0:"a'^n dvd b'^n" by auto
   3.993 +    have "a' dvd a'^n" by (simp add: m)
   3.994 +    with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   3.995 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   3.996 +    from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
   3.997 +    have "a' dvd b'" by (subst (asm) mult_commute, blast)
   3.998 +    hence "a'*?g dvd b'*?g" by simp
   3.999 +    with ab'(1,2)  have ?thesis by simp }
  3.1000 +  ultimately show ?thesis by blast
  3.1001 +qed
  3.1002 +
  3.1003 +lemma int_pow_divides_pow:
  3.1004 +  assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  3.1005 +  shows "a dvd b"
  3.1006  proof-
  3.1007 -  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
  3.1008 -  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
  3.1009 +  let ?g = "gcd a b"
  3.1010 +  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  3.1011 +  {assume "?g = 0" with ab n have ?thesis by auto }
  3.1012 +  moreover
  3.1013 +  {assume z: "?g \<noteq> 0"
  3.1014 +    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
  3.1015 +    from int_gcd_coprime_exists[OF z]
  3.1016 +    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  3.1017 +      by blast
  3.1018 +    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  3.1019 +      by (simp add: ab'(1,2)[symmetric])
  3.1020 +    hence "?g^n*a'^n dvd ?g^n *b'^n"
  3.1021 +      by (simp only: power_mult_distrib mult_commute)
  3.1022 +    with zn z n have th0:"a'^n dvd b'^n" by auto
  3.1023 +    have "a' dvd a'^n" by (simp add: m)
  3.1024 +    with th0 have "a' dvd b'^n"
  3.1025 +      using dvd_trans[of a' "a'^n" "b'^n"] by simp
  3.1026 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
  3.1027 +    from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
  3.1028 +    have "a' dvd b'" by (subst (asm) mult_commute, blast)
  3.1029 +    hence "a'*?g dvd b'*?g" by simp
  3.1030 +    with ab'(1,2)  have ?thesis by simp }
  3.1031 +  ultimately show ?thesis by blast
  3.1032 +qed
  3.1033 +
  3.1034 +lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
  3.1035 +  by (auto intro: nat_pow_divides_pow dvd_power_same)
  3.1036 +
  3.1037 +lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
  3.1038 +  by (auto intro: int_pow_divides_pow dvd_power_same)
  3.1039 +
  3.1040 +lemma nat_divides_mult:
  3.1041 +  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  3.1042 +  shows "m * n dvd r"
  3.1043 +proof-
  3.1044 +  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  3.1045 +    unfolding dvd_def by blast
  3.1046 +  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
  3.1047 +  hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
  3.1048 +  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  3.1049 +  from n' k show ?thesis unfolding dvd_def by auto
  3.1050 +qed
  3.1051 +
  3.1052 +lemma int_divides_mult:
  3.1053 +  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  3.1054 +  shows "m * n dvd r"
  3.1055 +proof-
  3.1056 +  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  3.1057 +    unfolding dvd_def by blast
  3.1058 +  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
  3.1059 +  hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
  3.1060 +  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  3.1061 +  from n' k show ?thesis unfolding dvd_def by auto
  3.1062  qed
  3.1063  
  3.1064 -lemma ind_euclid: 
  3.1065 -  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
  3.1066 -  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
  3.1067 +lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
  3.1068 +  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
  3.1069 +  apply force
  3.1070 +  apply (rule nat_dvd_diff)
  3.1071 +  apply auto
  3.1072 +done
  3.1073 +
  3.1074 +lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
  3.1075 +  using nat_coprime_plus_one by (simp add: One_nat_def)
  3.1076 +
  3.1077 +lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
  3.1078 +  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
  3.1079 +  apply force
  3.1080 +  apply (rule dvd_diff)
  3.1081 +  apply auto
  3.1082 +done
  3.1083 +
  3.1084 +lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  3.1085 +  using nat_coprime_plus_one [of "n - 1"]
  3.1086 +    nat_gcd_commute [of "n - 1" n] by auto
  3.1087 +
  3.1088 +lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
  3.1089 +  using int_coprime_plus_one [of "n - 1"]
  3.1090 +    int_gcd_commute [of "n - 1" n] by auto
  3.1091 +
  3.1092 +lemma nat_setprod_coprime [rule_format]:
  3.1093 +    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
  3.1094 +  apply (case_tac "finite A")
  3.1095 +  apply (induct set: finite)
  3.1096 +  apply (auto simp add: nat_gcd_mult_cancel)
  3.1097 +done
  3.1098 +
  3.1099 +lemma int_setprod_coprime [rule_format]:
  3.1100 +    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
  3.1101 +  apply (case_tac "finite A")
  3.1102 +  apply (induct set: finite)
  3.1103 +  apply (auto simp add: int_gcd_mult_cancel)
  3.1104 +done
  3.1105 +
  3.1106 +lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  3.1107 +  unfolding prime_nat_def
  3.1108 +  apply (subst even_mult_two_ex)
  3.1109 +  apply clarify
  3.1110 +  apply (drule_tac x = 2 in spec)
  3.1111 +  apply auto
  3.1112 +done
  3.1113 +
  3.1114 +lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  3.1115 +  unfolding prime_int_def
  3.1116 +  apply (frule nat_prime_odd)
  3.1117 +  apply (auto simp add: even_nat_def)
  3.1118 +done
  3.1119 +
  3.1120 +lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  3.1121 +    x dvd b \<Longrightarrow> x = 1"
  3.1122 +  apply (subgoal_tac "x dvd gcd a b")
  3.1123 +  apply simp
  3.1124 +  apply (erule (1) nat_gcd_greatest)
  3.1125 +done
  3.1126 +
  3.1127 +lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  3.1128 +    x dvd b \<Longrightarrow> abs x = 1"
  3.1129 +  apply (subgoal_tac "x dvd gcd a b")
  3.1130 +  apply simp
  3.1131 +  apply (erule (1) int_gcd_greatest)
  3.1132 +done
  3.1133 +
  3.1134 +lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  3.1135 +    coprime d e"
  3.1136 +  apply (auto simp add: dvd_def)
  3.1137 +  apply (frule int_coprime_lmult)
  3.1138 +  apply (subst int_gcd_commute)
  3.1139 +  apply (subst (asm) (2) int_gcd_commute)
  3.1140 +  apply (erule int_coprime_lmult)
  3.1141 +done
  3.1142 +
  3.1143 +lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  3.1144 +apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
  3.1145 +done
  3.1146 +
  3.1147 +lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  3.1148 +apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
  3.1149 +done
  3.1150 +
  3.1151 +
  3.1152 +subsection {* Bezout's theorem *}
  3.1153 +
  3.1154 +(* Function bezw returns a pair of witnesses to Bezout's theorem --
  3.1155 +   see the theorems that follow the definition. *)
  3.1156 +fun
  3.1157 +  bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  3.1158 +where
  3.1159 +  "bezw x y =
  3.1160 +  (if y = 0 then (1, 0) else
  3.1161 +      (snd (bezw y (x mod y)),
  3.1162 +       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  3.1163 +
  3.1164 +lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  3.1165 +
  3.1166 +lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  3.1167 +       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  3.1168 +  by simp
  3.1169 +
  3.1170 +declare bezw.simps [simp del]
  3.1171 +
  3.1172 +lemma bezw_aux [rule_format]:
  3.1173 +    "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  3.1174 +proof (induct x y rule: nat_gcd_induct)
  3.1175 +  fix m :: nat
  3.1176 +  show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  3.1177 +    by auto
  3.1178 +  next fix m :: nat and n
  3.1179 +    assume ngt0: "n > 0" and
  3.1180 +      ih: "fst (bezw n (m mod n)) * int n +
  3.1181 +        snd (bezw n (m mod n)) * int (m mod n) =
  3.1182 +        int (gcd n (m mod n))"
  3.1183 +    thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  3.1184 +      apply (simp add: bezw_non_0 nat_gcd_non_0)
  3.1185 +      apply (erule subst)
  3.1186 +      apply (simp add: ring_simps)
  3.1187 +      apply (subst mod_div_equality [of m n, symmetric])
  3.1188 +      (* applying simp here undoes the last substitution!
  3.1189 +         what is procedure cancel_div_mod? *)
  3.1190 +      apply (simp only: ring_simps zadd_int [symmetric]
  3.1191 +        zmult_int [symmetric])
  3.1192 +      done
  3.1193 +qed
  3.1194 +
  3.1195 +lemma int_bezout:
  3.1196 +  fixes x y
  3.1197 +  shows "EX u v. u * (x::int) + v * y = gcd x y"
  3.1198 +proof -
  3.1199 +  have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  3.1200 +      EX u v. u * x + v * y = gcd x y"
  3.1201 +    apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  3.1202 +    apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  3.1203 +    apply (unfold gcd_int_def)
  3.1204 +    apply simp
  3.1205 +    apply (subst bezw_aux [symmetric])
  3.1206 +    apply auto
  3.1207 +    done
  3.1208 +  have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  3.1209 +      (x \<le> 0 \<and> y \<le> 0)"
  3.1210 +    by auto
  3.1211 +  moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  3.1212 +    by (erule (1) bezout_aux)
  3.1213 +  moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  3.1214 +    apply (insert bezout_aux [of x "-y"])
  3.1215 +    apply auto
  3.1216 +    apply (rule_tac x = u in exI)
  3.1217 +    apply (rule_tac x = "-v" in exI)
  3.1218 +    apply (subst int_gcd_neg2 [symmetric])
  3.1219 +    apply auto
  3.1220 +    done
  3.1221 +  moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  3.1222 +    apply (insert bezout_aux [of "-x" y])
  3.1223 +    apply auto
  3.1224 +    apply (rule_tac x = "-u" in exI)
  3.1225 +    apply (rule_tac x = v in exI)
  3.1226 +    apply (subst int_gcd_neg1 [symmetric])
  3.1227 +    apply auto
  3.1228 +    done
  3.1229 +  moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  3.1230 +    apply (insert bezout_aux [of "-x" "-y"])
  3.1231 +    apply auto
  3.1232 +    apply (rule_tac x = "-u" in exI)
  3.1233 +    apply (rule_tac x = "-v" in exI)
  3.1234 +    apply (subst int_gcd_neg1 [symmetric])
  3.1235 +    apply (subst int_gcd_neg2 [symmetric])
  3.1236 +    apply auto
  3.1237 +    done
  3.1238 +  ultimately show ?thesis by blast
  3.1239 +qed
  3.1240 +
  3.1241 +text {* versions of Bezout for nat, by Amine Chaieb *}
  3.1242 +
  3.1243 +lemma ind_euclid:
  3.1244 +  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  3.1245 +  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  3.1246    shows "P a b"
  3.1247  proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  3.1248    fix n a b
  3.1249    assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  3.1250    have "a = b \<or> a < b \<or> b < a" by arith
  3.1251    moreover {assume eq: "a= b"
  3.1252 -    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
  3.1253 +    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  3.1254 +    by simp}
  3.1255    moreover
  3.1256    {assume lt: "a < b"
  3.1257      hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  3.1258 @@ -269,65 +1139,67 @@
  3.1259  ultimately  show "P a b" by blast
  3.1260  qed
  3.1261  
  3.1262 -lemma bezout_lemma: 
  3.1263 -  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
  3.1264 -  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  3.1265 -using ex
  3.1266 -apply clarsimp
  3.1267 -apply (rule_tac x="d" in exI, simp add: dvd_add)
  3.1268 -apply (case_tac "a * x = b * y + d" , simp_all)
  3.1269 -apply (rule_tac x="x + y" in exI)
  3.1270 -apply (rule_tac x="y" in exI)
  3.1271 -apply algebra
  3.1272 -apply (rule_tac x="x" in exI)
  3.1273 -apply (rule_tac x="x + y" in exI)
  3.1274 -apply algebra
  3.1275 +lemma nat_bezout_lemma:
  3.1276 +  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  3.1277 +    (a * x = b * y + d \<or> b * x = a * y + d)"
  3.1278 +  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  3.1279 +    (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  3.1280 +  using ex
  3.1281 +  apply clarsimp
  3.1282 +  apply (rule_tac x="d" in exI, simp add: dvd_add)
  3.1283 +  apply (case_tac "a * x = b * y + d" , simp_all)
  3.1284 +  apply (rule_tac x="x + y" in exI)
  3.1285 +  apply (rule_tac x="y" in exI)
  3.1286 +  apply algebra
  3.1287 +  apply (rule_tac x="x" in exI)
  3.1288 +  apply (rule_tac x="x + y" in exI)
  3.1289 +  apply algebra
  3.1290  done
  3.1291  
  3.1292 -lemma bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
  3.1293 -apply(induct a b rule: ind_euclid)
  3.1294 -apply blast
  3.1295 -apply clarify
  3.1296 -apply (rule_tac x="a" in exI, simp add: dvd_add)
  3.1297 -apply clarsimp
  3.1298 -apply (rule_tac x="d" in exI)
  3.1299 -apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  3.1300 -apply (rule_tac x="x+y" in exI)
  3.1301 -apply (rule_tac x="y" in exI)
  3.1302 -apply algebra
  3.1303 -apply (rule_tac x="x" in exI)
  3.1304 -apply (rule_tac x="x+y" in exI)
  3.1305 -apply algebra
  3.1306 +lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  3.1307 +    (a * x = b * y + d \<or> b * x = a * y + d)"
  3.1308 +  apply(induct a b rule: ind_euclid)
  3.1309 +  apply blast
  3.1310 +  apply clarify
  3.1311 +  apply (rule_tac x="a" in exI, simp add: dvd_add)
  3.1312 +  apply clarsimp
  3.1313 +  apply (rule_tac x="d" in exI)
  3.1314 +  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  3.1315 +  apply (rule_tac x="x+y" in exI)
  3.1316 +  apply (rule_tac x="y" in exI)
  3.1317 +  apply algebra
  3.1318 +  apply (rule_tac x="x" in exI)
  3.1319 +  apply (rule_tac x="x+y" in exI)
  3.1320 +  apply algebra
  3.1321  done
  3.1322  
  3.1323 -lemma bezout: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)"
  3.1324 -using bezout_add[of a b]
  3.1325 -apply clarsimp
  3.1326 -apply (rule_tac x="d" in exI, simp)
  3.1327 -apply (rule_tac x="x" in exI)
  3.1328 -apply (rule_tac x="y" in exI)
  3.1329 -apply auto
  3.1330 +lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  3.1331 +    (a * x - b * y = d \<or> b * x - a * y = d)"
  3.1332 +  using nat_bezout_add[of a b]
  3.1333 +  apply clarsimp
  3.1334 +  apply (rule_tac x="d" in exI, simp)
  3.1335 +  apply (rule_tac x="x" in exI)
  3.1336 +  apply (rule_tac x="y" in exI)
  3.1337 +  apply auto
  3.1338  done
  3.1339  
  3.1340 -
  3.1341 -text {* We can get a stronger version with a nonzeroness assumption. *}
  3.1342 -lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
  3.1343 -
  3.1344 -lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  3.1345 +lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  3.1346    shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  3.1347  proof-
  3.1348 -  from nz have ap: "a > 0" by simp
  3.1349 - from bezout_add[of a b] 
  3.1350 - have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  3.1351 + from nz have ap: "a > 0" by simp
  3.1352 + from nat_bezout_add[of a b]
  3.1353 + have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  3.1354 +   (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  3.1355   moreover
  3.1356 - {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  3.1357 -   from H have ?thesis by blast }
  3.1358 +    {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  3.1359 +     from H have ?thesis by blast }
  3.1360   moreover
  3.1361   {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  3.1362     {assume b0: "b = 0" with H  have ?thesis by simp}
  3.1363 -   moreover 
  3.1364 +   moreover
  3.1365     {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  3.1366 -     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
  3.1367 +     from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  3.1368 +       by auto
  3.1369       moreover
  3.1370       {assume db: "d=b"
  3.1371         from prems have ?thesis apply simp
  3.1372 @@ -335,18 +1207,22 @@
  3.1373  	 apply (rule exI[where x = b])
  3.1374  	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  3.1375      moreover
  3.1376 -    {assume db: "d < b" 
  3.1377 +    {assume db: "d < b"
  3.1378  	{assume "x=0" hence ?thesis  using prems by simp }
  3.1379  	moreover
  3.1380  	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  3.1381 -	  
  3.1382  	  from db have "d \<le> b - 1" by simp
  3.1383  	  hence "d*b \<le> b*(b - 1)" by simp
  3.1384  	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  3.1385  	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  3.1386 -	  from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
  3.1387 +	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  3.1388 +            by simp
  3.1389 +	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  3.1390 +	    by (simp only: mult_assoc right_distrib)
  3.1391 +	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  3.1392 +            by algebra
  3.1393  	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  3.1394 -	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
  3.1395 +	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  3.1396  	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  3.1397  	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  3.1398  	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  3.1399 @@ -361,156 +1237,156 @@
  3.1400   ultimately show ?thesis by blast
  3.1401  qed
  3.1402  
  3.1403 -
  3.1404 -lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
  3.1405 -proof-
  3.1406 -  let ?g = "gcd a b"
  3.1407 -  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
  3.1408 -  from d(1,2) have "d dvd ?g" by simp
  3.1409 -  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  3.1410 -  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
  3.1411 -  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k" 
  3.1412 -    by (algebra add: diff_mult_distrib)
  3.1413 -  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g" 
  3.1414 -    by (simp add: k mult_assoc)
  3.1415 -  thus ?thesis by blast
  3.1416 -qed
  3.1417 -
  3.1418 -lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
  3.1419 +lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
  3.1420    shows "\<exists>x y. a * x = b * y + gcd a b"
  3.1421  proof-
  3.1422    let ?g = "gcd a b"
  3.1423 -  from bezout_add_strong[OF a, of b]
  3.1424 +  from nat_bezout_add_strong[OF a, of b]
  3.1425    obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  3.1426    from d(1,2) have "d dvd ?g" by simp
  3.1427    then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  3.1428 -  from d(3) have "a * x * k = (b * y + d) *k " by algebra
  3.1429 +  from d(3) have "a * x * k = (b * y + d) *k " by auto
  3.1430    hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  3.1431    thus ?thesis by blast
  3.1432  qed
  3.1433  
  3.1434 -lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
  3.1435 -by(simp add: gcd_mult_distrib2 mult_commute)
  3.1436 +
  3.1437 +subsection {* LCM *}
  3.1438 +
  3.1439 +lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  3.1440 +  by (simp add: lcm_int_def lcm_nat_def zdiv_int
  3.1441 +    zmult_int [symmetric] gcd_int_def)
  3.1442 +
  3.1443 +lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
  3.1444 +  unfolding lcm_nat_def
  3.1445 +  by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
  3.1446 +
  3.1447 +lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
  3.1448 +  unfolding lcm_int_def gcd_int_def
  3.1449 +  apply (subst int_mult [symmetric])
  3.1450 +  apply (subst nat_prod_gcd_lcm [symmetric])
  3.1451 +  apply (subst nat_abs_mult_distrib [symmetric])
  3.1452 +  apply (simp, simp add: abs_mult)
  3.1453 +done
  3.1454 +
  3.1455 +lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
  3.1456 +  unfolding lcm_nat_def by simp
  3.1457 +
  3.1458 +lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
  3.1459 +  unfolding lcm_int_def by simp
  3.1460 +
  3.1461 +lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
  3.1462 +  unfolding lcm_nat_def by simp
  3.1463 +
  3.1464 +lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
  3.1465 +  unfolding lcm_nat_def by (simp add: One_nat_def)
  3.1466 +
  3.1467 +lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
  3.1468 +  unfolding lcm_int_def by simp
  3.1469 +
  3.1470 +lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
  3.1471 +  unfolding lcm_nat_def by simp
  3.1472  
  3.1473 -lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
  3.1474 -  (is "?lhs \<longleftrightarrow> ?rhs")
  3.1475 -proof-
  3.1476 -  let ?g = "gcd a b"
  3.1477 -  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
  3.1478 -    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
  3.1479 -      by blast
  3.1480 -    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
  3.1481 -    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
  3.1482 -      by (simp only: diff_mult_distrib)
  3.1483 -    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d"
  3.1484 -      by (simp add: k[symmetric] mult_assoc)
  3.1485 -    hence ?lhs by blast}
  3.1486 +lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
  3.1487 +  unfolding lcm_int_def by simp
  3.1488 +
  3.1489 +lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
  3.1490 +  unfolding lcm_nat_def by simp
  3.1491 +
  3.1492 +lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
  3.1493 +  unfolding lcm_nat_def by (simp add: One_nat_def)
  3.1494 +
  3.1495 +lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
  3.1496 +  unfolding lcm_int_def by simp
  3.1497 +
  3.1498 +lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
  3.1499 +  unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
  3.1500 +
  3.1501 +lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
  3.1502 +  unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
  3.1503 +
  3.1504 +(* to do: show lcm is associative, and then declare ac simps *)
  3.1505 +
  3.1506 +lemma nat_lcm_pos:
  3.1507 +  assumes mpos: "(m::nat) > 0"
  3.1508 +  and npos: "n>0"
  3.1509 +  shows "lcm m n > 0"
  3.1510 +proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
  3.1511 +  assume h:"m*n div gcd m n = 0"
  3.1512 +  from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
  3.1513 +  hence gcdp: "gcd m n > 0" by simp
  3.1514 +  with h
  3.1515 +  have "m*n < gcd m n"
  3.1516 +    by (cases "m * n < gcd m n")
  3.1517 +       (auto simp add: div_if[OF gcdp, where m="m*n"])
  3.1518    moreover
  3.1519 -  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
  3.1520 -    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
  3.1521 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
  3.1522 -    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
  3.1523 -    have ?rhs by auto}
  3.1524 -  ultimately show ?thesis by blast
  3.1525 -qed
  3.1526 -
  3.1527 -lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
  3.1528 -proof-
  3.1529 -  let ?g = "gcd a b"
  3.1530 -    have dv: "?g dvd a*x" "?g dvd b * y" 
  3.1531 -      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
  3.1532 -    from dvd_add[OF dv] H
  3.1533 -    show ?thesis by auto
  3.1534 +  have "gcd m n dvd m" by simp
  3.1535 +  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
  3.1536 +  with npos have t1:"gcd m n*n \<le> m*n" by simp
  3.1537 +  have "gcd m n \<le> gcd m n*n" using npos by simp
  3.1538 +  with t1 have "gcd m n \<le> m*n" by arith
  3.1539 +  ultimately show "False" by simp
  3.1540  qed
  3.1541  
  3.1542 -lemma gcd_mult': "gcd b (a * b) = b"
  3.1543 -by (simp add: gcd_mult mult_commute[of a b]) 
  3.1544 -
  3.1545 -lemma gcd_add: "gcd(a + b) b = gcd a b" 
  3.1546 -  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
  3.1547 -apply (simp_all add: gcd_add1)
  3.1548 -by (simp add: gcd_commute gcd_add1)
  3.1549 -
  3.1550 -lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
  3.1551 -proof-
  3.1552 -  {fix a b assume H: "b \<le> (a::nat)"
  3.1553 -    hence th: "a - b + b = a" by arith
  3.1554 -    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
  3.1555 -  note th = this
  3.1556 -{
  3.1557 -  assume ab: "b \<le> a"
  3.1558 -  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
  3.1559 -next
  3.1560 -  assume ab: "a \<le> b"
  3.1561 -  from th[OF ab] show "gcd a (b - a) = gcd a b" 
  3.1562 -    by (simp add: gcd_commute)}
  3.1563 -qed
  3.1564 -
  3.1565 +lemma int_lcm_pos:
  3.1566 +  assumes mneq0: "(m::int) ~= 0"
  3.1567 +  and npos: "n ~= 0"
  3.1568 +  shows "lcm m n > 0"
  3.1569  
  3.1570 -subsection {* LCM defined by GCD *}
  3.1571 -
  3.1572 -
  3.1573 -definition
  3.1574 -  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  3.1575 -where
  3.1576 -  lcm_def: "lcm m n = m * n div gcd m n"
  3.1577 -
  3.1578 -lemma prod_gcd_lcm:
  3.1579 -  "m * n = gcd m n * lcm m n"
  3.1580 -  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  3.1581 +  apply (subst int_lcm_abs)
  3.1582 +  apply (rule nat_lcm_pos [transferred])
  3.1583 +  using prems apply auto
  3.1584 +done
  3.1585  
  3.1586 -lemma lcm_0 [simp]: "lcm m 0 = 0"
  3.1587 -  unfolding lcm_def by simp
  3.1588 -
  3.1589 -lemma lcm_1 [simp]: "lcm m 1 = m"
  3.1590 -  unfolding lcm_def by simp
  3.1591 -
  3.1592 -lemma lcm_0_left [simp]: "lcm 0 n = 0"
  3.1593 -  unfolding lcm_def by simp
  3.1594 -
  3.1595 -lemma lcm_1_left [simp]: "lcm 1 m = m"
  3.1596 -  unfolding lcm_def by simp
  3.1597 -
  3.1598 -lemma dvd_pos:
  3.1599 +lemma nat_dvd_pos:
  3.1600    fixes n m :: nat
  3.1601    assumes "n > 0" and "m dvd n"
  3.1602    shows "m > 0"
  3.1603  using assms by (cases m) auto
  3.1604  
  3.1605 -lemma lcm_least:
  3.1606 -  assumes "m dvd k" and "n dvd k"
  3.1607 +lemma nat_lcm_least:
  3.1608 +  assumes "(m::nat) dvd k" and "n dvd k"
  3.1609    shows "lcm m n dvd k"
  3.1610  proof (cases k)
  3.1611    case 0 then show ?thesis by auto
  3.1612  next
  3.1613    case (Suc _) then have pos_k: "k > 0" by auto
  3.1614 -  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  3.1615 -  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  3.1616 +  from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  3.1617 +  with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  3.1618    from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  3.1619    from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  3.1620    from pos_k k_m have pos_p: "p > 0" by auto
  3.1621    from pos_k k_n have pos_q: "q > 0" by auto
  3.1622    have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  3.1623 -    by (simp add: mult_ac gcd_mult_distrib2)
  3.1624 +    by (simp add: mult_ac nat_gcd_mult_distrib)
  3.1625    also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  3.1626      by (simp add: k_m [symmetric] k_n [symmetric])
  3.1627    also have "\<dots> = k * p * q * gcd m n"
  3.1628 -    by (simp add: mult_ac gcd_mult_distrib2)
  3.1629 +    by (simp add: mult_ac nat_gcd_mult_distrib)
  3.1630    finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  3.1631      by (simp only: k_m [symmetric] k_n [symmetric])
  3.1632    then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  3.1633      by (simp add: mult_ac)
  3.1634    with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  3.1635      by simp
  3.1636 -  with prod_gcd_lcm [of m n]
  3.1637 +  with nat_prod_gcd_lcm [of m n]
  3.1638    have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  3.1639      by (simp add: mult_ac)
  3.1640 -  with pos_gcd have "lcm m n * gcd q p = k" by simp
  3.1641 +  with pos_gcd have "lcm m n * gcd q p = k" by auto
  3.1642    then show ?thesis using dvd_def by auto
  3.1643  qed
  3.1644  
  3.1645 -lemma lcm_dvd1 [iff]:
  3.1646 -  "m dvd lcm m n"
  3.1647 +lemma int_lcm_least:
  3.1648 +  assumes "(m::int) dvd k" and "n dvd k"
  3.1649 +  shows "lcm m n dvd k"
  3.1650 +
  3.1651 +  apply (subst int_lcm_abs)
  3.1652 +  apply (rule dvd_trans)
  3.1653 +  apply (rule nat_lcm_least [transferred, of _ "abs k" _])
  3.1654 +  using prems apply auto
  3.1655 +done
  3.1656 +
  3.1657 +lemma nat_lcm_dvd1 [iff]: "(m::nat) dvd lcm m n"
  3.1658  proof (cases m)
  3.1659    case 0 then show ?thesis by simp
  3.1660  next
  3.1661 @@ -524,264 +1400,323 @@
  3.1662      then have npos: "n > 0" by simp
  3.1663      have "gcd m n dvd n" by simp
  3.1664      then obtain k where "n = gcd m n * k" using dvd_def by auto
  3.1665 -    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
  3.1666 -    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
  3.1667 -    finally show ?thesis by (simp add: lcm_def)
  3.1668 -  qed
  3.1669 -qed
  3.1670 -
  3.1671 -lemma lcm_dvd2 [iff]: 
  3.1672 -  "n dvd lcm m n"
  3.1673 -proof (cases n)
  3.1674 -  case 0 then show ?thesis by simp
  3.1675 -next
  3.1676 -  case (Suc _)
  3.1677 -  then have npos: "n > 0" by simp
  3.1678 -  show ?thesis
  3.1679 -  proof (cases m)
  3.1680 -    case 0 then show ?thesis by simp
  3.1681 -  next
  3.1682 -    case (Suc _)
  3.1683 -    then have mpos: "m > 0" by simp
  3.1684 -    have "gcd m n dvd m" by simp
  3.1685 -    then obtain k where "m = gcd m n * k" using dvd_def by auto
  3.1686 -    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
  3.1687 -    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
  3.1688 -    finally show ?thesis by (simp add: lcm_def)
  3.1689 +    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  3.1690 +      by (simp add: mult_ac)
  3.1691 +    also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
  3.1692 +    finally show ?thesis by (simp add: lcm_nat_def)
  3.1693    qed
  3.1694  qed
  3.1695  
  3.1696 -lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
  3.1697 -  by (simp add: gcd_commute)
  3.1698 +lemma int_lcm_dvd1 [iff]: "(m::int) dvd lcm m n"
  3.1699 +  apply (subst int_lcm_abs)
  3.1700 +  apply (rule dvd_trans)
  3.1701 +  prefer 2
  3.1702 +  apply (rule nat_lcm_dvd1 [transferred])
  3.1703 +  apply auto
  3.1704 +done
  3.1705 +
  3.1706 +lemma nat_lcm_dvd2 [iff]: "(n::nat) dvd lcm m n"
  3.1707 +  by (subst nat_lcm_commute, rule nat_lcm_dvd1)
  3.1708 +
  3.1709 +lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
  3.1710 +  by (subst int_lcm_commute, rule int_lcm_dvd1)
  3.1711 +
  3.1712 +lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
  3.1713 +    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  3.1714 +  by (auto intro: dvd_anti_sym nat_lcm_least)
  3.1715  
  3.1716 -lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
  3.1717 -  apply (subgoal_tac "n = m + (n - m)")
  3.1718 -  apply (erule ssubst, rule gcd_add1_eq, simp)  
  3.1719 -  done
  3.1720 +lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  3.1721 +    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  3.1722 +  by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
  3.1723 +
  3.1724 +lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  3.1725 +  apply (rule sym)
  3.1726 +  apply (subst nat_lcm_unique [symmetric])
  3.1727 +  apply auto
  3.1728 +done
  3.1729 +
  3.1730 +lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
  3.1731 +  apply (rule sym)
  3.1732 +  apply (subst int_lcm_unique [symmetric])
  3.1733 +  apply auto
  3.1734 +done
  3.1735 +
  3.1736 +lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  3.1737 +  by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
  3.1738 +
  3.1739 +lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
  3.1740 +  by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
  3.1741 +
  3.1742  
  3.1743  
  3.1744 -subsection {* GCD and LCM on integers *}
  3.1745 -
  3.1746 -definition
  3.1747 -  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
  3.1748 -  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
  3.1749 +subsection {* Primes *}
  3.1750  
  3.1751 -lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
  3.1752 -by (simp add: zgcd_def int_dvd_iff)
  3.1753 +(* Is there a better way to handle these, rather than making them
  3.1754 +   elim rules? *)
  3.1755  
  3.1756 -lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
  3.1757 -by (simp add: zgcd_def int_dvd_iff)
  3.1758 +lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  3.1759 +  by (unfold prime_nat_def, auto)
  3.1760  
  3.1761 -lemma zgcd_pos: "zgcd i j \<ge> 0"
  3.1762 -by (simp add: zgcd_def)
  3.1763 +lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  3.1764 +  by (unfold prime_nat_def, auto)
  3.1765  
  3.1766 -lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
  3.1767 -by (simp add: zgcd_def gcd_zero)
  3.1768 +lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  3.1769 +  by (unfold prime_nat_def, auto)
  3.1770  
  3.1771 -lemma zgcd_commute: "zgcd i j = zgcd j i"
  3.1772 -unfolding zgcd_def by (simp add: gcd_commute)
  3.1773 +lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  3.1774 +  by (unfold prime_nat_def, auto)
  3.1775  
  3.1776 -lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
  3.1777 -unfolding zgcd_def by simp
  3.1778 +lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  3.1779 +  by (unfold prime_nat_def, auto)
  3.1780  
  3.1781 -lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
  3.1782 -unfolding zgcd_def by simp
  3.1783 +lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  3.1784 +  by (unfold prime_nat_def, auto)
  3.1785 +
  3.1786 +lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  3.1787 +  by (unfold prime_nat_def, auto)
  3.1788 +
  3.1789 +lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  3.1790 +  by (unfold prime_int_def prime_nat_def, auto)
  3.1791  
  3.1792 -  (* should be solved by algebra*)
  3.1793 -lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
  3.1794 -  unfolding zgcd_def
  3.1795 -proof -
  3.1796 -  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
  3.1797 -  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
  3.1798 -  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
  3.1799 -  have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
  3.1800 -    unfolding dvd_def
  3.1801 -    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
  3.1802 -  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
  3.1803 -    unfolding dvd_def by blast
  3.1804 -  from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
  3.1805 -  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
  3.1806 -  then show ?thesis
  3.1807 -    apply (subst abs_dvd_iff [symmetric])
  3.1808 -    apply (subst dvd_abs_iff [symmetric])
  3.1809 -    apply (unfold dvd_def)
  3.1810 -    apply (rule_tac x = "int h'" in exI, simp)
  3.1811 -    done
  3.1812 -qed
  3.1813 +lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  3.1814 +  by (unfold prime_int_def prime_nat_def, auto)
  3.1815 +
  3.1816 +lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  3.1817 +  by (unfold prime_int_def prime_nat_def, auto)
  3.1818  
  3.1819 -lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
  3.1820 +lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  3.1821 +  by (unfold prime_int_def prime_nat_def, auto)
  3.1822 +
  3.1823 +lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  3.1824 +  by (unfold prime_int_def prime_nat_def, auto)
  3.1825  
  3.1826 -lemma zgcd_greatest:
  3.1827 -  assumes "k dvd m" and "k dvd n"
  3.1828 -  shows "k dvd zgcd m n"
  3.1829 -proof -
  3.1830 -  let ?k' = "nat \<bar>k\<bar>"
  3.1831 -  let ?m' = "nat \<bar>m\<bar>"
  3.1832 -  let ?n' = "nat \<bar>n\<bar>"
  3.1833 -  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
  3.1834 -    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
  3.1835 -  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
  3.1836 -    unfolding zgcd_def by (simp only: zdvd_int)
  3.1837 -  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
  3.1838 -  then show "k dvd zgcd m n" by simp
  3.1839 -qed
  3.1840 +thm prime_nat_def;
  3.1841 +thm prime_nat_def [transferred];
  3.1842 +
  3.1843 +lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  3.1844 +    m = 1 \<or> m = p))"
  3.1845 +  using prime_nat_def [transferred]
  3.1846 +    apply (case_tac "p >= 0")
  3.1847 +    by (blast, auto simp add: int_prime_ge_0)
  3.1848 +
  3.1849 +(* To do: determine primality of any numeral *)
  3.1850 +
  3.1851 +lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
  3.1852 +  by (simp add: prime_nat_def)
  3.1853 +
  3.1854 +lemma int_zero_not_prime [simp]: "~prime (0::int)"
  3.1855 +  by (simp add: prime_int_def)
  3.1856 +
  3.1857 +lemma nat_one_not_prime [simp]: "~prime (1::nat)"
  3.1858 +  by (simp add: prime_nat_def)
  3.1859  
  3.1860 -lemma div_zgcd_relprime:
  3.1861 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  3.1862 -  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
  3.1863 -proof -
  3.1864 -  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
  3.1865 -  let ?g = "zgcd a b"
  3.1866 -  let ?a' = "a div ?g"
  3.1867 -  let ?b' = "b div ?g"
  3.1868 -  let ?g' = "zgcd ?a' ?b'"
  3.1869 -  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
  3.1870 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
  3.1871 -  from dvdg dvdg' obtain ka kb ka' kb' where
  3.1872 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
  3.1873 -    unfolding dvd_def by blast
  3.1874 -  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
  3.1875 -  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  3.1876 -    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
  3.1877 -      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  3.1878 -  have "?g \<noteq> 0" using nz by simp
  3.1879 -  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
  3.1880 -  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  3.1881 -  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
  3.1882 -  with zgcd_pos show "?g' = 1" by simp
  3.1883 -qed
  3.1884 +lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
  3.1885 +  by (simp add: prime_nat_def One_nat_def)
  3.1886 +
  3.1887 +lemma int_one_not_prime [simp]: "~prime (1::int)"
  3.1888 +  by (simp add: prime_int_def)
  3.1889 +
  3.1890 +lemma nat_two_is_prime [simp]: "prime (2::nat)"
  3.1891 +  apply (auto simp add: prime_nat_def)
  3.1892 +  apply (case_tac m)
  3.1893 +  apply (auto dest!: dvd_imp_le)
  3.1894 +  done
  3.1895  
  3.1896 -lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
  3.1897 -  by (simp add: zgcd_def abs_if)
  3.1898 -
  3.1899 -lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
  3.1900 -  by (simp add: zgcd_def abs_if)
  3.1901 +lemma int_two_is_prime [simp]: "prime (2::int)"
  3.1902 +  by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
  3.1903  
  3.1904 -lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
  3.1905 -  apply (frule_tac b = n and a = m in pos_mod_sign)
  3.1906 -  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
  3.1907 -  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
  3.1908 -  apply (frule_tac a = m in pos_mod_bound)
  3.1909 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
  3.1910 +lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  3.1911 +  apply (unfold prime_nat_def)
  3.1912 +  apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
  3.1913 +  done
  3.1914 +
  3.1915 +lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  3.1916 +  apply (unfold prime_int_altdef)
  3.1917 +  apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
  3.1918    done
  3.1919  
  3.1920 -lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
  3.1921 -  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
  3.1922 -  apply (auto simp add: linorder_neq_iff zgcd_non_0)
  3.1923 -  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
  3.1924 -  done
  3.1925 +lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  3.1926 +  by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
  3.1927 +
  3.1928 +lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  3.1929 +  by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
  3.1930 +
  3.1931 +lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
  3.1932 +    p dvd m * n = (p dvd m \<or> p dvd n)"
  3.1933 +  by (rule iffI, rule nat_prime_dvd_mult, auto)
  3.1934  
  3.1935 -lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
  3.1936 -  by (simp add: zgcd_def abs_if)
  3.1937 +lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
  3.1938 +    p dvd m * n = (p dvd m \<or> p dvd n)"
  3.1939 +  by (rule iffI, rule int_prime_dvd_mult, auto)
  3.1940  
  3.1941 -lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
  3.1942 -  by (simp add: zgcd_def abs_if)
  3.1943 -
  3.1944 -lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
  3.1945 -  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
  3.1946 +lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  3.1947 +    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  3.1948 +  unfolding prime_nat_def dvd_def apply auto
  3.1949 +  apply (subgoal_tac "k > 1")
  3.1950 +  apply force
  3.1951 +  apply (subgoal_tac "k ~= 0")
  3.1952 +  apply force
  3.1953 +  apply (rule notI)
  3.1954 +  apply force
  3.1955 +done
  3.1956  
  3.1957 -lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
  3.1958 -  by (simp add: zgcd_def gcd_1_left)
  3.1959 -
  3.1960 -lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
  3.1961 -  by (simp add: zgcd_def gcd_assoc)
  3.1962 +(* there's a lot of messing around with signs of products here --
  3.1963 +   could this be made more automatic? *)
  3.1964 +lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  3.1965 +    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  3.1966 +  unfolding prime_int_altdef dvd_def
  3.1967 +  apply auto
  3.1968 +  apply (rule_tac x = m in exI)
  3.1969 +  apply (rule_tac x = k in exI)
  3.1970 +  apply (auto simp add: mult_compare_simps)
  3.1971 +  apply (subgoal_tac "k > 0")
  3.1972 +  apply arith
  3.1973 +  apply (case_tac "k <= 0")
  3.1974 +  apply (subgoal_tac "m * k <= 0")
  3.1975 +  apply force
  3.1976 +  apply (subst zero_compare_simps(8))
  3.1977 +  apply auto
  3.1978 +  apply (subgoal_tac "m * k <= 0")
  3.1979 +  apply force
  3.1980 +  apply (subst zero_compare_simps(8))
  3.1981 +  apply auto
  3.1982 +done
  3.1983  
  3.1984 -lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
  3.1985 -  apply (rule zgcd_commute [THEN trans])
  3.1986 -  apply (rule zgcd_assoc [THEN trans])
  3.1987 -  apply (rule zgcd_commute [THEN arg_cong])
  3.1988 -  done
  3.1989 +lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
  3.1990 +    n > 0 --> (p dvd x^n --> p dvd x)"
  3.1991 +  by (induct n rule: nat_induct, auto)
  3.1992  
  3.1993 -lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
  3.1994 -  -- {* addition is an AC-operator *}
  3.1995 +lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
  3.1996 +    n > 0 --> (p dvd x^n --> p dvd x)"
  3.1997 +  apply (induct n rule: nat_induct, auto)
  3.1998 +  apply (frule int_prime_ge_0)
  3.1999 +  apply auto
  3.2000 +done
  3.2001 +
  3.2002 +lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  3.2003 +    coprime a (p^m)"
  3.2004 +  apply (rule nat_coprime_exp)
  3.2005 +  apply (subst nat_gcd_commute)
  3.2006 +  apply (erule (1) nat_prime_imp_coprime)
  3.2007 +done
  3.2008  
  3.2009 -lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
  3.2010 -  by (simp del: minus_mult_right [symmetric]
  3.2011 -      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
  3.2012 -          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
  3.2013 +lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  3.2014 +    coprime a (p^m)"
  3.2015 +  apply (rule int_coprime_exp)
  3.2016 +  apply (subst int_gcd_commute)
  3.2017 +  apply (erule (1) int_prime_imp_coprime)
  3.2018 +done
  3.2019  
  3.2020 -lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
  3.2021 -  by (simp add: abs_if zgcd_zmult_distrib2)
  3.2022 +lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  3.2023 +  apply (rule nat_prime_imp_coprime, assumption)
  3.2024 +  apply (unfold prime_nat_def, auto)
  3.2025 +done
  3.2026  
  3.2027 -lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
  3.2028 -  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
  3.2029 +lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  3.2030 +  apply (rule int_prime_imp_coprime, assumption)
  3.2031 +  apply (unfold prime_int_altdef, clarify)
  3.2032 +  apply (drule_tac x = q in spec)
  3.2033 +  apply (drule_tac x = p in spec)
  3.2034 +  apply auto
  3.2035 +done
  3.2036  
  3.2037 -lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
  3.2038 -  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
  3.2039 +lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  3.2040 +    coprime (p^m) (q^n)"
  3.2041 +  by (rule nat_coprime_exp2, rule nat_primes_coprime)
  3.2042  
  3.2043 -lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
  3.2044 -  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
  3.2045 +lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  3.2046 +    coprime (p^m) (q^n)"
  3.2047 +  by (rule int_coprime_exp2, rule int_primes_coprime)
  3.2048  
  3.2049 -
  3.2050 -definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
  3.2051 +lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  3.2052 +  apply (induct n rule: nat_less_induct)
  3.2053 +  apply (case_tac "n = 0")
  3.2054 +  using nat_two_is_prime apply blast
  3.2055 +  apply (case_tac "prime n")
  3.2056 +  apply blast
  3.2057 +  apply (subgoal_tac "n > 1")
  3.2058 +  apply (frule (1) nat_not_prime_eq_prod)
  3.2059 +  apply (auto intro: dvd_mult dvd_mult2)
  3.2060 +done
  3.2061  
  3.2062 -lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
  3.2063 -by(simp add:zlcm_def dvd_int_iff)
  3.2064 +(* An Isar version:
  3.2065 +
  3.2066 +lemma nat_prime_factor_b:
  3.2067 +  fixes n :: nat
  3.2068 +  assumes "n \<noteq> 1"
  3.2069 +  shows "\<exists>p. prime p \<and> p dvd n"
  3.2070  
  3.2071 -lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
  3.2072 -by(simp add:zlcm_def dvd_int_iff)
  3.2073 -
  3.2074 -
  3.2075 -lemma dvd_imp_dvd_zlcm1:
  3.2076 -  assumes "k dvd i" shows "k dvd (zlcm i j)"
  3.2077 -proof -
  3.2078 -  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
  3.2079 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  3.2080 -  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  3.2081 +using `n ~= 1`
  3.2082 +proof (induct n rule: nat_less_induct)
  3.2083 +  fix n :: nat
  3.2084 +  assume "n ~= 1" and
  3.2085 +    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  3.2086 +  thus "\<exists>p. prime p \<and> p dvd n"
  3.2087 +  proof -
  3.2088 +  {
  3.2089 +    assume "n = 0"
  3.2090 +    moreover note nat_two_is_prime
  3.2091 +    ultimately have ?thesis
  3.2092 +      by (auto simp del: nat_two_is_prime)
  3.2093 +  }
  3.2094 +  moreover
  3.2095 +  {
  3.2096 +    assume "prime n"
  3.2097 +    hence ?thesis by auto
  3.2098 +  }
  3.2099 +  moreover
  3.2100 +  {
  3.2101 +    assume "n ~= 0" and "~ prime n"
  3.2102 +    with `n ~= 1` have "n > 1" by auto
  3.2103 +    with `~ prime n` and nat_not_prime_eq_prod obtain m k where
  3.2104 +      "n = m * k" and "1 < m" and "m < n" by blast
  3.2105 +    with ih obtain p where "prime p" and "p dvd m" by blast
  3.2106 +    with `n = m * k` have ?thesis by auto
  3.2107 +  }
  3.2108 +  ultimately show ?thesis by blast
  3.2109 +  qed
  3.2110  qed
  3.2111  
  3.2112 -lemma dvd_imp_dvd_zlcm2:
  3.2113 -  assumes "k dvd j" shows "k dvd (zlcm i j)"
  3.2114 -proof -
  3.2115 -  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
  3.2116 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
  3.2117 -  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
  3.2118 +*)
  3.2119 +
  3.2120 +text {* One property of coprimality is easier to prove via prime factors. *}
  3.2121 +
  3.2122 +lemma nat_prime_divprod_pow:
  3.2123 +  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  3.2124 +  shows "p^n dvd a \<or> p^n dvd b"
  3.2125 +proof-
  3.2126 +  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  3.2127 +      apply (cases "n=0", simp_all)
  3.2128 +      apply (cases "a=1", simp_all) done}
  3.2129 +  moreover
  3.2130 +  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  3.2131 +    then obtain m where m: "n = Suc m" by (cases n, auto)
  3.2132 +    from n have "p dvd p^n" by (intro dvd_power, auto)
  3.2133 +    also note pab
  3.2134 +    finally have pab': "p dvd a * b".
  3.2135 +    from nat_prime_dvd_mult[OF p pab']
  3.2136 +    have "p dvd a \<or> p dvd b" .
  3.2137 +    moreover
  3.2138 +    {assume pa: "p dvd a"
  3.2139 +      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  3.2140 +      from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
  3.2141 +      with p have "coprime b p"
  3.2142 +        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  3.2143 +      hence pnb: "coprime (p^n) b"
  3.2144 +        by (subst nat_gcd_commute, rule nat_coprime_exp)
  3.2145 +      from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
  3.2146 +    moreover
  3.2147 +    {assume pb: "p dvd b"
  3.2148 +      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  3.2149 +      from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
  3.2150 +        by auto
  3.2151 +      with p have "coprime a p"
  3.2152 +        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  3.2153 +      hence pna: "coprime (p^n) a"
  3.2154 +        by (subst nat_gcd_commute, rule nat_coprime_exp)
  3.2155 +      from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
  3.2156 +    ultimately have ?thesis by blast}
  3.2157 +  ultimately show ?thesis by blast
  3.2158  qed
  3.2159  
  3.2160 -
  3.2161 -lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
  3.2162 -by (case_tac "d <0", simp_all)
  3.2163 -
  3.2164 -lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
  3.2165 -by (case_tac "d<0", simp_all)
  3.2166 -
  3.2167 -(* lcm a b is positive for positive a and b *)
  3.2168 -
  3.2169 -lemma lcm_pos: 
  3.2170 -  assumes mpos: "m > 0"
  3.2171 -  and npos: "n>0"
  3.2172 -  shows "lcm m n > 0"
  3.2173 -proof(rule ccontr, simp add: lcm_def gcd_zero)
  3.2174 -assume h:"m*n div gcd m n = 0"
  3.2175 -from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
  3.2176 -hence gcdp: "gcd m n > 0" by simp
  3.2177 -with h
  3.2178 -have "m*n < gcd m n"
  3.2179 -  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
  3.2180 -moreover 
  3.2181 -have "gcd m n dvd m" by simp
  3.2182 - with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
  3.2183 - with npos have t1:"gcd m n *n \<le> m*n" by simp
  3.2184 - have "gcd m n \<le> gcd m n*n" using npos by simp
  3.2185 - with t1 have "gcd m n \<le> m*n" by arith
  3.2186 -ultimately show "False" by simp
  3.2187 -qed
  3.2188 -
  3.2189 -lemma zlcm_pos: 
  3.2190 -  assumes anz: "a \<noteq> 0"
  3.2191 -  and bnz: "b \<noteq> 0" 
  3.2192 -  shows "0 < zlcm a b"
  3.2193 -proof-
  3.2194 -  let ?na = "nat (abs a)"
  3.2195 -  let ?nb = "nat (abs b)"
  3.2196 -  have nap: "?na >0" using anz by simp
  3.2197 -  have nbp: "?nb >0" using bnz by simp
  3.2198 -  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
  3.2199 -  thus ?thesis by (simp add: zlcm_def)
  3.2200 -qed
  3.2201 -
  3.2202 -lemma zgcd_code [code]:
  3.2203 -  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  3.2204 -  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
  3.2205 -
  3.2206  end
     4.1 --- a/src/HOL/IsaMakefile	Tue Jun 16 22:07:39 2009 -0700
     4.2 +++ b/src/HOL/IsaMakefile	Wed Jun 17 16:55:01 2009 -0700
     4.3 @@ -284,6 +284,7 @@
     4.4    Ln.thy \
     4.5    Log.thy \
     4.6    MacLaurin.thy \
     4.7 +  NatTransfer.thy \
     4.8    NthRoot.thy \
     4.9    SEQ.thy \
    4.10    Series.thy \
    4.11 @@ -300,6 +301,7 @@
    4.12    Real.thy \
    4.13    RealVector.thy \
    4.14    Tools/float_syntax.ML \
    4.15 +  Tools/transfer_data.ML \
    4.16    Tools/Qelim/ferrante_rackoff_data.ML \
    4.17    Tools/Qelim/ferrante_rackoff.ML \
    4.18    Tools/Qelim/langford_data.ML \
    4.19 @@ -325,6 +327,7 @@
    4.20    Library/FrechetDeriv.thy \
    4.21    Library/Fundamental_Theorem_Algebra.thy \
    4.22    Library/Inner_Product.thy Library/Lattice_Syntax.thy \
    4.23 +  Library/Legacy_GCD.thy \
    4.24    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    4.25    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
    4.26    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
     5.1 --- a/src/HOL/Library/Abstract_Rat.thy	Tue Jun 16 22:07:39 2009 -0700
     5.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jun 17 16:55:01 2009 -0700
     5.3 @@ -21,17 +21,17 @@
     5.4  definition
     5.5    isnormNum :: "Num \<Rightarrow> bool"
     5.6  where
     5.7 -  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> zgcd a b = 1))"
     5.8 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
     5.9  
    5.10  definition
    5.11    normNum :: "Num \<Rightarrow> Num"
    5.12  where
    5.13    "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    5.14 -  (let g = zgcd a b 
    5.15 +  (let g = gcd a b 
    5.16     in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    5.17  
    5.18 -declare zgcd_zdvd1[presburger] 
    5.19 -declare zgcd_zdvd2[presburger]
    5.20 +declare int_gcd_dvd1[presburger]
    5.21 +declare int_gcd_dvd2[presburger]
    5.22  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    5.23  proof -
    5.24    have " \<exists> a b. x = (a,b)" by auto
    5.25 @@ -39,19 +39,19 @@
    5.26    {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    5.27    moreover
    5.28    {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    5.29 -    let ?g = "zgcd a b"
    5.30 +    let ?g = "gcd a b"
    5.31      let ?a' = "a div ?g"
    5.32      let ?b' = "b div ?g"
    5.33 -    let ?g' = "zgcd ?a' ?b'"
    5.34 -    from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
    5.35 +    let ?g' = "gcd ?a' ?b'"
    5.36 +    from anz bnz have "?g \<noteq> 0" by simp  with int_gcd_ge_0[of a b] 
    5.37      have gpos: "?g > 0"  by arith
    5.38      have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    5.39      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    5.40      anz bnz
    5.41 -    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    5.42 -      by - (rule notI,simp add:zgcd_def)+
    5.43 +    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
    5.44 +      by - (rule notI, simp)+
    5.45      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
    5.46 -    from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
    5.47 +    from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
    5.48      from bnz have "b < 0 \<or> b > 0" by arith
    5.49      moreover
    5.50      {assume b: "b > 0"
    5.51 @@ -67,7 +67,7 @@
    5.52  	have False using b by arith }
    5.53        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    5.54        from anz bnz nz' b b' gp1 have ?thesis 
    5.55 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    5.56 +	by (simp add: isnormNum_def normNum_def Let_def split_def)}
    5.57      ultimately have ?thesis by blast
    5.58    }
    5.59    ultimately show ?thesis by blast
    5.60 @@ -85,7 +85,7 @@
    5.61  definition
    5.62    Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    5.63  where
    5.64 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b') 
    5.65 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') 
    5.66      in (a*a' div g, b*b' div g))"
    5.67  
    5.68  definition
    5.69 @@ -121,11 +121,11 @@
    5.70    then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
    5.71    {assume "a = 0"
    5.72      hence ?thesis using xn ab ab'
    5.73 -      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    5.74 +      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
    5.75    moreover
    5.76    {assume "a' = 0"
    5.77      hence ?thesis using yn ab ab' 
    5.78 -      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    5.79 +      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
    5.80    moreover
    5.81    {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
    5.82      hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
    5.83 @@ -137,11 +137,11 @@
    5.84  
    5.85  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    5.86    by (simp add: Ninv_def isnormNum_def split_def)
    5.87 -    (cases "fst x = 0", auto simp add: zgcd_commute)
    5.88 +    (cases "fst x = 0", auto simp add: int_gcd_commute)
    5.89  
    5.90  lemma isnormNum_int[simp]: 
    5.91    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    5.92 -  by (simp_all add: isnormNum_def zgcd_def)
    5.93 +  by (simp_all add: isnormNum_def)
    5.94  
    5.95  
    5.96  text {* Relations over Num *}
    5.97 @@ -202,8 +202,8 @@
    5.98      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    5.99      from prems have eq:"a * b' = a'*b" 
   5.100        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
   5.101 -    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
   5.102 -      by (simp_all add: isnormNum_def add: zgcd_commute)
   5.103 +    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
   5.104 +      by (simp_all add: isnormNum_def add: int_gcd_commute)
   5.105      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
   5.106        apply - 
   5.107        apply algebra
   5.108 @@ -211,8 +211,8 @@
   5.109        apply simp
   5.110        apply algebra
   5.111        done
   5.112 -    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   5.113 -      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   5.114 +    from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   5.115 +      int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   5.116        have eq1: "b = b'" using pos by arith  
   5.117        with eq have "a = a'" using pos by simp
   5.118        with eq1 have ?rhs by simp}
   5.119 @@ -258,7 +258,7 @@
   5.120        by (simp add: INum_def normNum_def split_def Let_def)}
   5.121    moreover 
   5.122    {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   5.123 -    let ?g = "zgcd a b"
   5.124 +    let ?g = "gcd a b"
   5.125      from a b have g: "?g \<noteq> 0"by simp
   5.126      from of_int_div[OF g, where ?'a = 'a]
   5.127      have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
   5.128 @@ -294,11 +294,11 @@
   5.129        from z aa' bb' have ?thesis 
   5.130  	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   5.131      moreover {assume z: "a * b' + b * a' \<noteq> 0"
   5.132 -      let ?g = "zgcd (a * b' + b * a') (b*b')"
   5.133 +      let ?g = "gcd (a * b' + b * a') (b*b')"
   5.134        have gz: "?g \<noteq> 0" using z by simp
   5.135        have ?thesis using aa' bb' z gz
   5.136 -	of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a * b' + b * a'" and j="b*b'"]]	of_int_div[where ?'a = 'a,
   5.137 -	OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
   5.138 +	of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
   5.139 +	OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
   5.140  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   5.141      ultimately have ?thesis using aa' bb' 
   5.142        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   5.143 @@ -317,10 +317,10 @@
   5.144        done }
   5.145    moreover
   5.146    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   5.147 -    let ?g="zgcd (a*a') (b*b')"
   5.148 +    let ?g="gcd (a*a') (b*b')"
   5.149      have gz: "?g \<noteq> 0" using z by simp
   5.150 -    from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]] 
   5.151 -      of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]] 
   5.152 +    from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]] 
   5.153 +      of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]] 
   5.154      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   5.155    ultimately show ?thesis by blast
   5.156  qed
   5.157 @@ -478,7 +478,7 @@
   5.158  qed
   5.159  
   5.160  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   5.161 -  by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
   5.162 +  by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
   5.163  
   5.164  lemma Nmul_assoc:
   5.165    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Legacy_GCD.thy	Wed Jun 17 16:55:01 2009 -0700
     6.3 @@ -0,0 +1,787 @@
     6.4 +(*  Title:      HOL/GCD.thy
     6.5 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
     6.6 +    Copyright   1996  University of Cambridge
     6.7 +*)
     6.8 +
     6.9 +header {* The Greatest Common Divisor *}
    6.10 +
    6.11 +theory Legacy_GCD
    6.12 +imports Main
    6.13 +begin
    6.14 +
    6.15 +text {*
    6.16 +  See \cite{davenport92}. \bigskip
    6.17 +*}
    6.18 +
    6.19 +subsection {* Specification of GCD on nats *}
    6.20 +
    6.21 +definition
    6.22 +  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    6.23 +  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    6.24 +    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    6.25 +
    6.26 +text {* Uniqueness *}
    6.27 +
    6.28 +lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
    6.29 +  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
    6.30 +
    6.31 +text {* Connection to divides relation *}
    6.32 +
    6.33 +lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
    6.34 +  by (auto simp add: is_gcd_def)
    6.35 +
    6.36 +text {* Commutativity *}
    6.37 +
    6.38 +lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
    6.39 +  by (auto simp add: is_gcd_def)
    6.40 +
    6.41 +
    6.42 +subsection {* GCD on nat by Euclid's algorithm *}
    6.43 +
    6.44 +fun
    6.45 +  gcd  :: "nat => nat => nat"
    6.46 +where
    6.47 +  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
    6.48 +lemma gcd_induct [case_names "0" rec]:
    6.49 +  fixes m n :: nat
    6.50 +  assumes "\<And>m. P m 0"
    6.51 +    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
    6.52 +  shows "P m n"
    6.53 +proof (induct m n rule: gcd.induct)
    6.54 +  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
    6.55 +qed
    6.56 +
    6.57 +lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
    6.58 +  by simp
    6.59 +
    6.60 +lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
    6.61 +  by simp
    6.62 +
    6.63 +lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
    6.64 +  by simp
    6.65 +
    6.66 +lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
    6.67 +  by simp
    6.68 +
    6.69 +lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
    6.70 +  unfolding One_nat_def by (rule gcd_1)
    6.71 +
    6.72 +declare gcd.simps [simp del]
    6.73 +
    6.74 +text {*
    6.75 +  \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
    6.76 +  conjunctions don't seem provable separately.
    6.77 +*}
    6.78 +
    6.79 +lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
    6.80 +  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
    6.81 +  apply (induct m n rule: gcd_induct)
    6.82 +     apply (simp_all add: gcd_non_0)
    6.83 +  apply (blast dest: dvd_mod_imp_dvd)
    6.84 +  done
    6.85 +
    6.86 +text {*
    6.87 +  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    6.88 +  naturals, if @{term k} divides @{term m} and @{term k} divides
    6.89 +  @{term n} then @{term k} divides @{term "gcd m n"}.
    6.90 +*}
    6.91 +
    6.92 +lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    6.93 +  by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
    6.94 +
    6.95 +text {*
    6.96 +  \medskip Function gcd yields the Greatest Common Divisor.
    6.97 +*}
    6.98 +
    6.99 +lemma is_gcd: "is_gcd m n (gcd m n) "
   6.100 +  by (simp add: is_gcd_def gcd_greatest)
   6.101 +
   6.102 +
   6.103 +subsection {* Derived laws for GCD *}
   6.104 +
   6.105 +lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
   6.106 +  by (blast intro!: gcd_greatest intro: dvd_trans)
   6.107 +
   6.108 +lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   6.109 +  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   6.110 +
   6.111 +lemma gcd_commute: "gcd m n = gcd n m"
   6.112 +  apply (rule is_gcd_unique)
   6.113 +   apply (rule is_gcd)
   6.114 +  apply (subst is_gcd_commute)
   6.115 +  apply (simp add: is_gcd)
   6.116 +  done
   6.117 +
   6.118 +lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
   6.119 +  apply (rule is_gcd_unique)
   6.120 +   apply (rule is_gcd)
   6.121 +  apply (simp add: is_gcd_def)
   6.122 +  apply (blast intro: dvd_trans)
   6.123 +  done
   6.124 +
   6.125 +lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
   6.126 +  by (simp add: gcd_commute)
   6.127 +
   6.128 +lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
   6.129 +  unfolding One_nat_def by (rule gcd_1_left)
   6.130 +
   6.131 +text {*
   6.132 +  \medskip Multiplication laws
   6.133 +*}
   6.134 +
   6.135 +lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
   6.136 +    -- {* \cite[page 27]{davenport92} *}
   6.137 +  apply (induct m n rule: gcd_induct)
   6.138 +   apply simp
   6.139 +  apply (case_tac "k = 0")
   6.140 +   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   6.141 +  done
   6.142 +
   6.143 +lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
   6.144 +  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   6.145 +  done
   6.146 +
   6.147 +lemma gcd_self [simp, algebra]: "gcd k k = k"
   6.148 +  apply (rule gcd_mult [of k 1, simplified])
   6.149 +  done
   6.150 +
   6.151 +lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
   6.152 +  apply (insert gcd_mult_distrib2 [of m k n])
   6.153 +  apply simp
   6.154 +  apply (erule_tac t = m in ssubst)
   6.155 +  apply simp
   6.156 +  done
   6.157 +
   6.158 +lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
   6.159 +  by (auto intro: relprime_dvd_mult dvd_mult2)
   6.160 +
   6.161 +lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   6.162 +  apply (rule dvd_anti_sym)
   6.163 +   apply (rule gcd_greatest)
   6.164 +    apply (rule_tac n = k in relprime_dvd_mult)
   6.165 +     apply (simp add: gcd_assoc)
   6.166 +     apply (simp add: gcd_commute)
   6.167 +    apply (simp_all add: mult_commute)
   6.168 +  done
   6.169 +
   6.170 +
   6.171 +text {* \medskip Addition laws *}
   6.172 +
   6.173 +lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
   6.174 +  by (cases "n = 0") (auto simp add: gcd_non_0)
   6.175 +
   6.176 +lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
   6.177 +proof -
   6.178 +  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
   6.179 +  also have "... = gcd (n + m) m" by (simp add: add_commute)
   6.180 +  also have "... = gcd n m" by simp
   6.181 +  also have  "... = gcd m n" by (rule gcd_commute)
   6.182 +  finally show ?thesis .
   6.183 +qed
   6.184 +
   6.185 +lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
   6.186 +  apply (subst add_commute)
   6.187 +  apply (rule gcd_add2)
   6.188 +  done
   6.189 +
   6.190 +lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
   6.191 +  by (induct k) (simp_all add: add_assoc)
   6.192 +
   6.193 +lemma gcd_dvd_prod: "gcd m n dvd m * n" 
   6.194 +  using mult_dvd_mono [of 1] by auto
   6.195 +
   6.196 +text {*
   6.197 +  \medskip Division by gcd yields rrelatively primes.
   6.198 +*}
   6.199 +
   6.200 +lemma div_gcd_relprime:
   6.201 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   6.202 +  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
   6.203 +proof -
   6.204 +  let ?g = "gcd a b"
   6.205 +  let ?a' = "a div ?g"
   6.206 +  let ?b' = "b div ?g"
   6.207 +  let ?g' = "gcd ?a' ?b'"
   6.208 +  have dvdg: "?g dvd a" "?g dvd b" by simp_all
   6.209 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   6.210 +  from dvdg dvdg' obtain ka kb ka' kb' where
   6.211 +      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   6.212 +    unfolding dvd_def by blast
   6.213 +  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
   6.214 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   6.215 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   6.216 +      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   6.217 +  have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
   6.218 +  then have gp: "?g > 0" by simp
   6.219 +  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   6.220 +  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   6.221 +qed
   6.222 +
   6.223 +
   6.224 +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"
   6.225 +proof(auto)
   6.226 +  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   6.227 +  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   6.228 +  have th: "gcd a b dvd d" by blast
   6.229 +  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   6.230 +qed
   6.231 +
   6.232 +lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
   6.233 +  shows "gcd x y = gcd u v"
   6.234 +proof-
   6.235 +  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
   6.236 +  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
   6.237 +qed
   6.238 +
   6.239 +lemma ind_euclid: 
   6.240 +  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
   6.241 +  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
   6.242 +  shows "P a b"
   6.243 +proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
   6.244 +  fix n a b
   6.245 +  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
   6.246 +  have "a = b \<or> a < b \<or> b < a" by arith
   6.247 +  moreover {assume eq: "a= b"
   6.248 +    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
   6.249 +  moreover
   6.250 +  {assume lt: "a < b"
   6.251 +    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
   6.252 +    moreover
   6.253 +    {assume "a =0" with z c have "P a b" by blast }
   6.254 +    moreover
   6.255 +    {assume ab: "a + b - a < n"
   6.256 +      have th0: "a + b - a = a + (b - a)" using lt by arith
   6.257 +      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   6.258 +      have "P a b" by (simp add: th0[symmetric])}
   6.259 +    ultimately have "P a b" by blast}
   6.260 +  moreover
   6.261 +  {assume lt: "a > b"
   6.262 +    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
   6.263 +    moreover
   6.264 +    {assume "b =0" with z c have "P a b" by blast }
   6.265 +    moreover
   6.266 +    {assume ab: "b + a - b < n"
   6.267 +      have th0: "b + a - b = b + (a - b)" using lt by arith
   6.268 +      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   6.269 +      have "P b a" by (simp add: th0[symmetric])
   6.270 +      hence "P a b" using c by blast }
   6.271 +    ultimately have "P a b" by blast}
   6.272 +ultimately  show "P a b" by blast
   6.273 +qed
   6.274 +
   6.275 +lemma bezout_lemma: 
   6.276 +  assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
   6.277 +  shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
   6.278 +using ex
   6.279 +apply clarsimp
   6.280 +apply (rule_tac x="d" in exI, simp add: dvd_add)
   6.281 +apply (case_tac "a * x = b * y + d" , simp_all)
   6.282 +apply (rule_tac x="x + y" in exI)
   6.283 +apply (rule_tac x="y" in exI)
   6.284 +apply algebra
   6.285 +apply (rule_tac x="x" in exI)
   6.286 +apply (rule_tac x="x + y" in exI)
   6.287 +apply algebra
   6.288 +done
   6.289 +
   6.290 +lemma bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
   6.291 +apply(induct a b rule: ind_euclid)
   6.292 +apply blast
   6.293 +apply clarify
   6.294 +apply (rule_tac x="a" in exI, simp add: dvd_add)
   6.295 +apply clarsimp
   6.296 +apply (rule_tac x="d" in exI)
   6.297 +apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
   6.298 +apply (rule_tac x="x+y" in exI)
   6.299 +apply (rule_tac x="y" in exI)
   6.300 +apply algebra
   6.301 +apply (rule_tac x="x" in exI)
   6.302 +apply (rule_tac x="x+y" in exI)
   6.303 +apply algebra
   6.304 +done
   6.305 +
   6.306 +lemma bezout: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)"
   6.307 +using bezout_add[of a b]
   6.308 +apply clarsimp
   6.309 +apply (rule_tac x="d" in exI, simp)
   6.310 +apply (rule_tac x="x" in exI)
   6.311 +apply (rule_tac x="y" in exI)
   6.312 +apply auto
   6.313 +done
   6.314 +
   6.315 +
   6.316 +text {* We can get a stronger version with a nonzeroness assumption. *}
   6.317 +lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
   6.318 +
   6.319 +lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
   6.320 +  shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
   6.321 +proof-
   6.322 +  from nz have ap: "a > 0" by simp
   6.323 + from bezout_add[of a b] 
   6.324 + have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
   6.325 + moreover
   6.326 + {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
   6.327 +   from H have ?thesis by blast }
   6.328 + moreover
   6.329 + {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
   6.330 +   {assume b0: "b = 0" with H  have ?thesis by simp}
   6.331 +   moreover 
   6.332 +   {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
   6.333 +     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
   6.334 +     moreover
   6.335 +     {assume db: "d=b"
   6.336 +       from prems have ?thesis apply simp
   6.337 +	 apply (rule exI[where x = b], simp)
   6.338 +	 apply (rule exI[where x = b])
   6.339 +	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
   6.340 +    moreover
   6.341 +    {assume db: "d < b" 
   6.342 +	{assume "x=0" hence ?thesis  using prems by simp }
   6.343 +	moreover
   6.344 +	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
   6.345 +	  
   6.346 +	  from db have "d \<le> b - 1" by simp
   6.347 +	  hence "d*b \<le> b*(b - 1)" by simp
   6.348 +	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
   6.349 +	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
   6.350 +	  from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
   6.351 +	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
   6.352 +	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
   6.353 +	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
   6.354 +	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
   6.355 +	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
   6.356 +	  hence ?thesis using H(1,2)
   6.357 +	    apply -
   6.358 +	    apply (rule exI[where x=d], simp)
   6.359 +	    apply (rule exI[where x="(b - 1) * y"])
   6.360 +	    by (rule exI[where x="x*(b - 1) - d"], simp)}
   6.361 +	ultimately have ?thesis by blast}
   6.362 +    ultimately have ?thesis by blast}
   6.363 +  ultimately have ?thesis by blast}
   6.364 + ultimately show ?thesis by blast
   6.365 +qed
   6.366 +
   6.367 +
   6.368 +lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   6.369 +proof-
   6.370 +  let ?g = "gcd a b"
   6.371 +  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
   6.372 +  from d(1,2) have "d dvd ?g" by simp
   6.373 +  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   6.374 +  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
   6.375 +  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k" 
   6.376 +    by (algebra add: diff_mult_distrib)
   6.377 +  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g" 
   6.378 +    by (simp add: k mult_assoc)
   6.379 +  thus ?thesis by blast
   6.380 +qed
   6.381 +
   6.382 +lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
   6.383 +  shows "\<exists>x y. a * x = b * y + gcd a b"
   6.384 +proof-
   6.385 +  let ?g = "gcd a b"
   6.386 +  from bezout_add_strong[OF a, of b]
   6.387 +  obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
   6.388 +  from d(1,2) have "d dvd ?g" by simp
   6.389 +  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   6.390 +  from d(3) have "a * x * k = (b * y + d) *k " by algebra
   6.391 +  hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
   6.392 +  thus ?thesis by blast
   6.393 +qed
   6.394 +
   6.395 +lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
   6.396 +by(simp add: gcd_mult_distrib2 mult_commute)
   6.397 +
   6.398 +lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
   6.399 +  (is "?lhs \<longleftrightarrow> ?rhs")
   6.400 +proof-
   6.401 +  let ?g = "gcd a b"
   6.402 +  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
   6.403 +    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
   6.404 +      by blast
   6.405 +    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
   6.406 +    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
   6.407 +      by (simp only: diff_mult_distrib)
   6.408 +    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d"
   6.409 +      by (simp add: k[symmetric] mult_assoc)
   6.410 +    hence ?lhs by blast}
   6.411 +  moreover
   6.412 +  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
   6.413 +    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
   6.414 +      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
   6.415 +    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
   6.416 +    have ?rhs by auto}
   6.417 +  ultimately show ?thesis by blast
   6.418 +qed
   6.419 +
   6.420 +lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
   6.421 +proof-
   6.422 +  let ?g = "gcd a b"
   6.423 +    have dv: "?g dvd a*x" "?g dvd b * y" 
   6.424 +      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
   6.425 +    from dvd_add[OF dv] H
   6.426 +    show ?thesis by auto
   6.427 +qed
   6.428 +
   6.429 +lemma gcd_mult': "gcd b (a * b) = b"
   6.430 +by (simp add: gcd_mult mult_commute[of a b]) 
   6.431 +
   6.432 +lemma gcd_add: "gcd(a + b) b = gcd a b" 
   6.433 +  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
   6.434 +apply (simp_all add: gcd_add1)
   6.435 +by (simp add: gcd_commute gcd_add1)
   6.436 +
   6.437 +lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
   6.438 +proof-
   6.439 +  {fix a b assume H: "b \<le> (a::nat)"
   6.440 +    hence th: "a - b + b = a" by arith
   6.441 +    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
   6.442 +  note th = this
   6.443 +{
   6.444 +  assume ab: "b \<le> a"
   6.445 +  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
   6.446 +next
   6.447 +  assume ab: "a \<le> b"
   6.448 +  from th[OF ab] show "gcd a (b - a) = gcd a b" 
   6.449 +    by (simp add: gcd_commute)}
   6.450 +qed
   6.451 +
   6.452 +
   6.453 +subsection {* LCM defined by GCD *}
   6.454 +
   6.455 +
   6.456 +definition
   6.457 +  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   6.458 +where
   6.459 +  lcm_def: "lcm m n = m * n div gcd m n"
   6.460 +
   6.461 +lemma prod_gcd_lcm:
   6.462 +  "m * n = gcd m n * lcm m n"
   6.463 +  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
   6.464 +
   6.465 +lemma lcm_0 [simp]: "lcm m 0 = 0"
   6.466 +  unfolding lcm_def by simp
   6.467 +
   6.468 +lemma lcm_1 [simp]: "lcm m 1 = m"
   6.469 +  unfolding lcm_def by simp
   6.470 +
   6.471 +lemma lcm_0_left [simp]: "lcm 0 n = 0"
   6.472 +  unfolding lcm_def by simp
   6.473 +
   6.474 +lemma lcm_1_left [simp]: "lcm 1 m = m"
   6.475 +  unfolding lcm_def by simp
   6.476 +
   6.477 +lemma dvd_pos:
   6.478 +  fixes n m :: nat
   6.479 +  assumes "n > 0" and "m dvd n"
   6.480 +  shows "m > 0"
   6.481 +using assms by (cases m) auto
   6.482 +
   6.483 +lemma lcm_least:
   6.484 +  assumes "m dvd k" and "n dvd k"
   6.485 +  shows "lcm m n dvd k"
   6.486 +proof (cases k)
   6.487 +  case 0 then show ?thesis by auto
   6.488 +next
   6.489 +  case (Suc _) then have pos_k: "k > 0" by auto
   6.490 +  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
   6.491 +  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
   6.492 +  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   6.493 +  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   6.494 +  from pos_k k_m have pos_p: "p > 0" by auto
   6.495 +  from pos_k k_n have pos_q: "q > 0" by auto
   6.496 +  have "k * k * gcd q p = k * gcd (k * q) (k * p)"
   6.497 +    by (simp add: mult_ac gcd_mult_distrib2)
   6.498 +  also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
   6.499 +    by (simp add: k_m [symmetric] k_n [symmetric])
   6.500 +  also have "\<dots> = k * p * q * gcd m n"
   6.501 +    by (simp add: mult_ac gcd_mult_distrib2)
   6.502 +  finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
   6.503 +    by (simp only: k_m [symmetric] k_n [symmetric])
   6.504 +  then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
   6.505 +    by (simp add: mult_ac)
   6.506 +  with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
   6.507 +    by simp
   6.508 +  with prod_gcd_lcm [of m n]
   6.509 +  have "lcm m n * gcd q p * gcd m n = k * gcd m n"
   6.510 +    by (simp add: mult_ac)
   6.511 +  with pos_gcd have "lcm m n * gcd q p = k" by simp
   6.512 +  then show ?thesis using dvd_def by auto
   6.513 +qed
   6.514 +
   6.515 +lemma lcm_dvd1 [iff]:
   6.516 +  "m dvd lcm m n"
   6.517 +proof (cases m)
   6.518 +  case 0 then show ?thesis by simp
   6.519 +next
   6.520 +  case (Suc _)
   6.521 +  then have mpos: "m > 0" by simp
   6.522 +  show ?thesis
   6.523 +  proof (cases n)
   6.524 +    case 0 then show ?thesis by simp
   6.525 +  next
   6.526 +    case (Suc _)
   6.527 +    then have npos: "n > 0" by simp
   6.528 +    have "gcd m n dvd n" by simp
   6.529 +    then obtain k where "n = gcd m n * k" using dvd_def by auto
   6.530 +    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
   6.531 +    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
   6.532 +    finally show ?thesis by (simp add: lcm_def)
   6.533 +  qed
   6.534 +qed
   6.535 +
   6.536 +lemma lcm_dvd2 [iff]: 
   6.537 +  "n dvd lcm m n"
   6.538 +proof (cases n)
   6.539 +  case 0 then show ?thesis by simp
   6.540 +next
   6.541 +  case (Suc _)
   6.542 +  then have npos: "n > 0" by simp
   6.543 +  show ?thesis
   6.544 +  proof (cases m)
   6.545 +    case 0 then show ?thesis by simp
   6.546 +  next
   6.547 +    case (Suc _)
   6.548 +    then have mpos: "m > 0" by simp
   6.549 +    have "gcd m n dvd m" by simp
   6.550 +    then obtain k where "m = gcd m n * k" using dvd_def by auto
   6.551 +    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
   6.552 +    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
   6.553 +    finally show ?thesis by (simp add: lcm_def)
   6.554 +  qed
   6.555 +qed
   6.556 +
   6.557 +lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
   6.558 +  by (simp add: gcd_commute)
   6.559 +
   6.560 +lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
   6.561 +  apply (subgoal_tac "n = m + (n - m)")
   6.562 +  apply (erule ssubst, rule gcd_add1_eq, simp)  
   6.563 +  done
   6.564 +
   6.565 +
   6.566 +subsection {* GCD and LCM on integers *}
   6.567 +
   6.568 +definition
   6.569 +  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   6.570 +  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
   6.571 +
   6.572 +lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
   6.573 +by (simp add: zgcd_def int_dvd_iff)
   6.574 +
   6.575 +lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
   6.576 +by (simp add: zgcd_def int_dvd_iff)
   6.577 +
   6.578 +lemma zgcd_pos: "zgcd i j \<ge> 0"
   6.579 +by (simp add: zgcd_def)
   6.580 +
   6.581 +lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
   6.582 +by (simp add: zgcd_def gcd_zero)
   6.583 +
   6.584 +lemma zgcd_commute: "zgcd i j = zgcd j i"
   6.585 +unfolding zgcd_def by (simp add: gcd_commute)
   6.586 +
   6.587 +lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
   6.588 +unfolding zgcd_def by simp
   6.589 +
   6.590 +lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
   6.591 +unfolding zgcd_def by simp
   6.592 +
   6.593 +  (* should be solved by algebra*)
   6.594 +lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   6.595 +  unfolding zgcd_def
   6.596 +proof -
   6.597 +  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   6.598 +  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
   6.599 +  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
   6.600 +  have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
   6.601 +    unfolding dvd_def
   6.602 +    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
   6.603 +  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
   6.604 +    unfolding dvd_def by blast
   6.605 +  from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
   6.606 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   6.607 +  then show ?thesis
   6.608 +    apply (subst abs_dvd_iff [symmetric])
   6.609 +    apply (subst dvd_abs_iff [symmetric])
   6.610 +    apply (unfold dvd_def)
   6.611 +    apply (rule_tac x = "int h'" in exI, simp)
   6.612 +    done
   6.613 +qed
   6.614 +
   6.615 +lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
   6.616 +
   6.617 +lemma zgcd_greatest:
   6.618 +  assumes "k dvd m" and "k dvd n"
   6.619 +  shows "k dvd zgcd m n"
   6.620 +proof -
   6.621 +  let ?k' = "nat \<bar>k\<bar>"
   6.622 +  let ?m' = "nat \<bar>m\<bar>"
   6.623 +  let ?n' = "nat \<bar>n\<bar>"
   6.624 +  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
   6.625 +    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
   6.626 +  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
   6.627 +    unfolding zgcd_def by (simp only: zdvd_int)
   6.628 +  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
   6.629 +  then show "k dvd zgcd m n" by simp
   6.630 +qed
   6.631 +
   6.632 +lemma div_zgcd_relprime:
   6.633 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   6.634 +  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
   6.635 +proof -
   6.636 +  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
   6.637 +  let ?g = "zgcd a b"
   6.638 +  let ?a' = "a div ?g"
   6.639 +  let ?b' = "b div ?g"
   6.640 +  let ?g' = "zgcd ?a' ?b'"
   6.641 +  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
   6.642 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
   6.643 +  from dvdg dvdg' obtain ka kb ka' kb' where
   6.644 +   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
   6.645 +    unfolding dvd_def by blast
   6.646 +  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   6.647 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   6.648 +    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
   6.649 +      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   6.650 +  have "?g \<noteq> 0" using nz by simp
   6.651 +  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
   6.652 +  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   6.653 +  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
   6.654 +  with zgcd_pos show "?g' = 1" by simp
   6.655 +qed
   6.656 +
   6.657 +lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
   6.658 +  by (simp add: zgcd_def abs_if)
   6.659 +
   6.660 +lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
   6.661 +  by (simp add: zgcd_def abs_if)
   6.662 +
   6.663 +lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
   6.664 +  apply (frule_tac b = n and a = m in pos_mod_sign)
   6.665 +  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
   6.666 +  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   6.667 +  apply (frule_tac a = m in pos_mod_bound)
   6.668 +  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
   6.669 +  done
   6.670 +
   6.671 +lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
   6.672 +  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
   6.673 +  apply (auto simp add: linorder_neq_iff zgcd_non_0)
   6.674 +  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
   6.675 +  done
   6.676 +
   6.677 +lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
   6.678 +  by (simp add: zgcd_def abs_if)
   6.679 +
   6.680 +lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
   6.681 +  by (simp add: zgcd_def abs_if)
   6.682 +
   6.683 +lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
   6.684 +  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
   6.685 +
   6.686 +lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
   6.687 +  by (simp add: zgcd_def gcd_1_left)
   6.688 +
   6.689 +lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
   6.690 +  by (simp add: zgcd_def gcd_assoc)
   6.691 +
   6.692 +lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
   6.693 +  apply (rule zgcd_commute [THEN trans])
   6.694 +  apply (rule zgcd_assoc [THEN trans])
   6.695 +  apply (rule zgcd_commute [THEN arg_cong])
   6.696 +  done
   6.697 +
   6.698 +lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
   6.699 +  -- {* addition is an AC-operator *}
   6.700 +
   6.701 +lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
   6.702 +  by (simp del: minus_mult_right [symmetric]
   6.703 +      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
   6.704 +          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   6.705 +
   6.706 +lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
   6.707 +  by (simp add: abs_if zgcd_zmult_distrib2)
   6.708 +
   6.709 +lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
   6.710 +  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
   6.711 +
   6.712 +lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
   6.713 +  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
   6.714 +
   6.715 +lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
   6.716 +  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
   6.717 +
   6.718 +
   6.719 +definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
   6.720 +
   6.721 +lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
   6.722 +by(simp add:zlcm_def dvd_int_iff)
   6.723 +
   6.724 +lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
   6.725 +by(simp add:zlcm_def dvd_int_iff)
   6.726 +
   6.727 +
   6.728 +lemma dvd_imp_dvd_zlcm1:
   6.729 +  assumes "k dvd i" shows "k dvd (zlcm i j)"
   6.730 +proof -
   6.731 +  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
   6.732 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   6.733 +  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   6.734 +qed
   6.735 +
   6.736 +lemma dvd_imp_dvd_zlcm2:
   6.737 +  assumes "k dvd j" shows "k dvd (zlcm i j)"
   6.738 +proof -
   6.739 +  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
   6.740 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   6.741 +  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   6.742 +qed
   6.743 +
   6.744 +
   6.745 +lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
   6.746 +by (case_tac "d <0", simp_all)
   6.747 +
   6.748 +lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
   6.749 +by (case_tac "d<0", simp_all)
   6.750 +
   6.751 +(* lcm a b is positive for positive a and b *)
   6.752 +
   6.753 +lemma lcm_pos: 
   6.754 +  assumes mpos: "m > 0"
   6.755 +  and npos: "n>0"
   6.756 +  shows "lcm m n > 0"
   6.757 +proof(rule ccontr, simp add: lcm_def gcd_zero)
   6.758 +assume h:"m*n div gcd m n = 0"
   6.759 +from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
   6.760 +hence gcdp: "gcd m n > 0" by simp
   6.761 +with h
   6.762 +have "m*n < gcd m n"
   6.763 +  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
   6.764 +moreover 
   6.765 +have "gcd m n dvd m" by simp
   6.766 + with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
   6.767 + with npos have t1:"gcd m n *n \<le> m*n" by simp
   6.768 + have "gcd m n \<le> gcd m n*n" using npos by simp
   6.769 + with t1 have "gcd m n \<le> m*n" by arith
   6.770 +ultimately show "False" by simp
   6.771 +qed
   6.772 +
   6.773 +lemma zlcm_pos: 
   6.774 +  assumes anz: "a \<noteq> 0"
   6.775 +  and bnz: "b \<noteq> 0" 
   6.776 +  shows "0 < zlcm a b"
   6.777 +proof-
   6.778 +  let ?na = "nat (abs a)"
   6.779 +  let ?nb = "nat (abs b)"
   6.780 +  have nap: "?na >0" using anz by simp
   6.781 +  have nbp: "?nb >0" using bnz by simp
   6.782 +  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
   6.783 +  thus ?thesis by (simp add: zlcm_def)
   6.784 +qed
   6.785 +
   6.786 +lemma zgcd_code [code]:
   6.787 +  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   6.788 +  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
   6.789 +
   6.790 +end
     7.1 --- a/src/HOL/Library/Primes.thy	Tue Jun 16 22:07:39 2009 -0700
     7.2 +++ b/src/HOL/Library/Primes.thy	Wed Jun 17 16:55:01 2009 -0700
     7.3 @@ -6,9 +6,11 @@
     7.4  header {* Primality on nat *}
     7.5  
     7.6  theory Primes
     7.7 -imports Complex_Main
     7.8 +imports Complex_Main Legacy_GCD
     7.9  begin
    7.10  
    7.11 +hide (open) const GCD.gcd GCD.coprime GCD.prime
    7.12 +
    7.13  definition
    7.14    coprime :: "nat => nat => bool" where
    7.15    "coprime m n \<longleftrightarrow> gcd m n = 1"
     8.1 --- a/src/HOL/Rational.thy	Tue Jun 16 22:07:39 2009 -0700
     8.2 +++ b/src/HOL/Rational.thy	Wed Jun 17 16:55:01 2009 -0700
     8.3 @@ -851,11 +851,11 @@
     8.4  
     8.5  subsection {* Implementation of rational numbers as pairs of integers *}
     8.6  
     8.7 -lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"
     8.8 +lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
     8.9  proof (cases "a = 0 \<or> b = 0")
    8.10    case True then show ?thesis by (auto simp add: eq_rat)
    8.11  next
    8.12 -  let ?c = "zgcd a b"
    8.13 +  let ?c = "gcd a b"
    8.14    case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    8.15    then have "?c \<noteq> 0" by simp
    8.16    then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
    8.17 @@ -870,7 +870,7 @@
    8.18  definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
    8.19    [simp, code del]: "Fract_norm a b = Fract a b"
    8.20  
    8.21 -lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
    8.22 +lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = gcd a b in
    8.23    if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
    8.24    by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
    8.25  
     9.1 --- a/src/HOL/RealDef.thy	Tue Jun 16 22:07:39 2009 -0700
     9.2 +++ b/src/HOL/RealDef.thy	Wed Jun 17 16:55:01 2009 -0700
     9.3 @@ -895,14 +895,15 @@
     9.4  
     9.5  lemma Rats_abs_nat_div_natE:
     9.6    assumes "x \<in> \<rat>"
     9.7 -  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
     9.8 +  obtains m n :: nat
     9.9 +  where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
    9.10  proof -
    9.11    from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
    9.12      by(auto simp add: Rats_eq_int_div_nat)
    9.13    hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
    9.14    then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
    9.15    let ?gcd = "gcd m n"
    9.16 -  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    9.17 +  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp
    9.18    let ?k = "m div ?gcd"
    9.19    let ?l = "n div ?gcd"
    9.20    let ?gcd' = "gcd ?k ?l"
    9.21 @@ -924,9 +925,9 @@
    9.22    have "?gcd' = 1"
    9.23    proof -
    9.24      have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
    9.25 -      by (rule gcd_mult_distrib2)
    9.26 +      by (rule nat_gcd_mult_distrib)
    9.27      with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    9.28 -    with gcd show ?thesis by simp
    9.29 +    with gcd show ?thesis by auto
    9.30    qed
    9.31    ultimately show ?thesis ..
    9.32  qed
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/transfer_data.ML	Wed Jun 17 16:55:01 2009 -0700
    10.3 @@ -0,0 +1,242 @@
    10.4 +(*  Title:      Tools/transfer.ML
    10.5 +    Author:     Amine Chaieb, University of Cambridge, 2009
    10.6 +                Jeremy Avigad, Carnegie Mellon University
    10.7 +*)
    10.8 +
    10.9 +signature TRANSFER_DATA =
   10.10 +sig
   10.11 +  type data
   10.12 +  type entry
   10.13 +  val get: Proof.context -> data
   10.14 +  val del: attribute
   10.15 +  val add: attribute 
   10.16 +  val setup: theory -> theory
   10.17 +end;
   10.18 +
   10.19 +structure TransferData (* : TRANSFER_DATA*) =
   10.20 +struct
   10.21 +type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list}; 
   10.22 +type data = simpset * (thm * entry) list;
   10.23 +
   10.24 +val eq_key = Thm.eq_thm;
   10.25 +fun eq_data arg = eq_fst eq_key arg;
   10.26 +
   10.27 +structure Data = GenericDataFun
   10.28 +(
   10.29 +  type T = data;
   10.30 +  val empty = (HOL_ss, []);
   10.31 +  val extend  = I;
   10.32 +  fun merge _ ((ss, e), (ss', e')) =
   10.33 +    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
   10.34 +);
   10.35 +
   10.36 +val get = Data.get o Context.Proof;
   10.37 +
   10.38 +fun del_data key = apsnd (remove eq_data (key, []));
   10.39 +
   10.40 +val del = Thm.declaration_attribute (Data.map o del_data);
   10.41 +val add_ss = Thm.declaration_attribute 
   10.42 +   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
   10.43 +
   10.44 +val del_ss = Thm.declaration_attribute 
   10.45 +   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
   10.46 +
   10.47 +val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
   10.48 +
   10.49 +fun merge_update eq m (k,v) [] = [(k,v)]
   10.50 +  | merge_update eq m (k,v) ((k',v')::al) = 
   10.51 +           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
   10.52 +
   10.53 +fun C f x y = f y x
   10.54 +
   10.55 +fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
   10.56 + HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
   10.57 +
   10.58 +fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
   10.59 + let 
   10.60 +  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import_thms true (map Drule.mk_term [a0, D0]) ctxt0)
   10.61 +  val (aT,bT) = 
   10.62 +     let val T = typ_of (ctyp_of_term a) 
   10.63 +     in (Term.range_type T, Term.domain_type T)
   10.64 +     end
   10.65 +  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
   10.66 +  val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
   10.67 +  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
   10.68 +  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
   10.69 +  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
   10.70 +  val cis = map (Thm.capply a) cfis
   10.71 +  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
   10.72 +  val th1 = Drule.cterm_instantiate (cns~~ cis) th
   10.73 +  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
   10.74 +  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
   10.75 +                                         (fold_rev implies_intr (map cprop_of hs) th2)
   10.76 +in hd (Variable.export ctxt''' ctxt0 [th3]) end;
   10.77 +
   10.78 +local
   10.79 +fun transfer_ruleh a D leave ctxt th = 
   10.80 + let val (ss,al) = get ctxt
   10.81 +     val a0 = cterm_of (ProofContext.theory_of ctxt) a
   10.82 +     val D0 = cterm_of (ProofContext.theory_of ctxt) D
   10.83 +     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
   10.84 +                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
   10.85 +                 end
   10.86 + in case get_first h al of
   10.87 +      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
   10.88 +    | NONE => error "Transfer: corresponding instance not found in context-data"
   10.89 + end
   10.90 +in fun transfer_rule (a,D) leave (gctxt,th) = 
   10.91 +   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
   10.92 +end;
   10.93 +
   10.94 +fun  splits P [] = []
   10.95 +   | splits P (xxs as (x::xs)) = 
   10.96 +    let val pss = filter (P x) xxs
   10.97 +        val qss = filter_out (P x) xxs
   10.98 +    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
   10.99 +    end
  10.100 +
  10.101 +fun all_transfers leave (gctxt,th) = 
  10.102 + let 
  10.103 +  val ctxt = Context.proof_of gctxt
  10.104 +  val tys = map snd (Term.add_vars (prop_of th) [])
  10.105 +  val _ = if null tys then error "transfer: Unable to guess instance" else ()
  10.106 +  val tyss = splits (curry Type.could_unify) tys 
  10.107 +  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
  10.108 +  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  10.109 +  val insts = 
  10.110 +    map_filter (fn tys => 
  10.111 +          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
  10.112 +                                  then SOME (get_aD k, ss) 
  10.113 +                                  else NONE) (snd (get ctxt))) tyss
  10.114 +  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
  10.115 +  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  10.116 +  val cth = Conjunction.intr_balanced ths
  10.117 + in (gctxt, cth)
  10.118 + end;
  10.119 +
  10.120 +fun transfer_rule_by_hint ls leave (gctxt,th) = 
  10.121 + let 
  10.122 +  val ctxt = Context.proof_of gctxt
  10.123 +  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
  10.124 +  val insts = 
  10.125 +    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
  10.126 +			    then SOME (get_aD k, e) else NONE)
  10.127 +        (snd (get ctxt))
  10.128 +  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
  10.129 +  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
  10.130 +  val cth = Conjunction.intr_balanced ths
  10.131 + in (gctxt, cth)
  10.132 + end;
  10.133 +
  10.134 +
  10.135 +fun transferred_attribute ls NONE leave = 
  10.136 +         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
  10.137 +  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
  10.138 +
  10.139 +                                                    (* Add data to the context *)
  10.140 +fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
  10.141 +                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  10.142 +                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
  10.143 + = 
  10.144 + let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
  10.145 + {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
  10.146 +  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
  10.147 +  hints = subtract (op = : string*string -> bool) hints0 
  10.148 +            (hints1 union_string hints2)}
  10.149 + end;
  10.150 +
  10.151 +local
  10.152 + val h = curry (merge Thm.eq_thm)
  10.153 +in
  10.154 +fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
  10.155 +                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
  10.156 +    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
  10.157 +end; 
  10.158 +
  10.159 +fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
  10.160 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
  10.161 +   (fn (ss, al) => 
  10.162 +     let
  10.163 +      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
  10.164 +                in 0 end) 
  10.165 +                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
  10.166 +      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
  10.167 +      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
  10.168 +      val entry = 
  10.169 +        if g then 
  10.170 +         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
  10.171 +             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
  10.172 +             val inj' = if null inja then #inj (case AList.lookup eq_key al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
  10.173 +                        else inja
  10.174 +             val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
  10.175 +         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
  10.176 +        else e0
  10.177 +    in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
  10.178 +    end));
  10.179 +
  10.180 +
  10.181 +
  10.182 +(* concrete syntax *)
  10.183 +
  10.184 +local
  10.185 +
  10.186 +fun keyword k = Scan.lift (Args.$$$ k) >> K ()
  10.187 +fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  10.188 +
  10.189 +val congN = "cong"
  10.190 +val injN = "inj"
  10.191 +val embedN = "embed"
  10.192 +val returnN = "return"
  10.193 +val addN = "add"
  10.194 +val delN = "del"
  10.195 +val modeN = "mode"
  10.196 +val automaticN = "automatic"
  10.197 +val manualN = "manual"
  10.198 +val directionN = "direction"
  10.199 +val labelsN = "labels"
  10.200 +val leavingN = "leaving"
  10.201 +
  10.202 +val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
  10.203 +
  10.204 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
  10.205 +val terms = thms >> map Drule.dest_term
  10.206 +val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
  10.207 +val name = Scan.lift Args.name
  10.208 +val names = Scan.repeat (Scan.unless any_keyword name)
  10.209 +fun optional scan = Scan.optional scan []
  10.210 +fun optional2 scan = Scan.optional scan ([],[])
  10.211 +
  10.212 +val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
  10.213 +val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
  10.214 +val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
  10.215 +val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
  10.216 +val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
  10.217 +val addscan = Scan.unless any_keyword (keyword addN)
  10.218 +val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
  10.219 +val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
  10.220 +
  10.221 +val transf_add = addscan |-- entry
  10.222 +in
  10.223 +
  10.224 +val install_att_syntax =
  10.225 +  (Scan.lift (Args.$$$ delN >> K del) ||
  10.226 +    transf_add
  10.227 +    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
  10.228 +
  10.229 +val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term)) -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
  10.230 +
  10.231 +end;
  10.232 +
  10.233 +
  10.234 +(* theory setup *)
  10.235 +
  10.236 +
  10.237 +val setup =
  10.238 +  Attrib.setup @{binding transfer} install_att_syntax
  10.239 +    "Installs transfer data" #>
  10.240 +  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
  10.241 +    "simp rules for transfer" #>
  10.242 +  Attrib.setup @{binding transferred} transferred_att_syntax
  10.243 +    "Transfers theorems";
  10.244 +
  10.245 +end;