# HG changeset patch # User haftmann # Date 1288190434 -7200 # Node ID 43916ac560a4e6e0f77e9e2d2cbac614caaeb9b9 # Parent 8ec474f94d6184d37ee9dd941f988d3e52f04f27# Parent aee7ef725330da363dd7d73608b09df331f2e23d merged diff -r 8ec474f94d61 -r 43916ac560a4 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Oct 27 13:46:30 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Wed Oct 27 16:40:34 2010 +0200 @@ -837,11 +837,11 @@ context linorder begin -lemma multiset_of_insort_key [simp]: +lemma multiset_of_insort [simp]: "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" by (induct xs) (simp_all add: ac_simps) -lemma multiset_of_sort_key [simp]: +lemma multiset_of_sort [simp]: "multiset_of (sort_key k xs) = multiset_of xs" by (induct xs) (simp_all add: ac_simps) diff -r 8ec474f94d61 -r 43916ac560a4 src/HOL/List.thy --- a/src/HOL/List.thy Wed Oct 27 13:46:30 2010 +0200 +++ b/src/HOL/List.thy Wed Oct 27 16:40:34 2010 +0200 @@ -303,11 +303,12 @@ definition sort_key :: "('b \ 'a) \ 'b list \ 'b list" where "sort_key f xs = foldr (insort_key f) xs []" +definition insort_insert_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where + "insort_insert_key f x xs = (if f x \ f ` set xs then xs else insort_key f x xs)" + abbreviation "sort \ sort_key (\x. x)" abbreviation "insort \ insort_key (\x. x)" - -definition insort_insert :: "'a \ 'a list \ 'a list" where - "insort_insert x xs = (if x \ set xs then xs else insort x xs)" +abbreviation "insort_insert \ insort_insert_key (\x. x)" end @@ -757,6 +758,14 @@ subsubsection {* @{text map} *} +lemma hd_map: + "xs \ [] \ hd (map f xs) = f (hd xs)" + by (cases xs) simp_all + +lemma map_tl: + "map f (tl xs) = tl (map f xs)" + by (cases xs) simp_all + lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs" by (induct xs) simp_all @@ -2669,6 +2678,10 @@ subsubsection {* @{text "distinct"} and @{text remdups} *} +lemma distinct_tl: + "distinct xs \ distinct (tl xs)" + by (cases xs) simp_all + lemma distinct_append [simp]: "distinct (xs @ ys) = (distinct xs \ distinct ys \ set xs \ set ys = {})" by (induct xs) auto @@ -3629,12 +3642,18 @@ context linorder begin -lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)" -by (induct xs, auto) +lemma length_insort [simp]: + "length (insort_key f x xs) = Suc (length xs)" + by (induct xs) simp_all + +lemma insort_key_left_comm: + assumes "f x \ f y" + shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)" + by (induct xs) (auto simp add: assms dest: antisym) lemma insort_left_comm: "insort x (insort y xs) = insort y (insort x xs)" - by (induct xs) auto + by (cases "x = y") (auto intro: insort_key_left_comm) lemma fun_left_comm_insort: "fun_left_comm insort" @@ -3657,6 +3676,10 @@ apply(induct xs arbitrary: x) apply simp by simp (blast intro: order_trans) +lemma sorted_tl: + "sorted xs \ sorted (tl xs)" + by (cases xs) (simp_all add: sorted_Cons) + lemma sorted_append: "sorted (xs@ys) = (sorted xs & sorted ys & (\x \ set xs. \y \ set ys. x\y))" by (induct xs) (auto simp add:sorted_Cons) @@ -3712,16 +3735,16 @@ by(induct xs)(simp_all add:distinct_insort set_sort) lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)" -by(induct xs)(auto simp:sorted_Cons set_insort) + by (induct xs) (auto simp:sorted_Cons set_insort) lemma sorted_insort: "sorted (insort x xs) = sorted xs" -using sorted_insort_key[where f="\x. x"] by simp - -theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))" -by(induct xs)(auto simp:sorted_insort_key) - -theorem sorted_sort[simp]: "sorted (sort xs)" -by(induct xs)(auto simp:sorted_insort) + using sorted_insort_key [where f="\x. x"] by simp + +theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))" + by (induct xs) (auto simp:sorted_insort_key) + +theorem sorted_sort [simp]: "sorted (sort xs)" + using sorted_sort_key [where f="\x. x"] by simp lemma sorted_butlast: assumes "xs \ []" and "sorted xs" @@ -3870,32 +3893,53 @@ finally show "\ t < f x" by simp qed +lemma insort_insert_key_triv: + "f x \ f ` set xs \ insort_insert_key f x xs = xs" + by (simp add: insort_insert_key_def) + +lemma insort_insert_triv: + "x \ set xs \ insort_insert x xs = xs" + using insort_insert_key_triv [of "\x. x"] by simp + +lemma insort_insert_insort_key: + "f x \ f ` set xs \ insort_insert_key f x xs = insort_key f x xs" + by (simp add: insort_insert_key_def) + +lemma insort_insert_insort: + "x \ set xs \ insort_insert x xs = insort x xs" + using insort_insert_insort_key [of "\x. x"] by simp + lemma set_insort_insert: "set (insort_insert x xs) = insert x (set xs)" - by (auto simp add: insort_insert_def set_insort) + by (auto simp add: insort_insert_key_def set_insort) lemma distinct_insort_insert: assumes "distinct xs" - shows "distinct (insort_insert x xs)" - using assms by (induct xs) (auto simp add: insort_insert_def set_insort) + shows "distinct (insort_insert_key f x xs)" + using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort) + +lemma sorted_insort_insert_key: + assumes "sorted (map f xs)" + shows "sorted (map f (insort_insert_key f x xs))" + using assms by (simp add: insort_insert_key_def sorted_insort_key) lemma sorted_insort_insert: assumes "sorted xs" shows "sorted (insort_insert x xs)" - using assms by (simp add: insort_insert_def sorted_insort) - -lemma filter_insort_key_triv: + using assms sorted_insort_insert_key [of "\x. x"] by simp + +lemma filter_insort_triv: "\ P x \ filter P (insort_key f x xs) = filter P xs" by (induct xs) simp_all -lemma filter_insort_key: +lemma filter_insort: "sorted (map f xs) \ P x \ filter P (insort_key f x xs) = insort_key f x (filter P xs)" using assms by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto) -lemma filter_sort_key: +lemma filter_sort: "filter P (sort_key f xs) = sort_key f (filter P xs)" - by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key) + by (induct xs) (simp_all add: filter_insort_triv filter_insort) lemma sorted_same [simp]: "sorted [x\xs. x = f xs]"