src/HOL/GCD.thy
 changeset 65555 85ed070017b7 parent 65552 f533820e7248 child 65811 2653f1cd8775
```     1.1 --- a/src/HOL/GCD.thy	Sun Apr 23 14:27:22 2017 +0200
1.2 +++ b/src/HOL/GCD.thy	Sun Apr 23 14:53:33 2017 +0200
1.3 @@ -31,21 +31,21 @@
1.4  section \<open>Greatest common divisor and least common multiple\<close>
1.5
1.6  theory GCD
1.7 -  imports Pre_Main
1.8 +  imports Groups_List
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 -  fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
1.15 +  fixes top :: 'a  ("\<^bold>\<top>") and bot :: 'a  ("\<^bold>\<bottom>")
1.16      and normalize :: "'a \<Rightarrow> 'a"
1.17    assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
1.18      and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
1.19      and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
1.20 -    and normalize_top [simp]: "normalize \<top> = \<top>"
1.21 -    and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
1.22 -    and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
1.23 -    and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
1.24 +    and normalize_top [simp]: "normalize \<^bold>\<top> = \<^bold>\<top>"
1.25 +    and normalize_bottom [simp]: "normalize \<^bold>\<bottom> = \<^bold>\<bottom>"
1.26 +    and top_left_normalize [simp]: "\<^bold>\<top> \<^bold>* a = normalize a"
1.27 +    and bottom_left_bottom [simp]: "\<^bold>\<bottom> \<^bold>* a = \<^bold>\<bottom>"
1.28  begin
1.29
1.30  lemma left_idem [simp]:
1.31 @@ -63,11 +63,11 @@
1.32    by (fact comp_fun_idem)
1.33
1.34  lemma top_right_normalize [simp]:
1.35 -  "a \<^bold>* \<top> = normalize a"
1.36 +  "a \<^bold>* \<^bold>\<top> = normalize a"
1.37    using top_left_normalize [of a] by (simp add: ac_simps)
1.38
1.39  lemma bottom_right_bottom [simp]:
1.40 -  "a \<^bold>* \<bottom> = \<bottom>"
1.41 +  "a \<^bold>* \<^bold>\<bottom> = \<^bold>\<bottom>"
1.42    using bottom_left_bottom [of a] by (simp add: ac_simps)
1.43
1.44  lemma normalize_right_idem [simp]:
1.45 @@ -84,18 +84,18 @@
1.46
1.47  definition F :: "'a set \<Rightarrow> 'a"
1.48  where
1.49 -  eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
1.50 +  eq_fold: "F A = (if finite A then Finite_Set.fold f \<^bold>\<top> A else \<^bold>\<bottom>)"
1.51 +
1.52 +lemma infinite [simp]:
1.53 +  "infinite A \<Longrightarrow> F A = \<^bold>\<bottom>"
1.54 +  by (simp add: eq_fold)
1.55
1.56  lemma set_eq_fold [code]:
1.57 -  "F (set xs) = fold f xs \<top>"
1.58 +  "F (set xs) = fold f xs \<^bold>\<top>"
1.59    by (simp add: eq_fold fold_set_fold)
1.60
1.61 -lemma infinite [simp]:
1.62 -  "infinite A \<Longrightarrow> F A = \<bottom>"
1.63 -  by (simp add: eq_fold)
1.64 -
1.65  lemma empty [simp]:
1.66 -  "F {} = \<top>"
1.67 +  "F {} = \<^bold>\<top>"
1.69
1.70  lemma insert [simp]:
1.71 @@ -908,7 +908,7 @@
1.72    from ab'(1) have "a' dvd a"
1.73      unfolding dvd_def by blast
1.74    with assms have "a' dvd b * c"
1.75 -    using dvd_trans[of a' a "b*c"] by simp
1.76 +    using dvd_trans [of a' a "b * c"] by simp
1.77    from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
1.78      by simp
1.79    then have "?d * a' dvd ?d * (b' * c)"
1.80 @@ -2663,16 +2663,6 @@
1.81    by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
1.82
1.83
1.84 -text \<open>Nitpick:\<close>
1.85 -
1.86 -lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
1.87 -  by (induct x y rule: nat_gcd.induct)
1.88 -    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
1.89 -
1.90 -lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
1.91 -  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
1.92 -
1.93 -
1.94  subsubsection \<open>Setwise GCD and LCM for integers\<close>
1.95
1.96  instantiation int :: semiring_Gcd
```