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