src/HOL/Algebra/Lattice.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 66580 e5b1d4d55bf6
child 67091 1393c2340eec
permissions -rw-r--r--
tuned: each session has at most one defining entry;
wenzelm@35849
     1
(*  Title:      HOL/Algebra/Lattice.thy
wenzelm@35849
     2
    Author:     Clemens Ballarin, started 7 November 2003
wenzelm@35849
     3
    Copyright:  Clemens Ballarin
ballarin@27714
     4
ballarin@27717
     5
Most congruence rules by Stephan Hohe.
ballarin@65099
     6
With additional contributions from Alasdair Armstrong and Simon Foster.
ballarin@14551
     7
*)
ballarin@14551
     8
wenzelm@35849
     9
theory Lattice
ballarin@65099
    10
imports Order
wenzelm@44472
    11
begin
ballarin@27713
    12
ballarin@65099
    13
section \<open>Lattices\<close>
ballarin@65099
    14
  
ballarin@65099
    15
subsection \<open>Supremum and infimum\<close>
ballarin@27713
    16
wenzelm@35847
    17
definition
ballarin@27713
    18
  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
wenzelm@35848
    19
  where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
ballarin@27713
    20
wenzelm@35847
    21
definition
ballarin@27713
    22
  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
wenzelm@35848
    23
  where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
ballarin@27713
    24
ballarin@65099
    25
definition supr :: 
ballarin@65099
    26
  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
ballarin@65099
    27
  where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
ballarin@65099
    28
ballarin@65099
    29
definition infi :: 
ballarin@65099
    30
  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
ballarin@65099
    31
  where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
ballarin@65099
    32
ballarin@65099
    33
syntax
ballarin@65099
    34
  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
ballarin@65099
    35
  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
ballarin@65099
    36
  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
ballarin@65099
    37
  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
ballarin@65099
    38
ballarin@65099
    39
translations
ballarin@65099
    40
  "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
ballarin@65099
    41
  "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
ballarin@65099
    42
  "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
ballarin@65099
    43
  "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
ballarin@65099
    44
wenzelm@35847
    45
definition
ballarin@27713
    46
  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
wenzelm@35848
    47
  where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
ballarin@27713
    48
wenzelm@35847
    49
definition
ballarin@27713
    50
  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
wenzelm@35848
    51
  where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
ballarin@27713
    52
ballarin@65099
    53
definition
ballarin@66580
    54
  LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
ballarin@66580
    55
  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
ballarin@65099
    56
ballarin@65099
    57
definition
ballarin@66580
    58
  GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
ballarin@66580
    59
  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
ballarin@65099
    60
ballarin@65099
    61
ballarin@65099
    62
subsection \<open>Dual operators\<close>
ballarin@65099
    63
ballarin@65099
    64
lemma sup_dual [simp]: 
ballarin@65099
    65
  "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
ballarin@65099
    66
  by (simp add: sup_def inf_def)
ballarin@65099
    67
ballarin@65099
    68
lemma inf_dual [simp]: 
ballarin@65099
    69
  "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
ballarin@65099
    70
  by (simp add: sup_def inf_def)
ballarin@65099
    71
ballarin@65099
    72
lemma join_dual [simp]:
ballarin@65099
    73
  "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
ballarin@65099
    74
  by (simp add:join_def meet_def)
ballarin@65099
    75
ballarin@65099
    76
lemma meet_dual [simp]:
ballarin@65099
    77
  "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
ballarin@65099
    78
  by (simp add:join_def meet_def)
ballarin@65099
    79
ballarin@65099
    80
lemma top_dual [simp]:
ballarin@65099
    81
  "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
ballarin@65099
    82
  by (simp add: top_def bottom_def)
ballarin@65099
    83
ballarin@65099
    84
lemma bottom_dual [simp]:
ballarin@65099
    85
  "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
ballarin@65099
    86
  by (simp add: top_def bottom_def)
ballarin@65099
    87
ballarin@65099
    88
lemma LFP_dual [simp]:
ballarin@66580
    89
  "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"
ballarin@66580
    90
  by (simp add:LEAST_FP_def GREATEST_FP_def)
ballarin@65099
    91
ballarin@65099
    92
lemma GFP_dual [simp]:
ballarin@66580
    93
  "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"
ballarin@66580
    94
  by (simp add:LEAST_FP_def GREATEST_FP_def)
ballarin@65099
    95
ballarin@27713
    96
wenzelm@61382
    97
subsection \<open>Lattices\<close>
ballarin@27713
    98
ballarin@27713
    99
locale weak_upper_semilattice = weak_partial_order +
ballarin@27713
   100
  assumes sup_of_two_exists:
ballarin@27713
   101
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
ballarin@27713
   102
ballarin@27713
   103
locale weak_lower_semilattice = weak_partial_order +
ballarin@27713
   104
  assumes inf_of_two_exists:
ballarin@27713
   105
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
ballarin@27713
   106
ballarin@27713
   107
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
ballarin@27713
   108
ballarin@65099
   109
lemma (in weak_lattice) dual_weak_lattice:
ballarin@65099
   110
  "weak_lattice (inv_gorder L)"
ballarin@65099
   111
