src/HOL/Lattices.thy
author haftmann
Fri Mar 09 08:45:50 2007 +0100 (2007-03-09)
changeset 22422 ee19cdb07528
parent 22384 33a46e6c7f04
child 22454 c3654ba76a09
permissions -rw-r--r--
stepping towards uniform lattice theory development in HOL
     1 (*  Title:      HOL/Lattices.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4 *)
     5 
     6 header {* Lattices via Locales *}
     7 
     8 theory Lattices
     9 imports Orderings
    10 begin
    11 
    12 subsection{* Lattices *}
    13 
    14 text{* This theory of lattice locales only defines binary sup and inf
    15 operations. The extension to finite sets is done in theory @{text
    16 Finite_Set}. In the longer term it may be better to define arbitrary
    17 sups and infs via @{text THE}. *}
    18 
    19 class lower_semilattice = order +
    20   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    21   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    22   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    23 
    24 class upper_semilattice = order +
    25   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    26   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    27   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    28 
    29 class lattice = lower_semilattice + upper_semilattice
    30 
    31 subsubsection{* Intro and elim rules*}
    32 
    33 context lower_semilattice
    34 begin
    35 
    36 lemmas antisym_intro [intro!] = antisym
    37 lemmas (in -) [rule del] = antisym_intro
    38 
    39 lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    40 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    41  apply(blast intro: order_trans)
    42 apply simp
    43 done
    44 lemmas (in -) [rule del] = le_infI1
    45 
    46 lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    47 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    48  apply(blast intro: order_trans)
    49 apply simp
    50 done
    51 lemmas (in -) [rule del] = le_infI2
    52 
    53 lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    54 by(blast intro: inf_greatest)
    55 lemmas (in -) [rule del] = le_infI
    56 
    57 lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    58   by (blast intro: order_trans)
    59 lemmas (in -) [rule del] = le_infE
    60 
    61 lemma le_inf_iff [simp]:
    62  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    63 by blast
    64 
    65 lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
    66 by(blast dest:eq_iff[THEN iffD1])
    67 
    68 end
    69 
    70 
    71 context upper_semilattice
    72 begin
    73 
    74 lemmas antisym_intro [intro!] = antisym
    75 lemmas (in -) [rule del] = antisym_intro
    76 
    77 lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    78 apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    79  apply(blast intro: order_trans)
    80 apply simp
    81 done
    82 lemmas (in -) [rule del] = le_supI1
    83 
    84 lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    85 apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    86  apply(blast intro: order_trans)
    87 apply simp
    88 done
    89 lemmas (in -) [rule del] = le_supI2
    90 
    91 lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    92 by(blast intro: sup_least)
    93 lemmas (in -) [rule del] = le_supI
    94 
    95 lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    96   by (blast intro: order_trans)
    97 lemmas (in -) [rule del] = le_supE
    98 
    99 
   100 lemma ge_sup_conv[simp]:
   101  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
   102 by blast
   103 
   104 lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
   105 by(blast dest:eq_iff[THEN iffD1])
   106 
   107 end
   108 
   109 
   110 subsubsection{* Equational laws *}
   111 
   112 
   113 context lower_semilattice
   114 begin
   115 
   116 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   117 by blast
   118 
   119 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   120 by blast
   121 
   122 lemma inf_idem[simp]: "x \<sqinter> x = x"
   123 by blast
   124 
   125 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   126 by blast
   127 
   128 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   129 by blast
   130 
   131 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   132 by blast
   133 
   134 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   135 by blast
   136 
   137 lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
   138 
   139 end
   140 
   141 
   142 context upper_semilattice
   143 begin
   144 
   145 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   146 by blast
   147 
   148 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   149 by blast
   150 
   151 lemma sup_idem[simp]: "x \<squnion> x = x"
   152 by blast
   153 
   154 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   155 by blast
   156 
   157 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   158 by blast
   159 
   160 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   161 by blast
   162 
   163 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   164 by blast
   165 
   166 lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
   167 
   168 end
   169 
   170 context lattice
   171 begin
   172 
   173 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   174 by(blast intro: antisym inf_le1 inf_greatest sup_ge1)
   175 
   176 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   177 by(blast intro: antisym sup_ge1 sup_least inf_le1)
   178 
   179 lemmas ACI = inf_ACI sup_ACI
   180 
   181 text{* Towards distributivity *}
   182 
   183 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   184 by blast
   185 
   186 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   187 by blast
   188 
   189 
   190 text{* If you have one of them, you have them all. *}
   191 
   192 lemma distrib_imp1:
   193 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   194 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   195 proof-
   196   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
   197   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
   198   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
   199     by(simp add:inf_sup_absorb inf_commute)
   200   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
   201   finally show ?thesis .
   202 qed
   203 
   204 lemma distrib_imp2:
   205 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   206 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   207 proof-
   208   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
   209   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
   210   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   211     by(simp add:sup_inf_absorb sup_commute)
   212   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   213   finally show ?thesis .
   214 qed
   215 
   216 (* seems unused *)
   217 lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
   218 by blast
   219 
   220 end
   221 
   222 
   223 subsection{* Distributive lattices *}
   224 
   225 locale distrib_lattice = lattice +
   226   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   227 
   228 context distrib_lattice
   229 begin
   230 
   231 lemma sup_inf_distrib2:
   232  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   233 by(simp add:ACI sup_inf_distrib1)
   234 
   235 lemma inf_sup_distrib1:
   236  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   237 by(rule distrib_imp2[OF sup_inf_distrib1])
   238 
   239 lemma inf_sup_distrib2:
   240  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   241 by(simp add:ACI inf_sup_distrib1)
   242 
   243 lemmas distrib =
   244   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   245 
   246 end
   247 
   248 
   249 subsection {* min/max on linear orders as special case of inf/sup *}
   250 
   251 interpretation min_max:
   252   distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   253 apply unfold_locales
   254 apply (simp add: min_def linorder_not_le order_less_imp_le)
   255 apply (simp add: min_def linorder_not_le order_less_imp_le)
   256 apply (simp add: min_def linorder_not_le order_less_imp_le)
   257 apply (simp add: max_def linorder_not_le order_less_imp_le)
   258 apply (simp add: max_def linorder_not_le order_less_imp_le)
   259 unfolding min_def max_def by auto
   260 
   261 text {*
   262   Now we have inherited antisymmetry as an intro-rule on all
   263   linear orders. This is a problem because it applies to bool, which is
   264   undesirable.
   265 *}
   266 
   267 lemmas [rule del] = min_max.antisym_intro  min_max.le_infI min_max.le_supI
   268   min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   269   min_max.le_infI1 min_max.le_infI2
   270 
   271 lemmas le_maxI1 = min_max.sup_ge1
   272 lemmas le_maxI2 = min_max.sup_ge2
   273  
   274 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   275   mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
   276 
   277 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   278   mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   279 
   280 text {* ML legacy bindings *}
   281 
   282 ML {*
   283 val Least_def = @{thm Least_def}
   284 val Least_equality = @{thm Least_equality}
   285 val min_def = @{thm min_def}
   286 val min_of_mono = @{thm min_of_mono}
   287 val max_def = @{thm max_def}
   288 val max_of_mono = @{thm max_of_mono}
   289 val min_leastL = @{thm min_leastL}
   290 val max_leastL = @{thm max_leastL}
   291 val min_leastR = @{thm min_leastR}
   292 val max_leastR = @{thm max_leastR}
   293 val le_max_iff_disj = @{thm le_max_iff_disj}
   294 val le_maxI1 = @{thm le_maxI1}
   295 val le_maxI2 = @{thm le_maxI2}
   296 val less_max_iff_disj = @{thm less_max_iff_disj}
   297 val max_less_iff_conj = @{thm max_less_iff_conj}
   298 val min_less_iff_conj = @{thm min_less_iff_conj}
   299 val min_le_iff_disj = @{thm min_le_iff_disj}
   300 val min_less_iff_disj = @{thm min_less_iff_disj}
   301 val split_min = @{thm split_min}
   302 val split_max = @{thm split_max}
   303 *}
   304 
   305 end