src/HOL/Lattice/Lattice.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23393 31781b2de73d
child 25469 f81b3be9dfdd
permissions -rw-r--r--
Name.uu, Name.aT;
wenzelm@10157
     1
(*  Title:      HOL/Lattice/Lattice.thy
wenzelm@10157
     2
    ID:         $Id$
wenzelm@10157
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10157
     4
*)
wenzelm@10157
     5
wenzelm@10157
     6
header {* Lattices *}
wenzelm@10157
     7
haftmann@16417
     8
theory Lattice imports Bounds begin
wenzelm@10157
     9
wenzelm@10157
    10
subsection {* Lattice operations *}
wenzelm@10157
    11
wenzelm@10157
    12
text {*
wenzelm@10157
    13
  A \emph{lattice} is a partial order with infimum and supremum of any
wenzelm@10157
    14
  two elements (thus any \emph{finite} number of elements have bounds
wenzelm@10157
    15
  as well).
wenzelm@10157
    16
*}
wenzelm@10157
    17
wenzelm@11099
    18
axclass lattice \<subseteq> partial_order
wenzelm@10157
    19
  ex_inf: "\<exists>inf. is_inf x y inf"
wenzelm@10157
    20
  ex_sup: "\<exists>sup. is_sup x y sup"
wenzelm@10157
    21
wenzelm@10157
    22
text {*
wenzelm@10157
    23
  The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
wenzelm@10157
    24
  infimum and supremum elements.
wenzelm@10157
    25
*}
wenzelm@10157
    26
wenzelm@19736
    27
definition
wenzelm@21404
    28
  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70) where
wenzelm@19736
    29
  "x && y = (THE inf. is_inf x y inf)"
wenzelm@21404
    30
definition
wenzelm@21404
    31
  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65) where
wenzelm@19736
    32
  "x || y = (THE sup. is_sup x y sup)"
wenzelm@19736
    33
wenzelm@21210
    34
notation (xsymbols)
wenzelm@21404
    35
  meet  (infixl "\<sqinter>" 70) and
wenzelm@19736
    36
  join  (infixl "\<squnion>" 65)
wenzelm@10157
    37
wenzelm@10157
    38
text {*
wenzelm@10157
    39
  Due to unique existence of bounds, the lattice operations may be
wenzelm@10157
    40
  exhibited as follows.
wenzelm@10157
    41
*}
wenzelm@10157
    42
wenzelm@10157
    43
lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
wenzelm@10157
    44
proof (unfold meet_def)
wenzelm@10157
    45
  assume "is_inf x y inf"
wenzelm@23373
    46
  then show "(THE inf. is_inf x y inf) = inf"
wenzelm@23373
    47
    by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
wenzelm@10157
    48
qed
wenzelm@10157
    49
wenzelm@10157
    50
lemma meetI [intro?]:
wenzelm@10157
    51
    "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"
wenzelm@10157
    52
  by (rule meet_equality, rule is_infI) blast+
wenzelm@10157
    53
wenzelm@10157
    54
lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
wenzelm@10157
    55
proof (unfold join_def)
wenzelm@10157
    56
  assume "is_sup x y sup"
wenzelm@23373
    57
  then show "(THE sup. is_sup x y sup) = sup"
wenzelm@23373
    58
    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
wenzelm@10157
    59
qed
wenzelm@10157
    60
wenzelm@10157
    61
lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
wenzelm@10157
    62
    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"
wenzelm@10157
    63
  by (rule join_equality, rule is_supI) blast+
wenzelm@10157
    64
wenzelm@10157
    65
wenzelm@10157
    66
text {*
wenzelm@10157
    67
  \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine
wenzelm@10157
    68
  bounds on a lattice structure.
wenzelm@10157
    69
*}
wenzelm@10157
    70
wenzelm@10157
    71
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
wenzelm@10157
    72
proof (unfold meet_def)
wenzelm@11441
    73
  from ex_inf obtain inf where "is_inf x y inf" ..
