src/HOL/Enum.thy
author haftmann
Sat Oct 20 10:00:21 2012 +0200 (2012-10-20)
changeset 49950 cd882d53ba6b
parent 49949 be3dd2e602e8
child 49972 f11f8905d9fd
permissions -rw-r--r--
tailored enum specification towards simple instantiation;
tuned enum instantiations
haftmann@31596
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@26348
     2
haftmann@26348
     3
header {* Finite types as explicit enumerations *}
haftmann@26348
     4
haftmann@26348
     5
theory Enum
bulwahn@40650
     6
imports Map String
haftmann@26348
     7
begin
haftmann@26348
     8
haftmann@26348
     9
subsection {* Class @{text enum} *}
haftmann@26348
    10
haftmann@29797
    11
class enum =
haftmann@26348
    12
  fixes enum :: "'a list"
bulwahn@41078
    13
  fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
haftmann@49950
    14
  fixes enum_ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
haftmann@33635
    15
  assumes UNIV_enum: "UNIV = set enum"
haftmann@26444
    16
    and enum_distinct: "distinct enum"
haftmann@49950
    17
  assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
haftmann@49950
    18
  assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P" 
haftmann@49950
    19
   -- {* tailored towards simple instantiation *}
haftmann@26348
    20
begin
haftmann@26348
    21
haftmann@29797
    22
subclass finite proof
haftmann@29797
    23
qed (simp add: UNIV_enum)
haftmann@26444
    24
haftmann@49950
    25
lemma enum_UNIV:
haftmann@49950
    26
  "set enum = UNIV"
haftmann@49950
    27
  by (simp only: UNIV_enum)
haftmann@26444
    28
bulwahn@40683
    29
lemma in_enum: "x \<in> set enum"
haftmann@49950
    30
  by (simp add: enum_UNIV)
haftmann@26348
    31
haftmann@26348
    32
lemma enum_eq_I:
haftmann@26348
    33
  assumes "\<And>x. x \<in> set xs"
haftmann@26348
    34
  shows "set enum = set xs"
haftmann@26348
    35
proof -
haftmann@26348
    36
  from assms UNIV_eq_I have "UNIV = set xs" by auto
bulwahn@41078
    37
  with enum_UNIV show ?thesis by simp
haftmann@26348
    38
qed
haftmann@26348
    39
haftmann@49950
    40
lemma enum_all [simp]:
haftmann@49950
    41
  "enum_all = HOL.All"
haftmann@49950
    42
  by (simp add: fun_eq_iff enum_all_UNIV)
haftmann@49950
    43
haftmann@49950
    44
lemma enum_ex [simp]:
haftmann@49950
    45
  "enum_ex = HOL.Ex" 
haftmann@49950
    46
  by (simp add: fun_eq_iff enum_ex_UNIV)
haftmann@49950
    47
haftmann@26348
    48
end
haftmann@26348
    49
haftmann@26348
    50
haftmann@49949
    51
subsection {* Implementations using @{class enum} *}
haftmann@49949
    52
haftmann@49949
    53
subsubsection {* Unbounded operations and quantifiers *}
haftmann@49949
    54
haftmann@49949
    55
lemma Collect_code [code]:
haftmann@49949
    56
  "Collect P = set (filter P enum)"
haftmann@49950
    57
  by (simp add: enum_UNIV)
haftmann@49949
    58
haftmann@49949
    59
definition card_UNIV :: "'a itself \<Rightarrow> nat"
haftmann@49949
    60
