generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
authorhaftmann
Fri Sep 17 20:53:50 2010 +0200 (2010-09-17)
changeset 3953391a0ff0ff237
parent 39532 fafabbcd808c
child 39534 c798d4f1b682
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
src/HOL/Library/Multiset.thy
     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