wenzelm@23373
    74
  then show "is_inf x y (THE inf. is_inf x y inf)"
wenzelm@23373
    75
    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
wenzelm@10157
    76
qed
wenzelm@10157
    77
wenzelm@10157
    78
lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
wenzelm@10157
    79
  by (rule is_inf_greatest) (rule is_inf_meet)
wenzelm@10157
    80
wenzelm@10157
    81
lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"
wenzelm@10157
    82
  by (rule is_inf_lower) (rule is_inf_meet)
wenzelm@10157
    83
wenzelm@10157
    84
lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"
wenzelm@10157
    85
  by (rule is_inf_lower) (rule is_inf_meet)
wenzelm@10157
    86
wenzelm@10157
    87
wenzelm@10157
    88
lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
wenzelm@10157
    89
proof (unfold join_def)
wenzelm@11441
    90
  from ex_sup obtain sup where "is_sup x y sup" ..
wenzelm@23373
    91
  then show "is_sup x y (THE sup. is_sup x y sup)"
wenzelm@23373
    92
    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
wenzelm@10157
    93
qed
wenzelm@10157
    94
wenzelm@10157
    95
lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
wenzelm@10157
    96
  by (rule is_sup_least) (rule is_sup_join)
wenzelm@10157
    97
wenzelm@10157
    98
lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"
wenzelm@10157
    99
  by (rule is_sup_upper) (rule is_sup_join)
wenzelm@10157
   100
wenzelm@10157
   101
lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"
wenzelm@10157
   102
  by (rule is_sup_upper) (rule is_sup_join)
wenzelm@10157
   103
wenzelm@10157
   104
wenzelm@10157
   105
subsection {* Duality *}
wenzelm@10157
   106
wenzelm@10157
   107
text {*
wenzelm@10157
   108
  The class of lattices is closed under formation of dual structures.
wenzelm@10157
   109
  This means that for any theorem of lattice theory, the dualized
wenzelm@10157
   110
  statement holds as well; this important fact simplifies many proofs
wenzelm@10157
   111
  of lattice theory.
wenzelm@10157
   112
*}
wenzelm@10157
   113
wenzelm@10157
   114
instance dual :: (lattice) lattice
wenzelm@10309
   115
proof
wenzelm@10157
   116
  fix x' y' :: "'a::lattice dual"
wenzelm@10157
   117
  show "\<exists>inf'. is_inf x' y' inf'"
wenzelm@10157
   118
  proof -
wenzelm@10157
   119
    have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
wenzelm@23373
   120
    then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
wenzelm@10157
   121
      by (simp only: dual_inf)
wenzelm@23373
   122
    then show ?thesis by (simp add: dual_ex [symmetric])
wenzelm@10157
   123
  qed
wenzelm@10157
   124
  show "\<exists>sup'. is_sup x' y' sup'"
wenzelm@10157
   125
  proof -
wenzelm@10157
   126
    have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
wenzelm@23373
   127
    then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
wenzelm@10157
   128
      by (simp only: dual_sup)
wenzelm@23373
   129
    then show ?thesis by (simp add: dual_ex [symmetric])
wenzelm@10157
   130
  qed
wenzelm@10157
   131
qed
wenzelm@10157
   132
wenzelm@10157
   133
text {*
wenzelm@10157
   134
  Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each
wenzelm@10157
   135
  other.
wenzelm@10157
   136
*}
wenzelm@10157
   137
wenzelm@10157
   138
theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
wenzelm@10157
   139
proof -
wenzelm@10157
   140
  from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
wenzelm@23373
   141
  then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
wenzelm@23373
   142
  then show ?thesis ..
wenzelm@10157
   143
qed
wenzelm@10157
   144
wenzelm@10157
   145
theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
wenzelm@10157
   146
proof -
wenzelm@10157
   147
  from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
wenzelm@23373
   148
  then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
wenzelm@23373
   149
  then show ?thesis ..
wenzelm@10157
   150
