src/HOL/Library/Lattice_Constructions.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60679 ade12ef2773c
child 62390 842917225d56
permissions -rw-r--r--
more symbols;
Andreas@57998
     1
(*  Title:      HOL/Library/Lattice_Constructions.thy
bulwahn@37915
     2
    Author:     Lukas Bulwahn
bulwahn@37915
     3
    Copyright   2010 TU Muenchen
bulwahn@37915
     4
*)
bulwahn@37915
     5
Andreas@57998
     6
theory Lattice_Constructions
wenzelm@57645
     7
imports Main
bulwahn@37915
     8
begin
bulwahn@37915
     9
wenzelm@60500
    10
subsection \<open>Values extended by a bottom element\<close>
bulwahn@37915
    11
blanchet@58310
    12
datatype 'a bot = Value 'a | Bot
bulwahn@37915
    13
bulwahn@37915
    14
instantiation bot :: (preorder) preorder
bulwahn@37915
    15
begin
bulwahn@37915
    16
bulwahn@37915
    17
definition less_eq_bot where
bulwahn@37915
    18
  "x \<le> y \<longleftrightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> x \<le> y))"
bulwahn@37915
    19
bulwahn@37915
    20
definition less_bot where
bulwahn@37915
    21
  "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
bulwahn@37915
    22
bulwahn@37915
    23
lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
bulwahn@37915
    24
  by (simp add: less_eq_bot_def)
bulwahn@37915
    25
bulwahn@37915
    26
lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
bulwahn@37915
    27
  by simp
bulwahn@37915
    28
bulwahn@37915
    29
lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
bulwahn@37915
    30
  by (cases x) (simp_all add: less_eq_bot_def)
bulwahn@37915
    31
bulwahn@37915
    32
lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
bulwahn@37915
    33
  by (simp add: less_eq_bot_def)
bulwahn@37915
    34
bulwahn@37915
    35
lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
bulwahn@37915
    36
  by (simp add: less_eq_bot_def)
bulwahn@37915
    37
bulwahn@37915
    38
lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
bulwahn@37915
    39
  by (simp add: less_bot_def)
bulwahn@37915
    40
bulwahn@37915
    41
lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
bulwahn@37915
    42
  by (cases x) (simp_all add: less_bot_def)
bulwahn@37915
    43
bulwahn@37915
    44
lemma less_bot_Bot_Value [simp]: "Bot < Value x"
bulwahn@37915
    45
  by (simp add: less_bot_def)
bulwahn@37915
    46
bulwahn@37915
    47
lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
bulwahn@37915
    48
  by simp
bulwahn@37915
    49
bulwahn@37915
    50
lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
bulwahn@37915
    51
  by (simp add: less_bot_def)
bulwahn@37915
    52
wenzelm@60508
    53
instance
wenzelm@60679
    54
  by standard
wenzelm@60508
    55
    (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
bulwahn@37915
    56
wenzelm@60508
    57
end
bulwahn@37915
    58
wenzelm@60508
    59
instance bot :: (order) order
wenzelm@60679
    60
  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915
    61
wenzelm@60508
    62
instance bot :: (linorder) linorder
wenzelm@60679
    63
  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915
    64
haftmann@43815
    65
instantiation bot :: (order) bot
bulwahn@37915
    66
begin
wenzelm@60508
    67
  definition "bot = Bot"
wenzelm@60508
    68
  instance ..
bulwahn@37915
    69
end
bulwahn@37915
    70
bulwahn@37915
    71
instantiation bot :: (top) top
bulwahn@37915
    72
begin
wenzelm@60508
    73
  definition "top = Value top"
wenzelm@60508
    74
  instance ..
bulwahn@37915
    75
end
bulwahn@37915
    76
bulwahn@37915
    77
instantiation bot :: (semilattice_inf) semilattice_inf
bulwahn@37915
    78
begin
bulwahn@37915
    79
bulwahn@37915
    80
definition inf_bot
bulwahn@37915
    81
where
wenzelm@60508
    82
  "inf x y =
wenzelm@60508
    83
    (case x of
wenzelm@60508
    84
      Bot \<Rightarrow> Bot
wenzelm@60508
    85
    | Value v \<Rightarrow>
wenzelm@60508
    86
        (case y of
wenzelm@60508
    87
          Bot \<Rightarrow> Bot
wenzelm@60508
    88
        | Value v' \<Rightarrow> Value (inf v v')))"