proof -
ballarin@65099
   112
  interpret dual: weak_partial_order "inv_gorder L"
ballarin@65099
   113
    by (metis dual_weak_order)
ballarin@65099
   114
ballarin@65099
   115
  show ?thesis
ballarin@65099
   116
    apply (unfold_locales)
ballarin@65099
   117
    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
ballarin@65099
   118
  done
ballarin@65099
   119
qed
ballarin@65099
   120
wenzelm@14666
   121
wenzelm@61382
   122
subsubsection \<open>Supremum\<close>
ballarin@14551
   123
ballarin@27713
   124
lemma (in weak_upper_semilattice) joinI:
ballarin@22063
   125
  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
ballarin@14551
   126
  ==> P (x \<squnion> y)"
ballarin@14551
   127
proof (unfold join_def sup_def)
ballarin@22063
   128
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@22063
   129
    and P: "!!l. least L l (Upper L {x, y}) ==> P l"
ballarin@22063
   130
  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
ballarin@27713
   131
  with L show "P (SOME l. least L l (Upper L {x, y}))"
ballarin@27713
   132
    by (fast intro: someI2 P)
ballarin@14551
   133
qed
ballarin@14551
   134
ballarin@27713
   135
lemma (in weak_upper_semilattice) join_closed [simp]:
ballarin@22063
   136
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
ballarin@27700
   137
  by (rule joinI) (rule least_closed)
ballarin@14551
   138
ballarin@27713
   139
lemma (in weak_upper_semilattice) join_cong_l:
ballarin@27713
   140
  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
ballarin@27713
   141
    and xx': "x .= x'"
ballarin@27713
   142
  shows "x \<squnion> y .= x' \<squnion> y"
ballarin@27713
   143
proof (rule joinI, rule joinI)
ballarin@27713
   144
  fix a b
ballarin@27713
   145
  from xx' carr
ballarin@27713
   146
      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
ballarin@27713
   147
ballarin@27713
   148
  assume leasta: "least L a (Upper L {x, y})"
ballarin@27713
   149
  assume "least L b (Upper L {x', y})"
ballarin@27713
   150
  with carr
ballarin@27713
   151
      have leastb: "least L b (Upper L {x, y})"
ballarin@27713
   152
      by (simp add: least_Upper_cong_r[OF _ _ seq])
ballarin@27713
   153
ballarin@27713
   154
  from leasta leastb
ballarin@27713
   155
      show "a .= b" by (rule weak_least_unique)
ballarin@27713
   156
qed (rule carr)+
ballarin@14551
   157
ballarin@27713
   158
lemma (in weak_upper_semilattice) join_cong_r:
ballarin@27713
   159
  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
ballarin@27713
   160
    and yy': "y .= y'"
ballarin@27713
   161
  shows "x \<squnion> y .= x \<squnion> y'"
ballarin@27713
   162
proof (rule joinI, rule joinI)
ballarin@27713
   163
  fix a b
ballarin@27713
   164
  have "{x, y} = {y, x}" by fast
ballarin@27713
   165
  also from carr yy'
ballarin@27713
   166
      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
ballarin@27713
   167
  also have "{y', x} = {x, y'}" by fast
ballarin@27713
   168
  finally
ballarin@27713
   169
      have seq: "{x, y} {.=} {x, y'}" .
ballarin@14551
   170
ballarin@27713
   171
  assume leasta: "least L a (Upper L {x, y})"
ballarin@27713
   172
  assume "least L b (Upper L {x, y'})"
ballarin@27713
   173
  with carr
ballarin@27713
   174
      have leastb: "least L b (Upper L {x, y})"
ballarin@27713
   175
      by (simp add: least_Upper_cong_r[OF _ _ seq])
ballarin@27713
   176
ballarin@27713
   177
  from leasta leastb
ballarin@27713
   178
      show "a .= b" by (rule weak_least_unique)
ballarin@27713
   179
qed (rule carr)+
ballarin@27713
   180
ballarin@27713
   181
lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
ballarin@27713
   182
  "x \<in> carrier L ==> least L x (Upper L {x})"
ballarin@27713
   183
  by (rule least_UpperI) auto
ballarin@27713
   184
ballarin@27713
   185
lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
ballarin@27713
   186
  "x \<in> carrier L ==> \<Squnion>{x} .= x"
ballarin@27713
   187
  unfolding sup_def
ballarin@27713
   188
  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
ballarin@27713
   189
ballarin@27713
   190
lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
ballarin@27713
   191
  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
ballarin@27713
   192
  unfolding sup_def
ballarin@27713
   193
  by (rule someI2) (auto intro: sup_of_singletonI)
wenzelm@14666
   194
wenzelm@63167
   195
text \<open>Condition on \<open>A\<close>: supremum exists.\<close>
ballarin@14551
   196
ballarin@27713
   197
lemma (in weak_upper_semilattice) sup_insertI:
ballarin@22063
   198
  "[| !!s. least L s (Upper L (insert x A)) ==> P s;
ballarin@22063
   199
  least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
wenzelm@14693
   200
  ==> P (\<Squnion>(insert x A))"
ballarin@14551
   201
proof (unfold sup_def)
ballarin@22063
   202
  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
ballarin@22063
   203
    and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