qed
wenzelm@10157
   151
wenzelm@10157
   152
wenzelm@10157
   153
subsection {* Algebraic properties \label{sec:lattice-algebra} *}
wenzelm@10157
   154
wenzelm@10157
   155
text {*
kleing@12818
   156
  The @{text \<sqinter>} and @{text \<squnion>} operations have the following
wenzelm@10157
   157
  characteristic algebraic properties: associative (A), commutative
wenzelm@10157
   158
  (C), and absorptive (AB).
wenzelm@10157
   159
*}
wenzelm@10157
   160
wenzelm@10157
   161
theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
wenzelm@10157
   162
proof
wenzelm@10157
   163
  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
wenzelm@10157
   164
  proof
wenzelm@10157
   165
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
wenzelm@10157
   166
    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
wenzelm@10157
   167
    proof -
wenzelm@10157
   168
      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
wenzelm@10157
   169
      also have "\<dots> \<sqsubseteq> y" ..
wenzelm@10157
   170
      finally show ?thesis .
wenzelm@10157
   171
    qed
wenzelm@10157
   172
  qed
wenzelm@10157
   173
  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
wenzelm@10157
   174
  proof -
wenzelm@10157
   175
    have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
wenzelm@10157
   176
    also have "\<dots> \<sqsubseteq> z" ..
wenzelm@10157
   177
    finally show ?thesis .
wenzelm@10157
   178
  qed
wenzelm@10157
   179
  fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
wenzelm@10157
   180
  show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
wenzelm@10157
   181
  proof
wenzelm@10157
   182
    show "w \<sqsubseteq> x"
wenzelm@10157
   183
    proof -
wenzelm@23373
   184
      have "w \<sqsubseteq> x \<sqinter> y" by fact
wenzelm@10157
   185
      also have "\<dots> \<sqsubseteq> x" ..
wenzelm@10157
   186
      finally show ?thesis .
wenzelm@10157
   187
    qed
wenzelm@10157
   188
    show "w \<sqsubseteq> y \<sqinter> z"
wenzelm@10157
   189
    proof
wenzelm@10157
   190
      show "w \<sqsubseteq> y"
wenzelm@10157
   191
      proof -
wenzelm@23373
   192
        have "w \<sqsubseteq> x \<sqinter> y" by fact
wenzelm@10157
   193
        also have "\<dots> \<sqsubseteq> y" ..
wenzelm@10157
   194
        finally show ?thesis .
wenzelm@10157
   195
      qed
wenzelm@23373
   196
      show "w \<sqsubseteq> z" by fact
wenzelm@10157
   197
    qed
wenzelm@10157
   198
  qed
wenzelm@10157
   199
qed
wenzelm@10157
   200
wenzelm@10157
   201
theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
wenzelm@10157
   202
proof -
wenzelm@10157
   203
  have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"
wenzelm@10157
   204
    by (simp only: dual_join)
wenzelm@10157
   205
  also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"
wenzelm@10157
   206
    by (rule meet_assoc)
wenzelm@10157
   207
  also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"
wenzelm@10157
   208
    by (simp only: dual_join)
wenzelm@10157
   209
  finally show ?thesis ..
wenzelm@10157
   210
qed
wenzelm@10157
   211
wenzelm@10157
   212
theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
wenzelm@10157
   213
proof
wenzelm@10157
   214
  show "y \<sqinter> x \<sqsubseteq> x" ..
wenzelm@10157
   215
  show "y \<sqinter> x \<sqsubseteq> y" ..
wenzelm@23373
   216
  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
wenzelm@23373
   217
  then show "z \<sqsubseteq> y \<sqinter> x" ..
wenzelm@10157
   218
qed
wenzelm@10157
   219
wenzelm@10157
   220
theorem join_commute: "x \<squnion> y = y \<squnion> x"
wenzelm@10157
   221
proof -
wenzelm@10157
   222
  have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..
