src/HOL/Lattices.thy
 changeset 22454 c3654ba76a09 parent 22422 ee19cdb07528 child 22548 6ce4bddf3bcb
```     1.1 --- a/src/HOL/Lattices.thy	Fri Mar 16 21:32:09 2007 +0100
1.2 +++ b/src/HOL/Lattices.thy	Fri Mar 16 21:32:10 2007 +0100
1.3 @@ -3,7 +3,7 @@
1.4      Author:     Tobias Nipkow
1.5  *)
1.6
1.7 -header {* Lattices via Locales *}
1.8 +header {* Abstract lattices *}
1.9
1.10  theory Lattices
1.11  imports Orderings
1.12 @@ -11,10 +11,11 @@
1.13
1.14  subsection{* Lattices *}
1.15
1.16 -text{* This theory of lattice locales only defines binary sup and inf
1.17 -operations. The extension to finite sets is done in theory @{text
1.18 -Finite_Set}. In the longer term it may be better to define arbitrary
1.19 -sups and infs via @{text THE}. *}
1.20 +text{*
1.21 +  This theory of lattices only defines binary sup and inf
1.22 +  operations. The extension to (finite) sets is done in theories @{text FixedPoint}
1.23 +  and @{text Finite_Set}.
1.24 +*}
1.25
1.26  class lower_semilattice = order +
1.27    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
1.28 @@ -178,6 +179,8 @@
1.29
1.30  lemmas ACI = inf_ACI sup_ACI
1.31
1.32 +lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
1.33 +
1.34  text{* Towards distributivity *}
1.35
1.36  lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
1.37 @@ -222,7 +225,7 @@
1.38
1.39  subsection{* Distributive lattices *}
1.40
1.41 -locale distrib_lattice = lattice +
1.42 +class distrib_lattice = lattice +
1.43    assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
1.44
1.45  context distrib_lattice
1.46 @@ -246,10 +249,37 @@
1.47  end
1.48
1.49
1.50 +subsection {* Uniqueness of inf and sup *}
1.51 +
1.52 +lemma inf_unique:
1.53 +  fixes f (infixl "\<triangle>" 70)
1.54 +  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
1.55 +  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
1.56 +  shows "inf x y = f x y"
1.57 +proof (rule antisym)
1.58 +  show "x \<triangle> y \<le> inf x y" by (rule le_infI) (rule le1 le2)
1.59 +next
1.60 +  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
1.61 +  show "inf x y \<le> x \<triangle> y" by (rule leI) simp_all
1.62 +qed
1.63 +
1.64 +lemma sup_unique:
1.65 +  fixes f (infixl "\<nabla>" 70)
1.66 +  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
1.67 +  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
1.68 +  shows "sup x y = f x y"
1.69 +proof (rule antisym)
1.70 +  show "sup x y \<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
1.71 +next
1.72 +  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
1.73 +  show "x \<nabla> y \<le> sup x y" by (rule leI) simp_all
1.74 +qed
1.75 +
1.76 +
1.77  subsection {* min/max on linear orders as special case of inf/sup *}
1.78
1.79  interpretation min_max:
1.80 -  distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
1.81 +  distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
1.82  apply unfold_locales
1.83  apply (simp add: min_def linorder_not_le order_less_imp_le)
1.84  apply (simp add: min_def linorder_not_le order_less_imp_le)
1.85 @@ -258,15 +288,11 @@
1.86  apply (simp add: max_def linorder_not_le order_less_imp_le)
1.87  unfolding min_def max_def by auto
1.88
1.89 -text {*
1.90 -  Now we have inherited antisymmetry as an intro-rule on all
1.91 -  linear orders. This is a problem because it applies to bool, which is
1.92 -  undesirable.
1.93 -*}
1.94 +lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
1.95 +  by (rule ext)+ auto
1.96
1.97 -lemmas [rule del] = min_max.antisym_intro  min_max.le_infI min_max.le_supI
1.98 -  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
1.99 -  min_max.le_infI1 min_max.le_infI2
1.100 +lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
1.101 +  by (rule ext)+ auto
1.102
1.103  lemmas le_maxI1 = min_max.sup_ge1
1.104  lemmas le_maxI2 = min_max.sup_ge2
1.105 @@ -277,6 +303,31 @@
1.106  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
1.107    mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
1.108
1.109 +text {*
1.110 +  Now we have inherited antisymmetry as an intro-rule on all
1.111 +  linear orders. This is a problem because it applies to bool, which is
1.112 +  undesirable.
1.113 +*}
1.114 +
1.115 +lemmas [rule del] = min_max.antisym_intro min_max.le_infI min_max.le_supI
1.116 +  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
1.117 +  min_max.le_infI1 min_max.le_infI2
1.118 +
1.119 +
1.120 +subsection {* Bool as lattice *}
1.121 +
1.122 +instance bool :: distrib_lattice
1.123 +  inf_bool_eq: "inf P Q \<equiv> P \<and> Q"
1.124 +  sup_bool_eq: "sup P Q \<equiv> P \<or> Q"
1.125 +  by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
1.126 +
1.127 +
1.128 +text {* duplicates *}
1.129 +
1.130 +lemmas inf_aci = inf_ACI
1.131 +lemmas sup_aci = sup_ACI
1.132 +
1.133 +
1.134  text {* ML legacy bindings *}
1.135
1.136  ML {*
```