where
haftmann@49949
    61
  [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
haftmann@49949
    62
haftmann@49949
    63
lemma [code]:
haftmann@49949
    64
  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
haftmann@49949
    65
  by (simp only: card_UNIV_def enum_UNIV)
haftmann@49949
    66
haftmann@49949
    67
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
haftmann@49950
    68
  by simp
haftmann@49949
    69
haftmann@49949
    70
lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
haftmann@49950
    71
  by simp
haftmann@49949
    72
haftmann@49949
    73
lemma exists1_code [code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
haftmann@49950
    74
  by (auto simp add: list_ex1_iff enum_UNIV)
haftmann@49949
    75
haftmann@49949
    76
haftmann@49949
    77
subsubsection {* An executable choice operator *}
haftmann@49949
    78
haftmann@49949
    79
definition
haftmann@49949
    80
  [code del]: "enum_the = The"
haftmann@49949
    81
haftmann@49949
    82
lemma [code]:
haftmann@49949
    83
  "The P = (case filter P enum of [x] => x | _ => enum_the P)"
haftmann@49949
    84
proof -
haftmann@49949
    85
  {
haftmann@49949
    86
    fix a
haftmann@49949
    87
    assume filter_enum: "filter P enum = [a]"
haftmann@49949
    88
    have "The P = a"
haftmann@49949
    89
    proof (rule the_equality)
haftmann@49949
    90
      fix x
haftmann@49949
    91
      assume "P x"
haftmann@49949
    92
      show "x = a"
haftmann@49949
    93
      proof (rule ccontr)
haftmann@49949
    94
        assume "x \<noteq> a"
haftmann@49949
    95
        from filter_enum obtain us vs
haftmann@49949
    96
          where enum_eq: "enum = us @ [a] @ vs"
haftmann@49949
    97
          and "\<forall> x \<in> set us. \<not> P x"
haftmann@49949
    98
          and "\<forall> x \<in> set vs. \<not> P x"
haftmann@49949
    99
          and "P a"
haftmann@49949
   100
          by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
haftmann@49949
   101
        with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
haftmann@49949
   102
      qed
haftmann@49949
   103
    next
haftmann@49949
   104
      from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
haftmann@49949
   105
    qed
haftmann@49949
   106
  }
haftmann@49949
   107
  from this show ?thesis
haftmann@49949
   108
    unfolding enum_the_def by (auto split: list.split)
haftmann@49949
   109
qed
haftmann@49949
   110
haftmann@49949
   111
code_abort enum_the
haftmann@49949
   112
code_const enum_the (Eval "(fn p => raise Match)")
haftmann@49949
   113
haftmann@49949
   114
haftmann@49949
   115
subsubsection {* Equality and order on functions *}
haftmann@26348
   116
haftmann@38857
   117
instantiation "fun" :: (enum, equal) equal
haftmann@26513
   118
begin
haftmann@26348
   119
haftmann@26513
   120
definition
haftmann@38857
   121
  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
haftmann@26513
   122
haftmann@31464
   123
instance proof
haftmann@49950
   124
qed (simp_all add: equal_fun_def fun_eq_iff enum_UNIV)
haftmann@26513
   125
haftmann@26513
   126
end
haftmann@26348
   127
bulwahn@40898
   128
lemma [code]:
bulwahn@41078
   129
  "HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
haftmann@49950
   130
  by (auto simp add: equal fun_eq_iff)
bulwahn@40898
   131
haftmann@38857
   132
lemma [code nbe]:
haftmann@38857
   133
  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
haftmann@38857
   134
  by (fact equal_refl)
haftmann@38857
   135
haftmann@28562
   136
lemma order_fun [code]:
haftmann@26348
   137
  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
bulwahn@41078
   138
  shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
bulwahn@41078
   139
    and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
haftmann@49950
   140
  by (simp_all add: fun_eq_iff le_fun_def order_less_le)
haftmann@26968
   141
haftmann@26968
   142
haftmann@49949
   143
subsubsection {* Operations on relations *}
haftmann@49949
   144
haftmann@49949
   145
lemma [code]:
haftmann@49949
   146
  "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
haftmann@49949
   147
  by (auto intro: imageI in_enum)
haftmann@26968
   148
haftmann@49949
   149
lemma tranclp_unfold [code, no_atp]:
haftmann@49949
   150
  "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
haftmann@49949
   151
  by (simp add: trancl_def)
haftmann@49949
   152
haftmann@49949
   153
lemma rtranclp_rtrancl_eq [code, no_atp]:
haftmann@49949
   154
  "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
haftmann@49949
   155
  by (simp add: rtrancl_def)
haftmann@26968
   156
haftmann@49949
   157
lemma max_ext_eq [code]:
haftmann@49949
   158
  "max_ext R = {(X, Y). finite X \<and> finite Y \<and> Y \<noteq> {} \<and> (\<forall>x. x \<in> X \<longrightarrow> (\<exists>xa \<in> Y. (x, xa) \<in> R))}"
haftmann@49949
   159
  by (auto simp add: max_ext.simps)
haftmann@49949
   160
haftmann@49949
   161
lemma max_extp_eq [code]:
haftmann@49949
   162
  "max_extp r x y \<longleftrightarrow> (x, y) \<in> max_ext {(x, y). r x y}"
haftmann@49949
   163
  by (simp add: max_ext_def)
haftmann@26348
   164
haftmann@49949
   165
lemma mlex_eq [code]:
haftmann@49949
   166
  "f <*mlex*> R = {(x, y). f x < f y \<or> (f x \<le> f y \<and> (x, y) \<in> R)}"
haftmann@49949
   167
  by (auto simp add: mlex_prod_def)
haftmann@49949
   168
haftmann@49949
   169
lemma [code]:
haftmann@49949
   170
  fixes xs :: "('a::finite \<times> 'a) list"
haftmann@49949
   171
  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
haftmann@49949
   172
  by (simp add: card_UNIV_def acc_bacc_eq)
haftmann@49949
   173
haftmann@49949
   174
lemma [code]:
haftmann@49949
   175
  "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
haftmann@49949
   176
  by (simp add: acc_def)
bulwahn@40652
   177
haftmann@26348
   178
haftmann@49949
   179
subsection {* Default instances for @{class enum} *}
haftmann@26348
   180
haftmann@26444
   181
lemma map_of_zip_enum_is_Some:
haftmann@26444
   182
  assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
haftmann@26444
   183
  shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
haftmann@26444
   184
proof -
haftmann@26444
   185
  from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
haftmann@26444
   186
    (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
haftmann@26444
   187
    by (auto intro!: map_of_zip_is_Some)
bulwahn@41078
   188
  then show ?thesis using enum_UNIV by auto
haftmann@26444
   189
qed
haftmann@26444
   190
haftmann@26444
   191
lemma map_of_zip_enum_inject:
haftmann@26444
   192
  fixes xs ys :: "'b\<Colon>enum list"
haftmann@26444
   193
  assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
haftmann@26444
   194
      "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
haftmann@26444
   195
    and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
haftmann@26444
   196
  shows "xs = ys"
haftmann@26444
   197
proof -
haftmann@26444
   198
  have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
haftmann@26444
   199
  proof
haftmann@26444
   200
    fix x :: 'a
haftmann@26444
   201
    from length map_of_zip_enum_is_Some obtain y1 y2
haftmann@26444
   202
      where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
haftmann@26444
   203
        and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
wenzelm@47230
   204
    moreover from map_of
wenzelm@47230
   205
      have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
haftmann@26444
   206
      by (auto dest: fun_cong)
haftmann@26444
   207
    ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
haftmann@26444
   208
      by simp
haftmann@26444
   209
  qed
haftmann@26444
   210
  with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
haftmann@26444
   211
qed
haftmann@26444
   212
haftmann@49950
   213
definition all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
bulwahn@41078
   214
where
haftmann@49950
   215
  "all_n_lists P n \<longleftrightarrow> (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
bulwahn@41078
   216
bulwahn@41078
   217
lemma [code]:
haftmann@49950
   218
  "all_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
haftmann@49950
   219
  unfolding all_n_lists_def enum_all
haftmann@49950
   220
  by (cases n) (auto simp add: enum_UNIV)
bulwahn@41078
   221
haftmann@49950
   222
definition ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
bulwahn@41078
   223
where
haftmann@49950
   224
  "ex_n_lists P n \<longleftrightarrow> (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
bulwahn@41078
   225
bulwahn@41078
   226
lemma [code]:
haftmann@49950
   227
  "ex_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
haftmann@49950
   228
  unfolding ex_n_lists_def enum_ex
haftmann@49950
   229
  by (cases n) (auto simp add: enum_UNIV)
bulwahn@41078
   230
haftmann@26444
   231
instantiation "fun" :: (enum, enum) enum
haftmann@26444
   232
begin
haftmann@26444
   233
haftmann@26444
   234
definition
haftmann@49948
   235
  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (List.n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
haftmann@26444
   236
bulwahn@41078
   237
definition
bulwahn@41078
   238
  "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
bulwahn@41078
   239
bulwahn@41078
   240
definition
bulwahn@41078
   241
  "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
bulwahn@41078
   242
haftmann@26444
   243
instance proof
haftmann@26444
   244
  show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
haftmann@26444
   245
  proof (rule UNIV_eq_I)
haftmann@26444
   246
    fix f :: "'a \<Rightarrow> 'b"
haftmann@26444
   247
    have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
bulwahn@40683
   248
      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
haftmann@26444
   249
    then show "f \<in> set enum"
bulwahn@40683
   250
      by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
haftmann@26444
   251
  qed
haftmann@26444
   252
next
haftmann@26444
   253
  from map_of_zip_enum_inject
haftmann@26444
   254
  show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
haftmann@26444
   255
    by (auto intro!: inj_onI simp add: enum_fun_def
haftmann@49950
   256
      distinct_map distinct_n_lists enum_distinct set_n_lists)
bulwahn@41078
   257
next
bulwahn@41078
   258
  fix P
haftmann@49950
   259
  show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Ball UNIV P"
bulwahn@41078
   260
  proof
bulwahn@41078
   261
    assume "enum_all P"
haftmann@49950
   262
    show "Ball UNIV P"
bulwahn@41078
   263
    proof
bulwahn@41078
   264
      fix f :: "'a \<Rightarrow> 'b"
bulwahn@41078
   265
      have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
bulwahn@41078
   266
        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
bulwahn@41078
   267
      from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))"
bulwahn@41078
   268
        unfolding enum_all_fun_def all_n_lists_def
bulwahn@41078
   269
        apply (simp add: set_n_lists)
bulwahn@41078
   270
        apply (erule_tac x="map f enum" in allE)
bulwahn@41078
   271
        apply (auto intro!: in_enum)
bulwahn@41078
   272
        done
bulwahn@41078
   273
      from this f show "P f" by auto
bulwahn@41078
   274
    qed
bulwahn@41078
   275
  next
haftmann@49950
   276
    assume "Ball UNIV P"
bulwahn@41078
   277
    from this show "enum_all P"
bulwahn@41078
   278
      unfolding enum_all_fun_def all_n_lists_def by auto
bulwahn@41078
   279
  qed
bulwahn@41078
   280
next
bulwahn@41078
   281
  fix P
haftmann@49950
   282
  show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Bex UNIV P"
bulwahn@41078
   283
  proof
bulwahn@41078
   284
    assume "enum_ex P"
haftmann@49950
   285
    from this show "Bex UNIV P"
bulwahn@41078
   286
      unfolding enum_ex_fun_def ex_n_lists_def by auto
bulwahn@41078
   287
  next
haftmann@49950
   288
    assume "Bex UNIV P"
bulwahn@41078
   289
    from this obtain f where "P f" ..
bulwahn@41078
   290
    have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
bulwahn@41078
   291
      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
bulwahn@41078
   292
    from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
bulwahn@41078
   293
      by auto
bulwahn@41078
   294
    from  this show "enum_ex P"
bulwahn@41078
   295
      unfolding enum_ex_fun_def ex_n_lists_def
bulwahn@41078
   296
      apply (auto simp add: set_n_lists)
bulwahn@41078
   297
      apply (rule_tac x="map f enum" in exI)
bulwahn@41078
   298
      apply (auto intro!: in_enum)
bulwahn@41078
   299
      done
bulwahn@41078
   300
  qed
haftmann@26444
   301
qed
haftmann@26444
   302
haftmann@26444
   303
end
haftmann@26444
   304
haftmann@38857
   305
lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
haftmann@49948
   306
  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
haftmann@28245
   307
  by (simp add: enum_fun_def Let_def)
haftmann@26444
   308
bulwahn@41078
   309
lemma enum_all_fun_code [code]:
bulwahn@41078
   310
  "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
bulwahn@41078
   311
   in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
haftmann@49950
   312
  by (simp only: enum_all_fun_def Let_def)
bulwahn@41078
   313
bulwahn@41078
   314
lemma enum_ex_fun_code [code]:
bulwahn@41078
   315
  "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
bulwahn@41078
   316
   in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
haftmann@49950
   317
  by (simp only: enum_ex_fun_def Let_def)
haftmann@45963
   318
haftmann@45963
   319
instantiation set :: (enum) enum
haftmann@45963
   320
begin
haftmann@45963
   321
haftmann@45963
   322
definition
haftmann@45963
   323
  "enum = map set (sublists enum)"
haftmann@45963
   324
haftmann@45963
   325
definition
haftmann@45963
   326
  "enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
haftmann@45963
   327
haftmann@45963
   328
definition
haftmann@45963
   329
  "enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
haftmann@45963
   330
haftmann@45963
   331
instance proof
haftmann@45963
   332
qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
haftmann@45963
   333
  enum_distinct enum_UNIV)
huffman@29024
   334
huffman@29024
   335
end
huffman@29024
   336
haftmann@49950
   337
instantiation unit :: enum
haftmann@49950
   338
begin
haftmann@49950
   339
haftmann@49950
   340
definition
haftmann@49950
   341
  "enum = [()]"
haftmann@49950
   342
haftmann@49950
   343
definition
haftmann@49950
   344
  "enum_all P = P ()"
haftmann@49950
   345
haftmann@49950
   346
definition
haftmann@49950
   347
  "enum_ex P = P ()"
haftmann@49950
   348
haftmann@49950
   349
instance proof
haftmann@49950
   350
qed (auto simp add: enum_unit_def enum_all_unit_def enum_ex_unit_def)
haftmann@49950
   351
haftmann@49950
   352
end
haftmann@49950
   353
haftmann@49950
   354
instantiation bool :: enum
haftmann@49950
   355
begin
haftmann@49950
   356
haftmann@49950
   357
definition
haftmann@49950
   358
  "enum = [False, True]"
haftmann@49950
   359
haftmann@49950
   360
definition
haftmann@49950
   361
  "enum_all P \<longleftrightarrow> P False \<and> P True"
haftmann@49950
   362
haftmann@49950
   363
definition
haftmann@49950
   364
  "enum_ex P \<longleftrightarrow> P False \<or> P True"
haftmann@49950
   365
haftmann@49950
   366
instance proof
haftmann@49950
   367
qed (simp_all only: enum_bool_def enum_all_bool_def enum_ex_bool_def UNIV_bool, simp_all)
haftmann@49950
   368
haftmann@49950
   369
end
haftmann@49950
   370
haftmann@49950
   371
instantiation prod :: (enum, enum) enum
haftmann@49950
   372
begin
haftmann@49950
   373
haftmann@49950
   374
definition
haftmann@49950
   375
  "enum = List.product enum enum"
haftmann@49950
   376
haftmann@49950
   377
definition
haftmann@49950
   378
  "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
haftmann@49950
   379
haftmann@49950
   380
definition
haftmann@49950
   381
  "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
haftmann@49950
   382
haftmann@49950
   383
 
haftmann@49950
   384
instance by default
haftmann@49950
   385
  (simp_all add: enum_prod_def product_list_set distinct_product
haftmann@49950
   386
    enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
haftmann@49950
   387
haftmann@49950
   388
end
haftmann@49950
   389
haftmann@49950
   390
instantiation sum :: (enum, enum) enum
haftmann@49950
   391
begin
haftmann@49950
   392
haftmann@49950
   393
definition
haftmann@49950
   394
  "enum = map Inl enum @ map Inr enum"
haftmann@49950
   395
haftmann@49950
   396
definition
haftmann@49950
   397
  "enum_all P \<longleftrightarrow> enum_all (\<lambda>x. P (Inl x)) \<and> enum_all (\<lambda>x. P (Inr x))"
haftmann@49950
   398
haftmann@49950
   399
definition
haftmann@49950
   400
  "enum_ex P \<longleftrightarrow> enum_ex (\<lambda>x. P (Inl x)) \<or> enum_ex (\<lambda>x. P (Inr x))"
haftmann@49950
   401
haftmann@49950
   402
instance proof
haftmann@49950
   403
qed (simp_all only: enum_sum_def enum_all_sum_def enum_ex_sum_def UNIV_sum,
haftmann@49950
   404
  auto simp add: enum_UNIV distinct_map enum_distinct)
haftmann@49950
   405
haftmann@49950
   406
end
haftmann@49950
   407
haftmann@49950
   408
instantiation nibble :: enum
haftmann@49950
   409
begin
haftmann@49950
   410
haftmann@49950
   411
definition
haftmann@49950
   412
  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
haftmann@49950
   413
    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
haftmann@49950
   414
haftmann@49950
   415
definition
haftmann@49950
   416
  "enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
haftmann@49950
   417
     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
haftmann@49950
   418
haftmann@49950
   419
definition
haftmann@49950
   420
  "enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
haftmann@49950
   421
     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
haftmann@49950
   422
haftmann@49950
   423
instance proof
haftmann@49950
   424
qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
haftmann@49950
   425
haftmann@49950
   426
end
haftmann@49950
   427
haftmann@49950
   428
instantiation char :: enum
haftmann@49950
   429
begin
haftmann@49950
   430
haftmann@49950
   431
definition
haftmann@49950
   432
  "enum = chars"
haftmann@49950
   433
haftmann@49950
   434
definition
haftmann@49950
   435
  "enum_all P \<longleftrightarrow> list_all P chars"
haftmann@49950
   436
haftmann@49950
   437
definition
haftmann@49950
   438
  "enum_ex P \<longleftrightarrow> list_ex P chars"
haftmann@49950
   439
haftmann@49950
   440
instance proof
haftmann@49950
   441
qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
haftmann@49950
   442
  simp_all add: list_all_iff list_ex_iff)
haftmann@49950
   443
haftmann@49950
   444
end
haftmann@49950
   445
haftmann@49950
   446
instantiation option :: (enum) enum
haftmann@49950
   447
begin
haftmann@49950
   448
haftmann@49950
   449
definition
haftmann@49950
   450
  "enum = None # map Some enum"
haftmann@49950
   451
haftmann@49950
   452
definition
haftmann@49950
   453
  "enum_all P \<longleftrightarrow> P None \<and> enum_all (\<lambda>x. P (Some x))"
haftmann@49950
   454
haftmann@49950
   455
definition
haftmann@49950
   456
  "enum_ex P \<longleftrightarrow> P None \<or> enum_ex (\<lambda>x. P (Some x))"
haftmann@49950
   457
haftmann@49950
   458
instance proof
haftmann@49950
   459
qed (simp_all only: enum_option_def enum_all_option_def enum_ex_option_def UNIV_option_conv,
haftmann@49950
   460
  auto simp add: distinct_map enum_UNIV enum_distinct)
haftmann@49950
   461
haftmann@49950
   462
end
haftmann@49950
   463
haftmann@45963
   464
bulwahn@40647
   465
subsection {* Small finite types *}
bulwahn@40647
   466
bulwahn@40647
   467
text {* We define small finite types for the use in Quickcheck *}
bulwahn@40647
   468
bulwahn@40647
   469
datatype finite_1 = a\<^isub>1
bulwahn@40647
   470
bulwahn@40900
   471
notation (output) a\<^isub>1  ("a\<^isub>1")
bulwahn@40900
   472
haftmann@49950
   473
lemma UNIV_finite_1:
haftmann@49950
   474
  "UNIV = {a\<^isub>1}"
haftmann@49950
   475
  by (auto intro: finite_1.exhaust)
haftmann@49950
   476
bulwahn@40647
   477
instantiation finite_1 :: enum
bulwahn@40647
   478
begin
bulwahn@40647
   479
bulwahn@40647
   480
definition
bulwahn@40647
   481
  "enum = [a\<^isub>1]"
bulwahn@40647
   482
bulwahn@41078
   483
definition
bulwahn@41078
   484
  "enum_all P = P a\<^isub>1"
bulwahn@41078
   485
bulwahn@41078
   486
definition
bulwahn@41078
   487
  "enum_ex P = P a\<^isub>1"
bulwahn@41078
   488
bulwahn@40647
   489
instance proof
haftmann@49950
   490
qed (simp_all only: enum_finite_1_def enum_all_finite_1_def enum_ex_finite_1_def UNIV_finite_1, simp_all)
bulwahn@40647
   491
huffman@29024
   492
end
bulwahn@40647
   493
bulwahn@40651
   494
instantiation finite_1 :: linorder
bulwahn@40651
   495
begin
bulwahn@40651
   496
haftmann@49950
   497
definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
haftmann@49950
   498
where
haftmann@49950
   499
  "x < (y :: finite_1) \<longleftrightarrow> False"
haftmann@49950
   500
bulwahn@40651
   501
definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
bulwahn@40651
   502
where
haftmann@49950
   503
  "x \<le> (y :: finite_1) \<longleftrightarrow> True"
bulwahn@40651
   504
bulwahn@40651
   505
instance
bulwahn@40651
   506
apply (intro_classes)
bulwahn@40651
   507
apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
bulwahn@40651
   508
apply (metis finite_1.exhaust)
bulwahn@40651
   509
done
bulwahn@40651
   510
bulwahn@40651
   511
end
bulwahn@40651
   512
bulwahn@41085
   513
hide_const (open) a\<^isub>1
bulwahn@40657
   514
bulwahn@40647
   515
datatype finite_2 = a\<^isub>1 | a\<^isub>2
bulwahn@40647
   516
bulwahn@40900
   517
notation (output) a\<^isub>1  ("a\<^isub>1")
bulwahn@40900
   518
notation (output) a\<^isub>2  ("a\<^isub>2")
bulwahn@40900
   519
haftmann@49950
   520
lemma UNIV_finite_2:
haftmann@49950
   521
  "UNIV = {a\<^isub>1, a\<^isub>2}"
haftmann@49950
   522
  by (auto intro: finite_2.exhaust)
haftmann@49950
   523
bulwahn@40647
   524
instantiation finite_2 :: enum
bulwahn@40647
   525
begin
bulwahn@40647
   526
bulwahn@40647
   527
definition
bulwahn@40647
   528
  "enum = [a\<^isub>1, a\<^isub>2]"
bulwahn@40647
   529
bulwahn@41078
   530
definition
haftmann@49950
   531
  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2"
bulwahn@41078
   532
bulwahn@41078
   533
definition
haftmann@49950
   534
  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2"
bulwahn@41078
   535
bulwahn@40647
   536
instance proof
haftmann@49950
   537
qed (simp_all only: enum_finite_2_def enum_all_finite_2_def enum_ex_finite_2_def UNIV_finite_2, simp_all)
bulwahn@40647
   538
bulwahn@40647
   539
end
bulwahn@40647
   540
bulwahn@40651
   541
instantiation finite_2 :: linorder
bulwahn@40651
   542
begin
bulwahn@40651
   543
bulwahn@40651
   544
definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
bulwahn@40651
   545
where
haftmann@49950
   546
  "x < y \<longleftrightarrow> x = a\<^isub>1 \<and> y = a\<^isub>2"
bulwahn@40651
   547
bulwahn@40651
   548
definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
bulwahn@40651
   549
where
haftmann@49950
   550
  "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_2)"
bulwahn@40651
   551
bulwahn@40651
   552
instance
bulwahn@40651
   553
apply (intro_classes)
bulwahn@40651
   554
apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
haftmann@49950
   555
apply (metis finite_2.nchotomy)+
bulwahn@40651
   556
done
bulwahn@40651
   557
bulwahn@40651
   558
end
bulwahn@40651
   559
bulwahn@41085
   560
hide_const (open) a\<^isub>1 a\<^isub>2
bulwahn@40657
   561
bulwahn@40647
   562
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
bulwahn@40647
   563
bulwahn@40900
   564
notation (output) a\<^isub>1  ("a\<^isub>1")
bulwahn@40900
   565
notation (output) a\<^isub>2  ("a\<^isub>2")
bulwahn@40900
   566
notation (output) a\<^isub>3  ("a\<^isub>3")
bulwahn@40900
   567
haftmann@49950
   568
lemma UNIV_finite_3:
haftmann@49950
   569
  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3}"
