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)