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