src/HOL/GCD.thy
 changeset 60689 8a2d7c04d8c0 parent 60688 01488b559910 child 60690 a9e45c9588c3
```     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 14:01:41 2015 +0200
1.3 @@ -100,10 +100,18 @@
1.4      and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
1.5  begin
1.6
1.7 -lemma gcd_greatest_iff [iff]:
1.8 +lemma gcd_greatest_iff [simp]:
1.9    "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
1.10    by (blast intro!: gcd_greatest intro: dvd_trans)
1.11
1.12 +lemma gcd_dvdI1:
1.13 +  "a dvd c \<Longrightarrow> gcd a b dvd c"
1.14 +  by (rule dvd_trans) (rule gcd_dvd1)
1.15 +
1.16 +lemma gcd_dvdI2:
1.17 +  "b dvd c \<Longrightarrow> gcd a b dvd c"
1.18 +  by (rule dvd_trans) (rule gcd_dvd2)
1.19 +
1.20  lemma gcd_0_left [simp]:
1.21    "gcd 0 a = normalize a"
1.22    by (rule associated_eqI) simp_all
1.23 @@ -202,7 +210,7 @@
1.24    "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
1.25    using mult_gcd_left [of c a b] by (simp add: ac_simps)
1.26
1.27 -lemma lcm_dvd1 [iff]:
1.28 +lemma dvd_lcm1 [iff]:
1.29    "a dvd lcm a b"
1.30  proof -
1.31    have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
1.32 @@ -211,7 +219,7 @@
1.33      by (simp add: lcm_gcd)
1.34  qed
1.35
1.36 -lemma lcm_dvd2 [iff]:
1.37 +lemma dvd_lcm2 [iff]:
1.38    "b dvd lcm a b"
1.39  proof -
1.40    have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
1.41 @@ -220,6 +228,14 @@
1.42      by (simp add: lcm_gcd)
1.43  qed
1.44
1.45 +lemma dvd_lcmI1:
1.46 +  "a dvd b \<Longrightarrow> a dvd lcm b c"
1.47 +  by (rule dvd_trans) (assumption, blast)
1.48 +
1.49 +lemma dvd_lcmI2:
1.50 +  "a dvd c \<Longrightarrow> a dvd lcm b c"
1.51 +  by (rule dvd_trans) (assumption, blast)
1.52 +
1.53  lemma lcm_least:
1.54    assumes "a dvd c" and "b dvd c"
1.55    shows "lcm a b dvd c"
1.56 @@ -246,7 +262,7 @@
1.57    qed
1.58  qed
1.59
1.60 -lemma lcm_least_iff [iff]:
1.61 +lemma lcm_least_iff [simp]:
1.62    "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
1.63    by (blast intro!: lcm_least intro: dvd_trans)
1.64
1.65 @@ -822,18 +838,21 @@
1.66  lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
1.67    by (rule zdvd_imp_le, auto)
1.68
1.69 -lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
1.70 -    (k dvd m & k dvd n)"
1.71 -  by (blast intro!: gcd_greatest intro: dvd_trans)
1.72 +lemma gcd_greatest_iff_nat:
1.73 +  "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)"
1.74 +  by (fact gcd_greatest_iff)
1.75 +
1.76 +lemma gcd_greatest_iff_int:
1.77 +  "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
1.78 +  by (fact gcd_greatest_iff)
1.79
1.80 -lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
1.81 -  by (blast intro!: gcd_greatest intro: dvd_trans)
1.82 +lemma gcd_zero_nat:
1.83 +  "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
1.84 +  by (fact gcd_eq_0_iff)
1.85
1.86 -lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
1.87 -  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
1.88 -
1.89 -lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
1.90 -  by (auto simp add: gcd_int_def)
1.91 +lemma gcd_zero_int [simp]:
1.92 +  "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
1.93 +  by (fact gcd_eq_0_iff)
1.94
1.95  lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
1.96    by (insert gcd_zero_nat [of m n], arith)
1.97 @@ -1042,8 +1061,7 @@
1.98  (* to do: differences, and all variations of addition rules
1.99      as simplification rules for nat and int *)
1.100
1.101 -(* FIXME remove iff *)
1.102 -lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
1.103 +lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
1.104    using mult_dvd_mono [of 1] by auto
1.105
1.106  (* to do: add the three variations of these, and for ints? *)
1.107 @@ -1799,39 +1817,16 @@
1.108    by (rule lcm_least)
1.109
1.110  lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
1.111 -proof (cases m)
1.112 -  case 0 then show ?thesis by simp
1.113 -next
1.114 -  case (Suc _)
1.115 -  then have mpos: "m > 0" by simp
1.116 -  show ?thesis
1.117 -  proof (cases n)
1.118 -    case 0 then show ?thesis by simp
1.119 -  next
1.120 -    case (Suc _)
1.121 -    then have npos: "n > 0" by simp
1.122 -    have "gcd m n dvd n" by simp
1.123 -    then obtain k where "n = gcd m n * k" using dvd_def by auto
1.124 -    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
1.125 -      by (simp add: ac_simps)
1.126 -    also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
1.127 -    finally show ?thesis by (simp add: lcm_nat_def)
1.128 -  qed
1.129 -qed
1.130 +  by (fact dvd_lcm1)
1.131
1.132  lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
1.133 -  apply (subst lcm_abs_int)
1.134 -  apply (rule dvd_trans)
1.135 -  prefer 2
1.136 -  apply (rule lcm_dvd1_nat [transferred])
1.137 -  apply auto
1.138 -done
1.139 +  by (fact dvd_lcm1)
1.140
1.141  lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
1.142 -  by (rule lcm_dvd2)
1.143 +  by (fact dvd_lcm2)
1.144
1.145  lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
1.146 -  by (rule lcm_dvd2)
1.147 +  by (fact dvd_lcm2)
1.148
1.149  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
1.150  by(metis lcm_dvd1_nat dvd_trans)
```