ballarin@22063
   204
    and least_a: "least L a (Upper L A)"
ballarin@22063
   205
  from L least_a have La: "a \<in> carrier L" by simp
ballarin@14551
   206
  from L sup_of_two_exists least_a
ballarin@22063
   207
  obtain s where least_s: "least L s (Upper L {a, x})" by blast
ballarin@27713
   208
  show "P (SOME l. least L l (Upper L (insert x A)))"
ballarin@27713
   209
  proof (rule someI2)
ballarin@22063
   210
    show "least L s (Upper L (insert x A))"
ballarin@14551
   211
    proof (rule least_UpperI)
ballarin@14551
   212
      fix z
wenzelm@14693
   213
      assume "z \<in> insert x A"
wenzelm@14693
   214
      then show "z \<sqsubseteq> s"
wenzelm@14693
   215
      proof
wenzelm@14693
   216
        assume "z = x" then show ?thesis
wenzelm@14693
   217
          by (simp add: least_Upper_above [OF least_s] L La)
wenzelm@14693
   218
      next
wenzelm@14693
   219
        assume "z \<in> A"
wenzelm@14693
   220
        with L least_s least_a show ?thesis
ballarin@27713
   221
          by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
wenzelm@14693
   222
      qed
wenzelm@14693
   223
    next
wenzelm@14693
   224
      fix y
ballarin@22063
   225
      assume y: "y \<in> Upper L (insert x A)"
wenzelm@14693
   226
      show "s \<sqsubseteq> y"
wenzelm@14693
   227
      proof (rule least_le [OF least_s], rule Upper_memI)
wenzelm@32960
   228
        fix z
wenzelm@32960
   229
        assume z: "z \<in> {a, x}"
wenzelm@32960
   230
        then show "z \<sqsubseteq> y"
wenzelm@32960
   231
        proof
ballarin@22063
   232
          have y': "y \<in> Upper L A"
ballarin@22063
   233
            apply (rule subsetD [where A = "Upper L (insert x A)"])
wenzelm@23463
   234
             apply (rule Upper_antimono)
wenzelm@32960
   235
             apply blast
wenzelm@32960
   236
            apply (rule y)
wenzelm@14693
   237
            done
wenzelm@14693
   238
          assume "z = a"
wenzelm@14693
   239
          with y' least_a show ?thesis by (fast dest: least_le)
wenzelm@32960
   240
        next
wenzelm@32960
   241
          assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
wenzelm@14693
   242
          with y L show ?thesis by blast
wenzelm@32960
   243
        qed
wenzelm@23350
   244
      qed (rule Upper_closed [THEN subsetD, OF y])
wenzelm@14693
   245
    next
ballarin@22063
   246
      from L show "insert x A \<subseteq> carrier L" by simp
ballarin@22063
   247
      from least_s show "s \<in> carrier L" by simp
ballarin@14551
   248
    qed
wenzelm@23350
   249
  qed (rule P)
ballarin@14551
   250
qed
ballarin@14551
   251
ballarin@27713
   252
lemma (in weak_upper_semilattice) finite_sup_least:
ballarin@22063
   253
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
berghofe@22265
   254
proof (induct set: finite)
wenzelm@14693
   255
  case empty
wenzelm@14693
   256
  then show ?case by simp
ballarin@14551
   257
next
nipkow@15328
   258
  case (insert x A)
ballarin@14551
   259
  show ?case
ballarin@14551
   260
  proof (cases "A = {}")
ballarin@14551
   261
    case True
ballarin@27713
   262
    with insert show ?thesis
wenzelm@44472
   263
      by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
wenzelm@32960
   264
        (* The above step is hairy; least_cong can make simp loop.
wenzelm@32960
   265
        Would want special version of simp to apply least_cong. *)
ballarin@14551
   266
  next
ballarin@14551
   267
    case False
ballarin@22063
   268
    with insert have "least L (\<Squnion>A) (Upper L A)" by simp
wenzelm@14693
   269
    with _ show ?thesis
wenzelm@14693
   270
      by (rule sup_insertI) (simp_all add: insert [simplified])
ballarin@14551
   271
  qed
ballarin@14551
   272
qed
ballarin@14551
   273
ballarin@27713
   274
lemma (in weak_upper_semilattice) finite_sup_insertI:
ballarin@22063
   275
  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
ballarin@22063
   276
    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
ballarin@65099
   277
  shows "P (\<Squnion> (insert x A))"
ballarin@14551
   278
proof (cases "A = {}")
ballarin@14551
   279
  case True with P and xA show ?thesis
ballarin@27713
   280
    by (simp add: finite_sup_least)
ballarin@14551
   281
next
ballarin@14551
   282
  case False with P and xA show ?thesis
ballarin@14551
   283
    by (simp add: sup_insertI finite_sup_least)
ballarin@14551
   284
qed
ballarin@14551
   285
ballarin@27713
   286
lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
ballarin@22063
   287
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
berghofe@22265
   288
proof (induct set: finite)
ballarin@14551
   289
  case empty then show ?case by simp
ballarin@14551
   290
next
nipkow@15328
   291
  case insert then show ?case
wenzelm@14693
   292
    by - (rule finite_sup_insertI, simp_all)
