Cleaned up GCD
authornipkow
Thu Jun 25 07:34:12 2009 +0200 (2009-06-25)
changeset 31798fe9a3043d36c
parent 31792 d5a6096b94ad
child 31799 294b955d0e80
Cleaned up GCD
src/HOL/GCD.thy
src/HOL/NewNumberTheory/Residues.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Jun 24 17:50:49 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu Jun 25 07:34:12 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      GCD.thy
     1.5      Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     1.6 -                Thomas M. Rasmussen, Jeremy Avigad
     1.7 +                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     1.8  
     1.9  
    1.10  This file deals with the functions gcd and lcm, and properties of
    1.11 @@ -20,6 +20,7 @@
    1.12  the congruence relations on the integers. The notion was extended to
    1.13  the natural numbers by Chiaeb.
    1.14  
    1.15 +Tobias Nipkow cleaned up a lot.
    1.16  *)
    1.17  
    1.18  
    1.19 @@ -247,11 +248,11 @@
    1.20  lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
    1.21    by (simp add: gcd_int_def)
    1.22  
    1.23 -lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
    1.24 -  by simp
    1.25 +lemma nat_gcd_idem: "gcd (x::nat) x = x"
    1.26 +by simp
    1.27  
    1.28 -lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
    1.29 -  by (subst int_gcd_abs, auto simp add: gcd_int_def)
    1.30 +lemma int_gcd_idem: "gcd (x::int) x = abs x"
    1.31 +by (subst int_gcd_abs, auto simp add: gcd_int_def)
    1.32  
    1.33  declare gcd_nat.simps [simp del]
    1.34  
    1.35 @@ -267,8 +268,6 @@
    1.36    apply (blast dest: dvd_mod_imp_dvd)
    1.37  done
    1.38  
    1.39 -thm nat_gcd_dvd1 [transferred]
    1.40 -
    1.41  lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
    1.42    apply (subst int_gcd_abs)
    1.43    apply (rule dvd_trans)
    1.44 @@ -308,7 +307,7 @@
    1.45    by (rule zdvd_imp_le, auto)
    1.46  
    1.47  lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.48 -  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
    1.49 +by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
    1.50  
    1.51  lemma int_gcd_greatest:
    1.52    assumes "(k::int) dvd m" and "k dvd n"
    1.53 @@ -364,15 +363,6 @@
    1.54  
    1.55  lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
    1.56  
    1.57 -lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
    1.58 -  by (subst nat_gcd_commute, simp)
    1.59 -
    1.60 -lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
    1.61 -  by (subst nat_gcd_commute, simp add: One_nat_def)
    1.62 -
    1.63 -lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
    1.64 -  by (subst int_gcd_commute, simp)
    1.65 -
    1.66  lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
    1.67      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.68    apply auto
    1.69 @@ -395,6 +385,19 @@
    1.70    apply (auto intro: int_gcd_greatest)
    1.71  done
    1.72  
    1.73 +lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    1.74 +by (metis dvd.eq_iff nat_gcd_unique)
    1.75 +
    1.76 +lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
    1.77 +by (metis dvd.eq_iff nat_gcd_unique)
    1.78 +
    1.79 +lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
    1.80 +by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique)
    1.81 +
    1.82 +lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
    1.83 +by (metis gcd_proj1_if_dvd_int int_gcd_commute)
    1.84 +
    1.85 +
    1.86  text {*
    1.87    \medskip Multiplication laws
    1.88  *}
    1.89 @@ -414,12 +417,6 @@
    1.90    apply auto
    1.91  done
    1.92  
    1.93 -lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
    1.94 -  by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
    1.95 -
    1.96 -lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
    1.97 -  by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
    1.98 -
    1.99  lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   1.100    apply (insert nat_gcd_mult_distrib [of m k n])
   1.101    apply simp
   1.102 @@ -517,42 +514,22 @@
   1.103  done
   1.104  
   1.105  lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   1.106 -  apply (case_tac "n = 0", force)
   1.107 -  apply (subst (1 2) int_gcd_red)
   1.108 -  apply auto
   1.109 -done
   1.110 +by (metis int_gcd_red mod_add_self1 zadd_commute)
   1.111  
   1.112  lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.113 -  apply (subst int_gcd_commute)
   1.114 -  apply (subst add_commute)
   1.115 -  apply (subst int_gcd_add1)
   1.116 -  apply (subst int_gcd_commute)
   1.117 -  apply (rule refl)
   1.118 -done
   1.119 +by (metis int_gcd_add1 int_gcd_commute zadd_commute)
   1.120  
   1.121  lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   1.122 -  by (induct k, simp_all add: ring_simps)
   1.123 +by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red)
   1.124  
   1.125  lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   1.126 -  apply (subgoal_tac "ALL s. ALL m. ALL n.
   1.127 -      gcd m (int (s::nat) * m + n) = gcd m n")
   1.128 -  apply (case_tac "k >= 0")
   1.129 -  apply (drule_tac x = "nat k" in spec, force)
   1.130 -  apply (subst (1 2) int_gcd_neg2 [symmetric])
   1.131 -  apply (drule_tac x = "nat (- k)" in spec)
   1.132 -  apply (drule_tac x = "m" in spec)
   1.133 -  apply (drule_tac x = "-n" in spec)
   1.134 -  apply auto
   1.135 -  apply (rule nat_induct)
   1.136 -  apply auto
   1.137 -  apply (auto simp add: left_distrib)
   1.138 -  apply (subst add_assoc)
   1.139 -  apply simp
   1.140 -done
   1.141 +by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute)
   1.142 +
   1.143  
   1.144  (* to do: differences, and all variations of addition rules
   1.145      as simplification rules for nat and int *)
   1.146  
   1.147 +(* FIXME remove iff *)
   1.148  lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   1.149    using mult_dvd_mono [of 1] by auto
   1.150  
   1.151 @@ -714,20 +691,20 @@
   1.152  qed
   1.153  
   1.154  lemma int_coprime_lmult:
   1.155 -  assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
   1.156 +  assumes "coprime (d::int) (a * b)" shows "coprime d a"
   1.157  proof -
   1.158    have "gcd d a dvd gcd d (a * b)"
   1.159      by (rule int_gcd_greatest, auto)
   1.160 -  with dab show ?thesis
   1.161 +  with assms show ?thesis
   1.162      by auto
   1.163  qed
   1.164  
   1.165  lemma nat_coprime_rmult:
   1.166 -  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
   1.167 +  assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   1.168  proof -
   1.169    have "gcd d b dvd gcd d (a * b)"
   1.170      by (rule nat_gcd_greatest, auto intro: dvd_mult)
   1.171 -  with dab show ?thesis
   1.172 +  with assms show ?thesis
   1.173      by auto
   1.174  qed
   1.175  
   1.176 @@ -937,6 +914,7 @@
   1.177    ultimately show ?thesis by blast
   1.178  qed
   1.179  
   1.180 +(* FIXME move to Divides(?) *)
   1.181  lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   1.182    by (auto intro: nat_pow_divides_pow dvd_power_same)
   1.183  
   1.184 @@ -1316,30 +1294,12 @@
   1.185  lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
   1.186    unfolding lcm_int_def by simp
   1.187  
   1.188 -lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
   1.189 -  unfolding lcm_nat_def by simp
   1.190 -
   1.191 -lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
   1.192 -  unfolding lcm_nat_def by (simp add: One_nat_def)
   1.193 -
   1.194 -lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
   1.195 -  unfolding lcm_int_def by simp
   1.196 -
   1.197  lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
   1.198    unfolding lcm_nat_def by simp
   1.199  
   1.200  lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
   1.201    unfolding lcm_int_def by simp
   1.202  
   1.203 -lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
   1.204 -  unfolding lcm_nat_def by simp
   1.205 -
   1.206 -lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
   1.207 -  unfolding lcm_nat_def by (simp add: One_nat_def)
   1.208 -
   1.209 -lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
   1.210 -  unfolding lcm_int_def by simp
   1.211 -
   1.212  lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
   1.213    unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
   1.214  
   1.215 @@ -1348,34 +1308,14 @@
   1.216  
   1.217  
   1.218  lemma nat_lcm_pos:
   1.219 -  assumes mpos: "(m::nat) > 0"
   1.220 -  and npos: "n>0"
   1.221 -  shows "lcm m n > 0"
   1.222 -proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
   1.223 -  assume h:"m*n div gcd m n = 0"
   1.224 -  from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
   1.225 -  hence gcdp: "gcd m n > 0" by simp
   1.226 -  with h
   1.227 -  have "m*n < gcd m n"
   1.228 -    by (cases "m * n < gcd m n")
   1.229 -       (auto simp add: div_if[OF gcdp, where m="m*n"])
   1.230 -  moreover
   1.231 -  have "gcd m n dvd m" by simp
   1.232 -  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
   1.233 -  with npos have t1:"gcd m n*n \<le> m*n" by simp
   1.234 -  have "gcd m n \<le> gcd m n*n" using npos by simp
   1.235 -  with t1 have "gcd m n \<le> m*n" by arith
   1.236 -  ultimately show "False" by simp
   1.237 -qed
   1.238 +  "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
   1.239 +by (metis gr0I mult_is_0 nat_prod_gcd_lcm)
   1.240  
   1.241  lemma int_lcm_pos:
   1.242 -  assumes mneq0: "(m::int) ~= 0"
   1.243 -  and npos: "n ~= 0"
   1.244 -  shows "lcm m n > 0"
   1.245 -
   1.246 +  "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
   1.247    apply (subst int_lcm_abs)
   1.248    apply (rule nat_lcm_pos [transferred])
   1.249 -  using prems apply auto
   1.250 +  apply auto
   1.251  done
   1.252  
   1.253  lemma nat_dvd_pos:
   1.254 @@ -1417,13 +1357,11 @@
   1.255  qed
   1.256  
   1.257  lemma int_lcm_least:
   1.258 -  assumes "(m::int) dvd k" and "n dvd k"
   1.259 -  shows "lcm m n dvd k"
   1.260 -
   1.261 -  apply (subst int_lcm_abs)
   1.262 -  apply (rule dvd_trans)
   1.263 -  apply (rule nat_lcm_least [transferred, of _ "abs k" _])
   1.264 -  using prems apply auto
   1.265 +  "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
   1.266 +apply (subst int_lcm_abs)
   1.267 +apply (rule dvd_trans)
   1.268 +apply (rule nat_lcm_least [transferred, of _ "abs k" _])
   1.269 +apply auto
   1.270  done
   1.271  
   1.272  lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
   1.273 @@ -1481,23 +1419,23 @@
   1.274      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.275    by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
   1.276  
   1.277 -lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   1.278 +lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   1.279    apply (rule sym)
   1.280    apply (subst nat_lcm_unique [symmetric])
   1.281    apply auto
   1.282  done
   1.283  
   1.284 -lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
   1.285 +lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
   1.286    apply (rule sym)
   1.287    apply (subst int_lcm_unique [symmetric])
   1.288    apply auto
   1.289  done
   1.290  
   1.291 -lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   1.292 -  by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
   1.293 +lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   1.294 +by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat)
   1.295  
   1.296 -lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
   1.297 -  by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
   1.298 +lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
   1.299 +by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int)
   1.300  
   1.301  
   1.302  lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
     2.1 --- a/src/HOL/NewNumberTheory/Residues.thy	Wed Jun 24 17:50:49 2009 +0200
     2.2 +++ b/src/HOL/NewNumberTheory/Residues.thy	Thu Jun 25 07:34:12 2009 +0200
     2.3 @@ -202,9 +202,6 @@
     2.4    apply (subgoal_tac "a mod m ~= 0")
     2.5    apply arith
     2.6    apply auto
     2.7 -  apply (subst (asm) int_gcd_commute)
     2.8 -  apply (subst (asm) int_gcd_mult)
     2.9 -  apply auto
    2.10    apply (subst (asm) int_gcd_red)
    2.11    apply (subst int_gcd_commute, assumption)
    2.12  done