wenzelm@10157
   223
  also have "\<dots> = dual y \<sqinter> dual x"
wenzelm@10157
   224
    by (rule meet_commute)
wenzelm@10157
   225
  also have "\<dots> = dual (y \<squnion> x)"
wenzelm@10157
   226
    by (simp only: dual_join)
wenzelm@10157
   227
  finally show ?thesis ..
wenzelm@10157
   228
qed
wenzelm@10157
   229
wenzelm@10157
   230
theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
wenzelm@10157
   231
proof
wenzelm@10157
   232
  show "x \<sqsubseteq> x" ..
wenzelm@10157
   233
  show "x \<sqsubseteq> x \<squnion> y" ..
wenzelm@10157
   234
  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
wenzelm@23393
   235
  show "z \<sqsubseteq> x" by fact
wenzelm@10157
   236
qed
wenzelm@10157
   237
wenzelm@10157
   238
theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
wenzelm@10157
   239
proof -
wenzelm@10157
   240
  have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
wenzelm@10157
   241
    by (rule meet_join_absorb)
wenzelm@23373
   242
  then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
wenzelm@10157
   243
    by (simp only: dual_meet dual_join)
wenzelm@23373
   244
  then show ?thesis ..
wenzelm@10157
   245
qed
wenzelm@10157
   246
wenzelm@10157
   247
text {*
wenzelm@10157
   248
  \medskip Some further algebraic properties hold as well.  The
wenzelm@10157
   249
  property idempotent (I) is a basic algebraic consequence of (AB).
wenzelm@10157
   250
*}
wenzelm@10157
   251
wenzelm@10157
   252
theorem meet_idem: "x \<sqinter> x = x"
wenzelm@10157
   253
proof -
wenzelm@10157
   254
  have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
wenzelm@10157
   255
  also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
wenzelm@10157
   256
  finally show ?thesis .
wenzelm@10157
   257
qed
wenzelm@10157
   258
wenzelm@10157
   259
theorem join_idem: "x \<squnion> x = x"
wenzelm@10157
   260
proof -
wenzelm@10157
   261
  have "dual x \<sqinter> dual x = dual x"
wenzelm@10157
   262
    by (rule meet_idem)
wenzelm@23373
   263
  then have "dual (x \<squnion> x) = dual x"
wenzelm@10157
   264
    by (simp only: dual_join)
wenzelm@23373
   265
  then show ?thesis ..
wenzelm@10157
   266
qed
wenzelm@10157
   267
wenzelm@10157
   268
text {*
wenzelm@10157
   269
  Meet and join are trivial for related elements.
wenzelm@10157
   270
*}
wenzelm@10157
   271
wenzelm@10157
   272
theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
wenzelm@10157
   273
proof
wenzelm@10157
   274
  assume "x \<sqsubseteq> y"
wenzelm@10157
   275
  show "x \<sqsubseteq> x" ..
wenzelm@23373
   276
  show "x \<sqsubseteq> y" by fact
wenzelm@23373
   277
  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
wenzelm@23373
   278
  show "z \<sqsubseteq> x" by fact
wenzelm@10157
   279
qed
wenzelm@10157
   280
wenzelm@10157
   281
theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
wenzelm@10157
   282
proof -
wenzelm@23373
   283
  assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
wenzelm@23373
   284
  then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
wenzelm@10157
   285
  also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
wenzelm@10157
   286
  also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
wenzelm@10157
   287
  finally show ?thesis ..
wenzelm@10157
   288
qed
wenzelm@10157
   289
wenzelm@10157
   290
wenzelm@10157
   291
subsection {* Order versus algebraic structure *}
wenzelm@10157
   292
wenzelm@10157
   293
text {*
wenzelm@10157
   294
  The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the
wenzelm@10157
   295
  underlying @{text \<sqsubseteq>} relation in a canonical manner.
wenzelm@10157
   296
*}
wenzelm@10157
   297
wenzelm@10157
   298
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
wenzelm@10157
   299