ballarin@14551
   293
qed
ballarin@14551
   294
ballarin@27713
   295
lemma (in weak_upper_semilattice) join_left:
ballarin@22063
   296
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
wenzelm@14693
   297
  by (rule joinI [folded join_def]) (blast dest: least_mem)
ballarin@14551
   298
ballarin@27713
   299
lemma (in weak_upper_semilattice) join_right:
ballarin@22063
   300
  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
wenzelm@14693
   301
  by (rule joinI [folded join_def]) (blast dest: least_mem)
ballarin@14551
   302
ballarin@27713
   303
lemma (in weak_upper_semilattice) sup_of_two_least:
ballarin@22063
   304
  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
ballarin@14551
   305
proof (unfold sup_def)
ballarin@22063
   306
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@22063
   307
  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
ballarin@27713
   308
  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
ballarin@27713
   309
  by (fast intro: someI2 weak_least_unique)  (* blast fails *)
ballarin@14551
   310
qed
ballarin@14551
   311
ballarin@27713
   312
lemma (in weak_upper_semilattice) join_le:
wenzelm@14693
   313
  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
wenzelm@23350
   314
    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
ballarin@14551
   315
  shows "x \<squnion> y \<sqsubseteq> z"
wenzelm@23350
   316
proof (rule joinI [OF _ x y])
ballarin@14551
   317
  fix s
ballarin@22063
   318
  assume "least L s (Upper L {x, y})"
wenzelm@23350
   319
  with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
ballarin@14551
   320
qed
wenzelm@14693
   321
ballarin@65099
   322
lemma (in weak_lattice) weak_le_iff_meet:
ballarin@65099
   323
  assumes "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
   324
  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
ballarin@65099
   325
  by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
ballarin@65099
   326
  
ballarin@27713
   327
lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
ballarin@22063
   328
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@27713
   329
  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
ballarin@14551
   330
proof (rule finite_sup_insertI)
wenzelm@63167
   331
  \<comment> \<open>The textbook argument in Jacobson I, p 457\<close>
ballarin@14551
   332
  fix s
ballarin@22063
   333
  assume sup: "least L s (Upper L {x, y, z})"
ballarin@27713
   334
  show "x \<squnion> (y \<squnion> z) .= s"
nipkow@33657
   335
  proof (rule weak_le_antisym)
ballarin@14551
   336
    from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
nipkow@44890
   337
      by (fastforce intro!: join_le elim: least_Upper_above)
ballarin@14551
   338
  next
ballarin@14551
   339
    from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
ballarin@14551
   340
    by (erule_tac least_le)
ballarin@27713
   341
      (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
ballarin@27700
   342
  qed (simp_all add: L least_closed [OF sup])
ballarin@14551
   343
qed (simp_all add: L)
ballarin@14551
   344
wenzelm@63167
   345
text \<open>Commutativity holds for \<open>=\<close>.\<close>
ballarin@27713
   346
ballarin@22063
   347
lemma join_comm:
ballarin@22063
   348
  fixes L (structure)
ballarin@22063
   349
  shows "x \<squnion> y = y \<squnion> x"
ballarin@14551
   350
  by (unfold join_def) (simp add: insert_commute)
ballarin@14551
   351
ballarin@27713
   352
lemma (in weak_upper_semilattice) weak_join_assoc:
ballarin@22063
   353
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@27713
   354
  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
ballarin@14551
   355
proof -
ballarin@27713
   356
  (* FIXME: could be simplified by improved simp: uniform use of .=,
ballarin@27713
   357
     omit [symmetric] in last step. *)
ballarin@14551
   358
  have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
ballarin@27713
   359
  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
wenzelm@14693
   360
  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
ballarin@27713
   361
  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
ballarin@27713
   362
  finally show ?thesis by (simp add: L)
ballarin@14551
   363
qed
ballarin@14551
   364
wenzelm@14693
   365
wenzelm@61382
   366
subsubsection \<open>Infimum\<close>
ballarin@14551
   367
ballarin@27713
   368
lemma (in weak_lower_semilattice) meetI:
ballarin@22063
   369
  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
ballarin@22063
   370
  x \<in> carrier L; y \<in> carrier L |]
ballarin@14551
   371
  ==> P (x \<sqinter> y)"
ballarin@14551
   372
proof (unfold meet_def inf_def)
ballarin@22063
   373
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@22063
   374
    and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
ballarin@22063
   375
  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
ballarin@27713
   376
  with L show "P (SOME g. greatest L g (Lower L {x, y}))"
ballarin@27713
   377
  by (fast intro: someI2 weak_greatest_unique P)
ballarin@14551
   378
qed
ballarin@14551
   379
ballarin@27713
   380
lemma (in weak_lower_semilattice) meet_closed [simp]:
ballarin@22063
   381
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
ballarin@27700
   382
  by (rule meetI) (rule greatest_closed)
ballarin@14551
   383
ballarin@27713
   384
lemma (in weak_lower_semilattice) meet_cong_l:
ballarin@27713
   385
  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
ballarin@27713
   386
    and xx': "x .= x'"
ballarin@27713
   387
  shows "x \<sqinter> y .= x' \<sqinter> y"
