author | haftmann |

Fri Sep 17 20:53:50 2010 +0200 (2010-09-17) | |

changeset 39533 | 91a0ff0ff237 |

parent 39532 | fafabbcd808c |

child 39534 | c798d4f1b682 |

generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants

1.1 --- a/src/HOL/Library/Multiset.thy Fri Sep 17 20:13:07 2010 +0200 1.2 +++ b/src/HOL/Library/Multiset.thy Fri Sep 17 20:53:50 2010 +0200 1.3 @@ -779,8 +779,8 @@ 1.4 by (induct xs) (auto simp: add_ac) 1.5 1.6 lemma count_filter: 1.7 - "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]" 1.8 -by (induct xs) auto 1.9 + "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" 1.10 + by (induct xs) auto 1.11 1.12 lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" 1.13 apply (induct ls arbitrary: i) 1.14 @@ -809,12 +809,40 @@ 1.15 by (auto simp add: length_remove1 dest: length_pos_if_in_set) 1.16 qed 1.17 1.18 -lemma (in linorder) multiset_of_insort [simp]: 1.19 - "multiset_of (insort x xs) = {#x#} + multiset_of xs" 1.20 +lemma multiset_of_eq_length_filter: 1.21 + assumes "multiset_of xs = multiset_of ys" 1.22 + shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" 1.23 +proof (cases "z \<in># multiset_of xs") 1.24 + case False 1.25 + moreover have "\<not> z \<in># multiset_of ys" using assms False by simp 1.26 + ultimately show ?thesis by (simp add: count_filter) 1.27 +next 1.28 + case True 1.29 + moreover have "z \<in># multiset_of ys" using assms True by simp 1.30 + show ?thesis using assms proof (induct xs arbitrary: ys) 1.31 + case Nil then show ?case by simp 1.32 + next 1.33 + case (Cons x xs) 1.34 + from `multiset_of (x # xs) = multiset_of ys` [symmetric] 1.35 + have *: "multiset_of xs = multiset_of (remove1 x ys)" 1.36 + and "x \<in> set ys" 1.37 + by (auto simp add: mem_set_multiset_eq) 1.38 + from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps) 1.39 + moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv) 1.40 + ultimately show ?case using `x \<in> set ys` 1.41 + by (simp add: filter_remove1) (auto simp add: length_remove1) 1.42 + qed 1.43 +qed 1.44 + 1.45 +context linorder 1.46 +begin 1.47 + 1.48 +lemma multiset_of_insort_key [simp]: 1.49 + "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs" 1.50 by (induct xs) (simp_all add: ac_simps) 1.51 - 1.52 -lemma (in linorder) multiset_of_sort [simp]: 1.53 - "multiset_of (sort xs) = multiset_of xs" 1.54 + 1.55 +lemma multiset_of_sort_key [simp]: 1.56 + "multiset_of (sort_key k xs) = multiset_of xs" 1.57 by (induct xs) (simp_all add: ac_simps) 1.58 1.59 text {* 1.60 @@ -822,18 +850,42 @@ 1.61 @{text "f"} with @{text "f xs = ys"} behaves like sort. 1.62 *} 1.63 1.64 -lemma (in linorder) properties_for_sort: 1.65 - "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys" 1.66 -proof (induct xs arbitrary: ys) 1.67 +lemma properties_for_sort_key: 1.68 + assumes "multiset_of ys = multiset_of xs" 1.69 + and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs" 1.70 + and "sorted (map f ys)" 1.71 + shows "sort_key f xs = ys" 1.72 +using assms proof (induct xs arbitrary: ys) 1.73 case Nil then show ?case by simp 1.74 next 1.75 case (Cons x xs) 1.76 - then have "x \<in> set ys" 1.77 - by (auto simp add: mem_set_multiset_eq intro!: ccontr) 1.78 - with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case 1.79 - by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) 1.80 + from Cons.prems(2) have 1.81 + "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs" 1.82 + by (simp add: filter_remove1) 1.83 + with Cons.prems have "sort_key f xs = remove1 x ys" 1.84 + by (auto intro!: Cons.hyps simp add: sorted_map_remove1) 1.85 + moreover from Cons.prems have "x \<in> set ys" 1.86 + by (auto simp add: mem_set_multiset_eq intro!: ccontr) 1.87 + ultimately show ?case using Cons.prems by (simp add: insort_key_remove1) 1.88 qed 1.89 1.90 +lemma properties_for_sort: 1.91 + assumes multiset: "multiset_of ys = multiset_of xs" 1.92 + and "sorted ys" 1.93 + shows "sort xs = ys" 1.94 +proof (rule properties_for_sort_key) 1.95 + from multiset show "multiset_of ys = multiset_of xs" . 1.96 + from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp 1.97 + from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" 1.98 + by (rule multiset_of_eq_length_filter) 1.99 + then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k" 1.100 + by simp 1.101 + then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" 1.102 + by (simp add: replicate_length_filter) 1.103 +qed 1.104 + 1.105 +end 1.106 + 1.107 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs" 1.108 by (induct xs) (auto intro: order_trans) 1.109