author haftmann Tue Nov 02 16:59:40 2010 +0100 (2010-11-02) changeset 40307 ad053b4e2b6d parent 40306 e4461b9854a5 child 40308 628dc6f24ddf
tuned proof
```     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
```