ballarin@27713
   388
proof (rule meetI, rule meetI)
ballarin@27713
   389
  fix a b
ballarin@27713
   390
  from xx' carr
ballarin@27713
   391
      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
ballarin@27713
   392
ballarin@27713
   393
  assume greatesta: "greatest L a (Lower L {x, y})"
ballarin@27713
   394
  assume "greatest L b (Lower L {x', y})"
ballarin@27713
   395
  with carr
ballarin@27713
   396
      have greatestb: "greatest L b (Lower L {x, y})"
ballarin@27713
   397
      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
ballarin@27713
   398
ballarin@27713
   399
  from greatesta greatestb
ballarin@27713
   400
      show "a .= b" by (rule weak_greatest_unique)
ballarin@27713
   401
qed (rule carr)+
ballarin@14551
   402
ballarin@27713
   403
lemma (in weak_lower_semilattice) meet_cong_r:
ballarin@27713
   404
  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
ballarin@27713
   405
    and yy': "y .= y'"
ballarin@27713
   406
  shows "x \<sqinter> y .= x \<sqinter> y'"
ballarin@27713
   407
proof (rule meetI, rule meetI)
ballarin@27713
   408
  fix a b
ballarin@27713
   409
  have "{x, y} = {y, x}" by fast
ballarin@27713
   410
  also from carr yy'
ballarin@27713
   411
      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
ballarin@27713
   412
  also have "{y', x} = {x, y'}" by fast
ballarin@27713
   413
  finally
ballarin@27713
   414
      have seq: "{x, y} {.=} {x, y'}" .
ballarin@27713
   415
ballarin@27713
   416
  assume greatesta: "greatest L a (Lower L {x, y})"
ballarin@27713
   417
  assume "greatest L b (Lower L {x, y'})"
ballarin@27713
   418
  with carr
ballarin@27713
   419
      have greatestb: "greatest L b (Lower L {x, y})"
ballarin@27713
   420
      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
ballarin@14551
   421
ballarin@27713
   422
  from greatesta greatestb
ballarin@27713
   423
      show "a .= b" by (rule weak_greatest_unique)
ballarin@27713
   424
qed (rule carr)+
ballarin@27713
   425
ballarin@27713
   426
lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
ballarin@27713
   427
  "x \<in> carrier L ==> greatest L x (Lower L {x})"
ballarin@27713
   428
  by (rule greatest_LowerI) auto
ballarin@14551
   429
ballarin@27713
   430
lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
ballarin@27713
   431
  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
ballarin@27713
   432
  unfolding inf_def
ballarin@27713
   433
  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
ballarin@27713
   434
ballarin@27713
   435
lemma (in weak_partial_order) inf_of_singleton_closed:
ballarin@27713
   436
  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
ballarin@27713
   437
  unfolding inf_def
ballarin@27713
   438
  by (rule someI2) (auto intro: inf_of_singletonI)
ballarin@27713
   439
wenzelm@63167
   440
text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
ballarin@27713
   441
ballarin@27713
   442
lemma (in weak_lower_semilattice) inf_insertI:
ballarin@22063
   443
  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
ballarin@22063
   444
  greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
wenzelm@14693
   445
  ==> P (\<Sqinter>(insert x A))"
ballarin@14551
   446
proof (unfold inf_def)
ballarin@22063
   447
  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
ballarin@22063
   448
    and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
ballarin@22063
   449
    and greatest_a: "greatest L a (Lower L A)"
ballarin@22063
   450
  from L greatest_a have La: "a \<in> carrier L" by simp
ballarin@14551
   451
  from L inf_of_two_exists greatest_a
ballarin@22063
   452
  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
ballarin@27713
   453
  show "P (SOME g. greatest L g (Lower L (insert x A)))"
ballarin@27713
   454
  proof (rule someI2)
ballarin@22063
   455
    show "greatest L i (Lower L (insert x A))"
ballarin@14551
   456
    proof (rule greatest_LowerI)
ballarin@14551
   457
      fix z
wenzelm@14693
   458
      assume "z \<in> insert x A"
wenzelm@14693
   459
      then show "i \<sqsubseteq> z"
wenzelm@14693
   460
      proof
wenzelm@14693
   461
        assume "z = x" then show ?thesis
ballarin@27700
   462
          by (simp add: greatest_Lower_below [OF greatest_i] L La)
wenzelm@14693
   463
      next
wenzelm@14693
   464
        assume "z \<in> A"
wenzelm@14693
   465
        with L greatest_i greatest_a show ?thesis
ballarin@27713
   466
          by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
wenzelm@14693
   467
      qed
wenzelm@14693
   468
    next
wenzelm@14693
   469
      fix y
ballarin@22063
   470
      assume y: "y \<in> Lower L (insert x A)"
wenzelm@14693
   471
      show "y \<sqsubseteq> i"
wenzelm@14693
   472
      proof (rule greatest_le [OF greatest_i], rule Lower_memI)
wenzelm@32960
   473
        fix z
wenzelm@32960
   474
        assume z: "z \<in> {a, x}"
wenzelm@32960
   475
        then show "y \<sqsubseteq> z"
wenzelm@32960
   476
        proof
