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.74    by (simp add: gcd_int_def)
    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.320    by (simp add: gcd.commute)
   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)"
   1.348 -apply(auto simp add:inj_on_def)
   1.349 +apply (auto simp add: inj_on_def simp del: One_nat_def)
   1.350  apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
   1.351  apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
   1.352               dvd.neq_le_trans dvd_triv_right mult.commute)