summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 53721 | ccaceea6c768 |

parent 53689 | 705f0b728b1b |

child 53940 | 36cf426cb1c6 |

--- a/src/HOL/List.thy Wed Sep 18 22:59:11 2013 +0200 +++ b/src/HOL/List.thy Wed Sep 18 18:11:32 2013 +0200 @@ -146,6 +146,10 @@ hide_const (open) product +primrec product_lists :: "'a list list \<Rightarrow> 'a list list" where +"product_lists [] = [[]]" | +"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)" + primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where upt_0: "[i..<0] = []" | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" @@ -185,6 +189,11 @@ "remdups [] = []" | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)" +fun remdups_adj :: "'a list \<Rightarrow> 'a list" where +"remdups_adj [] = []" | +"remdups_adj [x] = [x]" | +"remdups_adj (x # y # xs) = (if x = y then remdups_adj (x # xs) else x # remdups_adj (y # xs))" + primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where replicate_0: "replicate 0 x = []" | replicate_Suc: "replicate (Suc n) x = x # replicate n x" @@ -250,6 +259,7 @@ @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ @{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\ @{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\ +@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ @@ -260,6 +270,7 @@ @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\ @{lemma "distinct [2,0,1::nat]" by simp}\\ @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ +@{lemma "remdups_adj [2,2,3,1,1::nat,2,1] = [2,3,1,2,1]" by simp}\\ @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\ @@ -2663,7 +2674,7 @@ by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong) -subsubsection {* @{const List.product} *} +subsubsection {* @{const List.product} and @{const product_lists} *} lemma product_list_set: "set (List.product xs ys) = set xs \<times> set ys" @@ -2685,6 +2696,21 @@ by (auto simp add: nth_append not_less le_mod_geq le_div_geq) qed +lemma in_set_product_lists_length: + "xs \<in> set (product_lists xss) \<Longrightarrow> length xs = length xss" + by (induct xss arbitrary: xs) auto + +lemma product_lists_set: + "set (product_lists xss) = {xs. list_all2 (\<lambda>x ys. x \<in> set ys) xs xss}" (is "?L = Collect ?R") +proof (intro equalityI subsetI, unfold mem_Collect_eq) + fix xs assume "xs \<in> ?L" + then have "length xs = length xss" by (rule in_set_product_lists_length) + from this `xs \<in> ?L` show "?R xs" by (induct xs xss rule: list_induct2) auto +next + fix xs assume "?R xs" + then show "xs \<in> ?L" by induct auto +qed + subsubsection {* @{const fold} with natural argument order *} @@ -3085,7 +3111,7 @@ by(simp add: upto_aux_def) -subsubsection {* @{const distinct} and @{const remdups} *} +subsubsection {* @{const distinct} and @{const remdups} and @{const remdups_adj} *} lemma distinct_tl: "distinct xs \<Longrightarrow> distinct (tl xs)" @@ -3280,6 +3306,20 @@ using assms by (induct xs) (auto intro: inj_onI simp add: product_list_set distinct_map) +lemma distinct_product_lists: + assumes "\<forall>xs \<in> set xss. distinct xs" + shows "distinct (product_lists xss)" +using assms proof (induction xss) + case (Cons xs xss) note * = this + then show ?case + proof (cases "product_lists xss") + case Nil then show ?thesis by (induct xs) simp_all + next + case (Cons ps pss) with * show ?thesis + by (auto intro!: inj_onI distinct_concat simp add: distinct_map) + qed +qed simp + lemma length_remdups_concat: "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)" by (simp add: distinct_card [symmetric]) @@ -3343,6 +3383,49 @@ "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))" by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons) +lemma remdups_adj_Cons: "remdups_adj (x # xs) = + (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)" + by (induct xs arbitrary: x) (auto split: list.splits) + +lemma remdups_adj_append_two: + "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])" + by (induct xs rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_rev[simp]: "remdups_adj (rev xs) = rev (remdups_adj xs)" + by (induct xs rule: remdups_adj.induct, simp_all add: remdups_adj_append_two) + +lemma remdups_adj_length[simp]: "length (remdups_adj xs) \<le> length xs" + by (induct xs rule: remdups_adj.induct, auto) + +lemma remdups_adj_length_ge1[simp]: "xs \<noteq> [] \<Longrightarrow> length (remdups_adj xs) \<ge> Suc 0" + by (induct xs rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_Nil_iff[simp]: "remdups_adj xs = [] \<longleftrightarrow> xs = []" + by (induct xs rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_set[simp]: "set (remdups_adj xs) = set xs" + by (induct xs rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_Cons_alt[simp]: "x # tl (remdups_adj (x # xs)) = remdups_adj (x # xs)" + by (induct xs rule: remdups_adj.induct, auto) + +lemma remdups_adj_distinct: "distinct xs \<Longrightarrow> remdups_adj xs = xs" + by (induct xs rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_append: + "remdups_adj (xs\<^sub>1 @ x # xs\<^sub>2) = remdups_adj (xs\<^sub>1 @ [x]) @ tl (remdups_adj (x # xs\<^sub>2))" + by (induct xs\<^sub>1 rule: remdups_adj.induct, simp_all) + +lemma remdups_adj_singleton: + "remdups_adj xs = [x] \<Longrightarrow> xs = replicate (length xs) x" + by (induct xs rule: remdups_adj.induct, auto split: split_if_asm) + +lemma remdups_adj_map_injective: + assumes "inj f" + shows "remdups_adj (map f xs) = map f (remdups_adj xs)" + by (induct xs rule: remdups_adj.induct, + auto simp add: injD[OF assms]) + subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} @@ -3396,6 +3479,12 @@ "length (concat xss) = listsum (map length xss)" by (induct xss) simp_all +lemma (in monoid_add) length_product_lists: + "length (product_lists xss) = foldr op * (map length xss) 1" +proof (induct xss) + case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) +qed simp + lemma (in monoid_add) listsum_map_filter: assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" shows "listsum (map f (filter P xs)) = listsum (map f xs)" @@ -4573,6 +4662,10 @@ "sorted l \<Longrightarrow> sorted (remdups l)" by (induct l) (auto simp: sorted_Cons) +lemma sorted_remdups_adj[simp]: + "sorted xs \<Longrightarrow> sorted (remdups_adj xs)" +by (induct xs rule: remdups_adj.induct, simp_all split: split_if_asm add: sorted_Cons) + lemma sorted_distinct_set_unique: assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys" shows "xs = ys" @@ -6462,6 +6555,14 @@ "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip" unfolding zip_def by transfer_prover +lemma product_transfer [transfer_rule]: + "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) List.product List.product" + unfolding List.product_def by transfer_prover + +lemma product_lists_transfer [transfer_rule]: + "(list_all2 (list_all2 A) ===> list_all2 (list_all2 A)) product_lists product_lists" + unfolding product_lists_def by transfer_prover + lemma insert_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A" shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert" @@ -6491,6 +6592,12 @@ shows "(list_all2 A ===> list_all2 A) remdups remdups" unfolding remdups_def by transfer_prover +lemma remdups_adj_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "(list_all2 A ===> list_all2 A) remdups_adj remdups_adj" + proof (rule fun_relI, erule list_all2_induct) + qed (auto simp: remdups_adj_Cons assms[unfolded bi_unique_def] split: list.splits) + lemma replicate_transfer [transfer_rule]: "(op = ===> A ===> list_all2 A) replicate replicate" unfolding replicate_def by transfer_prover