# HG changeset patch # User haftmann # Date 1266421778 -3600 # Node ID 5163c2d009046b089036e12fd82fdd60b66588de # Parent a6c573d133851e3b2ce6788f10bff185323d167f more lemmas about sort(_key) diff -r a6c573d13385 -r 5163c2d00904 src/HOL/List.thy --- a/src/HOL/List.thy Wed Feb 17 16:49:37 2010 +0100 +++ b/src/HOL/List.thy Wed Feb 17 16:49:38 2010 +0100 @@ -284,9 +284,8 @@ "insort_key f x [] = [x]" | "insort_key f x (y#ys) = (if f x \ f y then (x#y#ys) else y#(insort_key f x ys))" -primrec sort_key :: "('b \ 'a) \ 'b list \ 'b list" where -"sort_key f [] = []" | -"sort_key f (x#xs) = insort_key f x (sort_key f xs)" +definition sort_key :: "('b \ 'a) \ 'b list \ 'b list" where +"sort_key f xs = foldr (insort_key f) xs []" abbreviation "sort \ sort_key (\x. x)" abbreviation "insort \ insort_key (\x. x)" @@ -2266,6 +2265,12 @@ ==> foldr f l a = foldr g k b" by (induct k arbitrary: a b l) simp_all +lemma foldl_fun_comm: + assumes "\x y s. f (f s x) y = f (f s y) x" + shows "f (foldl f s xs) x = foldl f (f s x) xs" + by (induct xs arbitrary: s) + (simp_all add: assms) + lemma (in semigroup_add) foldl_assoc: shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)" by (induct zs arbitrary: y) (simp_all add:add_assoc) @@ -2274,6 +2279,15 @@ shows "x + (foldl op+ 0 zs) = foldl op+ x zs" by (induct zs) (simp_all add:foldl_assoc) +lemma foldl_rev: + assumes "\x y s. f (f s x) y = f (f s y) x" + shows "foldl f s (rev xs) = foldl f s xs" +proof (induct xs arbitrary: s) + case Nil then show ?case by simp +next + case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) +qed + text{* The ``First Duality Theorem'' in Bird \& Wadler: *} @@ -2342,6 +2356,10 @@ text {* @{const Finite_Set.fold} and @{const foldl} *} +lemma (in fun_left_comm) fold_set_remdups: + "fold f y (set xs) = foldl (\y x. f x y) y (remdups xs)" + by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) + lemma (in fun_left_comm_idem) fold_set: "fold f y (set xs) = foldl (\y x. f x y) y xs" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) @@ -3438,6 +3456,24 @@ lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)" by (induct xs, auto) +lemma insort_left_comm: + "insort x (insort y xs) = insort y (insort x xs)" + by (induct xs) auto + +lemma fun_left_comm_insort: + "fun_left_comm insort" +proof +qed (fact insort_left_comm) + +lemma sort_key_simps [simp]: + "sort_key f [] = []" + "sort_key f (x#xs) = insort_key f x (sort_key f xs)" + by (simp_all add: sort_key_def) + +lemma sort_foldl_insort: + "sort xs = foldl (\ys x. insort x ys) [] xs" + by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm) + lemma length_sort[simp]: "length (sort_key f xs) = length xs" by (induct xs, auto) @@ -3800,27 +3836,35 @@ sets to lists but one should convert in the other direction (via @{const set}). *} - context linorder begin -definition - sorted_list_of_set :: "'a set \ 'a list" where - [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs" - -lemma sorted_list_of_set[simp]: "finite A \ - set(sorted_list_of_set A) = A & - sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)" -apply(simp add:sorted_list_of_set_def) -apply(rule the1I2) - apply(simp_all add: finite_sorted_distinct_unique) -done - -lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []" -unfolding sorted_list_of_set_def -apply(subst the_equality[of _ "[]"]) -apply simp_all -done +definition sorted_list_of_set :: "'a set \ 'a list" where + "sorted_list_of_set = Finite_Set.fold insort []" + +lemma sorted_list_of_set_empty [simp]: + "sorted_list_of_set {} = []" + by (simp add: sorted_list_of_set_def) + +lemma sorted_list_of_set_insert [simp]: + assumes "finite A" + shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))" +proof - + interpret fun_left_comm insort by (fact fun_left_comm_insort) + with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove) +qed + +lemma sorted_list_of_set [simp]: + "finite A \ set (sorted_list_of_set A) = A \ sorted (sorted_list_of_set A) + \ distinct (sorted_list_of_set A)" + by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort) + +lemma sorted_list_of_set_sort_remdups: + "sorted_list_of_set (set xs) = sort (remdups xs)" +proof - + interpret fun_left_comm insort by (fact fun_left_comm_insort) + show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups) +qed end