src/HOL/Enum.thy
 changeset 49950 cd882d53ba6b parent 49949 be3dd2e602e8 child 49972 f11f8905d9fd
```     1.1 --- a/src/HOL/Enum.thy	Sat Oct 20 10:00:21 2012 +0200
1.2 +++ b/src/HOL/Enum.thy	Sat Oct 20 10:00:21 2012 +0200
1.3 @@ -11,20 +11,23 @@
1.4  class enum =
1.5    fixes enum :: "'a list"
1.6    fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
1.7 -  fixes enum_ex  :: "('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 +  assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
1.14 +  assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P"
1.15 +   -- {* tailored towards simple instantiation *}
1.16  begin
1.17
1.18  subclass finite proof
1.20
1.21 -lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum ..
1.22 +lemma enum_UNIV:
1.23 +  "set enum = UNIV"
1.24 +  by (simp only: UNIV_enum)
1.25
1.26  lemma in_enum: "x \<in> set enum"
1.27 -  unfolding enum_UNIV by auto
1.28 +  by (simp add: enum_UNIV)
1.29
1.30  lemma enum_eq_I:
1.31    assumes "\<And>x. x \<in> set xs"
1.32 @@ -34,6 +37,14 @@
1.33    with enum_UNIV show ?thesis by simp
1.34  qed
1.35
1.36 +lemma enum_all [simp]:
1.37 +  "enum_all = HOL.All"
1.38 +  by (simp add: fun_eq_iff enum_all_UNIV)
1.39 +
1.40 +lemma enum_ex [simp]:
1.41 +  "enum_ex = HOL.Ex"
1.42 +  by (simp add: fun_eq_iff enum_ex_UNIV)
1.43 +
1.44  end
1.45
1.46
1.47 @@ -43,7 +54,7 @@
1.48
1.49  lemma Collect_code [code]:
1.50    "Collect P = set (filter P enum)"
1.51 -  by (auto simp add: enum_UNIV)
1.52 +  by (simp add: enum_UNIV)
1.53
1.54  definition card_UNIV :: "'a itself \<Rightarrow> nat"
1.55  where
1.56 @@ -54,13 +65,13 @@
1.57    by (simp only: card_UNIV_def enum_UNIV)
1.58
1.59  lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
1.60 -  by (simp add: enum_all)
1.61 +  by simp
1.62
1.63  lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
1.64 -  by (simp add: enum_ex)
1.65 +  by simp
1.66
1.67  lemma exists1_code [code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
1.68 -  by (auto simp add: enum_UNIV list_ex1_iff)
1.69 +  by (auto simp add: list_ex1_iff enum_UNIV)
1.70
1.71
1.72  subsubsection {* An executable choice operator *}
1.73 @@ -110,13 +121,13 @@
1.74    "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
1.75
1.76  instance proof
1.77 -qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff)
1.78 +qed (simp_all add: equal_fun_def fun_eq_iff enum_UNIV)
1.79
1.80  end
1.81
1.82  lemma [code]:
1.83    "HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
1.84 -by (auto simp add: equal enum_all fun_eq_iff)
1.85 +  by (auto simp add: equal fun_eq_iff)
1.86
1.87  lemma [code nbe]:
1.88    "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
1.89 @@ -126,7 +137,7 @@
1.90    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
1.91    shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
1.92      and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
1.93 -  by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
1.94 +  by (simp_all add: fun_eq_iff le_fun_def order_less_le)
1.95
1.96
1.97  subsubsection {* Operations on relations *}
1.98 @@ -199,26 +210,23 @@
1.99    with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
1.100  qed
1.101
1.102 -definition
1.103 -  all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.104 +definition all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.105  where
1.106 -  "all_n_lists P n = (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
1.107 +  "all_n_lists P n \<longleftrightarrow> (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
1.108
1.109  lemma [code]:
1.110 -  "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
1.111 -unfolding all_n_lists_def enum_all
1.112 -by (cases n) (auto simp add: enum_UNIV)
1.113 +  "all_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
1.114 +  unfolding all_n_lists_def enum_all
1.115 +  by (cases n) (auto simp add: enum_UNIV)
1.116
1.117 -definition
1.118 -  ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.119 +definition ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
1.120  where
1.121 -  "ex_n_lists P n = (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
1.122 +  "ex_n_lists P n \<longleftrightarrow> (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
1.123
1.124  lemma [code]:
1.125 -  "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
1.126 -unfolding ex_n_lists_def enum_ex
1.127 -by (cases n) (auto simp add: enum_UNIV)
1.128 -
1.129 +  "ex_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
1.130 +  unfolding ex_n_lists_def enum_ex
1.131 +  by (cases n) (auto simp add: enum_UNIV)
1.132
1.133  instantiation "fun" :: (enum, enum) enum
1.134  begin
1.135 @@ -232,7 +240,6 @@
1.136  definition
1.137    "enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
1.138
1.139 -
1.140  instance proof
1.141    show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.142    proof (rule UNIV_eq_I)
1.143 @@ -246,13 +253,13 @@
1.144    from map_of_zip_enum_inject
1.145    show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.146      by (auto intro!: inj_onI simp add: enum_fun_def
1.147 -      distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
1.148 +      distinct_map distinct_n_lists enum_distinct set_n_lists)
1.149  next
1.150    fix P
1.151 -  show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
1.152 +  show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Ball UNIV P"
1.153    proof
1.154      assume "enum_all P"
1.155 -    show "\<forall>x. P x"
1.156 +    show "Ball UNIV P"
1.157      proof
1.158        fix f :: "'a \<Rightarrow> 'b"
1.159        have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.160 @@ -266,19 +273,19 @@
1.161        from this f show "P f" by auto
1.162      qed
1.163    next
1.164 -    assume "\<forall>x. P x"
1.165 +    assume "Ball UNIV P"
1.166      from this show "enum_all P"
1.167        unfolding enum_all_fun_def all_n_lists_def by auto
1.168    qed
1.169  next
1.170    fix P
1.171 -  show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
1.172 +  show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Bex UNIV P"
1.173    proof
1.174      assume "enum_ex P"
1.175 -    from this show "\<exists>x. P x"
1.176 +    from this show "Bex UNIV P"
1.177        unfolding enum_ex_fun_def ex_n_lists_def by auto
1.178    next
1.179 -    assume "\<exists>x. P x"
1.180 +    assume "Bex UNIV P"
1.181      from this obtain f where "P f" ..
1.182      have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.183        by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
1.184 @@ -302,188 +309,12 @@
1.185  lemma enum_all_fun_code [code]:
1.186    "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.187     in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.188 -  by (simp add: enum_all_fun_def Let_def)
1.189 +  by (simp only: enum_all_fun_def Let_def)
1.190
1.191  lemma enum_ex_fun_code [code]:
1.192    "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
1.193     in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
1.194 -  by (simp add: enum_ex_fun_def Let_def)
1.195 -
1.196 -instantiation unit :: enum
1.197 -begin
1.198 -
1.199 -definition
1.200 -  "enum = [()]"
1.201 -
1.202 -definition
1.203 -  "enum_all P = P ()"
1.204 -
1.205 -definition
1.206 -  "enum_ex P = P ()"
1.207 -
1.208 -instance proof
1.209 -qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust)
1.210 -
1.211 -end
1.212 -
1.213 -instantiation bool :: enum
1.214 -begin
1.215 -
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 -  fix P
1.227 -  show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)"
1.228 -    unfolding enum_all_bool_def by (auto, case_tac x) auto
1.229 -next
1.230 -  fix P
1.231 -  show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)"
1.232 -    unfolding enum_ex_bool_def by (auto, case_tac x) auto
1.233 -qed (auto simp add: enum_bool_def UNIV_bool)
1.234 -
1.235 -end
1.236 -
1.237 -instantiation prod :: (enum, enum) enum
1.238 -begin
1.239 -
1.240 -definition
1.241 -  "enum = List.product enum enum"
1.242 -
1.243 -definition
1.244 -  "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
1.245 -
1.246 -definition
1.247 -  "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
1.248 -
1.249 -
1.250 -instance by default
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 -instantiation sum :: (enum, enum) enum
1.257 -begin
1.258 -
1.259 -definition
1.260 -  "enum = map Inl enum @ map Inr enum"
1.261 -
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 -instantiation nibble :: enum
1.283 -begin
1.284 -
1.285 -definition
1.286 -  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
1.287 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
1.288 -
1.289 -definition
1.290 -  "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.291 -     \<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.292 -
1.293 -definition
1.294 -  "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.295 -     \<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.296 -
1.297 -instance proof
1.298 -  fix P
1.299 -  show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)"
1.300 -    unfolding enum_all_nibble_def
1.301 -    by (auto, case_tac x) auto
1.302 -next
1.303 -  fix P
1.304 -  show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)"
1.305 -    unfolding enum_ex_nibble_def
1.306 -    by (auto, case_tac x) auto
1.307 -qed (simp_all add: enum_nibble_def UNIV_nibble)
1.308 -
1.309 -end
1.310 -
1.311 -instantiation char :: enum
1.312 -begin
1.313 -
1.314 -definition
1.315 -  "enum = map (split Char) (List.product enum enum)"
1.316 -
1.317 -lemma enum_chars [code]:
1.318 -  "enum = chars"
1.319 -  unfolding enum_char_def chars_def enum_nibble_def by simp
1.320 -
1.321 -definition
1.322 -  "enum_all P = list_all P chars"
1.323 -
1.324 -definition
1.325 -  "enum_ex P = list_ex P chars"
1.326 -
1.327 -lemma set_enum_char: "set (enum :: char list) = UNIV"
1.328 -    by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric])
1.329 -
1.330 -instance proof
1.331 -  fix P
1.332 -  show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)"
1.333 -    unfolding enum_all_char_def enum_chars[symmetric]
1.334 -    by (auto simp add: list_all_iff set_enum_char)
1.335 -next
1.336 -  fix P
1.337 -  show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)"
1.338 -    unfolding enum_ex_char_def enum_chars[symmetric]
1.339 -    by (auto simp add: list_ex_iff set_enum_char)
1.340 -next
1.341 -  show "distinct (enum :: char list)"
1.342 -    by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct)
1.343 -qed (auto simp add: set_enum_char)
1.344 -
1.345 -end
1.346 -
1.347 -instantiation option :: (enum) enum
1.348 -begin
1.349 -
1.350 -definition
1.351 -  "enum = None # map Some enum"
1.352 -
1.353 -definition
1.354 -  "enum_all P = (P None \<and> enum_all (%x. P (Some x)))"
1.355 -
1.356 -definition
1.357 -  "enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))"
1.358 -
1.359 -instance proof
1.360 -  fix P
1.361 -  show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)"
1.362 -    unfolding enum_all_option_def enum_all
1.363 -    by (auto, case_tac x) auto
1.364 -next
1.365 -  fix P
1.366 -  show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)"
1.367 -    unfolding enum_ex_option_def enum_ex
1.368 -    by (auto, case_tac x) auto
1.369 -qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
1.370 -end
1.371 +  by (simp only: enum_ex_fun_def Let_def)
1.372
1.373  instantiation set :: (enum) enum
1.374  begin
1.375 @@ -503,6 +334,133 @@
1.376
1.377  end
1.378
1.379 +instantiation unit :: enum
1.380 +begin
1.381 +
1.382 +definition
1.383 +  "enum = [()]"
1.384 +
1.385 +definition
1.386 +  "enum_all P = P ()"
1.387 +
1.388 +definition
1.389 +  "enum_ex P = P ()"
1.390 +
1.391 +instance proof
1.392 +qed (auto simp add: enum_unit_def enum_all_unit_def enum_ex_unit_def)
1.393 +
1.394 +end
1.395 +
1.396 +instantiation bool :: enum
1.397 +begin
1.398 +
1.399 +definition
1.400 +  "enum = [False, True]"
1.401 +
1.402 +definition
1.403 +  "enum_all P \<longleftrightarrow> P False \<and> P True"
1.404 +
1.405 +definition
1.406 +  "enum_ex P \<longleftrightarrow> P False \<or> P True"
1.407 +
1.408 +instance proof
1.409 +qed (simp_all only: enum_bool_def enum_all_bool_def enum_ex_bool_def UNIV_bool, simp_all)
1.410 +
1.411 +end
1.412 +
1.413 +instantiation prod :: (enum, enum) enum
1.414 +begin
1.415 +
1.416 +definition
1.417 +  "enum = List.product enum enum"
1.418 +
1.419 +definition
1.420 +  "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
1.421 +
1.422 +definition
1.423 +  "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
1.424 +
1.425 +
1.426 +instance by default
1.427 +  (simp_all add: enum_prod_def product_list_set distinct_product
1.428 +    enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
1.429 +
1.430 +end
1.431 +
1.432 +instantiation sum :: (enum, enum) enum
1.433 +begin
1.434 +
1.435 +definition
1.436 +  "enum = map Inl enum @ map Inr enum"
1.437 +
1.438 +definition
1.439 +  "enum_all P \<longleftrightarrow> enum_all (\<lambda>x. P (Inl x)) \<and> enum_all (\<lambda>x. P (Inr x))"
1.440 +
1.441 +definition
1.442 +  "enum_ex P \<longleftrightarrow> enum_ex (\<lambda>x. P (Inl x)) \<or> enum_ex (\<lambda>x. P (Inr x))"
1.443 +
1.444 +instance proof
1.445 +qed (simp_all only: enum_sum_def enum_all_sum_def enum_ex_sum_def UNIV_sum,
1.446 +  auto simp add: enum_UNIV distinct_map enum_distinct)
1.447 +
1.448 +end
1.449 +
1.450 +instantiation nibble :: enum
1.451 +begin
1.452 +
1.453 +definition
1.454 +  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
1.455 +    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
1.456 +
1.457 +definition
1.458 +  "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
1.459 +     \<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.460 +
1.461 +definition
1.462 +  "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
1.463 +     \<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.464 +
1.465 +instance proof
1.466 +qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
1.467 +
1.468 +end
1.469 +
1.470 +instantiation char :: enum
1.471 +begin
1.472 +
1.473 +definition
1.474 +  "enum = chars"
1.475 +
1.476 +definition
1.477 +  "enum_all P \<longleftrightarrow> list_all P chars"
1.478 +
1.479 +definition
1.480 +  "enum_ex P \<longleftrightarrow> list_ex P chars"
1.481 +
1.482 +instance proof
1.483 +qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
1.484 +  simp_all add: list_all_iff list_ex_iff)
1.485 +
1.486 +end
1.487 +
1.488 +instantiation option :: (enum) enum
1.489 +begin
1.490 +
1.491 +definition
1.492 +  "enum = None # map Some enum"
1.493 +
1.494 +definition
1.495 +  "enum_all P \<longleftrightarrow> P None \<and> enum_all (\<lambda>x. P (Some x))"
1.496 +
1.497 +definition
1.498 +  "enum_ex P \<longleftrightarrow> P None \<or> enum_ex (\<lambda>x. P (Some x))"
1.499 +
1.500 +instance proof
1.501 +qed (simp_all only: enum_option_def enum_all_option_def enum_ex_option_def UNIV_option_conv,
1.502 +  auto simp add: distinct_map enum_UNIV enum_distinct)
1.503 +
1.504 +end
1.505 +
1.506
1.507  subsection {* Small finite types *}
1.508
1.509 @@ -512,6 +470,10 @@
1.510
1.511  notation (output) a\<^isub>1  ("a\<^isub>1")
1.512
1.513 +lemma UNIV_finite_1:
1.514 +  "UNIV = {a\<^isub>1}"
1.515 +  by (auto intro: finite_1.exhaust)
1.516 +
1.517  instantiation finite_1 :: enum
1.518  begin
1.519
1.520 @@ -525,29 +487,20 @@
1.521    "enum_ex P = P a\<^isub>1"
1.522
1.523  instance proof
1.524 -  fix P
1.525 -  show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)"
1.526 -    unfolding enum_all_finite_1_def
1.527 -    by (auto, case_tac x) auto
1.528 -next
1.529 -  fix P
1.530 -  show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)"
1.531 -    unfolding enum_ex_finite_1_def
1.532 -    by (auto, case_tac x) auto
1.533 -qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
1.534 +qed (simp_all only: enum_finite_1_def enum_all_finite_1_def enum_ex_finite_1_def UNIV_finite_1, simp_all)
1.535
1.536  end
1.537
1.538  instantiation finite_1 :: linorder
1.539  begin
1.540
1.541 +definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
1.542 +where
1.543 +  "x < (y :: finite_1) \<longleftrightarrow> False"
1.544 +
1.545  definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
1.546  where
1.547 -  "less_eq_finite_1 x y = True"
1.548 -
1.549 -definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
1.550 -where
1.551 -  "less_finite_1 x y = False"
1.552 +  "x \<le> (y :: finite_1) \<longleftrightarrow> True"
1.553
1.554  instance
1.555  apply (intro_classes)
1.556 @@ -564,6 +517,10 @@
1.557  notation (output) a\<^isub>1  ("a\<^isub>1")
1.558  notation (output) a\<^isub>2  ("a\<^isub>2")
1.559
1.560 +lemma UNIV_finite_2:
1.561 +  "UNIV = {a\<^isub>1, a\<^isub>2}"
1.562 +  by (auto intro: finite_2.exhaust)
1.563 +
1.564  instantiation finite_2 :: enum
1.565  begin
1.566
1.567 @@ -571,22 +528,13 @@
1.568    "enum = [a\<^isub>1, a\<^isub>2]"
1.569
1.570  definition
1.571 -  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)"
1.572 +  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2"
1.573
1.574  definition
1.575 -  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)"
1.576 +  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2"
1.577
1.578  instance proof
1.579 -  fix P
1.580 -  show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)"
1.581 -    unfolding enum_all_finite_2_def
1.582 -    by (auto, case_tac x) auto
1.583 -next
1.584 -  fix P
1.585 -  show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)"
1.586 -    unfolding enum_ex_finite_2_def
1.587 -    by (auto, case_tac x) auto
1.588 -qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
1.589 +qed (simp_all only: enum_finite_2_def enum_all_finite_2_def enum_ex_finite_2_def UNIV_finite_2, simp_all)
1.590
1.591  end
1.592
1.593 @@ -595,30 +543,32 @@
1.594
1.595  definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
1.596  where
1.597 -  "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
1.598 +  "x < y \<longleftrightarrow> x = a\<^isub>1 \<and> y = a\<^isub>2"
1.599
1.600  definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
1.601  where
1.602 -  "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
1.603 -
1.604 +  "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_2)"
1.605
1.606  instance
1.607  apply (intro_classes)
1.608  apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
1.609 -apply (metis finite_2.distinct finite_2.nchotomy)+
1.610 +apply (metis finite_2.nchotomy)+
1.611  done
1.612
1.613  end
1.614
1.615  hide_const (open) a\<^isub>1 a\<^isub>2
1.616
1.617 -
1.618  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
1.619
1.620  notation (output) a\<^isub>1  ("a\<^isub>1")
1.621  notation (output) a\<^isub>2  ("a\<^isub>2")
1.622  notation (output) a\<^isub>3  ("a\<^isub>3")
1.623
1.624 +lemma UNIV_finite_3:
1.625 +  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3}"
1.626 +  by (auto intro: finite_3.exhaust)
1.627 +
1.628  instantiation finite_3 :: enum
1.629  begin
1.630
1.631 @@ -626,22 +576,13 @@
1.632    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
1.633
1.634  definition
1.635 -  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)"
1.636 +  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3"
1.637
1.638  definition
1.639 -  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)"
1.640 +  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3"
1.641
1.642  instance proof
1.643 -  fix P
1.644 -  show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)"
1.645 -    unfolding enum_all_finite_3_def
1.646 -    by (auto, case_tac x) auto
1.647 -next
1.648 -  fix P
1.649 -  show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)"
1.650 -    unfolding enum_ex_finite_3_def
1.651 -    by (auto, case_tac x) auto
1.652 -qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
1.653 +qed (simp_all only: enum_finite_3_def enum_all_finite_3_def enum_ex_finite_3_def UNIV_finite_3, simp_all)
1.654
1.655  end
1.656
1.657 @@ -650,13 +591,11 @@
1.658
1.659  definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
1.660  where
1.661 -  "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
1.662 -     | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
1.663 +  "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)"
1.664
1.665  definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
1.666  where
1.667 -  "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
1.668 -
1.669 +  "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_3)"
1.670
1.671  instance proof (intro_classes)
1.672  qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
1.673 @@ -665,7 +604,6 @@
1.674
1.675  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
1.676
1.677 -
1.678  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
1.679
1.680  notation (output) a\<^isub>1  ("a\<^isub>1")
1.681 @@ -673,6 +611,10 @@
1.682  notation (output) a\<^isub>3  ("a\<^isub>3")
1.683  notation (output) a\<^isub>4  ("a\<^isub>4")
1.684
1.685 +lemma UNIV_finite_4:
1.686 +  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4}"
1.687 +  by (auto intro: finite_4.exhaust)
1.688 +
1.689  instantiation finite_4 :: enum
1.690  begin
1.691
1.692 @@ -680,22 +622,13 @@
1.693    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
1.694
1.695  definition
1.696 -  "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)"
1.697 +  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4"
1.698
1.699  definition
1.700 -  "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)"
1.701 +  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4"
1.702
1.703  instance proof
1.704 -  fix P
1.705 -  show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)"
1.706 -    unfolding enum_all_finite_4_def
1.707 -    by (auto, case_tac x) auto
1.708 -next
1.709 -  fix P
1.710 -  show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)"
1.711 -    unfolding enum_ex_finite_4_def
1.712 -    by (auto, case_tac x) auto
1.713 -qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
1.714 +qed (simp_all only: enum_finite_4_def enum_all_finite_4_def enum_ex_finite_4_def UNIV_finite_4, simp_all)
1.715
1.716  end
1.717
1.718 @@ -710,6 +643,10 @@
1.719  notation (output) a\<^isub>4  ("a\<^isub>4")
1.720  notation (output) a\<^isub>5  ("a\<^isub>5")
1.721
1.722 +lemma UNIV_finite_5:
1.723 +  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5}"
1.724 +  by (auto intro: finite_5.exhaust)
1.725 +
1.726  instantiation finite_5 :: enum
1.727  begin
1.728
1.729 @@ -717,22 +654,13 @@
1.730    "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
1.731
1.732  definition
1.733 -  "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.734 +  "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"
1.735
1.736  definition
1.737 -  "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.738 +  "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"
1.739
1.740  instance proof
1.741 -  fix P
1.742 -  show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)"
1.743 -    unfolding enum_all_finite_5_def
1.744 -    by (auto, case_tac x) auto
1.745 -next
1.746 -  fix P
1.747 -  show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)"
1.748 -    unfolding enum_ex_finite_5_def
1.749 -    by (auto, case_tac x) auto
1.750 -qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
1.751 +qed (simp_all only: enum_finite_5_def enum_all_finite_5_def enum_ex_finite_5_def UNIV_finite_5, simp_all)
1.752
1.753  end
1.754
```