Theory Examples.Sorting_Final_insertion

theory Sorting_Final_insertion_Sort imports Sorting_Quicksort_Scheme Sorting_Unguarded_Insertion_Sort begin context weak_ordering begin definition "final_insertion_sort xs ≡ doN { ASSERT (1 < length xs); if length xs ≤ is_threshold then gen_insertion_sort True 1 (length xs) xs else doN { xs ← gen_insertion_sort True 1 is_threshold xs; gen_insertion_sort False is_threshold (length xs) xs } }" lemma transfer_guard_over_initial_sorting: assumes PS: "part_sorted_wrt (le_by_lt (<)) n xs" assumes B: "length xs' = length xs" "0<n" "n ≤ i" "i < length xs" assumes DEQ: "drop n xs' = drop n xs" assumes SORTED: "sort_spec (<) (slice 0 n xs) (slice 0 n xs')" assumes LT: "xs' ! i < xs' ! 0" shows False proof - from part_sorted_guardedI[OF PS ‹n≤i› ‹i < length xs›] have GUARD: "xs!0 ≤ xs!i" by (auto simp: le_by_lt) have [simp]: "xs!i = xs'!i" using B DEQ by (metis atLeastLessThan_iff conv_idxs_to_drop_eq) have "xs!0 ∈# mset (slice 0 n xs)" using B apply (auto simp: Misc.slice_def) by (metis atLeast0LessThan image_eqI le_less_trans lessThan_iff less_imp_le_nat nth_image) hence "xs!0 ∈# mset (slice 0 n xs')" using SORTED unfolding sort_spec_def by auto then obtain j where "j<n" and [simp]: "xs!0=xs'!j" using B by (auto simp: in_set_conv_nth slice_nth) have "xs'!0 ≤ xs'!j" using SORTED B ‹j<n› apply (cases "j=0") apply simp unfolding sort_spec_def by (auto simp: le_by_lt sorted_wrt_iff_nth_less slice_nth) then show False using LT GUARD apply simp using local.trans wo_leD by blast qed lemma final_insertion_sort_correct: "⟦part_sorted_wrt (le_by_lt (<)) is_threshold xs; 1 < length xs⟧ ⟹ final_insertion_sort xs ≤ SPEC (sort_spec (<) xs)" unfolding final_insertion_sort_def apply (refine_vcg gen_insertion_sort_correct[THEN order_trans]) apply simp_all subgoal apply (rule sorted_wrt01) by auto subgoal unfolding slice_sort_spec_def apply refine_vcg apply (auto simp: ) using slice_complete by metis subgoal apply (rule sorted_wrt01) by auto subgoal unfolding slice_sort_spec_def apply (refine_vcg gen_insertion_sort_correct[THEN order_trans]) apply (simp_all) subgoal by (simp add: Misc.slice_def sort_spec_def) subgoal for xs' apply (clarsimp) by (auto intro!: transfer_guard_over_initial_sorting) subgoal unfolding slice_sort_spec_def apply refine_vcg apply (auto simp: sort_spec_def) apply (metis Misc.slice_def append_take_drop_id drop0 drop_take slice_complete union_code) by (metis slice_complete) done done definition "final_insertion_sort2 xs l h ≡ doN { ASSERT (l<h); if h-l ≤ is_threshold then gen_insertion_sort2 True l (l+1) h xs else doN { xs ← gen_insertion_sort2 True l (l+1) (l+is_threshold) xs; gen_insertion_sort2 False l (l+is_threshold) h xs } }" lemma final_insertion_sort2_refine: "⟦(xsi,xs) ∈ slicep_rel l h⟧ ⟹ final_insertion_sort2 xsi l h ≤ ⇓(slice_rel xsi l h) (final_insertion_sort xs)" unfolding final_insertion_sort2_def final_insertion_sort_def apply (refine_rcg gen_insertion_sort2_refine) apply clarsimp_all apply (auto simp: slicep_rel_def idx_shift_rel_def) [7] apply (subst slice_rel_rebase, assumption) apply (refine_rcg gen_insertion_sort2_refine) apply (auto simp: slice_rel_alt idx_shift_rel_def slicep_rel_def) done lemma final_insertion_sort2_correct: assumes [simplified, simp]: "(xs',xs)∈Id" "(l',l)∈Id" "(h',h)∈Id" shows "final_insertion_sort2 xs' l' h' ≤ final_sort_spec xs l h" proof (simp,rule le_nofailI) assume "nofail (final_sort_spec xs l h)" hence PS: "part_sorted_wrt (le_by_lt (<)) is_threshold (slice l h xs)" and LB: "h-l>1" "h ≤ length xs" unfolding final_sort_spec_def slice_sort_spec_def by (auto simp add: refine_pw_simps) from LB have LENGT1: "1 < length (slice l h xs)" by auto have SLR: "(xs, slice l h xs) ∈ slicep_rel l h" using LB by (auto simp: slicep_rel_def) note final_insertion_sort2_refine[OF SLR] also note final_insertion_sort_correct[OF PS LENGT1] also note slice_sort_spec_refine_sort'_sym[OF SLR refl refl refl] also have "slice_sort_spec (<) xs l h ≤ final_sort_spec xs l h" unfolding final_sort_spec_def using PS LB by simp finally show "final_insertion_sort2 xs l h ≤ final_sort_spec xs l h" . qed end context sort_impl_context begin sepref_register final_insertion_sort2 sepref_def final_insertion_sort_impl is "uncurry2 (PR_CONST final_insertion_sort2)" :: "[λ_. True]_c (woarray_slice_assn elem_assn)^d *_a size_assn^k *_a size_assn^k → woarray_slice_assn elem_assn [λ((ai,_),_) r. r=ai]_c" unfolding final_insertion_sort2_def PR_CONST_def apply (annot_snat_const "TYPE(size_t)") by sepref end context parameterized_weak_ordering begin definition "final_insertion_sort_param cparam xs l h ≡ doN { ASSERT (l<h); if h-l ≤ is_threshold then gen_insertion_sort_param True cparam l (l+1) h xs else doN { xs ← gen_insertion_sort_param True cparam l (l+1) (l+is_threshold) xs; gen_insertion_sort_param False cparam l (l+is_threshold) h xs } }" lemma final_insertion_sort_param_refine[refine]: "⟦ (l',l)∈Id; (h',h)∈Id; (xs',xs)∈cdom_list_rel cparam ⟧ ⟹ final_insertion_sort_param cparam xs' l' h' ≤ ⇓(cdom_list_rel cparam) (WO.final_insertion_sort2 cparam xs l h)" unfolding final_insertion_sort_param_def WO.final_insertion_sort2_def apply refine_rcg apply auto done end context parameterized_sort_impl_context begin sepref_register final_insertion_sort_param sepref_def final_insertion_sort_param_impl is "uncurry3 (PR_CONST final_insertion_sort_param)" :: "[λ_. True]_c cparam_assn^k *_a wo_assn^d *_a size_assn^k *_a size_assn^k → wo_assn [λ(((_,ai),_),_) r. r=ai]_c" unfolding final_insertion_sort_param_def PR_CONST_def apply (annot_snat_const "TYPE(size_t)") by sepref end end

Theory Examples.Sorting_Final_insertion_Sort