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"