src/HOL/List.thy
changeset 49948 744934b818c7
parent 49808 418991ce7567
child 49963 326f87427719
     1.1 --- a/src/HOL/List.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -160,6 +160,13 @@
     1.4    -- {*Warning: simpset does not contain this definition, but separate
     1.5         theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
     1.6  
     1.7 +primrec
     1.8 +  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
     1.9 +    "product [] _ = []"
    1.10 +  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
    1.11 +
    1.12 +hide_const (open) product
    1.13 +
    1.14  primrec 
    1.15    upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
    1.16      upt_0: "[i..<0] = []"
    1.17 @@ -228,6 +235,18 @@
    1.18    sublist :: "'a list => nat set => 'a list" where
    1.19    "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
    1.20  
    1.21 +primrec
    1.22 +  sublists :: "'a list \<Rightarrow> 'a list list" where
    1.23 +  "sublists [] = [[]]"
    1.24 +| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
    1.25 +
    1.26 +primrec
    1.27 +  n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    1.28 +  "n_lists 0 xs = [[]]"
    1.29 +| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    1.30 +
    1.31 +hide_const (open) n_lists
    1.32 +
    1.33  fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.34  "splice [] ys = ys" |
    1.35  "splice xs [] = xs" |
    1.36 @@ -253,6 +272,7 @@
    1.37  @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    1.38  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    1.39  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    1.40 +@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
    1.41  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    1.42  @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
    1.43  @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
    1.44 @@ -272,6 +292,8 @@
    1.45  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    1.46  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
    1.47  @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
    1.48 +@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
    1.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)}\\
    1.50  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
    1.51  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
    1.52  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    1.53 @@ -490,6 +512,7 @@
    1.54  
    1.55  hide_const (open) coset
    1.56  
    1.57 +
    1.58  subsubsection {* @{const Nil} and @{const Cons} *}
    1.59  
    1.60  lemma not_Cons_self [simp]:
    1.61 @@ -527,6 +550,7 @@
    1.62  lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
    1.63    by (auto intro!: inj_onI)
    1.64  
    1.65 +
    1.66  subsubsection {* @{const length} *}
    1.67  
    1.68  text {*
    1.69 @@ -788,7 +812,7 @@
    1.70  *}
    1.71  
    1.72  
    1.73 -subsubsection {* @{text map} *}
    1.74 +subsubsection {* @{const map} *}
    1.75  
    1.76  lemma hd_map:
    1.77    "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
    1.78 @@ -917,9 +941,10 @@
    1.79  enriched_type map: map
    1.80  by (simp_all add: id_def)
    1.81  
    1.82 -declare map.id[simp]
    1.83 -
    1.84 -subsubsection {* @{text rev} *}
    1.85 +declare map.id [simp]
    1.86 +
    1.87 +
    1.88 +subsubsection {* @{const rev} *}
    1.89  
    1.90  lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
    1.91  by (induct xs) auto
    1.92 @@ -966,7 +991,7 @@
    1.93  by(rule rev_cases[of xs]) auto
    1.94  
    1.95  
    1.96 -subsubsection {* @{text set} *}
    1.97 +subsubsection {* @{const set} *}
    1.98  
    1.99  declare set.simps [code_post]  --"pretty output"
   1.100  
   1.101 @@ -1128,7 +1153,7 @@
   1.102    by (induct xs) auto
   1.103  
   1.104  
   1.105 -subsubsection {* @{text filter} *}
   1.106 +subsubsection {* @{const filter} *}
   1.107  
   1.108  lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
   1.109  by (induct xs) auto
   1.110 @@ -1310,7 +1335,7 @@
   1.111  declare partition.simps[simp del]
   1.112  
   1.113  
   1.114 -subsubsection {* @{text concat} *}
   1.115 +subsubsection {* @{const concat} *}
   1.116  
   1.117  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
   1.118  by (induct xs) auto
   1.119 @@ -1346,7 +1371,7 @@
   1.120  by (simp add: concat_eq_concat_iff)
   1.121  
   1.122  
   1.123 -subsubsection {* @{text nth} *}
   1.124 +subsubsection {* @{const nth} *}
   1.125  
   1.126  lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
   1.127  by auto
   1.128 @@ -1458,7 +1483,7 @@
   1.129  qed
   1.130  
   1.131  
   1.132 -subsubsection {* @{text list_update} *}
   1.133 +subsubsection {* @{const list_update} *}
   1.134  
   1.135  lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
   1.136  by (induct xs arbitrary: i) (auto split: nat.split)
   1.137 @@ -1548,7 +1573,7 @@
   1.138    by simp_all
   1.139  
   1.140  
   1.141 -subsubsection {* @{text last} and @{text butlast} *}
   1.142 +subsubsection {* @{const last} and @{const butlast} *}
   1.143  
   1.144  lemma last_snoc [simp]: "last (xs @ [x]) = x"
   1.145  by (induct xs) auto
   1.146 @@ -1650,7 +1675,7 @@
   1.147  by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
   1.148  
   1.149  
   1.150 -subsubsection {* @{text take} and @{text drop} *}
   1.151 +subsubsection {* @{const take} and @{const drop} *}
   1.152  
   1.153  lemma take_0 [simp]: "take 0 xs = []"
   1.154  by (induct xs) auto
   1.155 @@ -1904,7 +1929,7 @@
   1.156  done
   1.157  
   1.158  
   1.159 -subsubsection {* @{text takeWhile} and @{text dropWhile} *}
   1.160 +subsubsection {* @{const takeWhile} and @{const dropWhile} *}
   1.161  
   1.162  lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
   1.163    by (induct xs) auto
   1.164 @@ -2068,7 +2093,7 @@
   1.165  by (induct k arbitrary: l, simp_all)
   1.166  
   1.167  
   1.168 -subsubsection {* @{text zip} *}
   1.169 +subsubsection {* @{const zip} *}
   1.170  
   1.171  lemma zip_Nil [simp]: "zip [] ys = []"
   1.172  by (induct ys) auto
   1.173 @@ -2230,7 +2255,7 @@
   1.174    by (auto simp add: zip_map_fst_snd)
   1.175  
   1.176  
   1.177 -subsubsection {* @{text list_all2} *}
   1.178 +subsubsection {* @{const list_all2} *}
   1.179  
   1.180  lemma list_all2_lengthD [intro?]: 
   1.181    "list_all2 P xs ys ==> length xs = length ys"
   1.182 @@ -2387,6 +2412,13 @@
   1.183  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
   1.184  
   1.185  
   1.186 +subsubsection {* @{const List.product} *}
   1.187 +
   1.188 +lemma product_list_set:
   1.189 +  "set (List.product xs ys) = set xs \<times> set ys"
   1.190 +  by (induct xs) auto
   1.191 +
   1.192 +
   1.193  subsubsection {* @{const fold} with natural argument order *}
   1.194  
   1.195  lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
   1.196 @@ -2613,6 +2645,7 @@
   1.197  
   1.198  declare SUP_set_fold [code]
   1.199  
   1.200 +
   1.201  subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
   1.202  
   1.203  text {* Correspondence *}
   1.204 @@ -2667,7 +2700,7 @@
   1.205    by (simp add: fold_append_concat_rev foldr_conv_fold)
   1.206  
   1.207  
   1.208 -subsubsection {* @{text upt} *}
   1.209 +subsubsection {* @{const upt} *}
   1.210  
   1.211  lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
   1.212  -- {* simp does not terminate! *}
   1.213 @@ -2830,7 +2863,7 @@
   1.214  qed
   1.215  
   1.216  
   1.217 -subsubsection {* @{text "distinct"} and @{text remdups} *}
   1.218 +subsubsection {* @{const distinct} and @{const remdups} *}
   1.219  
   1.220  lemma distinct_tl:
   1.221    "distinct xs \<Longrightarrow> distinct (tl xs)"
   1.222 @@ -2885,7 +2918,6 @@
   1.223    "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
   1.224  by (induct xs) auto
   1.225  
   1.226 -
   1.227  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
   1.228  by (induct xs) auto
   1.229  
   1.230 @@ -3020,6 +3052,12 @@
   1.231    qed
   1.232  qed (auto simp: dec_def)
   1.233  
   1.234 +lemma distinct_product:
   1.235 +  assumes "distinct xs" and "distinct ys"
   1.236 +  shows "distinct (List.product xs ys)"
   1.237 +  using assms by (induct xs)
   1.238 +    (auto intro: inj_onI simp add: product_list_set distinct_map)
   1.239 +
   1.240  lemma length_remdups_concat:
   1.241    "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
   1.242    by (simp add: distinct_card [symmetric])
   1.243 @@ -3083,6 +3121,7 @@
   1.244  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
   1.245  by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
   1.246  
   1.247 +
   1.248  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   1.249  
   1.250  lemma (in monoid_add) listsum_simps [simp]:
   1.251 @@ -3342,7 +3381,7 @@
   1.252    using assms by (induct xs) simp_all
   1.253  
   1.254  
   1.255 -subsubsection {* @{text removeAll} *}
   1.256 +subsubsection {* @{const removeAll} *}
   1.257  
   1.258  lemma removeAll_filter_not_eq:
   1.259    "removeAll x = filter (\<lambda>y. x \<noteq> y)"
   1.260 @@ -3388,7 +3427,7 @@
   1.261  by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
   1.262  
   1.263  
   1.264 -subsubsection {* @{text replicate} *}
   1.265 +subsubsection {* @{const replicate} *}
   1.266  
   1.267  lemma length_replicate [simp]: "length (replicate n x) = n"
   1.268  by (induct n) auto
   1.269 @@ -3578,7 +3617,7 @@
   1.270  qed
   1.271  
   1.272  
   1.273 -subsubsection{*@{text rotate1} and @{text rotate}*}
   1.274 +subsubsection {* @{const rotate1} and @{const rotate} *}
   1.275  
   1.276  lemma rotate0[simp]: "rotate 0 = id"
   1.277  by(simp add:rotate_def)
   1.278 @@ -3672,7 +3711,7 @@
   1.279  using mod_less_divisor[of "length xs" n] by arith
   1.280  
   1.281  
   1.282 -subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
   1.283 +subsubsection {* @{const sublist} --- a generalization of @{const nth} to sets *}
   1.284  
   1.285  lemma sublist_empty [simp]: "sublist xs {} = []"
   1.286  by (auto simp add: sublist_def)
   1.287 @@ -3755,6 +3794,82 @@
   1.288  qed
   1.289  
   1.290  
   1.291 +subsubsection {* @{const sublists} and @{const List.n_lists} *}
   1.292 +
   1.293 +lemma length_sublists:
   1.294 +  "length (sublists xs) = 2 ^ length xs"
   1.295 +  by (induct xs) (simp_all add: Let_def)
   1.296 +
   1.297 +lemma sublists_powset:
   1.298 +  "set ` set (sublists xs) = Pow (set xs)"
   1.299 +proof -
   1.300 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   1.301 +    by (auto simp add: image_def)
   1.302 +  have "set (map set (sublists xs)) = Pow (set xs)"
   1.303 +    by (induct xs)
   1.304 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   1.305 +  then show ?thesis by simp
   1.306 +qed
   1.307 +
   1.308 +lemma distinct_set_sublists:
   1.309 +  assumes "distinct xs"
   1.310 +  shows "distinct (map set (sublists xs))"
   1.311 +proof (rule card_distinct)
   1.312 +  have "finite (set xs)" by rule
   1.313 +  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
   1.314 +  with assms distinct_card [of xs]
   1.315 +    have "card (Pow (set xs)) = 2 ^ length xs" by simp
   1.316 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   1.317 +    by (simp add: sublists_powset length_sublists)
   1.318 +qed
   1.319 +
   1.320 +lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
   1.321 +  by (induct n) simp_all
   1.322 +
   1.323 +lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   1.324 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
   1.325 +
   1.326 +lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
   1.327 +  by (induct n arbitrary: ys) auto
   1.328 +
   1.329 +lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
   1.330 +proof (rule set_eqI)
   1.331 +  fix ys :: "'a list"
   1.332 +  show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
   1.333 +  proof -
   1.334 +    have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
   1.335 +      by (induct n arbitrary: ys) auto
   1.336 +    moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
   1.337 +      by (induct n arbitrary: ys) auto
   1.338 +    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
   1.339 +      by (induct ys) auto
   1.340 +    ultimately show ?thesis by auto
   1.341 +  qed
   1.342 +qed
   1.343 +
   1.344 +lemma distinct_n_lists:
   1.345 +  assumes "distinct xs"
   1.346 +  shows "distinct (List.n_lists n xs)"
   1.347 +proof (rule card_distinct)
   1.348 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   1.349 +  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
   1.350 +  proof (induct n)
   1.351 +    case 0 then show ?case by simp
   1.352 +  next
   1.353 +    case (Suc n)
   1.354 +    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   1.355 +      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   1.356 +      by (rule card_UN_disjoint) auto
   1.357 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   1.358 +      by (rule card_image) (simp add: inj_on_def)
   1.359 +    ultimately show ?case by auto
   1.360 +  qed
   1.361 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   1.362 +  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
   1.363 +    by (simp add: length_n_lists)
   1.364 +qed
   1.365 +
   1.366 +
   1.367  subsubsection {* @{const splice} *}
   1.368  
   1.369  lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
   1.370 @@ -5319,6 +5434,15 @@
   1.371    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
   1.372  by (simp add: list_ex_iff)
   1.373  
   1.374 +definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   1.375 +where
   1.376 +  [code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
   1.377 +
   1.378 +lemma can_select_set_list_ex1 [code]:
   1.379 +  "can_select P (set A) = list_ex1 P A"
   1.380 +  by (simp add: list_ex1_iff can_select_def)
   1.381 +
   1.382 +
   1.383  text {* Executable checks for relations on sets *}
   1.384  
   1.385  definition listrel1p :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.386 @@ -5531,6 +5655,7 @@
   1.387  
   1.388  hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
   1.389  
   1.390 +
   1.391  subsubsection {* Pretty lists *}
   1.392  
   1.393  ML_file "Tools/list_code.ML"
   1.394 @@ -5698,6 +5823,7 @@
   1.395  
   1.396  hide_const (open) map_project
   1.397  
   1.398 +
   1.399  text {* Operations on relations *}
   1.400  
   1.401  lemma product_code [code]: