complete_linorder is also a complete_distrib_lattice
authorhoelzl
Tue Mar 05 15:43:12 2013 +0100 (2013-03-05)
changeset 513418c10293e7ea7
parent 51340 5e6296afe08d
child 51342 763c6872bd10
complete_linorder is also a complete_distrib_lattice
src/HOL/Complete_Lattices.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Tue Mar 05 15:43:08 2013 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Mar 05 15:43:12 2013 +0100
     1.3 @@ -589,6 +589,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance complete_linorder \<subseteq> complete_distrib_lattice
     1.8 +  apply default
     1.9 +  apply (safe intro!: INF_eqI[symmetric] sup_mono complete_lattice_class.Inf_lower
    1.10 +                      SUP_eqI[symmetric] inf_mono complete_lattice_class.Sup_upper)
    1.11 +  apply (auto simp: not_less[symmetric]
    1.12 +                    Inf_less_iff less_Sup_iff le_max_iff_disj sup_max min_le_iff_disj inf_min)
    1.13 +  done
    1.14 +
    1.15  subsection {* Complete lattice on @{typ bool} *}
    1.16  
    1.17  instantiation bool :: complete_lattice