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.21 +qed (simp add: UNIV_enum)
    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