moved quite generic material from theory Enum to more appropriate places
authorhaftmann
Sat Oct 20 09:12:16 2012 +0200 (2012-10-20)
changeset 49948744934b818c7
parent 49947 29cd291bfea6
child 49949 be3dd2e602e8
moved quite generic material from theory Enum to more appropriate places
NEWS
src/HOL/Codegenerator_Test/RBT_Set_Test.thy
src/HOL/Enum.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/RBT_Set.thy
src/HOL/List.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/String.thy
src/HOL/Sum_Type.thy
     1.1 --- a/NEWS	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/NEWS	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -70,6 +70,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Moved operation product, sublists and n_lists from Enum.thy
     1.8 +to List.thy.  INCOMPATIBILITY.
     1.9 +
    1.10  * Simplified 'typedef' specifications: historical options for implicit
    1.11  set definition and alternative name have been discontinued.  The
    1.12  former behavior of "typedef (open) t = A" is now the default, but
     2.1 --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Sat Oct 20 09:09:37 2012 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Sat Oct 20 09:12:16 2012 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Test of the code generator using an implementation of sets by RBT trees *}
     2.5  
     2.6  theory RBT_Set_Test
     2.7 -imports Library "~~/src/HOL/Library/RBT_Set"
     2.8 +imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
     2.9  begin
    2.10  
    2.11  (* 
     3.1 --- a/src/HOL/Enum.thy	Sat Oct 20 09:09:37 2012 +0200
     3.2 +++ b/src/HOL/Enum.thy	Sat Oct 20 09:12:16 2012 +0200
     3.3 @@ -74,61 +74,11 @@
     3.4    by (simp add: enum_ex)
     3.5  
     3.6  lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
     3.7 -unfolding list_ex1_iff enum_UNIV by auto
     3.8 +  by (auto simp add: enum_UNIV list_ex1_iff)
     3.9  
    3.10  
    3.11  subsection {* Default instances *}
    3.12  
    3.13 -primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    3.14 -  "n_lists 0 xs = [[]]"
    3.15 -  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    3.16 -
    3.17 -lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    3.18 -  by (induct n) simp_all
    3.19 -
    3.20 -lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    3.21 -  by (induct n) (auto simp add: length_concat o_def listsum_triv)
    3.22 -
    3.23 -lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    3.24 -  by (induct n arbitrary: ys) auto
    3.25 -
    3.26 -lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    3.27 -proof (rule set_eqI)
    3.28 -  fix ys :: "'a list"
    3.29 -  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    3.30 -  proof -
    3.31 -    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    3.32 -      by (induct n arbitrary: ys) auto
    3.33 -    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
    3.34 -      by (induct n arbitrary: ys) auto
    3.35 -    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
    3.36 -      by (induct ys) auto
    3.37 -    ultimately show ?thesis by auto
    3.38 -  qed
    3.39 -qed
    3.40 -
    3.41 -lemma distinct_n_lists:
    3.42 -  assumes "distinct xs"
    3.43 -  shows "distinct (n_lists n xs)"
    3.44 -proof (rule card_distinct)
    3.45 -  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
    3.46 -  have "card (set (n_lists n xs)) = card (set xs) ^ n"
    3.47 -  proof (induct n)
    3.48 -    case 0 then show ?case by simp
    3.49 -  next
    3.50 -    case (Suc n)
    3.51 -    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
    3.52 -      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
    3.53 -      by (rule card_UN_disjoint) auto
    3.54 -    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
    3.55 -      by (rule card_image) (simp add: inj_on_def)
    3.56 -    ultimately show ?case by auto
    3.57 -  qed
    3.58 -  also have "\<dots> = length xs ^ n" by (simp add: card_length)
    3.59 -  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
    3.60 -    by (simp add: length_n_lists)
    3.61 -qed
    3.62 -
    3.63  lemma map_of_zip_enum_is_Some:
    3.64    assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
    3.65    shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
    3.66 @@ -164,7 +114,7 @@
    3.67  definition
    3.68    all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
    3.69  where
    3.70 -  "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
    3.71 +  "all_n_lists P n = (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
    3.72  
    3.73  lemma [code]:
    3.74    "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
    3.75 @@ -174,7 +124,7 @@
    3.76  definition
    3.77    ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
    3.78  where
    3.79 -  "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
    3.80 +  "ex_n_lists P n = (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
    3.81  
    3.82  lemma [code]:
    3.83    "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
    3.84 @@ -186,7 +136,7 @@
    3.85  begin
    3.86  
    3.87  definition
    3.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)"
    3.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)"
    3.90  
    3.91  definition
    3.92    "enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
    3.93 @@ -258,7 +208,7 @@
    3.94  end
    3.95  
    3.96  lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
    3.97 -  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
    3.98 +  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
    3.99    by (simp add: enum_fun_def Let_def)
   3.100  
   3.101  lemma enum_all_fun_code [code]:
   3.102 @@ -312,25 +262,11 @@
   3.103  
   3.104  end
   3.105  
   3.106 -primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   3.107 -  "product [] _ = []"
   3.108 -  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   3.109 -
   3.110 -lemma product_list_set:
   3.111 -  "set (product xs ys) = set xs \<times> set ys"
   3.112 -  by (induct xs) auto
   3.113 -
   3.114 -lemma distinct_product:
   3.115 -  assumes "distinct xs" and "distinct ys"
   3.116 -  shows "distinct (product xs ys)"
   3.117 -  using assms by (induct xs)
   3.118 -    (auto intro: inj_onI simp add: product_list_set distinct_map)
   3.119 -
   3.120  instantiation prod :: (enum, enum) enum
   3.121  begin
   3.122  
   3.123  definition
   3.124 -  "enum = product enum enum"
   3.125 +  "enum = List.product enum enum"
   3.126  
   3.127  definition
   3.128    "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
   3.129 @@ -404,7 +340,7 @@
   3.130  begin
   3.131  
   3.132  definition
   3.133 -  "enum = map (split Char) (product enum enum)"
   3.134 +  "enum = map (split Char) (List.product enum enum)"
   3.135  
   3.136  lemma enum_chars [code]:
   3.137    "enum = chars"
   3.138 @@ -461,37 +397,6 @@
   3.139  qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
   3.140  end
   3.141  
   3.142 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   3.143 -  "sublists [] = [[]]"
   3.144 -  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   3.145 -
   3.146 -lemma length_sublists:
   3.147 -  "length (sublists xs) = 2 ^ length xs"
   3.148 -  by (induct xs) (simp_all add: Let_def)
   3.149 -
   3.150 -lemma sublists_powset:
   3.151 -  "set ` set (sublists xs) = Pow (set xs)"
   3.152 -proof -
   3.153 -  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   3.154 -    by (auto simp add: image_def)
   3.155 -  have "set (map set (sublists xs)) = Pow (set xs)"
   3.156 -    by (induct xs)
   3.157 -      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   3.158 -  then show ?thesis by simp
   3.159 -qed
   3.160 -
   3.161 -lemma distinct_set_sublists:
   3.162 -  assumes "distinct xs"
   3.163 -  shows "distinct (map set (sublists xs))"
   3.164 -proof (rule card_distinct)
   3.165 -  have "finite (set xs)" by rule
   3.166 -  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   3.167 -  with assms distinct_card [of xs]
   3.168 -    have "card (Pow (set xs)) = 2 ^ length xs" by simp
   3.169 -  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   3.170 -    by (simp add: sublists_powset length_sublists)
   3.171 -qed
   3.172 -
   3.173  instantiation set :: (enum) enum
   3.174  begin
   3.175  
   3.176 @@ -745,10 +650,11 @@
   3.177  
   3.178  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   3.179  
   3.180 +
   3.181  subsection {* An executable THE operator on finite types *}
   3.182  
   3.183  definition
   3.184 -  [code del]: "enum_the P = The P"
   3.185 +  [code del]: "enum_the = The"
   3.186  
   3.187  lemma [code]:
   3.188    "The P = (case filter P enum of [x] => x | _ => enum_the P)"
   3.189 @@ -782,9 +688,10 @@
   3.190  code_abort enum_the
   3.191  code_const enum_the (Eval "(fn p => raise Match)")
   3.192  
   3.193 +
   3.194  subsection {* Further operations on finite types *}
   3.195  
   3.196 -lemma Collect_code[code]:
   3.197 +lemma Collect_code [code]:
   3.198    "Collect P = set (filter P enum)"
   3.199  by (auto simp add: enum_UNIV)
   3.200  
   3.201 @@ -796,11 +703,11 @@
   3.202    "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
   3.203  by (simp add: trancl_def)
   3.204  
   3.205 -lemma rtranclp_rtrancl_eq[code, no_atp]:
   3.206 +lemma rtranclp_rtrancl_eq [code, no_atp]:
   3.207    "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
   3.208  unfolding rtrancl_def by auto
   3.209  
   3.210 -lemma max_ext_eq[code]:
   3.211 +lemma max_ext_eq [code]:
   3.212    "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
   3.213  by (auto simp add: max_ext.simps)
   3.214  
   3.215 @@ -813,157 +720,26 @@
   3.216  unfolding mlex_prod_def by auto
   3.217  
   3.218  subsection {* Executable accessible part *}
   3.219 -(* FIXME: should be moved somewhere else !? *)
   3.220 -
   3.221 -subsubsection {* Finite monotone eventually stable sequences *}
   3.222 -
   3.223 -lemma finite_mono_remains_stable_implies_strict_prefix:
   3.224 -  fixes f :: "nat \<Rightarrow> 'a::order"
   3.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))"
   3.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)"
   3.227 -  using assms
   3.228 -proof -
   3.229 -  have "\<exists>n. f n = f (Suc n)"
   3.230 -  proof (rule ccontr)
   3.231 -    assume "\<not> ?thesis"
   3.232 -    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
   3.233 -    then have "\<And>n. f n < f (Suc n)"
   3.234 -      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
   3.235 -    with lift_Suc_mono_less_iff[of f]
   3.236 -    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
   3.237 -    then have "inj f"
   3.238 -      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
   3.239 -    with `finite (range f)` have "finite (UNIV::nat set)"
   3.240 -      by (rule finite_imageD)
   3.241 -    then show False by simp
   3.242 -  qed
   3.243 -  then obtain n where n: "f n = f (Suc n)" ..
   3.244 -  def N \<equiv> "LEAST n. f n = f (Suc n)"
   3.245 -  have N: "f N = f (Suc N)"
   3.246 -    unfolding N_def using n by (rule LeastI)
   3.247 -  show ?thesis
   3.248 -  proof (intro exI[of _ N] conjI allI impI)
   3.249 -    fix n assume "N \<le> n"
   3.250 -    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
   3.251 -    proof (induct rule: dec_induct)
   3.252 -      case (step n) then show ?case
   3.253 -        using eq[rule_format, of "n - 1"] N
   3.254 -        by (cases n) (auto simp add: le_Suc_eq)
   3.255 -    qed simp
   3.256 -    from this[of n] `N \<le> n` show "f N = f n" by auto
   3.257 -  next
   3.258 -    fix n m :: nat assume "m < n" "n \<le> N"
   3.259 -    then show "f m < f n"
   3.260 -    proof (induct rule: less_Suc_induct[consumes 1])
   3.261 -      case (1 i)
   3.262 -      then have "i < N" by simp
   3.263 -      then have "f i \<noteq> f (Suc i)"
   3.264 -        unfolding N_def by (rule not_less_Least)
   3.265 -      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
   3.266 -    qed auto
   3.267 -  qed
   3.268 -qed
   3.269 -
   3.270 -lemma finite_mono_strict_prefix_implies_finite_fixpoint:
   3.271 -  fixes f :: "nat \<Rightarrow> 'a set"
   3.272 -  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
   3.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)"
   3.274 -  shows "f (card S) = (\<Union>n. f n)"
   3.275 -proof -
   3.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
   3.277 -
   3.278 -  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
   3.279 -    proof (induct i)
   3.280 -      case 0 then show ?case by simp
   3.281 -    next
   3.282 -      case (Suc i)
   3.283 -      with inj[rule_format, of "Suc i" i]
   3.284 -      have "(f i) \<subset> (f (Suc i))" by auto
   3.285 -      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
   3.286 -      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
   3.287 -      with Suc show ?case using inj by auto
   3.288 -    qed
   3.289 -  }
   3.290 -  then have "N \<le> card (f N)" by simp
   3.291 -  also have "\<dots> \<le> card S" using S by (intro card_mono)
   3.292 -  finally have "f (card S) = f N" using eq by auto
   3.293 -  then show ?thesis using eq inj[rule_format, of N]
   3.294 -    apply auto
   3.295 -    apply (case_tac "n < N")
   3.296 -    apply (auto simp: not_less)
   3.297 -    done
   3.298 -qed
   3.299 -
   3.300 -subsubsection {* Bounded accessible part *}
   3.301 -
   3.302 -fun bacc :: "('a * 'a) set => nat => 'a set" 
   3.303 -where
   3.304 -  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
   3.305 -| "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
   3.306 -
   3.307 -lemma bacc_subseteq_acc:
   3.308 -  "bacc r n \<subseteq> acc r"
   3.309 -by (induct n) (auto intro: acc.intros)
   3.310 -
   3.311 -lemma bacc_mono:
   3.312 -  "n <= m ==> bacc r n \<subseteq> bacc r m"
   3.313 -by (induct rule: dec_induct) auto
   3.314 -  
   3.315 -lemma bacc_upper_bound:
   3.316 -  "bacc (r :: ('a * 'a) set)  (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
   3.317 -proof -
   3.318 -  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
   3.319 -  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
   3.320 -  moreover have "finite (range (bacc r))" by auto
   3.321 -  ultimately show ?thesis
   3.322 -   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
   3.323 -     (auto intro: finite_mono_remains_stable_implies_strict_prefix  simp add: enum_UNIV)
   3.324 -qed
   3.325 -
   3.326 -lemma acc_subseteq_bacc:
   3.327 -  assumes "finite r"
   3.328 -  shows "acc r \<subseteq> (UN n. bacc r n)"
   3.329 -proof
   3.330 -  fix x
   3.331 -  assume "x : acc r"
   3.332 -  then have "\<exists> n. x : bacc r n"
   3.333 -  proof (induct x arbitrary: rule: acc.induct)
   3.334 -    case (accI x)
   3.335 -    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
   3.336 -    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
   3.337 -    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
   3.338 -    proof
   3.339 -      fix y assume y: "(y, x) : r"
   3.340 -      with n have "y : bacc r (n y)" by auto
   3.341 -      moreover have "n y <= Max ((%(y, x). n y) ` r)"
   3.342 -        using y `finite r` by (auto intro!: Max_ge)
   3.343 -      note bacc_mono[OF this, of r]
   3.344 -      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
   3.345 -    qed
   3.346 -    then show ?case
   3.347 -      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   3.348 -  qed
   3.349 -  then show "x : (UN n. bacc r n)" by auto
   3.350 -qed
   3.351 -
   3.352 -lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
   3.353 -by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
   3.354  
   3.355  definition 
   3.356    [code del]: "card_UNIV = card UNIV"
   3.357  
   3.358  lemma [code]:
   3.359    "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
   3.360 -unfolding card_UNIV_def enum_UNIV ..
   3.361 +  unfolding card_UNIV_def enum_UNIV ..
   3.362  
   3.363 -declare acc_bacc_eq[folded card_UNIV_def, code]
   3.364 +lemma [code]:
   3.365 +  fixes xs :: "('a::finite \<times> 'a) list"
   3.366 +  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
   3.367 +  by (simp add: card_UNIV_def acc_bacc_eq)
   3.368  
   3.369 -lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
   3.370 -unfolding acc_def by simp
   3.371 +lemma [code_unfold]: "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
   3.372 +  unfolding acc_def by simp
   3.373  
   3.374  subsection {* Closing up *}
   3.375  
   3.376  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
   3.377 -hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
   3.378 +hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
   3.379  
   3.380  end
   3.381 +
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:09:37 2012 +0200
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:12:16 2012 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     4.5  
     4.6  theory Hilbert_Choice
     4.7 -imports Nat Wellfounded Plain
     4.8 +imports Nat Wellfounded Big_Operators
     4.9  keywords "specification" "ax_specification" :: thy_goal
    4.10  begin
    4.11  
    4.12 @@ -643,6 +643,144 @@
    4.13    done
    4.14  
    4.15  
    4.16 +subsection {* An aside: bounded accessible part *}
    4.17 +
    4.18 +text {* Finite monotone eventually stable sequences *}
    4.19 +
    4.20 +lemma finite_mono_remains_stable_implies_strict_prefix:
    4.21 +  fixes f :: "nat \<Rightarrow> 'a::order"
    4.22 +  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
    4.23 +  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)"
    4.24 +  using assms
    4.25 +proof -
    4.26 +  have "\<exists>n. f n = f (Suc n)"
    4.27 +  proof (rule ccontr)
    4.28 +    assume "\<not> ?thesis"
    4.29 +    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
    4.30 +    then have "\<And>n. f n < f (Suc n)"
    4.31 +      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
    4.32 +    with lift_Suc_mono_less_iff[of f]
    4.33 +    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
    4.34 +    then have "inj f"
    4.35 +      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
    4.36 +    with `finite (range f)` have "finite (UNIV::nat set)"
    4.37 +      by (rule finite_imageD)
    4.38 +    then show False by simp
    4.39 +  qed
    4.40 +  then obtain n where n: "f n = f (Suc n)" ..
    4.41 +  def N \<equiv> "LEAST n. f n = f (Suc n)"
    4.42 +  have N: "f N = f (Suc N)"
    4.43 +    unfolding N_def using n by (rule LeastI)
    4.44 +  show ?thesis
    4.45 +  proof (intro exI[of _ N] conjI allI impI)
    4.46 +    fix n assume "N \<le> n"
    4.47 +    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
    4.48 +    proof (induct rule: dec_induct)
    4.49 +      case (step n) then show ?case
    4.50 +        using eq[rule_format, of "n - 1"] N
    4.51 +        by (cases n) (auto simp add: le_Suc_eq)
    4.52 +    qed simp
    4.53 +    from this[of n] `N \<le> n` show "f N = f n" by auto
    4.54 +  next
    4.55 +    fix n m :: nat assume "m < n" "n \<le> N"
    4.56 +    then show "f m < f n"
    4.57 +    proof (induct rule: less_Suc_induct[consumes 1])
    4.58 +      case (1 i)
    4.59 +      then have "i < N" by simp
    4.60 +      then have "f i \<noteq> f (Suc i)"
    4.61 +        unfolding N_def by (rule not_less_Least)
    4.62 +      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
    4.63 +    qed auto
    4.64 +  qed
    4.65 +qed
    4.66 +
    4.67 +lemma finite_mono_strict_prefix_implies_finite_fixpoint:
    4.68 +  fixes f :: "nat \<Rightarrow> 'a set"
    4.69 +  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
    4.70 +    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)"
    4.71 +  shows "f (card S) = (\<Union>n. f n)"
    4.72 +proof -
    4.73 +  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
    4.74 +
    4.75 +  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
    4.76 +    proof (induct i)
    4.77 +      case 0 then show ?case by simp
    4.78 +    next
    4.79 +      case (Suc i)
    4.80 +      with inj[rule_format, of "Suc i" i]
    4.81 +      have "(f i) \<subset> (f (Suc i))" by auto
    4.82 +      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
    4.83 +      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
    4.84 +      with Suc show ?case using inj by auto
    4.85 +    qed
    4.86 +  }
    4.87 +  then have "N \<le> card (f N)" by simp
    4.88 +  also have "\<dots> \<le> card S" using S by (intro card_mono)
    4.89 +  finally have "f (card S) = f N" using eq by auto
    4.90 +  then show ?thesis using eq inj[rule_format, of N]
    4.91 +    apply auto
    4.92 +    apply (case_tac "n < N")
    4.93 +    apply (auto simp: not_less)
    4.94 +    done
    4.95 +qed
    4.96 +
    4.97 +primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set" 
    4.98 +where
    4.99 +  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
   4.100 +| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
   4.101 +
   4.102 +lemma bacc_subseteq_acc:
   4.103 +  "bacc r n \<subseteq> acc r"
   4.104 +  by (induct n) (auto intro: acc.intros)
   4.105 +
   4.106 +lemma bacc_mono:
   4.107 +  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
   4.108 +  by (induct rule: dec_induct) auto
   4.109 +  
   4.110 +lemma bacc_upper_bound:
   4.111 +  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
   4.112 +proof -
   4.113 +  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
   4.114 +  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
   4.115 +  moreover have "finite (range (bacc r))" by auto
   4.116 +  ultimately show ?thesis
   4.117 +   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
   4.118 +     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
   4.119 +qed
   4.120 +
   4.121 +lemma acc_subseteq_bacc:
   4.122 +  assumes "finite r"
   4.123 +  shows "acc r \<subseteq> (\<Union>n. bacc r n)"
   4.124 +proof
   4.125 +  fix x
   4.126 +  assume "x : acc r"
   4.127 +  then have "\<exists> n. x : bacc r n"
   4.128 +  proof (induct x arbitrary: rule: acc.induct)
   4.129 +    case (accI x)
   4.130 +    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
   4.131 +    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
   4.132 +    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
   4.133 +    proof
   4.134 +      fix y assume y: "(y, x) : r"
   4.135 +      with n have "y : bacc r (n y)" by auto
   4.136 +      moreover have "n y <= Max ((%(y, x). n y) ` r)"
   4.137 +        using y `finite r` by (auto intro!: Max_ge)
   4.138 +      note bacc_mono[OF this, of r]
   4.139 +      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
   4.140 +    qed
   4.141 +    then show ?case
   4.142 +      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   4.143 +  qed
   4.144 +  then show "x : (UN n. bacc r n)" by auto
   4.145 +qed
   4.146 +
   4.147 +lemma acc_bacc_eq:
   4.148 +  fixes A :: "('a :: finite \<times> 'a) set"
   4.149 +  assumes "finite A"
   4.150 +  shows "acc A = bacc A (card (UNIV :: 'a set))"
   4.151 +  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
   4.152 +
   4.153 +
   4.154  subsection {* Specification package -- Hilbertized version *}
   4.155  
   4.156  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
   4.157 @@ -651,3 +789,4 @@
   4.158  ML_file "Tools/choice_specification.ML"
   4.159  
   4.160  end
   4.161 +
     5.1 --- a/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:09:37 2012 +0200
     5.2 +++ b/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:12:16 2012 +0200
     5.3 @@ -92,7 +92,7 @@
     5.4        unfolding bs[symmetric] distinct_card[OF distb] ..
     5.5      have ca: "CARD('a) = length as"
     5.6        unfolding as[symmetric] distinct_card[OF dista] ..
     5.7 -    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
     5.8 +    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)"
     5.9      have "UNIV = set ?xs"
    5.10      proof(rule UNIV_eq_I)
    5.11        fix f :: "'a \<Rightarrow> 'b"
    5.12 @@ -103,8 +103,8 @@
    5.13      moreover have "distinct ?xs" unfolding distinct_map
    5.14      proof(intro conjI distinct_n_lists distb inj_onI)
    5.15        fix xs ys :: "'b list"
    5.16 -      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
    5.17 -        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
    5.18 +      assume xs: "xs \<in> set (List.n_lists (length as) bs)"
    5.19 +        and ys: "ys \<in> set (List.n_lists (length as) bs)"
    5.20          and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
    5.21        from xs ys have [simp]: "length xs = length as" "length ys = length as"
    5.22          by(simp_all add: length_n_lists_elem)
    5.23 @@ -472,3 +472,4 @@
    5.24  hide_const (open) card' finite' subset' eq_set
    5.25  
    5.26  end
    5.27 +
     6.1 --- a/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:09:37 2012 +0200
     6.2 +++ b/src/HOL/Library/RBT_Set.thy	Sat Oct 20 09:12:16 2012 +0200
     6.3 @@ -63,6 +63,11 @@
     6.4  lemma [code, code del]:
     6.5    "Bex = Bex" ..
     6.6  
     6.7 +term can_select
     6.8 +
     6.9 +lemma [code, code del]:
    6.10 +  "can_select = can_select" ..
    6.11 +
    6.12  lemma [code, code del]:
    6.13    "Set.union = Set.union" ..
    6.14  
     7.1 --- a/src/HOL/List.thy	Sat Oct 20 09:09:37 2012 +0200
     7.2 +++ b/src/HOL/List.thy	Sat Oct 20 09:12:16 2012 +0200
     7.3 @@ -160,6 +160,13 @@
     7.4    -- {*Warning: simpset does not contain this definition, but separate
     7.5         theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
     7.6  
     7.7 +primrec
     7.8 +  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
     7.9 +    "product [] _ = []"
    7.10 +  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
    7.11 +
    7.12 +hide_const (open) product
    7.13 +
    7.14  primrec 
    7.15    upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
    7.16      upt_0: "[i..<0] = []"
    7.17 @@ -228,6 +235,18 @@
    7.18    sublist :: "'a list => nat set => 'a list" where
    7.19    "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
    7.20  
    7.21 +primrec
    7.22 +  sublists :: "'a list \<Rightarrow> 'a list list" where
    7.23 +  "sublists [] = [[]]"
    7.24 +| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
    7.25 +
    7.26 +primrec
    7.27 +  n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    7.28 +  "n_lists 0 xs = [[]]"
    7.29 +| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    7.30 +
    7.31 +hide_const (open) n_lists
    7.32 +
    7.33  fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    7.34  "splice [] ys = ys" |
    7.35  "splice xs [] = xs" |
    7.36 @@ -253,6 +272,7 @@
    7.37  @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    7.38  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    7.39  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    7.40 +@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
    7.41  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    7.42  @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
    7.43  @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
    7.44 @@ -272,6 +292,8 @@
    7.45  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    7.46  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
    7.47  @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
    7.48 +@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
    7.49 +@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
    7.50  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
    7.51  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
    7.52  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    7.53 @@ -490,6 +512,7 @@
    7.54  
    7.55  hide_const (open) coset
    7.56  
    7.57 +
    7.58  subsubsection {* @{const Nil} and @{const Cons} *}
    7.59  
    7.60  lemma not_Cons_self [simp]:
    7.61 @@ -527,6 +550,7 @@
    7.62  lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
    7.63    by (auto intro!: inj_onI)
    7.64  
    7.65 +
    7.66  subsubsection {* @{const length} *}
    7.67  
    7.68  text {*
    7.69 @@ -788,7 +812,7 @@
    7.70  *}
    7.71  
    7.72  
    7.73 -subsubsection {* @{text map} *}
    7.74 +subsubsection {* @{const map} *}
    7.75  
    7.76  lemma hd_map:
    7.77    "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
    7.78 @@ -917,9 +941,10 @@
    7.79  enriched_type map: map
    7.80  by (simp_all add: id_def)
    7.81  
    7.82 -declare map.id[simp]
    7.83 -
    7.84 -subsubsection {* @{text rev} *}
    7.85 +declare map.id [simp]
    7.86 +
    7.87 +
    7.88 +subsubsection {* @{const rev} *}
    7.89  
    7.90  lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
    7.91  by (induct xs) auto
    7.92 @@ -966,7 +991,7 @@
    7.93  by(rule rev_cases[of xs]) auto
    7.94  
    7.95  
    7.96 -subsubsection {* @{text set} *}
    7.97 +subsubsection {* @{const set} *}
    7.98  
    7.99  declare set.simps [code_post]  --"pretty output"
   7.100  
   7.101 @@ -1128,7 +1153,7 @@
   7.102    by (induct xs) auto
   7.103  
   7.104  
   7.105 -subsubsection {* @{text filter} *}
   7.106 +subsubsection {* @{const filter} *}
   7.107  
   7.108  lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
   7.109  by (induct xs) auto
   7.110 @@ -1310,7 +1335,7 @@
   7.111  declare partition.simps[simp del]
   7.112  
   7.113  
   7.114 -subsubsection {* @{text concat} *}
   7.115 +subsubsection {* @{const concat} *}
   7.116  
   7.117  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
   7.118  by (induct xs) auto
   7.119 @@ -1346,7 +1371,7 @@
   7.120  by (simp add: concat_eq_concat_iff)
   7.121  
   7.122  
   7.123 -subsubsection {* @{text nth} *}
   7.124 +subsubsection {* @{const nth} *}
   7.125  
   7.126  lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
   7.127  by auto
   7.128 @@ -1458,7 +1483,7 @@
   7.129  qed
   7.130  
   7.131  
   7.132 -subsubsection {* @{text list_update} *}
   7.133 +subsubsection {* @{const list_update} *}
   7.134  
   7.135  lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
   7.136  by (induct xs arbitrary: i) (auto split: nat.split)
   7.137 @@ -1548,7 +1573,7 @@
   7.138    by simp_all
   7.139  
   7.140  
   7.141 -subsubsection {* @{text last} and @{text butlast} *}
   7.142 +subsubsection {* @{const last} and @{const butlast} *}
   7.143  
   7.144  lemma last_snoc [simp]: "last (xs @ [x]) = x"
   7.145  by (induct xs) auto
   7.146 @@ -1650,7 +1675,7 @@
   7.147  by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
   7.148  
   7.149  
   7.150 -subsubsection {* @{text take} and @{text drop} *}
   7.151 +subsubsection {* @{const take} and @{const drop} *}
   7.152  
   7.153  lemma take_0 [simp]: "take 0 xs = []"
   7.154  by (induct xs) auto
   7.155 @@ -1904,7 +1929,7 @@
   7.156  done
   7.157  
   7.158  
   7.159 -subsubsection {* @{text takeWhile} and @{text dropWhile} *}
   7.160 +subsubsection {* @{const takeWhile} and @{const dropWhile} *}
   7.161  
   7.162  lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
   7.163    by (induct xs) auto
   7.164 @@ -2068,7 +2093,7 @@
   7.165  by (induct k arbitrary: l, simp_all)
   7.166  
   7.167  
   7.168 -subsubsection {* @{text zip} *}
   7.169 +subsubsection {* @{const zip} *}
   7.170  
   7.171  lemma zip_Nil [simp]: "zip [] ys = []"
   7.172  by (induct ys) auto
   7.173 @@ -2230,7 +2255,7 @@
   7.174    by (auto simp add: zip_map_fst_snd)
   7.175  
   7.176  
   7.177 -subsubsection {* @{text list_all2} *}
   7.178 +subsubsection {* @{const list_all2} *}
   7.179  
   7.180  lemma list_all2_lengthD [intro?]: 
   7.181    "list_all2 P xs ys ==> length xs = length ys"
   7.182 @@ -2387,6 +2412,13 @@
   7.183  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
   7.184  
   7.185  
   7.186 +subsubsection {* @{const List.product} *}
   7.187 +
   7.188 +lemma product_list_set:
   7.189 +  "set (List.product xs ys) = set xs \<times> set ys"
   7.190 +  by (induct xs) auto
   7.191 +
   7.192 +
   7.193  subsubsection {* @{const fold} with natural argument order *}
   7.194  
   7.195  lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
   7.196 @@ -2613,6 +2645,7 @@
   7.197  
   7.198  declare SUP_set_fold [code]
   7.199  
   7.200 +
   7.201  subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
   7.202  
   7.203  text {* Correspondence *}
   7.204 @@ -2667,7 +2700,7 @@
   7.205    by (simp add: fold_append_concat_rev foldr_conv_fold)
   7.206  
   7.207  
   7.208 -subsubsection {* @{text upt} *}
   7.209 +subsubsection {* @{const upt} *}
   7.210  
   7.211  lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
   7.212  -- {* simp does not terminate! *}
   7.213 @@ -2830,7 +2863,7 @@
   7.214  qed
   7.215  
   7.216  
   7.217 -subsubsection {* @{text "distinct"} and @{text remdups} *}
   7.218 +subsubsection {* @{const distinct} and @{const remdups} *}
   7.219  
   7.220  lemma distinct_tl:
   7.221    "distinct xs \<Longrightarrow> distinct (tl xs)"
   7.222 @@ -2885,7 +2918,6 @@
   7.223    "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
   7.224  by (induct xs) auto
   7.225  
   7.226 -
   7.227  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
   7.228  by (induct xs) auto
   7.229  
   7.230 @@ -3020,6 +3052,12 @@
   7.231    qed
   7.232  qed (auto simp: dec_def)
   7.233  
   7.234 +lemma distinct_product:
   7.235 +  assumes "distinct xs" and "distinct ys"
   7.236 +  shows "distinct (List.product xs ys)"
   7.237 +  using assms by (induct xs)
   7.238 +    (auto intro: inj_onI simp add: product_list_set distinct_map)
   7.239 +
   7.240  lemma length_remdups_concat:
   7.241    "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
   7.242    by (simp add: distinct_card [symmetric])
   7.243 @@ -3083,6 +3121,7 @@
   7.244  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
   7.245  by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
   7.246  
   7.247 +
   7.248  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   7.249  
   7.250  lemma (in monoid_add) listsum_simps [simp]:
   7.251 @@ -3342,7 +3381,7 @@
   7.252    using assms by (induct xs) simp_all
   7.253  
   7.254  
   7.255 -subsubsection {* @{text removeAll} *}
   7.256 +subsubsection {* @{const removeAll} *}
   7.257  
   7.258  lemma removeAll_filter_not_eq:
   7.259    "removeAll x = filter (\<lambda>y. x \<noteq> y)"
   7.260 @@ -3388,7 +3427,7 @@
   7.261  by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
   7.262  
   7.263  
   7.264 -subsubsection {* @{text replicate} *}
   7.265 +subsubsection {* @{const replicate} *}
   7.266  
   7.267  lemma length_replicate [simp]: "length (replicate n x) = n"
   7.268  by (induct n) auto
   7.269 @@ -3578,7 +3617,7 @@
   7.270  qed
   7.271  
   7.272  
   7.273 -subsubsection{*@{text rotate1} and @{text rotate}*}
   7.274 +subsubsection {* @{const rotate1} and @{const rotate} *}
   7.275  
   7.276  lemma rotate0[simp]: "rotate 0 = id"
   7.277  by(simp add:rotate_def)
   7.278 @@ -3672,7 +3711,7 @@
   7.279  using mod_less_divisor[of "length xs" n] by arith
   7.280  
   7.281  
   7.282 -subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
   7.283 +subsubsection {* @{const sublist} --- a generalization of @{const nth} to sets *}
   7.284  
   7.285  lemma sublist_empty [simp]: "sublist xs {} = []"
   7.286  by (auto simp add: sublist_def)
   7.287 @@ -3755,6 +3794,82 @@
   7.288  qed
   7.289  
   7.290  
   7.291 +subsubsection {* @{const sublists} and @{const List.n_lists} *}
   7.292 +
   7.293 +lemma length_sublists:
   7.294 +  "length (sublists xs) = 2 ^ length xs"
   7.295 +  by (induct xs) (simp_all add: Let_def)
   7.296 +
   7.297 +lemma sublists_powset:
   7.298 +  "set ` set (sublists xs) = Pow (set xs)"
   7.299 +proof -
   7.300 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   7.301 +    by (auto simp add: image_def)
   7.302 +  have "set (map set (sublists xs)) = Pow (set xs)"
   7.303 +    by (induct xs)
   7.304 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   7.305 +  then show ?thesis by simp
   7.306 +qed
   7.307 +
   7.308 +lemma distinct_set_sublists:
   7.309 +  assumes "distinct xs"
   7.310 +  shows "distinct (map set (sublists xs))"
   7.311 +proof (rule card_distinct)
   7.312 +  have "finite (set xs)" by rule
   7.313 +  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   7.314 +  with assms distinct_card [of xs]
   7.315 +    have "card (Pow (set xs)) = 2 ^ length xs" by simp
   7.316 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   7.317 +    by (simp add: sublists_powset length_sublists)
   7.318 +qed
   7.319 +
   7.320 +lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
   7.321 +  by (induct n) simp_all
   7.322 +
   7.323 +lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   7.324 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
   7.325 +
   7.326 +lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
   7.327 +  by (induct n arbitrary: ys) auto
   7.328 +
   7.329 +lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
   7.330 +proof (rule set_eqI)
   7.331 +  fix ys :: "'a list"
   7.332 +  show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
   7.333 +  proof -
   7.334 +    have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
   7.335 +      by (induct n arbitrary: ys) auto
   7.336 +    moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
   7.337 +      by (induct n arbitrary: ys) auto
   7.338 +    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
   7.339 +      by (induct ys) auto
   7.340 +    ultimately show ?thesis by auto
   7.341 +  qed
   7.342 +qed
   7.343 +
   7.344 +lemma distinct_n_lists:
   7.345 +  assumes "distinct xs"
   7.346 +  shows "distinct (List.n_lists n xs)"
   7.347 +proof (rule card_distinct)
   7.348 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   7.349 +  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
   7.350 +  proof (induct n)
   7.351 +    case 0 then show ?case by simp
   7.352 +  next
   7.353 +    case (Suc n)
   7.354 +    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   7.355 +      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   7.356 +      by (rule card_UN_disjoint) auto
   7.357 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   7.358 +      by (rule card_image) (simp add: inj_on_def)
   7.359 +    ultimately show ?case by auto
   7.360 +  qed
   7.361 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   7.362 +  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
   7.363 +    by (simp add: length_n_lists)
   7.364 +qed
   7.365 +
   7.366 +
   7.367  subsubsection {* @{const splice} *}
   7.368  
   7.369  lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
   7.370 @@ -5319,6 +5434,15 @@
   7.371    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
   7.372  by (simp add: list_ex_iff)
   7.373  
   7.374 +definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   7.375 +where
   7.376 +  [code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
   7.377 +
   7.378 +lemma can_select_set_list_ex1 [code]:
   7.379 +  "can_select P (set A) = list_ex1 P A"
   7.380 +  by (simp add: list_ex1_iff can_select_def)
   7.381 +
   7.382 +
   7.383  text {* Executable checks for relations on sets *}
   7.384  
   7.385  definition listrel1p :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   7.386 @@ -5531,6 +5655,7 @@
   7.387  
   7.388  hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
   7.389  
   7.390 +
   7.391  subsubsection {* Pretty lists *}
   7.392  
   7.393  ML_file "Tools/list_code.ML"
   7.394 @@ -5698,6 +5823,7 @@
   7.395  
   7.396  hide_const (open) map_project
   7.397  
   7.398 +
   7.399  text {* Operations on relations *}
   7.400  
   7.401  lemma product_code [code]:
     8.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:09:37 2012 +0200
     8.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:12:16 2012 +0200
     8.3 @@ -234,7 +234,7 @@
     8.4    "enum_term_of_fun = (%_ _. let
     8.5      enum_term_of_a = enum_term_of (TYPE('a));
     8.6      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
     8.7 -  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
     8.8 +  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
     8.9   
    8.10  instance ..
    8.11  
    8.12 @@ -308,7 +308,7 @@
    8.13  definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
    8.14  where
    8.15    "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
    8.16 -     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
    8.17 +     (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
    8.18  
    8.19  instance ..
    8.20  
     9.1 --- a/src/HOL/String.thy	Sat Oct 20 09:09:37 2012 +0200
     9.2 +++ b/src/HOL/String.thy	Sat Oct 20 09:12:16 2012 +0200
     9.3 @@ -149,6 +149,14 @@
     9.4    Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
     9.5    Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
     9.6  
     9.7 +lemma UNIV_set_chars:
     9.8 +  "UNIV = set chars"
     9.9 +  by (simp only: UNIV_char UNIV_nibble) code_simp
    9.10 +
    9.11 +lemma distinct_chars:
    9.12 +  "distinct chars"
    9.13 +  by code_simp
    9.14 +
    9.15  
    9.16  subsection {* Strings as dedicated type *}
    9.17  
    9.18 @@ -213,3 +221,4 @@
    9.19  hide_type (open) literal
    9.20  
    9.21  end
    9.22 +
    10.1 --- a/src/HOL/Sum_Type.thy	Sat Oct 20 09:09:37 2012 +0200
    10.2 +++ b/src/HOL/Sum_Type.thy	Sat Oct 20 09:12:16 2012 +0200
    10.3 @@ -209,8 +209,19 @@
    10.4    show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
    10.5  qed
    10.6  
    10.7 +lemma UNIV_sum:
    10.8 +  "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
    10.9 +proof -
   10.10 +  { fix x :: "'a + 'b"
   10.11 +    assume "x \<notin> range Inr"
   10.12 +    then have "x \<in> range Inl"
   10.13 +    by (cases x) simp_all
   10.14 +  } then show ?thesis by auto
   10.15 +qed
   10.16 +
   10.17  hide_const (open) Suml Sumr Projl Projr
   10.18  
   10.19  hide_const (open) sum
   10.20  
   10.21  end
   10.22 +