src/HOL/Library/Multiset.thy
changeset 40305 41833242cc42
parent 40303 2d507370e879
child 40306 e4461b9854a5
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Nov 02 16:31:57 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Nov 02 16:36:33 2010 +0100
     1.3 @@ -856,7 +856,7 @@
     1.4  
     1.5  lemma properties_for_sort_key:
     1.6    assumes "multiset_of ys = multiset_of xs"
     1.7 -  and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs"
     1.8 +  and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
     1.9    and "sorted (map f ys)"
    1.10    shows "sort_key f xs = ys"
    1.11  using assms proof (induct xs arbitrary: ys)
    1.12 @@ -864,7 +864,7 @@
    1.13  next
    1.14    case (Cons x xs)
    1.15    from Cons.prems(2) have
    1.16 -    "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs"
    1.17 +    "\<forall>k \<in> set ys. filter (\<lambda>x. f k = f x) (remove1 x ys) = filter (\<lambda>x. f k = f x) xs"
    1.18      by (simp add: filter_remove1)
    1.19    with Cons.prems have "sort_key f xs = remove1 x ys"
    1.20      by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
    1.21 @@ -884,7 +884,7 @@
    1.22      by (rule multiset_of_eq_length_filter)
    1.23    then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
    1.24      by simp
    1.25 -  then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
    1.26 +  then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
    1.27      by (simp add: replicate_length_filter)
    1.28  qed
    1.29  
    1.30 @@ -899,40 +899,36 @@
    1.31    show "sorted (map f ?rhs)"
    1.32      by (auto simp add: sorted_append intro: sorted_map_same)
    1.33  next
    1.34 -  show "\<forall>k\<in> f ` set ?rhs. [x \<leftarrow> ?rhs. k = f x] = [x \<leftarrow> ?lhs. k = f x]"
    1.35 -  proof
    1.36 -    let ?pivot = "f (xs ! (length xs div 2))"
    1.37 -    fix k
    1.38 -    assume k: "k \<in> f ` set ?rhs"
    1.39 -    then obtain l where f_l: "k = f l" by blast
    1.40 -    have *: "\<And>x P. P (f x) \<and> f x = f l \<longleftrightarrow> P (f l) \<and> f x = f l" by auto
    1.41 -    have **: "\<And>x. k = f x \<longleftrightarrow> f x = k" by auto
    1.42 -    have [simp]: "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
    1.43 -      unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
    1.44 -    have "[x \<leftarrow> ?rhs. f x = k] = [x \<leftarrow> ?lhs. f x = k]"
    1.45 -    proof (cases "f l" ?pivot rule: linorder_cases)
    1.46 -      case less then show ?thesis
    1.47 -        apply (auto simp add: filter_sort [symmetric] f_l)
    1.48 -        apply (subst *) apply simp
    1.49 -        apply (frule less_imp_neq) apply simp
    1.50 -        apply (subst *) apply (frule less_not_sym) apply simp
    1.51 -        done
    1.52 -    next
    1.53 -      case equal from this [symmetric] show ?thesis 
    1.54 -        apply (auto simp add: filter_sort [symmetric] f_l)
    1.55 -        apply (subst *) apply simp
    1.56 -        apply (subst *) apply simp
    1.57 -        done
    1.58 -    next
    1.59 -      case greater then show ?thesis
    1.60 -        apply (auto simp add: filter_sort [symmetric] f_l)
    1.61 -        apply (subst *) apply (frule less_not_sym) apply simp
    1.62 -        apply (frule less_imp_neq) apply simp
    1.63 -        apply (subst *) apply simp
    1.64 -        done
    1.65 -    qed      
    1.66 -    then show "[x \<leftarrow> ?rhs. k = f x] = [x \<leftarrow> ?lhs. k = f x]" by (simp add: **)
    1.67 -  qed
    1.68 +  fix l
    1.69 +  assume "l \<in> set ?rhs"
    1.70 +  let ?pivot = "f (xs ! (length xs div 2))"
    1.71 +  have *: "\<And>x P. P (f x) \<and> f x = f l \<longleftrightarrow> P (f l) \<and> f x = f l" by auto
    1.72 +  have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
    1.73 +  have [simp]: "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
    1.74 +    unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
    1.75 +  have "[x \<leftarrow> ?rhs. f x = f l] = [x \<leftarrow> ?lhs. f x = f l]"
    1.76 +  proof (cases "f l" ?pivot rule: linorder_cases)
    1.77 +    case less then show ?thesis
    1.78 +      apply (auto simp add: filter_sort [symmetric])
    1.79 +      apply (subst *) apply simp
    1.80 +      apply (frule less_imp_neq) apply simp
    1.81 +      apply (subst *) apply (frule less_not_sym) apply simp
    1.82 +      done
    1.83 +  next
    1.84 +    case equal from this [symmetric] show ?thesis 
    1.85 +      apply (auto simp add: filter_sort [symmetric])
    1.86 +      apply (subst *) apply simp
    1.87 +      apply (subst *) apply simp
    1.88 +      done
    1.89 +  next
    1.90 +    case greater then show ?thesis
    1.91 +      apply (auto simp add: filter_sort [symmetric])
    1.92 +      apply (subst *) apply (frule less_not_sym) apply simp
    1.93 +      apply (frule less_imp_neq) apply simp
    1.94 +      apply (subst *) apply simp
    1.95 +      done
    1.96 +  qed      
    1.97 +  then show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" by (simp add: **)
    1.98  qed
    1.99  
   1.100  lemma sort_by_quicksort: