2580 proof (rule properties_for_sort_key) |
2580 proof (rule properties_for_sort_key) |
2581 from mset_equal |
2581 from mset_equal |
2582 show "mset ys = mset xs" by simp |
2582 show "mset ys = mset xs" by simp |
2583 from \<open>sorted (map f ys)\<close> |
2583 from \<open>sorted (map f ys)\<close> |
2584 show "sorted (map f ys)" . |
2584 show "sorted (map f ys)" . |
2585 show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k |
2585 show "filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" if "k \<in> set ys" for k |
2586 proof - |
2586 proof - |
2587 from mset_equal |
2587 from mset_equal |
2588 have set_equal: "set xs = set ys" by (rule mset_eq_setD) |
2588 have set_equal: "set xs = set ys" by (rule mset_eq_setD) |
2589 with that have "insert k (set ys) = set ys" by auto |
2589 with that have "insert k (set ys) = set ys" by auto |
2590 with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))" |
2590 with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))" |
2591 by (simp add: set_equal) |
2591 by (simp add: set_equal) |
2592 from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys" |
2592 from inj have "filter (\<lambda>x. f k = f x) ys = filter (HOL.eq k) ys" |
2593 by (auto intro!: inj_on_filter_key_eq) |
2593 by (auto intro!: inj_on_filter_key_eq) |
2594 also have "\<dots> = replicate (count (mset ys) k) k" |
2594 also have "\<dots> = replicate (count (mset ys) k) k" |
2595 by (simp add: replicate_count_mset_eq_filter_eq) |
2595 by (simp add: replicate_count_mset_eq_filter_eq) |
2596 also have "\<dots> = replicate (count (mset xs) k) k" |
2596 also have "\<dots> = replicate (count (mset xs) k) k" |
2597 using mset_equal by simp |
2597 using mset_equal by simp |
2598 also have "\<dots> = filter (HOL.eq k) xs" |
2598 also have "\<dots> = filter (HOL.eq k) xs" |
2599 by (simp add: replicate_count_mset_eq_filter_eq) |
2599 by (simp add: replicate_count_mset_eq_filter_eq) |
2600 also have "\<dots> = [x\<leftarrow>xs . f k = f x]" |
2600 also have "\<dots> = filter (\<lambda>x. f k = f x) xs" |
2601 using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal) |
2601 using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal) |
2602 finally show ?thesis . |
2602 finally show ?thesis . |
2603 qed |
2603 qed |
2604 qed |
2604 qed |
2605 |
2605 |
2608 and "inj_on f (set xs)" |
2608 and "inj_on f (set xs)" |
2609 shows "sort_key f xs = sort_key f ys" |
2609 shows "sort_key f xs = sort_key f ys" |
2610 by (rule sort_key_inj_key_eq) (simp_all add: assms) |
2610 by (rule sort_key_inj_key_eq) (simp_all add: assms) |
2611 |
2611 |
2612 lemma sort_key_by_quicksort: |
2612 lemma sort_key_by_quicksort: |
2613 "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))] |
2613 "sort_key f xs = sort_key f (filter (\<lambda>x. f x < f (xs ! (length xs div 2))) xs) |
2614 @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))] |
2614 @ filter (\<lambda>x. f x = f (xs ! (length xs div 2))) xs |
2615 @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs") |
2615 @ sort_key f (filter (\<lambda>x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs") |
2616 proof (rule properties_for_sort_key) |
2616 proof (rule properties_for_sort_key) |
2617 show "mset ?rhs = mset ?lhs" |
2617 show "mset ?rhs = mset ?lhs" |
2618 by (rule multiset_eqI) (auto simp add: mset_filter) |
2618 by (rule multiset_eqI) (auto simp add: mset_filter) |
2619 show "sorted (map f ?rhs)" |
2619 show "sorted (map f ?rhs)" |
2620 by (auto simp add: sorted_append intro: sorted_map_same) |
2620 by (auto simp add: sorted_append intro: sorted_map_same) |
2621 next |
2621 next |
2622 fix l |
2622 fix l |
2623 assume "l \<in> set ?rhs" |
2623 assume "l \<in> set ?rhs" |
2624 let ?pivot = "f (xs ! (length xs div 2))" |
2624 let ?pivot = "f (xs ! (length xs div 2))" |
2625 have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto |
2625 have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto |
2626 have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]" |
2626 have "filter (\<lambda>x. f x = f l) (sort_key f xs) = filter (\<lambda>x. f x = f l) xs" |
2627 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
2627 unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) |
2628 with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp |
2628 with * have **: "filter (\<lambda>x. f l = f x) (sort_key f xs) = filter (\<lambda>x. f l = f x) xs" by simp |
2629 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 |
2629 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 |
2630 then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] = |
2630 then have "\<And>P. filter (\<lambda>x. P (f x) ?pivot \<and> f l = f x) (sort_key f xs) = |
2631 [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp |
2631 filter (\<lambda>x. P (f l) ?pivot \<and> f l = f x) (sort_key f xs)" by simp |
2632 note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"] |
2632 note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"] |
2633 show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" |
2633 show "filter (\<lambda>x. f l = f x) ?rhs = filter (\<lambda>x. f l = f x) ?lhs" |
2634 proof (cases "f l" ?pivot rule: linorder_cases) |
2634 proof (cases "f l" ?pivot rule: linorder_cases) |
2635 case less |
2635 case less |
2636 then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto |
2636 then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto |
2637 with less show ?thesis |
2637 with less show ?thesis |
2638 by (simp add: filter_sort [symmetric] ** ***) |
2638 by (simp add: filter_sort [symmetric] ** ***) |
2646 by (simp add: filter_sort [symmetric] ** ***) |
2646 by (simp add: filter_sort [symmetric] ** ***) |
2647 qed |
2647 qed |
2648 qed |
2648 qed |
2649 |
2649 |
2650 lemma sort_by_quicksort: |
2650 lemma sort_by_quicksort: |
2651 "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)] |
2651 "sort xs = sort (filter (\<lambda>x. x < xs ! (length xs div 2)) xs) |
2652 @ [x\<leftarrow>xs. x = xs ! (length xs div 2)] |
2652 @ filter (\<lambda>x. x = xs ! (length xs div 2)) xs |
2653 @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") |
2653 @ sort (filter (\<lambda>x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs") |
2654 using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp |
2654 using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp |
2655 |
2655 |
2656 text \<open>A stable parametrized quicksort\<close> |
2656 text \<open>A stable parametrized quicksort\<close> |
2657 |
2657 |
2658 definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where |
2658 definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where |
2659 "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])" |
2659 "part f pivot xs = (filter (\<lambda>x. f x < pivot) xs, filter (\<lambda>x. f x = pivot) xs, filter (\<lambda>x. f x > pivot) xs)" |
2660 |
2660 |
2661 lemma part_code [code]: |
2661 lemma part_code [code]: |
2662 "part f pivot [] = ([], [], [])" |
2662 "part f pivot [] = ([], [], [])" |
2663 "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in |
2663 "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in |
2664 if x' < pivot then (x # lts, eqs, gts) |
2664 if x' < pivot then (x # lts, eqs, gts) |