Theory Sorting_Final_insertion_Sort
section ‹Final Insertion Sort›
theory Sorting_Final_insertion_Sort
imports Sorting_Quicksort_Scheme Sorting_Unguarded_Insertion_Sort
begin
paragraph ‹Summary›
text ‹This theory implements an algorithm final insertion sort, that
assumes a list that is almost-sorted @{term part_sorted_wrt} and returns
a sorted list in linear time.›
paragraph ‹Main Theorems/Definitions›
text ‹
▪ final_insertion_sort: the abstract algorithm that models final insertion sort
▪ final_insertion_sort_correct: final insertion sort, sorts an almost-sorted list
in time fi_cost, which is linear in the length of the list
▪ final_insertion_sort_impl: the synthesized algorithm
›
context weak_ordering begin
subsection ‹final_insertion_sort›
definition "final_insertion_sort xs ≡ doN {
ASSERT (1 < length xs);
lxs ← SPECT [length xs ↦ cost ''sub'' 1];
if⇩N SPECc2 ''icmp_sle'' (≤) lxs is_threshold then doN {
SPECT [() ↦ cost ''add'' 1];
insertion_sort_guarded 1 lxs xs
}
else doN {
SPECT [() ↦ cost ''add'' 2];
xs ← insertion_sort_guarded 1 is_threshold xs;
insertion_sort_unguarded is_threshold is_threshold lxs xs
}
}"
subsubsection ‹reasoning about stopper elements›
lemma has_stopperI:
assumes "i<length xs" "j'<i" "i-j'≤N" "∀j≤j'. ¬xs!i❙<xs!j"
shows "has_stopper N xs i"
using assms unfolding has_stopper_def by blast
lemma part_sorted_guardedI:
assumes S: "part_sorted_wrt (le_by_lt (❙<)) N xs" and B: "N≤i" "i<length xs"
shows "has_stopper N xs i"
proof -
from S have "N≠0" ‹i≠0› using B by (cases N; auto)+
from S obtain ss where SL: "is_slicing N xs ss" and SORTED: "sorted_wrt (slice_LT (le_by_lt (❙<))) ss" unfolding part_sorted_wrt_def by auto
have XS_EQ: "xs = concat ss" using SL unfolding is_slicing_def by auto
define xi where "xi = xs!i"
obtain xs1 xs2 where XSEQ2: "xs=xs1@xi#xs2" and LEN_XS1: "length xs1 = i"
unfolding xi_def using id_take_nth_drop[OF ‹i<length xs›] B by simp
have [simp]: "ss≠[]"
using XS_EQ assms(3) by auto
have "concat ss = xs1@xi#xs2" by (simp add: XS_EQ[symmetric] XSEQ2)
then obtain ss1 ssi1 ssi2 ss2 where 1: "ss = ss1 @ (ssi1 @ ssi2) # ss2" "xs1 = concat ss1 @ ssi1" "xi # xs2 = ssi2 @ concat ss2"
by (auto dest: concat_eq_appendD)
have SS1_NGT: "∀x∈set (concat ss1). ∀y∈set (ssi1@ssi2). ¬x ❙> y"
using SORTED by (auto simp add: "1"(1) sorted_wrt_append slice_LT_def le_by_lt_def)
have XS1_NGT: "∀x∈set xs1. ∀y∈set (concat ss2). ¬x ❙> y"
using SORTED by (auto simp add: "1" sorted_wrt_append slice_LT_def le_by_lt_def)
from SL 1 have SLI_BND: "length (ssi1@ssi2) ≤ N" unfolding is_slicing_def by auto
show ?thesis proof (cases ssi2)
case [simp]: Nil
obtain ssi2' ss2' where [simp]: "ss2 = (xi#ssi2') # ss2'" using 1
apply simp
apply (cases ss2; simp)
subgoal for ss2_1 ss2_r
using SL unfolding is_slicing_def
apply (cases ss2_1; simp)
done
done
show ?thesis
apply (rule has_stopperI[where j'="length xs1 - 1"])
subgoal by fact
subgoal using ‹i ≠ 0› ‹length xs1 = i› by auto
subgoal
using LEN_XS1 ‹N ≠ 0› by linarith
subgoal
apply (auto simp add: XS_EQ 1 simp flip: LEN_XS1)
apply (simp add: nth_append split: if_splits)
subgoal for j using XS1_NGT nth_mem unfolding 1(2) by fastforce
subgoal for j using XS1_NGT nth_mem unfolding 1(2) by fastforce
done
done
next
case (Cons _ ssi2') hence [simp]: "ssi2 = xi#ssi2'" using 1 by auto
have "ss1≠[]" proof
assume [simp]: "ss1=[]"
from 1 have "xs1 = ssi1" by simp
hence "length ssi1 = i" using ‹length xs1 = i› by simp
hence "length (ssi1@ssi2) > i" by simp
moreover note SLI_BND
ultimately show False using ‹N≤i› by auto
qed
have 11: "length (concat ss1) ≤ i" using ‹length xs1 = i› by (simp add: 1)
have 12: "i < N + length (concat ss1)"
by (metis "1"(2) "11" SLI_BND ‹length xs1 = i› add_diff_cancel_left' add_lessD1 le_eq_less_or_eq length_append length_greater_0_conv less_add_same_cancel1 less_diff_conv2 list.simps(3) local.Cons)
show ?thesis
apply (rule has_stopperI[where j'="length (concat ss1) - 1"])
subgoal using assms(3) by auto
subgoal using "1"(2) ‹i ≠ 0› ‹length xs1 = i› by auto
subgoal using 12 by linarith
subgoal
apply (auto simp add: XS_EQ 1 simp flip: LEN_XS1)
apply (simp add: nth_append split: if_splits)
subgoal for j using SS1_NGT using nth_mem by fastforce
subgoal using "12" assms(2) by linarith
done
done
qed
qed
lemma mset_slice_eq_xform_aux:
assumes "mset (slice 0 N xs') = mset (slice 0 N xs)"
assumes "j < N" "N < length xs" "length xs' = length xs"
obtains jj where "jj<N" "xs'!j = xs!jj"
using assms by (auto simp: list_eq_iff_nth_eq set_slice_conv dest!: mset_eq_setD; auto)
lemma filter_mset_eq_empty_conv: "filter_mset P m = {#} ⟷ (∀x∈#m. ¬P x)"
by (auto simp: filter_mset_eq_conv)
lemma filter_mset_eq_same_conv: "filter_mset P m = m ⟷ (∀x∈#m. P x)"
by (auto simp: filter_mset_eq_conv)
lemma sorted_pos_aux:
assumes "size (filter_mset (λx. x ❙≤ a) (mset xs)) ≥ n" "sorted_wrt (❙≤) xs"
shows "∀i<n. xs!i ❙≤ a"
proof -
from assms(1) have NL: "n≤length xs"
by (metis le_trans size_filter_mset_lesseq size_mset)
show ?thesis proof (rule ccontr, simp add: unfold_le_to_lt, clarify)
fix i
assume "i<n" "a ❙< xs!i"
hence 1: "∀j∈{i..<length xs}. a ❙< xs!j"
by (metis antisym_conv2 assms(2) atLeastLessThan_iff itrans sorted_wrt_nth_less wo_leD)
define xs⇩1 where "xs⇩1 = take i xs"
define xs⇩2 where "xs⇩2 = drop i xs"
have "xs = xs⇩1@xs⇩2" "∀x∈set xs⇩2. ¬x❙≤a"
unfolding xs⇩1_def xs⇩2_def using 1
by (auto simp: in_set_conv_nth unfold_le_to_lt)
hence "filter_mset (λx. x ❙≤ a) (mset xs) = filter_mset (λx. x ❙≤ a) (mset xs⇩1)"
by (auto simp: filter_mset_eq_empty_conv)
hence "size (filter_mset (λx. x ❙≤ a) (mset xs)) ≤ length xs⇩1"
apply auto
by (metis size_filter_mset_lesseq size_mset)
also have "length xs⇩1 < n" unfolding xs⇩1_def using ‹i<n› NL by auto
finally show False using assms(1) by simp
qed
qed
lemma filter_mset_eq_sameI:
"(∀x∈#m. P x) ⟹ filter_mset P m = m" by (simp add: filter_mset_eq_same_conv)
lemma xfer_stopper_leN_aux:
assumes "length xs' = length xs"
assumes I: "N ≤ i" "i < length xs"
assumes DEQ: "drop N xs' = drop N xs"
assumes S: "mset (slice 0 N xs') = mset (slice 0 N xs)" "sorted_wrt_lt (❙<) (slice 0 N xs')"
assumes LE: "∀j≤j'. ¬ xs ! i ❙< xs ! j" "j' < N" "j ≤ j'"
shows "¬ (xs' ! i ❙< xs' ! j)"
proof -
define xs⇩1 where "xs⇩1 = take (Suc j') (slice 0 N xs)"
define xs⇩2 where "xs⇩2 = drop (Suc j') (slice 0 N xs)"
have S0NXS_EQ: "(slice 0 N xs) = xs⇩1@xs⇩2"
unfolding xs⇩1_def xs⇩2_def by (auto)
have "∀x∈set (take (Suc j') xs). x ❙≤ xs!i"
unfolding unfold_le_to_lt using LE
by (auto simp: in_set_conv_nth)
also have "take (Suc j') xs = xs⇩1"
using LE
apply (auto simp: take_slice xs⇩1_def)
by (simp add: Misc.slice_def)
finally have 1: "∀x∈set xs⇩1. x ❙≤ xs ! i" .
have [simp]: "xs!i = xs'!i"
by (metis DEQ assms(1) assms(2) assms(3) drop_eq_mono hd_drop_conv_nth)
have "Suc j' = length xs⇩1" unfolding xs⇩1_def using LE I by auto
also from 1 have "length xs⇩1 ≤ size (filter_mset (λx. x ❙≤ xs!i) (mset (slice 0 N xs)))"
by (simp add: S0NXS_EQ filter_mset_eq_sameI)
also have "mset (slice 0 N xs) = mset (slice 0 N xs')" using S by simp
finally have "∀ia<Suc j'. slice 0 N xs' ! ia ❙≤ xs ! i"
using S(2)
apply -
apply (erule sorted_pos_aux)
using le_by_lt by blast
hence "∀ia<Suc j'. xs' ! ia ❙≤ xs ! i"
using LE by (simp add: Misc.slice_def)
thus ?thesis using LE by (auto simp: unfold_le_to_lt)
qed
lemma transfer_stopper_over_initial_sorting:
assumes "has_stopper N xs i"
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')"
shows "has_stopper N xs' i"
using assms[unfolded sort_spec_def has_stopper_def]
apply clarify
subgoal for j'
apply (cases "j'<N")
subgoal
apply (rule has_stopperI[where j'=j'])
using xfer_stopper_leN_aux
apply auto
done
subgoal
apply (rule has_stopperI[where j'=j'])
apply auto
subgoal for j
apply (subgoal_tac "xs'!i = xs!i")
subgoal
apply (cases "j<N")
subgoal by (erule (1) mset_slice_eq_xform_aux[where j=j]; simp)
subgoal by (smt assms(6) drop_eq_mono hd_drop_conv_nth leI le_eq_less_or_eq le_less_trans)
done
subgoal by (metis assms(4) drop_eq_mono hd_drop_conv_nth)
done
done
done
done
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')"
shows "has_stopper N xs' i"
using assms transfer_stopper_over_initial_sorting part_sorted_guardedI by blast
lemma pull_refinement_into_slice_sort_specT:
"slice_sort_specT (enat (h-i⇩0+1) *m insort_guarded_step_cost) (❙<) xs 0 h
= ⇓Id (timerefine (TId(''slice_sort'' := enat (h-i⇩0+1) *m insort_guarded_step_cost)) (
slice_sort_spec (❙<) xs 0 h))"
unfolding slice_sort_spec_def slice_sort_specT_def
apply(cases "h ≤ length xs"; auto)
apply(simp add: SPEC_timerefine_conv)
apply(rule SPEC_cong, simp)
by(simp add: timerefineA_cost)
abbreviation "guarded_insort_cost lxs ≡ enat (lxs+1) *m insort_guarded_step_cost"
lemma insertion_sort_guarded_correct_fl:
"⟦sorted_wrt_lt (❙<) (take i⇩0 xs); h≤length xs ; i⇩0<h; h≤length xs ⟧
⟹ insertion_sort_guarded i⇩0 h xs
≤ slice_sort_specT (guarded_insort_cost (h-i⇩0)) (❙<) xs 0 h"
apply(subst pull_refinement_into_slice_sort_specT)
apply(rule insertion_sort_guarded_correct)
apply auto
done
lemma insertion_sort_guarded_correct_threshold:
"⟦sorted_wrt_lt (❙<) (take i⇩0 xs); h≤length xs ; i⇩0<h; h≤length xs; (h-i⇩0)≤is_threshold ⟧
⟹ insertion_sort_guarded i⇩0 h xs
≤ slice_sort_specT (guarded_insort_cost is_threshold) (❙<) xs 0 h"
apply(rule order_trans)
apply(rule insertion_sort_guarded_correct_fl)
apply auto [4]
unfolding slice_sort_specT_def
apply(rule nrest_le_formatI)
apply(intro refine0 SPEC_both_refine)
apply clarsimp
apply(rule costmult_right_mono)
by auto
lemma final_insertion_sort_correct_aux:
"⟦sorted_wrt_lt (❙<) (take i⇩0 xs⇩0); h ≤ length xs⇩0; i⇩0 < h; h ≤ length xs⇩0; h - i⇩0 ≤ is_threshold;
0 ≤ h ∧ h ≤ length xs⇩0⟧
⟹ insertion_sort_guarded i⇩0 h xs⇩0 ≤
SPECT
(emb (λxs. length xs = length xs⇩0 ∧ take 0 xs = take 0 xs⇩0 ∧ drop h xs = drop h xs⇩0 ∧ sort_spec (❙<) (slice 0 h xs⇩0) (slice 0 h xs))
(guarded_insort_cost is_threshold))
"
using insertion_sort_guarded_correct_threshold[of i⇩0 xs⇩0 h]
unfolding slice_sort_specT_def SPEC_REST_emb'_conv
by(cases "0 ≤ h ∧ h ≤ length xs⇩0", auto)
abbreviation "unguarded_insort_cost lxs ≡ enat (lxs+1) *m insort_step_cost"
thm insertion_sort_unguarded_correct
lemma pull_refinement_into_slice_sort_specT_guarded:
"slice_sort_specT (enat (h-i⇩0+1) *m insort_step_cost) (❙<) xs 0 h
= ⇓Id (timerefine (TId(''slice_sort'' := enat (h-i⇩0+1) *m insort_step_cost)) (
slice_sort_spec (❙<) xs 0 h))"
unfolding slice_sort_spec_def slice_sort_specT_def
apply(cases "h ≤ length xs"; auto)
apply(simp add: SPEC_timerefine_conv)
apply(rule SPEC_cong, simp)
by(simp add: timerefineA_cost)
lemma insertion_sort_unguarded_correct_prepared:
"⟦sorted_wrt_lt (❙<) (take i⇩0 xs⇩0); (∀i∈{i⇩0..<h}. has_stopper N xs⇩0 i) ∧ h≤length xs⇩0 ; i⇩0<h; h≤length xs⇩0 ⟧
⟹ insertion_sort_unguarded N i⇩0 h xs⇩0
≤ SPECT
(emb (λxs. length xs = length xs⇩0 ∧ take 0 xs = take 0 xs⇩0 ∧ drop h xs = drop h xs⇩0 ∧ sort_spec (❙<) (slice 0 h xs⇩0) (slice 0 h xs))
(unguarded_insort_cost (h)))"
apply(rule order.trans)
apply(rule insertion_sort_unguarded_correct)
apply auto [4]
unfolding slice_sort_spec_def slice_sort_specT_def
apply auto
unfolding SPEC_timerefine_conv SPEC_REST_emb'_conv[symmetric]
apply(rule SPEC_leq_SPEC_I, simp)
apply(simp add: timerefineA_cost)
apply(rule costmult_right_mono)
apply simp
done
abbreviation "fi_cost lxs == guarded_insort_cost (is_threshold)
+ cost ''add'' 1 + cost ''add'' 1
+ cost ''if'' 1 + cost ''sub'' 1 + cost ''icmp_sle'' 1
+ unguarded_insort_cost lxs
"
subsubsection ‹Correctness Theorem›
lemma final_insertion_sort_correct:
"⟦part_sorted_wrt (le_by_lt (❙<)) is_threshold xs; 1 < length xs; lxs=length xs⟧
⟹ final_insertion_sort xs
≤ ⇓Id (timerefine (TId(''sort_spec'':=fi_cost lxs))
(SPEC (sort_spec (❙<) xs) (λ_. cost ''sort_spec'' 1)))"
unfolding final_insertion_sort_def SPEC_timerefine_conv
apply simp
unfolding SPEC_def
unfolding SPECc2_def
apply(rule gwp_specifies_I)
apply (refine_vcg ‹-›)
subgoal
apply(rule final_insertion_sort_correct_aux[THEN gwp_specifies_rev_I, THEN gwp_conseq_0 ])
apply simp_all
subgoal apply (rule sorted_wrt01) by auto
apply safe
apply(simp_all add: emb_eq_Some_conv)
subgoal apply auto using slice_complete by metis
apply(simp add: norm_cost add.assoc )
apply sc_solve by (auto simp: one_enat_def)
subgoal
apply(rule final_insertion_sort_correct_aux[THEN gwp_specifies_rev_I, THEN gwp_conseq_0 ])
apply simp_all
subgoal apply (rule sorted_wrt01) by auto
apply(rule insertion_sort_unguarded_correct_prepared[THEN gwp_specifies_rev_I, THEN gwp_conseq_0 ])
apply(simp_all add: emb_eq_Some_conv)
subgoal by (simp add: Misc.slice_def sort_spec_def)
subgoal for xs' M
apply safe
apply(rule transfer_guard_over_initial_sorting[where xs=xs])
by auto
subgoal
apply rule
subgoal
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)
subgoal
apply(simp add: norm_cost add.assoc)
apply sc_solve
by (auto simp: one_enat_def numeral_eq_enat)
done
done
done
subsection ‹final_insertion_sort2›
definition "final_insertion_sort2 xs l h ≡ doN {
ASSERT (l<h);
lxs ← SPECc2 ''sub'' (-) h l;
if⇩N SPECc2 ''icmp_sle'' (≤) lxs is_threshold then do {
l' ← SPECc2 ''add'' (+) l 1;
insertion_sort_guarded2 l l' h xs
}
else doN {
l' ← SPECc2 ''add'' (+) l 1;
l'' ← SPECc2 ''add'' (+) l is_threshold;
xs ← insertion_sort_guarded2 l l' l'' xs;
insertion_sort_unguarded2 is_threshold l'' h xs
}
}"
abbreviation "TR_fi2 N == (TR_is_insert3 N)"
lemma wfR''_TR_fi2[simp]: "wfR'' (TR_fi2 N)"
by (auto simp: pp_TId_absorbs_right pp_fun_upd intro!: wfR''_upd)
lemma sp_TR_fi2[simp]: "struct_preserving (TR_fi2 N)"
unfolding TR_is_insert3_def
by (auto simp: pp_TId_absorbs_right pp_fun_upd intro!: struct_preserving_upd_I)
thm insertion_sort_guarded2_refine
lemma insertion_sort_guarded2_refine_prepared:
"⟦ (xsi,xs) ∈ slicep_rel l h; (ii,i)∈idx_shift_rel l; (ji,j)∈idx_shift_rel l; j≤N ⟧
⟹ insertion_sort_guarded2 l ii ji xsi ≤⇓(slice_rel xsi l h) (timerefine (TR_fi2 N) (insertion_sort_guarded i j xs))"
apply(rule insertion_sort_guarded2_refine)
apply auto done
lemma insertion_sort_unguarded2_refine_prepared:
"⟦ (xsi,xs) ∈ slicep_rel l h; (ii,i)∈idx_shift_rel l; (ji,j)∈idx_shift_rel l ⟧
⟹ insertion_sort_unguarded2 N ii ji xsi ≤⇓(slice_rel xsi l h) (timerefine (TR_fi2 N) (insertion_sort_unguarded N i j xs))"
apply(rule insertion_sort_unguarded2_refine)
apply auto done
lemma final_insertion_sort2_refine: "⟦(xsi,xs) ∈ slicep_rel l h⟧
⟹ final_insertion_sort2 xsi l h ≤ ⇓(slice_rel xsi l h) (timerefine (TR_fi2 is_threshold) (final_insertion_sort xs))"
unfolding final_insertion_sort2_def final_insertion_sort_def
unfolding SPECc2_alt consume_RETURNT[symmetric]
apply normalize_blocks
supply [refine] = insertion_sort_guarded2_refine_prepared
insertion_sort_unguarded2_refine_prepared
apply (refine_rcg bindT_refine_conc_time_my_inres MIf_refine consumea_refine)
apply refine_dref_type
apply clarsimp_all
apply(all ‹(simp add: timerefineA_propagate timerefineA_update_cost timerefineA_update_apply_same_cost;fail)?›)
apply (auto simp: slicep_rel_def idx_shift_rel_def ) [10]
subgoal
apply(simp add: norm_cost norm_pp TR_is_insert3_def)
apply(subst timerefineA_propagate)
by(auto simp: norm_cost intro!: wfR''_upd)
subgoal
by (simp add: norm_cost norm_pp TR_is_insert3_def)
subgoal
apply(simp add: norm_cost norm_pp TR_is_insert3_def)
apply sc_solve by simp
subgoal
apply (subst slice_rel_rebase, assumption)
apply(refine_rcg insertion_sort_unguarded2_refine_prepared)
by (auto simp: slice_rel_alt idx_shift_rel_def slicep_rel_def)
done
abbreviation "fi2_cost s ≡ enat 17 *m TR_is_insert3 is_threshold ''icmp_slt''
+ enat 17 *m TR_is_insert3 is_threshold ''add''
+ enat 17 *m TR_is_insert3 is_threshold ''is_insert_g''
+ enat 17 *m TR_is_insert3 is_threshold ''call'' +
enat 17 *m TR_is_insert3 is_threshold ''if'' +
TR_is_insert3 is_threshold ''add'' +
TR_is_insert3 is_threshold ''add'' +
TR_is_insert3 is_threshold ''if'' +
TR_is_insert3 is_threshold ''sub'' +
TR_is_insert3 is_threshold ''icmp_sle'' +
(enat (Suc (s)) *m TR_is_insert3 is_threshold ''icmp_slt''
+ enat (Suc (s)) *m TR_is_insert3 is_threshold ''add''
+ enat (Suc (s)) *m TR_is_insert3 is_threshold ''is_insert'' +
enat (Suc (s)) *m TR_is_insert3 is_threshold ''call'' +
enat (Suc (s)) *m TR_is_insert3 is_threshold ''if'')"
subsubsection ‹Correctness Theorem›
lemma final_insertion_sort2_correct:
assumes [simplified, simp]: "(xs',xs)∈Id" "(l',l)∈Id" "(h',h)∈Id"
and "T ''slice_sort'' = fi2_cost (h-l)"
shows "final_insertion_sort2 xs' l' h' ≤ ⇓Id (timerefine T (final_sort_spec xs l h))"
unfolding final_sort_spec_def slice_sort_spec_def
apply(intro refine0)
apply(rule order_trans)
apply(rule final_insertion_sort2_refine[where xs="slice l h xs"])
subgoal by(auto simp: slicep_rel_def)
apply(rule order_trans[OF nrest_Rel_mono])
apply(rule timerefine_mono2)
subgoal by simp
apply(rule final_insertion_sort_correct)
apply simp
apply simp
apply simp
apply(simp add: SPEC_timerefine_conv)
unfolding slice_rel_def
apply(simp add: build_rel_SPEC_conv)
apply(rule SPEC_leq_SPEC_I_strong)
subgoal by auto
subgoal apply (auto simp: timerefineA_cost_apply_costmult norm_cost)
apply(subst assms(4)) apply simp
done
done
end
subsection ‹final_insertion_sort3›
context sort_impl_context begin
definition "final_insertion_sort3 xs l h ≡ doN {
ASSERT (l<h);
lxs ← SPECc2 ''sub'' (-) h l;
if⇩N SPECc2 ''icmp_sle'' (≤) lxs is_threshold then do {
l' ← SPECc2 ''add'' (+) l 1;
insertion_sort_guarded3 l l' h xs
}
else doN {
l' ← SPECc2 ''add'' (+) l 1;
l'' ← SPECc2 ''add'' (+) l is_threshold;
xs ← insertion_sort_guarded3 l l' l'' xs;
insertion_sort_unguarded3 is_threshold l'' h xs
}
}"
subsubsection ‹Refinement Lemma›
lemma final_insertion_sort3_refines:
"(xs,xs')∈Id ⟹ (l,l')∈Id ⟹ (h,h')∈Id
⟹ final_insertion_sort3 xs l h ≤ ⇓Id (timerefine TR_cmp_swap (final_insertion_sort2 xs' l' h'))"
supply conc_Id[simp del]
unfolding final_insertion_sort3_def final_insertion_sort2_def
supply [refine] = insertion_sort_unguarded3_refines insertion_sort_guarded3_refines
apply(refine_rcg MIf_refine SPECc2_refine' bindT_refine_conc_time_my_inres monadic_WHILEIT_refine' )
apply refine_dref_type
apply(all ‹(intro preserves_curr_other_updI wfR''_upd wfR''_TId preserves_curr_TId)?›)
apply (simp_all (no_asm))
by auto
subsubsection ‹Synthesize final_insertion_sort_impl›
sepref_register final_insertion_sort3
sepref_def final_insertion_sort_impl is "uncurry2 (PR_CONST final_insertion_sort3)"
:: "(array_assn elem_assn)⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a array_assn elem_assn"
unfolding final_insertion_sort3_def PR_CONST_def
apply (annot_snat_const "TYPE('size_t)")
by sepref
end
end