src/HOL/GCD.thy
changeset 59008 f61482b0f240
parent 58889 5b7a9633cfa8
child 59497 0c5cd369a643
     1.1 --- a/src/HOL/GCD.thy	Fri Nov 14 22:13:45 2014 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Nov 17 14:55:32 2014 +0100
     1.3 @@ -47,6 +47,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class semiring_gcd = comm_semiring_1 + gcd +
     1.8 +  assumes gcd_dvd1 [iff]: "gcd a b dvd a"
     1.9 +		and gcd_dvd2 [iff]: "gcd a b dvd b"
    1.10 +		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 
    1.11 +
    1.12 +class ring_gcd = comm_ring_1 + semiring_gcd
    1.13 +
    1.14  instantiation nat :: gcd
    1.15  begin
    1.16  
    1.17 @@ -240,30 +247,40 @@
    1.18    conjunctions don't seem provable separately.
    1.19  *}
    1.20  
    1.21 -lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
    1.22 -  and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
    1.23 -  apply (induct m n rule: gcd_nat_induct)
    1.24 -  apply (simp_all add: gcd_non_0_nat gcd_0_nat)
    1.25 -  apply (blast dest: dvd_mod_imp_dvd)
    1.26 -done
    1.27 -
    1.28 -lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
    1.29 -by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
    1.30 -
    1.31 -lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
    1.32 -by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
    1.33 -
    1.34 +instance nat :: semiring_gcd
    1.35 +proof
    1.36 +  fix m n :: nat
    1.37 +  show "gcd m n dvd m" and "gcd m n dvd n"
    1.38 +  proof (induct m n rule: gcd_nat_induct)
    1.39 +    fix m n :: nat
    1.40 +    assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
    1.41 +    then have "gcd n (m mod n) dvd m"
    1.42 +      by (rule dvd_mod_imp_dvd)
    1.43 +    moreover assume "0 < n"
    1.44 +    ultimately show "gcd m n dvd m"
    1.45 +      by (simp add: gcd_non_0_nat)
    1.46 +  qed (simp_all add: gcd_0_nat gcd_non_0_nat)
    1.47 +next
    1.48 +  fix m n k :: nat
    1.49 +  assume "k dvd m" and "k dvd n"
    1.50 +  then show "k dvd gcd m n"
    1.51 +    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
    1.52 +qed
    1.53 +  
    1.54 +instance int :: ring_gcd
    1.55 +  by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
    1.56 +  
    1.57  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
    1.58 -by(metis gcd_dvd1_nat dvd_trans)
    1.59 +  by (metis gcd_dvd1 dvd_trans)
    1.60  
    1.61  lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
    1.62 -by(metis gcd_dvd2_nat dvd_trans)
    1.63 +  by (metis gcd_dvd2 dvd_trans)
    1.64  
    1.65  lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
    1.66 -by(metis gcd_dvd1_int dvd_trans)
    1.67 +  by (metis gcd_dvd1 dvd_trans)
    1.68  
    1.69  lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
    1.70 -by(metis gcd_dvd2_int dvd_trans)
    1.71 +  by (metis gcd_dvd2 dvd_trans)
    1.72  
    1.73  lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
    1.74    by (rule dvd_imp_le, auto)
    1.75 @@ -277,23 +294,12 @@
    1.76  lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
    1.77    by (rule zdvd_imp_le, auto)
    1.78  
    1.79 -lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.80 -by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
    1.81 -
    1.82 -lemma gcd_greatest_int:
    1.83 -  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.84 -  apply (subst gcd_abs_int)
    1.85 -  apply (subst abs_dvd_iff [symmetric])
    1.86 -  apply (rule gcd_greatest_nat [transferred])
    1.87 -  apply auto
    1.88 -done
    1.89 -
    1.90  lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
    1.91      (k dvd m & k dvd n)"
    1.92 -  by (blast intro!: gcd_greatest_nat intro: dvd_trans)
    1.93 +  by (blast intro!: gcd_greatest intro: dvd_trans)
    1.94  
    1.95  lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
    1.96 -  by (blast intro!: gcd_greatest_int intro: dvd_trans)
    1.97 +  by (blast intro!: gcd_greatest intro: dvd_trans)
    1.98  
    1.99  lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   1.100    by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   1.101 @@ -311,7 +317,7 @@
   1.102      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.103    apply auto
   1.104    apply (rule dvd_antisym)
   1.105 -  apply (erule (1) gcd_greatest_nat)
   1.106 +  apply (erule (1) gcd_greatest)
   1.107    apply auto
   1.108  done
   1.109  
   1.110 @@ -321,7 +327,7 @@
   1.111   apply simp
   1.112  apply (rule iffI)
   1.113   apply (rule zdvd_antisym_nonneg)
   1.114 - apply (auto intro: gcd_greatest_int)
   1.115 + apply (auto intro: gcd_greatest)
   1.116  done
   1.117  
   1.118  interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.119 @@ -406,7 +412,7 @@
   1.120  
   1.121  lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   1.122    apply (rule dvd_antisym)
   1.123 -  apply (rule gcd_greatest_nat)
   1.124 +  apply (rule gcd_greatest)
   1.125    apply (rule_tac n = k in coprime_dvd_mult_nat)
   1.126    apply (simp add: gcd_assoc_nat)
   1.127    apply (simp add: gcd_commute_nat)
   1.128 @@ -591,7 +597,7 @@
   1.129        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.130    have "?g \<noteq> 0" using nz by simp
   1.131    then have gp: "?g > 0" by arith
   1.132 -  from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.133 +  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.134    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   1.135  qed
   1.136  
   1.137 @@ -681,7 +687,7 @@
   1.138    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   1.139  proof -
   1.140    have "gcd d a dvd gcd d (a * b)"
   1.141 -    by (rule gcd_greatest_nat, auto)
   1.142 +    by (rule gcd_greatest, auto)
   1.143    with dab show ?thesis
   1.144      by auto
   1.145  qed
   1.146 @@ -690,7 +696,7 @@
   1.147    assumes "coprime (d::int) (a * b)" shows "coprime d a"
   1.148  proof -
   1.149    have "gcd d a dvd gcd d (a * b)"
   1.150 -    by (rule gcd_greatest_int, auto)
   1.151 +    by (rule gcd_greatest, auto)
   1.152    with assms show ?thesis
   1.153      by auto
   1.154  qed
   1.155 @@ -699,7 +705,7 @@
   1.156    assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   1.157  proof -
   1.158    have "gcd d b dvd gcd d (a * b)"
   1.159 -    by (rule gcd_greatest_nat, auto intro: dvd_mult)
   1.160 +    by (rule gcd_greatest, auto intro: dvd_mult)
   1.161    with assms show ?thesis
   1.162      by auto
   1.163  qed
   1.164 @@ -708,7 +714,7 @@
   1.165    assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   1.166  proof -
   1.167    have "gcd d b dvd gcd d (a * b)"
   1.168 -    by (rule gcd_greatest_int, auto intro: dvd_mult)
   1.169 +    by (rule gcd_greatest, auto intro: dvd_mult)
   1.170    with dab show ?thesis
   1.171      by auto
   1.172  qed
   1.173 @@ -746,7 +752,7 @@
   1.174      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.175    apply (rule_tac x = "a div gcd a b" in exI)
   1.176    apply (rule_tac x = "b div gcd a b" in exI)
   1.177 -  using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   1.178 +  using nz apply (auto simp add: div_gcd_coprime_int)
   1.179  done
   1.180  
   1.181  lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   1.182 @@ -984,14 +990,14 @@
   1.183      x dvd b \<Longrightarrow> x = 1"
   1.184    apply (subgoal_tac "x dvd gcd a b")
   1.185    apply simp
   1.186 -  apply (erule (1) gcd_greatest_nat)
   1.187 +  apply (erule (1) gcd_greatest)
   1.188  done
   1.189  
   1.190  lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
   1.191      x dvd b \<Longrightarrow> abs x = 1"
   1.192    apply (subgoal_tac "x dvd gcd a b")
   1.193    apply simp
   1.194 -  apply (erule (1) gcd_greatest_int)
   1.195 +  apply (erule (1) gcd_greatest)
   1.196  done
   1.197  
   1.198  lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
   1.199 @@ -1226,7 +1232,7 @@
   1.200            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
   1.201              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
   1.202            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
   1.203 -            by (simp only: diff_mult_distrib2 add.commute ac_simps)
   1.204 +            by (simp only: diff_mult_distrib2 ac_simps)
   1.205            hence ?thesis using H(1,2)
   1.206              apply -
   1.207              apply (rule exI[where x=d], simp)
   1.208 @@ -1746,5 +1752,16 @@
   1.209    "Gcd (set xs) = fold gcd xs (0::int)"
   1.210    by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
   1.211  
   1.212 +
   1.213 +text \<open>Fact aliasses\<close>
   1.214 +  
   1.215 +lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat] 
   1.216 +  and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
   1.217 +  and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
   1.218 +
   1.219 +lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int] 
   1.220 +  and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
   1.221 +  and gcd_greatest_int = gcd_greatest [where ?'a = int]
   1.222 +
   1.223  end
   1.224