haftmann@49950
   570
  by (auto intro: finite_3.exhaust)
haftmann@49950
   571
bulwahn@40647
   572
instantiation finite_3 :: enum
bulwahn@40647
   573
begin
bulwahn@40647
   574
bulwahn@40647
   575
definition
bulwahn@40647
   576
  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
bulwahn@40647
   577
bulwahn@41078
   578
definition
haftmann@49950
   579
  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3"
bulwahn@41078
   580
bulwahn@41078
   581
definition
haftmann@49950
   582
  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3"
bulwahn@41078
   583
bulwahn@40647
   584
instance proof
haftmann@49950
   585
qed (simp_all only: enum_finite_3_def enum_all_finite_3_def enum_ex_finite_3_def UNIV_finite_3, simp_all)
bulwahn@40647
   586
bulwahn@40647
   587
end
bulwahn@40647
   588
bulwahn@40651
   589
instantiation finite_3 :: linorder
bulwahn@40651
   590
begin
bulwahn@40651
   591
bulwahn@40651
   592
definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
bulwahn@40651
   593
where
haftmann@49950
   594
  "x < y = (case x of a\<^isub>1 \<Rightarrow> y \<noteq> a\<^isub>1 | a\<^isub>2 \<Rightarrow> y = a\<^isub>3 | a\<^isub>3 \<Rightarrow> False)"
