tuned proof
authorhaftmann
Tue Nov 02 16:48:19 2010 +0100 (2010-11-02)
changeset 40306e4461b9854a5
parent 40305 41833242cc42
child 40307 ad053b4e2b6d
tuned proof
src/HOL/Library/Multiset.thy
     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: