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)] 