bulwahn@37915
    89
wenzelm@60508
    90
instance
wenzelm@60679
    91
  by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915
    92
bulwahn@37915
    93
end
bulwahn@37915
    94
bulwahn@37915
    95
instantiation bot :: (semilattice_sup) semilattice_sup
bulwahn@37915
    96
begin
bulwahn@37915
    97
bulwahn@37915
    98
definition sup_bot
bulwahn@37915
    99
where
wenzelm@60508
   100
  "sup x y =
wenzelm@60508
   101
    (case x of
wenzelm@60508
   102
      Bot \<Rightarrow> y
wenzelm@60508
   103
    | Value v \<Rightarrow>
wenzelm@60508
   104
        (case y of
wenzelm@60508
   105
          Bot \<Rightarrow> x
wenzelm@60508
   106
        | Value v' \<Rightarrow> Value (sup v v')))"
bulwahn@37915
   107
wenzelm@60508
   108
instance
wenzelm@60679
   109
  by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915
   110
bulwahn@37915
   111
end
bulwahn@37915
   112
Andreas@57543
   113
instance bot :: (lattice) bounded_lattice_bot
wenzelm@60508
   114
  by intro_classes (simp add: bot_bot_def)
bulwahn@37915
   115
wenzelm@60508
   116
wenzelm@60508
   117
subsection \<open>Values extended by a top element\<close>
bulwahn@37915
   118
blanchet@58310
   119
datatype 'a top = Value 'a | Top
bulwahn@37915
   120
bulwahn@37915
   121
instantiation top :: (preorder) preorder
bulwahn@37915
   122
begin
bulwahn@37915
   123
bulwahn@37915
   124
definition less_eq_top where
bulwahn@37915
   125
  "x \<le> y \<longleftrightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> x \<le> y))"
bulwahn@37915
   126
bulwahn@37915
   127
definition less_top where
bulwahn@37915
   128
  "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
bulwahn@37915
   129
wenzelm@60508
   130
lemma less_eq_top_Top [simp]: "x \<le> Top"
bulwahn@37915
   131
  by (simp add: less_eq_top_def)
bulwahn@37915
   132
bulwahn@37915
   133
lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
bulwahn@37915
   134
  by simp
bulwahn@37915
   135
bulwahn@37915
   136
lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
bulwahn@37915
   137
  by (cases x) (simp_all add: less_eq_top_def)
bulwahn@37915
   138
bulwahn@37915
   139
lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
bulwahn@37915
   140
  by (simp add: less_eq_top_def)
bulwahn@37915
   141
bulwahn@37915
   142
lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
bulwahn@37915
   143
  by (simp add: less_eq_top_def)
bulwahn@37915
   144
bulwahn@37915
   145
lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
bulwahn@37915
   146
  by (simp add: less_top_def)
bulwahn@37915
   147
bulwahn@37915
   148
lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
bulwahn@37915
   149
  by (cases x) (simp_all add: less_top_def)
bulwahn@37915
   150
bulwahn@37915
   151
lemma less_top_Value_Top [simp]: "Value x < Top"
bulwahn@37915
   152
  by (simp add: less_top_def)
bulwahn@37915
   153
bulwahn@37915
   154
lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
bulwahn@37915
   155
  by simp
bulwahn@37915
   156
bulwahn@37915
   157
lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
bulwahn@37915
   158
  by (simp add: less_top_def)
bulwahn@37915
   159
wenzelm@60508
   160
instance
wenzelm@60679
   161
  by standard
wenzelm@60508
   162
    (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
bulwahn@37915
   163
wenzelm@60508
   164
end
bulwahn@37915
   165
wenzelm@60508
   166
instance top :: (order) order
wenzelm@60679
   167
  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915
   168
wenzelm@60508
   169
instance top :: (linorder) linorder
wenzelm@60679
   170
  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915
   171
haftmann@43815
   172
instantiation top :: (order) top
bulwahn@37915
   173
begin
wenzelm@60508
   174
  definition "top = Top"
wenzelm@60508
   175
  instance ..
bulwahn@37915
   176
end
bulwahn@37915
   177
bulwahn@37915
   178
instantiation top :: (bot) bot
bulwahn@37915
   179
begin
wenzelm@60508
   180
  definition "bot = Value bot"
wenzelm@60508
   181
  instance ..
bulwahn@37915
   182
end
bulwahn@37915
   183
bulwahn@37915
   184
instantiation top :: (semilattice_inf) semilattice_inf
bulwahn@37915
   185
begin
bulwahn@37915
   186
bulwahn@37915
   187
definition inf_top
bulwahn@37915
   188
where
wenzelm@60508
   189
  "inf x y =
wenzelm@60508
   190
    (case x of
wenzelm@60508
   191
      Top \<Rightarrow> y
wenzelm@60508
   192
    | Value v \<Rightarrow>
wenzelm@60508
   193
        (case y of
wenzelm@60508
   194
          Top \<Rightarrow> x
wenzelm@60508
   195
        | Value v' \<Rightarrow> Value (inf v v')))"