ballarin@22063
   477
          have y': "y \<in> Lower L A"
ballarin@22063
   478
            apply (rule subsetD [where A = "Lower L (insert x A)"])
wenzelm@23463
   479
            apply (rule Lower_antimono)
wenzelm@32960
   480
             apply blast
wenzelm@32960
   481
            apply (rule y)
wenzelm@14693
   482
            done
wenzelm@14693
   483
          assume "z = a"
wenzelm@14693
   484
          with y' greatest_a show ?thesis by (fast dest: greatest_le)
wenzelm@32960
   485
        next
wenzelm@14693
   486
          assume "z \<in> {x}"
wenzelm@14693
   487
          with y L show ?thesis by blast
wenzelm@32960
   488
        qed
wenzelm@23350
   489
      qed (rule Lower_closed [THEN subsetD, OF y])
wenzelm@14693
   490
    next
ballarin@22063
   491
      from L show "insert x A \<subseteq> carrier L" by simp
ballarin@22063
   492
      from greatest_i show "i \<in> carrier L" by simp
ballarin@14551
   493
    qed
wenzelm@23350
   494
  qed (rule P)
ballarin@14551
   495
qed
ballarin@14551
   496
ballarin@27713
   497
lemma (in weak_lower_semilattice) finite_inf_greatest:
ballarin@22063
   498
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
berghofe@22265
   499
proof (induct set: finite)
ballarin@14551
   500
  case empty then show ?case by simp
ballarin@14551
   501
next
nipkow@15328
   502
  case (insert x A)
ballarin@14551
   503
  show ?case
ballarin@14551
   504
  proof (cases "A = {}")
ballarin@14551
   505
    case True
ballarin@27713
   506
    with insert show ?thesis
ballarin@27713
   507
      by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
wenzelm@32960
   508
        inf_of_singleton_closed inf_of_singletonI)
ballarin@14551
   509
  next
ballarin@14551
   510
    case False
ballarin@14551
   511
    from insert show ?thesis
ballarin@14551
   512
    proof (rule_tac inf_insertI)
ballarin@22063
   513
      from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
ballarin@14551
   514
    qed simp_all
ballarin@14551
   515
  qed
ballarin@14551
   516
qed
ballarin@14551
   517
ballarin@27713
   518
lemma (in weak_lower_semilattice) finite_inf_insertI:
ballarin@22063
   519
  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
ballarin@22063
   520
    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
ballarin@65099
   521
  shows "P (\<Sqinter> (insert x A))"
ballarin@14551
   522
proof (cases "A = {}")
ballarin@14551
   523
  case True with P and xA show ?thesis
ballarin@27713
   524
    by (simp add: finite_inf_greatest)
ballarin@14551
   525
next
ballarin@14551
   526
  case False with P and xA show ?thesis
ballarin@14551
   527
    by (simp add: inf_insertI finite_inf_greatest)
ballarin@14551
   528
qed
ballarin@14551
   529
ballarin@27713
   530
lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
ballarin@22063
   531
  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
berghofe@22265
   532
proof (induct set: finite)
ballarin@14551
   533
  case empty then show ?case by simp
ballarin@14551
   534
next
nipkow@15328
   535
  case insert then show ?case
ballarin@14551
   536
    by (rule_tac finite_inf_insertI) (simp_all)
ballarin@14551
   537
qed
ballarin@14551
   538
ballarin@27713
   539
lemma (in weak_lower_semilattice) meet_left:
ballarin@22063
   540
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
wenzelm@14693
   541
  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
ballarin@14551
   542
ballarin@27713
   543
lemma (in weak_lower_semilattice) meet_right:
ballarin@22063
   544
  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
wenzelm@14693
   545
  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
ballarin@14551
   546
ballarin@27713
   547
lemma (in weak_lower_semilattice) inf_of_two_greatest:
ballarin@22063
   548
  "[| x \<in> carrier L; y \<in> carrier L |] ==>
wenzelm@60585
   549
  greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
ballarin@14551
   550
proof (unfold inf_def)
ballarin@22063
   551
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@22063
   552
  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
ballarin@14551
   553
  with L
ballarin@27713
   554
  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
ballarin@27713
   555
  by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
ballarin@14551
   556
qed
ballarin@14551
   557
ballarin@27713
   558
lemma (in weak_lower_semilattice) meet_le:
wenzelm@14693
   559
  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
wenzelm@23350
   560
    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
ballarin@14551
   561
  shows "z \<sqsubseteq> x \<sqinter> y"
wenzelm@23350
   562
proof (rule meetI [OF _ x y])
ballarin@14551
   563
  fix i
ballarin@22063
   564
  assume "greatest L i (Lower L {x, y})"
wenzelm@23350
   565
  with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
ballarin@14551
   566
qed
wenzelm@14693
   567
ballarin@65099
   568
lemma (in weak_lattice) weak_le_iff_join:
ballarin@65099
   569
  assumes "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
   570
  shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
ballarin@65099
   571
  by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)
ballarin@65099
   572
  
ballarin@27713
   573
lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
ballarin@22063
   574
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@27713
   575
  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
ballarin@14551
   576
proof (rule finite_inf_insertI)
wenzelm@61382
   577
  txt \<open>The textbook argument in Jacobson I, p 457\<close>
