src/HOL/GCD.thy
 changeset 65552 f533820e7248 parent 64850 fc9265882329 child 65555 85ed070017b7
```     1.1 --- a/src/HOL/GCD.thy	Sat Apr 22 12:52:55 2017 +0200
1.2 +++ b/src/HOL/GCD.thy	Sat Apr 22 22:01:35 2017 +0200
1.3 @@ -31,12 +31,12 @@
1.4  section \<open>Greatest common divisor and least common multiple\<close>
1.5
1.6  theory GCD
1.7 -  imports Main
1.8 +  imports Pre_Main
1.9  begin
1.10
1.11  subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
1.12 -
1.13 -locale bounded_quasi_semilattice = abel_semigroup +
1.14 +
1.15 +locale bounded_quasi_semilattice = abel_semigroup +
1.16    fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
1.17      and normalize :: "'a \<Rightarrow> 'a"
1.18    assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
1.19 @@ -65,7 +65,7 @@
1.20  lemma top_right_normalize [simp]:
1.21    "a \<^bold>* \<top> = normalize a"
1.22    using top_left_normalize [of a] by (simp add: ac_simps)
1.23 -
1.24 +
1.25  lemma bottom_right_bottom [simp]:
1.26    "a \<^bold>* \<bottom> = \<bottom>"
1.27    using bottom_left_bottom [of a] by (simp add: ac_simps)
1.28 @@ -74,7 +74,7 @@
1.29    "a \<^bold>* normalize b = a \<^bold>* b"
1.30    using normalize_left_idem [of b a] by (simp add: ac_simps)
1.31
1.32 -end
1.33 +end
1.34
1.35  locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
1.36  begin
1.37 @@ -134,7 +134,7 @@
1.38    assumes "B \<subseteq> A"
1.39    shows "F B \<^bold>* F A = F A"
1.40    using assms by (simp add: union [symmetric] Un_absorb1)
1.41 -
1.42 +
1.43  end
1.44
1.45  subsection \<open>Abstract GCD and LCM\<close>
1.46 @@ -282,7 +282,7 @@
1.47    show "coprime 1 a" for a
1.48      by (rule associated_eqI) simp_all
1.49  qed simp_all
1.50 -
1.51 +
1.52  lemma gcd_self: "gcd a a = normalize a"
1.53    by (fact gcd.idem_normalize)
1.54
1.55 @@ -1071,7 +1071,7 @@
1.56    moreover from assms have "p dvd gcd (b * a) (b * p)"
1.57      by (intro gcd_greatest) (simp_all add: mult.commute)
1.58    hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
1.59 -  with False have "y dvd b"
1.60 +  with False have "y dvd b"
1.61      by (simp add: x_def y_def div_dvd_iff_mult assms)
1.62    ultimately show ?thesis by (rule that)
1.63  qed
1.64 @@ -1527,7 +1527,7 @@
1.65
1.66  end
1.67
1.68 -
1.69 +
1.70  subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
1.71
1.72  context semiring_gcd
1.73 @@ -1546,15 +1546,15 @@
1.74
1.75  abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
1.76    where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
1.77 -
1.78 +
1.79  lemma Gcd_fin_dvd:
1.80    "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
1.81 -  by (induct A rule: infinite_finite_induct)
1.82 +  by (induct A rule: infinite_finite_induct)
1.83      (auto intro: dvd_trans)
1.84
1.85  lemma dvd_Lcm_fin:
1.86    "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
1.87 -  by (induct A rule: infinite_finite_induct)
1.88 +  by (induct A rule: infinite_finite_induct)
1.89      (auto intro: dvd_trans)
1.90
1.91  lemma Gcd_fin_greatest:
1.92 @@ -1580,7 +1580,7 @@
1.93  lemma dvd_gcd_list_iff:
1.94    "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"