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.68    by (simp add: eq_fold)
    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