# HG changeset patch
# User huffman
# Date 1245336675 25200
# Node ID 99f08ce977f9f098b18a1913747f48bcac36f8b5
# Parent  4e6064759aeb79e37ce94758dfcca82fdd3fee6e# Parent  061f01ee9978a8fc5c8dbb44db40c69c28561d13
merged

diff -r 4e6064759aeb -r 99f08ce977f9 doc-src/TutorialI/Types/Overloading.thy
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -478,8 +478,8 @@
   by (induct t rule: maxcoeff.induct, auto)
 
 recdef numgcdh "measure size"
-  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
-  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
+  "numgcdh (C i) = (\<lambda>g. gcd i g)"
+  "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
   "numgcdh t = (\<lambda>g. 1)"
 defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
 
@@ -512,11 +512,11 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
-  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
+  by (induct t rule: numgcdh.induct, auto)
 
 lemma numgcd_pos: "numgcd t \<ge>0"
   by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
@@ -551,15 +551,15 @@
   from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
 qed simp_all
 
-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))"
-  apply (cases "abs i = 0", simp_all add: zgcd_def)
+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))"
+  apply (cases "abs i = 0", simp_all add: gcd_int_def)
   apply (cases "abs j = 0", simp_all)
   apply (cases "abs i = 1", simp_all)
   apply (cases "abs j = 1", simp_all)
   apply auto
   done
 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
-  by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
+  by (induct t rule: numgcdh.induct, auto)
 
 lemma dvdnumcoeff_aux:
   assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
@@ -568,22 +568,22 @@
 proof(induct t rule: numgcdh.induct)
   case (2 n c t) 
   let ?g = "numgcdh t m"
