src/HOL/Enum.thy
 changeset 41078 051251fde456 parent 40900 1d5f76d79856 child 41085 a549ff1d4070
```     1.1 --- a/src/HOL/Enum.thy	Wed Dec 08 14:25:07 2010 +0100
1.2 +++ b/src/HOL/Enum.thy	Wed Dec 08 14:25:08 2010 +0100
1.3 @@ -10,24 +10,28 @@
1.4
1.5  class enum =
1.6    fixes enum :: "'a list"
1.7 +  fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
1.8 +  fixes enum_ex  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
1.9    assumes UNIV_enum: "UNIV = set enum"
1.10      and enum_distinct: "distinct enum"
1.11 +  assumes enum_all : "enum_all P = (\<forall> x. P x)"
1.12 +  assumes enum_ex  : "enum_ex P = (\<exists> x. P x)"
1.13  begin
1.14
1.15  subclass finite proof
1.17
1.18 -lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
1.19 +lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum ..
1.20
1.21  lemma in_enum: "x \<in> set enum"
1.22 -  unfolding enum_all by auto
1.23 +  unfolding enum_UNIV by auto
1.24
1.25  lemma enum_eq_I:
1.26    assumes "\<And>x. x \<in> set xs"
1.27    shows "set enum = set xs"
1.28  proof -
1.29    from assms UNIV_eq_I have "UNIV = set xs" by auto
1.30 -  with enum_all show ?thesis by simp
1.31 +  with enum_UNIV show ?thesis by simp
1.32  qed
1.33
1.34  end
1.35 @@ -42,13 +46,13 @@
1.36    "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
1.37
1.38  instance proof
1.39 -qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
1.40 +qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff)
1.41
1.42  end
1.43
1.44  lemma [code]:
1.45 -  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
1.46 -by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
1.47 +  "HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
1.48 +by (auto simp add: equal enum_all fun_eq_iff)
1.49
1.50  lemma [code nbe]:
1.51    "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
1.52 @@ -56,21 +60,21 @@
1.53
1.54  lemma order_fun [code]:
1.55    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
1.56 -  shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
1.57 -    and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
1.58 -  by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
1.59 +  shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
1.60 +    and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
1.61 +  by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
1.62
1.63
1.64  subsection {* Quantifiers *}
1.65
1.66 -lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
1.67 -  by (simp add: list_all_iff enum_all)
1.68 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
1.69 +  by (simp add: enum_all)
1.70
1.71 -lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
1.72 -  by (simp add: list_ex_iff enum_all)
1.73 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
1.74 +  by (simp add: enum_ex)
1.75
1.76  lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
1.77 -unfolding list_ex1_iff enum_all by auto
1.78 +unfolding list_ex1_iff enum_UNIV by auto
1.79
1.80
1.81  subsection {* Default instances *}
1.82 @@ -132,7 +136,7 @@
1.83    from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
1.84      (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
1.85      by (auto intro!: map_of_zip_is_Some)
1.86 -  then show ?thesis using enum_all by auto
1.87 +  then show ?thesis using enum_UNIV by auto
1.88  qed
1.89
1.90  lemma map_of_zip_enum_inject:
1.91 @@ -156,12 +160,40 @@
1.92    with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
1.93  qed
1.94
1.95 +definition
1.96 +  all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.97 +where
1.98 +  "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
1.99 +
1.100 +lemma [code]:
1.101 +  "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
1.102 +unfolding all_n_lists_def enum_all
1.103 +by (cases n) (auto simp add: enum_UNIV)
1.104 +
1.105 +definition
1.106 +  ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.107 +where
1.108 +  "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
1.109 +
1.110 +lemma [code]:
1.111 +  "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
1.112 +unfolding ex_n_lists_def enum_ex
1.113 +by (cases n) (auto simp add: enum_UNIV)
1.114 +
1.115 +
1.116  instantiation "fun" :: (enum, enum) enum
1.117  begin
1.118
1.119  definition
1.120    "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
1.121
1.122 +definition
1.123 +  "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
1.124 +
1.125 +definition
1.126 +  "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
1.127 +
1.128 +
1.129  instance proof
1.130    show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.131    proof (rule UNIV_eq_I)
1.132 @@ -176,6 +208,50 @@
1.133    show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.134      by (auto intro!: inj_onI simp add: enum_fun_def
1.135        distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
1.136 +next
1.137 +  fix P
1.138 +  show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
1.139 +  proof
1.140 +    assume "enum_all P"
1.141 +    show "\<forall>x. P x"
1.142 +    proof
1.143 +      fix f :: "'a \<Rightarrow> 'b"
1.144 +      have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.145 +        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
1.146 +      from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))"
1.147 +        unfolding enum_all_fun_def all_n_lists_def
1.148 +        apply (simp add: set_n_lists)
1.149 +        apply (erule_tac x="map f enum" in allE)
1.150 +        apply (auto intro!: in_enum)
1.151 +        done
1.152 +      from this f show "P f" by auto
1.153 +    qed
1.154 +  next
1.155 +    assume "\<forall>x. P x"
1.156 +    from this show "enum_all P"
1.157 +      unfolding enum_all_fun_def all_n_lists_def by auto
1.158 +  qed
1.159 +next
1.160 +  fix P
1.161 +  show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
1.162 +  proof
1.163 +    assume "enum_ex P"
1.164 +    from this show "\<exists>x. P x"
1.165 +      unfolding enum_ex_fun_def ex_n_lists_def by auto
1.166 +  next
1.167 +    assume "\<exists>x. P x"
1.168 +    from this obtain f where "P f" ..
1.169 +    have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.170 +      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
1.171 +    from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))"
1.172 +      by auto
1.173 +    from  this show "enum_ex P"
1.174 +      unfolding enum_ex_fun_def ex_n_lists_def
1.175 +      apply (auto simp add: set_n_lists)
1.176 +      apply (rule_tac x="map f enum" in exI)
1.177 +      apply (auto intro!: in_enum)
1.178 +      done
1.179 +  qed
1.180  qed
1.181
1.182  end
1.183 @@ -184,14 +260,30 @@
1.184    in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
1.185    by (simp add: enum_fun_def Let_def)
1.186
1.187 +lemma enum_all_fun_code [code]:
1.188 +  "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.189 +   in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.190 +  by (simp add: enum_all_fun_def Let_def)
1.191 +
1.192 +lemma enum_ex_fun_code [code]:
1.193 +  "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.194 +   in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.195 +  by (simp add: enum_ex_fun_def Let_def)
1.196 +
1.197  instantiation unit :: enum
1.198  begin
1.199
1.200  definition
1.201    "enum = [()]"
1.202
1.203 +definition
1.204 +  "enum_all P = P ()"
1.205 +
1.206 +definition
1.207 +  "enum_ex P = P ()"
1.208 +
1.209  instance proof
1.210 -qed (simp_all add: enum_unit_def UNIV_unit)
1.211 +qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust)
1.212
1.213  end
1.214
1.215 @@ -201,8 +293,21 @@
1.216  definition
1.217    "enum = [False, True]"
1.218
1.219 +definition
1.220 +  "enum_all P = (P False \<and> P True)"
1.221 +
1.222 +definition
1.223 +  "enum_ex P = (P False \<or> P True)"
1.224 +
1.225  instance proof
1.226 -qed (simp_all add: enum_bool_def UNIV_bool)
1.227 +  fix P
1.228 +  show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)"
1.229 +    unfolding enum_all_bool_def by (auto, case_tac x) auto
1.230 +next
1.231 +  fix P
1.232 +  show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)"
1.233 +    unfolding enum_ex_bool_def by (auto, case_tac x) auto
1.234 +qed (auto simp add: enum_bool_def UNIV_bool)
1.235
1.236  end
1.237
1.238 @@ -226,8 +331,16 @@
1.239  definition
1.240    "enum = product enum enum"
1.241
1.242 +definition
1.243 +  "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
1.244 +
1.245 +definition
1.246 +  "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
1.247 +
1.248 +
1.249  instance by default
1.250 -  (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
1.251 +  (simp_all add: enum_prod_def product_list_set distinct_product
1.252 +    enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex)
1.253
1.254  end
1.255
1.256 @@ -237,8 +350,23 @@
1.257  definition
1.258    "enum = map Inl enum @ map Inr enum"
1.259
1.260 -instance by default
1.261 -  (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
1.262 +definition
1.263 +  "enum_all P = (enum_all (%x. P (Inl x)) \<and> enum_all (%x. P (Inr x)))"
1.264 +
1.265 +definition
1.266 +  "enum_ex P = (enum_ex (%x. P (Inl x)) \<or> enum_ex (%x. P (Inr x)))"
1.267 +
1.268 +instance proof
1.269 +  fix P
1.270 +  show "enum_all (P :: ('a + 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
1.271 +    unfolding enum_all_sum_def enum_all
1.272 +    by (auto, case_tac x) auto
1.273 +next
1.274 +  fix P
1.275 +  show "enum_ex (P :: ('a + 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
1.276 +    unfolding enum_ex_sum_def enum_ex
1.277 +    by (auto, case_tac x) auto
1.278 +qed (auto simp add: enum_UNIV enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
1.279
1.280  end
1.281
1.282 @@ -280,7 +408,24 @@
1.283    "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
1.284      Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
1.285
1.286 +definition
1.287 +  "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
1.288 +     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF)"
1.289 +
1.290 +definition
1.291 +  "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
1.292 +     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF)"
1.293 +
1.294  instance proof
1.295 +  fix P
1.296 +  show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)"
1.297 +    unfolding enum_all_nibble_def
1.298 +    by (auto, case_tac x) auto
1.299 +next
1.300 +  fix P
1.301 +  show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)"
1.302 +    unfolding enum_ex_nibble_def
1.303 +    by (auto, case_tac x) auto
1.304  qed (simp_all add: enum_nibble_def UNIV_nibble)
1.305
1.306  end
1.307 @@ -295,9 +440,29 @@
1.308    "enum = chars"
1.309    unfolding enum_char_def chars_def enum_nibble_def by simp
1.310
1.311 +definition
1.312 +  "enum_all P = list_all P chars"
1.313 +
1.314 +definition
1.315 +  "enum_ex P = list_ex P chars"
1.316 +
1.317 +lemma set_enum_char: "set (enum :: char list) = UNIV"
1.318 +    by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric])
1.319 +
1.320  instance proof
1.321 -qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
1.322 -  distinct_map distinct_product enum_distinct)
1.323 +  fix P
1.324 +  show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)"
1.325 +    unfolding enum_all_char_def enum_chars[symmetric]
1.326 +    by (auto simp add: list_all_iff set_enum_char)
1.327 +next
1.328 +  fix P
1.329 +  show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)"
1.330 +    unfolding enum_ex_char_def enum_chars[symmetric]
1.331 +    by (auto simp add: list_ex_iff set_enum_char)
1.332 +next
1.333 +  show "distinct (enum :: char list)"
1.334 +    by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct)
1.335 +qed (auto simp add: set_enum_char)
1.336
1.337  end
1.338
1.339 @@ -307,8 +472,23 @@
1.340  definition
1.341    "enum = None # map Some enum"
1.342
1.343 +definition
1.344 +  "enum_all P = (P None \<and> enum_all (%x. P (Some x)))"
1.345 +
1.346 +definition
1.347 +  "enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))"
1.348 +
1.349  instance proof
1.350 -qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
1.351 +  fix P
1.352 +  show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)"
1.353 +    unfolding enum_all_option_def enum_all
1.354 +    by (auto, case_tac x) auto
1.355 +next
1.356 +  fix P
1.357 +  show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)"
1.358 +    unfolding enum_ex_option_def enum_ex
1.359 +    by (auto, case_tac x) auto
1.360 +qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
1.361
1.362  end
1.363
1.364 @@ -326,7 +506,22 @@
1.365  definition
1.366    "enum = [a\<^isub>1]"
1.367
1.368 +definition
1.369 +  "enum_all P = P a\<^isub>1"
1.370 +
1.371 +definition
1.372 +  "enum_ex P = P a\<^isub>1"
1.373 +
1.374  instance proof
1.375 +  fix P
1.376 +  show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)"
1.377 +    unfolding enum_all_finite_1_def
1.378 +    by (auto, case_tac x) auto
1.379 +next
1.380 +  fix P
1.381 +  show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)"
1.382 +    unfolding enum_ex_finite_1_def
1.383 +    by (auto, case_tac x) auto
1.384  qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
1.385
1.386  end
1.387 @@ -363,7 +558,22 @@
1.388  definition
1.389    "enum = [a\<^isub>1, a\<^isub>2]"
1.390
1.391 +definition
1.392 +  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)"
1.393 +
1.394 +definition
1.395 +  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)"
1.396 +
1.397  instance proof
1.398 +  fix P
1.399 +  show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)"
1.400 +    unfolding enum_all_finite_2_def
1.401 +    by (auto, case_tac x) auto
1.402 +next
1.403 +  fix P
1.404 +  show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)"
1.405 +    unfolding enum_ex_finite_2_def
1.406 +    by (auto, case_tac x) auto
1.407  qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
1.408
1.409  end
1.410 @@ -403,7 +613,22 @@
1.411  definition
1.412    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
1.413
1.414 +definition
1.415 +  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)"
1.416 +
1.417 +definition
1.418 +  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)"
1.419 +
1.420  instance proof
1.421 +  fix P
1.422 +  show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)"
1.423 +    unfolding enum_all_finite_3_def
1.424 +    by (auto, case_tac x) auto
1.425 +next
1.426 +  fix P
1.427 +  show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)"
1.428 +    unfolding enum_ex_finite_3_def
1.429 +    by (auto, case_tac x) auto
1.430  qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
1.431
1.432  end
1.433 @@ -442,7 +667,22 @@
1.434  definition
1.435    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
1.436
1.437 +definition
1.438 +  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)"
1.439 +
1.440 +definition
1.441 +  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)"
1.442 +
1.443  instance proof
1.444 +  fix P
1.445 +  show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)"
1.446 +    unfolding enum_all_finite_4_def
1.447 +    by (auto, case_tac x) auto
1.448 +next
1.449 +  fix P
1.450 +  show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)"
1.451 +    unfolding enum_ex_finite_4_def
1.452 +    by (auto, case_tac x) auto
1.453  qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
1.454
1.455  end
1.456 @@ -464,7 +704,22 @@
1.457  definition
1.458    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
1.459
1.460 +definition
1.461 +  "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)"
1.462 +
1.463 +definition
1.464 +  "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)"
1.465 +
1.466  instance proof
1.467 +  fix P
1.468 +  show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)"
1.469 +    unfolding enum_all_finite_5_def
1.470 +    by (auto, case_tac x) auto
1.471 +next
1.472 +  fix P
1.473 +  show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)"
1.474 +    unfolding enum_ex_finite_5_def
1.475 +    by (auto, case_tac x) auto
1.476  qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
1.477
1.478  end
1.479 @@ -473,6 +728,6 @@
1.480
1.481
1.482  hide_type finite_1 finite_2 finite_3 finite_4 finite_5
1.483 -hide_const (open) enum n_lists product
1.484 +hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
1.485
1.486  end
```