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