src/HOL/Enum.thy
author wenzelm
Fri Mar 30 17:25:34 2012 +0200 (2012-03-30)
changeset 47231 3ff8c79a9e2f
parent 47221 7205eb4a0a05
parent 47230 6584098d5378
child 48123 104e5fccea12
permissions -rw-r--r--
merged
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Finite types as explicit enumerations *}
     4 
     5 theory Enum
     6 imports Map String
     7 begin
     8 
     9 subsection {* Class @{text enum} *}
    10 
    11 class enum =
    12   fixes enum :: "'a list"
    13   fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    14   fixes enum_ex  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    15   assumes UNIV_enum: "UNIV = set enum"
    16     and enum_distinct: "distinct enum"
    17   assumes enum_all : "enum_all P = (\<forall> x. P x)"
    18   assumes enum_ex  : "enum_ex P = (\<exists> x. P x)" 
    19 begin
    20 
    21 subclass finite proof
    22 qed (simp add: UNIV_enum)
    23 
    24 lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum ..
    25 
    26 lemma in_enum: "x \<in> set enum"
    27   unfolding enum_UNIV by auto
    28 
    29 lemma enum_eq_I:
    30   assumes "\<And>x. x \<in> set xs"
    31   shows "set enum = set xs"
    32 proof -
    33   from assms UNIV_eq_I have "UNIV = set xs" by auto
    34   with enum_UNIV show ?thesis by simp
    35 qed
    36 
    37 end
    38 
    39 
    40 subsection {* Equality and order on functions *}
    41 
    42 instantiation "fun" :: (enum, equal) equal
    43 begin
    44 
    45 definition
    46   "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    47 
    48 instance proof
    49 qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff)
    50 
    51 end
    52 
    53 lemma [code]:
    54   "HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
    55 by (auto simp add: equal enum_all fun_eq_iff)
    56 
    57 lemma [code nbe]:
    58   "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
    59   by (fact equal_refl)
    60 
    61 lemma order_fun [code]:
    62   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    63   shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
    64     and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
    65   by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
    66 
    67 
    68 subsection {* Quantifiers *}
    69 
    70 lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
    71   by (simp add: enum_all)
    72 
    73 lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
    74   by (simp add: enum_ex)
    75 
    76 lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
    77 unfolding list_ex1_iff enum_UNIV by auto
    78 
    79 
    80 subsection {* Default instances *}
    81 
    82 primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    83   "n_lists 0 xs = [[]]"
    84   | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    85 
    86 lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    87   by (induct n) simp_all
    88 
    89 lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    90   by (induct n) (auto simp add: length_concat o_def listsum_triv)
    91 
    92 lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    93   by (induct n arbitrary: ys) auto
    94 
    95 lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    96 proof (rule set_eqI)
    97   fix ys :: "'a list"
    98   show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    99   proof -
   100     have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
   101       by (induct n arbitrary: ys) auto
   102     moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
   103       by (induct n arbitrary: ys) auto
   104     moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
   105       by (induct ys) auto
   106     ultimately show ?thesis by auto
   107   qed
   108 qed
   109 
   110 lemma distinct_n_lists:
   111   assumes "distinct xs"
   112   shows "distinct (n_lists n xs)"
   113 proof (rule card_distinct)
   114   from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   115   have "card (set (n_lists n xs)) = card (set xs) ^ n"
   116   proof (induct n)
   117     case 0 then show ?case by simp
   118   next
   119     case (Suc n)
   120     moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   121       = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   122       by (rule card_UN_disjoint) auto
   123     moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   124       by (rule card_image) (simp add: inj_on_def)
   125     ultimately show ?case by auto
   126   qed
   127   also have "\<dots> = length xs ^ n" by (simp add: card_length)
   128   finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
   129     by (simp add: length_n_lists)
   130 qed
   131 
   132 lemma map_of_zip_enum_is_Some:
   133   assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   134   shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
   135 proof -
   136   from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
   137     (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
   138     by (auto intro!: map_of_zip_is_Some)
   139   then show ?thesis using enum_UNIV by auto
   140 qed
   141 
   142 lemma map_of_zip_enum_inject:
   143   fixes xs ys :: "'b\<Colon>enum list"
   144   assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
   145       "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   146     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)"
   147   shows "xs = ys"
   148 proof -
   149   have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
   150   proof
   151     fix x :: 'a
   152     from length map_of_zip_enum_is_Some obtain y1 y2
   153       where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
   154         and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
   155     moreover from map_of
   156       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)"
   157       by (auto dest: fun_cong)
   158     ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
   159       by simp
   160   qed
   161   with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
   162 qed
   163 
   164 definition
   165   all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
   166 where
   167   "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
   168 
   169 lemma [code]:
   170   "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
   171 unfolding all_n_lists_def enum_all
   172 by (cases n) (auto simp add: enum_UNIV)
   173 
   174 definition
   175   ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
   176 where
   177   "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
   178 
   179 lemma [code]:
   180   "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
   181 unfolding ex_n_lists_def enum_ex
   182 by (cases n) (auto simp add: enum_UNIV)
   183 
   184 
   185 instantiation "fun" :: (enum, enum) enum
   186 begin
   187 
   188 definition
   189   "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   190 
   191 definition
   192   "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
   193 
   194 definition
   195   "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
   196 
   197 
   198 instance proof
   199   show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   200   proof (rule UNIV_eq_I)
   201     fix f :: "'a \<Rightarrow> 'b"
   202     have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   203       by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
   204     then show "f \<in> set enum"
   205       by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
   206   qed
   207 next
   208   from map_of_zip_enum_inject
   209   show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   210     by (auto intro!: inj_onI simp add: enum_fun_def
   211       distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   212 next
   213   fix P
   214   show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
   215   proof
   216     assume "enum_all P"
   217     show "\<forall>x. P x"
   218     proof
   219       fix f :: "'a \<Rightarrow> 'b"
   220       have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   221         by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
   222       from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))"
   223         unfolding enum_all_fun_def all_n_lists_def
   224         apply (simp add: set_n_lists)
   225         apply (erule_tac x="map f enum" in allE)
   226         apply (auto intro!: in_enum)
   227         done
   228       from this f show "P f" by auto
   229     qed
   230   next
   231     assume "\<forall>x. P x"
   232     from this show "enum_all P"
   233       unfolding enum_all_fun_def all_n_lists_def by auto
   234   qed
   235 next
   236   fix P
   237   show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
   238   proof
   239     assume "enum_ex P"
   240     from this show "\<exists>x. P x"
   241       unfolding enum_ex_fun_def ex_n_lists_def by auto
   242   next
   243     assume "\<exists>x. P x"
   244     from this obtain f where "P f" ..
   245     have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   246       by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
   247     from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
   248       by auto
   249     from  this show "enum_ex P"
   250       unfolding enum_ex_fun_def ex_n_lists_def
   251       apply (auto simp add: set_n_lists)
   252       apply (rule_tac x="map f enum" in exI)
   253       apply (auto intro!: in_enum)
   254       done
   255   qed
   256 qed
   257 
   258 end
   259 
   260 lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   261   in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   262   by (simp add: enum_fun_def Let_def)
   263 
   264 lemma enum_all_fun_code [code]:
   265   "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
   266    in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
   267   by (simp add: enum_all_fun_def Let_def)
   268 
   269 lemma enum_ex_fun_code [code]:
   270   "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
   271    in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
   272   by (simp add: enum_ex_fun_def Let_def)
   273 
   274 instantiation unit :: enum
   275 begin
   276 
   277 definition
   278   "enum = [()]"
   279 
   280 definition
   281   "enum_all P = P ()"
   282 
   283 definition
   284   "enum_ex P = P ()"
   285 
   286 instance proof
   287 qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust)
   288 
   289 end
   290 
   291 instantiation bool :: enum
   292 begin
   293 
   294 definition
   295   "enum = [False, True]"
   296 
   297 definition
   298   "enum_all P = (P False \<and> P True)"
   299 
   300 definition
   301   "enum_ex P = (P False \<or> P True)"
   302 
   303 instance proof
   304   fix P
   305   show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)"
   306     unfolding enum_all_bool_def by (auto, case_tac x) auto
   307 next
   308   fix P
   309   show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)"
   310     unfolding enum_ex_bool_def by (auto, case_tac x) auto
   311 qed (auto simp add: enum_bool_def UNIV_bool)
   312 
   313 end
   314 
   315 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   316   "product [] _ = []"
   317   | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   318 
   319 lemma product_list_set:
   320   "set (product xs ys) = set xs \<times> set ys"
   321   by (induct xs) auto
   322 
   323 lemma distinct_product:
   324   assumes "distinct xs" and "distinct ys"
   325   shows "distinct (product xs ys)"
   326   using assms by (induct xs)
   327     (auto intro: inj_onI simp add: product_list_set distinct_map)
   328 
   329 instantiation prod :: (enum, enum) enum
   330 begin
   331 
   332 definition
   333   "enum = product enum enum"
   334 
   335 definition
   336   "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
   337 
   338 definition
   339   "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
   340 
   341  
   342 instance by default
   343   (simp_all add: enum_prod_def product_list_set distinct_product
   344     enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex)
   345 
   346 end
   347 
   348 instantiation sum :: (enum, enum) enum
   349 begin
   350 
   351 definition
   352   "enum = map Inl enum @ map Inr enum"
   353 
   354 definition
   355   "enum_all P = (enum_all (%x. P (Inl x)) \<and> enum_all (%x. P (Inr x)))"
   356 
   357 definition
   358   "enum_ex P = (enum_ex (%x. P (Inl x)) \<or> enum_ex (%x. P (Inr x)))"
   359 
   360 instance proof
   361   fix P
   362   show "enum_all (P :: ('a + 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
   363     unfolding enum_all_sum_def enum_all
   364     by (auto, case_tac x) auto
   365 next
   366   fix P
   367   show "enum_ex (P :: ('a + 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
   368     unfolding enum_ex_sum_def enum_ex
   369     by (auto, case_tac x) auto
   370 qed (auto simp add: enum_UNIV enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
   371 
   372 end
   373 
   374 instantiation nibble :: enum
   375 begin
   376 
   377 definition
   378   "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   379     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   380 
   381 definition
   382   "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
   383      \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF)"
   384 
   385 definition
   386   "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
   387      \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF)"
   388 
   389 instance proof
   390   fix P
   391   show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)"
   392     unfolding enum_all_nibble_def
   393     by (auto, case_tac x) auto
   394 next
   395   fix P
   396   show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)"
   397     unfolding enum_ex_nibble_def
   398     by (auto, case_tac x) auto
   399 qed (simp_all add: enum_nibble_def UNIV_nibble)
   400 
   401 end
   402 
   403 instantiation char :: enum
   404 begin
   405 
   406 definition
   407   "enum = map (split Char) (product enum enum)"
   408 
   409 lemma enum_chars [code]:
   410   "enum = chars"
   411   unfolding enum_char_def chars_def enum_nibble_def by simp
   412 
   413 definition
   414   "enum_all P = list_all P chars"
   415 
   416 definition
   417   "enum_ex P = list_ex P chars"
   418 
   419 lemma set_enum_char: "set (enum :: char list) = UNIV"
   420     by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric])
   421 
   422 instance proof
   423   fix P
   424   show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)"
   425     unfolding enum_all_char_def enum_chars[symmetric]
   426     by (auto simp add: list_all_iff set_enum_char)
   427 next
   428   fix P
   429   show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)"
   430     unfolding enum_ex_char_def enum_chars[symmetric]
   431     by (auto simp add: list_ex_iff set_enum_char)
   432 next
   433   show "distinct (enum :: char list)"
   434     by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct)
   435 qed (auto simp add: set_enum_char)
   436 
   437 end
   438 
   439 instantiation option :: (enum) enum
   440 begin
   441 
   442 definition
   443   "enum = None # map Some enum"
   444 
   445 definition
   446   "enum_all P = (P None \<and> enum_all (%x. P (Some x)))"
   447 
   448 definition
   449   "enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))"
   450 
   451 instance proof
   452   fix P
   453   show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)"
   454     unfolding enum_all_option_def enum_all
   455     by (auto, case_tac x) auto
   456 next
   457   fix P
   458   show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)"
   459     unfolding enum_ex_option_def enum_ex
   460     by (auto, case_tac x) auto
   461 qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
   462 end
   463 
   464 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   465   "sublists [] = [[]]"
   466   | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   467 
   468 lemma length_sublists:
   469   "length (sublists xs) = 2 ^ length xs"
   470   by (induct xs) (simp_all add: Let_def)
   471 
   472 lemma sublists_powset:
   473   "set ` set (sublists xs) = Pow (set xs)"
   474 proof -
   475   have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   476     by (auto simp add: image_def)
   477   have "set (map set (sublists xs)) = Pow (set xs)"
   478     by (induct xs)
   479       (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   480   then show ?thesis by simp
   481 qed
   482 
   483 lemma distinct_set_sublists:
   484   assumes "distinct xs"
   485   shows "distinct (map set (sublists xs))"
   486 proof (rule card_distinct)
   487   have "finite (set xs)" by rule
   488   then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   489   with assms distinct_card [of xs]
   490     have "card (Pow (set xs)) = 2 ^ length xs" by simp
   491   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   492     by (simp add: sublists_powset length_sublists)
   493 qed
   494 
   495 instantiation set :: (enum) enum
   496 begin
   497 
   498 definition
   499   "enum = map set (sublists enum)"
   500 
   501 definition
   502   "enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
   503 
   504 definition
   505   "enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
   506 
   507 instance proof
   508 qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
   509   enum_distinct enum_UNIV)
   510 
   511 end
   512 
   513 
   514 subsection {* Small finite types *}
   515 
   516 text {* We define small finite types for the use in Quickcheck *}
   517 
   518 datatype finite_1 = a\<^isub>1
   519 
   520 notation (output) a\<^isub>1  ("a\<^isub>1")
   521 
   522 instantiation finite_1 :: enum
   523 begin
   524 
   525 definition
   526   "enum = [a\<^isub>1]"
   527 
   528 definition
   529   "enum_all P = P a\<^isub>1"
   530 
   531 definition
   532   "enum_ex P = P a\<^isub>1"
   533 
   534 instance proof
   535   fix P
   536   show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)"
   537     unfolding enum_all_finite_1_def
   538     by (auto, case_tac x) auto
   539 next
   540   fix P
   541   show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)"
   542     unfolding enum_ex_finite_1_def
   543     by (auto, case_tac x) auto
   544 qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
   545 
   546 end
   547 
   548 instantiation finite_1 :: linorder
   549 begin
   550 
   551 definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
   552 where
   553   "less_eq_finite_1 x y = True"
   554 
   555 definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
   556 where
   557   "less_finite_1 x y = False"
   558 
   559 instance
   560 apply (intro_classes)
   561 apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
   562 apply (metis finite_1.exhaust)
   563 done
   564 
   565 end
   566 
   567 hide_const (open) a\<^isub>1
   568 
   569 datatype finite_2 = a\<^isub>1 | a\<^isub>2
   570 
   571 notation (output) a\<^isub>1  ("a\<^isub>1")
   572 notation (output) a\<^isub>2  ("a\<^isub>2")
   573 
   574 instantiation finite_2 :: enum
   575 begin
   576 
   577 definition
   578   "enum = [a\<^isub>1, a\<^isub>2]"
   579 
   580 definition
   581   "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)"
   582 
   583 definition
   584   "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)"
   585 
   586 instance proof
   587   fix P
   588   show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)"
   589     unfolding enum_all_finite_2_def
   590     by (auto, case_tac x) auto
   591 next
   592   fix P
   593   show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)"
   594     unfolding enum_ex_finite_2_def
   595     by (auto, case_tac x) auto
   596 qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
   597 
   598 end
   599 
   600 instantiation finite_2 :: linorder
   601 begin
   602 
   603 definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
   604 where
   605   "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
   606 
   607 definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
   608 where
   609   "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
   610 
   611 
   612 instance
   613 apply (intro_classes)
   614 apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
   615 apply (metis finite_2.distinct finite_2.nchotomy)+
   616 done
   617 
   618 end
   619 
   620 hide_const (open) a\<^isub>1 a\<^isub>2
   621 
   622 
   623 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
   624 
   625 notation (output) a\<^isub>1  ("a\<^isub>1")
   626 notation (output) a\<^isub>2  ("a\<^isub>2")
   627 notation (output) a\<^isub>3  ("a\<^isub>3")
   628 
   629 instantiation finite_3 :: enum
   630 begin
   631 
   632 definition
   633   "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
   634 
   635 definition
   636   "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)"
   637 
   638 definition
   639   "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)"
   640 
   641 instance proof
   642   fix P
   643   show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)"
   644     unfolding enum_all_finite_3_def
   645     by (auto, case_tac x) auto
   646 next
   647   fix P
   648   show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)"
   649     unfolding enum_ex_finite_3_def
   650     by (auto, case_tac x) auto
   651 qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
   652 
   653 end
   654 
   655 instantiation finite_3 :: linorder
   656 begin
   657 
   658 definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   659 where
   660   "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
   661      | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
   662 
   663 definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   664 where
   665   "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
   666 
   667 
   668 instance proof (intro_classes)
   669 qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
   670 
   671 end
   672 
   673 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
   674 
   675 
   676 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
   677 
   678 notation (output) a\<^isub>1  ("a\<^isub>1")
   679 notation (output) a\<^isub>2  ("a\<^isub>2")
   680 notation (output) a\<^isub>3  ("a\<^isub>3")
   681 notation (output) a\<^isub>4  ("a\<^isub>4")
   682 
   683 instantiation finite_4 :: enum
   684 begin
   685 
   686 definition
   687   "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
   688 
   689 definition
   690   "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)"
   691 
   692 definition
   693   "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)"
   694 
   695 instance proof
   696   fix P
   697   show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)"
   698     unfolding enum_all_finite_4_def
   699     by (auto, case_tac x) auto
   700 next
   701   fix P
   702   show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)"
   703     unfolding enum_ex_finite_4_def
   704     by (auto, case_tac x) auto
   705 qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
   706 
   707 end
   708 
   709 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
   710 
   711 
   712 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
   713 
   714 notation (output) a\<^isub>1  ("a\<^isub>1")
   715 notation (output) a\<^isub>2  ("a\<^isub>2")
   716 notation (output) a\<^isub>3  ("a\<^isub>3")
   717 notation (output) a\<^isub>4  ("a\<^isub>4")
   718 notation (output) a\<^isub>5  ("a\<^isub>5")
   719 
   720 instantiation finite_5 :: enum
   721 begin
   722 
   723 definition
   724   "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
   725 
   726 definition
   727   "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)"
   728 
   729 definition
   730   "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)"
   731 
   732 instance proof
   733   fix P
   734   show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)"
   735     unfolding enum_all_finite_5_def
   736     by (auto, case_tac x) auto
   737 next
   738   fix P
   739   show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)"
   740     unfolding enum_ex_finite_5_def
   741     by (auto, case_tac x) auto
   742 qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
   743 
   744 end
   745 
   746 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   747 
   748 subsection {* An executable THE operator on finite types *}
   749 
   750 definition
   751   [code del]: "enum_the P = The P"
   752 
   753 lemma [code]:
   754   "The P = (case filter P enum of [x] => x | _ => enum_the P)"
   755 proof -
   756   {
   757     fix a
   758     assume filter_enum: "filter P enum = [a]"
   759     have "The P = a"
   760     proof (rule the_equality)
   761       fix x
   762       assume "P x"
   763       show "x = a"
   764       proof (rule ccontr)
   765         assume "x \<noteq> a"
   766         from filter_enum obtain us vs
   767           where enum_eq: "enum = us @ [a] @ vs"
   768           and "\<forall> x \<in> set us. \<not> P x"
   769           and "\<forall> x \<in> set vs. \<not> P x"
   770           and "P a"
   771           by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
   772         with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
   773       qed
   774     next
   775       from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
   776     qed
   777   }
   778   from this show ?thesis
   779     unfolding enum_the_def by (auto split: list.split)
   780 qed
   781 
   782 code_abort enum_the
   783 code_const enum_the (Eval "(fn p => raise Match)")
   784 
   785 subsection {* Further operations on finite types *}
   786 
   787 lemma [code]:
   788   "Collect P = set (filter P enum)"
   789 by (auto simp add: enum_UNIV)
   790 
   791 lemma tranclp_unfold [code, no_atp]:
   792   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
   793 by (simp add: trancl_def)
   794 
   795 lemma rtranclp_rtrancl_eq[code, no_atp]:
   796   "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
   797 unfolding rtrancl_def by auto
   798 
   799 lemma max_ext_eq[code]:
   800   "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
   801 by (auto simp add: max_ext.simps)
   802 
   803 lemma max_extp_eq[code]:
   804   "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})"
   805 unfolding max_ext_def by auto
   806 
   807 lemma mlex_eq[code]:
   808   "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}"
   809 unfolding mlex_prod_def by auto
   810 
   811 subsection {* Executable accessible part *}
   812 (* FIXME: should be moved somewhere else !? *)
   813 
   814 subsubsection {* Finite monotone eventually stable sequences *}
   815 
   816 lemma finite_mono_remains_stable_implies_strict_prefix:
   817   fixes f :: "nat \<Rightarrow> 'a::order"
   818   assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
   819   shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   820   using assms
   821 proof -
   822   have "\<exists>n. f n = f (Suc n)"
   823   proof (rule ccontr)
   824     assume "\<not> ?thesis"
   825     then have "\<And>n. f n \<noteq> f (Suc n)" by auto
   826     then have "\<And>n. f n < f (Suc n)"
   827       using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
   828     with lift_Suc_mono_less_iff[of f]
   829     have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
   830     then have "inj f"
   831       by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
   832     with `finite (range f)` have "finite (UNIV::nat set)"
   833       by (rule finite_imageD)
   834     then show False by simp
   835   qed
   836   then obtain n where n: "f n = f (Suc n)" ..
   837   def N \<equiv> "LEAST n. f n = f (Suc n)"
   838   have N: "f N = f (Suc N)"
   839     unfolding N_def using n by (rule LeastI)
   840   show ?thesis
   841   proof (intro exI[of _ N] conjI allI impI)
   842     fix n assume "N \<le> n"
   843     then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
   844     proof (induct rule: dec_induct)
   845       case (step n) then show ?case
   846         using eq[rule_format, of "n - 1"] N
   847         by (cases n) (auto simp add: le_Suc_eq)
   848     qed simp
   849     from this[of n] `N \<le> n` show "f N = f n" by auto
   850   next
   851     fix n m :: nat assume "m < n" "n \<le> N"
   852     then show "f m < f n"
   853     proof (induct rule: less_Suc_induct[consumes 1])
   854       case (1 i)
   855       then have "i < N" by simp
   856       then have "f i \<noteq> f (Suc i)"
   857         unfolding N_def by (rule not_less_Least)
   858       with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
   859     qed auto
   860   qed
   861 qed
   862 
   863 lemma finite_mono_strict_prefix_implies_finite_fixpoint:
   864   fixes f :: "nat \<Rightarrow> 'a set"
   865   assumes S: "\<And>i. f i \<subseteq> S" "finite S"
   866     and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   867   shows "f (card S) = (\<Union>n. f n)"
   868 proof -
   869   from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
   870 
   871   { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
   872     proof (induct i)
   873       case 0 then show ?case by simp
   874     next
   875       case (Suc i)
   876       with inj[rule_format, of "Suc i" i]
   877       have "(f i) \<subset> (f (Suc i))" by auto
   878       moreover have "finite (f (Suc i))" using S by (rule finite_subset)
   879       ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
   880       with Suc show ?case using inj by auto
   881     qed
   882   }
   883   then have "N \<le> card (f N)" by simp
   884   also have "\<dots> \<le> card S" using S by (intro card_mono)
   885   finally have "f (card S) = f N" using eq by auto
   886   then show ?thesis using eq inj[rule_format, of N]
   887     apply auto
   888     apply (case_tac "n < N")
   889     apply (auto simp: not_less)
   890     done
   891 qed
   892 
   893 subsubsection {* Bounded accessible part *}
   894 
   895 fun bacc :: "('a * 'a) set => nat => 'a set" 
   896 where
   897   "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
   898 | "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
   899 
   900 lemma bacc_subseteq_acc:
   901   "bacc r n \<subseteq> acc r"
   902 by (induct n) (auto intro: acc.intros)
   903 
   904 lemma bacc_mono:
   905   "n <= m ==> bacc r n \<subseteq> bacc r m"
   906 by (induct rule: dec_induct) auto
   907   
   908 lemma bacc_upper_bound:
   909   "bacc (r :: ('a * 'a) set)  (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
   910 proof -
   911   have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
   912   moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
   913   moreover have "finite (range (bacc r))" by auto
   914   ultimately show ?thesis
   915    by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
   916      (auto intro: finite_mono_remains_stable_implies_strict_prefix  simp add: enum_UNIV)
   917 qed
   918 
   919 lemma acc_subseteq_bacc:
   920   assumes "finite r"
   921   shows "acc r \<subseteq> (UN n. bacc r n)"
   922 proof
   923   fix x
   924   assume "x : acc r"
   925   then have "\<exists> n. x : bacc r n"
   926   proof (induct x arbitrary: rule: acc.induct)
   927     case (accI x)
   928     then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
   929     from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
   930     obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
   931     proof
   932       fix y assume y: "(y, x) : r"
   933       with n have "y : bacc r (n y)" by auto
   934       moreover have "n y <= Max ((%(y, x). n y) ` r)"
   935         using y `finite r` by (auto intro!: Max_ge)
   936       note bacc_mono[OF this, of r]
   937       ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
   938     qed
   939     then show ?case
   940       by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   941   qed
   942   then show "x : (UN n. bacc r n)" by auto
   943 qed
   944 
   945 lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
   946 by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
   947 
   948 definition 
   949   [code del]: "card_UNIV = card UNIV"
   950 
   951 lemma [code]:
   952   "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
   953 unfolding card_UNIV_def enum_UNIV ..
   954 
   955 declare acc_bacc_eq[folded card_UNIV_def, code]
   956 
   957 lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
   958 unfolding acc_def by simp
   959 
   960 subsection {* Closing up *}
   961 
   962 hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
   963 hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
   964 
   965 end