summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Multiset.thy

changeset 48012 | b6e5e86a7303 |

parent 48011 | 391439b10100 |

child 48023 | 6dfe5e774012 |

1.1 --- a/src/HOL/Library/Multiset.thy Tue May 29 11:30:13 2012 +0200 1.2 +++ b/src/HOL/Library/Multiset.thy Tue May 29 11:41:37 2012 +0200 1.3 @@ -682,6 +682,9 @@ 1.4 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)" 1.5 by (induct xs) auto 1.6 1.7 +lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs" 1.8 + by (induct xs) simp_all 1.9 + 1.10 lemma multiset_of_append [simp]: 1.11 "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 1.12 by (induct xs arbitrary: ys) (auto simp: add_ac) 1.13 @@ -755,45 +758,12 @@ 1.14 lemma multiset_of_eq_length: 1.15 assumes "multiset_of xs = multiset_of ys" 1.16 shows "length xs = length ys" 1.17 -using assms 1.18 -proof (induct xs arbitrary: ys) 1.19 - case Nil then show ?case by simp 1.20 -next 1.21 - case (Cons x xs) 1.22 - then have "x \<in># multiset_of ys" by (simp add: union_single_eq_member) 1.23 - then have "x \<in> set ys" by (simp add: in_multiset_in_set) 1.24 - from Cons.prems [symmetric] have "multiset_of xs = multiset_of (remove1 x ys)" 1.25 - by simp 1.26 - with Cons.hyps have "length xs = length (remove1 x ys)" . 1.27 - with `x \<in> set ys` show ?case 1.28 - by (auto simp add: length_remove1 dest: length_pos_if_in_set) 1.29 -qed 1.30 + using assms by (metis size_multiset_of) 1.31 1.32 lemma multiset_of_eq_length_filter: 1.33 assumes "multiset_of xs = multiset_of ys" 1.34 shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" 1.35 -proof (cases "z \<in># multiset_of xs") 1.36 - case False 1.37 - moreover have "\<not> z \<in># multiset_of ys" using assms False by simp 1.38 - ultimately show ?thesis by (simp add: count_multiset_of_length_filter) 1.39 -next 1.40 - case True 1.41 - moreover have "z \<in># multiset_of ys" using assms True by simp 1.42 - show ?thesis using assms 1.43 - proof (induct xs arbitrary: ys) 1.44 - case Nil then show ?case by simp 1.45 - next 1.46 - case (Cons x xs) 1.47 - from `multiset_of (x # xs) = multiset_of ys` [symmetric] 1.48 - have *: "multiset_of xs = multiset_of (remove1 x ys)" 1.49 - and "x \<in> set ys" 1.50 - by (auto simp add: mem_set_multiset_eq) 1.51 - from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps) 1.52 - moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv) 1.53 - ultimately show ?case using `x \<in> set ys` 1.54 - by (simp add: filter_remove1) (auto simp add: length_remove1) 1.55 - qed 1.56 -qed 1.57 + using assms by (metis count_multiset_of) 1.58 1.59 lemma fold_multiset_equiv: 1.60 assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"