-  from prems have th:"zgcd c ?g > 1" by simp
+  from prems have th:"gcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
   moreover {assume "abs c > 1" and gp: "?g > 1" with prems
     have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
   moreover {assume "abs c = 0 \<and> ?g > 1"
     with prems have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp
     hence ?case by simp }
   moreover {assume "abs c > 1" and g0:"?g = 0" 
     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   ultimately show ?case by blast
-qed(auto simp add: zgcd_zdvd1)
+qed auto
 
 lemma dvdnumcoeff_aux2:
   assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -727,7 +727,7 @@
 constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
   "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
    (let t' = simpnum t ; g = numgcd t' in 
-      if g > 1 then (let g' = zgcd n g in 
+      if g > 1 then (let g' = gcd n g in 
         if g' = 1 then (t',n) 
         else (reducecoeffh t' g', n div g')) 
       else (t',n))))"
@@ -738,23 +738,23 @@
 proof-
   let ?t' = "simpnum t"
   let ?g = "numgcd ?t'"
-  let ?g' = "zgcd n ?g"
+  let ?g' = "gcd n ?g"
   {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   moreover
   { assume nnz: "n \<noteq> 0"
     {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
     moreover
     {assume g1:"?g>1" hence g0: "?g > 0" by simp
-      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
-      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith 
+      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
+      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith 
       hence "?g'= 1 \<or> ?g' > 1" by arith
       moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
       moreover {assume g'1:"?g'>1"
 	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
 	let ?tt = "reducecoeffh ?t' ?g'"
 	let ?t = "Inum bs ?tt"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
+	have gpdg: "?g' dvd ?g" by simp
+	have gpdd: "?g' dvd n" by simp 
 	have gpdgp: "?g' dvd ?g'" by simp
 	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
 	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -774,21 +774,21 @@
 proof-
     let ?t' = "simpnum t"
   let ?g = "numgcd ?t'"
-  let ?g' = "zgcd n ?g"
+  let ?g' = "gcd n ?g"
   {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   moreover
   { assume nnz: "n \<noteq> 0"
     {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
     moreover
     {assume g1:"?g>1" hence g0: "?g > 0" by simp
-      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
-      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
+      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
+      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
       hence "?g'= 1 \<or> ?g' > 1" by arith
       moreover {assume "?g'=1" hence ?thesis using prems 
 	  by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
       moreover {assume g'1:"?g'>1"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
+	have gpdg: "?g' dvd ?g" by simp
+	have gpdd: "?g' dvd n" by simp 
 	have gpdgp: "?g' dvd ?g'" by simp
 	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
 	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -642,9 +642,9 @@
   done
 
 recdef numgcdh "measure size"
-  "numgcdh (C i) = (\<lambda>g. zgcd i g)"
-  "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
-  "numgcdh (CF c s t) = (\<lambda>g. zgcd c (numgcdh t g))"
+  "numgcdh (C i) = (\<lambda>g. gcd i g)"
+  "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
+  "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"
   "numgcdh t = (\<lambda>g. 1)"
 
 definition
@@ -687,13 +687,13 @@
   shows "Inum bs t = 0"
 proof-
   have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0"
-    by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
+    by (induct t rule: numgcdh.induct, auto)
   thus ?thesis using g0[simplified numgcd_def] by blast
 qed
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
-  by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
+  by (induct t rule: numgcdh.induct, auto)
 
 lemma numgcd_pos: "numgcd t \<ge>0"
   by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
@@ -738,8 +738,8 @@
   from ismaxcoeff_mono[OF H1 thh1] show ?case by (simp add: le_maxI1)
 qed simp_all
 
-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))"
-  apply (unfold zgcd_def)
+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))"
+  apply (unfold gcd_int_def)
   apply (cases "i = 0", simp_all)
   apply (cases "j = 0", simp_all)
   apply (cases "abs i = 1", simp_all)
@@ -747,7 +747,7 @@
   apply auto
   done
 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
-  by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
+  by (induct t rule: numgcdh.induct, auto)
 
 lemma dvdnumcoeff_aux:
   assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
@@ -756,17 +756,17 @@
 proof(induct t rule: numgcdh.induct)
   case (2 n c t) 
   let ?g = "numgcdh t m"
-  from prems have th:"zgcd c ?g > 1" by simp
+  from prems have th:"gcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
   moreover {assume "abs c > 1" and gp: "?g > 1" with prems
     have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
   moreover {assume "abs c = 0 \<and> ?g > 1"
     with prems have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp
     hence ?case by simp }
   moreover {assume "abs c > 1" and g0:"?g = 0" 
     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
@@ -774,22 +774,22 @@
 next
   case (3 c s t) 
   let ?g = "numgcdh t m"
-  from prems have th:"zgcd c ?g > 1" by simp
+  from prems have th:"gcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
   moreover {assume "abs c > 1" and gp: "?g > 1" with prems
     have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
   moreover {assume "abs c = 0 \<and> ?g > 1"
     with prems have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
+    have th': "gcd c ?g dvd ?g" by simp
+    from dvdnumcoeff_trans[OF th' th] have ?case by simp
     hence ?case by simp }
   moreover {assume "abs c > 1" and g0:"?g = 0" 
     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   ultimately show ?case by blast
-qed(auto simp add: zgcd_zdvd1)
+qed auto
 
 lemma dvdnumcoeff_aux2:
   assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -1041,7 +1041,7 @@
 constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
   "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
    (let t' = simpnum t ; g = numgcd t' in 
-      if g > 1 then (let g' = zgcd n g in 
+      if g > 1 then (let g' = gcd n g in 
         if g' = 1 then (t',n) 
         else (reducecoeffh t' g', n div g')) 
       else (t',n))))"
@@ -1052,23 +1052,23 @@
 proof-
   let ?t' = "simpnum t"
   let ?g = "numgcd ?t'"
-  let ?g' = "zgcd n ?g"
+  let ?g' = "gcd n ?g"
   {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   moreover
   { assume nnz: "n \<noteq> 0"
     {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
     moreover
     {assume g1:"?g>1" hence g0: "?g > 0" by simp
-      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
-      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
+      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
+      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
       hence "?g'= 1 \<or> ?g' > 1" by arith
       moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
       moreover {assume g'1:"?g'>1"
 	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
 	let ?tt = "reducecoeffh ?t' ?g'"
 	let ?t = "Inum bs ?tt"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
+	have gpdg: "?g' dvd ?g" by simp
+	have gpdd: "?g' dvd n" by simp
 	have gpdgp: "?g' dvd ?g'" by simp
 	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
 	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -1088,21 +1088,21 @@
 proof-
     let ?t' = "simpnum t"
   let ?g = "numgcd ?t'"
-  let ?g' = "zgcd n ?g"
+  let ?g' = "gcd n ?g"
   {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
   moreover
   { assume nnz: "n \<noteq> 0"
     {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}
     moreover
     {assume g1:"?g>1" hence g0: "?g > 0" by simp
-      from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
-      hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
+      from g1 nnz have gp0: "?g' \<noteq> 0" by simp
+      hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith
       hence "?g'= 1 \<or> ?g' > 1" by arith
       moreover {assume "?g'=1" hence ?thesis using prems 
 	  by (auto simp add: Let_def simp_num_pair_def)}
       moreover {assume g'1:"?g'>1"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
+	have gpdg: "?g' dvd ?g" by simp
+	have gpdd: "?g' dvd n" by simp
 	have gpdgp: "?g' dvd ?g'" by simp
 	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
 	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
@@ -1219,7 +1219,7 @@
 constdefs simpdvd:: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)"
   "simpdvd d t \<equiv> 
    (let g = numgcd t in 
-      if g > 1 then (let g' = zgcd d g in 
+      if g > 1 then (let g' = gcd d g in 
         if g' = 1 then (d, t) 
         else (d div g',reducecoeffh t g')) 
       else (d, t))"
@@ -1228,20 +1228,20 @@
   shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)"
 proof-
   let ?g = "numgcd t"
-  let ?g' = "zgcd d ?g"
+  let ?g' = "gcd d ?g"
   {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)}
   moreover
   {assume g1:"?g>1" hence g0: "?g > 0" by simp
-    from zgcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
-    hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="numgcd t"] by arith
+    from g1 dnz have gp0: "?g' \<noteq> 0" by simp
+    hence g'p: "?g' > 0" using int_gcd_ge_0[where x="d" and y="numgcd t"] by arith
     hence "?g'= 1 \<or> ?g' > 1" by arith
     moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}
     moreover {assume g'1:"?g'>1"
       from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
       let ?tt = "reducecoeffh t ?g'"
       let ?t = "Inum bs ?tt"
-      have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
-      have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1) 
+      have gpdg: "?g' dvd ?g" by simp
+      have gpdd: "?g' dvd d" by simp
       have gpdgp: "?g' dvd ?g'" by simp
       from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
       have th2:"real ?g' * ?t = Inum bs t" by simp
@@ -2093,8 +2093,8 @@
   "plusinf p = p"
 
 recdef \<delta> "measure size"
-  "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)" 
-  "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)" 
+  "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 
+  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
   "\<delta> (Dvd i (CN 0 c e)) = i"
   "\<delta> (NDvd i (CN 0 c e)) = i"
   "\<delta> p = 1"
@@ -2126,20 +2126,20 @@
 proof (induct p rule: iszlfm.induct)
   case (1 p q) 
   let ?d = "\<delta> (And p q)"
-  from prems zlcm_pos have dp: "?d >0" by simp
+  from prems int_lcm_pos have dp: "?d >0" by simp
   have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
    hence th: "d\<delta> p ?d" 
-     using delta_mono prems by (auto simp del: dvd_zlcm_self1)
+     using delta_mono prems by (auto simp del: int_lcm_dvd1)
   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)
+  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
   from th th' dp show ?case by simp 
 next
   case (2 p q)  
   let ?d = "\<delta> (And p q)"
-  from prems zlcm_pos have dp: "?d >0" by simp
+  from prems int_lcm_pos have dp: "?d >0" by simp
   have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
-    by (auto simp del: dvd_zlcm_self1)
-  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)
+    by (auto simp del: int_lcm_dvd1)
+  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)
   from th th' dp show ?case by simp 
 qed simp_all
 
@@ -2388,8 +2388,8 @@
   "d\<beta> p = (\<lambda> k. True)"
 
 recdef \<zeta> "measure size"
-  "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)" 
-  "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)" 
+  "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
+  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" 
   "\<zeta> (Eq  (CN 0 c e)) = c"
   "\<zeta> (NEq (CN 0 c e)) = c"
   "\<zeta> (Lt  (CN 0 c e)) = c"
@@ -2510,19 +2510,19 @@
 using linp
 proof(induct p rule: iszlfm.induct)
   case (1 p q)
-  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
-    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
+  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    dl1 dl2 show ?case by (auto simp add: int_lcm_pos)
 next
   case (2 p q)
-  from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
-  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"] 
-    dl1 dl2 show ?case by (auto simp add: zlcm_pos)
-qed (auto simp add: zlcm_pos)
+  from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    dl1 dl2 show ?case by (auto simp add: int_lcm_pos)
+qed (auto simp add: int_lcm_pos)
 
 lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
   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)"
@@ -4173,9 +4173,9 @@
 
 lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
   by (induct p rule: isrlfm.induct, auto)
-lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
+lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \<le> i"
 proof-
-  from zgcd_zdvd1 have th: "zgcd i j dvd i" by blast
+  from int_gcd_dvd1 have th: "gcd i j dvd i" by blast
   from zdvd_imp_le[OF th ip] show ?thesis .
 qed
 
@@ -5119,9 +5119,9 @@
   let ?M = "?I x (minusinf ?rq)"
   let ?P = "?I x (plusinf ?rq)"
   have MF: "?M = False"
-    apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
+    apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
     by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
-  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)
+  have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
     by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
   have "(\<exists> x. ?I x ?q ) = 
     ((?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))))"
@@ -5286,7 +5286,7 @@
   let ?F = "\<lambda> p. \<exists> a \<in> set (\<Upsilon> p). \<exists> b \<in> set (\<Upsilon> p). ?I x (\<upsilon> p (?g(a,b)))"
   let ?ep = "evaldjf (\<upsilon> ?q) ?Y"
   from rlfm_l[OF qf] have lq: "isrlfm ?q" 
-    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def zgcd_def)
+    by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def)
   from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   from U_l UpU 
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/GCD.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -1,202 +1,563 @@
-(*  Title:      HOL/GCD.thy
-    Author:     Christophe Tabacznyj and Lawrence C Paulson
-    Copyright   1996  University of Cambridge
+(*  Title:      GCD.thy
+    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
+                Thomas M. Rasmussen, Jeremy Avigad
+
+
+This file deals with the functions gcd and lcm, and properties of
+primes. Definitions and lemmas are proved uniformly for the natural
+numbers and integers.
+
+This file combines and revises a number of prior developments.
+
+The original theories "GCD" and "Primes" were by Christophe Tabacznyj
+and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+gcd, lcm, and prime for the natural numbers.
+
+The original theory "IntPrimes" was by Thomas M. Rasmussen, and
+extended gcd, lcm, primes to the integers. Amine Chaieb provided
+another extension of the notions to the integers, and added a number
+of results to "Primes" and "GCD". IntPrimes also defined and developed
+the congruence relations on the integers. The notion was extended to
+the natural numbers by Chiaeb.
+
 *)
 
-header {* The Greatest Common Divisor *}
+
+header {* GCD *}
 
 theory GCD
-imports Main
+imports NatTransfer
+begin
+
+declare One_nat_def [simp del]
+
+subsection {* gcd *}
+
+class gcd = one +
+
+fixes
+  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
+  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
 begin
 
-text {*
-  See \cite{davenport92}. \bigskip
-*}
+abbreviation
+  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  "coprime x y == (gcd x y = 1)"
+
+end
+
+class prime = one +
+
+fixes
+  prime :: "'a \<Rightarrow> bool"
+
+
+(* definitions for the natural numbers *)
+
+instantiation nat :: gcd
+
+begin
 
-subsection {* Specification of GCD on nats *}
+fun
+  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "gcd_nat x y =
+   (if y = 0 then x else gcd y (x mod y))"
+
+definition
+  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "lcm_nat x y = x * y div (gcd x y)"
+
+instance proof qed
+
+end
+
+
+instantiation nat :: prime
+
+begin
 
 definition
-  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
-  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
-    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
+  prime_nat :: "nat \<Rightarrow> bool"
+where
+  [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+
+instance proof qed
 
-text {* Uniqueness *}
+end
+
 
-lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
-  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
+(* definitions for the integers *)
+
+instantiation int :: gcd
 
-text {* Connection to divides relation *}
+begin
 
-lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
-  by (auto simp add: is_gcd_def)
+definition
+  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
 
-text {* Commutativity *}
+definition
+  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
 
-lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
-  by (auto simp add: is_gcd_def)
+instance proof qed
+
+end
 
 
-subsection {* GCD on nat by Euclid's algorithm *}
+instantiation int :: prime
+
+begin
+
+definition
+  prime_int :: "int \<Rightarrow> bool"
+where
+  [code del]: "prime_int p = prime (nat p)"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up Transfer *}
+
+
+lemma transfer_nat_int_gcd:
+  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
+  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
+  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
+  unfolding gcd_int_def lcm_int_def prime_int_def
+  by auto
 
-fun
-  gcd  :: "nat => nat => nat"
-where
-  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
-lemma gcd_induct [case_names "0" rec]:
+lemma transfer_nat_int_gcd_closures:
+  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
+  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
+  by (auto simp add: gcd_int_def lcm_int_def)
+
+declare TransferMorphism_nat_int[transfer add return:
+    transfer_nat_int_gcd transfer_nat_int_gcd_closures]
+
+lemma transfer_int_nat_gcd:
+  "gcd (int x) (int y) = int (gcd x y)"
+  "lcm (int x) (int y) = int (lcm x y)"
+  "prime (int x) = prime x"
+  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
+
+lemma transfer_int_nat_gcd_closures:
+  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
+  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
+  by (auto simp add: gcd_int_def lcm_int_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+    transfer_int_nat_gcd transfer_int_nat_gcd_closures]
+
+
+
+subsection {* GCD *}
+
+(* was gcd_induct *)
+lemma nat_gcd_induct:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   shows "P m n"
-proof (induct m n rule: gcd.induct)
-  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
-qed
+  apply (rule gcd_nat.induct)
+  apply (case_tac "y = 0")
+  using assms apply simp_all
+done
+
+(* specific to int *)
+
+lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
+  by (simp add: gcd_int_def)
+
+lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
+  by (simp add: gcd_int_def)
+
+lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
+  by (simp add: gcd_int_def)
+
+lemma int_gcd_cases:
+  fixes x :: int and y
+  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
+      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
+      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
+      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
+  shows "P (gcd x y)"
+by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
 
-lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
-  by simp
+lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
+  by (simp add: gcd_int_def)
+
+lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
+  by (simp add: lcm_int_def)
+
+lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
+  by (simp add: lcm_int_def)
+
+lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
+  by (simp add: lcm_int_def)
 
-lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
+lemma int_lcm_cases:
+  fixes x :: int and y
+  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
+      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
+      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
+      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
+  shows "P (lcm x y)"
+by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
+
+lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
+  by (simp add: lcm_int_def)
+
+(* was gcd_0, etc. *)
+lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
   by simp
 
-lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
+(* was igcd_0, etc. *)
+lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
+  by (unfold gcd_int_def, auto)
+
+lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
   by simp
 
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
+lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
+  by (unfold gcd_int_def, auto)
+
+lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
+  by (case_tac "y = 0", auto)
+
+(* weaker, but useful for the simplifier *)
+
+lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
+  by simp
+
+lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   by simp
 
-lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
-  unfolding One_nat_def by (rule gcd_1)
+lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
+  by (simp add: One_nat_def)
+
+lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
+  by (simp add: gcd_int_def)
 
-declare gcd.simps [simp del]
+lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
+  by simp
+
+lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
+  by (subst int_gcd_abs, auto simp add: gcd_int_def)
+
+declare gcd_nat.simps [simp del]
 
 text {*
   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   conjunctions don't seem provable separately.
 *}
 
-lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
-  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
-  apply (induct m n rule: gcd_induct)
-     apply (simp_all add: gcd_non_0)
+lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
+  and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
+  apply (induct m n rule: nat_gcd_induct)
+  apply (simp_all add: nat_gcd_non_0)
   apply (blast dest: dvd_mod_imp_dvd)
-  done
+done
+
+thm nat_gcd_dvd1 [transferred]
+
+lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
+  apply (subst int_gcd_abs)
+  apply (rule dvd_trans)
+  apply (rule nat_gcd_dvd1 [transferred])
+  apply auto
+done
 
-text {*
-  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
-  naturals, if @{term k} divides @{term m} and @{term k} divides
-  @{term n} then @{term k} divides @{term "gcd m n"}.
-*}
+lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
+  apply (subst int_gcd_abs)
+  apply (rule dvd_trans)
+  apply (rule nat_gcd_dvd2 [transferred])
+  apply auto
+done
+
+lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
+  by (rule dvd_imp_le, auto)
+
+lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
+  by (rule dvd_imp_le, auto)
+
+lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
+  by (rule zdvd_imp_le, auto)
 
-lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
-  by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
+lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
+  by (rule zdvd_imp_le, auto)
+
+lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
+  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
+
+lemma int_gcd_greatest:
+  assumes "(k::int) dvd m" and "k dvd n"
+  shows "k dvd gcd m n"
+
+  apply (subst int_gcd_abs)
+  apply (subst abs_dvd_iff [symmetric])
+  apply (rule nat_gcd_greatest [transferred])
+  using prems apply auto
+done
 
-text {*
-  \medskip Function gcd yields the Greatest Common Divisor.
-*}
+lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
+    (k dvd m & k dvd n)"
+  by (blast intro!: nat_gcd_greatest intro: dvd_trans)
+
+lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
+  by (blast intro!: int_gcd_greatest intro: dvd_trans)
 
-lemma is_gcd: "is_gcd m n (gcd m n) "
-  by (simp add: is_gcd_def gcd_greatest)
+lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
+  by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
 
+lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
+  by (auto simp add: gcd_int_def)
 
-subsection {* Derived laws for GCD *}
+lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
+  by (insert nat_gcd_zero [of m n], arith)
 
-lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
-  by (blast intro!: gcd_greatest intro: dvd_trans)
+lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
+  by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
+
+lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
+  by (rule dvd_anti_sym, auto)
 
-lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
-  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
+lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
+  by (auto simp add: gcd_int_def nat_gcd_commute)
+
+lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
+  apply (rule dvd_anti_sym)
+  apply (blast intro: dvd_trans)+
+done
 
-lemma gcd_commute: "gcd m n = gcd n m"
-  apply (rule is_gcd_unique)
-   apply (rule is_gcd)
-  apply (subst is_gcd_commute)
-  apply (simp add: is_gcd)
-  done
+lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
+  by (auto simp add: gcd_int_def nat_gcd_assoc)
+
+lemma nat_gcd_left_commute: "gcd (k::nat) (gcd m n) = gcd m (gcd k n)"
+  apply (rule nat_gcd_commute [THEN trans])
+  apply (rule nat_gcd_assoc [THEN trans])
+  apply (rule nat_gcd_commute [THEN arg_cong])
+done
+
+lemma int_gcd_left_commute: "gcd (k::int) (gcd m n) = gcd m (gcd k n)"
+  apply (rule int_gcd_commute [THEN trans])
+  apply (rule int_gcd_assoc [THEN trans])
+  apply (rule int_gcd_commute [THEN arg_cong])
+done
+
+lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
+  -- {* gcd is an AC-operator *}
 
-lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
-  apply (rule is_gcd_unique)
-   apply (rule is_gcd)
-  apply (simp add: is_gcd_def)
-  apply (blast intro: dvd_trans)
-  done
+lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
+
+lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
+  by (subst nat_gcd_commute, simp)
+
+lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
+  by (subst nat_gcd_commute, simp add: One_nat_def)
+
+lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
+  by (subst int_gcd_commute, simp)
 
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
-  by (simp add: gcd_commute)
+lemma nat_gcd_unique: "(d::nat) 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"
+  apply auto
+  apply (rule dvd_anti_sym)
+  apply (erule (1) nat_gcd_greatest)
+  apply auto
+done
 
-lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
-  unfolding One_nat_def by (rule gcd_1_left)
+lemma int_gcd_unique: "d >= 0 & (d::int) 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"
+  apply (case_tac "d = 0")
+  apply force
+  apply (rule iffI)
+  apply (rule zdvd_anti_sym)
+  apply arith
+  apply (subst int_gcd_pos)
+  apply clarsimp
+  apply (drule_tac x = "d + 1" in spec)
+  apply (frule zdvd_imp_le)
+  apply (auto intro: int_gcd_greatest)
+done
 
 text {*
   \medskip Multiplication laws
 *}
 
-lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
+lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
     -- {* \cite[page 27]{davenport92} *}
-  apply (induct m n rule: gcd_induct)
-   apply simp
+  apply (induct m n rule: nat_gcd_induct)
+  apply simp
   apply (case_tac "k = 0")
-   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
-  done
+  apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
+done
 
-lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
-  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
-  done
+lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
+  apply (subst (1 2) int_gcd_abs)
+  apply (simp add: abs_mult)
+  apply (rule nat_gcd_mult_distrib [transferred])
+  apply auto
+done
 
-lemma gcd_self [simp, algebra]: "gcd k k = k"
-  apply (rule gcd_mult [of k 1, simplified])
-  done
+lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
+  by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
 
-lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
-  apply (insert gcd_mult_distrib2 [of m k n])
+lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
+  by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
+
+lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
+  apply (insert nat_gcd_mult_distrib [of m k n])
   apply simp
   apply (erule_tac t = m in ssubst)
   apply simp
   done
 
-lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
-  by (auto intro: relprime_dvd_mult dvd_mult2)
+lemma int_coprime_dvd_mult:
+  assumes "coprime (k::int) n" and "k dvd m * n"
+  shows "k dvd m"
 
-lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
+  using prems
+  apply (subst abs_dvd_iff [symmetric])
+  apply (subst dvd_abs_iff [symmetric])
+  apply (subst (asm) int_gcd_abs)
+  apply (rule nat_coprime_dvd_mult [transferred])
+  apply auto
+  apply (subst abs_mult [symmetric], auto)
+done
+
+lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
+    (k dvd m * n) = (k dvd m)"
+  by (auto intro: nat_coprime_dvd_mult)
+
+lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
+    (k dvd m * n) = (k dvd m)"
+  by (auto intro: int_coprime_dvd_mult)
+
+lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   apply (rule dvd_anti_sym)
-   apply (rule gcd_greatest)
-    apply (rule_tac n = k in relprime_dvd_mult)
-     apply (simp add: gcd_assoc)
-     apply (simp add: gcd_commute)
-    apply (simp_all add: mult_commute)
-  done
+  apply (rule nat_gcd_greatest)
+  apply (rule_tac n = k in nat_coprime_dvd_mult)
+  apply (simp add: nat_gcd_assoc)
+  apply (simp add: nat_gcd_commute)
+  apply (simp_all add: mult_commute)
+done
 
+lemma int_gcd_mult_cancel:
+  assumes "coprime (k::int) n"
+  shows "gcd (k * m) n = gcd m n"
+
+  using prems
+  apply (subst (1 2) int_gcd_abs)
+  apply (subst abs_mult)
+  apply (rule nat_gcd_mult_cancel [transferred])
+  apply (auto simp add: int_gcd_abs [symmetric])
+done
 
 text {* \medskip Addition laws *}
 
-lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
-  by (cases "n = 0") (auto simp add: gcd_non_0)
+lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
+  apply (case_tac "n = 0")
+  apply (simp_all add: nat_gcd_non_0)
+done
+
+lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
+  apply (subst (1 2) nat_gcd_commute)
+  apply (subst add_commute)
+  apply simp
+done
+
+(* to do: add the other variations? *)
+
+lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
+  by (subst nat_gcd_add1 [symmetric], auto)
+
+lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
+  apply (subst nat_gcd_commute)
+  apply (subst nat_gcd_diff1 [symmetric])
+  apply auto
+  apply (subst nat_gcd_commute)
+  apply (subst nat_gcd_diff1)
+  apply assumption
+  apply (rule nat_gcd_commute)
+done
+
+lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+  apply (frule_tac b = y and a = x in pos_mod_sign)
+  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
+  apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
+    zmod_zminus1_eq_if)
+  apply (frule_tac a = x in pos_mod_bound)
+  apply (subst (1 2) nat_gcd_commute)
+  apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
+    nat_le_eq_zle)
+done
 
-lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
-proof -
-  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
-  also have "... = gcd (n + m) m" by (simp add: add_commute)
-  also have "... = gcd n m" by simp
-  also have  "... = gcd m n" by (rule gcd_commute)
-  finally show ?thesis .
-qed
+lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
+  apply (case_tac "y = 0")
+  apply force
+  apply (case_tac "y > 0")
+  apply (subst int_gcd_non_0, auto)
+  apply (insert int_gcd_non_0 [of "-y" "-x"])
+  apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
+done
+
+lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
+  apply (case_tac "n = 0", force)
+  apply (subst (1 2) int_gcd_red)
+  apply auto
+done
+
+lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
+  apply (subst int_gcd_commute)
+  apply (subst add_commute)
+  apply (subst int_gcd_add1)
+  apply (subst int_gcd_commute)
+  apply (rule refl)
+done
 
-lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
-  apply (subst add_commute)
-  apply (rule gcd_add2)
-  done
+lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
+  by (induct k, simp_all add: ring_simps)
 
-lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
-  by (induct k) (simp_all add: add_assoc)
+lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
+  apply (subgoal_tac "ALL s. ALL m. ALL n.
+      gcd m (int (s::nat) * m + n) = gcd m n")
+  apply (case_tac "k >= 0")
+  apply (drule_tac x = "nat k" in spec, force)
+  apply (subst (1 2) int_gcd_neg2 [symmetric])
+  apply (drule_tac x = "nat (- k)" in spec)
+  apply (drule_tac x = "m" in spec)
+  apply (drule_tac x = "-n" in spec)
+  apply auto
+  apply (rule nat_induct)
+  apply auto
+  apply (auto simp add: left_distrib)
+  apply (subst add_assoc)
+  apply simp
+done
 
-lemma gcd_dvd_prod: "gcd m n dvd m * n" 
+(* to do: differences, and all variations of addition rules
+    as simplification rules for nat and int *)
+
+lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   using mult_dvd_mono [of 1] by auto
 
-text {*
-  \medskip Division by gcd yields rrelatively primes.
-*}
+(* to do: add the three variations of these, and for ints? *)
+
 
-lemma div_gcd_relprime:
-  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
-  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
+subsection {* Coprimality *}
+
+lemma nat_div_gcd_coprime [intro]:
+  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
+  shows "coprime (a div gcd a b) (b div gcd a b)"
 proof -
   let ?g = "gcd a b"
   let ?a' = "a div ?g"
@@ -207,42 +568,551 @@
   from dvdg dvdg' obtain ka kb ka' kb' where
       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     unfolding dvd_def by blast
-  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
+  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+    by simp_all
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
-  then have gp: "?g > 0" by simp
-  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
+  then have gp: "?g > 0" by arith
+  from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
 qed
 
+lemma int_div_gcd_coprime [intro]:
+  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
+  shows "coprime (a div gcd a b) (b div gcd a b)"
 
-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"
-proof(auto)
-  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
-  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
-  have th: "gcd a b dvd d" by blast
-  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
+  apply (subst (1 2 3) int_gcd_abs)
+  apply (subst (1 2) abs_div)
+  apply auto
+  prefer 3
+  apply (rule nat_div_gcd_coprime [transferred])
+  using nz apply (auto simp add: int_gcd_abs [symmetric])
+done
+
+lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+  using nat_gcd_unique[of 1 a b, simplified] by auto
+
+lemma nat_coprime_Suc_0:
+    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
+  using nat_coprime by (simp add: One_nat_def)
+
+lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
+    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+  using int_gcd_unique [of 1 a b]
+  apply clarsimp
+  apply (erule subst)
+  apply (rule iffI)
+  apply force
+  apply (drule_tac x = "abs e" in exI)
+  apply (case_tac "e >= 0")
+  apply force
+  apply force
+done
+
+lemma nat_gcd_coprime:
+  assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
+    b: "b = b' * gcd a b"
+  shows    "coprime a' b'"
+
+  apply (subgoal_tac "a' = a div gcd a b")
+  apply (erule ssubst)
+  apply (subgoal_tac "b' = b div gcd a b")
+  apply (erule ssubst)
+  apply (rule nat_div_gcd_coprime)
+  using prems
+  apply force
+  apply (subst (1) b)
+  using z apply force
+  apply (subst (1) a)
+  using z apply force
+done
+
+lemma int_gcd_coprime:
+  assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
+    b: "b = b' * gcd a b"
+  shows    "coprime a' b'"
+
+  apply (subgoal_tac "a' = a div gcd a b")
+  apply (erule ssubst)
+  apply (subgoal_tac "b' = b div gcd a b")
+  apply (erule ssubst)
+  apply (rule int_div_gcd_coprime)
+  using prems
+  apply force
+  apply (subst (1) b)
+  using z apply force
+  apply (subst (1) a)
+  using z apply force
+done
+
+lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
+    shows "coprime d (a * b)"
+  apply (subst nat_gcd_commute)
+  using da apply (subst nat_gcd_mult_cancel)
+  apply (subst nat_gcd_commute, assumption)
+  apply (subst nat_gcd_commute, rule db)
+done
+
+lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
+    shows "coprime d (a * b)"
+  apply (subst int_gcd_commute)
+  using da apply (subst int_gcd_mult_cancel)
+  apply (subst int_gcd_commute, assumption)
+  apply (subst int_gcd_commute, rule db)
+done
+
+lemma nat_coprime_lmult:
+  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
+proof -
+  have "gcd d a dvd gcd d (a * b)"
+    by (rule nat_gcd_greatest, auto)
+  with dab show ?thesis
+    by auto
+qed
+
+lemma int_coprime_lmult:
+  assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
+proof -
+  have "gcd d a dvd gcd d (a * b)"
+    by (rule int_gcd_greatest, auto)
+  with dab show ?thesis
+    by auto
+qed
+
+lemma nat_coprime_rmult:
+  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
+proof -
+  have "gcd d b dvd gcd d (a * b)"
+    by (rule nat_gcd_greatest, auto intro: dvd_mult)
+  with dab show ?thesis
+    by auto
+qed
+
+lemma int_coprime_rmult:
+  assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
+proof -
+  have "gcd d b dvd gcd d (a * b)"
+    by (rule int_gcd_greatest, auto intro: dvd_mult)
+  with dab show ?thesis
+    by auto
+qed
+
+lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
+    coprime d a \<and>  coprime d b"
+  using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
+    nat_coprime_mult[of d a b]
+  by blast
+
+lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
+    coprime d a \<and>  coprime d b"
+  using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
+    int_coprime_mult[of d a b]
+  by blast
+
+lemma nat_gcd_coprime_exists:
+    assumes nz: "gcd (a::nat) b \<noteq> 0"
+    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+  apply (rule_tac x = "a div gcd a b" in exI)
+  apply (rule_tac x = "b div gcd a b" in exI)
+  using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
+done
+
+lemma int_gcd_coprime_exists:
+    assumes nz: "gcd (a::int) b \<noteq> 0"
+    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+  apply (rule_tac x = "a div gcd a b" in exI)
+  apply (rule_tac x = "b div gcd a b" in exI)
+  using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
+done
+
+lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
+  by (induct n, simp_all add: nat_coprime_mult)
+
+lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
+  by (induct n, simp_all add: int_coprime_mult)
+
+lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
+  apply (rule nat_coprime_exp)
+  apply (subst nat_gcd_commute)
+  apply (rule nat_coprime_exp)
+  apply (subst nat_gcd_commute, assumption)
+done
+
+lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
+  apply (rule int_coprime_exp)
+  apply (subst int_gcd_commute)
+  apply (rule int_coprime_exp)
+  apply (subst int_gcd_commute, assumption)
+done
+
+lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
+proof (cases)
+  assume "a = 0 & b = 0"
+  thus ?thesis by simp
+  next assume "~(a = 0 & b = 0)"
+  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
+    by auto
+  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
+      ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
+    apply (subst (1 2) mult_commute)
+    apply (subst nat_gcd_mult_distrib [symmetric])
+    apply simp
+    done
+  also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
+    apply (subst div_power)
+    apply auto
+    apply (rule dvd_div_mult_self)
+    apply (rule dvd_power_same)
+    apply auto
+    done
+  also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
+    apply (subst div_power)
+    apply auto
+    apply (rule dvd_div_mult_self)
+    apply (rule dvd_power_same)
+    apply auto
+    done
+  finally show ?thesis .
+qed
+
+lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
+  apply (subst (1 2) int_gcd_abs)
+  apply (subst (1 2) power_abs)
+  apply (rule nat_gcd_exp [where n = n, transferred])
+  apply auto
+done
+
+lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
+  using nat_coprime_dvd_mult_iff[of d a b]
+  by (auto simp add: mult_commute)
+
+lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
+  using int_coprime_dvd_mult_iff[of d a b]
+  by (auto simp add: mult_commute)
+
+lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
+  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof-
+  let ?g = "gcd a b"
+  {assume "?g = 0" with dc have ?thesis by auto}
+  moreover
+  {assume z: "?g \<noteq> 0"
+    from nat_gcd_coprime_exists[OF z]
+    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
+      by blast
+    have thb: "?g dvd b" by auto
+    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
+    with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
+    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
+    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
+    with z have th_1: "a' dvd b' * c" by auto
+    from nat_coprime_dvd_mult[OF ab'(3)] th_1
+    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
+    from ab' have "a = ?g*a'" by algebra
+    with thb thc have ?thesis by blast }
+  ultimately show ?thesis by blast
+qed
+
+lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
+  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof-
+  let ?g = "gcd a b"
+  {assume "?g = 0" with dc have ?thesis by auto}
+  moreover
+  {assume z: "?g \<noteq> 0"
+    from int_gcd_coprime_exists[OF z]
+    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
+      by blast
+    have thb: "?g dvd b" by auto
+    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
+    with dc have th0: "a' dvd b*c"
+      using dvd_trans[of a' a "b*c"] by simp
+    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
+    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
+    with z have th_1: "a' dvd b' * c" by auto
+    from int_coprime_dvd_mult[OF ab'(3)] th_1
+    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
+    from ab' have "a = ?g*a'" by algebra
+    with thb thc have ?thesis by blast }
+  ultimately show ?thesis by blast
 qed
 
-lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
-  shows "gcd x y = gcd u v"
+lemma nat_pow_divides_pow:
+  assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
+  shows "a dvd b"
+proof-
+  let ?g = "gcd a b"
+  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
+  {assume "?g = 0" with ab n have ?thesis by auto }
+  moreover
+  {assume z: "?g \<noteq> 0"
+    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+    from nat_gcd_coprime_exists[OF z]
+    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
+      by blast
+    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
+      by (simp add: ab'(1,2)[symmetric])
+    hence "?g^n*a'^n dvd ?g^n *b'^n"
+      by (simp only: power_mult_distrib mult_commute)
+    with zn z n have th0:"a'^n dvd b'^n" by auto
+    have "a' dvd a'^n" by (simp add: m)
+    with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
+    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
+    from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
+    have "a' dvd b'" by (subst (asm) mult_commute, blast)
+    hence "a'*?g dvd b'*?g" by simp
+    with ab'(1,2)  have ?thesis by simp }
+  ultimately show ?thesis by blast
+qed
+
+lemma int_pow_divides_pow:
+  assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
+  shows "a dvd b"
 proof-
-  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
-  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
+  let ?g = "gcd a b"
+  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
+  {assume "?g = 0" with ab n have ?thesis by auto }
+  moreover
+  {assume z: "?g \<noteq> 0"
+    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+    from int_gcd_coprime_exists[OF z]
+    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
+      by blast
+    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
+      by (simp add: ab'(1,2)[symmetric])
+    hence "?g^n*a'^n dvd ?g^n *b'^n"
+      by (simp only: power_mult_distrib mult_commute)
+    with zn z n have th0:"a'^n dvd b'^n" by auto
+    have "a' dvd a'^n" by (simp add: m)
+    with th0 have "a' dvd b'^n"
+      using dvd_trans[of a' "a'^n" "b'^n"] by simp
+    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
+    from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
+    have "a' dvd b'" by (subst (asm) mult_commute, blast)
+    hence "a'*?g dvd b'*?g" by simp
+    with ab'(1,2)  have ?thesis by simp }
+  ultimately show ?thesis by blast
+qed
+
+lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
+  by (auto intro: nat_pow_divides_pow dvd_power_same)
+
+lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
+  by (auto intro: int_pow_divides_pow dvd_power_same)
+
+lemma nat_divides_mult:
+  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
+  shows "m * n dvd r"
+proof-
+  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
+    unfolding dvd_def by blast
+  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
+  hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
+  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
+  from n' k show ?thesis unfolding dvd_def by auto
+qed
+
+lemma int_divides_mult:
+  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
+  shows "m * n dvd r"
+proof-
+  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
+    unfolding dvd_def by blast
+  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
+  hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
+  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
+  from n' k show ?thesis unfolding dvd_def by auto
 qed
 
-lemma ind_euclid: 
-  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
-  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
+lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
+  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
+  apply force
+  apply (rule nat_dvd_diff)
+  apply auto
+done
+
+lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
+  using nat_coprime_plus_one by (simp add: One_nat_def)
+
+lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
+  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
+  apply force
+  apply (rule dvd_diff)
+  apply auto
+done
+
+lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
+  using nat_coprime_plus_one [of "n - 1"]
+    nat_gcd_commute [of "n - 1" n] by auto
+
+lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
+  using int_coprime_plus_one [of "n - 1"]
+    int_gcd_commute [of "n - 1" n] by auto
+
+lemma nat_setprod_coprime [rule_format]:
+    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto simp add: nat_gcd_mult_cancel)
+done
+
+lemma int_setprod_coprime [rule_format]:
+    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto simp add: int_gcd_mult_cancel)
+done
+
+lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+  unfolding prime_nat_def
+  apply (subst even_mult_two_ex)
+  apply clarify
+  apply (drule_tac x = 2 in spec)
+  apply auto
+done
+
+lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+  unfolding prime_int_def
+  apply (frule nat_prime_odd)
+  apply (auto simp add: even_nat_def)
+done
+
+lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
+    x dvd b \<Longrightarrow> x = 1"
+  apply (subgoal_tac "x dvd gcd a b")
+  apply simp
+  apply (erule (1) nat_gcd_greatest)
+done
+
+lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
+    x dvd b \<Longrightarrow> abs x = 1"
+  apply (subgoal_tac "x dvd gcd a b")
+  apply simp
+  apply (erule (1) int_gcd_greatest)
+done
+
+lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
+    coprime d e"
+  apply (auto simp add: dvd_def)
+  apply (frule int_coprime_lmult)
+  apply (subst int_gcd_commute)
+  apply (subst (asm) (2) int_gcd_commute)
+  apply (erule int_coprime_lmult)
+done
+
+lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
+apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
+done
+
+lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
+apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
+done
+
+
+subsection {* Bezout's theorem *}
+
+(* Function bezw returns a pair of witnesses to Bezout's theorem --
+   see the theorems that follow the definition. *)
+fun
+  bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
+where
+  "bezw x y =
+  (if y = 0 then (1, 0) else
+      (snd (bezw y (x mod y)),
+       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
+
+lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
+
+lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
+       fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
+  by simp
+
+declare bezw.simps [simp del]
+
+lemma bezw_aux [rule_format]:
+    "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
+proof (induct x y rule: nat_gcd_induct)
+  fix m :: nat
+  show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
+    by auto
+  next fix m :: nat and n
+    assume ngt0: "n > 0" and
+      ih: "fst (bezw n (m mod n)) * int n +
+        snd (bezw n (m mod n)) * int (m mod n) =
+        int (gcd n (m mod n))"
+    thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
+      apply (simp add: bezw_non_0 nat_gcd_non_0)
+      apply (erule subst)
+      apply (simp add: ring_simps)
+      apply (subst mod_div_equality [of m n, symmetric])
+      (* applying simp here undoes the last substitution!
+         what is procedure cancel_div_mod? *)
+      apply (simp only: ring_simps zadd_int [symmetric]
+        zmult_int [symmetric])
+      done
+qed
+
+lemma int_bezout:
+  fixes x y
+  shows "EX u v. u * (x::int) + v * y = gcd x y"
+proof -
+  have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
+      EX u v. u * x + v * y = gcd x y"
+    apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
+    apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
+    apply (unfold gcd_int_def)
+    apply simp
+    apply (subst bezw_aux [symmetric])
+    apply auto
+    done
+  have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
+      (x \<le> 0 \<and> y \<le> 0)"
+    by auto
+  moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
+    by (erule (1) bezout_aux)
+  moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
+    apply (insert bezout_aux [of x "-y"])
+    apply auto
+    apply (rule_tac x = u in exI)
+    apply (rule_tac x = "-v" in exI)
+    apply (subst int_gcd_neg2 [symmetric])
+    apply auto
+    done
+  moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
+    apply (insert bezout_aux [of "-x" y])
+    apply auto
+    apply (rule_tac x = "-u" in exI)
+    apply (rule_tac x = v in exI)
+    apply (subst int_gcd_neg1 [symmetric])
+    apply auto
+    done
+  moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
+    apply (insert bezout_aux [of "-x" "-y"])
+    apply auto
+    apply (rule_tac x = "-u" in exI)
+    apply (rule_tac x = "-v" in exI)
+    apply (subst int_gcd_neg1 [symmetric])
+    apply (subst int_gcd_neg2 [symmetric])
+    apply auto
+    done
+  ultimately show ?thesis by blast
+qed
+
+text {* versions of Bezout for nat, by Amine Chaieb *}
+
+lemma ind_euclid:
+  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
+  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   shows "P a b"
 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
   fix n a b
   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
   have "a = b \<or> a < b \<or> b < a" by arith
   moreover {assume eq: "a= b"
-    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
+    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
+    by simp}
   moreover
   {assume lt: "a < b"
     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
@@ -269,65 +1139,67 @@
 ultimately  show "P a b" by blast
 qed
 
-lemma bezout_lemma: 
-  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)"
-  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)"
-using ex
-apply clarsimp
-apply (rule_tac x="d" in exI, simp add: dvd_add)
-apply (case_tac "a * x = b * y + d" , simp_all)
-apply (rule_tac x="x + y" in exI)
-apply (rule_tac x="y" in exI)
-apply algebra
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="x + y" in exI)
-apply algebra
+lemma nat_bezout_lemma:
+  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)"
+  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)"
+  using ex
+  apply clarsimp
+  apply (rule_tac x="d" in exI, simp add: dvd_add)
+  apply (case_tac "a * x = b * y + d" , simp_all)
+  apply (rule_tac x="x + y" in exI)
+  apply (rule_tac x="y" in exI)
+  apply algebra
+  apply (rule_tac x="x" in exI)
+  apply (rule_tac x="x + y" in exI)
+  apply algebra
 done
 
-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)"
-apply(induct a b rule: ind_euclid)
-apply blast
-apply clarify
-apply (rule_tac x="a" in exI, simp add: dvd_add)
-apply clarsimp
-apply (rule_tac x="d" in exI)
-apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
-apply (rule_tac x="x+y" in exI)
-apply (rule_tac x="y" in exI)
-apply algebra
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="x+y" in exI)
-apply algebra
+lemma nat_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)"
+  apply(induct a b rule: ind_euclid)
+  apply blast
+  apply clarify
+  apply (rule_tac x="a" in exI, simp add: dvd_add)
+  apply clarsimp
+  apply (rule_tac x="d" in exI)
+  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
+  apply (rule_tac x="x+y" in exI)
+  apply (rule_tac x="y" in exI)
+  apply algebra
+  apply (rule_tac x="x" in exI)
+  apply (rule_tac x="x+y" in exI)
+  apply algebra
 done
 
-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)"
-using bezout_add[of a b]
-apply clarsimp
-apply (rule_tac x="d" in exI, simp)
-apply (rule_tac x="x" in exI)
-apply (rule_tac x="y" in exI)
-apply auto
+lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
+    (a * x - b * y = d \<or> b * x - a * y = d)"
+  using nat_bezout_add[of a b]
+  apply clarsimp
+  apply (rule_tac x="d" in exI, simp)
+  apply (rule_tac x="x" in exI)
+  apply (rule_tac x="y" in exI)
+  apply auto
 done
 
-
-text {* We can get a stronger version with a nonzeroness assumption. *}
-lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
-
-lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
+lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
 proof-
-  from nz have ap: "a > 0" by simp
- from bezout_add[of a b] 
- 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
+ from nz have ap: "a > 0" by simp
+ from nat_bezout_add[of a b]
+ 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
  moreover
- {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
-   from H have ?thesis by blast }
+    {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
+     from H have ?thesis by blast }
  moreover
  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
    {assume b0: "b = 0" with H  have ?thesis by simp}
-   moreover 
+   moreover
    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
-     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
+     from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
+       by auto
      moreover
      {assume db: "d=b"
        from prems have ?thesis apply simp
@@ -335,18 +1207,22 @@
 	 apply (rule exI[where x = b])
 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
     moreover
-    {assume db: "d < b" 
+    {assume db: "d < b"
 	{assume "x=0" hence ?thesis  using prems by simp }
 	moreover
 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
-	  
 	  from db have "d \<le> b - 1" by simp
 	  hence "d*b \<le> b*(b - 1)" by simp
 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
-	  from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
+	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
+            by simp
+	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
+	    by (simp only: mult_assoc right_distrib)
+	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
+            by algebra
 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
-	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
+	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
@@ -361,156 +1237,156 @@
  ultimately show ?thesis by blast
 qed
 
-
-lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
-proof-
-  let ?g = "gcd a b"
-  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
-  from d(1,2) have "d dvd ?g" by simp
-  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
-  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
-  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k" 
-    by (algebra add: diff_mult_distrib)
-  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g" 
-    by (simp add: k mult_assoc)
-  thus ?thesis by blast
-qed
-
-lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
+lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
   shows "\<exists>x y. a * x = b * y + gcd a b"
 proof-
   let ?g = "gcd a b"
-  from bezout_add_strong[OF a, of b]
+  from nat_bezout_add_strong[OF a, of b]
   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
   from d(1,2) have "d dvd ?g" by simp
   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
-  from d(3) have "a * x * k = (b * y + d) *k " by algebra
+  from d(3) have "a * x * k = (b * y + d) *k " by auto
   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
   thus ?thesis by blast
 qed
 
-lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
-by(simp add: gcd_mult_distrib2 mult_commute)
+
+subsection {* LCM *}
+
+lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
+  by (simp add: lcm_int_def lcm_nat_def zdiv_int
+    zmult_int [symmetric] gcd_int_def)
+
+lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
+  unfolding lcm_nat_def
+  by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
+
+lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
+  unfolding lcm_int_def gcd_int_def
+  apply (subst int_mult [symmetric])
+  apply (subst nat_prod_gcd_lcm [symmetric])
+  apply (subst nat_abs_mult_distrib [symmetric])
+  apply (simp, simp add: abs_mult)
+done
+
+lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
+  unfolding lcm_nat_def by simp
+
+lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
+  unfolding lcm_int_def by simp
+
+lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
+  unfolding lcm_nat_def by simp
+
+lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
+  unfolding lcm_nat_def by (simp add: One_nat_def)
+
+lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
+  unfolding lcm_int_def by simp
+
+lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
+  unfolding lcm_nat_def by simp
 
-lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  let ?g = "gcd a b"
-  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
-    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
-      by blast
-    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
-    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
-      by (simp only: diff_mult_distrib)
-    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d"
-      by (simp add: k[symmetric] mult_assoc)
-    hence ?lhs by blast}
+lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
+  unfolding lcm_int_def by simp
+
+lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
+  unfolding lcm_nat_def by simp
+
+lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
+  unfolding lcm_nat_def by (simp add: One_nat_def)
+
+lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
+  unfolding lcm_int_def by simp
+
+lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
+  unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
+
+lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
+  unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
+
+(* to do: show lcm is associative, and then declare ac simps *)
+
+lemma nat_lcm_pos:
+  assumes mpos: "(m::nat) > 0"
+  and npos: "n>0"
+  shows "lcm m n > 0"
+proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
+  assume h:"m*n div gcd m n = 0"
+  from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
+  hence gcdp: "gcd m n > 0" by simp
+  with h
+  have "m*n < gcd m n"
+    by (cases "m * n < gcd m n")
+       (auto simp add: div_if[OF gcdp, where m="m*n"])
   moreover
-  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
-    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
-      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
-    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
-    have ?rhs by auto}
-  ultimately show ?thesis by blast
-qed
-
-lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
-proof-
-  let ?g = "gcd a b"
-    have dv: "?g dvd a*x" "?g dvd b * y" 
-      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
-    from dvd_add[OF dv] H
-    show ?thesis by auto
+  have "gcd m n dvd m" by simp
+  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+  with npos have t1:"gcd m n*n \<le> m*n" by simp
+  have "gcd m n \<le> gcd m n*n" using npos by simp
+  with t1 have "gcd m n \<le> m*n" by arith
+  ultimately show "False" by simp
 qed
 
-lemma gcd_mult': "gcd b (a * b) = b"
-by (simp add: gcd_mult mult_commute[of a b]) 
-
-lemma gcd_add: "gcd(a + b) b = gcd a b" 
-  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
-apply (simp_all add: gcd_add1)
-by (simp add: gcd_commute gcd_add1)
-
-lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
-proof-
-  {fix a b assume H: "b \<le> (a::nat)"
-    hence th: "a - b + b = a" by arith
-    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
-  note th = this
-{
-  assume ab: "b \<le> a"
-  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
-next
-  assume ab: "a \<le> b"
-  from th[OF ab] show "gcd a (b - a) = gcd a b" 
-    by (simp add: gcd_commute)}
-qed
-
+lemma int_lcm_pos:
+  assumes mneq0: "(m::int) ~= 0"
+  and npos: "n ~= 0"
+  shows "lcm m n > 0"
 
-subsection {* LCM defined by GCD *}
-
-
-definition
-  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  lcm_def: "lcm m n = m * n div gcd m n"
-
-lemma prod_gcd_lcm:
-  "m * n = gcd m n * lcm m n"
-  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
+  apply (subst int_lcm_abs)
+  apply (rule nat_lcm_pos [transferred])
+  using prems apply auto
+done
 
-lemma lcm_0 [simp]: "lcm m 0 = 0"
-  unfolding lcm_def by simp
-
-lemma lcm_1 [simp]: "lcm m 1 = m"
-  unfolding lcm_def by simp
-
-lemma lcm_0_left [simp]: "lcm 0 n = 0"
-  unfolding lcm_def by simp
-
-lemma lcm_1_left [simp]: "lcm 1 m = m"
-  unfolding lcm_def by simp
-
-lemma dvd_pos:
+lemma nat_dvd_pos:
   fixes n m :: nat
   assumes "n > 0" and "m dvd n"
   shows "m > 0"
 using assms by (cases m) auto
 
-lemma lcm_least:
-  assumes "m dvd k" and "n dvd k"
+lemma nat_lcm_least:
+  assumes "(m::nat) dvd k" and "n dvd k"
   shows "lcm m n dvd k"
 proof (cases k)
   case 0 then show ?thesis by auto
 next
   case (Suc _) then have pos_k: "k > 0" by auto
-  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
-  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
+  from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
+  with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   from pos_k k_m have pos_p: "p > 0" by auto
   from pos_k k_n have pos_q: "q > 0" by auto
   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: mult_ac nat_gcd_mult_distrib)
   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
     by (simp add: k_m [symmetric] k_n [symmetric])
   also have "\<dots> = k * p * q * gcd m n"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: mult_ac nat_gcd_mult_distrib)
   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
     by (simp only: k_m [symmetric] k_n [symmetric])
   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
     by (simp add: mult_ac)
   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
     by simp
-  with prod_gcd_lcm [of m n]
+  with nat_prod_gcd_lcm [of m n]
   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
     by (simp add: mult_ac)
-  with pos_gcd have "lcm m n * gcd q p = k" by simp
+  with pos_gcd have "lcm m n * gcd q p = k" by auto
   then show ?thesis using dvd_def by auto
 qed
 
-lemma lcm_dvd1 [iff]:
-  "m dvd lcm m n"
+lemma int_lcm_least:
+  assumes "(m::int) dvd k" and "n dvd k"
+  shows "lcm m n dvd k"
+
+  apply (subst int_lcm_abs)
+  apply (rule dvd_trans)
+  apply (rule nat_lcm_least [transferred, of _ "abs k" _])
+  using prems apply auto
+done
+
+lemma nat_lcm_dvd1 [iff]: "(m::nat) dvd lcm m n"
 proof (cases m)
   case 0 then show ?thesis by simp
 next
@@ -524,264 +1400,323 @@
     then have npos: "n > 0" by simp
     have "gcd m n dvd n" by simp
     then obtain k where "n = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
-    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
-    finally show ?thesis by (simp add: lcm_def)
-  qed
-qed
-
-lemma lcm_dvd2 [iff]: 
-  "n dvd lcm m n"
-proof (cases n)
-  case 0 then show ?thesis by simp
-next
-  case (Suc _)
-  then have npos: "n > 0" by simp
-  show ?thesis
-  proof (cases m)
-    case 0 then show ?thesis by simp
-  next
-    case (Suc _)
-    then have mpos: "m > 0" by simp
-    have "gcd m n dvd m" by simp
-    then obtain k where "m = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
-    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
-    finally show ?thesis by (simp add: lcm_def)
+    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
+      by (simp add: mult_ac)
+    also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
+    finally show ?thesis by (simp add: lcm_nat_def)
   qed
 qed
 
-lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
-  by (simp add: gcd_commute)
+lemma int_lcm_dvd1 [iff]: "(m::int) dvd lcm m n"
+  apply (subst int_lcm_abs)
+  apply (rule dvd_trans)
+  prefer 2
+  apply (rule nat_lcm_dvd1 [transferred])
+  apply auto
+done
+
+lemma nat_lcm_dvd2 [iff]: "(n::nat) dvd lcm m n"
+  by (subst nat_lcm_commute, rule nat_lcm_dvd1)
+
+lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
+  by (subst int_lcm_commute, rule int_lcm_dvd1)
+
+lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
+    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+  by (auto intro: dvd_anti_sym nat_lcm_least)
 
-lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
-  apply (subgoal_tac "n = m + (n - m)")
-  apply (erule ssubst, rule gcd_add1_eq, simp)  
-  done
+lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
+    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+  by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
+
+lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
+  apply (rule sym)
+  apply (subst nat_lcm_unique [symmetric])
+  apply auto
+done
+
+lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
+  apply (rule sym)
+  apply (subst int_lcm_unique [symmetric])
+  apply auto
+done
+
+lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
+  by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
+
+lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
+  by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
+
 
 
-subsection {* GCD and LCM on integers *}
-
-definition
-  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
+subsection {* Primes *}
 
-lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
-by (simp add: zgcd_def int_dvd_iff)
+(* Is there a better way to handle these, rather than making them
+   elim rules? *)
 
-lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
-by (simp add: zgcd_def int_dvd_iff)
+lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
+  by (unfold prime_nat_def, auto)
 
-lemma zgcd_pos: "zgcd i j \<ge> 0"
-by (simp add: zgcd_def)
+lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
+  by (unfold prime_nat_def, auto)
 
-lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
-by (simp add: zgcd_def gcd_zero)
+lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
+  by (unfold prime_nat_def, auto)
 
-lemma zgcd_commute: "zgcd i j = zgcd j i"
-unfolding zgcd_def by (simp add: gcd_commute)
+lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
+  by (unfold prime_nat_def, auto)
 
-lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
-unfolding zgcd_def by simp
+lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
+  by (unfold prime_nat_def, auto)
 
-lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
-unfolding zgcd_def by simp
+lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
+  by (unfold prime_nat_def, auto)
+
+lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
+  by (unfold prime_nat_def, auto)
+
+lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
+  by (unfold prime_int_def prime_nat_def, auto)
 
-  (* should be solved by algebra*)
-lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
-  unfolding zgcd_def
-proof -
-  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
-  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
-  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
-  have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
-    unfolding dvd_def
-    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
-  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
-    unfolding dvd_def by blast
-  from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
-  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
-  then show ?thesis
-    apply (subst abs_dvd_iff [symmetric])
-    apply (subst dvd_abs_iff [symmetric])
-    apply (unfold dvd_def)
-    apply (rule_tac x = "int h'" in exI, simp)
-    done
-qed
+lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
+  by (unfold prime_int_def prime_nat_def, auto)
 
-lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
+lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
+  by (unfold prime_int_def prime_nat_def, auto)
 
-lemma zgcd_greatest:
-  assumes "k dvd m" and "k dvd n"
-  shows "k dvd zgcd m n"
-proof -
-  let ?k' = "nat \<bar>k\<bar>"
-  let ?m' = "nat \<bar>m\<bar>"
-  let ?n' = "nat \<bar>n\<bar>"
-  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
-    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
-  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
-    unfolding zgcd_def by (simp only: zdvd_int)
-  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
-  then show "k dvd zgcd m n" by simp
-qed
+thm prime_nat_def;
+thm prime_nat_def [transferred];
+
+lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
+    m = 1 \<or> m = p))"
+  using prime_nat_def [transferred]
+    apply (case_tac "p >= 0")
+    by (blast, auto simp add: int_prime_ge_0)
+
+(* To do: determine primality of any numeral *)
+
+lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
+  by (simp add: prime_nat_def)
+
+lemma int_zero_not_prime [simp]: "~prime (0::int)"
+  by (simp add: prime_int_def)
+
+lemma nat_one_not_prime [simp]: "~prime (1::nat)"
+  by (simp add: prime_nat_def)
 
-lemma div_zgcd_relprime:
-  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
-  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
-proof -
-  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
-  let ?g = "zgcd a b"
-  let ?a' = "a div ?g"
-  let ?b' = "b div ?g"
-  let ?g' = "zgcd ?a' ?b'"
-  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
-  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
-  from dvdg dvdg' obtain ka kb ka' kb' where
-   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
-    unfolding dvd_def by blast
-  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
-  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
-      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0" using nz by simp
-  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
-  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
-  with zgcd_pos show "?g' = 1" by simp
-qed
+lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
+  by (simp add: prime_nat_def One_nat_def)
+
+lemma int_one_not_prime [simp]: "~prime (1::int)"
+  by (simp add: prime_int_def)
+
+lemma nat_two_is_prime [simp]: "prime (2::nat)"
+  apply (auto simp add: prime_nat_def)
+  apply (case_tac m)
+  apply (auto dest!: dvd_imp_le)
+  done
 
-lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
-  by (simp add: zgcd_def abs_if)
-
-lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
-  by (simp add: zgcd_def abs_if)
+lemma int_two_is_prime [simp]: "prime (2::int)"
+  by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
 
-lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
-  apply (frule_tac b = n and a = m in pos_mod_sign)
-  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
-  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
-  apply (frule_tac a = m in pos_mod_bound)
-  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+  apply (unfold prime_nat_def)
+  apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
+  done
+
+lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+  apply (unfold prime_int_altdef)
+  apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
   done
 
-lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
-  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
-  apply (auto simp add: linorder_neq_iff zgcd_non_0)
-  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
-  done
+lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+  by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
+
+lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+  by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
+
+lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
+    p dvd m * n = (p dvd m \<or> p dvd n)"
+  by (rule iffI, rule nat_prime_dvd_mult, auto)
 
-lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
-  by (simp add: zgcd_def abs_if)
+lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
+    p dvd m * n = (p dvd m \<or> p dvd n)"
+  by (rule iffI, rule int_prime_dvd_mult, auto)
 
-lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
-  by (simp add: zgcd_def abs_if)
-
-lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
-  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
+lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
+  unfolding prime_nat_def dvd_def apply auto
+  apply (subgoal_tac "k > 1")
+  apply force
+  apply (subgoal_tac "k ~= 0")
+  apply force
+  apply (rule notI)
+  apply force
+done
 
-lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
-  by (simp add: zgcd_def gcd_1_left)
-
-lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
-  by (simp add: zgcd_def gcd_assoc)
+(* there's a lot of messing around with signs of products here --
+   could this be made more automatic? *)
+lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
+  unfolding prime_int_altdef dvd_def
+  apply auto
+  apply (rule_tac x = m in exI)
+  apply (rule_tac x = k in exI)
+  apply (auto simp add: mult_compare_simps)
+  apply (subgoal_tac "k > 0")
+  apply arith
+  apply (case_tac "k <= 0")
+  apply (subgoal_tac "m * k <= 0")
+  apply force
+  apply (subst zero_compare_simps(8))
+  apply auto
+  apply (subgoal_tac "m * k <= 0")
+  apply force
+  apply (subst zero_compare_simps(8))
+  apply auto
+done
 
-lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
-  apply (rule zgcd_commute [THEN trans])
-  apply (rule zgcd_assoc [THEN trans])
-  apply (rule zgcd_commute [THEN arg_cong])
-  done
+lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
+    n > 0 --> (p dvd x^n --> p dvd x)"
+  by (induct n rule: nat_induct, auto)
 
-lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
-  -- {* addition is an AC-operator *}
+lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
+    n > 0 --> (p dvd x^n --> p dvd x)"
+  apply (induct n rule: nat_induct, auto)
+  apply (frule int_prime_ge_0)
+  apply auto
+done
+
+lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
+    coprime a (p^m)"
+  apply (rule nat_coprime_exp)
+  apply (subst nat_gcd_commute)
+  apply (erule (1) nat_prime_imp_coprime)
+done
 
-lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
-  by (simp del: minus_mult_right [symmetric]
-      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
-          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
+    coprime a (p^m)"
+  apply (rule int_coprime_exp)
+  apply (subst int_gcd_commute)
+  apply (erule (1) int_prime_imp_coprime)
+done
 
-lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
-  by (simp add: abs_if zgcd_zmult_distrib2)
+lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+  apply (rule nat_prime_imp_coprime, assumption)
+  apply (unfold prime_nat_def, auto)
+done
 
-lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
-  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
+lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+  apply (rule int_prime_imp_coprime, assumption)
+  apply (unfold prime_int_altdef, clarify)
+  apply (drule_tac x = q in spec)
+  apply (drule_tac x = p in spec)
+  apply auto
+done
 
-lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
-  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
+lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
+    coprime (p^m) (q^n)"
+  by (rule nat_coprime_exp2, rule nat_primes_coprime)
 
-lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
-  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
+lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
+    coprime (p^m) (q^n)"
+  by (rule int_coprime_exp2, rule int_primes_coprime)
 
-
-definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
+lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
+  apply (induct n rule: nat_less_induct)
+  apply (case_tac "n = 0")
+  using nat_two_is_prime apply blast
+  apply (case_tac "prime n")
+  apply blast
+  apply (subgoal_tac "n > 1")
+  apply (frule (1) nat_not_prime_eq_prod)
+  apply (auto intro: dvd_mult dvd_mult2)
+done
 
-lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
-by(simp add:zlcm_def dvd_int_iff)
+(* An Isar version:
+
+lemma nat_prime_factor_b:
+  fixes n :: nat
+  assumes "n \<noteq> 1"
+  shows "\<exists>p. prime p \<and> p dvd n"
 
-lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
-by(simp add:zlcm_def dvd_int_iff)
-
-
-lemma dvd_imp_dvd_zlcm1:
-  assumes "k dvd i" shows "k dvd (zlcm i j)"
-proof -
-  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
-    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
-  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
+using `n ~= 1`
+proof (induct n rule: nat_less_induct)
+  fix n :: nat
+  assume "n ~= 1" and
+    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
+  thus "\<exists>p. prime p \<and> p dvd n"
+  proof -
+  {
+    assume "n = 0"
+    moreover note nat_two_is_prime
+    ultimately have ?thesis
+      by (auto simp del: nat_two_is_prime)
+  }
+  moreover
+  {
+    assume "prime n"
+    hence ?thesis by auto
+  }
+  moreover
+  {
+    assume "n ~= 0" and "~ prime n"
+    with `n ~= 1` have "n > 1" by auto
+    with `~ prime n` and nat_not_prime_eq_prod obtain m k where
+      "n = m * k" and "1 < m" and "m < n" by blast
+    with ih obtain p where "prime p" and "p dvd m" by blast
+    with `n = m * k` have ?thesis by auto
+  }
+  ultimately show ?thesis by blast
+  qed
 qed
 
-lemma dvd_imp_dvd_zlcm2:
-  assumes "k dvd j" shows "k dvd (zlcm i j)"
-proof -
-  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
-    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
-  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
+*)
+
+text {* One property of coprimality is easier to prove via prime factors. *}
+
+lemma nat_prime_divprod_pow:
+  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
+  shows "p^n dvd a \<or> p^n dvd b"
+proof-
+  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
+      apply (cases "n=0", simp_all)
+      apply (cases "a=1", simp_all) done}
+  moreover
+  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
+    then obtain m where m: "n = Suc m" by (cases n, auto)
+    from n have "p dvd p^n" by (intro dvd_power, auto)
+    also note pab
+    finally have pab': "p dvd a * b".
+    from nat_prime_dvd_mult[OF p pab']
+    have "p dvd a \<or> p dvd b" .
+    moreover
+    {assume pa: "p dvd a"
+      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+      from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
+      with p have "coprime b p"
+        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
+      hence pnb: "coprime (p^n) b"
+        by (subst nat_gcd_commute, rule nat_coprime_exp)
+      from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
+    moreover
+    {assume pb: "p dvd b"
+      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+      from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
+        by auto
+      with p have "coprime a p"
+        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
+      hence pna: "coprime (p^n) a"
+        by (subst nat_gcd_commute, rule nat_coprime_exp)
+      from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
+    ultimately have ?thesis by blast}
+  ultimately show ?thesis by blast
 qed
 
-
-lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
-by (case_tac "d <0", simp_all)
-
-lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
-by (case_tac "d<0", simp_all)
-
-(* lcm a b is positive for positive a and b *)
-
-lemma lcm_pos: 
-  assumes mpos: "m > 0"
-  and npos: "n>0"
-  shows "lcm m n > 0"
-proof(rule ccontr, simp add: lcm_def gcd_zero)
-assume h:"m*n div gcd m n = 0"
-from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
-hence gcdp: "gcd m n > 0" by simp
-with h
-have "m*n < gcd m n"
-  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
-moreover 
-have "gcd m n dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n *n \<le> m*n" by simp
- have "gcd m n \<le> gcd m n*n" using npos by simp
- with t1 have "gcd m n \<le> m*n" by arith
-ultimately show "False" by simp
-qed
-
-lemma zlcm_pos: 
-  assumes anz: "a \<noteq> 0"
-  and bnz: "b \<noteq> 0" 
-  shows "0 < zlcm a b"
-proof-
-  let ?na = "nat (abs a)"
-  let ?nb = "nat (abs b)"
-  have nap: "?na >0" using anz by simp
-  have nbp: "?nb >0" using bnz by simp
-  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
-  thus ?thesis by (simp add: zlcm_def)
-qed
-
-lemma zgcd_code [code]:
-  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
-  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
-
 end
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 18 07:51:15 2009 -0700
@@ -284,6 +284,7 @@
   Ln.thy \
   Log.thy \
   MacLaurin.thy \
+  NatTransfer.thy \
   NthRoot.thy \
   SEQ.thy \
   Series.thy \
@@ -300,6 +301,7 @@
   Real.thy \
   RealVector.thy \
   Tools/float_syntax.ML \
+  Tools/transfer_data.ML \
   Tools/Qelim/ferrante_rackoff_data.ML \
   Tools/Qelim/ferrante_rackoff.ML \
   Tools/Qelim/langford_data.ML \
@@ -325,6 +327,7 @@
   Library/FrechetDeriv.thy \
   Library/Fundamental_Theorem_Algebra.thy \
   Library/Inner_Product.thy Library/Lattice_Syntax.thy \
+  Library/Legacy_GCD.thy \
   Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
   Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
   Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -21,17 +21,17 @@
 definition
   isnormNum :: "Num \<Rightarrow> bool"
 where
-  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> zgcd a b = 1))"
+  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
 
 definition
   normNum :: "Num \<Rightarrow> Num"
 where
   "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
-  (let g = zgcd a b 
+  (let g = gcd a b 
    in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
 
-declare zgcd_zdvd1[presburger] 
-declare zgcd_zdvd2[presburger]
+declare int_gcd_dvd1[presburger]
+declare int_gcd_dvd2[presburger]
 lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
 proof -
   have " \<exists> a b. x = (a,b)" by auto
@@ -39,19 +39,19 @@
   {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
   moreover
   {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
-    let ?g = "zgcd a b"
+    let ?g = "gcd a b"
     let ?a' = "a div ?g"
     let ?b' = "b div ?g"
-    let ?g' = "zgcd ?a' ?b'"
-    from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
+    let ?g' = "gcd ?a' ?b'"
+    from anz bnz have "?g \<noteq> 0" by simp  with int_gcd_ge_0[of a b] 
     have gpos: "?g > 0"  by arith
     have gdvd: "?g dvd a" "?g dvd b" by arith+ 
     from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
     anz bnz
-    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
-      by - (rule notI,simp add:zgcd_def)+
+    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
+      by - (rule notI, simp)+
     from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
-    from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
+    from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
     from bnz have "b < 0 \<or> b > 0" by arith
     moreover
     {assume b: "b > 0"
@@ -67,7 +67,7 @@
 	have False using b by arith }
       hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
       from anz bnz nz' b b' gp1 have ?thesis 
-	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
+	by (simp add: isnormNum_def normNum_def Let_def split_def)}
     ultimately have ?thesis by blast
   }
   ultimately show ?thesis by blast
@@ -85,7 +85,7 @@
 definition
   Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
 where
-  "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b') 
+  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') 
     in (a*a' div g, b*b' div g))"
 
 definition
@@ -121,11 +121,11 @@
   then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
   {assume "a = 0"
     hence ?thesis using xn ab ab'
-      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
+      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
   moreover
   {assume "a' = 0"
     hence ?thesis using yn ab ab' 
-      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
+      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
   moreover
   {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
     hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
@@ -137,11 +137,11 @@
 
 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   by (simp add: Ninv_def isnormNum_def split_def)
-    (cases "fst x = 0", auto simp add: zgcd_commute)
+    (cases "fst x = 0", auto simp add: int_gcd_commute)
 
 lemma isnormNum_int[simp]: 
   "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
-  by (simp_all add: isnormNum_def zgcd_def)
+  by (simp_all add: isnormNum_def)
 
 
 text {* Relations over Num *}
@@ -202,8 +202,8 @@
     from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
     from prems have eq:"a * b' = a'*b" 
       by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
-    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
-      by (simp_all add: isnormNum_def add: zgcd_commute)
+    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
+      by (simp_all add: isnormNum_def add: int_gcd_commute)
     from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
       apply - 
       apply algebra
@@ -211,8 +211,8 @@
       apply simp
       apply algebra
       done
-    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
-      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
+    from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
+      int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
       have eq1: "b = b'" using pos by arith  
       with eq have "a = a'" using pos by simp
       with eq1 have ?rhs by simp}
@@ -258,7 +258,7 @@
       by (simp add: INum_def normNum_def split_def Let_def)}
   moreover 
   {assume a: "a\<noteq>0" and b: "b\<noteq>0"
-    let ?g = "zgcd a b"
+    let ?g = "gcd a b"
     from a b have g: "?g \<noteq> 0"by simp
     from of_int_div[OF g, where ?'a = 'a]
     have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
@@ -294,11 +294,11 @@
       from z aa' bb' have ?thesis 
 	by (simp add: th Nadd_def normNum_def INum_def split_def)}
     moreover {assume z: "a * b' + b * a' \<noteq> 0"
-      let ?g = "zgcd (a * b' + b * a') (b*b')"
+      let ?g = "gcd (a * b' + b * a') (b*b')"
       have gz: "?g \<noteq> 0" using z by simp
       have ?thesis using aa' bb' z gz
-	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,
-	OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
+	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,
+	OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
 	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
     ultimately have ?thesis using aa' bb' 
       by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
@@ -317,10 +317,10 @@
       done }
   moreover
   {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
-    let ?g="zgcd (a*a') (b*b')"
+    let ?g="gcd (a*a') (b*b')"
     have gz: "?g \<noteq> 0" using z by simp
-    from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]] 
-      of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]] 
+    from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]] 
+      of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]] 
     have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   ultimately show ?thesis by blast
 qed
@@ -478,7 +478,7 @@
 qed
 
 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
-  by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
+  by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
 
 lemma Nmul_assoc:
   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Library/Legacy_GCD.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Legacy_GCD.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -0,0 +1,787 @@
+(*  Title:      HOL/GCD.thy
+    Author:     Christophe Tabacznyj and Lawrence C Paulson
+    Copyright   1996  University of Cambridge
+*)
+
+header {* The Greatest Common Divisor *}
+
+theory Legacy_GCD
+imports Main
+begin
+
+text {*
+  See \cite{davenport92}. \bigskip
+*}
+
+subsection {* Specification of GCD on nats *}
+
+definition
+  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
+  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
+
+text {* Uniqueness *}
+
+lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
+  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
+
+text {* Connection to divides relation *}
+
+lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
+  by (auto simp add: is_gcd_def)
+
+text {* Commutativity *}
+
+lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
+  by (auto simp add: is_gcd_def)
+
+
+subsection {* GCD on nat by Euclid's algorithm *}
+
+fun
+  gcd  :: "nat => nat => nat"
+where
+  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+lemma gcd_induct [case_names "0" rec]:
+  fixes m n :: nat
+  assumes "\<And>m. P m 0"
+    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
+  shows "P m n"
+proof (induct m n rule: gcd.induct)
+  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
+qed
+
+lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
+  by simp
+
+lemma gcd_0_left [simp,algebra]: "gcd 0 m = m"
+  by simp
+
+lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
+  by simp
+
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
+  by simp
+
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+  unfolding One_nat_def by (rule gcd_1)
+
+declare gcd.simps [simp del]
+
+text {*
+  \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
+  conjunctions don't seem provable separately.
+*}
+
+lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
+  and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
+  apply (induct m n rule: gcd_induct)
+     apply (simp_all add: gcd_non_0)
+  apply (blast dest: dvd_mod_imp_dvd)
+  done
+
+text {*
+  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
+  naturals, if @{term k} divides @{term m} and @{term k} divides
+  @{term n} then @{term k} divides @{term "gcd m n"}.
+*}
+
+lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
+  by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
+
+text {*
+  \medskip Function gcd yields the Greatest Common Divisor.
+*}
+
+lemma is_gcd: "is_gcd m n (gcd m n) "
+  by (simp add: is_gcd_def gcd_greatest)
+
+
+subsection {* Derived laws for GCD *}
+
+lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
+  by (blast intro!: gcd_greatest intro: dvd_trans)
+
+lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
+  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
+
+lemma gcd_commute: "gcd m n = gcd n m"
+  apply (rule is_gcd_unique)
+   apply (rule is_gcd)
+  apply (subst is_gcd_commute)
+  apply (simp add: is_gcd)
+  done
+
+lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
+  apply (rule is_gcd_unique)
+   apply (rule is_gcd)
+  apply (simp add: is_gcd_def)
+  apply (blast intro: dvd_trans)
+  done
+
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
+  by (simp add: gcd_commute)
+
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+  unfolding One_nat_def by (rule gcd_1_left)
+
+text {*
+  \medskip Multiplication laws
+*}
+
+lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
+    -- {* \cite[page 27]{davenport92} *}
+  apply (induct m n rule: gcd_induct)
+   apply simp
+  apply (case_tac "k = 0")
+   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
+  done
+
+lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
+  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
+  done
+
+lemma gcd_self [simp, algebra]: "gcd k k = k"
+  apply (rule gcd_mult [of k 1, simplified])
+  done
+
+lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
+  apply (insert gcd_mult_distrib2 [of m k n])
+  apply simp
+  apply (erule_tac t = m in ssubst)
+  apply simp
+  done
+
+lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
+  by (auto intro: relprime_dvd_mult dvd_mult2)
+
+lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
+  apply (rule dvd_anti_sym)
+   apply (rule gcd_greatest)
+    apply (rule_tac n = k in relprime_dvd_mult)
+     apply (simp add: gcd_assoc)
+     apply (simp add: gcd_commute)
+    apply (simp_all add: mult_commute)
+  done
+
+
+text {* \medskip Addition laws *}
+
+lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
+  by (cases "n = 0") (auto simp add: gcd_non_0)
+
+lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n"
+proof -
+  have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
+  also have "... = gcd (n + m) m" by (simp add: add_commute)
+  also have "... = gcd n m" by simp
+  also have  "... = gcd m n" by (rule gcd_commute)
+  finally show ?thesis .
+qed
+
+lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n"
+  apply (subst add_commute)
+  apply (rule gcd_add2)
+  done
+
+lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n"
+  by (induct k) (simp_all add: add_assoc)
+
+lemma gcd_dvd_prod: "gcd m n dvd m * n" 
+  using mult_dvd_mono [of 1] by auto
+
+text {*
+  \medskip Division by gcd yields rrelatively primes.
+*}
+
+lemma div_gcd_relprime:
+  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
+  shows "gcd (a div gcd a b) (b div gcd a b) = 1"
+proof -
+  let ?g = "gcd a b"
+  let ?a' = "a div ?g"
+  let ?b' = "b div ?g"
+  let ?g' = "gcd ?a' ?b'"
+  have dvdg: "?g dvd a" "?g dvd b" by simp_all
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
+  from dvdg dvdg' obtain ka kb ka' kb' where
+      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
+    unfolding dvd_def by blast
+  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
+  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
+    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
+      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+  have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
+  then have gp: "?g > 0" by simp
+  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
+qed
+
+
+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"
+proof(auto)
+  assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
+  from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
+  have th: "gcd a b dvd d" by blast
+  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
+qed
+
+lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
+  shows "gcd x y = gcd u v"
+proof-
+  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
+  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
+qed
+
+lemma ind_euclid: 
+  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
+  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
+  shows "P a b"
+proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
+  fix n a b
+  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
+  have "a = b \<or> a < b \<or> b < a" by arith
+  moreover {assume eq: "a= b"
+    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
+  moreover
+  {assume lt: "a < b"
+    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
+    moreover
+    {assume "a =0" with z c have "P a b" by blast }
+    moreover
+    {assume ab: "a + b - a < n"
+      have th0: "a + b - a = a + (b - a)" using lt by arith
+      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
+      have "P a b" by (simp add: th0[symmetric])}
+    ultimately have "P a b" by blast}
+  moreover
+  {assume lt: "a > b"
+    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
+    moreover
+    {assume "b =0" with z c have "P a b" by blast }
+    moreover
+    {assume ab: "b + a - b < n"
+      have th0: "b + a - b = b + (a - b)" using lt by arith
+      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
+      have "P b a" by (simp add: th0[symmetric])
+      hence "P a b" using c by blast }
+    ultimately have "P a b" by blast}
+ultimately  show "P a b" by blast
+qed
+
+lemma bezout_lemma: 
+  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)"
+  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)"
+using ex
+apply clarsimp
+apply (rule_tac x="d" in exI, simp add: dvd_add)
+apply (case_tac "a * x = b * y + d" , simp_all)
+apply (rule_tac x="x + y" in exI)
+apply (rule_tac x="y" in exI)
+apply algebra
+apply (rule_tac x="x" in exI)
+apply (rule_tac x="x + y" in exI)
+apply algebra
+done
+
+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)"
+apply(induct a b rule: ind_euclid)
+apply blast
+apply clarify
+apply (rule_tac x="a" in exI, simp add: dvd_add)
+apply clarsimp
+apply (rule_tac x="d" in exI)
+apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
+apply (rule_tac x="x+y" in exI)
+apply (rule_tac x="y" in exI)
+apply algebra
+apply (rule_tac x="x" in exI)
+apply (rule_tac x="x+y" in exI)
+apply algebra
+done
+
+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)"
+using bezout_add[of a b]
+apply clarsimp
+apply (rule_tac x="d" in exI, simp)
+apply (rule_tac x="x" in exI)
+apply (rule_tac x="y" in exI)
+apply auto
+done
+
+
+text {* We can get a stronger version with a nonzeroness assumption. *}
+lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
+
+lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
+  shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
+proof-
+  from nz have ap: "a > 0" by simp
+ from bezout_add[of a b] 
+ 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
+ moreover
+ {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
+   from H have ?thesis by blast }
+ moreover
+ {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
+   {assume b0: "b = 0" with H  have ?thesis by simp}
+   moreover 
+   {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
+     from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
+     moreover
+     {assume db: "d=b"
+       from prems have ?thesis apply simp
+	 apply (rule exI[where x = b], simp)
+	 apply (rule exI[where x = b])
+	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
+    moreover
+    {assume db: "d < b" 
+	{assume "x=0" hence ?thesis  using prems by simp }
+	moreover
+	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
+	  
+	  from db have "d \<le> b - 1" by simp
+	  hence "d*b \<le> b*(b - 1)" by simp
+	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
+	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
+	  from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
+	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
+	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
+	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
+	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
+	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
+	  hence ?thesis using H(1,2)
+	    apply -
+	    apply (rule exI[where x=d], simp)
+	    apply (rule exI[where x="(b - 1) * y"])
+	    by (rule exI[where x="x*(b - 1) - d"], simp)}
+	ultimately have ?thesis by blast}
+    ultimately have ?thesis by blast}
+  ultimately have ?thesis by blast}
+ ultimately show ?thesis by blast
+qed
+
+
+lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
+proof-
+  let ?g = "gcd a b"
+  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
+  from d(1,2) have "d dvd ?g" by simp
+  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
+  from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
+  hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k" 
+    by (algebra add: diff_mult_distrib)
+  hence "a * (x * k) - b * (y*k) = ?g \<or> b * (x * k) - a * (y*k) = ?g" 
+    by (simp add: k mult_assoc)
+  thus ?thesis by blast
+qed
+
+lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
+  shows "\<exists>x y. a * x = b * y + gcd a b"
+proof-
+  let ?g = "gcd a b"
+  from bezout_add_strong[OF a, of b]
+  obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
+  from d(1,2) have "d dvd ?g" by simp
+  then obtain k where k: "?g = d*k" unfolding dvd_def by blast
+  from d(3) have "a * x * k = (b * y + d) *k " by algebra
+  hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
+  thus ?thesis by blast
+qed
+
+lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * gcd a b"
+by(simp add: gcd_mult_distrib2 mult_commute)
+
+lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof-
+  let ?g = "gcd a b"
+  {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
+    from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
+      by blast
+    hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
+    hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 
+      by (simp only: diff_mult_distrib)
+    hence "a * (x*k) - b * (y*k) = d \<or> b * (x * k) - a * (y*k) = d"
+      by (simp add: k[symmetric] mult_assoc)
+    hence ?lhs by blast}
+  moreover
+  {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
+    have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
+      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
+    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
+    have ?rhs by auto}
+  ultimately show ?thesis by blast
+qed
+
+lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
+proof-
+  let ?g = "gcd a b"
+    have dv: "?g dvd a*x" "?g dvd b * y" 
+      using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
+    from dvd_add[OF dv] H
+    show ?thesis by auto
+qed
+
+lemma gcd_mult': "gcd b (a * b) = b"
+by (simp add: gcd_mult mult_commute[of a b]) 
+
+lemma gcd_add: "gcd(a + b) b = gcd a b" 
+  "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
+apply (simp_all add: gcd_add1)
+by (simp add: gcd_commute gcd_add1)
+
+lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
+proof-
+  {fix a b assume H: "b \<le> (a::nat)"
+    hence th: "a - b + b = a" by arith
+    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b) b = gcd a b" by simp}
+  note th = this
+{
+  assume ab: "b \<le> a"
+  from th[OF ab] show "gcd (a - b)  b = gcd a b" by blast
+next
+  assume ab: "a \<le> b"
+  from th[OF ab] show "gcd a (b - a) = gcd a b" 
+    by (simp add: gcd_commute)}
+qed
+
+
+subsection {* LCM defined by GCD *}
+
+
+definition
+  lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  lcm_def: "lcm m n = m * n div gcd m n"
+
+lemma prod_gcd_lcm:
+  "m * n = gcd m n * lcm m n"
+  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
+
+lemma lcm_0 [simp]: "lcm m 0 = 0"
+  unfolding lcm_def by simp
+
+lemma lcm_1 [simp]: "lcm m 1 = m"
+  unfolding lcm_def by simp
+
+lemma lcm_0_left [simp]: "lcm 0 n = 0"
+  unfolding lcm_def by simp
+
+lemma lcm_1_left [simp]: "lcm 1 m = m"
+  unfolding lcm_def by simp
+
+lemma dvd_pos:
+  fixes n m :: nat
+  assumes "n > 0" and "m dvd n"
+  shows "m > 0"
+using assms by (cases m) auto
+
+lemma lcm_least:
+  assumes "m dvd k" and "n dvd k"
+  shows "lcm m n dvd k"
+proof (cases k)
+  case 0 then show ?thesis by auto
+next
+  case (Suc _) then have pos_k: "k > 0" by auto
+  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
+  with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
+  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
+  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
+  from pos_k k_m have pos_p: "p > 0" by auto
+  from pos_k k_n have pos_q: "q > 0" by auto
+  have "k * k * gcd q p = k * gcd (k * q) (k * p)"
+    by (simp add: mult_ac gcd_mult_distrib2)
+  also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
+    by (simp add: k_m [symmetric] k_n [symmetric])
+  also have "\<dots> = k * p * q * gcd m n"
+    by (simp add: mult_ac gcd_mult_distrib2)
+  finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
+    by (simp only: k_m [symmetric] k_n [symmetric])
+  then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
+    by (simp add: mult_ac)
+  with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
+    by simp
+  with prod_gcd_lcm [of m n]
+  have "lcm m n * gcd q p * gcd m n = k * gcd m n"
+    by (simp add: mult_ac)
+  with pos_gcd have "lcm m n * gcd q p = k" by simp
+  then show ?thesis using dvd_def by auto
+qed
+
+lemma lcm_dvd1 [iff]:
+  "m dvd lcm m n"
+proof (cases m)
+  case 0 then show ?thesis by simp
+next
+  case (Suc _)
+  then have mpos: "m > 0" by simp
+  show ?thesis
+  proof (cases n)
+    case 0 then show ?thesis by simp
+  next
+    case (Suc _)
+    then have npos: "n > 0" by simp
+    have "gcd m n dvd n" by simp
+    then obtain k where "n = gcd m n * k" using dvd_def by auto
+    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
+    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
+    finally show ?thesis by (simp add: lcm_def)
+  qed
+qed
+
+lemma lcm_dvd2 [iff]: 
+  "n dvd lcm m n"
+proof (cases n)
+  case 0 then show ?thesis by simp
+next
+  case (Suc _)
+  then have npos: "n > 0" by simp
+  show ?thesis
+  proof (cases m)
+    case 0 then show ?thesis by simp
+  next
+    case (Suc _)
+    then have mpos: "m > 0" by simp
+    have "gcd m n dvd m" by simp
+    then obtain k where "m = gcd m n * k" using dvd_def by auto
+    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
+    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
+    finally show ?thesis by (simp add: lcm_def)
+  qed
+qed
+
+lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
+  by (simp add: gcd_commute)
+
+lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
+  apply (subgoal_tac "n = m + (n - m)")
+  apply (erule ssubst, rule gcd_add1_eq, simp)  
+  done
+
+
+subsection {* GCD and LCM on integers *}
+
+definition
+  zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
+  "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
+
+lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
+by (simp add: zgcd_def int_dvd_iff)
+
+lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
+by (simp add: zgcd_def int_dvd_iff)
+
+lemma zgcd_pos: "zgcd i j \<ge> 0"
+by (simp add: zgcd_def)
+
+lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
+by (simp add: zgcd_def gcd_zero)
+
+lemma zgcd_commute: "zgcd i j = zgcd j i"
+unfolding zgcd_def by (simp add: gcd_commute)
+
+lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
+unfolding zgcd_def by simp
+
+lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
+unfolding zgcd_def by simp
+
+  (* should be solved by algebra*)
+lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
+  unfolding zgcd_def
+proof -
+  assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
+  then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
+  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
+  have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
+    unfolding dvd_def
+    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
+  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
+    unfolding dvd_def by blast
+  from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
+  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
+  then show ?thesis
+    apply (subst abs_dvd_iff [symmetric])
+    apply (subst dvd_abs_iff [symmetric])
+    apply (unfold dvd_def)
+    apply (rule_tac x = "int h'" in exI, simp)
+    done
+qed
+
+lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
+
+lemma zgcd_greatest:
+  assumes "k dvd m" and "k dvd n"
+  shows "k dvd zgcd m n"
+proof -
+  let ?k' = "nat \<bar>k\<bar>"
+  let ?m' = "nat \<bar>m\<bar>"
+  let ?n' = "nat \<bar>n\<bar>"
+  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
+    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
+  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
+    unfolding zgcd_def by (simp only: zdvd_int)
+  then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
+  then show "k dvd zgcd m n" by simp
+qed
+
+lemma div_zgcd_relprime:
+  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
+  shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
+proof -
+  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
+  let ?g = "zgcd a b"
+  let ?a' = "a div ?g"
+  let ?b' = "b div ?g"
+  let ?g' = "zgcd ?a' ?b'"
+  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
+  from dvdg dvdg' obtain ka kb ka' kb' where
+   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
+    unfolding dvd_def by blast
+  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
+  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
+    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
+      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+  have "?g \<noteq> 0" using nz by simp
+  then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
+  from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
+  with zgcd_pos show "?g' = 1" by simp
+qed
+
+lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
+  apply (frule_tac b = n and a = m in pos_mod_sign)
+  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
+  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
+  apply (frule_tac a = m in pos_mod_bound)
+  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  done
+
+lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
+  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
+  apply (auto simp add: linorder_neq_iff zgcd_non_0)
+  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
+  done
+
+lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
+  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
+
+lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
+  by (simp add: zgcd_def gcd_1_left)
+
+lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
+  by (simp add: zgcd_def gcd_assoc)
+
+lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
+  apply (rule zgcd_commute [THEN trans])
+  apply (rule zgcd_assoc [THEN trans])
+  apply (rule zgcd_commute [THEN arg_cong])
+  done
+
+lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
+  -- {* addition is an AC-operator *}
+
+lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
+  by (simp del: minus_mult_right [symmetric]
+      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
+          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+
+lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
+  by (simp add: abs_if zgcd_zmult_distrib2)
+
+lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
+  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
+
+lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
+  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
+
+lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
+  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
+
+
+definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
+
+lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
+by(simp add:zlcm_def dvd_int_iff)
+
+lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j"
+by(simp add:zlcm_def dvd_int_iff)
+
+
+lemma dvd_imp_dvd_zlcm1:
+  assumes "k dvd i" shows "k dvd (zlcm i j)"
+proof -
+  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
+  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
+qed
+
+lemma dvd_imp_dvd_zlcm2:
+  assumes "k dvd j" shows "k dvd (zlcm i j)"
+proof -
+  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
+  thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
+qed
+
+
+lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
+by (case_tac "d <0", simp_all)
+
+lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
+by (case_tac "d<0", simp_all)
+
+(* lcm a b is positive for positive a and b *)
+
+lemma lcm_pos: 
+  assumes mpos: "m > 0"
+  and npos: "n>0"
+  shows "lcm m n > 0"
+proof(rule ccontr, simp add: lcm_def gcd_zero)
+assume h:"m*n div gcd m n = 0"
+from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
+hence gcdp: "gcd m n > 0" by simp
+with h
+have "m*n < gcd m n"
+  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
+moreover 
+have "gcd m n dvd m" by simp
+ with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+ with npos have t1:"gcd m n *n \<le> m*n" by simp
+ have "gcd m n \<le> gcd m n*n" using npos by simp
+ with t1 have "gcd m n \<le> m*n" by arith
+ultimately show "False" by simp
+qed
+
+lemma zlcm_pos: 
+  assumes anz: "a \<noteq> 0"
+  and bnz: "b \<noteq> 0" 
+  shows "0 < zlcm a b"
+proof-
+  let ?na = "nat (abs a)"
+  let ?nb = "nat (abs b)"
+  have nap: "?na >0" using anz by simp
+  have nbp: "?nb >0" using bnz by simp
+  have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
+  thus ?thesis by (simp add: zlcm_def)
+qed
+
+lemma zgcd_code [code]:
+  "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+  by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
+
+end
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/Library/Primes.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -6,9 +6,11 @@
 header {* Primality on nat *}
 
 theory Primes
-imports Complex_Main
+imports Complex_Main Legacy_GCD
 begin
 
+hide (open) const GCD.gcd GCD.coprime GCD.prime
+
 definition
   coprime :: "nat => nat => bool" where
   "coprime m n \<longleftrightarrow> gcd m n = 1"
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/NatTransfer.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NatTransfer.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -0,0 +1,533 @@
+(*  Title:      HOL/Library/NatTransfer.thy
+    Authors:    Jeremy Avigad and Amine Chaieb
+
+    Sets up transfer from nats to ints and
+    back.
+*)
+
+
+header {* NatTransfer *}
+
+theory NatTransfer
+imports Main Parity
+uses ("Tools/transfer_data.ML")
+begin
+
+subsection {* A transfer Method between isomorphic domains*}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+  where "TransferMorphism a B = True"
+
+use "Tools/transfer_data.ML"
+
+setup TransferData.setup
+
+
+subsection {* Set up transfer from nat to int *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
+  by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_nat_int[transfer
+  add mode: manual
+  return: nat_0_le
+  labels: natint
+]
+
+(* basic functions and relations *)
+
+lemma transfer_nat_int_numerals:
+    "(0::nat) = nat 0"
+    "(1::nat) = nat 1"
+    "(2::nat) = nat 2"
+    "(3::nat) = nat 3"
+  by auto
+
+definition
+  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+  "tsub x y = (if x >= y then x - y else 0)"
+
+lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
+  by (simp add: tsub_def)
+
+
+lemma transfer_nat_int_functions:
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
+    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
+  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
+      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
+
+lemma transfer_nat_int_function_closures:
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+    "(0::int) >= 0"
+    "(1::int) >= 0"
+    "(2::int) >= 0"
+    "(3::int) >= 0"
+    "int z >= 0"
+  apply (auto simp add: zero_le_mult_iff tsub_def)
+  apply (case_tac "y = 0")
+  apply auto
+  apply (subst pos_imp_zdiv_nonneg_iff, auto)
+  apply (case_tac "y = 0")
+  apply force
+  apply (rule pos_mod_sign)
+  apply arith
+done
+
+lemma transfer_nat_int_relations:
+    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+      (nat (x::int) = nat y) = (x = y)"
+    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+      (nat (x::int) < nat y) = (x < y)"
+    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+      (nat (x::int) <= nat y) = (x <= y)"
+    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+      (nat (x::int) dvd nat y) = (x dvd y)"
+  by (auto simp add: zdvd_int even_nat_def)
+
+declare TransferMorphism_nat_int[transfer add return:
+  transfer_nat_int_numerals
+  transfer_nat_int_functions
+  transfer_nat_int_function_closures
+  transfer_nat_int_relations
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_nat_int_quantifiers:
+    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
+    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
+  by (rule all_nat, rule ex_nat)
+
+(* should we restrict these? *)
+lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
+  by auto
+
+lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
+  by auto
+
+declare TransferMorphism_nat_int[transfer add
+  return: transfer_nat_int_quantifiers
+  cong: all_cong ex_cong]
+
+
+(* if *)
+
+lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
+    nat (if P then x else y)"
+  by auto
+
+declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
+
+
+(* operations with sets *)
+
+definition
+  nat_set :: "int set \<Rightarrow> bool"
+where
+  "nat_set S = (ALL x:S. x >= 0)"
+
+lemma transfer_nat_int_set_functions:
+    "card A = card (int ` A)"
+    "{} = nat ` ({}::int set)"
+    "A Un B = nat ` (int ` A Un int ` B)"
+    "A Int B = nat ` (int ` A Int int ` B)"
+    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
+    "{..n} = nat ` {0..int n}"
+    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
+  apply (rule card_image [symmetric])
+  apply (auto simp add: inj_on_def image_def)
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in exI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+done
+
+lemma transfer_nat_int_set_function_closures:
+    "nat_set {}"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+    "x >= 0 \<Longrightarrow> nat_set {x..y}"
+    "nat_set {x. x >= 0 & P x}"
+    "nat_set (int ` C)"
+    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
+  unfolding nat_set_def apply auto
+done
+
+lemma transfer_nat_int_set_relations:
+    "(finite A) = (finite (int ` A))"
+    "(x : A) = (int x : int ` A)"
+    "(A = B) = (int ` A = int ` B)"
+    "(A < B) = (int ` A < int ` B)"
+    "(A <= B) = (int ` A <= int ` B)"
+
+  apply (rule iffI)
+  apply (erule finite_imageI)
+  apply (erule finite_imageD)
+  apply (auto simp add: image_def expand_set_eq inj_on_def)
+  apply (drule_tac x = "int x" in spec, auto)
+  apply (drule_tac x = "int x" in spec, auto)
+  apply (drule_tac x = "int x" in spec, auto)
+done
+
+lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
+    (int ` nat ` A = A)"
+  by (auto simp add: nat_set_def image_def)
+
+lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
+  by auto
+
+declare TransferMorphism_nat_int[transfer add
+  return: transfer_nat_int_set_functions
+    transfer_nat_int_set_function_closures
+    transfer_nat_int_set_relations
+    transfer_nat_int_set_return_embed
+  cong: transfer_nat_int_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is nat *)
+lemma transfer_nat_int_sum_prod:
+    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
+    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+  apply (subst setsum_reindex)
+  apply (unfold inj_on_def, auto)
+  apply (subst setprod_reindex)
+  apply (unfold inj_on_def o_def, auto)
+done
+
+(* this handles the case where the *range* of f is nat *)
+lemma transfer_nat_int_sum_prod2:
+    "setsum f A = nat(setsum (%x. int (f x)) A)"
+    "setprod f A = nat(setprod (%x. int (f x)) A)"
+  apply (subst int_setsum [symmetric])
+  apply auto
+  apply (subst int_setprod [symmetric])
+  apply auto
+done
+
+lemma transfer_nat_int_sum_prod_closure:
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+  unfolding nat_set_def
+  apply (rule setsum_nonneg)
+  apply auto
+  apply (rule setprod_nonneg)
+  apply auto
+done
+
+(* this version doesn't work, even with nat_set A \<Longrightarrow>
+      x : A \<Longrightarrow> x >= 0 turned on. Why not?
+
+  also: what does =simp=> do?
+
+lemma transfer_nat_int_sum_prod_closure:
+    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+  unfolding nat_set_def simp_implies_def
+  apply (rule setsum_nonneg)
+  apply auto
+  apply (rule setprod_nonneg)
+  apply auto
+done
+*)
+
+(* Making A = B in this lemma doesn't work. Why not?
+   Also, why aren't setsum_cong and setprod_cong enough,
+   with the previously mentioned rule turned on? *)
+
+lemma transfer_nat_int_sum_prod_cong:
+    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+      setsum f A = setsum g B"
+    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+      setprod f A = setprod g B"
+  unfolding nat_set_def
+  apply (subst setsum_cong, assumption)
+  apply auto [2]
+  apply (subst setprod_cong, assumption, auto)
+done
+
+declare TransferMorphism_nat_int[transfer add
+  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
+    transfer_nat_int_sum_prod_closure
+  cong: transfer_nat_int_sum_prod_cong]
+
+(* lists *)
+
+definition
+  embed_list :: "nat list \<Rightarrow> int list"
+where
+  "embed_list l = map int l";
+
+definition
+  nat_list :: "int list \<Rightarrow> bool"
+where
+  "nat_list l = nat_set (set l)";
+
+definition
+  return_list :: "int list \<Rightarrow> nat list"
+where
+  "return_list l = map nat l";
+
+thm nat_0_le;
+
+lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
+    embed_list (return_list l) = l";
+  unfolding embed_list_def return_list_def nat_list_def nat_set_def
+  apply (induct l);
+  apply auto;
+done;
+
+lemma transfer_nat_int_list_functions:
+  "l @ m = return_list (embed_list l @ embed_list m)"
+  "[] = return_list []";
+  unfolding return_list_def embed_list_def;
+  apply auto;
+  apply (induct l, auto);
+  apply (induct m, auto);
+done;
+
+(*
+lemma transfer_nat_int_fold1: "fold f l x =
+    fold (%x. f (nat x)) (embed_list l) x";
+*)
+
+
+
+
+subsection {* Set up transfer from int to nat *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
+  by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_int_nat[transfer add
+  mode: manual
+(*  labels: int-nat *)
+  return: nat_int
+]
+
+
+(* basic functions and relations *)
+
+definition
+  is_nat :: "int \<Rightarrow> bool"
+where
+  "is_nat x = (x >= 0)"
+
+lemma transfer_int_nat_numerals:
+    "0 = int 0"
+    "1 = int 1"
+    "2 = int 2"
+    "3 = int 3"
+  by auto
+
+lemma transfer_int_nat_functions:
+    "(int x) + (int y) = int (x + y)"
+    "(int x) * (int y) = int (x * y)"
+    "tsub (int x) (int y) = int (x - y)"
+    "(int x)^n = int (x^n)"
+    "(int x) div (int y) = int (x div y)"
+    "(int x) mod (int y) = int (x mod y)"
+  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
+
+lemma transfer_int_nat_function_closures:
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
+    "is_nat x \<Longrightarrow> is_nat (x^n)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
+    "is_nat 0"
+    "is_nat 1"
+    "is_nat 2"
+    "is_nat 3"
+    "is_nat (int z)"
+  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+lemma transfer_int_nat_relations:
+    "(int x = int y) = (x = y)"
+    "(int x < int y) = (x < y)"
+    "(int x <= int y) = (x <= y)"
+    "(int x dvd int y) = (x dvd y)"
+    "(even (int x)) = (even x)"
+  by (auto simp add: zdvd_int even_nat_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+  transfer_int_nat_numerals
+  transfer_int_nat_functions
+  transfer_int_nat_function_closures
+  transfer_int_nat_relations
+  UNIV_code
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_int_nat_quantifiers:
+    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
+    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
+  apply (subst all_nat)
+  apply auto [1]
+  apply (subst ex_nat)
+  apply auto
+done
+
+declare TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_quantifiers]
+
+
+(* if *)
+
+lemma int_if_cong: "(if P then (int x) else (int y)) =
+    int (if P then x else y)"
+  by auto
+
+declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+
+
+
+(* operations with sets *)
+
+lemma transfer_int_nat_set_functions:
+    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
+    "{} = int ` ({}::nat set)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
+    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
+    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
+       (* need all variants of these! *)
+  by (simp_all only: is_nat_def transfer_nat_int_set_functions
+          transfer_nat_int_set_function_closures
+          transfer_nat_int_set_return_embed nat_0_le
+          cong: transfer_nat_int_set_cong)
+
+lemma transfer_int_nat_set_function_closures:
+    "nat_set {}"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+    "is_nat x \<Longrightarrow> nat_set {x..y}"
+    "nat_set {x. x >= 0 & P x}"
+    "nat_set (int ` C)"
+    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
+  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
+
+lemma transfer_int_nat_set_relations:
+    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
+    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
+    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
+  by (simp_all only: is_nat_def transfer_nat_int_set_relations
+    transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
+  by (simp only: transfer_nat_int_set_relations
+    transfer_nat_int_set_function_closures
+    transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
+    {(x::nat). P x} = {x. P' x}"
+  by auto
+
+declare TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_set_functions
+    transfer_int_nat_set_function_closures
+    transfer_int_nat_set_relations
+    transfer_int_nat_set_return_embed
+  cong: transfer_int_nat_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is int *)
+lemma transfer_int_nat_sum_prod:
+    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
+    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+  apply (subst setsum_reindex)
+  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
+  apply (subst setprod_reindex)
+  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
+            cong: setprod_cong)
+done
+
+(* this handles the case where the *range* of f is int *)
+lemma transfer_int_nat_sum_prod2:
+    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
+    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
+      setprod f A = int(setprod (%x. nat (f x)) A)"
+  unfolding is_nat_def
+  apply (subst int_setsum, auto)
+  apply (subst int_setprod, auto simp add: cong: setprod_cong)
+done
+
+declare TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
+  cong: setsum_cong setprod_cong]
+
+
+subsection {* Test it out *}
+
+(* nat to int *)
+
+lemma ex1: "(x::nat) + y = y + x"
+  by auto
+
+thm ex1 [transferred]
+
+lemma ex2: "(a::nat) div b * b + a mod b = a"
+  by (rule mod_div_equality)
+
+thm ex2 [transferred]
+
+lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
+  by auto
+
+thm ex3 [transferred natint]
+
+lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
+  by auto
+
+thm ex4 [transferred]
+
+lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
+  by (induct n rule: nat_induct, auto)
+
+thm ex5 [transferred]
+
+theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+  by (rule ex5 [transferred])
+
+thm ex6 [transferred]
+
+thm ex5 [transferred, transferred]
+
+end
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/Rational.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -851,11 +851,11 @@
 
 subsection {* Implementation of rational numbers as pairs of integers *}
 
-lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"
+lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
 proof (cases "a = 0 \<or> b = 0")
   case True then show ?thesis by (auto simp add: eq_rat)
 next
-  let ?c = "zgcd a b"
+  let ?c = "gcd a b"
   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   then have "?c \<noteq> 0" by simp
   then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
@@ -870,7 +870,7 @@
 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
   [simp, code del]: "Fract_norm a b = Fract a b"
 
-lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
+lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = gcd a b in
   if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
   by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
 
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu Jun 18 15:08:57 2009 +0200
+++ b/src/HOL/RealDef.thy	Thu Jun 18 07:51:15 2009 -0700
@@ -895,14 +895,15 @@
 
 lemma Rats_abs_nat_div_natE:
   assumes "x \<in> \<rat>"
-  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
+  obtains m n :: nat
+  where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
 proof -
   from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
     by(auto simp add: Rats_eq_int_div_nat)
   hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
   then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
   let ?gcd = "gcd m n"
-  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
+  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp
   let ?k = "m div ?gcd"
   let ?l = "n div ?gcd"
   let ?gcd' = "gcd ?k ?l"
@@ -924,9 +925,9 @@
   have "?gcd' = 1"
   proof -
     have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
-      by (rule gcd_mult_distrib2)
+      by (rule nat_gcd_mult_distrib)
     with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
-    with gcd show ?thesis by simp
+    with gcd show ?thesis by auto
   qed
   ultimately show ?thesis ..
 qed
diff -r 4e6064759aeb -r 99f08ce977f9 src/HOL/Tools/transfer_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/transfer_data.ML	Thu Jun 18 07:51:15 2009 -0700
@@ -0,0 +1,242 @@
+(*  Title:      Tools/transfer.ML
+    Author:     Amine Chaieb, University of Cambridge, 2009
+                Jeremy Avigad, Carnegie Mellon University
+*)
+
+signature TRANSFER_DATA =
+sig
+  type data
+  type entry
+  val get: Proof.context -> data
+  val del: attribute
+  val add: attribute 
+  val setup: theory -> theory
+end;
+
+structure TransferData (* : TRANSFER_DATA*) =
+struct
+type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list}; 
+type data = simpset * (thm * entry) list;
+
+val eq_key = Thm.eq_thm;
+fun eq_data arg = eq_fst eq_key arg;
+
+structure Data = GenericDataFun
+(
+  type T = data;
+  val empty = (HOL_ss, []);
+  val extend  = I;
+  fun merge _ ((ss, e), (ss', e')) =
+    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
+);
+
+val get = Data.get o Context.Proof;
+
+fun del_data key = apsnd (remove eq_data (key, []));
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+val del_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
+
+val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
+
+fun merge_update eq m (k,v) [] = [(k,v)]
+  | merge_update eq m (k,v) ((k',v')::al) = 
+           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
+
+fun C f x y = f y x
+
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
+ HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
+
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
+ let 
+  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import_thms true (map Drule.mk_term [a0, D0]) ctxt0)
+  val (aT,bT) = 
+     let val T = typ_of (ctyp_of_term a) 
+     in (Term.range_type T, Term.domain_type T)
+     end
+  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
+  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) [])
+  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
+  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
+  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
+  val cis = map (Thm.capply a) cfis
+  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
+  val th1 = Drule.cterm_instantiate (cns~~ cis) th
+  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
+  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
+                                         (fold_rev implies_intr (map cprop_of hs) th2)
+in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+
+local
+fun transfer_ruleh a D leave ctxt th = 
+ let val (ss,al) = get ctxt
+     val a0 = cterm_of (ProofContext.theory_of ctxt) a
+     val D0 = cterm_of (ProofContext.theory_of ctxt) D
+     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
+                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
+                 end
+ in case get_first h al of
+      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
+    | NONE => error "Transfer: corresponding instance not found in context-data"
+ end
+in fun transfer_rule (a,D) leave (gctxt,th) = 
+   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
+end;
+
+fun  splits P [] = []
+   | splits P (xxs as (x::xs)) = 
+    let val pss = filter (P x) xxs
+        val qss = filter_out (P x) xxs
+    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
+    end
+
+fun all_transfers leave (gctxt,th) = 
+ let 
+  val ctxt = Context.proof_of gctxt
+  val tys = map snd (Term.add_vars (prop_of th) [])
+  val _ = if null tys then error "transfer: Unable to guess instance" else ()
+  val tyss = splits (curry Type.could_unify) tys 
+  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
+  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+  val insts = 
+    map_filter (fn tys => 
+          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
+                                  then SOME (get_aD k, ss) 
+                                  else NONE) (snd (get ctxt))) tyss
+  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+  val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+fun transfer_rule_by_hint ls leave (gctxt,th) = 
+ let 
+  val ctxt = Context.proof_of gctxt
+  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+  val insts = 
+    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
+			    then SOME (get_aD k, e) else NONE)
+        (snd (get ctxt))
+  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
+  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+  val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+
+fun transferred_attribute ls NONE leave = 
+         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
+  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
+
+                                                    (* Add data to the context *)
+fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
+                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
+                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
+ = 
+ let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
+  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
+  hints = subtract (op = : string*string -> bool) hints0 
+            (hints1 union_string hints2)}
+ end;
+
+local
+ val h = curry (merge Thm.eq_thm)
+in
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
+                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
+    {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}
+end; 
+
+fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
+  Thm.declaration_attribute (fn key => fn context => context |> Data.map
+   (fn (ss, al) => 
+     let
+      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
+                in 0 end) 
+                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
+      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
+      val entry = 
+        if g then 
+         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
+             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
+             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") 
+                        else inja
+             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)
+         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
+        else e0
+    in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
+    end));
+
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ()
+fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+
+val congN = "cong"
+val injN = "inj"
+val embedN = "embed"
+val returnN = "return"
+val addN = "add"
+val delN = "del"
+val modeN = "mode"
+val automaticN = "automatic"
+val manualN = "manual"
+val directionN = "direction"
+val labelsN = "labels"
+val leavingN = "leaving"
+
+val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
+val terms = thms >> map Drule.dest_term
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
+val name = Scan.lift Args.name
+val names = Scan.repeat (Scan.unless any_keyword name)
+fun optional scan = Scan.optional scan []
+fun optional2 scan = Scan.optional scan ([],[])
+
+val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
+val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
+val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
+val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
+val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
+val addscan = Scan.unless any_keyword (keyword addN)
+val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
+val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
+
+val transf_add = addscan |-- entry
+in
+
+val install_att_syntax =
+  (Scan.lift (Args.$$$ delN >> K del) ||
+    transf_add
+    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
+
+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));
+
+end;
+
+
+(* theory setup *)
+
+
+val setup =
+  Attrib.setup @{binding transfer} install_att_syntax
+    "Installs transfer data" #>
+  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
+    "simp rules for transfer" #>
+  Attrib.setup @{binding transferred} transferred_att_syntax
+    "Transfers theorems";
+
+end;