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
```