# HG changeset patch
# User haftmann
# Date 1416232532 -3600
# Node ID f61482b0f240c28e81584cab72a11d63dc0e807b
# Parent  059ba950a657e8c4a710991c43b04e0d0ca7b0a2
formally self-contained gcd type classes

diff -r 059ba950a657 -r f61482b0f240 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Nov 14 22:13:45 2014 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Mon Nov 17 14:55:32 2014 +0100
@@ -265,8 +265,8 @@
       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 gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
-        of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
+        of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * b' + b * a'" "b * b'"]]
+        of_int_div [where ?'a = 'a, OF gz gcd_dvd2 [of "a * b' + b * a'" "b * b'"]]
         by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps)
     }
     ultimately have ?thesis using aa' bb'
@@ -289,8 +289,8 @@
   { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
     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 gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
-      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
+    from z of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * a'" "b * b'"]]
+      of_int_div [where ?'a = 'a , OF gz gcd_dvd2 [of "a * a'" "b * b'"]]
     have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
   ultimately show ?thesis by blast
 qed
diff -r 059ba950a657 -r f61482b0f240 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Nov 14 22:13:45 2014 +0100
+++ b/src/HOL/GCD.thy	Mon Nov 17 14:55:32 2014 +0100
@@ -47,6 +47,13 @@
 
 end
 
+class semiring_gcd = comm_semiring_1 + gcd +
+  assumes gcd_dvd1 [iff]: "gcd a b dvd a"
+		and gcd_dvd2 [iff]: "gcd a b dvd b"
+		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 
+
+class ring_gcd = comm_ring_1 + semiring_gcd
+
 instantiation nat :: gcd
 begin
 
@@ -240,30 +247,40 @@
   conjunctions don't seem provable separately.
 *}
 
-lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
-  and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
-  apply (induct m n rule: gcd_nat_induct)
-  apply (simp_all add: gcd_non_0_nat gcd_0_nat)
-  apply (blast dest: dvd_mod_imp_dvd)
-done
-
-lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
-by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
-
-lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
-by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
-
+instance nat :: semiring_gcd
+proof
+  fix m n :: nat
+  show "gcd m n dvd m" and "gcd m n dvd n"
+  proof (induct m n rule: gcd_nat_induct)
+    fix m n :: nat
+    assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
+    then have "gcd n (m mod n) dvd m"
+      by (rule dvd_mod_imp_dvd)
+    moreover assume "0 < n"
+    ultimately show "gcd m n dvd m"
+      by (simp add: gcd_non_0_nat)
+  qed (simp_all add: gcd_0_nat gcd_non_0_nat)
+next
+  fix m n k :: nat
+  assume "k dvd m" and "k dvd n"
+  then show "k dvd gcd m n"
+    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
+qed
+  
+instance int :: ring_gcd
+  by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
+  
 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
-by(metis gcd_dvd1_nat dvd_trans)
+  by (metis gcd_dvd1 dvd_trans)
 
 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
-by(metis gcd_dvd2_nat dvd_trans)
+  by (metis gcd_dvd2 dvd_trans)
 
 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
-by(metis gcd_dvd1_int dvd_trans)
+  by (metis gcd_dvd1 dvd_trans)
 
 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
-by(metis gcd_dvd2_int dvd_trans)
+  by (metis gcd_dvd2 dvd_trans)
 
 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   by (rule dvd_imp_le, auto)
@@ -277,23 +294,12 @@
 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   by (rule zdvd_imp_le, auto)
 
-lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
-by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
-
-lemma gcd_greatest_int:
-  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
-  apply (subst gcd_abs_int)
-  apply (subst abs_dvd_iff [symmetric])
-  apply (rule gcd_greatest_nat [transferred])
-  apply auto
-done
-
 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
     (k dvd m & k dvd n)"
-  by (blast intro!: gcd_greatest_nat intro: dvd_trans)
+  by (blast intro!: gcd_greatest intro: dvd_trans)
 
 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
-  by (blast intro!: gcd_greatest_int intro: dvd_trans)
+  by (blast intro!: gcd_greatest intro: dvd_trans)
 
 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
@@ -311,7 +317,7 @@
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   apply auto
   apply (rule dvd_antisym)
-  apply (erule (1) gcd_greatest_nat)
+  apply (erule (1) gcd_greatest)
   apply auto
 done
 
@@ -321,7 +327,7 @@
  apply simp
 apply (rule iffI)
  apply (rule zdvd_antisym_nonneg)
- apply (auto intro: gcd_greatest_int)
+ apply (auto intro: gcd_greatest)
 done
 
 interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -406,7 +412,7 @@
 
 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   apply (rule dvd_antisym)
-  apply (rule gcd_greatest_nat)
+  apply (rule gcd_greatest)
   apply (rule_tac n = k in coprime_dvd_mult_nat)
   apply (simp add: gcd_assoc_nat)
   apply (simp add: gcd_commute_nat)
@@ -591,7 +597,7 @@
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   have "?g \<noteq> 0" using nz by simp
   then have gp: "?g > 0" by arith
-  from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
 qed
 
@@ -681,7 +687,7 @@
   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
 proof -
   have "gcd d a dvd gcd d (a * b)"
-    by (rule gcd_greatest_nat, auto)
+    by (rule gcd_greatest, auto)
   with dab show ?thesis
     by auto
 qed
@@ -690,7 +696,7 @@
   assumes "coprime (d::int) (a * b)" shows "coprime d a"
 proof -
   have "gcd d a dvd gcd d (a * b)"
-    by (rule gcd_greatest_int, auto)
+    by (rule gcd_greatest, auto)
   with assms show ?thesis
     by auto
 qed
@@ -699,7 +705,7 @@
   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
 proof -
   have "gcd d b dvd gcd d (a * b)"
-    by (rule gcd_greatest_nat, auto intro: dvd_mult)
+    by (rule gcd_greatest, auto intro: dvd_mult)
   with assms show ?thesis
     by auto
 qed
@@ -708,7 +714,7 @@
   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
 proof -
   have "gcd d b dvd gcd d (a * b)"
-    by (rule gcd_greatest_int, auto intro: dvd_mult)
+    by (rule gcd_greatest, auto intro: dvd_mult)
   with dab show ?thesis
     by auto
 qed
@@ -746,7 +752,7 @@
     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: div_gcd_coprime_int dvd_div_mult_self)
+  using nz apply (auto simp add: div_gcd_coprime_int)
 done
 
 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
@@ -984,14 +990,14 @@
     x dvd b \<Longrightarrow> x = 1"
   apply (subgoal_tac "x dvd gcd a b")
   apply simp
-  apply (erule (1) gcd_greatest_nat)
+  apply (erule (1) gcd_greatest)
 done
 
 lemma coprime_common_divisor_int: "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) gcd_greatest_int)
+  apply (erule (1) gcd_greatest)
 done
 
 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
@@ -1226,7 +1232,7 @@
           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 ac_simps)
+            by (simp only: diff_mult_distrib2 ac_simps)
           hence ?thesis using H(1,2)
             apply -
             apply (rule exI[where x=d], simp)
@@ -1746,5 +1752,16 @@
   "Gcd (set xs) = fold gcd xs (0::int)"
   by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
 
+
+text \<open>Fact aliasses\<close>
+  
+lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat] 
+  and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
+  and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
+
+lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int] 
+  and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
+  and gcd_greatest_int = gcd_greatest [where ?'a = int]
+
 end