src/HOL/GCD.thy
 changeset 31798 fe9a3043d36c parent 31766 f767c5b1702e child 31813 4df828bbc411
```     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.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.111
1.112  lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
1.113 -  apply (subst int_gcd_commute)
1.116 -  apply (subst int_gcd_commute)
1.117 -  apply (rule refl)
1.118 -done
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.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)"
```