proof
wenzelm@10157
   300
  assume "x \<sqsubseteq> y"
wenzelm@23373
   301
  then have "is_inf x y x" ..
wenzelm@23373
   302
  then show "x \<sqinter> y = x" ..
wenzelm@10157
   303
next
wenzelm@10157
   304
  have "x \<sqinter> y \<sqsubseteq> y" ..
wenzelm@10157
   305
  also assume "x \<sqinter> y = x"
wenzelm@10157
   306
  finally show "x \<sqsubseteq> y" .
wenzelm@10157
   307
qed
wenzelm@10157
   308
wenzelm@10157
   309
theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
wenzelm@10157
   310
proof
wenzelm@10157
   311
  assume "x \<sqsubseteq> y"
wenzelm@23373
   312
  then have "is_sup x y y" ..
wenzelm@23373
   313
  then show "x \<squnion> y = y" ..
wenzelm@10157
   314
next
wenzelm@10157
   315
  have "x \<sqsubseteq> x \<squnion> y" ..
wenzelm@10157
   316
  also assume "x \<squnion> y = y"
wenzelm@10157
   317
  finally show "x \<sqsubseteq> y" .
wenzelm@10157
   318
qed
wenzelm@10157
   319
wenzelm@10157
   320
text {*
wenzelm@10157
   321
  \medskip The most fundamental result of the meta-theory of lattices
wenzelm@10157
   322
  is as follows (we do not prove it here).
wenzelm@10157
   323
wenzelm@10157
   324
  Given a structure with binary operations @{text \<sqinter>} and @{text \<squnion>}
wenzelm@10157
   325
  such that (A), (C), and (AB) hold (cf.\
wenzelm@10157
   326
  \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
wenzelm@10157
   327
  if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
wenzelm@10157
   328
  (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and
wenzelm@10157
   329
  supremum with respect to this ordering coincide with the original
wenzelm@10157
   330
  @{text \<sqinter>} and @{text \<squnion>} operations.
wenzelm@10157
   331
*}
wenzelm@10157
   332
wenzelm@10157
   333
wenzelm@10157
   334
subsection {* Example instances *}
wenzelm@10157
   335
wenzelm@10157
   336
subsubsection {* Linear orders *}
wenzelm@10157
   337
wenzelm@10157
   338
text {*
kleing@12818
   339
  Linear orders with @{term minimum} and @{term maximum} operations
wenzelm@10157
   340
  are a (degenerate) example of lattice structures.
wenzelm@10157
   341
*}
wenzelm@10157
   342
wenzelm@19736
   343
definition
wenzelm@21404
   344
  minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
wenzelm@19736
   345
  "minimum x y = (if x \<sqsubseteq> y then x else y)"
wenzelm@21404
   346
definition
wenzelm@21404
   347
  maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
wenzelm@19736
   348
  "maximum x y = (if x \<sqsubseteq> y then y else x)"
wenzelm@10157
   349
wenzelm@10157
   350
lemma is_inf_minimum: "is_inf x y (minimum x y)"
wenzelm@10157
   351
proof
wenzelm@10157
   352
  let ?min = "minimum x y"
wenzelm@10157
   353
  from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)
wenzelm@10157
   354
  from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)
wenzelm@10157
   355
  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
wenzelm@10157
   356
  with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)
wenzelm@10157
   357
qed
wenzelm@10157
   358
wenzelm@10157
   359
lemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)
wenzelm@10157
   360
proof
wenzelm@10157
   361
  let ?max = "maximum x y"
wenzelm@10157
   362
  from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)
wenzelm@10157
   363
  from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)
wenzelm@10157
   364
  fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
wenzelm@10157
   365
  with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
wenzelm@10157
   366
qed
wenzelm@10157
   367
wenzelm@11099
   368
instance linear_order \<subseteq> lattice
wenzelm@10309
   369
proof
wenzelm@10157
   370
  fix x y :: "'a::linear_order"
wenzelm@10157
   371
  from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
