src/HOL/Library/Lattice_Constructions.thy
author Andreas Lochbihler
Tue Aug 19 15:19:16 2014 +0200 (2014-08-19)
changeset 57998 8b7508f848ef
parent 57997 src/HOL/Library/Quickcheck_Types.thy@4f93afabcdd2
child 58249 180f1b3508ed
permissions -rw-r--r--
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
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
bulwahn@37915
    10
subsection {* Values extended by a bottom element *}
bulwahn@37915
    11
bulwahn@37915
    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
bulwahn@37915
    53
instance proof
bulwahn@37915
    54
qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
bulwahn@37915
    55
bulwahn@37915
    56
end 
bulwahn@37915
    57
bulwahn@37915
    58
instance bot :: (order) order proof
bulwahn@37915
    59
qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915
    60
bulwahn@37915
    61
instance bot :: (linorder) linorder proof
bulwahn@37915
    62
qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
bulwahn@37915
    63
haftmann@43815
    64
instantiation bot :: (order) bot
bulwahn@37915
    65
begin
bulwahn@37915
    66
bulwahn@37915
    67
definition "bot = Bot"
bulwahn@37915
    68
Andreas@57543
    69
instance ..
bulwahn@37915
    70
bulwahn@37915
    71
end
bulwahn@37915
    72
bulwahn@37915
    73
instantiation bot :: (top) top
bulwahn@37915
    74
begin
bulwahn@37915
    75
bulwahn@37915
    76
definition "top = Value top"
bulwahn@37915
    77
Andreas@57543
    78
instance ..
bulwahn@37915
    79
bulwahn@37915
    80
end
bulwahn@37915
    81
bulwahn@37915
    82
instantiation bot :: (semilattice_inf) semilattice_inf
bulwahn@37915
    83
begin
bulwahn@37915
    84
bulwahn@37915
    85
definition inf_bot
bulwahn@37915
    86
where
bulwahn@37915
    87
  "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
bulwahn@37915
    88
bulwahn@37915
    89
instance proof
bulwahn@37915
    90
qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915
    91
bulwahn@37915
    92
end
bulwahn@37915
    93
bulwahn@37915
    94
instantiation bot :: (semilattice_sup) semilattice_sup
bulwahn@37915
    95
begin
bulwahn@37915
    96
bulwahn@37915
    97
definition sup_bot
bulwahn@37915
    98
where
bulwahn@37915
    99
  "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
bulwahn@37915
   100
bulwahn@37915
   101
instance proof
bulwahn@37915
   102
qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
bulwahn@37915
   103
bulwahn@37915
   104
end
bulwahn@37915
   105
Andreas@57543
   106
instance bot :: (lattice) bounded_lattice_bot
Andreas@57543
   107
by(intro_classes)(simp add: bot_bot_def)
bulwahn@37915
   108
bulwahn@37915
   109
section {* Values extended by a top element *}
bulwahn@37915
   110
bulwahn@37915
   111
datatype 'a top = Value 'a | Top
bulwahn@37915
   112
bulwahn@37915
   113
instantiation top :: (preorder) preorder
bulwahn@37915
   114
begin
bulwahn@37915
   115
bulwahn@37915
   116
definition less_eq_top where
bulwahn@37915
   117
  "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
   118
bulwahn@37915
   119
definition less_top where
bulwahn@37915
   120
  "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
   121
bulwahn@37915
   122
lemma less_eq_top_Top [simp]: "x <= Top"
bulwahn@37915
   123
  by (simp add: less_eq_top_def)
bulwahn@37915
   124
bulwahn@37915
   125
lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
bulwahn@37915
   126
  by simp
bulwahn@37915
   127
bulwahn@37915
   128
lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
bulwahn@37915
   129
  by (cases x) (simp_all add: less_eq_top_def)
bulwahn@37915
   130
bulwahn@37915
   131
lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
bulwahn@37915
   132
  by (simp add: less_eq_top_def)
bulwahn@37915
   133
bulwahn@37915
   134
lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
bulwahn@37915
   135
  by (simp add: less_eq_top_def)
bulwahn@37915
   136
bulwahn@37915
   137
lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
bulwahn@37915
   138
  by (simp add: less_top_def)
bulwahn@37915
   139
bulwahn@37915
   140
lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
bulwahn@37915
   141
  by (cases x) (simp_all add: less_top_def)
bulwahn@37915
   142
bulwahn@37915
   143
lemma less_top_Value_Top [simp]: "Value x < Top"
bulwahn@37915
   144
  by (simp add: less_top_def)
bulwahn@37915
   145
bulwahn@37915
   146
lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
bulwahn@37915
   147
  by simp
bulwahn@37915
   148
bulwahn@37915
   149
lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
bulwahn@37915
   150
  by (simp add: less_top_def)
bulwahn@37915
   151
bulwahn@37915
   152
instance proof
bulwahn@37915
   153
qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
bulwahn@37915
   154
bulwahn@37915
   155
end 
bulwahn@37915
   156
bulwahn@37915
   157
instance top :: (order) order proof
bulwahn@37915
   158
qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915
   159
bulwahn@37915
   160
instance top :: (linorder) linorder proof
bulwahn@37915
   161
qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
bulwahn@37915
   162
haftmann@43815
   163
instantiation top :: (order) top
bulwahn@37915
   164
begin
bulwahn@37915
   165
bulwahn@37915
   166
definition "top = Top"
bulwahn@37915
   167
Andreas@57543
   168
instance ..
bulwahn@37915
   169
bulwahn@37915
   170
end
bulwahn@37915
   171
bulwahn@37915
   172
instantiation top :: (bot) bot
bulwahn@37915
   173
begin
bulwahn@37915
   174
bulwahn@37915
   175
definition "bot = Value bot"
bulwahn@37915
   176
Andreas@57543
   177
instance ..
bulwahn@37915
   178
bulwahn@37915
   179
end
bulwahn@37915
   180
bulwahn@37915
   181
instantiation top :: (semilattice_inf) semilattice_inf
bulwahn@37915
   182
begin
bulwahn@37915
   183
bulwahn@37915
   184
definition inf_top
bulwahn@37915
   185
where
bulwahn@37915
   186
  "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
bulwahn@37915
   187
bulwahn@37915
   188
instance proof
bulwahn@37915
   189
qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
bulwahn@37915
   190
bulwahn@37915
   191
end
bulwahn@37915
   192
bulwahn@37915
   193
instantiation top :: (semilattice_sup) semilattice_sup
bulwahn@37915
   194
begin
bulwahn@37915
   195
bulwahn@37915
   196
definition sup_top
bulwahn@37915
   197
where
bulwahn@37915
   198
  "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
bulwahn@37915
   199
bulwahn@37915
   200
instance proof
bulwahn@37915
   201
qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
bulwahn@37915
   202
bulwahn@37915
   203
end
bulwahn@37915
   204
Andreas@57543
   205
instance top :: (lattice) bounded_lattice_top
Andreas@57543
   206
by(intro_classes)(simp add: top_top_def)
bulwahn@37915
   207
Andreas@57998
   208
subsection {* Values extended by a top and a bottom element *}
bulwahn@37918
   209
bulwahn@37918
   210
datatype 'a flat_complete_lattice = Value 'a | Bot | Top
bulwahn@37918
   211
bulwahn@37918
   212
instantiation flat_complete_lattice :: (type) order
bulwahn@37918
   213
begin
bulwahn@37918
   214
bulwahn@37918
   215
definition less_eq_flat_complete_lattice where
bulwahn@37918
   216
  "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
bulwahn@37918
   217
bulwahn@37918
   218
definition less_flat_complete_lattice where
bulwahn@37918
   219
  "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
bulwahn@37918
   220
bulwahn@37918
   221
lemma [simp]: "Bot <= y"
bulwahn@37918
   222
unfolding less_eq_flat_complete_lattice_def by auto
bulwahn@37918
   223
bulwahn@37918
   224
lemma [simp]: "y <= Top"
bulwahn@37918
   225
unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
bulwahn@37918
   226
bulwahn@37918
   227
lemma greater_than_two_values:
bulwahn@37918
   228
  assumes "a ~= aa" "Value a <= z" "Value aa <= z"
bulwahn@37918
   229
  shows "z = Top"
bulwahn@37918
   230
using assms
bulwahn@37918
   231
by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918
   232
bulwahn@37918
   233
lemma lesser_than_two_values:
bulwahn@37918
   234
  assumes "a ~= aa" "z <= Value a" "z <= Value aa"
bulwahn@37918
   235
  shows "z = Bot"
bulwahn@37918
   236
using assms
bulwahn@37918
   237
by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
bulwahn@37918
   238
bulwahn@37918
   239
instance proof
bulwahn@37918
   240
qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918
   241
bulwahn@37918
   242
end
bulwahn@37918
   243
bulwahn@37918
   244
instantiation flat_complete_lattice :: (type) bot
bulwahn@37918
   245
begin
bulwahn@37918
   246
bulwahn@37918
   247
definition "bot = Bot"
bulwahn@37918
   248
Andreas@57543
   249
instance ..
bulwahn@37918
   250
