src/HOL/Library/Multiset.thy
changeset 40346 58af2b8327b7
parent 40307 ad053b4e2b6d
child 40347 429bf4388b2f
equal deleted inserted replaced
40320:abc52faa7761 40346:58af2b8327b7
   899   show "sorted (map f ?rhs)"
   899   show "sorted (map f ?rhs)"
   900     by (auto simp add: sorted_append intro: sorted_map_same)
   900     by (auto simp add: sorted_append intro: sorted_map_same)
   901 next
   901 next
   902   fix l
   902   fix l
   903   assume "l \<in> set ?rhs"
   903   assume "l \<in> set ?rhs"
   904   have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto
   904   let ?pivot = "f (xs ! (length xs div 2))"
   905   have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
   905   have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
   906   have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
   906   have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
   907     unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
   907     unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
   908   with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
   908   with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
   909   let ?pivot = "f (xs ! (length xs div 2))"
   909   have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
       
   910   then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
       
   911     [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
       
   912   note *** = this [of "op <"] this [of "op >"] this [of "op ="]
   910   show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
   913   show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
   911   proof (cases "f l" ?pivot rule: linorder_cases)
   914   proof (cases "f l" ?pivot rule: linorder_cases)
   912     case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
   915     case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
   913     ultimately show ?thesis
   916     ultimately show ?thesis
   914       apply (auto simp add: filter_sort [symmetric])
   917       by (simp add: filter_sort [symmetric] ** ***)
   915       apply (subst *) apply simp
       
   916       apply (subst *) apply simp
       
   917       done
       
   918   next
   918   next
   919     case equal then show ?thesis
   919     case equal then show ?thesis
   920       by (auto simp add: ** less_le)
   920       by (simp add: * less_le)
   921   next
   921   next
   922     case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
   922     case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
   923     ultimately show ?thesis
   923     ultimately show ?thesis
   924       apply (auto simp add: filter_sort [symmetric])
   924       by (simp add: filter_sort [symmetric] ** ***)
   925       apply (subst *) apply simp
       
   926       apply (subst *) apply simp
       
   927       done
       
   928   qed
   925   qed
   929 qed
   926 qed
   930 
   927 
   931 lemma sort_by_quicksort:
   928 lemma sort_by_quicksort:
   932   "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
   929   "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]