wenzelm@10157
   372
  from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
wenzelm@10157
   373
qed
wenzelm@10157
   374
wenzelm@10157
   375
text {*
wenzelm@10157
   376
  The lattice operations on linear orders indeed coincide with @{term
wenzelm@10157
   377
  minimum} and @{term maximum}.
wenzelm@10157
   378
*}
wenzelm@10157
   379
wenzelm@10157
   380
theorem meet_mimimum: "x \<sqinter> y = minimum x y"
wenzelm@10157
   381
  by (rule meet_equality) (rule is_inf_minimum)
wenzelm@10157
   382
wenzelm@10157
   383
theorem meet_maximum: "x \<squnion> y = maximum x y"
wenzelm@10157
   384
  by (rule join_equality) (rule is_sup_maximum)
wenzelm@10157
   385
wenzelm@10157
   386
wenzelm@10157
   387
wenzelm@10157
   388
subsubsection {* Binary products *}
wenzelm@10157
   389
wenzelm@10157
   390
text {*
wenzelm@10157
   391
  The class of lattices is closed under direct binary products (cf.\
wenzelm@10158
   392
  \S\ref{sec:prod-order}).
wenzelm@10157
   393
*}
wenzelm@10157
   394
wenzelm@10157
   395
lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
wenzelm@10157
   396
proof
wenzelm@10157
   397
  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"
wenzelm@10157
   398
  proof -
wenzelm@10157
   399
    have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..
wenzelm@10157
   400
    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..
wenzelm@10157
   401
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   402
  qed
wenzelm@10157
   403
  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"
wenzelm@10157
   404
  proof -
wenzelm@10157
   405
    have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..
wenzelm@10157
   406
    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..
wenzelm@10157
   407
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   408
  qed
wenzelm@10157
   409
  fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"
wenzelm@10157
   410
  show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
wenzelm@10157
   411
  proof -
wenzelm@10157
   412
    have "fst r \<sqsubseteq> fst p \<sqinter> fst q"
wenzelm@10157
   413
    proof
wenzelm@10157
   414
      from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)
wenzelm@10157
   415
      from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)
wenzelm@10157
   416
    qed
wenzelm@10157
   417
    moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"
wenzelm@10157
   418
    proof
wenzelm@10157
   419
      from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)
wenzelm@10157
   420
      from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)
wenzelm@10157
   421
    qed
wenzelm@10157
   422
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   423
  qed
wenzelm@10157
   424
qed
wenzelm@10157
   425
wenzelm@10157
   426
lemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)
wenzelm@10157
   427
proof
wenzelm@10157
   428
  show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
wenzelm@10157
   429
  proof -
wenzelm@10157
   430
    have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..
wenzelm@10157
   431
    moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..
wenzelm@10157
   432
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   433
  qed
wenzelm@10157
   434
  show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
wenzelm@10157
   435
  proof -
wenzelm@10157
   436
    have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..
wenzelm@10157
   437
    moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..
wenzelm@10157
   438
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   439
  qed
wenzelm@10157
   440
  fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"
wenzelm@10157
   441
  show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"
wenzelm@10157
   442
  proof -
wenzelm@10157
   443
    have "fst p \<squnion> fst q \<sqsubseteq> fst r"
wenzelm@10157
   444
    proof
wenzelm@10157
   445
      from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)
wenzelm@10157
   446
      from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)
wenzelm@10157
   447
    qed
wenzelm@10157
   448
    moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"
wenzelm@10157
   449
    proof
wenzelm@10157
   450
      from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)
wenzelm@10157
   451
      from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)
wenzelm@10157
   452
    qed
wenzelm@10157
   453
    ultimately show ?thesis by (simp add: leq_prod_def)
wenzelm@10157
   454
  qed
wenzelm@10157
   455
qed
wenzelm@10157
   456
wenzelm@10157
   457
instance * :: (lattice, lattice) lattice
wenzelm@10309
   458