bulwahn@40651
   595
bulwahn@40651
   596
definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
bulwahn@40651
   597
where
haftmann@49950
   598
  "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_3)"
bulwahn@40651
   599
bulwahn@40651
   600
instance proof (intro_classes)
bulwahn@40651
   601
qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
bulwahn@40651
   602
bulwahn@40651
   603
end
bulwahn@40651
   604
bulwahn@41085
   605
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
bulwahn@40657
   606
bulwahn@40647
   607
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
bulwahn@40647
   608
bulwahn@40900
   609
notation (output) a\<^isub>1  ("a\<^isub>1")
bulwahn@40900
   610
notation (output) a\<^isub>2  ("a\<^isub>2")
bulwahn@40900
   611
notation (output) a\<^isub>3  ("a\<^isub>3")
bulwahn@40900
   612
notation (output) a\<^isub>4  ("a\<^isub>4")
bulwahn@40900
   613
haftmann@49950
   614
lemma UNIV_finite_4:
haftmann@49950
   615
  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4}"
haftmann@49950
   616
  by (auto intro: finite_4.exhaust)
haftmann@49950
   617
bulwahn@40647
   618
instantiation finite_4 :: enum
bulwahn@40647
   619
begin
bulwahn@40647
   620
bulwahn@40647
   621