bulwahn@37915
   196
wenzelm@60508
   197
instance
wenzelm@60679
   198
  by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
bulwahn@37915
   199
bulwahn@37915
   200
end
bulwahn@37915
   201
bulwahn@37915
   202
instantiation top :: (semilattice_sup) semilattice_sup
bulwahn@37915
   203
begin
bulwahn@37915
   204
bulwahn@37915
   205
definition sup_top
bulwahn@37915
   206
where
wenzelm@60508
   207
  "sup x y =
wenzelm@60508
   208
    (case x of
wenzelm@60508
   209
      Top \<Rightarrow> Top
wenzelm@60508
   210
    | Value v \<Rightarrow>
wenzelm@60508
   211
        (case y of
wenzelm@60508
   212
          Top \<Rightarrow> Top
wenzelm@60508
   213
        | Value v' \<Rightarrow> Value (sup v v')))"
bulwahn@37915
   214
wenzelm@60508
   215
instance
wenzelm@60679
   216
  by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
bulwahn@37915
   217
bulwahn@37915
   218
end
bulwahn@37915
   219
Andreas@57543
   220
instance top :: (lattice) bounded_lattice_top
wenzelm@60679
   221
  by standard (simp add: top_top_def)
wenzelm@60508
   222
bulwahn@37915
   223
wenzelm@60500
   224
subsection \<open>Values extended by a top and a bottom element\<close>
bulwahn@37918
   225
blanchet@58310
   226
datatype 'a flat_complete_lattice = Value 'a | Bot | Top
bulwahn@37918
   227
bulwahn@37918
   228
instantiation flat_complete_lattice :: (type) order
bulwahn@37918
   229
begin
bulwahn@37918
   230
wenzelm@60508
   231
definition less_eq_flat_complete_lattice
wenzelm@60508
   232
where
wenzelm@60508
   233
  "x \<le> y \<equiv>
wenzelm@60508
   234
    (case x of
wenzelm@60508
   235
      Bot \<Rightarrow> True
wenzelm@60508
   236
    | Value v1 \<Rightarrow>
wenzelm@60508
   237
        (case y of
wenzelm@60508
   238
          Bot \<Rightarrow> False
wenzelm@60508
   239
        | Value v2 \<Rightarrow> v1 = v2
wenzelm@60508
   240
        | Top \<Rightarrow> True)
wenzelm@60508
   241
    | Top \<Rightarrow> y = Top)"
bulwahn@37918
   242
wenzelm@60508
   243
definition less_flat_complete_lattice
wenzelm@60508
   244
where
wenzelm@60508
   245
  "x < y =
wenzelm@60508
   246
    (case x of
wenzelm@60508
   247
      Bot \<Rightarrow> y \<noteq> Bot
wenzelm@60508
   248
    | Value v1 \<Rightarrow> y = Top
wenzelm@60508
   249
    | Top \<Rightarrow> False)"
bulwahn@37918
   250
wenzelm@60508
   251
lemma [simp]: "Bot \<le> y"
wenzelm@60508
   252
  unfolding less_eq_flat_complete_lattice_def by auto
wenzelm@60508
   253
wenzelm@60508
   254
lemma [simp]: "y \<le> Top"
wenzelm@60508
   255
  unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
bulwahn@37918
   256
bulwahn@37918
   257
lemma greater_than_two_values:
wenzelm@60509
   258
  assumes "a \<noteq> b" "Value a \<le> z" "Value b \<le> z"
bulwahn@37918
   259
  shows "z = Top"
wenzelm@60508
   260
  using assms
wenzelm@60508
   261
  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918
   262
bulwahn@37918
   263
lemma lesser_than_two_values:
wenzelm@60509
   264
  assumes "a \<noteq> b" "z \<le> Value a" "z \<le> Value b"
