src/HOL/Library/Multiset.thy
changeset 40307 ad053b4e2b6d
parent 40306 e4461b9854a5
child 40346 58af2b8327b7
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Nov 02 16:48:19 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Nov 02 16:59:40 2010 +0100
     1.3 @@ -901,28 +901,28 @@
     1.4  next
     1.5    fix l
     1.6    assume "l \<in> set ?rhs"
     1.7 -  let ?pivot = "f (xs ! (length xs div 2))"
     1.8    have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto
     1.9    have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
    1.10    have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
    1.11      unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
    1.12    with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
    1.13 +  let ?pivot = "f (xs ! (length xs div 2))"
    1.14    show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
    1.15    proof (cases "f l" ?pivot rule: linorder_cases)
    1.16 -    case less then show ?thesis
    1.17 +    case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
    1.18 +    ultimately show ?thesis
    1.19        apply (auto simp add: filter_sort [symmetric])
    1.20        apply (subst *) apply simp
    1.21 -      apply (frule less_imp_neq) apply simp
    1.22 -      apply (subst *) apply (frule less_not_sym) apply simp
    1.23 +      apply (subst *) apply simp
    1.24        done
    1.25    next
    1.26      case equal then show ?thesis
    1.27        by (auto simp add: ** less_le)
    1.28    next
    1.29 -    case greater then show ?thesis
    1.30 +    case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
    1.31 +    ultimately show ?thesis
    1.32        apply (auto simp add: filter_sort [symmetric])
    1.33 -      apply (subst *) apply (frule less_not_sym) apply simp
    1.34 -      apply (frule less_imp_neq) apply simp
    1.35 +      apply (subst *) apply simp
    1.36        apply (subst *) apply simp
    1.37        done
    1.38    qed