definition
bulwahn@40647
   622
  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
bulwahn@40647
   623
bulwahn@41078
   624
definition
haftmann@49950
   625
  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4"
bulwahn@41078
   626
bulwahn@41078
   627
definition
haftmann@49950
   628
  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4"
bulwahn@41078
   629
bulwahn@40647
   630
instance proof
haftmann@49950
   631
qed (simp_all only: enum_finite_4_def enum_all_finite_4_def enum_ex_finite_4_def UNIV_finite_4, simp_all)
bulwahn@40647
   632
bulwahn@40647
   633
end
bulwahn@40647
   634
bulwahn@41085
   635
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
bulwahn@40651
   636
bulwahn@40651
   637
bulwahn@40647
   638
datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
bulwahn@40647
   639
bulwahn@40900
   640
notation (output) a\<^isub>1  ("a\<^isub>1")
bulwahn@40900
   641
notation (output) a\<^isub>2  ("a\<^isub>2")
bulwahn@40900
   642
notation (output) a\<^isub>3  ("a\<^isub>3")
bulwahn@40900
   643
notation (output) a\<^isub>4  ("a\<^isub>4")
bulwahn@40900
   644
notation (output) a\<^isub>5  ("a\<^isub>5")
bulwahn@40900
   645
haftmann@49950
   646
