# HG changeset patch # User haftmann # Date 1254852008 -7200 # Node ID bfb3e24a4936145708298612e26e3a7665dc4381 # Parent 13b153243ed463b93757842179faf514a56d0444# Parent 7f5ce7af45fdf929da09fe672b4239ccc312d445 merged diff -r 13b153243ed4 -r bfb3e24a4936 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Tue Oct 06 18:27:00 2009 +0200 +++ b/src/HOL/Complete_Lattice.thy Tue Oct 06 20:00:08 2009 +0200 @@ -15,21 +15,25 @@ bot ("\") +subsection {* Syntactic infimum and supremum operations *} + +class Inf = + fixes Inf :: "'a set \ 'a" ("\_" [900] 900) + +class Sup = + fixes Sup :: "'a set \ 'a" ("\_" [900] 900) + subsection {* Abstract complete lattices *} -class complete_lattice = lattice + bot + top + - fixes Inf :: "'a set \ 'a" ("\_" [900] 900) - and Sup :: "'a set \ 'a" ("\_" [900] 900) +class complete_lattice = lattice + bot + top + Inf + Sup + assumes Inf_lower: "x \ A \ \A \ x" and Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A" assumes Sup_upper: "x \ A \ x \ \A" and Sup_least: "(\x. x \ A \ x \ z) \ \A \ z" begin -term complete_lattice - lemma dual_complete_lattice: - "complete_lattice (op \) (op >) (op \) (op \) \ \ Sup Inf" + "complete_lattice Sup Inf (op \) (op >) (op \) (op \) \ \" by (auto intro!: complete_lattice.intro dual_lattice bot.intro top.intro dual_preorder, unfold_locales) (fact bot_least top_greatest diff -r 13b153243ed4 -r bfb3e24a4936 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Tue Oct 06 18:27:00 2009 +0200 +++ b/src/HOL/GCD.thy Tue Oct 06 20:00:08 2009 +0200 @@ -1575,7 +1575,7 @@ qed interpretation gcd_lcm_complete_lattice_nat: - complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM + complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 proof case goal1 show ?case by simp next