src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60690 a9e45c9588c3
parent 60688 01488b559910
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 20:19:12 2015 +0200
     1.3 @@ -794,15 +794,15 @@
     1.4  
     1.5  lemma dvd_lcm_D1:
     1.6    "lcm m n dvd k \<Longrightarrow> m dvd k"
     1.7 -  by (rule dvd_trans, rule lcm_dvd1, assumption)
     1.8 +  by (rule dvd_trans, rule dvd_lcm1, assumption)
     1.9  
    1.10  lemma dvd_lcm_D2:
    1.11    "lcm m n dvd k \<Longrightarrow> n dvd k"
    1.12 -  by (rule dvd_trans, rule lcm_dvd2, assumption)
    1.13 +  by (rule dvd_trans, rule dvd_lcm2, assumption)
    1.14  
    1.15  lemma gcd_dvd_lcm [simp]:
    1.16    "gcd a b dvd lcm a b"
    1.17 -  by (metis dvd_trans gcd_dvd2 lcm_dvd2)
    1.18 +  using gcd_dvd2 by (rule dvd_lcmI2)
    1.19  
    1.20  lemma lcm_1_iff:
    1.21    "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
    1.22 @@ -830,14 +830,6 @@
    1.23    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.24    by rule (auto intro: lcmI simp: lcm_least lcm_zero)
    1.25  
    1.26 -lemma dvd_lcm_I1 [simp]:
    1.27 -  "k dvd m \<Longrightarrow> k dvd lcm m n"
    1.28 -  by (metis lcm_dvd1 dvd_trans)
    1.29 -
    1.30 -lemma dvd_lcm_I2 [simp]:
    1.31 -  "k dvd n \<Longrightarrow> k dvd lcm m n"
    1.32 -  by (metis lcm_dvd2 dvd_trans)
    1.33 -
    1.34  lemma lcm_coprime:
    1.35    "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
    1.36    by (subst lcm_gcd) simp
    1.37 @@ -874,8 +866,8 @@
    1.38    assumes "a \<noteq> 0" and "b \<noteq> 0"
    1.39    shows "euclidean_size a \<le> euclidean_size (lcm a b)"
    1.40  proof -
    1.41 -  have "a dvd lcm a b" by (rule lcm_dvd1)
    1.42 -  then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
    1.43 +  have "a dvd lcm a b" by (rule dvd_lcm1)
    1.44 +  then obtain c where A: "lcm a b = a * c" ..
    1.45    with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
    1.46    then show ?thesis by (subst A, intro size_mult_mono)
    1.47  qed
    1.48 @@ -905,12 +897,7 @@
    1.49  
    1.50  lemma lcm_mult_unit1:
    1.51    "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
    1.52 -  apply (rule lcmI)
    1.53 -  apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
    1.54 -  apply (rule lcm_dvd2)
    1.55 -  apply (rule lcm_least, simp add: unit_simps, assumption)
    1.56 -  apply simp
    1.57 -  done
    1.58 +  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
    1.59  
    1.60  lemma lcm_mult_unit2:
    1.61    "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
    1.62 @@ -944,22 +931,11 @@
    1.63  
    1.64  lemma lcm_left_idem:
    1.65    "lcm a (lcm a b) = lcm a b"
    1.66 -  apply (rule lcmI)
    1.67 -  apply simp
    1.68 -  apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
    1.69 -  apply (rule lcm_least, assumption)
    1.70 -  apply (erule (1) lcm_least)
    1.71 -  apply (auto simp: lcm_zero)
    1.72 -  done
    1.73 +  by (rule associated_eqI) simp_all
    1.74  
    1.75  lemma lcm_right_idem:
    1.76    "lcm (lcm a b) b = lcm a b"
    1.77 -  apply (rule lcmI)
    1.78 -  apply (subst lcm.assoc, rule lcm_dvd1)
    1.79 -  apply (rule lcm_dvd2)
    1.80 -  apply (rule lcm_least, erule (1) lcm_least, assumption)
    1.81 -  apply (auto simp: lcm_zero)
    1.82 -  done
    1.83 +  by (rule associated_eqI) simp_all
    1.84  
    1.85  lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
    1.86  proof
    1.87 @@ -1012,10 +988,10 @@
    1.88          also note \<open>euclidean_size l = n\<close>
    1.89          finally show "euclidean_size (gcd l l') \<le> n" .
    1.90        qed
    1.91 -      ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
    1.92 +      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
    1.93          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
    1.94 -      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
    1.95 -        using dvd_euclidean_size_eq_imp_dvd by auto
    1.96 +      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
    1.97 +        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
    1.98        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
    1.99      }
   1.100