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