author haftmann Tue Nov 02 16:48:19 2010 +0100 (2010-11-02) changeset 40306 e4461b9854a5 parent 40305 41833242cc42 child 40307 ad053b4e2b6d
tuned proof
```     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Nov 02 16:36:33 2010 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Nov 02 16:48:19 2010 +0100
1.3 @@ -902,11 +902,12 @@
1.4    fix l
1.5    assume "l \<in> set ?rhs"
1.6    let ?pivot = "f (xs ! (length xs div 2))"
1.7 -  have *: "\<And>x P. P (f x) \<and> f x = f l \<longleftrightarrow> P (f l) \<and> f x = f l" by auto
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 [simp]: "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
1.11 +  have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
1.12      unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
1.13 -  have "[x \<leftarrow> ?rhs. f x = f l] = [x \<leftarrow> ?lhs. f x = f l]"
1.14 +  with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
1.15 +  show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
1.16    proof (cases "f l" ?pivot rule: linorder_cases)
1.17      case less then show ?thesis
1.18        apply (auto simp add: filter_sort [symmetric])
1.19 @@ -915,11 +916,8 @@
1.20        apply (subst *) apply (frule less_not_sym) apply simp
1.21        done
1.22    next
1.23 -    case equal from this [symmetric] show ?thesis
1.24 -      apply (auto simp add: filter_sort [symmetric])
1.25 -      apply (subst *) apply simp
1.26 -      apply (subst *) apply simp
1.27 -      done
1.28 +    case equal then show ?thesis
1.29 +      by (auto simp add: ** less_le)
1.30    next
1.31      case greater then show ?thesis
1.32        apply (auto simp add: filter_sort [symmetric])
1.33 @@ -927,8 +925,7 @@
1.34        apply (frule less_imp_neq) apply simp
1.35        apply (subst *) apply simp
1.36        done
1.37 -  qed
1.38 -  then show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" by (simp add: **)
1.39 +  qed
1.40  qed
1.41
1.42  lemma sort_by_quicksort:
```