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