src/HOL/Library/Countable_Complete_Lattices.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (19 months ago) changeset 67951 655aa11359dc parent 62390 842917225d56 child 69260 0a9688695a1b permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
 hoelzl@62373 ` 1` ```(* Title: HOL/Library/Countable_Complete_Lattices.thy ``` hoelzl@62373 ` 2` ``` Author: Johannes Hölzl ``` hoelzl@62373 ` 3` ```*) ``` hoelzl@62373 ` 4` hoelzl@62373 ` 5` ```section \Countable Complete Lattices\ ``` hoelzl@62373 ` 6` hoelzl@62373 ` 7` ```theory Countable_Complete_Lattices ``` hoelzl@62374 ` 8` ``` imports Main Countable_Set ``` hoelzl@62373 ` 9` ```begin ``` hoelzl@62373 ` 10` hoelzl@62373 ` 11` ```lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)" ``` hoelzl@62373 ` 12` ``` by (metis UNIV_eq_I nat.nchotomy insertCI rangeI) ``` hoelzl@62373 ` 13` hoelzl@62373 ` 14` ```class countable_complete_lattice = lattice + Inf + Sup + bot + top + ``` hoelzl@62374 ` 15` ``` assumes ccInf_lower: "countable A \ x \ A \ Inf A \ x" ``` hoelzl@62374 ` 16` ``` assumes ccInf_greatest: "countable A \ (\x. x \ A \ z \ x) \ z \ Inf A" ``` hoelzl@62374 ` 17` ``` assumes ccSup_upper: "countable A \ x \ A \ x \ Sup A" ``` hoelzl@62374 ` 18` ``` assumes ccSup_least: "countable A \ (\x. x \ A \ x \ z) \ Sup A \ z" ``` hoelzl@62374 ` 19` ``` assumes ccInf_empty [simp]: "Inf {} = top" ``` hoelzl@62374 ` 20` ``` assumes ccSup_empty [simp]: "Sup {} = bot" ``` hoelzl@62373 ` 21` ```begin ``` hoelzl@62373 ` 22` hoelzl@62373 ` 23` ```subclass bounded_lattice ``` hoelzl@62373 ` 24` ```proof ``` hoelzl@62373 ` 25` ``` fix a ``` hoelzl@62374 ` 26` ``` show "bot \ a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric]) ``` hoelzl@62374 ` 27` ``` show "a \ top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric]) ``` hoelzl@62373 ` 28` ```qed ``` hoelzl@62373 ` 29` hoelzl@62374 ` 30` ```lemma ccINF_lower: "countable A \ i \ A \ (INF i :A. f i) \ f i" ``` hoelzl@62373 ` 31` ``` using ccInf_lower [of "f ` A"] by simp ``` hoelzl@62373 ` 32` hoelzl@62374 ` 33` ```lemma ccINF_greatest: "countable A \ (\i. i \ A \ u \ f i) \ u \ (INF i :A. f i)" ``` hoelzl@62373 ` 34` ``` using ccInf_greatest [of "f ` A"] by auto ``` hoelzl@62373 ` 35` hoelzl@62374 ` 36` ```lemma ccSUP_upper: "countable A \ i \ A \ f i \ (SUP i :A. f i)" ``` hoelzl@62373 ` 37` ``` using ccSup_upper [of "f ` A"] by simp ``` hoelzl@62373 ` 38` hoelzl@62374 ` 39` ```lemma ccSUP_least: "countable A \ (\i. i \ A \ f i \ u) \ (SUP i :A. f i) \ u" ``` hoelzl@62373 ` 40` ``` using ccSup_least [of "f ` A"] by auto ``` hoelzl@62373 ` 41` hoelzl@62374 ` 42` ```lemma ccInf_lower2: "countable A \ u \ A \ u \ v \ Inf A \ v" ``` hoelzl@62373 ` 43` ``` using ccInf_lower [of A u] by auto ``` hoelzl@62373 ` 44` hoelzl@62374 ` 45` ```lemma ccINF_lower2: "countable A \ i \ A \ f i \ u \ (INF i :A. f i) \ u" ``` hoelzl@62373 ` 46` ``` using ccINF_lower [of A i f] by auto ``` hoelzl@62373 ` 47` hoelzl@62374 ` 48` ```lemma ccSup_upper2: "countable A \ u \ A \ v \ u \ v \ Sup A" ``` hoelzl@62373 ` 49` ``` using ccSup_upper [of A u] by auto ``` hoelzl@62373 ` 50` hoelzl@62374 ` 51` ```lemma ccSUP_upper2: "countable A \ i \ A \ u \ f i \ u \ (SUP i :A. f i)" ``` hoelzl@62373 ` 52` ``` using ccSUP_upper [of A i f] by auto ``` hoelzl@62373 ` 53` hoelzl@62374 ` 54` ```lemma le_ccInf_iff: "countable A \ b \ Inf A \ (\a\A. b \ a)" ``` hoelzl@62373 ` 55` ``` by (auto intro: ccInf_greatest dest: ccInf_lower) ``` hoelzl@62373 ` 56` hoelzl@62374 ` 57` ```lemma le_ccINF_iff: "countable A \ u \ (INF i :A. f i) \ (\i\A. u \ f i)" ``` hoelzl@62373 ` 58` ``` using le_ccInf_iff [of "f ` A"] by simp ``` hoelzl@62373 ` 59` hoelzl@62374 ` 60` ```lemma ccSup_le_iff: "countable A \ Sup A \ b \ (\a\A. a \ b)" ``` hoelzl@62373 ` 61` ``` by (auto intro: ccSup_least dest: ccSup_upper) ``` hoelzl@62373 ` 62` hoelzl@62374 ` 63` ```lemma ccSUP_le_iff: "countable A \ (SUP i :A. f i) \ u \ (\i\A. f i \ u)" ``` hoelzl@62373 ` 64` ``` using ccSup_le_iff [of "f ` A"] by simp ``` hoelzl@62373 ` 65` hoelzl@62374 ` 66` ```lemma ccInf_insert [simp]: "countable A \ Inf (insert a A) = inf a (Inf A)" ``` hoelzl@62373 ` 67` ``` by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower) ``` hoelzl@62373 ` 68` hoelzl@62374 ` 69` ```lemma ccINF_insert [simp]: "countable A \ (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)" ``` hoelzl@62373 ` 70` ``` unfolding image_insert by simp ``` hoelzl@62373 ` 71` hoelzl@62374 ` 72` ```lemma ccSup_insert [simp]: "countable A \ Sup (insert a A) = sup a (Sup A)" ``` hoelzl@62373 ` 73` ``` by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper) ``` hoelzl@62373 ` 74` hoelzl@62374 ` 75` ```lemma ccSUP_insert [simp]: "countable A \ (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)" ``` hoelzl@62373 ` 76` ``` unfolding image_insert by simp ``` hoelzl@62373 ` 77` hoelzl@62374 ` 78` ```lemma ccINF_empty [simp]: "(INF x:{}. f x) = top" ``` hoelzl@62373 ` 79` ``` unfolding image_empty by simp ``` hoelzl@62373 ` 80` hoelzl@62374 ` 81` ```lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot" ``` hoelzl@62373 ` 82` ``` unfolding image_empty by simp ``` hoelzl@62373 ` 83` hoelzl@62374 ` 84` ```lemma ccInf_superset_mono: "countable A \ B \ A \ Inf A \ Inf B" ``` hoelzl@62373 ` 85` ``` by (auto intro: ccInf_greatest ccInf_lower countable_subset) ``` hoelzl@62373 ` 86` hoelzl@62374 ` 87` ```lemma ccSup_subset_mono: "countable B \ A \ B \ Sup A \ Sup B" ``` hoelzl@62373 ` 88` ``` by (auto intro: ccSup_least ccSup_upper countable_subset) ``` hoelzl@62373 ` 89` hoelzl@62373 ` 90` ```lemma ccInf_mono: ``` hoelzl@62373 ` 91` ``` assumes [intro]: "countable B" "countable A" ``` hoelzl@62373 ` 92` ``` assumes "\b. b \ B \ \a\A. a \ b" ``` hoelzl@62374 ` 93` ``` shows "Inf A \ Inf B" ``` hoelzl@62373 ` 94` ```proof (rule ccInf_greatest) ``` hoelzl@62373 ` 95` ``` fix b assume "b \ B" ``` hoelzl@62373 ` 96` ``` with assms obtain a where "a \ A" and "a \ b" by blast ``` hoelzl@62374 ` 97` ``` from \a \ A\ have "Inf A \ a" by (rule ccInf_lower[rotated]) auto ``` hoelzl@62374 ` 98` ``` with \a \ b\ show "Inf A \ b" by auto ``` hoelzl@62373 ` 99` ```qed auto ``` hoelzl@62373 ` 100` hoelzl@62373 ` 101` ```lemma ccINF_mono: ``` hoelzl@62374 ` 102` ``` "countable A \ countable B \ (\m. m \ B \ \n\A. f n \ g m) \ (INF n:A. f n) \ (INF n:B. g n)" ``` hoelzl@62373 ` 103` ``` using ccInf_mono [of "g ` B" "f ` A"] by auto ``` hoelzl@62373 ` 104` hoelzl@62373 ` 105` ```lemma ccSup_mono: ``` hoelzl@62373 ` 106` ``` assumes [intro]: "countable B" "countable A" ``` hoelzl@62373 ` 107` ``` assumes "\a. a \ A \ \b\B. a \ b" ``` hoelzl@62374 ` 108` ``` shows "Sup A \ Sup B" ``` hoelzl@62373 ` 109` ```proof (rule ccSup_least) ``` hoelzl@62373 ` 110` ``` fix a assume "a \ A" ``` hoelzl@62373 ` 111` ``` with assms obtain b where "b \ B" and "a \ b" by blast ``` hoelzl@62374 ` 112` ``` from \b \ B\ have "b \ Sup B" by (rule ccSup_upper[rotated]) auto ``` hoelzl@62374 ` 113` ``` with \a \ b\ show "a \ Sup B" by auto ``` hoelzl@62373 ` 114` ```qed auto ``` hoelzl@62373 ` 115` hoelzl@62373 ` 116` ```lemma ccSUP_mono: ``` hoelzl@62374 ` 117` ``` "countable A \ countable B \ (\n. n \ A \ \m\B. f n \ g m) \ (SUP n:A. f n) \ (SUP n:B. g n)" ``` hoelzl@62373 ` 118` ``` using ccSup_mono [of "g ` B" "f ` A"] by auto ``` hoelzl@62373 ` 119` hoelzl@62373 ` 120` ```lemma ccINF_superset_mono: ``` hoelzl@62374 ` 121` ``` "countable A \ B \ A \ (\x. x \ B \ f x \ g x) \ (INF x:A. f x) \ (INF x:B. g x)" ``` hoelzl@62373 ` 122` ``` by (blast intro: ccINF_mono countable_subset dest: subsetD) ``` hoelzl@62373 ` 123` hoelzl@62373 ` 124` ```lemma ccSUP_subset_mono: ``` hoelzl@62374 ` 125` ``` "countable B \ A \ B \ (\x. x \ A \ f x \ g x) \ (SUP x:A. f x) \ (SUP x:B. g x)" ``` hoelzl@62373 ` 126` ``` by (blast intro: ccSUP_mono countable_subset dest: subsetD) ``` hoelzl@62373 ` 127` hoelzl@62373 ` 128` hoelzl@62374 ` 129` ```lemma less_eq_ccInf_inter: "countable A \ countable B \ sup (Inf A) (Inf B) \ Inf (A \ B)" ``` hoelzl@62373 ` 130` ``` by (auto intro: ccInf_greatest ccInf_lower) ``` hoelzl@62373 ` 131` hoelzl@62374 ` 132` ```lemma ccSup_inter_less_eq: "countable A \ countable B \ Sup (A \ B) \ inf (Sup A) (Sup B)" ``` hoelzl@62373 ` 133` ``` by (auto intro: ccSup_least ccSup_upper) ``` hoelzl@62373 ` 134` hoelzl@62374 ` 135` ```lemma ccInf_union_distrib: "countable A \ countable B \ Inf (A \ B) = inf (Inf A) (Inf B)" ``` hoelzl@62373 ` 136` ``` by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2) ``` hoelzl@62373 ` 137` hoelzl@62373 ` 138` ```lemma ccINF_union: ``` hoelzl@62374 ` 139` ``` "countable A \ countable B \ (INF i:A \ B. M i) = inf (INF i:A. M i) (INF i:B. M i)" ``` hoelzl@62373 ` 140` ``` by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower) ``` hoelzl@62373 ` 141` hoelzl@62374 ` 142` ```lemma ccSup_union_distrib: "countable A \ countable B \ Sup (A \ B) = sup (Sup A) (Sup B)" ``` hoelzl@62373 ` 143` ``` by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2) ``` hoelzl@62373 ` 144` hoelzl@62373 ` 145` ```lemma ccSUP_union: ``` hoelzl@62374 ` 146` ``` "countable A \ countable B \ (SUP i:A \ B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)" ``` hoelzl@62373 ` 147` ``` by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper) ``` hoelzl@62373 ` 148` hoelzl@62374 ` 149` ```lemma ccINF_inf_distrib: "countable A \ inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))" ``` hoelzl@62373 ` 150` ``` by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono) ``` hoelzl@62373 ` 151` hoelzl@62374 ` 152` ```lemma ccSUP_sup_distrib: "countable A \ sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))" ``` hoelzl@62373 ` 153` ``` by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono) ``` hoelzl@62373 ` 154` hoelzl@62374 ` 155` ```lemma ccINF_const [simp]: "A \ {} \ (INF i :A. f) = f" ``` hoelzl@62373 ` 156` ``` unfolding image_constant_conv by auto ``` hoelzl@62373 ` 157` hoelzl@62374 ` 158` ```lemma ccSUP_const [simp]: "A \ {} \ (SUP i :A. f) = f" ``` hoelzl@62373 ` 159` ``` unfolding image_constant_conv by auto ``` hoelzl@62373 ` 160` hoelzl@62374 ` 161` ```lemma ccINF_top [simp]: "(INF x:A. top) = top" ``` hoelzl@62373 ` 162` ``` by (cases "A = {}") simp_all ``` hoelzl@62373 ` 163` hoelzl@62374 ` 164` ```lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot" ``` hoelzl@62373 ` 165` ``` by (cases "A = {}") simp_all ``` hoelzl@62373 ` 166` hoelzl@62374 ` 167` ```lemma ccINF_commute: "countable A \ countable B \ (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" ``` hoelzl@62373 ` 168` ``` by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym) ``` hoelzl@62373 ` 169` hoelzl@62374 ` 170` ```lemma ccSUP_commute: "countable A \ countable B \ (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" ``` hoelzl@62373 ` 171` ``` by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym) ``` hoelzl@62373 ` 172` hoelzl@62373 ` 173` ```end ``` hoelzl@62373 ` 174` hoelzl@62373 ` 175` ```context ``` hoelzl@62373 ` 176` ``` fixes a :: "'a::{countable_complete_lattice, linorder}" ``` hoelzl@62373 ` 177` ```begin ``` hoelzl@62373 ` 178` hoelzl@62374 ` 179` ```lemma less_ccSup_iff: "countable S \ a < Sup S \ (\x\S. a < x)" ``` hoelzl@62373 ` 180` ``` unfolding not_le [symmetric] by (subst ccSup_le_iff) auto ``` hoelzl@62373 ` 181` hoelzl@62374 ` 182` ```lemma less_ccSUP_iff: "countable A \ a < (SUP i:A. f i) \ (\x\A. a < f x)" ``` hoelzl@62373 ` 183` ``` using less_ccSup_iff [of "f ` A"] by simp ``` hoelzl@62373 ` 184` hoelzl@62374 ` 185` ```lemma ccInf_less_iff: "countable S \ Inf S < a \ (\x\S. x < a)" ``` hoelzl@62373 ` 186` ``` unfolding not_le [symmetric] by (subst le_ccInf_iff) auto ``` hoelzl@62373 ` 187` hoelzl@62374 ` 188` ```lemma ccINF_less_iff: "countable A \ (INF i:A. f i) < a \ (\x\A. f x < a)" ``` hoelzl@62373 ` 189` ``` using ccInf_less_iff [of "f ` A"] by simp ``` hoelzl@62373 ` 190` hoelzl@62373 ` 191` ```end ``` hoelzl@62373 ` 192` hoelzl@62373 ` 193` ```class countable_complete_distrib_lattice = countable_complete_lattice + ``` hoelzl@62374 ` 194` ``` assumes sup_ccInf: "countable B \ sup a (Inf B) = (INF b:B. sup a b)" ``` hoelzl@62374 ` 195` ``` assumes inf_ccSup: "countable B \ inf a (Sup B) = (SUP b:B. inf a b)" ``` hoelzl@62373 ` 196` ```begin ``` hoelzl@62373 ` 197` hoelzl@62373 ` 198` ```lemma sup_ccINF: ``` hoelzl@62374 ` 199` ``` "countable B \ sup a (INF b:B. f b) = (INF b:B. sup a (f b))" ``` hoelzl@62373 ` 200` ``` by (simp only: sup_ccInf image_image countable_image) ``` hoelzl@62373 ` 201` hoelzl@62373 ` 202` ```lemma inf_ccSUP: ``` hoelzl@62374 ` 203` ``` "countable B \ inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))" ``` hoelzl@62373 ` 204` ``` by (simp only: inf_ccSup image_image countable_image) ``` hoelzl@62373 ` 205` hoelzl@62374 ` 206` ```subclass distrib_lattice ``` hoelzl@62374 ` 207` ```proof ``` hoelzl@62373 ` 208` ``` fix a b c ``` hoelzl@62374 ` 209` ``` from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)" ``` hoelzl@62373 ` 210` ``` by simp ``` hoelzl@62374 ` 211` ``` then show "sup a (inf b c) = inf (sup a b) (sup a c)" ``` hoelzl@62374 ` 212` ``` by simp ``` hoelzl@62373 ` 213` ```qed ``` hoelzl@62373 ` 214` hoelzl@62373 ` 215` ```lemma ccInf_sup: ``` hoelzl@62374 ` 216` ``` "countable B \ sup (Inf B) a = (INF b:B. sup b a)" ``` hoelzl@62373 ` 217` ``` by (simp add: sup_ccInf sup_commute) ``` hoelzl@62373 ` 218` hoelzl@62373 ` 219` ```lemma ccSup_inf: ``` hoelzl@62374 ` 220` ``` "countable B \ inf (Sup B) a = (SUP b:B. inf b a)" ``` hoelzl@62373 ` 221` ``` by (simp add: inf_ccSup inf_commute) ``` hoelzl@62373 ` 222` hoelzl@62373 ` 223` ```lemma ccINF_sup: ``` hoelzl@62374 ` 224` ``` "countable B \ sup (INF b:B. f b) a = (INF b:B. sup (f b) a)" ``` hoelzl@62373 ` 225` ``` by (simp add: sup_ccINF sup_commute) ``` hoelzl@62373 ` 226` hoelzl@62373 ` 227` ```lemma ccSUP_inf: ``` hoelzl@62374 ` 228` ``` "countable B \ inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)" ``` hoelzl@62373 ` 229` ``` by (simp add: inf_ccSUP inf_commute) ``` hoelzl@62373 ` 230` hoelzl@62373 ` 231` ```lemma ccINF_sup_distrib2: ``` hoelzl@62374 ` 232` ``` "countable A \ countable B \ sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))" ``` hoelzl@62373 ` 233` ``` by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup) ``` hoelzl@62373 ` 234` hoelzl@62373 ` 235` ```lemma ccSUP_inf_distrib2: ``` hoelzl@62374 ` 236` ``` "countable A \ countable B \ inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))" ``` hoelzl@62373 ` 237` ``` by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf) ``` hoelzl@62373 ` 238` hoelzl@62373 ` 239` ```context ``` hoelzl@62373 ` 240` ``` fixes f :: "'a \ 'b::countable_complete_lattice" ``` hoelzl@62373 ` 241` ``` assumes "mono f" ``` hoelzl@62373 ` 242` ```begin ``` hoelzl@62373 ` 243` hoelzl@62373 ` 244` ```lemma mono_ccInf: ``` hoelzl@62374 ` 245` ``` "countable A \ f (Inf A) \ (INF x:A. f x)" ``` hoelzl@62373 ` 246` ``` using \mono f\ ``` hoelzl@62373 ` 247` ``` by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD) ``` hoelzl@62373 ` 248` hoelzl@62373 ` 249` ```lemma mono_ccSup: ``` hoelzl@62374 ` 250` ``` "countable A \ (SUP x:A. f x) \ f (Sup A)" ``` hoelzl@62373 ` 251` ``` using \mono f\ by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD) ``` hoelzl@62373 ` 252` hoelzl@62373 ` 253` ```lemma mono_ccINF: ``` hoelzl@62373 ` 254` ``` "countable I \ f (INF i : I. A i) \ (INF x : I. f (A x))" ``` hoelzl@62373 ` 255` ``` by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \mono f\] ccINF_lower) ``` hoelzl@62373 ` 256` hoelzl@62373 ` 257` ```lemma mono_ccSUP: ``` hoelzl@62373 ` 258` ``` "countable I \ (SUP x : I. f (A x)) \ f (SUP i : I. A i)" ``` hoelzl@62373 ` 259` ``` by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \mono f\] ccSUP_upper) ``` hoelzl@62373 ` 260` hoelzl@62373 ` 261` ```end ``` hoelzl@62373 ` 262` hoelzl@62373 ` 263` ```end ``` hoelzl@62373 ` 264` hoelzl@62373 ` 265` ```subsubsection \Instances of countable complete lattices\ ``` hoelzl@62373 ` 266` hoelzl@62373 ` 267` ```instance "fun" :: (type, countable_complete_lattice) countable_complete_lattice ``` hoelzl@62373 ` 268` ``` by standard ``` hoelzl@62373 ` 269` ``` (auto simp: le_fun_def intro!: ccSUP_upper ccSUP_least ccINF_lower ccINF_greatest) ``` hoelzl@62373 ` 270` hoelzl@62373 ` 271` ```subclass (in complete_lattice) countable_complete_lattice ``` hoelzl@62373 ` 272` ``` by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) ``` hoelzl@62373 ` 273` hoelzl@62373 ` 274` ```subclass (in complete_distrib_lattice) countable_complete_distrib_lattice ``` hoelzl@62373 ` 275` ``` by standard (auto intro: sup_Inf inf_Sup) ``` hoelzl@62373 ` 276` nipkow@62390 ` 277` ```end ```