src/HOL/Library/Enum.thy
author haftmann
Thu Mar 20 12:01:10 2008 +0100 (2008-03-20)
changeset 26348 0f8e23edd357
child 26444 6a5faa5bcf19
permissions -rw-r--r--
added theory Library/Enum.thy
haftmann@26348
     1
(*  Title:      HOL/Library/Enum.thy
haftmann@26348
     2
    ID:         $Id$
haftmann@26348
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@26348
     4
*)
haftmann@26348
     5
haftmann@26348
     6
header {* Finite types as explicit enumerations *}
haftmann@26348
     7
haftmann@26348
     8
theory Enum
haftmann@26348
     9
imports Main
haftmann@26348
    10
begin
haftmann@26348
    11
haftmann@26348
    12
subsection {* Class @{text enum} *}
haftmann@26348
    13
haftmann@26348
    14
class enum = finite + -- FIXME
haftmann@26348
    15
  fixes enum :: "'a list"
haftmann@26348
    16
  assumes enum_all: "set enum = UNIV"
haftmann@26348
    17
begin
haftmann@26348
    18
haftmann@26348
    19
lemma in_enum [intro]: "x \<in> set enum"
haftmann@26348
    20
  unfolding enum_all by auto
haftmann@26348
    21
haftmann@26348
    22
lemma enum_eq_I:
haftmann@26348
    23
  assumes "\<And>x. x \<in> set xs"
haftmann@26348
    24
  shows "set enum = set xs"
haftmann@26348
    25
proof -
haftmann@26348
    26
  from assms UNIV_eq_I have "UNIV = set xs" by auto
haftmann@26348
    27
  with enum_all show ?thesis by simp
haftmann@26348
    28
qed
haftmann@26348
    29
haftmann@26348
    30
end
haftmann@26348
    31
haftmann@26348
    32
haftmann@26348
    33
subsection {* Equality and order on functions *}
haftmann@26348
    34
haftmann@26348
    35
declare eq_fun [code func del] order_fun [code func del]
haftmann@26348
    36
haftmann@26348
    37
instance "fun" :: (enum, eq) eq ..
haftmann@26348
    38
haftmann@26348
    39
lemma eq_fun [code func]:
haftmann@26348
    40
  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>eq"
haftmann@26348
    41
  shows "f = g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
haftmann@26348
    42
  by (simp add: enum_all expand_fun_eq)
haftmann@26348
    43
haftmann@26348
    44
lemma order_fun [code func]:
haftmann@26348
    45
  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
haftmann@26348
    46
  shows "f \<le> g \<longleftrightarrow> (\<forall>x \<in> set enum. f x \<le> g x)"
haftmann@26348
    47
    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x \<in> set enum. f x \<noteq> g x)"
haftmann@26348
    48
  by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
haftmann@26348
    49
haftmann@26348
    50
haftmann@26348
    51
subsection {* Default instances *}
haftmann@26348
    52
haftmann@26348
    53
instantiation unit :: enum
haftmann@26348
    54
begin
haftmann@26348
    55
haftmann@26348
    56
definition
haftmann@26348
    57
  "enum = [()]"
haftmann@26348
    58
haftmann@26348
    59
instance by default
haftmann@26348
    60
  (simp add: enum_unit_def UNIV_unit)
haftmann@26348
    61
haftmann@26348
    62
end
haftmann@26348
    63
haftmann@26348
    64
instantiation bool :: enum
haftmann@26348
    65
begin
haftmann@26348
    66
haftmann@26348
    67
definition
haftmann@26348
    68
  "enum = [False, True]"
haftmann@26348
    69
haftmann@26348
    70
instance by default
haftmann@26348
    71
  (simp add: enum_bool_def UNIV_bool)
haftmann@26348
    72
haftmann@26348
    73
end
haftmann@26348
    74
haftmann@26348
    75
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
haftmann@26348
    76
  "product [] _ = []"
haftmann@26348
    77
  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
haftmann@26348
    78
haftmann@26348
    79
lemma product_list_set:
haftmann@26348
    80
  "set (product xs ys) = set xs \<times> set ys"
haftmann@26348
    81
  by (induct xs) auto
