src/HOL/List.thy
changeset 53721 ccaceea6c768
parent 53689 705f0b728b1b
child 53940 36cf426cb1c6
     1.1 --- a/src/HOL/List.thy	Wed Sep 18 22:59:11 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Sep 18 18:11:32 2013 +0200
     1.3 @@ -146,6 +146,10 @@
     1.4  
     1.5  hide_const (open) product
     1.6  
     1.7 +primrec product_lists :: "'a list list \<Rightarrow> 'a list list" where
     1.8 +"product_lists [] = [[]]" |
     1.9 +"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)"
    1.10 +
    1.11  primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
    1.12  upt_0: "[i..<0] = []" |
    1.13  upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
    1.14 @@ -185,6 +189,11 @@
    1.15  "remdups [] = []" |
    1.16  "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
    1.17  
    1.18 +fun remdups_adj :: "'a list \<Rightarrow> 'a list" where
    1.19 +"remdups_adj [] = []" |
    1.20 +"remdups_adj [x] = [x]" |
    1.21 +"remdups_adj (x # y # xs) = (if x = y then remdups_adj (x # xs) else x # remdups_adj (y # xs))"
    1.22 +
    1.23  primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
    1.24  replicate_0: "replicate 0 x = []" |
    1.25  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    1.26 @@ -250,6 +259,7 @@
    1.27  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    1.28  @{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
    1.29  @{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
    1.30 +@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\
    1.31  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    1.32  @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
    1.33  @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
    1.34 @@ -260,6 +270,7 @@
    1.35  @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
    1.36  @{lemma "distinct [2,0,1::nat]" by simp}\\
    1.37  @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
    1.38 +@{lemma "remdups_adj [2,2,3,1,1::nat,2,1] = [2,3,1,2,1]" by simp}\\
    1.39  @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
    1.40  @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
    1.41  @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
    1.42 @@ -2663,7 +2674,7 @@
    1.43  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
    1.44  
    1.45  
    1.46 -subsubsection {* @{const List.product} *}
    1.47 +subsubsection {* @{const List.product} and @{const product_lists} *}
    1.48  
    1.49  lemma product_list_set:
    1.50    "set (List.product xs ys) = set xs \<times> set ys"
    1.51 @@ -2685,6 +2696,21 @@
    1.52      by (auto simp add: nth_append not_less le_mod_geq le_div_geq)
    1.53  qed
    1.54  
    1.55 +lemma in_set_product_lists_length: 
    1.56 +  "xs \<in> set (product_lists xss) \<Longrightarrow> length xs = length xss"
    1.57 +  by (induct xss arbitrary: xs) auto
    1.58 +
    1.59 +lemma product_lists_set:
    1.60 +  "set (product_lists xss) = {xs. list_all2 (\<lambda>x ys. x \<in> set ys) xs xss}" (is "?L = Collect ?R")
    1.61 +proof (intro equalityI subsetI, unfold mem_Collect_eq)
    1.62 +  fix xs assume "xs \<in> ?L"
    1.63 +  then have "length xs = length xss" by (rule in_set_product_lists_length)
    1.64 +  from this `xs \<in> ?L` show "?R xs" by (induct xs xss rule: list_induct2) auto
    1.65 +next
    1.66 +  fix xs assume "?R xs"
    1.67 +  then show "xs \<in> ?L" by induct auto
    1.68 +qed
    1.69 +
    1.70  
    1.71  subsubsection {* @{const fold} with natural argument order *}
    1.72  
    1.73 @@ -3085,7 +3111,7 @@
    1.74  by(simp add: upto_aux_def)
    1.75  
    1.76  
    1.77 -subsubsection {* @{const distinct} and @{const remdups} *}
    1.78 +subsubsection {* @{const distinct} and @{const remdups} and @{const remdups_adj} *}
    1.79  
    1.80  lemma distinct_tl:
    1.81    "distinct xs \<Longrightarrow> distinct (tl xs)"
    1.82 @@ -3280,6 +3306,20 @@
    1.83    using assms by (induct xs)
    1.84      (auto intro: inj_onI simp add: product_list_set distinct_map)
    1.85  
    1.86 +lemma distinct_product_lists:
    1.87 +  assumes "\<forall>xs \<in> set xss. distinct xs"
    1.88 +  shows "distinct (product_lists xss)"
    1.89 +using assms proof (induction xss)
    1.90 +  case (Cons xs xss) note * = this
    1.91 +  then show ?case
    1.92 +  proof (cases "product_lists xss")
    1.93 +    case Nil then show ?thesis by (induct xs) simp_all
    1.94 +  next
    1.95 +    case (Cons ps pss) with * show ?thesis 
    1.96 +      by (auto intro!: inj_onI distinct_concat simp add: distinct_map)
    1.97 +  qed
    1.98 +qed simp
    1.99 +
   1.100  lemma length_remdups_concat:
   1.101    "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
   1.102    by (simp add: distinct_card [symmetric])
   1.103 @@ -3343,6 +3383,49 @@
   1.104  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
   1.105  by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
   1.106  
   1.107 +lemma remdups_adj_Cons: "remdups_adj (x # xs) =
   1.108 +  (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
   1.109 +  by (induct xs arbitrary: x) (auto split: list.splits)
   1.110 +
   1.111 +lemma remdups_adj_append_two: 
   1.112 +  "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])"
   1.113 +  by (induct xs rule: remdups_adj.induct, simp_all)
   1.114 +
   1.115 +lemma remdups_adj_rev[simp]: "remdups_adj (rev xs) = rev (remdups_adj xs)"
   1.116 +  by (induct xs rule: remdups_adj.induct, simp_all add: remdups_adj_append_two)
   1.117 +
   1.118 +lemma remdups_adj_length[simp]: "length (remdups_adj xs) \<le> length xs"
   1.119 +  by (induct xs rule: remdups_adj.induct, auto)
   1.120 +
   1.121 +lemma remdups_adj_length_ge1[simp]: "xs \<noteq> [] \<Longrightarrow> length (remdups_adj xs) \<ge> Suc 0"
   1.122 +  by (induct xs rule: remdups_adj.induct, simp_all)
   1.123 +
   1.124 +lemma remdups_adj_Nil_iff[simp]: "remdups_adj xs = [] \<longleftrightarrow> xs = []"
   1.125 +  by (induct xs rule: remdups_adj.induct, simp_all)
   1.126 +
   1.127 +lemma remdups_adj_set[simp]: "set (remdups_adj xs) = set xs"
   1.128 +  by (induct xs rule: remdups_adj.induct, simp_all)
   1.129 +
   1.130 +lemma remdups_adj_Cons_alt[simp]: "x # tl (remdups_adj (x # xs)) = remdups_adj (x # xs)"
   1.131 +    by (induct xs rule: remdups_adj.induct, auto)
   1.132 +
   1.133 +lemma remdups_adj_distinct: "distinct xs \<Longrightarrow> remdups_adj xs = xs"
   1.134 +    by (induct xs rule: remdups_adj.induct, simp_all)
   1.135 +
   1.136 +lemma remdups_adj_append: 
   1.137 +  "remdups_adj (xs\<^sub>1 @ x # xs\<^sub>2) = remdups_adj (xs\<^sub>1 @ [x]) @ tl (remdups_adj (x # xs\<^sub>2))"
   1.138 +  by (induct xs\<^sub>1 rule: remdups_adj.induct, simp_all)
   1.139 +
   1.140 +lemma remdups_adj_singleton:
   1.141 +  "remdups_adj xs = [x] \<Longrightarrow> xs = replicate (length xs) x"
   1.142 +  by (induct xs rule: remdups_adj.induct, auto split: split_if_asm)
   1.143 +
   1.144 +lemma remdups_adj_map_injective:
   1.145 +  assumes "inj f"
   1.146 +  shows "remdups_adj (map f xs) = map f (remdups_adj xs)"
   1.147 +  by (induct xs rule: remdups_adj.induct, 
   1.148 +      auto simp add: injD[OF assms])
   1.149 +
   1.150  
   1.151  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   1.152  
   1.153 @@ -3396,6 +3479,12 @@
   1.154    "length (concat xss) = listsum (map length xss)"
   1.155    by (induct xss) simp_all
   1.156  
   1.157 +lemma (in monoid_add) length_product_lists:
   1.158 +  "length (product_lists xss) = foldr op * (map length xss) 1"
   1.159 +proof (induct xss)
   1.160 +  case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
   1.161 +qed simp
   1.162 +
   1.163  lemma (in monoid_add) listsum_map_filter:
   1.164    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
   1.165    shows "listsum (map f (filter P xs)) = listsum (map f xs)"
   1.166 @@ -4573,6 +4662,10 @@
   1.167    "sorted l \<Longrightarrow> sorted (remdups l)"
   1.168  by (induct l) (auto simp: sorted_Cons)
   1.169  
   1.170 +lemma sorted_remdups_adj[simp]:
   1.171 +  "sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
   1.172 +by (induct xs rule: remdups_adj.induct, simp_all split: split_if_asm add: sorted_Cons)
   1.173 +
   1.174  lemma sorted_distinct_set_unique:
   1.175  assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
   1.176  shows "xs = ys"
   1.177 @@ -6462,6 +6555,14 @@
   1.178    "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
   1.179    unfolding zip_def by transfer_prover
   1.180  
   1.181 +lemma product_transfer [transfer_rule]:
   1.182 +  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) List.product List.product"
   1.183 +  unfolding List.product_def by transfer_prover
   1.184 +
   1.185 +lemma product_lists_transfer [transfer_rule]:
   1.186 +  "(list_all2 (list_all2 A) ===> list_all2 (list_all2 A)) product_lists product_lists"
   1.187 +  unfolding product_lists_def by transfer_prover
   1.188 +
   1.189  lemma insert_transfer [transfer_rule]:
   1.190    assumes [transfer_rule]: "bi_unique A"
   1.191    shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert"
   1.192 @@ -6491,6 +6592,12 @@
   1.193    shows "(list_all2 A ===> list_all2 A) remdups remdups"
   1.194    unfolding remdups_def by transfer_prover
   1.195  
   1.196 +lemma remdups_adj_transfer [transfer_rule]:
   1.197 +  assumes [transfer_rule]: "bi_unique A"
   1.198 +  shows "(list_all2 A ===> list_all2 A) remdups_adj remdups_adj"
   1.199 +  proof (rule fun_relI, erule list_all2_induct)
   1.200 +  qed (auto simp: remdups_adj_Cons assms[unfolded bi_unique_def] split: list.splits)
   1.201 +
   1.202  lemma replicate_transfer [transfer_rule]:
   1.203    "(op = ===> A ===> list_all2 A) replicate replicate"
   1.204    unfolding replicate_def by transfer_prover