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
```