tailored enum specification towards simple instantiation;
authorhaftmann
Sat Oct 20 10:00:21 2012 +0200 (2012-10-20)
changeset 49950cd882d53ba6b
parent 49949 be3dd2e602e8
child 49951 119440fe1d5c
tailored enum specification towards simple instantiation;
tuned enum instantiations
src/HOL/Enum.thy
     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.19  qed (simp add: UNIV_enum)
    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