--- a/src/HOL/Library/Multiset.thy Tue Nov 02 16:48:19 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Nov 02 16:59:40 2010 +0100
@@ -901,28 +901,28 @@
next
fix l
assume "l \<in> set ?rhs"
- let ?pivot = "f (xs ! (length xs div 2))"
have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto
have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
+ let ?pivot = "f (xs ! (length xs div 2))"
show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
- case less then show ?thesis
+ case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
+ ultimately show ?thesis
apply (auto simp add: filter_sort [symmetric])
apply (subst *) apply simp
- apply (frule less_imp_neq) apply simp
- apply (subst *) apply (frule less_not_sym) apply simp
+ apply (subst *) apply simp
done
next
case equal then show ?thesis
by (auto simp add: ** less_le)
next
- case greater then show ?thesis
+ case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
+ ultimately show ?thesis
apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply (frule less_not_sym) apply simp
- apply (frule less_imp_neq) apply simp
+ apply (subst *) apply simp
apply (subst *) apply simp
done
qed