bulwahn@37918
   265
  shows "z = Bot"
wenzelm@60508
   266
  using assms
wenzelm@60508
   267
  by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918
   268
wenzelm@60508
   269
instance
wenzelm@60679
   270
  by standard
wenzelm@60508
   271
    (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
wenzelm@60508
   272
      split: flat_complete_lattice.splits)
bulwahn@37918
   273
bulwahn@37918
   274
end
bulwahn@37918
   275
bulwahn@37918
   276
instantiation flat_complete_lattice :: (type) bot
bulwahn@37918
   277
begin
wenzelm@60508
   278
  definition "bot = Bot"
wenzelm@60508
   279
  instance ..
bulwahn@37918
   280
end
bulwahn@37918
   281
bulwahn@37918
   282
instantiation flat_complete_lattice :: (type) top
bulwahn@37918
   283
begin
wenzelm@60508
   284
  definition "top = Top"
wenzelm@60508
   285
  instance ..
bulwahn@37918
   286
end
bulwahn@37918
   287
bulwahn@37918
   288
instantiation flat_complete_lattice :: (type) lattice
bulwahn@37918
   289
begin
bulwahn@37918
   290
bulwahn@37918
   291
definition inf_flat_complete_lattice
bulwahn@37918
   292
where
wenzelm@60508
   293
  "inf x y =
wenzelm@60508
   294
    (case x of
wenzelm@60508
   295
      Bot \<Rightarrow> Bot
wenzelm@60508
   296
    | Value v1 \<Rightarrow>
wenzelm@60508
   297
        (case y of
wenzelm@60508
   298
          Bot \<Rightarrow> Bot
wenzelm@60508
   299
        | Value v2 \<Rightarrow> if v1 = v2 then x else Bot
wenzelm@60508
   300
        | Top \<Rightarrow> x)
wenzelm@60508
   301
    | Top \<Rightarrow> y)"
bulwahn@37918
   302
bulwahn@37918
   303
definition sup_flat_complete_lattice
bulwahn@37918
   304
where
wenzelm@60508
   305
  "sup x y =
wenzelm@60508
   306
    (case x of
wenzelm@60508
   307
      Bot \<Rightarrow> y
wenzelm@60508
   308
    | Value v1 \<Rightarrow>
wenzelm@60508
   309
        (case y of
wenzelm@60508
   310
          Bot \<Rightarrow> x
wenzelm@60508
   311
        | Value v2 \<Rightarrow> if v1 = v2 then x else Top
wenzelm@60508
   312
        | Top \<Rightarrow> Top)
wenzelm@60508
   313
    | Top \<Rightarrow> Top)"
bulwahn@37918
   314
wenzelm@60508
   315
instance
wenzelm@60679
   316
  by standard
wenzelm@60508
   317
    (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
wenzelm@60508
   318
      less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918
   319
bulwahn@37918
   320
end
bulwahn@37918
   321
bulwahn@37918
   322
instantiation flat_complete_lattice :: (type) complete_lattice
bulwahn@37918
   323
begin
bulwahn@37918
   324
bulwahn@37918
   325
definition Sup_flat_complete_lattice
bulwahn@37918
   326
where
wenzelm@60508
   327
  "Sup A =
wenzelm@60508
   328
    (if A = {} \<or> A = {Bot} then Bot
wenzelm@60508
   329
     else if \<exists>v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v})
wenzelm@60508
   330
     else Top)"
bulwahn@37918
   331
bulwahn@37918
   332
definition Inf_flat_complete_lattice
bulwahn@37918
   333
where
wenzelm@60508
   334
  "Inf A =
wenzelm@60508
   335
    (if A = {} \<or> A = {Top} then Top
wenzelm@60508
   336
     else if \<exists>v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v})
wenzelm@60508
   337
     else Bot)"
wenzelm@60508
   338
bulwahn@37918
   339
instance
bulwahn@37918
   340
proof
wenzelm@60508
   341
  fix x :: "'a flat_complete_lattice"
wenzelm@60508
   342
  fix A
wenzelm@60508
   343
  assume "x \<in> A"
