adding more efficient implementations for quantifiers in Enum
authorbulwahn
Wed Dec 08 14:25:08 2010 +0100 (2010-12-08)
changeset 41078051251fde456
parent 41077 fd6f41d349ef
child 41084 a434f89a9962
adding more efficient implementations for quantifiers in Enum
src/HOL/Enum.thy
     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.16  qed (simp add: UNIV_enum)
    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