src/HOL/Library/Enum.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28245 9767dd8e1e54
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     1 (*  Title:      HOL/Library/Enum.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Finite types as explicit enumerations *}
     7 
     8 theory Enum
     9 imports Plain "~~/src/HOL/Map"
    10 begin
    11 
    12 subsection {* Class @{text enum} *}
    13 
    14 class enum = itself +
    15   fixes enum :: "'a list"
    16   assumes UNIV_enum [code func]: "UNIV = set enum"
    17     and enum_distinct: "distinct enum"
    18 begin
    19 
    20 lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
    21   unfolding UNIV_enum ..
    22 
    23 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
    24 
    25 lemma in_enum [intro]: "x \<in> set enum"
    26   unfolding enum_all by auto
    27 
    28 lemma enum_eq_I:
    29   assumes "\<And>x. x \<in> set xs"
    30   shows "set enum = set xs"
    31 proof -
    32   from assms UNIV_eq_I have "UNIV = set xs" by auto
    33   with enum_all show ?thesis by simp
    34 qed
    35 
    36 end
    37 
    38 
    39 subsection {* Equality and order on functions *}
    40 
    41 instantiation "fun" :: (enum, eq) eq
    42 begin
    43 
    44 definition
    45   "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    46 
    47 instance by default
    48   (simp_all add: eq_fun_def enum_all expand_fun_eq)
    49 
    50 end
    51 
    52 lemma order_fun [code func]:
    53   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    54   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
    55     and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
    56   by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
    57 
    58 
    59 subsection {* Quantifiers *}
    60 
    61 lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
    62   by (simp add: list_all_iff enum_all)
    63 
    64 lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
    65   by (simp add: list_all_iff enum_all)
    66 
    67 
    68 subsection {* Default instances *}
    69 
    70 primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    71   "n_lists 0 xs = [[]]"
    72   | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    73 
    74 lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    75   by (induct n) simp_all
    76 
    77 lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    78   by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv)
    79 
    80 lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    81   by (induct n arbitrary: ys) auto
    82 
    83 lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    84 proof (rule set_ext)
    85   fix ys :: "'a list"
    86   show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    87   proof -
    88     have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    89       by (induct n arbitrary: ys) auto
    90     moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
    91       by (induct n arbitrary: ys) auto
    92     moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
    93       by (induct ys) auto
    94     ultimately show ?thesis by auto
    95   qed
    96 qed
    97 
    98 lemma distinct_n_lists:
    99   assumes "distinct xs"
   100   shows "distinct (n_lists n xs)"
   101 proof (rule card_distinct)
   102   from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   103   have "card (set (n_lists n xs)) = card (set xs) ^ n"
   104   proof (induct n)
   105     case 0 then show ?case by simp
   106   next
   107     case (Suc n)
   108     moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   109       = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   110       by (rule card_UN_disjoint) auto
   111     moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   112       by (rule card_image) (simp add: inj_on_def)
   113     ultimately show ?case by auto
   114   qed
   115   also have "\<dots> = length xs ^ n" by (simp add: card_length)
   116   finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
   117     by (simp add: length_n_lists)
   118 qed
   119 
   120 lemma map_of_zip_map:
   121   fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum"
   122   shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
   123   by (induct xs) (simp_all add: expand_fun_eq)
   124 
   125 lemma map_of_zip_enum_is_Some:
   126   assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   127   shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
   128 proof -
   129   from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
   130     (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
   131     by (auto intro!: map_of_zip_is_Some)
   132   then show ?thesis using enum_all by auto
   133 qed
   134 
   135 lemma map_of_zip_enum_inject:
   136   fixes xs ys :: "'b\<Colon>enum list"
   137   assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
   138       "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   139     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)"
   140   shows "xs = ys"
   141 proof -
   142   have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
   143   proof
   144     fix x :: 'a
   145     from length map_of_zip_enum_is_Some obtain y1 y2
   146       where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
   147         and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
   148     moreover from map_of 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)"
   149       by (auto dest: fun_cong)
   150     ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
   151       by simp
   152   qed
   153   with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
   154 qed
   155 
   156 instantiation "fun" :: (enum, enum) enum
   157 begin
   158 
   159 definition
   160   [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   161 
   162 instance proof
   163   show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   164   proof (rule UNIV_eq_I)
   165     fix f :: "'a \<Rightarrow> 'b"
   166     have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   167       by (auto simp add: map_of_zip_map expand_fun_eq)
   168     then show "f \<in> set enum"
   169       by (auto simp add: enum_fun_def set_n_lists)
   170   qed
   171 next
   172   from map_of_zip_enum_inject
   173   show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   174     by (auto intro!: inj_onI simp add: enum_fun_def
   175       distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   176 qed
   177 
   178 end
   179 
   180 lemma [code func]:
   181   "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>('a\<Colon>{enum, eq}) list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>{enum, eq} list)) enum)"
   182   unfolding enum_fun_def ..
   183 
   184 instantiation unit :: enum
   185 begin
   186 
   187 definition
   188   "enum = [()]"
   189 
   190 instance by default
   191   (simp_all add: enum_unit_def UNIV_unit)
   192 
   193 end
   194 
   195 instantiation bool :: enum
   196 begin
   197 
   198 definition
   199   "enum = [False, True]"
   200 
   201 instance by default
   202   (simp_all add: enum_bool_def UNIV_bool)
   203 
   204 end
   205 
   206 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   207   "product [] _ = []"
   208   | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   209 
   210 lemma product_list_set:
   211   "set (product xs ys) = set xs \<times> set ys"
   212   by (induct xs) auto
   213 
   214 lemma distinct_product:
   215   assumes "distinct xs" and "distinct ys"
   216   shows "distinct (product xs ys)"
   217   using assms by (induct xs)
   218     (auto intro: inj_onI simp add: product_list_set distinct_map)
   219 
   220 instantiation * :: (enum, enum) enum
   221 begin
   222 
   223 definition
   224   "enum = product enum enum"
   225 
   226 instance by default
   227   (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
   228 
   229 end
   230 
   231 instantiation "+" :: (enum, enum) enum
   232 begin
   233 
   234 definition
   235   "enum = map Inl enum @ map Inr enum"
   236 
   237 instance by default
   238   (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
   239 
   240 end
   241 
   242 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   243   "sublists [] = [[]]"
   244   | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   245 
   246 lemma length_sublists:
   247   "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
   248   by (induct xs) (simp_all add: Let_def)
   249 
   250 lemma sublists_powset:
   251   "set ` set (sublists xs) = Pow (set xs)"
   252 proof -
   253   have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   254     by (auto simp add: image_def)
   255   have "set (map set (sublists xs)) = Pow (set xs)"
   256     by (induct xs)
   257       (simp_all add: aux Let_def Pow_insert Un_commute)
   258   then show ?thesis by simp
   259 qed
   260 
   261 lemma distinct_set_sublists:
   262   assumes "distinct xs"
   263   shows "distinct (map set (sublists xs))"
   264 proof (rule card_distinct)
   265   have "finite (set xs)" by rule
   266   then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
   267   with assms distinct_card [of xs]
   268     have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
   269   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   270     by (simp add: sublists_powset length_sublists)
   271 qed
   272 
   273 instantiation nibble :: enum
   274 begin
   275 
   276 definition
   277   "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   278     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   279 
   280 instance by default
   281   (simp_all add: enum_nibble_def UNIV_nibble)
   282 
   283 end
   284 
   285 instantiation char :: enum
   286 begin
   287 
   288 definition
   289   [code func del]: "enum = map (split Char) (product enum enum)"
   290 
   291 lemma enum_char [code func]:
   292   "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   293   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   294   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   295   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
   296   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
   297   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
   298   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
   299   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
   300   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
   301   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
   302   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
   303   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
   304   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
   305   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   306   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   307   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   308   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   309   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   310   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   311   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   312   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   313   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   314   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   315   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   316   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   317   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   318   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   319   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   320   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   321   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   322   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   323   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   324   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   325   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   326   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   327   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   328   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   329   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   330   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   331   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   332   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   333   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   334   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   335   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   336   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   337   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   338   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   339   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   340   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   341   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   342   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   343   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   344   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   345   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   346   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   347   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   348   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   349   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   350   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   351   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   352   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   353   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   354   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   355   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   356   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   357   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   358   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   359   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   360   unfolding enum_char_def enum_nibble_def by simp
   361 
   362 instance by default
   363   (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
   364     distinct_map distinct_product enum_distinct)
   365 
   366 end
   367 
   368 end