summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 17 Sep 2010 20:53:50 +0200 | |

changeset 39533 | 91a0ff0ff237 |

parent 39532 | fafabbcd808c |

child 39534 | c798d4f1b682 |

generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants

--- a/src/HOL/Library/Multiset.thy Fri Sep 17 20:13:07 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Sep 17 20:53:50 2010 +0200 @@ -779,8 +779,8 @@ by (induct xs) (auto simp: add_ac) lemma count_filter: - "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]" -by (induct xs) auto + "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" + by (induct xs) auto lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" apply (induct ls arbitrary: i) @@ -809,12 +809,40 @@ by (auto simp add: length_remove1 dest: length_pos_if_in_set) qed -lemma (in linorder) multiset_of_insort [simp]: - "multiset_of (insort x xs) = {#x#} + multiset_of xs" +lemma multiset_of_eq_length_filter: + assumes "multiset_of xs = multiset_of ys" + shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" +proof (cases "z \<in># multiset_of xs") + case False + moreover have "\<not> z \<in># multiset_of ys" using assms False by simp + ultimately show ?thesis by (simp add: count_filter) +next + case True + moreover have "z \<in># multiset_of ys" using assms True by simp + show ?thesis using assms proof (induct xs arbitrary: ys) + case Nil then show ?case by simp + next + case (Cons x xs) + from `multiset_of (x # xs) = multiset_of ys` [symmetric] + have *: "multiset_of xs = multiset_of (remove1 x ys)" + and "x \<in> set ys" + by (auto simp add: mem_set_multiset_eq) + from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps) + moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv) + ultimately show ?case using `x \<in> set ys` + by (simp add: filter_remove1) (auto simp add: length_remove1) + qed +qed + +context linorder +begin + +lemma multiset_of_insort_key [simp]: + "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" by (induct xs) (simp_all add: ac_simps) - -lemma (in linorder) multiset_of_sort [simp]: - "multiset_of (sort xs) = multiset_of xs" + +lemma multiset_of_sort_key [simp]: + "multiset_of (sort_key k xs) = multiset_of xs" by (induct xs) (simp_all add: ac_simps) text {* @@ -822,18 +850,42 @@ @{text "f"} with @{text "f xs = ys"} behaves like sort. *} -lemma (in linorder) properties_for_sort: - "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys" -proof (induct xs arbitrary: ys) +lemma properties_for_sort_key: + assumes "multiset_of ys = multiset_of xs" + and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs" + and "sorted (map f ys)" + shows "sort_key f xs = ys" +using assms proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) - then have "x \<in> set ys" - by (auto simp add: mem_set_multiset_eq intro!: ccontr) - with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case - by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) + from Cons.prems(2) have + "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs" + by (simp add: filter_remove1) + with Cons.prems have "sort_key f xs = remove1 x ys" + by (auto intro!: Cons.hyps simp add: sorted_map_remove1) + moreover from Cons.prems have "x \<in> set ys" + by (auto simp add: mem_set_multiset_eq intro!: ccontr) + ultimately show ?case using Cons.prems by (simp add: insort_key_remove1) qed +lemma properties_for_sort: + assumes multiset: "multiset_of ys = multiset_of xs" + and "sorted ys" + shows "sort xs = ys" +proof (rule properties_for_sort_key) + from multiset show "multiset_of ys = multiset_of xs" . + from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp + from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" + by (rule multiset_of_eq_length_filter) + then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k" + by simp + then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" + by (simp add: replicate_length_filter) +qed + +end + lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs" by (induct xs) (auto intro: order_trans)