ballarin@14551
   578
  fix i
ballarin@22063
   579
  assume inf: "greatest L i (Lower L {x, y, z})"
ballarin@27713
   580
  show "x \<sqinter> (y \<sqinter> z) .= i"
nipkow@33657
   581
  proof (rule weak_le_antisym)
ballarin@14551
   582
    from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
nipkow@44890
   583
      by (fastforce intro!: meet_le elim: greatest_Lower_below)
ballarin@14551
   584
  next
ballarin@14551
   585
    from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
ballarin@14551
   586
    by (erule_tac greatest_le)
ballarin@27713
   587
      (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
ballarin@27700
   588
  qed (simp_all add: L greatest_closed [OF inf])
ballarin@14551
   589
qed (simp_all add: L)
ballarin@14551
   590
ballarin@22063
   591
lemma meet_comm:
ballarin@22063
   592
  fixes L (structure)
ballarin@22063
   593
  shows "x \<sqinter> y = y \<sqinter> x"
ballarin@14551
   594
  by (unfold meet_def) (simp add: insert_commute)
ballarin@14551
   595
ballarin@27713
   596
lemma (in weak_lower_semilattice) weak_meet_assoc:
ballarin@22063
   597
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@27713
   598
  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
ballarin@14551
   599
proof -
ballarin@27713
   600
  (* FIXME: improved simp, see weak_join_assoc above *)
ballarin@14551
   601
  have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
ballarin@65099
   602
  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
ballarin@65099
   603
  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
ballarin@27713
   604
  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
ballarin@27713
   605
  finally show ?thesis by (simp add: L)
ballarin@14551
   606
qed
ballarin@14551
   607
wenzelm@61382
   608
text \<open>Total orders are lattices.\<close>
ballarin@24087
   609
ballarin@65099
   610
sublocale weak_total_order \<subseteq> weak?: weak_lattice
haftmann@28823
   611
proof
ballarin@24087
   612
  fix x y
ballarin@24087
   613
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@24087
   614
  show "EX s. least L s (Upper L {x, y})"
ballarin@24087
   615
  proof -
ballarin@24087
   616
    note total L
ballarin@24087
   617
    moreover
ballarin@24087
   618
    {
ballarin@24087
   619
      assume "x \<sqsubseteq> y"
ballarin@24087
   620
      with L have "least L y (Upper L {x, y})"
ballarin@24087
   621
        by (rule_tac least_UpperI) auto
ballarin@24087
   622
    }
ballarin@24087
   623
    moreover
ballarin@24087
   624
    {
ballarin@24087
   625
      assume "y \<sqsubseteq> x"
ballarin@24087
   626
      with L have "least L x (Upper L {x, y})"
ballarin@24087
   627
        by (rule_tac least_UpperI) auto
ballarin@24087
   628
    }
ballarin@24087
   629
    ultimately show ?thesis by blast
ballarin@14551
   630
  qed
ballarin@24087
   631
next
ballarin@24087
   632
  fix x y
ballarin@24087
   633
  assume L: "x \<in> carrier L"  "y \<in> carrier L"
ballarin@24087
   634
  show "EX i. greatest L i (Lower L {x, y})"
ballarin@24087
   635
  proof -
ballarin@24087
   636
    note total L
ballarin@24087
   637
    moreover
ballarin@24087
   638
    {
ballarin@24087
   639
      assume "y \<sqsubseteq> x"
ballarin@24087
   640
      with L have "greatest L y (Lower L {x, y})"
ballarin@24087
   641
        by (rule_tac greatest_LowerI) auto
ballarin@24087
   642
    }
ballarin@24087
   643
    moreover
ballarin@24087
   644
    {
ballarin@24087
   645
      assume "x \<sqsubseteq> y"
ballarin@24087
   646
      with L have "greatest L x (Lower L {x, y})"
ballarin@24087
   647
        by (rule_tac greatest_LowerI) auto
ballarin@24087
   648
    }
ballarin@24087
   649
    ultimately show ?thesis by blast
ballarin@24087
   650
  qed
ballarin@24087
   651
qed
ballarin@14551
   652
wenzelm@14693
   653
ballarin@65099
   654
subsection \<open>Weak Bounded Lattices\<close>
ballarin@14551
   655
ballarin@65099
   656
locale weak_bounded_lattice = 
ballarin@65099
   657
  weak_lattice + 
ballarin@65099
   658
  weak_partial_order_bottom + 
ballarin@65099
   659
  weak_partial_order_top
ballarin@27713
   660
begin
ballarin@27713
   661
ballarin@65099
   662
lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
ballarin@65099
   663
  by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
ballarin@27713
   664
ballarin@65099
   665
lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
ballarin@65099
   666
  by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
ballarin@27713
   667
ballarin@65099
   668
lemma bottom_weak_eq:
ballarin@65099
   669
  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
ballarin@65099
   670
  by (metis bottom_closed bottom_lower weak_le_antisym)
ballarin@27713
   671
ballarin@65099
   672
lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
ballarin@65099
   673
  by (metis join_closed join_left top_closed top_higher weak_le_antisym)
ballarin@65099
   674
ballarin@65099
   675
lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
ballarin@65099
   676
  by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
ballarin@65099
   677
ballarin@65099
   678
lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
ballarin@65099
   679
  by (metis top_closed top_higher weak_le_antisym)
ballarin@27713
   680
ballarin@27713
   681
end
ballarin@27713
   682
ballarin@65099
   683
sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
ballarin@27713
   684
ballarin@27713
   685
ballarin@65099
   686
subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
ballarin@27713
   687
ballarin@27713
   688
locale upper_semilattice = partial_order +
ballarin@27713
   689
  assumes sup_of_two_exists:
ballarin@27713
   690
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
ballarin@27713
   691
ballarin@65099
   692
sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
ballarin@65099
   693
  by unfold_locales (rule sup_of_two_exists)
ballarin@27713
   694
ballarin@27713
   695
locale lower_semilattice = partial_order +
ballarin@27713
   696
  assumes inf_of_two_exists:
ballarin@27713
   697
    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
ballarin@27713
   698
ballarin@65099
   699
sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
ballarin@65099
   700
  by unfold_locales (rule inf_of_two_exists)
ballarin@27713
   701
ballarin@27713
   702
locale lattice = upper_semilattice + lower_semilattice
ballarin@27713
   703
ballarin@65099
   704
sublocale lattice \<subseteq> weak_lattice ..
ballarin@27713
   705
ballarin@65099
   706
lemma (in lattice) dual_lattice:
ballarin@65099
   707
  "lattice (inv_gorder L)"
ballarin@65099
   708
proof -
ballarin@65099
   709
  interpret dual: weak_lattice "inv_gorder L"
ballarin@65099
   710
    by (metis dual_weak_lattice)
ballarin@27713
   711
ballarin@65099
   712
  show ?thesis
ballarin@65099
   713
    apply (unfold_locales)
ballarin@65099
   714
    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
ballarin@65099
   715
    apply (simp add:eq_is_equal)
ballarin@65099
   716
  done
ballarin@65099
   717
qed
ballarin@65099
   718
  
ballarin@65099
   719
lemma (in lattice) le_iff_join:
ballarin@65099
   720
  assumes "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
   721
  shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
ballarin@65099
   722
  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
ballarin@27713
   723
ballarin@65099
   724
lemma (in lattice) le_iff_meet:
ballarin@65099
   725
  assumes "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
   726
  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
ballarin@65099
   727
  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
ballarin@27713
   728
ballarin@65099
   729
text \<open> Total orders are lattices. \<close>
ballarin@27713
   730
ballarin@65099
   731
sublocale total_order \<subseteq> weak?: lattice
ballarin@65099
   732
  by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
ballarin@65099
   733
    
ballarin@65099
   734
text \<open>Functions that preserve joins and meets\<close>
ballarin@65099
   735
  
ballarin@65099
   736
definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
   737
"join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)"
ballarin@27713
   738
ballarin@65099
   739
definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
   740
"meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)"
ballarin@27713
   741
ballarin@65099
   742
lemma join_pres_isotone:
ballarin@65099
   743
  assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
ballarin@65099
   744
  shows "isotone X Y f"
ballarin@65099
   745
  using assms
ballarin@65099
   746
  apply (rule_tac isotoneI)
ballarin@65099
   747
  apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
ballarin@65099
   748
  using lattice_def partial_order_def upper_semilattice_def apply blast
ballarin@65099
   749
  using lattice_def partial_order_def upper_semilattice_def apply blast
ballarin@65099
   750
  apply fastforce
ballarin@65099
   751
done
ballarin@27713
   752
ballarin@65099
   753
lemma meet_pres_isotone:
ballarin@65099
   754
  assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
ballarin@65099
   755
  shows "isotone X Y f"
ballarin@65099
   756
  using assms
ballarin@65099
   757
  apply (rule_tac isotoneI)
ballarin@65099
   758
  apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
ballarin@65099
   759
  using lattice_def partial_order_def upper_semilattice_def apply blast
ballarin@65099
   760
  using lattice_def partial_order_def upper_semilattice_def apply blast
ballarin@65099
   761
  apply fastforce
ballarin@65099
   762
done
ballarin@27713
   763
ballarin@27713
   764
ballarin@65099
   765
subsection \<open>Bounded Lattices\<close>
ballarin@27713
   766
ballarin@65099
   767
locale bounded_lattice = 
ballarin@65099
   768
  lattice + 
ballarin@65099
   769
  weak_partial_order_bottom + 
ballarin@65099
   770
  weak_partial_order_top
ballarin@27713
   771
ballarin@65099
   772
sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
ballarin@27713
   773
ballarin@65099
   774
context bounded_lattice
ballarin@65099
   775
begin
ballarin@14551
   776
ballarin@65099
   777
lemma bottom_eq:  
ballarin@65099
   778
  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
ballarin@65099
   779
  by (metis bottom_closed bottom_lower le_antisym)
ballarin@14551
   780
ballarin@65099
   781
lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
ballarin@65099
   782
  by (metis le_antisym top_closed top_higher)
ballarin@14551
   783
wenzelm@14693
   784
end
ballarin@65099
   785
ballarin@65099
   786
end