lemma UNIV_finite_5:
haftmann@49950
   647
  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5}"
haftmann@49950
   648
  by (auto intro: finite_5.exhaust)
haftmann@49950
   649
bulwahn@40647
   650
instantiation finite_5 :: enum
bulwahn@40647
   651
begin
bulwahn@40647
   652
bulwahn@40647
   653
definition
bulwahn@40647
   654
  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
bulwahn@40647
   655
bulwahn@41078
   656
definition
haftmann@49950
   657
  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5"
bulwahn@41078
   658
bulwahn@41078
   659
definition
haftmann@49950
   660
  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5"
bulwahn@41078
   661
bulwahn@40647
   662
instance proof
haftmann@49950
   663
qed (simp_all only: enum_finite_5_def enum_all_finite_5_def enum_ex_finite_5_def UNIV_finite_5, simp_all)
bulwahn@40647
   664
bulwahn@40647
   665
end
bulwahn@40647
   666
bulwahn@46352
   667
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
bulwahn@46352
   668
haftmann@49948
   669
bulwahn@46352
   670
subsection {* Closing up *}
bulwahn@40657
   671
bulwahn@41085
   672
hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
haftmann@49948
   673
hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
bulwahn@40647
   674
bulwahn@40647
   675
end
haftmann@49948
   676