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)"
    1.95    by (simp add: dvd_Gcd_fin_iff)
    1.96 -  
    1.97 +
    1.98  lemma Lcm_fin_dvd_iff:
    1.99    "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
   1.100    using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])