src/HOL/GCD.thy
 changeset 60690 a9e45c9588c3 parent 60689 8a2d7c04d8c0 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
1.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 20:19:12 2015 +0200
1.3 @@ -31,51 +31,6 @@
1.4  imports Main
1.5  begin
1.6
1.7 -context semidom_divide
1.8 -begin
1.9 -
1.10 -lemma divide_1 [simp]:
1.11 -  "a div 1 = a"
1.12 -  using nonzero_mult_divide_cancel_left [of 1 a] by simp
1.13 -
1.14 -lemma dvd_mult_cancel_left [simp]:
1.15 -  assumes "a \<noteq> 0"
1.16 -  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.17 -proof
1.18 -  assume ?P then obtain d where "a * c = a * b * d" ..
1.19 -  with assms have "c = b * d" by (simp add: ac_simps)
1.20 -  then show ?Q ..
1.21 -next
1.22 -  assume ?Q then obtain d where "c = b * d" ..
1.23 -  then have "a * c = a * b * d" by (simp add: ac_simps)
1.24 -  then show ?P ..
1.25 -qed
1.26 -
1.27 -lemma dvd_mult_cancel_right [simp]:
1.28 -  assumes "a \<noteq> 0"
1.29 -  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.30 -using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps)
1.31 -
1.32 -lemma div_dvd_iff_mult:
1.33 -  assumes "b \<noteq> 0" and "b dvd a"
1.34 -  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
1.35 -proof -
1.36 -  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
1.37 -  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
1.38 -qed
1.39 -
1.40 -lemma dvd_div_iff_mult:
1.41 -  assumes "c \<noteq> 0" and "c dvd b"
1.42 -  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
1.43 -proof -
1.44 -  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
1.45 -  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
1.46 -qed
1.47 -
1.48 -end
1.49 -
1.50 -declare One_nat_def [simp del]
1.51 -
1.52  subsection {* GCD and LCM definitions *}
1.53
1.54  class gcd = zero + one + dvd +
1.55 @@ -145,6 +100,10 @@
1.56    with False show ?thesis by simp
1.57  qed
1.58
1.59 +lemma is_unit_gcd [simp]:
1.60 +  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
1.61 +  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
1.62 +
1.63  sublocale gcd!: abel_semigroup gcd
1.64  proof
1.65    fix a b c
1.66 @@ -772,7 +731,7 @@
1.67    by simp
1.68
1.69  lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
1.70 -  by (simp add: One_nat_def)
1.71 +  by simp
1.72
1.73  lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
1.75 @@ -928,23 +887,29 @@
1.76    apply auto
1.77  done
1.78
1.79 -lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
1.80 -  apply (insert gcd_mult_distrib_nat [of m k n])
1.81 -  apply simp
1.82 -  apply (erule_tac t = m in ssubst)
1.83 -  apply simp
1.84 -  done
1.85 +context semiring_gcd
1.86 +begin
1.87
1.88 -lemma coprime_dvd_mult_int:
1.89 -  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
1.90 -apply (subst abs_dvd_iff [symmetric])
1.91 -apply (subst dvd_abs_iff [symmetric])
1.92 -apply (subst (asm) gcd_abs_int)
1.93 -apply (rule coprime_dvd_mult_nat [transferred])
1.94 -    prefer 4 apply assumption
1.95 -   apply auto
1.96 -apply (subst abs_mult [symmetric], auto)
1.97 -done
1.98 +lemma coprime_dvd_mult:
1.99 +  assumes "coprime a b" and "a dvd c * b"
1.100 +  shows "a dvd c"
1.101 +proof (cases "c = 0")
1.102 +  case True then show ?thesis by simp
1.103 +next
1.104 +  case False
1.105 +  then have unit: "is_unit (unit_factor c)" by simp
1.106 +  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
1.107 +  have "gcd (c * a) (c * b) * unit_factor c = c"
1.108 +    by (simp add: ac_simps)
1.109 +  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
1.110 +    by (simp add: dvd_mult_unit_iff unit)
1.111 +  ultimately show ?thesis by simp
1.112 +qed
1.113 +
1.114 +end
1.115 +
1.116 +lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
1.117 +lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
1.118
1.119  lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
1.120      (k dvd m * n) = (k dvd m)"
1.121 @@ -954,21 +919,22 @@
1.122      (k dvd m * n) = (k dvd m)"
1.123    by (auto intro: coprime_dvd_mult_int)
1.124
1.125 -lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
1.126 -  apply (rule dvd_antisym)
1.127 +context semiring_gcd
1.128 +begin
1.129 +
1.130 +lemma gcd_mult_cancel:
1.131 +  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
1.132 +  apply (rule associated_eqI)
1.133    apply (rule gcd_greatest)
1.134 -  apply (rule_tac n = k in coprime_dvd_mult_nat)
1.135 -  apply (simp add: gcd_assoc_nat)
1.136 -  apply (simp add: gcd_commute_nat)
1.137 -  apply (simp_all add: mult.commute)
1.138 -done
1.139 +  apply (rule_tac b = c in coprime_dvd_mult)
1.140 +  apply (simp add: gcd.assoc)
1.141 +  apply (simp_all add: ac_simps)
1.142 +  done
1.143
1.144 -lemma gcd_mult_cancel_int:
1.145 -  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
1.146 -apply (subst (1 2) gcd_abs_int)
1.147 -apply (subst abs_mult)
1.148 -apply (rule gcd_mult_cancel_nat [transferred], auto)
1.149 -done
1.150 +end
1.151 +
1.152 +lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat]
1.153 +lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int]
1.154
1.155  lemma coprime_crossproduct_nat:
1.156    fixes a b c d :: nat
1.157 @@ -1121,8 +1087,11 @@
1.158
1.159  subsection {* Coprimality *}
1.160
1.161 -lemma div_gcd_coprime_nat:
1.162 -  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
1.163 +context semiring_gcd
1.164 +begin
1.165 +
1.166 +lemma div_gcd_coprime:
1.167 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
1.168    shows "coprime (a div gcd a b) (b div gcd a b)"
1.169  proof -
1.170    let ?g = "gcd a b"
1.171 @@ -1140,29 +1109,22 @@
1.172      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
1.173        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
1.174    have "?g \<noteq> 0" using nz by simp
1.175 -  then have gp: "?g > 0" by arith
1.176 -  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
1.177 -  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
1.178 +  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
1.179 +  thm dvd_mult_cancel_left
1.180 +  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
1.181  qed
1.182
1.183 -lemma div_gcd_coprime_int:
1.184 -  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
1.185 -  shows "coprime (a div gcd a b) (b div gcd a b)"
1.186 -apply (subst (1 2 3) gcd_abs_int)
1.187 -apply (subst (1 2) abs_div)
1.188 -  apply simp
1.189 - apply simp
1.190 -apply(subst (1 2) abs_gcd_int)
1.191 -apply (rule div_gcd_coprime_nat [transferred])
1.192 -using nz apply (auto simp add: gcd_abs_int [symmetric])
1.193 -done
1.194 +end
1.195 +
1.196 +lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
1.197 +lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
1.198
1.199  lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.200    using gcd_unique_nat[of 1 a b, simplified] by auto
1.201
1.202  lemma coprime_Suc_0_nat:
1.203      "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
1.204 -  using coprime_nat by (simp add: One_nat_def)
1.205 +  using coprime_nat by simp
1.206
1.207  lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
1.208      (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.209 @@ -1211,22 +1173,23 @@
1.210    using z apply force
1.211    done
1.212
1.213 -lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
1.214 -    shows "coprime d (a * b)"
1.215 -  apply (subst gcd_commute_nat)
1.216 -  using da apply (subst gcd_mult_cancel_nat)
1.217 -  apply (subst gcd_commute_nat, assumption)
1.218 -  apply (subst gcd_commute_nat, rule db)
1.219 -done
1.220 +context semiring_gcd
1.221 +begin
1.222
1.223 -lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
1.224 -    shows "coprime d (a * b)"
1.225 -  apply (subst gcd_commute_int)
1.226 -  using da apply (subst gcd_mult_cancel_int)
1.227 -  apply (subst gcd_commute_int, assumption)
1.228 -  apply (subst gcd_commute_int, rule db)
1.229 -done
1.230 +lemma coprime_mult:
1.231 +  assumes da: "coprime d a" and db: "coprime d b"
1.232 +  shows "coprime d (a * b)"
1.233 +  apply (subst gcd.commute)
1.234 +  using da apply (subst gcd_mult_cancel)
1.235 +  apply (subst gcd.commute, assumption)
1.236 +  apply (subst gcd.commute, rule db)
1.237 +  done
1.238
1.239 +end
1.240 +
1.241 +lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
1.242 +lemmas coprime_mult_int = coprime_mult [where ?'a = int]
1.243 +
1.244  lemma coprime_lmult_nat:
1.245    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
1.246  proof -
1.247 @@ -1305,20 +1268,41 @@
1.248  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
1.249    by (induct n) (simp_all add: coprime_mult_int)
1.250
1.251 +context semiring_gcd
1.252 +begin
1.253 +
1.254 +lemma coprime_exp_left:
1.255 +  assumes "coprime a b"
1.256 +  shows "coprime (a ^ n) b"
1.257 +  using assms by (induct n) (simp_all add: gcd_mult_cancel)
1.258 +
1.259 +lemma coprime_exp2:
1.260 +  assumes "coprime a b"
1.261 +  shows "coprime (a ^ n) (b ^ m)"
1.262 +proof (rule coprime_exp_left)
1.263 +  from assms show "coprime a (b ^ m)"
1.264 +    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
1.265 +qed
1.266 +
1.267 +end
1.268 +
1.269  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
1.270 -  by (simp add: coprime_exp_nat ac_simps)
1.271 +  by (fact coprime_exp2)
1.272
1.273  lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
1.274 -  by (simp add: coprime_exp_int ac_simps)
1.275 +  by (fact coprime_exp2)
1.276
1.277 -lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
1.278 -proof (cases)
1.279 -  assume "a = 0 & b = 0"
1.280 -  thus ?thesis by simp
1.281 -  next assume "~(a = 0 & b = 0)"
1.282 -  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
1.283 -    by (auto simp:div_gcd_coprime_nat)
1.284 -  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
1.285 +lemma gcd_exp_nat:
1.286 +  "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
1.287 +proof (cases "a = 0 \<and> b = 0")
1.288 +  case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
1.289 +next
1.290 +  case False
1.291 +  then have "coprime (a div gcd a b) (b div gcd a b)"
1.292 +    by (auto simp: div_gcd_coprime)
1.293 +  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
1.294 +    by (simp add: coprime_exp2)
1.295 +  then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
1.296        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
1.297      by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
1.298    also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
1.299 @@ -1373,7 +1357,7 @@
1.300      with dc have th0: "a' dvd b*c"
1.301        using dvd_trans[of a' a "b*c"] by simp
1.302      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
1.303 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
1.304 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
1.305      with z have th_1: "a' dvd b' * c" by auto
1.306      from coprime_dvd_mult_int[OF ab'(3)] th_1
1.307      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
1.308 @@ -1471,10 +1455,10 @@
1.309  qed
1.310
1.311  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
1.312 -  by (simp add: gcd.commute)
1.313 +  by (simp add: gcd.commute del: One_nat_def)
1.314
1.315  lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
1.316 -  using coprime_plus_one_nat by (simp add: One_nat_def)
1.317 +  using coprime_plus_one_nat by simp
1.318
1.319  lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
1.321 @@ -1850,7 +1834,7 @@
1.322
1.323  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.324    + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
1.325 -  by standard simp_all
1.326 +  by standard (simp_all del: One_nat_def)
1.327
1.328  interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
1.329
1.330 @@ -1950,11 +1934,11 @@
1.331
1.332  lemma Lcm_nat_empty:
1.333    "Lcm {} = (1::nat)"
1.334 -  by (simp add: Lcm_nat_def)
1.335 +  by (simp add: Lcm_nat_def del: One_nat_def)
1.336
1.337  lemma Lcm_nat_insert:
1.338    "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
1.339 -  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
1.340 +  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
1.341
1.342  definition
1.343    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
1.344 @@ -2107,7 +2091,7 @@
1.345  lemma mult_inj_if_coprime_nat:
1.346    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
1.347     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"