proof
wenzelm@10157
   459
  fix p q :: "'a::lattice \<times> 'b::lattice"
wenzelm@10157
   460
  from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
wenzelm@10157
   461
  from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
wenzelm@10157
   462
qed
wenzelm@10157
   463
wenzelm@10157
   464
text {*
wenzelm@10157
   465
  The lattice operations on a binary product structure indeed coincide
wenzelm@10157
   466
  with the products of the original ones.
wenzelm@10157
   467
*}
wenzelm@10157
   468
wenzelm@10157
   469
theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
wenzelm@10157
   470
  by (rule meet_equality) (rule is_inf_prod)
wenzelm@10157
   471
wenzelm@10157
   472
theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"
wenzelm@10157
   473
  by (rule join_equality) (rule is_sup_prod)
wenzelm@10157
   474
wenzelm@10157
   475
wenzelm@10157
   476
subsubsection {* General products *}
wenzelm@10157
   477
wenzelm@10157
   478
text {*
wenzelm@10157
   479
  The class of lattices is closed under general products (function
wenzelm@10158
   480
  spaces) as well (cf.\ \S\ref{sec:fun-order}).
wenzelm@10157
   481
*}
wenzelm@10157
   482
wenzelm@10157
   483
lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
wenzelm@10157
   484
proof
wenzelm@10157
   485
  show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"
wenzelm@10157
   486
  proof
wenzelm@10157
   487
    fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..
wenzelm@10157
   488
  qed
wenzelm@10157
   489
  show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"
wenzelm@10157
   490
  proof
wenzelm@10157
   491
    fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..
wenzelm@10157
   492
  qed
wenzelm@10157
   493
  fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"
wenzelm@10157
   494
  show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"
wenzelm@10157
   495
  proof
wenzelm@10157
   496
    fix x
wenzelm@10157
   497
    show "h x \<sqsubseteq> f x \<sqinter> g x"
wenzelm@10157
   498
    proof
wenzelm@10157
   499
      from hf show "h x \<sqsubseteq> f x" ..
wenzelm@10157
   500
      from hg show "h x \<sqsubseteq> g x" ..
wenzelm@10157
   501
    qed
wenzelm@10157
   502
  qed
wenzelm@10157
   503
qed
wenzelm@10157
   504
wenzelm@10157
   505
lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)"   (* FIXME dualize!? *)
wenzelm@10157
   506
proof
wenzelm@10157
   507
  show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
wenzelm@10157
   508
  proof
wenzelm@10157
   509
    fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..
wenzelm@10157
   510
  qed
wenzelm@10157
   511
  show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
wenzelm@10157
   512
  proof
wenzelm@10157
   513
    fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..
wenzelm@10157
   514
  qed
wenzelm@10157
   515
  fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"
wenzelm@10157
   516
  show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"
wenzelm@10157
   517
  proof
wenzelm@10157
   518
    fix x
wenzelm@10157
   519
    show "f x \<squnion> g x \<sqsubseteq> h x"
wenzelm@10157
   520
    proof
wenzelm@10157
   521
      from fh show "f x \<sqsubseteq> h x" ..
wenzelm@10157
   522
      from gh show "g x \<sqsubseteq> h x" ..
wenzelm@10157
   523
    qed
wenzelm@10157
   524
  qed
wenzelm@10157
   525
qed
wenzelm@10157
   526
krauss@20523
   527
instance "fun" :: (type, lattice) lattice
wenzelm@10309
   528
proof
wenzelm@10157
   529
  fix f g :: "'a \<Rightarrow> 'b::lattice"
wenzelm@10157
   530
  show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
wenzelm@10157
   531
  show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
wenzelm@10157
   532
qed
wenzelm@10157
   533
wenzelm@10157
   534
text {*
wenzelm@10157
   535
  The lattice operations on a general product structure (function
wenzelm@10157
   536
  space) indeed emerge by point-wise lifting of the original ones.
wenzelm@10157
   537
*}
wenzelm@10157
   538