haftmann@26348
    82
haftmann@26348
    83
instantiation * :: (enum, enum) enum
haftmann@26348
    84
begin
haftmann@26348
    85
haftmann@26348
    86
definition
haftmann@26348
    87
  "enum = product enum enum"
haftmann@26348
    88
haftmann@26348
    89
instance by default
haftmann@26348
    90
  (simp add: enum_prod_def product_list_set enum_all)
haftmann@26348
    91
haftmann@26348
    92
end
haftmann@26348
    93
haftmann@26348
    94
instantiation "+" :: (enum, enum) enum
haftmann@26348
    95
begin
haftmann@26348
    96
haftmann@26348
    97
definition
haftmann@26348
    98
  "enum = map Inl enum @ map Inr enum"
haftmann@26348
    99
haftmann@26348
   100
instance by default
haftmann@26348
   101
  (auto simp add: enum_all enum_sum_def, case_tac x, auto)
haftmann@26348
   102
haftmann@26348
   103
end
haftmann@26348
   104
haftmann@26348
   105
primrec sublists :: "'a list \<Rightarrow> 'a list list" where
haftmann@26348
   106
  "sublists [] = [[]]"
haftmann@26348
   107
  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
haftmann@26348
   108
haftmann@26348
   109
lemma sublists_powset:
haftmann@26348
   110
  "set (map set (sublists xs)) = Pow (set xs)"
haftmann@26348
   111
proof -
haftmann@26348
   112
  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
haftmann@26348
   113
    by (auto simp add: image_def)
haftmann@26348
   114
  show ?thesis
haftmann@26348
   115
    by (induct xs)
haftmann@26348
   116
     (simp_all add: aux Let_def Pow_insert Un_commute)
haftmann@26348
   117
qed
haftmann@26348
   118
haftmann@26348
   119
instantiation set :: (enum) enum
haftmann@26348
   120
begin
haftmann@26348
   121
haftmann@26348
   122
definition
haftmann@26348
   123
  "enum = map set (sublists enum)"
haftmann@26348
   124
haftmann@26348
   125
instance by default
haftmann@26348
   126
  (simp add: enum_set_def sublists_powset enum_all del: set_map)
haftmann@26348
   127
haftmann@26348
   128
end
haftmann@26348
   129
haftmann@26348
   130
instantiation nibble :: enum
haftmann@26348
   131
begin
haftmann@26348
   132
haftmann@26348
   133
definition
haftmann@26348
   134
  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
haftmann@26348
   135
    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
haftmann@26348
   136
haftmann@26348
   137
instance by default
haftmann@26348
   138
  (simp add: enum_nibble_def UNIV_nibble)
haftmann@26348
   139
haftmann@26348
   140
end
haftmann@26348
   141
haftmann@26348
   142
instantiation char :: enum
haftmann@26348
   143
begin
haftmann@26348
   144
haftmann@26348
   145
definition
haftmann@26348
   146
  "enum = map (split Char) (product enum enum)"
haftmann@26348
   147
haftmann@26348
   148
instance by default
haftmann@26348
   149
  (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric])
haftmann@26348
   150
haftmann@26348
   151
end
haftmann@26348
   152
haftmann@26348
   153
(*instantiation "fun" :: (enum, enum) enum
haftmann@26348
   154
begin
haftmann@26348
   155
haftmann@26348
   156
haftmann@26348
   157
definition
haftmann@26348
   158
  "enum 
haftmann@26348
   159
haftmann@26348
   160
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
haftmann@26348
   161
  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
haftmann@26348
   162
haftmann@26348
   163
instance "fun" :: (finite, finite) finite
haftmann@26348
   164
proof
haftmann@26348
   165
  show "finite (UNIV :: ('a => 'b) set)"
haftmann@26348
   166
  proof (rule finite_imageD)
haftmann@26348
   167
    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
haftmann@26348
   168
    show "finite (range ?graph)" by (rule finite)
haftmann@26348
   169
    show "inj ?graph" by (rule inj_graph)
haftmann@26348
   170
  qed
haftmann@26348
   171
qed*)
haftmann@26348
   172
haftmann@26348
   173
end