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 {*