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