wenzelm@10157
   539
theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
wenzelm@10157
   540
  by (rule meet_equality) (rule is_inf_fun)
wenzelm@10157
   541
wenzelm@10157
   542
theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
wenzelm@10157
   543
  by (rule join_equality) (rule is_sup_fun)
wenzelm@10157
   544
wenzelm@10157
   545
wenzelm@10157
   546
subsection {* Monotonicity and semi-morphisms *}
wenzelm@10157
   547
wenzelm@10157
   548
text {*
wenzelm@10157
   549
  The lattice operations are monotone in both argument positions.  In
wenzelm@10157
   550
  fact, monotonicity of the second position is trivial due to
wenzelm@10157
   551
  commutativity.
wenzelm@10157
   552
*}
wenzelm@10157
   553
wenzelm@10157
   554
theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
wenzelm@10157
   555
proof -
wenzelm@10157
   556
  {
wenzelm@10157
   557
    fix a b c :: "'a::lattice"
wenzelm@10157
   558
    assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
wenzelm@10157
   559
    proof
wenzelm@10157
   560
      have "a \<sqinter> b \<sqsubseteq> a" ..
wenzelm@23373
   561
      also have "\<dots> \<sqsubseteq> c" by fact
wenzelm@10157
   562
      finally show "a \<sqinter> b \<sqsubseteq> c" .
wenzelm@10157
   563
      show "a \<sqinter> b \<sqsubseteq> b" ..
wenzelm@10157
   564
    qed
wenzelm@10157
   565
  } note this [elim?]
wenzelm@23373
   566
  assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
wenzelm@10157
   567
  also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
wenzelm@23373
   568
  also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
wenzelm@10157
   569
  also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
wenzelm@10157
   570
  finally show ?thesis .
wenzelm@10157
   571
qed
wenzelm@10157
   572
wenzelm@10157
   573
theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
wenzelm@10157
   574
proof -
wenzelm@23373
   575
  assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
wenzelm@23373
   576
  moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
wenzelm@10157
   577
  ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
wenzelm@10157
   578
    by (rule meet_mono)
wenzelm@23373
   579
  then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
wenzelm@10157
   580
    by (simp only: dual_join)
wenzelm@23373
   581
  then show ?thesis ..
wenzelm@10157
   582
qed
wenzelm@10157
   583
wenzelm@10157
   584
text {*
wenzelm@10157
   585
  \medskip A semi-morphisms is a function $f$ that preserves the
wenzelm@10157
   586
  lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
wenzelm@10157
   587
  \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of
wenzelm@10157
   588
  these properties is equivalent with monotonicity.
wenzelm@10157
   589
*}  (* FIXME dual version !? *)
wenzelm@10157
   590
wenzelm@10157
   591
theorem meet_semimorph:
wenzelm@10157
   592
  "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
wenzelm@10157
   593
proof
wenzelm@10157
   594
  assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
wenzelm@10157
   595
  fix x y :: "'a::lattice"
wenzelm@23373
   596
  assume "x \<sqsubseteq> y" then have "x \<sqinter> y = x" ..
wenzelm@23373
   597
  then have "x = x \<sqinter> y" ..
wenzelm@10157
   598
  also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
wenzelm@10157
   599
  also have "\<dots> \<sqsubseteq> f y" ..
wenzelm@10157
   600
  finally show "f x \<sqsubseteq> f y" .
wenzelm@10157
   601
next
wenzelm@10157
   602
  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
wenzelm@10157
   603
  show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
wenzelm@10157
   604
  proof -
wenzelm@10157
   605
    fix x y
wenzelm@10157
   606
    show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
wenzelm@10157
   607
    proof
wenzelm@23373
   608
      have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
wenzelm@23373
   609
      have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
wenzelm@10157
   610
    qed
wenzelm@10157
   611
  qed
wenzelm@10157
   612
qed
wenzelm@10157
   613
wenzelm@10157
   614
end