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 let ?pivot = "f (xs ! (length xs div 2))" |
904 let ?pivot = "f (xs ! (length xs div 2))" |
905 have *: "\<And>x P. P (f x) \<and> f x = f l \<longleftrightarrow> P (f l) \<and> f x = f l" by auto |
905 have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto |
906 have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto |
906 have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto |
907 have [simp]: "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]" |
907 have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]" |
908 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
908 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
909 have "[x \<leftarrow> ?rhs. f x = f l] = [x \<leftarrow> ?lhs. f x = f l]" |
909 with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp |
|
910 show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" |
910 proof (cases "f l" ?pivot rule: linorder_cases) |
911 proof (cases "f l" ?pivot rule: linorder_cases) |
911 case less then show ?thesis |
912 case less then show ?thesis |
912 apply (auto simp add: filter_sort [symmetric]) |
913 apply (auto simp add: filter_sort [symmetric]) |
913 apply (subst *) apply simp |
914 apply (subst *) apply simp |
914 apply (frule less_imp_neq) apply simp |
915 apply (frule less_imp_neq) apply simp |
915 apply (subst *) apply (frule less_not_sym) apply simp |
916 apply (subst *) apply (frule less_not_sym) apply simp |
916 done |
917 done |
917 next |
918 next |
918 case equal from this [symmetric] show ?thesis |
919 case equal then show ?thesis |
919 apply (auto simp add: filter_sort [symmetric]) |
920 by (auto simp add: ** less_le) |
920 apply (subst *) apply simp |
|
921 apply (subst *) apply simp |
|
922 done |
|
923 next |
921 next |
924 case greater then show ?thesis |
922 case greater then show ?thesis |
925 apply (auto simp add: filter_sort [symmetric]) |
923 apply (auto simp add: filter_sort [symmetric]) |
926 apply (subst *) apply (frule less_not_sym) apply simp |
924 apply (subst *) apply (frule less_not_sym) apply simp |
927 apply (frule less_imp_neq) apply simp |
925 apply (frule less_imp_neq) apply simp |
928 apply (subst *) apply simp |
926 apply (subst *) apply simp |
929 done |
927 done |
930 qed |
928 qed |
931 then show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" by (simp add: **) |
|
932 qed |
929 qed |
933 |
930 |
934 lemma sort_by_quicksort: |
931 lemma sort_by_quicksort: |
935 "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)] |
932 "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)] |
936 @ [x\<leftarrow>xs. x = xs ! (length xs div 2)] |
933 @ [x\<leftarrow>xs. x = xs ! (length xs div 2)] |