bulwahn@37918
   251
end
bulwahn@37918
   252
bulwahn@37918
   253
instantiation flat_complete_lattice :: (type) top
bulwahn@37918
   254
begin
bulwahn@37918
   255
bulwahn@37918
   256
definition "top = Top"
bulwahn@37918
   257
Andreas@57543
   258
instance ..
bulwahn@37918
   259
bulwahn@37918
   260
end
bulwahn@37918
   261
bulwahn@37918
   262
instantiation flat_complete_lattice :: (type) lattice
bulwahn@37918
   263
begin
bulwahn@37918
   264
bulwahn@37918
   265
definition inf_flat_complete_lattice
bulwahn@37918
   266
where
bulwahn@37918
   267
  "inf x y = (case x of Bot => Bot | Value v1 => (case y of Bot => Bot | Value v2 => if (v1 = v2) then x else Bot | Top => x) | Top => y)"
bulwahn@37918
   268
bulwahn@37918
   269
definition sup_flat_complete_lattice
bulwahn@37918
   270
where
bulwahn@37918
   271
  "sup x y = (case x of Bot => y | Value v1 => (case y of Bot => x | Value v2 => if v1 = v2 then x else Top | Top => Top) | Top => Top)"
bulwahn@37918
   272
bulwahn@37918
   273
instance proof
bulwahn@37918
   274
