src/HOL/Enum.thy
changeset 49948 744934b818c7
parent 48123 104e5fccea12
child 49949 be3dd2e602e8
     1.1 --- a/src/HOL/Enum.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -74,61 +74,11 @@
     1.4    by (simp add: enum_ex)
     1.5  
     1.6  lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
     1.7 -unfolding list_ex1_iff enum_UNIV by auto
     1.8 +  by (auto simp add: enum_UNIV list_ex1_iff)
     1.9  
    1.10  
    1.11  subsection {* Default instances *}
    1.12  
    1.13 -primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    1.14 -  "n_lists 0 xs = [[]]"
    1.15 -  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    1.16 -
    1.17 -lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    1.18 -  by (induct n) simp_all
    1.19 -
    1.20 -lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    1.21 -  by (induct n) (auto simp add: length_concat o_def listsum_triv)
    1.22 -
    1.23 -lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    1.24 -  by (induct n arbitrary: ys) auto
    1.25 -
    1.26 -lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    1.27 -proof (rule set_eqI)
    1.28 -  fix ys :: "'a list"
    1.29 -  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    1.30 -  proof -
    1.31 -    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    1.32 -      by (induct n arbitrary: ys) auto
    1.33 -    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
    1.34 -      by (induct n arbitrary: ys) auto
    1.35 -    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
    1.36 -      by (induct ys) auto
    1.37 -    ultimately show ?thesis by auto
    1.38 -  qed
    1.39 -qed
    1.40 -
    1.41 -lemma distinct_n_lists:
    1.42 -  assumes "distinct xs"
    1.43 -  shows "distinct (n_lists n xs)"
    1.44 -proof (rule card_distinct)
    1.45 -  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
    1.46 -  have "card (set (n_lists n xs)) = card (set xs) ^ n"
    1.47 -  proof (induct n)
    1.48 -    case 0 then show ?case by simp
    1.49 -  next
    1.50 -    case (Suc n)
    1.51 -    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
    1.52 -      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
    1.53 -      by (rule card_UN_disjoint) auto
    1.54 -    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
    1.55 -      by (rule card_image) (simp add: inj_on_def)
    1.56 -    ultimately show ?case by auto
    1.57 -  qed
    1.58 -  also have "\<dots> = length xs ^ n" by (simp add: card_length)
    1.59 -  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
    1.60 -    by (simp add: length_n_lists)
    1.61 -qed
    1.62 -
    1.63  lemma map_of_zip_enum_is_Some:
    1.64    assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
    1.65    shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
    1.66 @@ -164,7 +114,7 @@
    1.67  definition
    1.68    all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
    1.69  where
    1.70 -  "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
    1.71 +  "all_n_lists P n = (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
    1.72  
    1.73  lemma [code]:
    1.74    "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
    1.75 @@ -174,7 +124,7 @@
    1.76  definition
    1.77    ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
    1.78  where
    1.79 -  "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
    1.80 +  "ex_n_lists P n = (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
    1.81  
    1.82  lemma [code]:
    1.83    "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
    1.84 @@ -186,7 +136,7 @@
    1.85  begin
    1.86  
    1.87  definition
    1.88 -  "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.89 +  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (List.n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
    1.90  
    1.91  definition
    1.92    "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
    1.93 @@ -258,7 +208,7 @@
    1.94  end
    1.95  
    1.96  lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
    1.97 -  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
    1.98 +  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
    1.99    by (simp add: enum_fun_def Let_def)
   1.100  
   1.101  lemma enum_all_fun_code [code]:
   1.102 @@ -312,25 +262,11 @@
   1.103  
   1.104  end
   1.105  
   1.106 -primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   1.107 -  "product [] _ = []"
   1.108 -  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   1.109 -
   1.110 -lemma product_list_set:
   1.111 -  "set (product xs ys) = set xs \<times> set ys"
   1.112 -  by (induct xs) auto
   1.113 -
   1.114 -lemma distinct_product:
   1.115 -  assumes "distinct xs" and "distinct ys"
   1.116 -  shows "distinct (product xs ys)"
   1.117 -  using assms by (induct xs)
   1.118 -    (auto intro: inj_onI simp add: product_list_set distinct_map)
   1.119 -
   1.120  instantiation prod :: (enum, enum) enum
   1.121  begin
   1.122  
   1.123  definition
   1.124 -  "enum = product enum enum"
   1.125 +  "enum = List.product enum enum"
   1.126  
   1.127  definition
   1.128    "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
   1.129 @@ -404,7 +340,7 @@
   1.130  begin
   1.131  
   1.132  definition
   1.133 -  "enum = map (split Char) (product enum enum)"
   1.134 +  "enum = map (split Char) (List.product enum enum)"
   1.135  
   1.136  lemma enum_chars [code]:
   1.137    "enum = chars"
   1.138 @@ -461,37 +397,6 @@
   1.139  qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
   1.140  end
   1.141  
   1.142 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   1.143 -  "sublists [] = [[]]"
   1.144 -  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   1.145 -
   1.146 -lemma length_sublists:
   1.147 -  "length (sublists xs) = 2 ^ length xs"
   1.148 -  by (induct xs) (simp_all add: Let_def)
   1.149 -
   1.150 -lemma sublists_powset:
   1.151 -  "set ` set (sublists xs) = Pow (set xs)"
   1.152 -proof -
   1.153 -  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   1.154 -    by (auto simp add: image_def)
   1.155 -  have "set (map set (sublists xs)) = Pow (set xs)"
   1.156 -    by (induct xs)
   1.157 -      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   1.158 -  then show ?thesis by simp
   1.159 -qed
   1.160 -
   1.161 -lemma distinct_set_sublists:
   1.162 -  assumes "distinct xs"
   1.163 -  shows "distinct (map set (sublists xs))"
   1.164 -proof (rule card_distinct)
   1.165 -  have "finite (set xs)" by rule
   1.166 -  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   1.167 -  with assms distinct_card [of xs]
   1.168 -    have "card (Pow (set xs)) = 2 ^ length xs" by simp
   1.169 -  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   1.170 -    by (simp add: sublists_powset length_sublists)
   1.171 -qed
   1.172 -
   1.173  instantiation set :: (enum) enum
   1.174  begin
   1.175  
   1.176 @@ -745,10 +650,11 @@
   1.177  
   1.178  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   1.179  
   1.180 +
   1.181  subsection {* An executable THE operator on finite types *}
   1.182  
   1.183  definition
   1.184 -  [code del]: "enum_the P = The P"
   1.185 +  [code del]: "enum_the = The"
   1.186  
   1.187  lemma [code]:
   1.188    "The P = (case filter P enum of [x] => x | _ => enum_the P)"
   1.189 @@ -782,9 +688,10 @@
   1.190  code_abort enum_the
   1.191  code_const enum_the (Eval "(fn p => raise Match)")
   1.192  
   1.193 +
   1.194  subsection {* Further operations on finite types *}
   1.195  
   1.196 -lemma Collect_code[code]:
   1.197 +lemma Collect_code [code]:
   1.198    "Collect P = set (filter P enum)"
   1.199  by (auto simp add: enum_UNIV)
   1.200  
   1.201 @@ -796,11 +703,11 @@
   1.202    "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
   1.203  by (simp add: trancl_def)
   1.204  
   1.205 -lemma rtranclp_rtrancl_eq[code, no_atp]:
   1.206 +lemma rtranclp_rtrancl_eq [code, no_atp]:
   1.207    "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
   1.208  unfolding rtrancl_def by auto
   1.209  
   1.210 -lemma max_ext_eq[code]:
   1.211 +lemma max_ext_eq [code]:
   1.212    "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
   1.213  by (auto simp add: max_ext.simps)
   1.214  
   1.215 @@ -813,157 +720,26 @@
   1.216  unfolding mlex_prod_def by auto
   1.217  
   1.218  subsection {* Executable accessible part *}
   1.219 -(* FIXME: should be moved somewhere else !? *)
   1.220 -
   1.221 -subsubsection {* Finite monotone eventually stable sequences *}
   1.222 -
   1.223 -lemma finite_mono_remains_stable_implies_strict_prefix:
   1.224 -  fixes f :: "nat \<Rightarrow> 'a::order"
   1.225 -  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
   1.226 -  shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   1.227 -  using assms
   1.228 -proof -
   1.229 -  have "\<exists>n. f n = f (Suc n)"
   1.230 -  proof (rule ccontr)
   1.231 -    assume "\<not> ?thesis"
   1.232 -    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
   1.233 -    then have "\<And>n. f n < f (Suc n)"
   1.234 -      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
   1.235 -    with lift_Suc_mono_less_iff[of f]
   1.236 -    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
   1.237 -    then have "inj f"
   1.238 -      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
   1.239 -    with `finite (range f)` have "finite (UNIV::nat set)"
   1.240 -      by (rule finite_imageD)
   1.241 -    then show False by simp
   1.242 -  qed
   1.243 -  then obtain n where n: "f n = f (Suc n)" ..
   1.244 -  def N \<equiv> "LEAST n. f n = f (Suc n)"
   1.245 -  have N: "f N = f (Suc N)"
   1.246 -    unfolding N_def using n by (rule LeastI)
   1.247 -  show ?thesis
   1.248 -  proof (intro exI[of _ N] conjI allI impI)
   1.249 -    fix n assume "N \<le> n"
   1.250 -    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
   1.251 -    proof (induct rule: dec_induct)
   1.252 -      case (step n) then show ?case
   1.253 -        using eq[rule_format, of "n - 1"] N
   1.254 -        by (cases n) (auto simp add: le_Suc_eq)
   1.255 -    qed simp
   1.256 -    from this[of n] `N \<le> n` show "f N = f n" by auto
   1.257 -  next
   1.258 -    fix n m :: nat assume "m < n" "n \<le> N"
   1.259 -    then show "f m < f n"
   1.260 -    proof (induct rule: less_Suc_induct[consumes 1])
   1.261 -      case (1 i)
   1.262 -      then have "i < N" by simp
   1.263 -      then have "f i \<noteq> f (Suc i)"
   1.264 -        unfolding N_def by (rule not_less_Least)
   1.265 -      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
   1.266 -    qed auto
   1.267 -  qed
   1.268 -qed
   1.269 -
   1.270 -lemma finite_mono_strict_prefix_implies_finite_fixpoint:
   1.271 -  fixes f :: "nat \<Rightarrow> 'a set"
   1.272 -  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
   1.273 -    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   1.274 -  shows "f (card S) = (\<Union>n. f n)"
   1.275 -proof -
   1.276 -  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
   1.277 -
   1.278 -  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
   1.279 -    proof (induct i)
   1.280 -      case 0 then show ?case by simp
   1.281 -    next
   1.282 -      case (Suc i)
   1.283 -      with inj[rule_format, of "Suc i" i]
   1.284 -      have "(f i) \<subset> (f (Suc i))" by auto
   1.285 -      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
   1.286 -      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
   1.287 -      with Suc show ?case using inj by auto
   1.288 -    qed
   1.289 -  }
   1.290 -  then have "N \<le> card (f N)" by simp
   1.291 -  also have "\<dots> \<le> card S" using S by (intro card_mono)
   1.292 -  finally have "f (card S) = f N" using eq by auto
   1.293 -  then show ?thesis using eq inj[rule_format, of N]
   1.294 -    apply auto
   1.295 -    apply (case_tac "n < N")
   1.296 -    apply (auto simp: not_less)
   1.297 -    done
   1.298 -qed
   1.299 -
   1.300 -subsubsection {* Bounded accessible part *}
   1.301 -
   1.302 -fun bacc :: "('a * 'a) set => nat => 'a set" 
   1.303 -where
   1.304 -  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
   1.305 -| "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
   1.306 -
   1.307 -lemma bacc_subseteq_acc:
   1.308 -  "bacc r n \<subseteq> acc r"
   1.309 -by (induct n) (auto intro: acc.intros)
   1.310 -
   1.311 -lemma bacc_mono:
   1.312 -  "n <= m ==> bacc r n \<subseteq> bacc r m"
   1.313 -by (induct rule: dec_induct) auto
   1.314 -  
   1.315 -lemma bacc_upper_bound:
   1.316 -  "bacc (r :: ('a * 'a) set)  (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
   1.317 -proof -
   1.318 -  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
   1.319 -  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
   1.320 -  moreover have "finite (range (bacc r))" by auto
   1.321 -  ultimately show ?thesis
   1.322 -   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
   1.323 -     (auto intro: finite_mono_remains_stable_implies_strict_prefix  simp add: enum_UNIV)
   1.324 -qed
   1.325 -
   1.326 -lemma acc_subseteq_bacc:
   1.327 -  assumes "finite r"
   1.328 -  shows "acc r \<subseteq> (UN n. bacc r n)"
   1.329 -proof
   1.330 -  fix x
   1.331 -  assume "x : acc r"
   1.332 -  then have "\<exists> n. x : bacc r n"
   1.333 -  proof (induct x arbitrary: rule: acc.induct)
   1.334 -    case (accI x)
   1.335 -    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
   1.336 -    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
   1.337 -    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
   1.338 -    proof
   1.339 -      fix y assume y: "(y, x) : r"
   1.340 -      with n have "y : bacc r (n y)" by auto
   1.341 -      moreover have "n y <= Max ((%(y, x). n y) ` r)"
   1.342 -        using y `finite r` by (auto intro!: Max_ge)
   1.343 -      note bacc_mono[OF this, of r]
   1.344 -      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
   1.345 -    qed
   1.346 -    then show ?case
   1.347 -      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   1.348 -  qed
   1.349 -  then show "x : (UN n. bacc r n)" by auto
   1.350 -qed
   1.351 -
   1.352 -lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
   1.353 -by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
   1.354  
   1.355  definition 
   1.356    [code del]: "card_UNIV = card UNIV"
   1.357  
   1.358  lemma [code]:
   1.359    "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
   1.360 -unfolding card_UNIV_def enum_UNIV ..
   1.361 +  unfolding card_UNIV_def enum_UNIV ..
   1.362  
   1.363 -declare acc_bacc_eq[folded card_UNIV_def, code]
   1.364 +lemma [code]:
   1.365 +  fixes xs :: "('a::finite \<times> 'a) list"
   1.366 +  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
   1.367 +  by (simp add: card_UNIV_def acc_bacc_eq)
   1.368  
   1.369 -lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
   1.370 -unfolding acc_def by simp
   1.371 +lemma [code_unfold]: "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
   1.372 +  unfolding acc_def by simp
   1.373  
   1.374  subsection {* Closing up *}
   1.375  
   1.376  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
   1.377 -hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
   1.378 +hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
   1.379  
   1.380  end
   1.381 +