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