bulwahn@37918
   344
  {
bulwahn@37918
   345
    fix v
bulwahn@37918
   346
    assume "A - {Top} = {Value v}"
wenzelm@60508
   347
    then have "(THE v. A - {Top} = {Value v}) = v"
bulwahn@37918
   348
      by (auto intro!: the1_equality)
bulwahn@37918
   349
    moreover
wenzelm@60508
   350
    from \<open>x \<in> A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
bulwahn@37918
   351
      by auto
wenzelm@60508
   352
    ultimately have "Value (THE v. A - {Top} = {Value v}) \<le> x"
bulwahn@37918
   353
      by auto
bulwahn@37918
   354
  }
wenzelm@60508
   355
  with \<open>x \<in> A\<close> show "Inf A \<le> x"
bulwahn@37918
   356
    unfolding Inf_flat_complete_lattice_def
nipkow@44890
   357
    by fastforce
bulwahn@37918
   358
next
wenzelm@60508
   359
  fix z :: "'a flat_complete_lattice"
wenzelm@60508
   360
  fix A
wenzelm@60509
   361
  show "z \<le> Inf A" if z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
wenzelm@60509
   362
  proof -
wenzelm@60509
   363
    consider "A = {} \<or> A = {Top}"
wenzelm@60509
   364
      | "A \<noteq> {}" "A \<noteq> {Top}" "\<exists>v. A - {Top} = {Value v}"
wenzelm@60509
   365
      | "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v. A - {Top} = {Value v})"
wenzelm@60509
   366
      by blast
wenzelm@60509
   367
    then show ?thesis
wenzelm@60509
   368
    proof cases
wenzelm@60509
   369
      case 1
wenzelm@60509
   370
      then have "Inf A = Top"
wenzelm@60509
   371
        unfolding Inf_flat_complete_lattice_def by auto
wenzelm@60509
   372
      then show ?thesis by simp
wenzelm@60509
   373
    next
wenzelm@60509
   374
      case 2
wenzelm@60509
   375
      then obtain v where v1: "A - {Top} = {Value v}"
bulwahn@37918
   376
        by auto
wenzelm@60509
   377
      then have v2: "(THE v. A - {Top} = {Value v}) = v"
wenzelm@60509
   378
        by (auto intro!: the1_equality)
wenzelm@60509
   379
      from 2 v2 have Inf: "Inf A = Value v"
wenzelm@60509
   380
        unfolding Inf_flat_complete_lattice_def by simp
wenzelm@60509
   381
      from v1 have "Value v \<in> A" by blast
wenzelm@60509
   382
      then have "z \<le> Value v" by (rule z)
wenzelm@60509
   383
      with Inf show ?thesis by simp
bulwahn@37918
   384
    next
wenzelm@60509
   385
      case 3
wenzelm@60509
   386
      then have Inf: "Inf A = Bot"
wenzelm@60509
   387
        unfolding Inf_flat_complete_lattice_def by auto
wenzelm@60509
   388
      have "z \<le> Bot"
wenzelm@60509
   389
      proof (cases "A - {Top} = {Bot}")
wenzelm@60509
   390
        case True
wenzelm@60509
   391
        then have "Bot \<in> A" by blast
wenzelm@60509
   392
        then show ?thesis by (rule z)
wenzelm@60509
   393
      next
wenzelm@60509
   394
        case False
wenzelm@60509
   395
        from 3 obtain a1 where a1: "a1 \<in> A - {Top}"
wenzelm@60509
   396
          by auto
wenzelm@60509
   397
        from 3 False a1 obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
wenzelm@60509
   398
          by (cases a1) auto
wenzelm@60509
   399
        with a1 z[of "a1"] z[of "a2"] show ?thesis
wenzelm@60509
   400
          apply (cases a1)
wenzelm@60509
   401
          apply auto
wenzelm@60509
   402
          apply (cases a2)
wenzelm@60509
   403
          apply auto
wenzelm@60509
   404
          apply (auto dest!: lesser_than_two_values)
wenzelm@60509
   405
          done
wenzelm@60509
   406
      qed
wenzelm@60509
   407
      with Inf show ?thesis by simp
bulwahn@37918
   408
    qed
wenzelm@60509
   409
  qed
bulwahn@37918
   410
next
wenzelm@60508
   411
  fix x :: "'a flat_complete_lattice"
wenzelm@60508
   412
  fix A
wenzelm@60508
   413
  assume "x \<in> A"