qed (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
bulwahn@37918
   275
bulwahn@37918
   276
end
bulwahn@37918
   277
bulwahn@37918
   278
instantiation flat_complete_lattice :: (type) complete_lattice
bulwahn@37918
   279
begin
bulwahn@37918
   280
bulwahn@37918
   281
definition Sup_flat_complete_lattice
bulwahn@37918
   282
where
bulwahn@37918
   283
  "Sup A = (if (A = {} \<or> A = {Bot}) then Bot else (if (\<exists> v. A - {Bot} = {Value v}) then Value (THE v. A - {Bot} = {Value v}) else Top))"
bulwahn@37918
   284
bulwahn@37918
   285
definition Inf_flat_complete_lattice
bulwahn@37918
   286
where
bulwahn@37918
   287
  "Inf A = (if (A = {} \<or> A = {Top}) then Top else (if (\<exists> v. A - {Top} = {Value v}) then Value (THE v. A - {Top} = {Value v}) else Bot))"
bulwahn@37918
   288
 
bulwahn@37918
   289
instance
bulwahn@37918
   290
proof
bulwahn@37918
   291
  fix x A
bulwahn@37918
   292
  assume "(x :: 'a flat_complete_lattice) : A"
bulwahn@37918
   293
  {
bulwahn@37918
   294
    fix v
bulwahn@37918
   295
    assume "A - {Top} = {Value v}"
bulwahn@37918
   296
    from this have "(THE v. A - {Top} = {Value v}) = v"
bulwahn@37918
   297
      by (auto intro!: the1_equality)
bulwahn@37918
   298
    moreover
bulwahn@37918
   299
    from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
bulwahn@37918
   300
      by auto
bulwahn@37918
   301
    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
bulwahn@37918
   302
      by auto
bulwahn@37918
   303
  }
bulwahn@37918
   304
  from `x : A` this show "Inf A <= x"
bulwahn@37918
   305
    unfolding Inf_flat_complete_lattice_def
nipkow@44890
   306
    by fastforce
bulwahn@37918
   307
next
bulwahn@37918
   308
  fix z A
bulwahn@37918
   309
  assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
bulwahn@37918
   310
  {
bulwahn@37918
   311
    fix v
bulwahn@37918
   312
    assume "A - {Top} = {Value v}"
bulwahn@37918
   313
    moreover
bulwahn@37918
   314
    from this have "(THE v. A - {Top} = {Value v}) = v"
bulwahn@37918
   315
      by (auto intro!: the1_equality)
bulwahn@37918
   316
    moreover
bulwahn@37918
   317
    note z
bulwahn@37918
   318
    moreover
bulwahn@37918
   319
    ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
bulwahn@37918
   320
      by auto
bulwahn@37918
   321
  } moreover
bulwahn@37918
   322
  {
bulwahn@37918
   323
    assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
bulwahn@37918
   324
    have "z <= Bot"
bulwahn@37918
   325
    proof (cases "A - {Top} = {Bot}")
bulwahn@37918
   326
      case True
bulwahn@37918
   327
      from this z show ?thesis
bulwahn@37918
   328
        by auto
bulwahn@37918
   329
    next
bulwahn@37918
   330
      case False
bulwahn@37918
   331
      from not_one_value
bulwahn@37918
   332
      obtain a1 where a1: "a1 : A - {Top}" by auto
bulwahn@37918
   333
      from not_one_value False a1
bulwahn@37918
   334
      obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
bulwahn@37918
   335
        by (cases a1) auto
bulwahn@37918
   336
      from this a1 z[of "a1"] z[of "a2"] show ?thesis
bulwahn@37918
   337
        apply (cases a1)
bulwahn@37918
   338
        apply auto
bulwahn@37918
   339
        apply (cases a2)
bulwahn@37918
   340
        apply auto
bulwahn@37918
   341
        apply (auto dest!: lesser_than_two_values)
bulwahn@37918
   342
        done
bulwahn@37918
   343
    qed
bulwahn@37918
   344
  } moreover
bulwahn@37918
   345
  note z moreover
bulwahn@37918
   346
  ultimately show "z <= Inf A"
bulwahn@37918
   347
    unfolding Inf_flat_complete_lattice_def
bulwahn@37918
   348
    by auto
bulwahn@37918
   349
next
bulwahn@37918
   350
  fix x A
bulwahn@37918
   351
  assume "(x :: 'a flat_complete_lattice) : A"
bulwahn@37918
   352
  {
bulwahn@37918
   353
    fix v
bulwahn@37918
   354
    assume "A - {Bot} = {Value v}"
bulwahn@37918
   355
    from this have "(THE v. A - {Bot} = {Value v}) = v"
bulwahn@37918
   356
      by (auto intro!: the1_equality)
bulwahn@37918
   357
    moreover
bulwahn@37918
   358
    from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
bulwahn@37918
   359
      by auto
bulwahn@37918
   360
    ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
bulwahn@37918
   361
      by auto
bulwahn@37918
   362
  }
bulwahn@37918
   363
  from `x : A` this show "x <= Sup A"
bulwahn@37918
   364
    unfolding Sup_flat_complete_lattice_def
nipkow@44890
   365
    by fastforce
bulwahn@37918
   366
next
bulwahn@37918
   367
  fix z A
bulwahn@37918
   368
  assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
bulwahn@37918
   369
  {
bulwahn@37918
   370
    fix v
bulwahn@37918
   371
    assume "A - {Bot} = {Value v}"
bulwahn@37918
   372
    moreover
bulwahn@37918
   373
    from this have "(THE v. A - {Bot} = {Value v}) = v"
bulwahn@37918
   374
      by (auto intro!: the1_equality)
bulwahn@37918
   375
    moreover
bulwahn@37918
   376
    note z
bulwahn@37918
   377
    moreover
bulwahn@37918
   378
    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
bulwahn@37918
   379
      by auto
bulwahn@37918
   380
  } moreover
bulwahn@37918
   381
  {
bulwahn@37918
   382
    assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
bulwahn@37918
   383
    have "Top <= z"
bulwahn@37918
   384
    proof (cases "A - {Bot} = {Top}")
bulwahn@37918
   385
      case True
bulwahn@37918
   386
      from this z show ?thesis
bulwahn@37918
   387
        by auto
bulwahn@37918
   388
    next
bulwahn@37918
   389
      case False
bulwahn@37918
   390
      from not_one_value
bulwahn@37918
   391
      obtain a1 where a1: "a1 : A - {Bot}" by auto
bulwahn@37918
   392
      from not_one_value False a1
bulwahn@37918
   393
      obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
bulwahn@37918
   394
        by (cases a1) auto
bulwahn@37918
   395
      from this a1 z[of "a1"] z[of "a2"] show ?thesis
bulwahn@37918
   396
        apply (cases a1)
bulwahn@37918
   397
        apply auto
bulwahn@37918
   398
        apply (cases a2)
bulwahn@37918
   399
        apply (auto dest!: greater_than_two_values)
bulwahn@37918
   400
        done
bulwahn@37918
   401
    qed
bulwahn@37918
   402
  } moreover
bulwahn@37918
   403
  note z moreover
bulwahn@37918
   404
  ultimately show "Sup A <= z"
bulwahn@37918
   405
    unfolding Sup_flat_complete_lattice_def
bulwahn@37918
   406
    by auto
Andreas@57543
   407
next
Andreas@57543
   408
  show "Inf {} = (top :: 'a flat_complete_lattice)"
Andreas@57543
   409
    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
Andreas@57543
   410
next
Andreas@57543
   411
  show "Sup {} = (bot :: 'a flat_complete_lattice)"
Andreas@57543
   412
    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
bulwahn@37918
   413
qed
bulwahn@37918
   414
bulwahn@37918
   415
end
bulwahn@37918
   416
bulwahn@37915
   417
end