Theory Sorting_Quicksort_Partition
theory Sorting_Quicksort_Partition
imports Sorting_Quicksort_Scheme
begin
hide_const (open) Transcendental.pi
lemma strict_itrans: "a < c ⟹ a < b ∨ b < c" for a b c :: "_::linorder"
by auto
context weak_ordering begin
subsection ‹Find Median›
definition "move_median_to_first ri ai bi ci (xs::'a list) ≡ doN {
ASSERT (ai≠bi ∧ ai≠ci ∧ bi≠ci ∧ ri≠ai ∧ ri≠bi ∧ ri≠ci);
a ← mop_list_get xs ai;
b ← mop_list_get xs bi;
c ← mop_list_get xs ci;
if a❙<b then (
if b❙<c then
mop_list_swap xs ri bi
else if a❙<c then
mop_list_swap xs ri ci
else
mop_list_swap xs ri ai
)
else if a❙<c then
mop_list_swap xs ri ai
else if b❙<c then
mop_list_swap xs ri ci
else
mop_list_swap xs ri bi
}"
lemma move_median_to_first_alt: "move_median_to_first ri ai bi ci (xs::'a list) = doN {
ASSERT (ai≠bi ∧ ai≠ci ∧ bi≠ci ∧ ri≠ai ∧ ri≠bi ∧ ri≠ci);
if⇩N mop_cmp_idxs xs ai bi then (
if⇩N mop_cmp_idxs xs bi ci then
mop_list_swap xs ri bi
else if⇩N mop_cmp_idxs xs ai ci then
mop_list_swap xs ri ci
else
mop_list_swap xs ri ai
)
else if⇩N mop_cmp_idxs xs ai ci then
mop_list_swap xs ri ai
else if⇩N mop_cmp_idxs xs bi ci then
mop_list_swap xs ri ci
else
mop_list_swap xs ri bi
}"
unfolding move_median_to_first_def
by (auto simp: pw_eq_iff refine_pw_simps split!: if_splits)
lemma move_median_to_first_correct:
"⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹
move_median_to_first ri ai bi ci xs
≤ SPEC (λxs'. ∃i∈{ai,bi,ci}.
xs' = swap xs ri i
∧ (∃j∈{ai,bi,ci}-{i}. xs!i❙≤xs!j)
∧ (∃j∈{ai,bi,ci}-{i}. xs!i❙≥xs!j)
)"
unfolding move_median_to_first_def
apply refine_vcg
supply aux = bexI[where P="λx. _=_ x ∧ _ x", OF conjI[OF refl]]
apply ((rule aux)?; insert connex,auto simp: unfold_lt_to_le)+
done
lemma move_median_to_first_correct':
"⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹
move_median_to_first ri ai bi ci xs
≤ SPEC (λxs'. slice_eq_mset ri (ci+1) xs' xs
∧ (∃i∈{ai,bi,ci}. xs'!i❙≤xs'!ri)
∧ (∃i∈{ai,bi,ci}. xs'!i❙≥xs'!ri)
)"
apply (rule order_trans[OF move_median_to_first_correct])
by auto
lemma move_median_to_first_correct'':
"⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹
move_median_to_first ri ai bi ci xs
≤ SPEC (λxs'. slice_eq_mset ri (ci+1) xs' xs
∧ (∃i∈{ai..ci}. xs'!i❙≤xs'!ri)
∧ (∃i∈{ai..ci}. xs'!i❙≥xs'!ri)
)"
apply (rule order_trans[OF move_median_to_first_correct'])
by auto
end
context sort_impl_context begin
sepref_register move_median_to_first
sepref_def move_median_to_first_impl [llvm_inline] is "uncurry4 (PR_CONST move_median_to_first)"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d
→ arr_assn [λ((((_,_),_),_),ai) r. r=ai]⇩c"
unfolding move_median_to_first_alt PR_CONST_def
by sepref
end
context weak_ordering begin
subsection ‹Hoare Partitioning Scheme›
definition "ungrd_qsp_next_l_spec xs pi li hi ≡
doN {
ASSERT (pi<li ∧ pi<hi ∧ hi≤length xs);
ASSERT (∃i∈{li..<hi}. xs!i ❙≥ xs!pi);
SPEC (λli'. li≤li' ∧ li'<hi ∧ (∀i∈{li..<li'}. xs!i❙<xs!pi) ∧ xs!li'❙≥xs!pi)
}"
definition "ungrd_qsp_next_h_spec xs pi hi ≡
doN {
ASSERT (pi<length xs ∧ hi≤length xs ∧ (∃i∈{pi<..<hi}. (xs!i) ❙≤ xs!pi));
SPEC (λhi'. hi'<hi ∧ (∀i∈{hi'<..<hi}. xs!i❙>xs!pi) ∧ xs!hi'❙≤xs!pi)
}"
definition qsp_next_l :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres" where
"qsp_next_l xs pi li hi ≡ doN {
monadic_WHILEIT (λli'. (∃i∈{li'..<hi}. xs!i❙≥xs!pi) ∧ li≤li' ∧ (∀i∈{li..<li'}. xs!i❙<xs!pi))
(λli. doN {ASSERT (li≠pi); mop_cmp_idxs xs li pi}) (λli. RETURN (li + 1)) li
}"
lemma qsp_next_l_refine: "(qsp_next_l,PR_CONST ungrd_qsp_next_l_spec)∈Id→Id→Id→Id→⟨Id⟩nres_rel"
unfolding qsp_next_l_def ungrd_qsp_next_l_spec_def PR_CONST_def
apply (intro fun_relI; clarsimp)
subgoal for xs p li hi
apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λli. hi - li)"])
apply simp_all
subgoal by auto
apply safe
subgoal by (metis atLeastLessThan_iff leI le_less_Suc_eq wo_leD)
subgoal by (metis atLeastLessThan_iff leI le_less_Suc_eq)
subgoal using less_eq_Suc_le by force
subgoal by auto
subgoal by (auto simp: unfold_le_to_lt)
done
done
definition qsp_next_h :: "'a list ⇒ nat ⇒ nat ⇒ nat nres" where
"qsp_next_h xs pi hi ≡ doN {
ASSERT (hi>0);
let hi = hi - 1;
ASSERT (hi<length xs);
monadic_WHILEIT (λhi'. hi'≤hi ∧ (∃i≤hi'. xs!i❙≤xs!pi) ∧ (∀i∈{hi'<..hi}. xs!i❙>xs!pi))
(λhi. doN {ASSERT(pi≠hi); mop_cmp_idxs xs pi hi}) (λhi. doN { ASSERT(hi>0); RETURN (hi - 1)}) hi
}"
lemma qsp_next_h_refine: "(qsp_next_h,PR_CONST (ungrd_qsp_next_h_spec)) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
unfolding qsp_next_h_def ungrd_qsp_next_h_spec_def PR_CONST_def
apply (refine_vcg monadic_WHILEIT_rule[where R="measure id"] split_ifI)
apply (all ‹(determ ‹elim conjE exE›)?›)
apply simp_all
subgoal by force
subgoal by (meson greaterThanLessThan_iff nat_le_Suc_less_imp)
subgoal by (meson greaterThanAtMost_iff greaterThanLessThan_iff nat_le_Suc_less_imp wo_leD)
subgoal by (metis gr0I le_zero_eq unfold_lt_to_le)
subgoal by (metis One_nat_def le_step_down_nat wo_leD)
subgoal by (metis Suc_pred greaterThanAtMost_iff linorder_neqE_nat not_less_eq)
subgoal by (meson greaterThanAtMost_iff greaterThanLessThan_iff nat_le_Suc_less_imp)
subgoal using wo_leI by blast
done
definition "qs_partition li⇩0 hi⇩0 pi xs⇩0 ≡ doN {
ASSERT (pi < li⇩0 ∧ li⇩0<hi⇩0 ∧ hi⇩0≤length xs⇩0);
li ← ungrd_qsp_next_l_spec xs⇩0 pi li⇩0 hi⇩0;
hi ← ungrd_qsp_next_h_spec xs⇩0 pi hi⇩0;
ASSERT (li⇩0≤hi);
(xs,li,hi) ← WHILEIT
(λ(xs,li,hi).
li⇩0≤li ∧ hi<hi⇩0
∧ li<hi⇩0 ∧ hi≥li⇩0
∧ slice_eq_mset li⇩0 hi⇩0 xs xs⇩0
∧ xs!pi = xs⇩0!pi
∧ (∀i∈{li⇩0..<li}. xs!i ❙≤ xs⇩0!pi)
∧ xs!li ❙≥ xs⇩0!pi
∧ (∀i∈{hi<..<hi⇩0}. xs!i ❙≥ xs⇩0!pi)
∧ xs!hi ❙≤ xs⇩0!pi
)
(λ(xs,li,hi). li<hi)
(λ(xs,li,hi). doN {
ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
xs ← mop_list_swap xs li hi;
let li = li + 1;
li ← ungrd_qsp_next_l_spec xs pi li hi⇩0;
hi ← ungrd_qsp_next_h_spec xs pi hi;
RETURN (xs,li,hi)
})
(xs⇩0,li,hi);
RETURN (xs,li)
}"
lemma qs_partition_correct:
"⟦ pi<li; li<hi; hi≤length xs⇩0; ∃i∈{li..<hi}. xs⇩0!pi❙≤xs⇩0!i; ∃i∈{li..<hi}. xs⇩0!i❙≤xs⇩0!pi ⟧ ⟹ qs_partition li hi pi xs⇩0
≤ SPEC (λ(xs,i). slice_eq_mset li hi xs xs⇩0 ∧ li≤i ∧ i<hi ∧ (∀i∈{li..<i}. xs!i❙≤xs⇩0!pi) ∧ (∀i∈{i..<hi}. xs!i❙≥xs⇩0!pi) )"
unfolding qs_partition_def ungrd_qsp_next_l_spec_def ungrd_qsp_next_h_spec_def
apply (refine_vcg WHILEIT_rule[where R="measure (λ(_,_,hi). hi)"])
supply [[put_named_ss HOL_ss]]
apply (all ‹(clarsimp;fail)?›)
apply clarsimp_all
supply [[put_named_ss Main_ss]]
apply (simp_all add: slice_eq_mset_eq_length unfold_lt_to_le)
subgoal by fastforce
subgoal by auto
subgoal
by (metis slice_eq_mset_eq_length swap_length)
subgoal apply (clarsimp simp: swap_def)
by (metis (full_types) More_List.swap_def atLeastSucLessThan_greaterThanLessThan greaterThanLessThan_iff less_le_trans swap_nth2)
subgoal
by (metis (mono_tags) greaterThanLessThan_iff leD le_less_trans less_le_trans nat_le_linear not_less_eq_eq slice_eq_mset_eq_length swap_indep swap_nth1)
subgoal
by (smt Suc_le_lessD dual_order.trans greaterThanLessThan_iff leI less_imp_le_nat swap_indep swap_length swap_nth1)
subgoal
by (smt Suc_le_lessD atLeastLessThan_iff le_less_trans less_imp_le_nat slice_eq_mset_eq_length slice_eq_mset_swap(2))
subgoal apply clarsimp
by (metis less_irrefl less_imp_not_less less_le_trans swap_indep)
subgoal apply clarsimp
by (smt Suc_leI atLeastLessThan_iff le_def less_le_trans less_Suc_eq swap_indep swap_length swap_nth1)
subgoal apply clarsimp
by (metis le_def less_trans swap_indep)
subgoal apply clarsimp
by (smt greaterThanLessThan_iff le_def less_le_trans le_neq_implies_less less_imp_le_nat slice_eq_mset_eq_length swap_indep swap_nth2)
subgoal
by (metis le_def less_trans swap_indep)
subgoal
by (metis greaterThanLessThan_iff strict_itrans le_neq_implies_less)
done
definition "partition_pivot xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0 ∧ h-l≥4);
let m = l + (h-l) div 2;
xs⇩1 ← move_median_to_first l (l+1) m (h-1) xs⇩0;
ASSERT (l<length xs⇩1 ∧ length xs⇩1 = length xs⇩0);
(xs,m) ← qs_partition (l+1) h l xs⇩1;
ASSERT (l<m ∧ m<h);
ASSERT ((∀i∈{l+1..<m}. xs!i❙≤xs⇩1!l) ∧ xs!l❙≤xs⇩1!l);
ASSERT (∀i∈{l..<m}. xs!i❙≤xs⇩1!l);
ASSERT (∀i∈{m..<h}. xs⇩1!l❙≤xs!i);
RETURN (xs,m)
}"
lemma slice_LT_I_aux:
assumes B: "l<m" "m<h" "h≤length xs"
assumes BND: "∀i∈{l..<m}. xs!i❙≤p" "∀i∈{m..<h}. p❙≤xs!i"
shows "slice_LT (❙≤) (slice l m xs) (slice m h xs)"
unfolding slice_LT_def
using B apply (clarsimp simp: in_set_conv_nth slice_nth)
subgoal for i j
apply (rule trans[OF BND(1)[THEN bspec, of "l+i"] BND(2)[THEN bspec, of "m+j"]])
by auto
done
lemma partition_pivot_correct: "⟦(xs,xs')∈Id; (l,l')∈Id; (h,h')∈Id⟧
⟹ partition_pivot xs l h ≤ ⇓Id (partition3_spec xs' l' h')"
unfolding partition_pivot_def partition3_spec_def
apply (refine_vcg move_median_to_first_correct'' qs_partition_correct)
apply (all ‹auto 0 3 dest: slice_eq_mset_eq_length; fail›) [17]
apply clarsimp
subgoal for xs⇩1 xs⇩2 i m j
apply (subst slice_eq_mset_nth_outside, assumption)
apply (auto dest: slice_eq_mset_eq_length)
done
subgoal apply clarsimp by (metis (full_types) Suc_leI atLeastLessThan_iff le_neq_implies_less)
subgoal by auto
subgoal
apply simp
by (metis Suc_le_eq le_add2 le_refl order.strict_trans plus_1_eq_Suc slice_eq_mset_subslice slice_eq_mset_trans)
apply (all ‹auto; fail›) [2]
subgoal by (auto dest: slice_eq_mset_eq_length intro!: slice_LT_I_aux)
done
end
context sort_impl_context begin
sepref_register ungrd_qsp_next_l_spec ungrd_qsp_next_h_spec
sepref_definition qsp_next_l_impl [llvm_inline] is "uncurry3 (qsp_next_l)" :: "(arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_l_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
lemmas [sepref_fr_rules] = qsp_next_l_impl.refine[FCOMP qsp_next_l_refine]
sepref_definition qsp_next_h_impl [llvm_inline] is "uncurry2 (qsp_next_h)" :: "(arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_h_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
lemmas [sepref_fr_rules] = qsp_next_h_impl.refine[FCOMP qsp_next_h_refine]
sepref_register qs_partition
sepref_def qs_partition_impl is "uncurry3 (PR_CONST qs_partition)"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d
→ arr_assn ×⇩a size_assn [λ(((_,_),_),ai) (r,_). r=ai]⇩c"
unfolding qs_partition_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
supply [dest] = slice_eq_mset_eq_length
by sepref
sepref_register partition_pivot
sepref_def partition_pivot_impl [llvm_inline] is "uncurry2 (PR_CONST partition_pivot)"
:: "[λ_. True]⇩c arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k → arr_assn ×⇩a size_assn [λ((ai,_),_) (r,_). r=ai]⇩c"
unfolding partition_pivot_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
end
subsection ‹Parameterization›
context parameterized_weak_ordering begin
thm WO.qsp_next_l_def
definition qsp_next_l_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres" where
"qsp_next_l_param cparam xs pi li hi ≡ doN {
monadic_WHILEIT (λ_. True)
(λli. doN {ASSERT (li≠pi); pcmp_idxs2 cparam xs li pi})
(λli. doN {ASSERT (li<hi); RETURN (li + 1)}) li
}"
lemma qsp_next_l_param_refine[refine]: "⟦
(xs',xs)∈cdom_list_rel cparam; (p',p)∈Id; (i',i)∈Id; (h',h)∈Id
⟧ ⟹ qsp_next_l_param cparam xs' p' i' h' ≤⇓nat_rel (WO.ungrd_qsp_next_l_spec cparam xs p i h)"
proof (goal_cases)
case 1
then have "qsp_next_l_param cparam xs' p' i' h' ≤⇓nat_rel (WO.qsp_next_l cparam xs p i h)"
unfolding qsp_next_l_param_def WO.qsp_next_l_def
apply refine_rcg
by auto
also note WO.qsp_next_l_refine[param_fo, OF IdI IdI IdI IdI, of cparam xs p i h, THEN nres_relD]
finally show ?case unfolding PR_CONST_def .
qed
definition qsp_next_h_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat nres" where
"qsp_next_h_param cparam xs pi hi ≡ doN {
ASSERT (hi>0);
let hi = hi - 1;
ASSERT (hi<length xs);
monadic_WHILEIT (λ_. True)
(λhi. doN {ASSERT(pi≠hi); pcmp_idxs2 cparam xs pi hi})
(λhi. doN { ASSERT(hi>0); RETURN (hi - 1)}) hi
}"
lemma qsp_next_h_param_refine[refine]: "⟦
(xs',xs)∈cdom_list_rel cparam; (p',p)∈Id; (h',h)∈Id
⟧ ⟹ qsp_next_h_param cparam xs' p' h' ≤⇓nat_rel (WO.ungrd_qsp_next_h_spec cparam xs p h)"
proof goal_cases
case 1
then have "qsp_next_h_param cparam xs' p' h' ≤⇓nat_rel (WO.qsp_next_h cparam xs p h)"
unfolding qsp_next_h_param_def WO.qsp_next_h_def
apply refine_rcg
by (auto simp: cdom_list_rel_alt in_br_conv)
also note WO.qsp_next_h_refine[param_fo, THEN nres_relD]
finally show ?thesis by simp
qed
definition "qs_partition_param cparam li⇩0 hi⇩0 pi xs⇩0 ≡ doN {
ASSERT (pi < li⇩0 ∧ li⇩0<hi⇩0 ∧ hi⇩0≤length xs⇩0);
li ← qsp_next_l_param cparam xs⇩0 pi li⇩0 hi⇩0;
hi ← qsp_next_h_param cparam xs⇩0 pi hi⇩0;
ASSERT (li⇩0≤hi);
(xs,li,hi) ← WHILEIT
(λ_. True)
(λ(xs,li,hi). li<hi)
(λ(xs,li,hi). doN {
ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
xs ← mop_list_swap xs li hi;
let li = li + 1;
li ← qsp_next_l_param cparam xs pi li hi⇩0;
hi ← qsp_next_h_param cparam xs pi hi;
RETURN (xs,li,hi)
})
(xs⇩0,li,hi);
RETURN (xs,li)
}"
lemma qs_partition_param_refine[refine]: "⟦
(li',li)∈Id; (hi',hi)∈Id; (pi',pi)∈Id; (xs',xs)∈cdom_list_rel cparam
⟧ ⟹ qs_partition_param cparam li' hi' pi' xs'
≤ ⇓(cdom_list_rel cparam ×⇩r nat_rel) (WO.qs_partition cparam li hi pi xs)"
unfolding qs_partition_param_def WO.qs_partition_def
supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"]
apply refine_rcg
apply refine_dref_type
apply (auto simp: cdom_list_rel_alt in_br_conv)
done
definition "move_median_to_first_param cparam ri ai bi ci (xs::'a list) = doN {
ASSERT (ai ≠ bi ∧ ai ≠ ci ∧ bi ≠ ci ∧ ri ≠ ai ∧ ri ≠ bi ∧ ri ≠ ci);
if⇩N pcmp_idxs2 cparam xs ai bi then (
if⇩N pcmp_idxs2 cparam xs bi ci then
mop_list_swap xs ri bi
else if⇩N pcmp_idxs2 cparam xs ai ci then
mop_list_swap xs ri ci
else
mop_list_swap xs ri ai
)
else if⇩N pcmp_idxs2 cparam xs ai ci then
mop_list_swap xs ri ai
else if⇩N pcmp_idxs2 cparam xs bi ci then
mop_list_swap xs ri ci
else
mop_list_swap xs ri bi
}"
lemma mop_list_swap_cdom_refine[refine]: "⟦
(xs',xs)∈cdom_list_rel cparam; (i',i)∈Id; (j',j)∈Id
⟧ ⟹ mop_list_swap xs' i' j' ≤ ⇓ (cdom_list_rel cparam) (mop_list_swap xs i j)"
apply simp
apply refine_rcg
apply (clarsimp_all simp: cdom_list_rel_def list_rel_imp_same_length)
apply (parametricity)
by auto
lemma move_median_to_first_param_refine[refine]: "⟦
(ri',ri)∈Id; (ai',ai)∈Id; (bi',bi)∈Id; (ci',ci)∈Id; (xs',xs)∈cdom_list_rel cparam
⟧ ⟹ move_median_to_first_param cparam ri' ai' bi' ci' xs'
≤ ⇓(cdom_list_rel cparam) (WO.move_median_to_first cparam ri ai bi ci xs)"
unfolding move_median_to_first_param_def WO.move_median_to_first_alt
apply refine_rcg
by auto
definition "partition_pivot_param cparam xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0 ∧ h-l≥4);
let m = l + (h-l) div 2;
xs⇩1 ← move_median_to_first_param cparam l (l+1) m (h-1) xs⇩0;
ASSERT (l<length xs⇩1 ∧ length xs⇩1 = length xs⇩0);
(xs,m) ← qs_partition_param cparam (l+1) h l xs⇩1;
RETURN (xs,m)
}"
lemma partition_pivot_param_refine[refine]: "⟦ (xs',xs)∈cdom_list_rel cparam; (l',l)∈Id; (h',h)∈Id
⟧ ⟹ partition_pivot_param cparam xs' l' h'
≤ ⇓(cdom_list_rel cparam ×⇩r nat_rel) (WO.partition_pivot cparam xs l h)"
unfolding partition_pivot_param_def WO.partition_pivot_def
apply refine_rcg
apply (auto simp: cdom_list_rel_alt in_br_conv)
done
end
context parameterized_sort_impl_context begin
abbreviation "arr_assn ≡ wo_assn"
sepref_register qsp_next_l_param qsp_next_h_param
sepref_def qsp_next_l_impl [llvm_inline] is "uncurry4 (PR_CONST qsp_next_l_param)"
:: "cparam_assn⇧k *⇩a (arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_l_param_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
sepref_def qsp_next_h_impl [llvm_inline] is "uncurry3 (PR_CONST qsp_next_h_param)" :: "cparam_assn⇧k *⇩a (arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_h_param_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
sepref_register qs_partition_param
sepref_def qs_partition_impl is "uncurry4 (PR_CONST qs_partition_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d
→ arr_assn ×⇩a size_assn [λ((((_,_),_),_),ai) (r,_). r=ai]⇩c"
unfolding qs_partition_param_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
supply [dest] = slice_eq_mset_eq_length
by sepref
sepref_register move_median_to_first_param
sepref_def move_median_to_first_param_impl
is "uncurry5 (PR_CONST move_median_to_first_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d
→ arr_assn [λ(((((_,_),_),_),_),ai) r. r=ai]⇩c"
unfolding move_median_to_first_param_def PR_CONST_def
by sepref
sepref_register partition_pivot_param
sepref_def partition_pivot_impl
is "uncurry3 (PR_CONST partition_pivot_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k
→ arr_assn ×⇩a size_assn [λ(((_,ai),_),_) (r,_). r=ai]⇩c"
unfolding partition_pivot_param_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref
end
end