src/HOL/GCD.thy
changeset 62343 24106dc44def
parent 61975 b4b11391c676
child 62344 759d684c0e60
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -1990,6 +1990,8 @@
     1.4  definition
     1.5    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
     1.6  
     1.7 +interpretation bla: semilattice_neutr_set gcd "0::nat" ..
     1.8 +
     1.9  instance ..
    1.10  
    1.11  end
    1.12 @@ -2012,19 +2014,7 @@
    1.13  
    1.14  interpretation gcd_lcm_complete_lattice_nat:
    1.15    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
    1.16 -rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    1.17 -  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    1.18 -proof -
    1.19 -  show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    1.20 -    by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
    1.21 -  then interpret gcd_lcm_complete_lattice_nat:
    1.22 -    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
    1.23 -  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
    1.24 -  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
    1.25 -qed
    1.26 -
    1.27 -declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
    1.28 -declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
    1.29 +  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
    1.30  
    1.31  lemma Lcm_empty_nat:
    1.32    "Lcm {} = (1::nat)"