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