src/HOL/Lattices.thy
changeset 22916 8caf6da610e2
parent 22737 d87ccbcc2702
child 23018 1d29bc31b0cb
     1.1 --- a/src/HOL/Lattices.thy	Thu May 10 04:06:56 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Thu May 10 10:21:44 2007 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4  
     1.5  text{*
     1.6    This theory of lattices only defines binary sup and inf
     1.7 -  operations. The extension to (finite) sets is done in theories
     1.8 -  @{text FixedPoint} and @{text Finite_Set}.
     1.9 +  operations. The extension to complete lattices is done in theory
    1.10 +  @{text FixedPoint}.
    1.11  *}
    1.12  
    1.13  class lower_semilattice = order +
    1.14 @@ -278,17 +278,24 @@
    1.15  qed
    1.16    
    1.17  
    1.18 -subsection {* min/max on linear orders as special case of inf/sup *}
    1.19 +subsection {* @{const min}/@{const max} on linear orders as
    1.20 +  special case of @{const inf}/@{const sup} *}
    1.21 +
    1.22 +lemma (in linorder) distrib_lattice_min_max:
    1.23 +  "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
    1.24 +proof unfold_locales
    1.25 +  have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    1.26 +    by (auto simp add: less_le antisym)
    1.27 +  fix x y z
    1.28 +  show "max x (min y z) = min (max x y) (max x z)"
    1.29 +  unfolding min_def max_def
    1.30 +    by (auto simp add: intro: antisym, unfold not_le,
    1.31 +      auto intro: less_trans le_less_trans aux)
    1.32 +qed (auto simp add: min_def max_def not_le less_imp_le)
    1.33  
    1.34  interpretation min_max:
    1.35    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
    1.36 -apply unfold_locales
    1.37 -apply (simp add: min_def linorder_not_le order_less_imp_le)
    1.38 -apply (simp add: min_def linorder_not_le order_less_imp_le)
    1.39 -apply (simp add: min_def linorder_not_le order_less_imp_le)
    1.40 -apply (simp add: max_def linorder_not_le order_less_imp_le)
    1.41 -apply (simp add: max_def linorder_not_le order_less_imp_le)
    1.42 -unfolding min_def max_def by auto
    1.43 +  by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
    1.44  
    1.45  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.46    by (rule ext)+ auto