src/HOL/Enum.thy
 changeset 40649 dc1b5aa908ff parent 40647 6e92ca8e981b child 40650 d40b347d5b0b
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:55 2010 +0100
1.3 @@ -0,0 +1,379 @@
1.4 +(* Author: Florian Haftmann, TU Muenchen *)
1.5 +
1.6 +header {* Finite types as explicit enumerations *}
1.7 +
1.8 +theory Enum
1.9 +imports Map Main
1.10 +begin
1.11 +
1.12 +subsection {* Class @{text enum} *}
1.13 +
1.14 +class enum =
1.15 +  fixes enum :: "'a list"
1.16 +  assumes UNIV_enum: "UNIV = set enum"
1.17 +    and enum_distinct: "distinct enum"
1.18 +begin
1.19 +
1.20 +subclass finite proof
1.22 +
1.23 +lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
1.24 +
1.25 +lemma in_enum [intro]: "x \<in> set enum"
1.26 +  unfolding enum_all by auto
1.27 +
1.28 +lemma enum_eq_I:
1.29 +  assumes "\<And>x. x \<in> set xs"
1.30 +  shows "set enum = set xs"
1.31 +proof -
1.32 +  from assms UNIV_eq_I have "UNIV = set xs" by auto
1.33 +  with enum_all show ?thesis by simp
1.34 +qed
1.35 +
1.36 +end
1.37 +
1.38 +
1.39 +subsection {* Equality and order on functions *}
1.40 +
1.41 +instantiation "fun" :: (enum, equal) equal
1.42 +begin
1.43 +
1.44 +definition
1.45 +  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
1.46 +
1.47 +instance proof
1.48 +qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
1.49 +
1.50 +end
1.51 +
1.52 +lemma [code nbe]:
1.53 +  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
1.54 +  by (fact equal_refl)
1.55 +
1.56 +lemma order_fun [code]:
1.57 +  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
1.58 +  shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
1.59 +    and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
1.60 +  by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
1.61 +
1.62 +
1.63 +subsection {* Quantifiers *}
1.64 +
1.65 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
1.66 +  by (simp add: list_all_iff enum_all)
1.67 +
1.68 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
1.69 +  by (simp add: list_ex_iff enum_all)
1.70 +
1.71 +
1.72 +subsection {* Default instances *}
1.73 +
1.74 +primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
1.75 +  "n_lists 0 xs = [[]]"
1.76 +  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
1.77 +
1.78 +lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
1.79 +  by (induct n) simp_all
1.80 +
1.81 +lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
1.82 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
1.83 +
1.84 +lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
1.85 +  by (induct n arbitrary: ys) auto
1.86 +
1.87 +lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
1.88 +proof (rule set_eqI)
1.89 +  fix ys :: "'a list"
1.90 +  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
1.91 +  proof -
1.92 +    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
1.93 +      by (induct n arbitrary: ys) auto
1.94 +    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
1.95 +      by (induct n arbitrary: ys) auto
1.96 +    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
1.97 +      by (induct ys) auto
1.98 +    ultimately show ?thesis by auto
1.99 +  qed
1.100 +qed
1.101 +
1.102 +lemma distinct_n_lists:
1.103 +  assumes "distinct xs"
1.104 +  shows "distinct (n_lists n xs)"
1.105 +proof (rule card_distinct)
1.106 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
1.107 +  have "card (set (n_lists n xs)) = card (set xs) ^ n"
1.108 +  proof (induct n)
1.109 +    case 0 then show ?case by simp
1.110 +  next
1.111 +    case (Suc n)
1.112 +    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
1.113 +      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
1.114 +      by (rule card_UN_disjoint) auto
1.115 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
1.116 +      by (rule card_image) (simp add: inj_on_def)
1.117 +    ultimately show ?case by auto
1.118 +  qed
1.119 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
1.120 +  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
1.121 +    by (simp add: length_n_lists)
1.122 +qed
1.123 +
1.124 +lemma map_of_zip_enum_is_Some:
1.125 +  assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
1.126 +  shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
1.127 +proof -
1.128 +  from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
1.129 +    (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
1.130 +    by (auto intro!: map_of_zip_is_Some)
1.131 +  then show ?thesis using enum_all by auto
1.132 +qed
1.133 +
1.134 +lemma map_of_zip_enum_inject:
1.135 +  fixes xs ys :: "'b\<Colon>enum list"
1.136 +  assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
1.137 +      "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
1.138 +    and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
1.139 +  shows "xs = ys"
1.140 +proof -
1.141 +  have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
1.142 +  proof
1.143 +    fix x :: 'a
1.144 +    from length map_of_zip_enum_is_Some obtain y1 y2
1.145 +      where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
1.146 +        and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
1.147 +    moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
1.148 +      by (auto dest: fun_cong)
1.149 +    ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
1.150 +      by simp
1.151 +  qed
1.152 +  with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
1.153 +qed
1.154 +
1.155 +instantiation "fun" :: (enum, enum) enum
1.156 +begin
1.157 +
1.158 +definition
1.159 +  "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.160 +
1.161 +instance proof
1.162 +  show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.163 +  proof (rule UNIV_eq_I)
1.164 +    fix f :: "'a \<Rightarrow> 'b"
1.165 +    have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
1.166 +      by (auto simp add: map_of_zip_map fun_eq_iff)
1.167 +    then show "f \<in> set enum"
1.168 +      by (auto simp add: enum_fun_def set_n_lists)
1.169 +  qed
1.170 +next
1.171 +  from map_of_zip_enum_inject
1.172 +  show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
1.173 +    by (auto intro!: inj_onI simp add: enum_fun_def
1.174 +      distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
1.175 +qed
1.176 +
1.177 +end
1.178 +
1.179 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
1.180 +  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
1.181 +  by (simp add: enum_fun_def Let_def)
1.182 +
1.183 +instantiation unit :: enum
1.184 +begin
1.185 +
1.186 +definition
1.187 +  "enum = [()]"
1.188 +
1.189 +instance proof
1.190 +qed (simp_all add: enum_unit_def UNIV_unit)
1.191 +
1.192 +end
1.193 +
1.194 +instantiation bool :: enum
1.195 +begin
1.196 +
1.197 +definition
1.198 +  "enum = [False, True]"
1.199 +
1.200 +instance proof
1.201 +qed (simp_all add: enum_bool_def UNIV_bool)
1.202 +
1.203 +end
1.204 +
1.205 +primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
1.206 +  "product [] _ = []"
1.207 +  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
1.208 +
1.209 +lemma product_list_set:
1.210 +  "set (product xs ys) = set xs \<times> set ys"
1.211 +  by (induct xs) auto
1.212 +
1.213 +lemma distinct_product:
1.214 +  assumes "distinct xs" and "distinct ys"
1.215 +  shows "distinct (product xs ys)"
1.216 +  using assms by (induct xs)
1.217 +    (auto intro: inj_onI simp add: product_list_set distinct_map)
1.218 +
1.219 +instantiation prod :: (enum, enum) enum
1.220 +begin
1.221 +
1.222 +definition
1.223 +  "enum = product enum enum"
1.224 +
1.225 +instance by default
1.226 +  (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
1.227 +
1.228 +end
1.229 +
1.230 +instantiation sum :: (enum, enum) enum
1.231 +begin
1.232 +
1.233 +definition
1.234 +  "enum = map Inl enum @ map Inr enum"
1.235 +
1.236 +instance by default
1.237 +  (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
1.238 +
1.239 +end
1.240 +
1.241 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
1.242 +  "sublists [] = [[]]"
1.243 +  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
1.244 +
1.245 +lemma length_sublists:
1.246 +  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
1.247 +  by (induct xs) (simp_all add: Let_def)
1.248 +
1.249 +lemma sublists_powset:
1.250 +  "set ` set (sublists xs) = Pow (set xs)"
1.251 +proof -
1.252 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
1.253 +    by (auto simp add: image_def)
1.254 +  have "set (map set (sublists xs)) = Pow (set xs)"
1.255 +    by (induct xs)
1.256 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
1.257 +  then show ?thesis by simp
1.258 +qed
1.259 +
1.260 +lemma distinct_set_sublists:
1.261 +  assumes "distinct xs"
1.262 +  shows "distinct (map set (sublists xs))"
1.263 +proof (rule card_distinct)
1.264 +  have "finite (set xs)" by rule
1.265 +  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
1.266 +  with assms distinct_card [of xs]
1.267 +    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
1.268 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
1.269 +    by (simp add: sublists_powset length_sublists)
1.270 +qed
1.271 +
1.272 +instantiation nibble :: enum
1.273 +begin
1.274 +
1.275 +definition
1.276 +  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
1.277 +    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
1.278 +
1.279 +instance proof
1.280 +qed (simp_all add: enum_nibble_def UNIV_nibble)
1.281 +
1.282 +end
1.283 +
1.284 +instantiation char :: enum
1.285 +begin
1.286 +
1.287 +definition
1.288 +  "enum = map (split Char) (product enum enum)"
1.289 +
1.290 +lemma enum_chars [code]:
1.291 +  "enum = chars"
1.292 +  unfolding enum_char_def chars_def enum_nibble_def by simp
1.293 +
1.294 +instance proof
1.295 +qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
1.296 +  distinct_map distinct_product enum_distinct)
1.297 +
1.298 +end
1.299 +
1.300 +instantiation option :: (enum) enum
1.301 +begin
1.302 +
1.303 +definition
1.304 +  "enum = None # map Some enum"
1.305 +
1.306 +instance proof
1.307 +qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
1.308 +
1.309 +end
1.310 +
1.311 +subsection {* Small finite types *}
1.312 +
1.313 +text {* We define small finite types for the use in Quickcheck *}
1.314 +
1.315 +datatype finite_1 = a\<^isub>1
1.316 +
1.317 +instantiation finite_1 :: enum
1.318 +begin
1.319 +
1.320 +definition
1.321 +  "enum = [a\<^isub>1]"
1.322 +
1.323 +instance proof
1.324 +qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
1.325 +
1.326 +end
1.327 +
1.328 +datatype finite_2 = a\<^isub>1 | a\<^isub>2
1.329 +
1.330 +instantiation finite_2 :: enum
1.331 +begin
1.332 +
1.333 +definition
1.334 +  "enum = [a\<^isub>1, a\<^isub>2]"
1.335 +
1.336 +instance proof
1.337 +qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
1.338 +
1.339 +end
1.340 +
1.341 +datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
1.342 +
1.343 +instantiation finite_3 :: enum
1.344 +begin
1.345 +
1.346 +definition
1.347 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
1.348 +
1.349 +instance proof
1.350 +qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
1.351 +
1.352 +end
1.353 +
1.354 +datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
1.355 +
1.356 +instantiation finite_4 :: enum
1.357 +begin
1.358 +
1.359 +definition
1.360 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
1.361 +
1.362 +instance proof
1.363 +qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
1.364 +
1.365 +end
1.366 +
1.367 +datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
1.368 +
1.369 +instantiation finite_5 :: enum
1.370 +begin
1.371 +
1.372 +definition
1.373 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
1.374 +
1.375 +instance proof
1.376 +qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
1.377 +
1.378 +end
1.379 +
1.380 +hide_type finite_1 finite_2 finite_3 finite_4 finite_5
1.381 +
1.382 +end
```