bulwahn@37918
   414
  {
bulwahn@37918
   415
    fix v
bulwahn@37918
   416
    assume "A - {Bot} = {Value v}"
wenzelm@60508
   417
    then have "(THE v. A - {Bot} = {Value v}) = v"
bulwahn@37918
   418
      by (auto intro!: the1_equality)
bulwahn@37918
   419
    moreover
wenzelm@60508
   420
    from \<open>x \<in> A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
bulwahn@37918
   421
      by auto
wenzelm@60508
   422
    ultimately have "x \<le> Value (THE v. A - {Bot} = {Value v})"
bulwahn@37918
   423
      by auto
bulwahn@37918
   424
  }
wenzelm@60508
   425
  with \<open>x \<in> A\<close> show "x \<le> Sup A"
bulwahn@37918
   426
    unfolding Sup_flat_complete_lattice_def
nipkow@44890
   427
    by fastforce
bulwahn@37918
   428
next
wenzelm@60508
   429
  fix z :: "'a flat_complete_lattice"
wenzelm@60508
   430
  fix A
wenzelm@60509
   431
  show "Sup A \<le> z" if z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
wenzelm@60509
   432
  proof -
wenzelm@60509
   433
    consider "A = {} \<or> A = {Bot}"
wenzelm@60509
   434
      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<exists>v. A - {Bot} = {Value v}"
wenzelm@60509
   435
      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v. A - {Bot} = {Value v})"
wenzelm@60509
   436
      by blast
wenzelm@60509
   437
    then show ?thesis
wenzelm@60509
   438
    proof cases
wenzelm@60509
   439
      case 1
wenzelm@60509
   440
      then have "Sup A = Bot"
wenzelm@60509
   441
        unfolding Sup_flat_complete_lattice_def by auto
wenzelm@60509
   442
      then show ?thesis by simp
wenzelm@60509
   443
    next
wenzelm@60509
   444
      case 2
wenzelm@60509
   445
      then obtain v where v1: "A - {Bot} = {Value v}"
bulwahn@37918
   446
        by auto
wenzelm@60509
   447
      then have v2: "(THE v. A - {Bot} = {Value v}) = v"
wenzelm@60509
   448
        by (auto intro!: the1_equality)
wenzelm@60509
   449
      from 2 v2 have Sup: "Sup A = Value v"
wenzelm@60509
   450
        unfolding Sup_flat_complete_lattice_def by simp
wenzelm@60509
   451
      from v1 have "Value v \<in> A" by blast
wenzelm@60509
   452
      then have "Value v \<le> z" by (rule z)
wenzelm@60509
   453
      with Sup show ?thesis by simp
bulwahn@37918
   454
    next
wenzelm@60509
   455
      case 3
wenzelm@60509
   456
      then have Sup: "Sup A = Top"
wenzelm@60509
   457
        unfolding Sup_flat_complete_lattice_def by auto
wenzelm@60509
   458
      have "Top \<le> z"
wenzelm@60509
   459
      proof (cases "A - {Bot} = {Top}")
wenzelm@60509
   460
        case True
wenzelm@60509
   461
        then have "Top \<in> A" by blast
wenzelm@60509
   462
        then show ?thesis by (rule z)
wenzelm@60509
   463
      next
wenzelm@60509
   464
        case False
wenzelm@60509
   465
        from 3 obtain a1 where a1: "a1 \<in> A - {Bot}"
wenzelm@60509
   466
          by auto
wenzelm@60509
   467
        from 3 False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
wenzelm@60509
   468
          by (cases a1) auto
wenzelm@60509
   469
        with a1 z[of "a1"] z[of "a2"] show ?thesis
wenzelm@60509
   470
          apply (cases a1)
wenzelm@60509
   471
          apply auto
wenzelm@60509
   472
          apply (cases a2)
wenzelm@60509
   473
          apply (auto dest!: greater_than_two_values)
wenzelm@60509
   474
          done
wenzelm@60509
   475
      qed
wenzelm@60509
   476
      with Sup show ?thesis by simp
bulwahn@37918
   477
    qed
wenzelm@60509
   478
  qed
Andreas@57543
   479
next
Andreas@57543
   480
  show "Inf {} = (top :: 'a flat_complete_lattice)"
wenzelm@60508
   481
    by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
Andreas@57543
   482
  show "Sup {} = (bot :: 'a flat_complete_lattice)"
wenzelm@60508
   483
    by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
bulwahn@37918
   484
qed
bulwahn@37918
   485
bulwahn@37918
   486
end
bulwahn@37918
   487
bulwahn@37915
   488
end