# HG changeset patch
# User haftmann
# Date 1288781429 -3600
# Node ID 58af2b8327b77850b7df9a5ea57ed75836335257
# Parent abc52faa7761eabb46a4c141b7e04dd55608222a
tuned proof
diff -r abc52faa7761 -r 58af2b8327b7 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Nov 03 11:50:29 2010 +0100
@@ -901,30 +901,27 @@
next
fix l
assume "l \ set ?rhs"
- have *: "\x P. P (f x) \ f l = f x \ P (f l) \ f l = f x" by auto
- have **: "\x. f l = f x \ f x = f l" by auto
+ let ?pivot = "f (xs ! (length xs div 2))"
+ have *: "\x. f l = f x \ f x = f l" by auto
have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
- with ** have [simp]: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp
- let ?pivot = "f (xs ! (length xs div 2))"
+ with * have **: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp
+ have "\x P. P (f x) ?pivot \ f l = f x \ P (f l) ?pivot \ f l = f x" by auto
+ then have "\P. [x \ sort_key f xs . P (f x) ?pivot \ f l = f x] =
+ [x \ sort_key f xs. P (f l) ?pivot \ f l = f x]" by simp
+ note *** = this [of "op <"] this [of "op >"] this [of "op ="]
show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
case less then moreover have "f l \ ?pivot" and "\ f l > ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
next
case equal then show ?thesis
- by (auto simp add: ** less_le)
+ by (simp add: * less_le)
next
case greater then moreover have "f l \ ?pivot" and "\ f l < ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
qed
qed