Theory Sorting_Setup
theory Sorting_Setup
imports "Isabelle_LLVM.IICF" "Isabelle_LLVM.Proto_IICF_EOArray" IICF_DS_Array_Idxs Sorting_Misc
begin
hide_const (open) Word.slice LLVM_DS_Array.array_assn LLVM_DS_NArray.array_slice_assn
lemma count_list_eq_count_mset: "count_list = count o mset"
proof (clarsimp simp: fun_eq_iff)
fix xs :: "'a list" and x
show "count_list xs x = count (mset xs) x"
by (induction xs) auto
qed
lemma permut_alt: "mset xs = mset xs' ⟷ (∀x. count_list xs x = count_list xs' x)"
by (auto simp: count_list_eq_count_mset multi_count_eq)
definition "is_copy A cp ≡ (cp,RETURN o COPY) ∈ A⇧k →⇩a A"
lemma is_copy_rule[sepref_fr_rules]:
"GEN_ALGO cp (is_copy A) ⟹ (cp,RETURN o COPY) ∈ A⇧k →⇩a A"
unfolding is_copy_def GEN_ALGO_def by auto
lemma is_copy_pure_gen_algo: "CONSTRAINT is_pure A ⟹ GEN_ALGO (Mreturn) (is_copy A)"
unfolding is_copy_def GEN_ALGO_def
by (rule hnr_pure_COPY)
definition [llvm_code]: "free_pure x ≡ Mreturn ()"
definition "le_by_lt lt a b ≡ ¬lt b a"
definition "lt_by_le le a b ≡ le a b ∧ ¬le b a"
locale weak_ordering_le =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "❙≤" 50)
assumes trans: "a ❙≤ b ⟹ b ❙≤ c ⟹ a ❙≤ c"
assumes connex: "a❙≤b ∨ b❙≤a"
locale weak_ordering_lt =
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "❙<" 50)
assumes asym: "a❙<b ⟹ ¬b❙<a"
assumes itrans: "a❙<c ⟹ a❙<b ∨ b❙<c"
locale weak_ordering =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "❙≤" 50)
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "❙<" 50)
assumes trans[trans]: "a ❙≤ b ⟹ b ❙≤ c ⟹ a ❙≤ c"
assumes connex: "a❙≤b ∨ b❙≤a"
assumes asym: "a❙<b ⟹ ¬b❙<a"
assumes itrans: "a❙<c ⟹ a❙<b ∨ b❙<c"
assumes lt_by_le: "lt_by_le (❙≤) = (❙<)"
assumes le_by_lt: "le_by_lt (❙<) = (❙≤)"
begin
lemma unfold_lt_to_le: "a ❙< b ⟷ a❙≤b ∧ ¬b❙≤a" unfolding lt_by_le[symmetric] lt_by_le_def by simp
lemma unfold_le_to_lt: "a ❙≤ b ⟷ ¬b❙<a" unfolding le_by_lt[symmetric] le_by_lt_def by simp
abbreviation (input) greater_eq (infix "❙≥" 50) where "b❙≥a ≡ a❙≤b"
abbreviation (input) greater (infix "❙>" 50) where "b❙>a ≡ a❙<b"
lemma wo_refl[iff]: "a ❙≤ a" using connex by auto
lemma wo_irrefl[iff]: "¬a❙<a" using asym by blast
lemma wo_less_trans[trans]: "a❙<b ⟹ b❙<c ⟹ a❙<c" using asym itrans by blast
lemma [iff]:
shows transp_le: "transp (❙≤)"
and reflp_le: "reflp (❙≤)"
and transp_lt: "transp (❙<)"
and irreflp_lt: "irreflp (❙<)"
unfolding transp_def reflp_def irreflp_def
using trans wo_less_trans
by blast+
definition eq (infix "❙=" 50) where "a ❙= b ≡ ¬a❙<b ∧ ¬b❙<a"
lemma eq_refl[iff]: "a ❙= a"
unfolding eq_def by blast
lemma eq_sym: "a ❙= b ⟷ b ❙= a"
unfolding eq_def by blast
lemma eq_trans: "a ❙= b ⟹ b ❙= c ⟹ a ❙= c"
unfolding eq_def using itrans by blast
lemma eq_equiv: "equivp (❙=)"
apply (intro equivpI reflpI sympI transpI)
using eq_sym eq_trans by blast+
text ‹Compatibility lemmas, similar names as for order›
lemma wo_leI: "¬ x ❙< y ⟹ y ❙≤ x" by (simp add: unfold_le_to_lt)
lemma wo_leD: "y ❙≤ x ⟹ ¬ x ❙< y" by (simp add: unfold_le_to_lt)
lemma wo_not_le_imp_less: "¬ y ❙≤ x ⟹ x ❙< y" by (simp add: unfold_le_to_lt)
lemma wo_le_less_trans[trans]: "x ❙≤ y ⟹ y ❙< z ⟹ x ❙< z"
using itrans wo_leD by blast
lemma wo_less_le_trans[trans]: "x ❙< y ⟹ y ❙≤ z ⟹ x ❙< z"
using itrans wo_leD by blast
lemma wo_less_not_sym: "x ❙< y ⟹ ¬ (y ❙< x)"
using asym by blast
lemma wo_less_asym: "x ❙< y ⟹ (¬ P ⟹ y ❙< x) ⟹ P"
using asym by blast
end
sublocale weak_ordering_lt < weak_ordering "le_by_lt (❙<)"
apply (unfold_locales)
unfolding le_by_lt_def lt_by_le_def using asym itrans by blast+
sublocale weak_ordering_le < weak_ordering "(❙≤)" "lt_by_le (❙≤)"
apply (unfold_locales)
unfolding le_by_lt_def lt_by_le_def using trans connex by blast+
lemma linwo: "weak_ordering (≤) ((<)::_::linorder ⇒ _)"
apply unfold_locales
unfolding le_by_lt_def lt_by_le_def
by (auto simp: fun_eq_iff)
lemma funwo: "weak_ordering (λa b. f a ≤ f b) (λa b. f a < f b)" for f :: "'a ⇒ 'b::linorder"
apply unfold_locales
unfolding le_by_lt_def lt_by_le_def
by (auto simp: fun_eq_iff)
lemma le_by_linorder[simp]: "le_by_lt ((<)::_::linorder ⇒ _) = (≤)"
unfolding le_by_lt_def less_le_not_le by (intro ext) auto
lemma lt_by_linorder[simp]: "lt_by_le ((≤)::_::linorder ⇒ _) = (<)"
unfolding lt_by_le_def less_le_not_le by (intro ext) auto
lemma bex_intv_shift_aux: "(∀x∈{0..<Suc n}. P x) ⟷ (P 0 ∧ (∀x∈{0..<n}. P (Suc x)))"
apply auto
using less_Suc_eq_0_disj by auto
lemma sorted_wrt_adjacent: "⟦transp R⟧ ⟹ sorted_wrt R xs ⟷ (∀i∈{0..<length xs-1}. R (xs!i) (xs!Suc i))"
supply [simp del] = sorted_wrt.simps(2) and [simp] = sorted_wrt2_simps
apply (induction xs rule: induct_list012)
apply (auto simp: bex_intv_shift_aux)
done
abbreviation "sorted_wrt_lt lt ≡ sorted_wrt (le_by_lt lt)"
lemma sorted_wrt_lt_adjacent:
assumes "weak_ordering_lt lt"
shows "sorted_wrt_lt lt xs ⟷ (∀i∈{0..<length xs-1}. ¬lt (xs!Suc i) (xs!i))"
proof -
interpret weak_ordering_lt lt by fact
show ?thesis
apply (subst sorted_wrt_adjacent)
apply (simp_all add: le_by_lt_def)
done
qed
lemma sorted_sorted_wrt_lt: "sorted = sorted_wrt_lt ((<)::_::linorder ⇒_)"
apply (intro ext) by simp
definition "sort_spec lt xs xs' ≡ mset xs'=mset xs ∧ sorted_wrt_lt lt xs'"
lemma (in weak_ordering) "sort_spec (❙<) xs xs' ⟷
(∀x. count_list xs' x = count_list xs x)
∧ (∀i j. i<j ∧ j<length xs' ⟶ ¬ xs'!j ❙< xs'!i)"
unfolding sort_spec_def permut_alt
by (auto simp: sorted_wrt_iff_nth_less le_by_lt_def)
definition "slice_sort_spec lt xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0);
SPEC (λxs. length xs = length xs⇩0 ∧ take l xs = take l xs⇩0 ∧ drop h xs = drop h xs⇩0 ∧ sort_spec lt (Misc.slice l h xs⇩0) (Misc.slice l h xs))
}"
lemma slice_sort_spec_refine_sort: "⟦(xsi,xs) ∈ slice_rel xs⇩0 l h; l'=l; h'=h⟧ ⟹ slice_sort_spec lt xsi l h ≤⇓(slice_rel xs⇩0 l' h') (SPEC (sort_spec lt xs))"
unfolding slice_sort_spec_def sort_spec_def
apply (refine_vcg RES_refine)
by (auto simp: slice_rel_def in_br_conv)
lemma slice_sort_spec_eq_sort': "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ ⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs)) = slice_sort_spec lt xsi l h"
unfolding slice_sort_spec_def sort_spec_def
apply (auto simp: slice_rel_def slicep_rel_def in_br_conv build_rel_SPEC_conv)
done
corollary slice_sort_spec_refine_sort': "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ slice_sort_spec lt xsi l h ≤⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs))"
by (simp add: slice_sort_spec_eq_sort')
corollary slice_sort_spec_refine_sort'_sym: "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ ⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs)) ≤ slice_sort_spec lt xsi l h"
by (simp add: slice_sort_spec_eq_sort')
lemma slice_sort_spec_alt: "slice_sort_spec lt xs l h = doN {
ASSERT (l≤h ∧ h≤length xs);
SPEC (λxs'. eq_outside_range xs' xs l h
∧ mset (slice l h xs') = mset (slice l h xs)
∧ sorted_wrt_lt lt (slice l h xs')
)
}"
unfolding slice_sort_spec_def sort_spec_def eq_outside_range_def
by (auto simp: pw_eq_iff refine_pw_simps)
lemma slice_sort_spec_sem_alt: "slice_sort_spec lt xs l h = doN {
ASSERT (l ≤ h ∧ h ≤ length xs);
SPEC (λxs'. slice_eq_mset l h xs xs' ∧ sorted_wrt_lt lt (slice l h xs'))
}"
unfolding slice_sort_spec_alt
by (auto simp: pw_eq_iff refine_pw_simps slice_eq_mset_alt slice_eq_mset_eq_length eq_outside_rane_lenD dest: eq_outside_range_sym)
text ‹ Sorting a permutation of a list amounts to sorting the list! ›
lemma sort_spec_permute: "⟦mset xs' = mset xs; sort_spec lt xs' ys⟧ ⟹ sort_spec lt xs ys"
unfolding sort_spec_def by auto
sepref_decl_op idx_v_swap: "λxs i v. (xs!i,xs[i:=v])" :: "[λ((xs,i),v). i<length xs]⇩f (⟨A⟩list_rel ×⇩r nat_rel) ×⇩r A → A ×⇩r ⟨A⟩list_rel" .
definition "idx_v_swap2 xs⇩0 i v ≡ do {
xs ← mop_to_eo_conv xs⇩0;
(v',xs) ← mop_eo_extract xs i;
xs ← mop_eo_set xs i v;
xs ← mop_to_wo_conv xs;
RETURN (v',xs)
}"
lemma idx_v_swap2_refine: "(idx_v_swap2,mop_idx_v_swap) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
unfolding idx_v_swap2_def
apply clarsimp
apply refine_vcg
apply (auto simp: map_update)
by (metis None_notin_image_Some list.set_map map_update)
sepref_def idx_v_swap_impl_woarray [llvm_code] is "uncurry2 idx_v_swap2"
:: "[λ_. True]⇩c (woarray_assn A)⇧d *⇩a snat_assn⇧k *⇩a A⇧d → A ×⇩a woarray_assn A [λ((ai,_),_) (_,r). r=ai]⇩c"
unfolding idx_v_swap2_def
by sepref
sepref_def idx_v_swap_impl_woarray_slice [llvm_code] is "uncurry2 idx_v_swap2"
:: "[λ_. True]⇩c (woarray_slice_assn A)⇧d *⇩a snat_assn⇧k *⇩a A⇧d → A ×⇩a woarray_slice_assn A [λ((ai,_),_) (_,r). r=ai]⇩c"
unfolding idx_v_swap2_def
by sepref
context notes [fcomp_norm_unfold] = list_rel_id_simp option_rel_id_simp begin
sepref_decl_impl (ismop) idx_v_swap_impl_woarray.refine[FCOMP idx_v_swap2_refine] uses mop_idx_v_swap.fref[where A=Id] .
sepref_decl_impl (ismop) idx_v_swap_impl_woarray_slice.refine[FCOMP idx_v_swap2_refine] uses mop_idx_v_swap.fref[where A=Id] .
end
find_theorems swap_eo
thm gen_mop_list_swap
find_theorems mop_list_swap array_slice_assn
context weak_ordering begin
sepref_decl_op cmpo_idxs: "λxs i j. the (xs!i) ❙< the (xs!j)"
:: "[λ((xs,i),j). i<length xs ∧ j<length xs ∧ xs!i≠None ∧ xs!j≠None]⇩f
(⟨⟨Id::'a rel⟩option_rel⟩list_rel ×⇩r nat_rel) ×⇩r nat_rel → bool_rel"
by simp
sepref_decl_op cmp_idxs: "λxs i j. xs!i ❙< xs!j"
:: "[λ((xs,i),j). i<length xs ∧ j<length xs]⇩f
(⟨Id::'a rel⟩list_rel ×⇩r nat_rel) ×⇩r nat_rel → bool_rel"
by simp
sepref_decl_op cmpo_v_idx: "λxs v j. v ❙< the (xs!j)" :: "[λ((xs,v),j). j<length xs ∧ xs!j ≠ None]⇩f (⟨⟨Id::'a rel⟩option_rel⟩list_rel ×⇩r (Id::'a rel)) ×⇩r nat_rel → bool_rel"
by simp
sepref_decl_op cmpo_idx_v: "λxs i v. the (xs!i) ❙< v" :: "[λ((xs,i),v). i<length xs ∧ xs!i≠None]⇩f (⟨⟨Id::'a rel⟩option_rel⟩list_rel ×⇩r nat_rel) ×⇩r (Id::'a rel) → bool_rel"
by simp
sepref_decl_op cmp_v_idx: "λxs v j. v ❙< xs!j" :: "[λ((xs,v),j). j<length xs]⇩f (⟨Id::'a rel⟩list_rel ×⇩r (Id::'a rel)) ×⇩r nat_rel → bool_rel"
by simp
sepref_decl_op cmp_idx_v: "λxs i v. xs!i ❙< v" :: "[λ((xs,i),v). i<length xs]⇩f (⟨Id::'a rel⟩list_rel ×⇩r nat_rel) ×⇩r (Id::'a rel) → bool_rel"
by simp
end
definition "refines_relp A R Rimpl ≡ (uncurry Rimpl,uncurry (RETURN oo R)) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn"
term "GEN_ALGO Rimpl (refines_relp A R)"
lemma gen_refines_relpD: "GEN_ALGO Rimpl (refines_relp A R) ⟹ (uncurry Rimpl,uncurry (RETURN oo R)) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn"
by (simp add: GEN_ALGO_def refines_relp_def)
lemma gen_refines_relpI[intro?]: "(uncurry Rimpl,uncurry (RETURN oo R)) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn ⟹ GEN_ALGO Rimpl (refines_relp A R)"
by (simp add: GEN_ALGO_def refines_relp_def)
locale sort_impl_context = weak_ordering +
fixes lt_impl :: "'ai::llvm_rep ⇒ 'ai ⇒ 1 word llM"
and elem_assn :: "'a ⇒ 'ai ⇒ assn"
assumes lt_impl: "GEN_ALGO lt_impl (refines_relp elem_assn (❙<))"
notes lt_hnr[sepref_fr_rules] = gen_refines_relpD[OF lt_impl]
notes [[sepref_register_adhoc "(❙<)"]]
begin
abbreviation "arr_assn ≡ woarray_slice_assn elem_assn"
definition "cmpo_idxs2 xs⇩0 i j ≡ doN {
ASSERT (i ≠ j);
(vi,xs) ← mop_eo_extract xs⇩0 i;
(vj,xs) ← mop_eo_extract xs j;
let r = vi ❙< vj;
xs ← mop_eo_set xs i vi;
xs ← mop_eo_set xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_v_idx2 xs⇩0 v j ≡ doN {
(vj,xs) ← mop_eo_extract xs⇩0 j;
let r = v ❙< vj;
xs ← mop_eo_set xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_idx_v2 xs⇩0 i v ≡ doN {
(vi,xs) ← mop_eo_extract xs⇩0 i;
let r = vi ❙< v;
xs ← mop_eo_set xs i vi;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmp_idxs2 xs⇩0 i j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← cmpo_idxs2 xs i j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
definition "cmp_idx_v2 xs⇩0 i v ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← cmpo_idx_v2 xs i v;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
definition "cmp_v_idx2 xs⇩0 v j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← cmpo_v_idx2 xs v j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
lemma cmpo_idxs2_refine: "(uncurry2 cmpo_idxs2, uncurry2 (PR_CONST mop_cmpo_idxs)) ∈ [λ((xs,i),j). i≠j]⇩f (Id×⇩rId)×⇩rId → ⟨Id⟩nres_rel"
unfolding cmpo_idxs2_def
apply (intro frefI nres_relI)
apply clarsimp
subgoal for xs i j
apply refine_vcg
apply (simp_all add: list_update_swap[of i j] map_update[symmetric])
done
done
lemma cmpo_v_idx2_refine: "(cmpo_v_idx2, PR_CONST mop_cmpo_v_idx) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
unfolding cmpo_v_idx2_def
apply clarsimp
apply refine_vcg
apply auto
done
lemma cmpo_idx_v2_refine: "(cmpo_idx_v2, PR_CONST mop_cmpo_idx_v) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
unfolding cmpo_idx_v2_def
apply clarsimp
apply refine_vcg
apply auto
done
lemma cmp_idxs2_refine: "(uncurry2 cmp_idxs2,uncurry2 (PR_CONST mop_cmp_idxs))∈[λ((xs,i),j). i≠j]⇩f (Id×⇩rId)×⇩rId → ⟨Id⟩nres_rel"
unfolding cmp_idxs2_def mop_cmp_idxs_def PR_CONST_def
apply (intro frefI nres_relI)
apply clarsimp
apply refine_vcg
apply (rule order_trans)
apply (rule cmpo_idxs2_refine[param_fo, THEN nres_relD], assumption, (rule IdI)+)
by (auto simp: pw_le_iff refine_pw_simps)
lemma cmp_idx_v2_refine: "(uncurry2 cmp_idx_v2,uncurry2 (PR_CONST mop_cmp_idx_v))∈(Id×⇩rId)×⇩rId → ⟨Id⟩nres_rel"
unfolding cmp_idx_v2_def mop_cmp_idx_v_def PR_CONST_def
apply (intro fun_relI nres_relI)
apply clarsimp
apply refine_vcg
apply (rule order_trans)
apply (rule cmpo_idx_v2_refine[param_fo, THEN nres_relD, OF IdI IdI IdI])
by (auto simp: pw_le_iff refine_pw_simps)
lemma cmp_v_idx2_refine: "(uncurry2 cmp_v_idx2,uncurry2 (PR_CONST mop_cmp_v_idx))∈(Id×⇩rId)×⇩rId → ⟨Id⟩nres_rel"
unfolding cmp_v_idx2_def mop_cmp_v_idx_def PR_CONST_def
apply (intro fun_relI nres_relI)
apply clarsimp
apply refine_vcg
apply (rule order_trans)
apply (rule cmpo_v_idx2_refine[param_fo, THEN nres_relD, OF IdI IdI IdI])
by (auto simp: pw_le_iff refine_pw_simps)
sepref_definition cmp_idxs_impl [llvm_inline] is "uncurry2 cmp_idxs2" :: "(woarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmp_idxs2_def cmpo_idxs2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_definition cmpo_idxs_impl [llvm_inline] is "uncurry2 cmpo_idxs2" :: "(eoarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmpo_idxs2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_definition cmpo_v_idx_impl [llvm_inline] is "uncurry2 cmpo_v_idx2" :: "(eoarray_slice_assn elem_assn)⇧k *⇩a elem_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmpo_v_idx2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_definition cmpo_idx_v_impl [llvm_inline] is "uncurry2 cmpo_idx_v2" :: "(eoarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding cmpo_idx_v2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_definition cmp_idx_v_impl [llvm_inline] is "uncurry2 cmp_idx_v2" :: "(woarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding cmp_idx_v2_def cmpo_idx_v2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_definition cmp_v_idx_impl [llvm_inline] is "uncurry2 cmp_v_idx2" :: "(woarray_slice_assn elem_assn)⇧k *⇩a elem_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmp_v_idx2_def cmpo_v_idx2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
context notes [fcomp_norm_unfold] = list_rel_id_simp option_rel_id_simp begin
sepref_decl_impl (ismop) cmp_idxs_impl.refine[FCOMP cmp_idxs2_refine] .
sepref_decl_impl (ismop) cmpo_idxs_impl.refine[FCOMP cmpo_idxs2_refine] .
sepref_decl_impl (ismop) cmpo_v_idx_impl.refine[FCOMP cmpo_v_idx2_refine] .
sepref_decl_impl (ismop) cmpo_idx_v_impl.refine[FCOMP cmpo_idx_v2_refine] .
sepref_decl_impl (ismop) cmp_v_idx_impl.refine[FCOMP cmp_v_idx2_refine] .
sepref_decl_impl (ismop) cmp_idx_v_impl.refine[FCOMP cmp_idx_v2_refine] .
end
end
locale sort_impl_copy_context = sort_impl_context +
fixes copy_elem_impl free_elem_impl
assumes elem_assn_copy[sepref_gen_algo_rules]: "GEN_ALGO copy_elem_impl (is_copy elem_assn)"
assumes elem_assn_free[sepref_frame_free_rules]: "MK_FREE elem_assn free_elem_impl"
begin
lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure elem_assn]
end
locale pure_sort_impl_context = sort_impl_context +
assumes pureA[safe_constraint_rules]: "CONSTRAINT is_pure elem_assn"
notes [sepref_frame_free_rules] = mk_free_is_pure[OF CONSTRAINT_D[OF pureA]]
begin
definition "cmp_idxs2' xs i j ≡ doN {
ASSERT (i<length xs ∧ j<length xs);
RETURN (xs!i ❙< xs!j)
}"
definition "cmp_idx_v2' xs i v ≡ doN {
ASSERT (i<length xs);
RETURN (xs!i ❙< v)
}"
definition "cmp_v_idx2' xs v j ≡ doN {
ASSERT (j<length xs);
RETURN (v ❙< xs!j)
}"
lemma cmp_idxs2'_refine: "(cmp_idxs2',PR_CONST mop_cmp_idxs)∈Id→Id→Id→⟨Id⟩nres_rel"
unfolding cmp_idxs2'_def mop_cmp_idxs_def
apply clarsimp
apply refine_vcg
by auto
lemma cmp_idx_v2'_refine: "(cmp_idx_v2',PR_CONST mop_cmp_idx_v)∈Id→Id→Id→⟨Id⟩nres_rel"
unfolding cmp_idx_v2'_def mop_cmp_idx_v_def
apply clarsimp
by refine_vcg
lemma cmp_v_idx2'_refine: "(cmp_v_idx2',PR_CONST mop_cmp_v_idx)∈Id→Id→Id→⟨Id⟩nres_rel"
unfolding cmp_v_idx2'_def
apply clarsimp
by refine_vcg
sepref_definition cmp_idxs'_impl [llvm_inline] is "uncurry2 cmp_idxs2'" :: "(woarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmp_idxs2'_def PR_CONST_def
by sepref
sepref_definition cmp_idx_v'_impl [llvm_inline] is "uncurry2 cmp_idx_v2'" :: "(woarray_slice_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding cmp_idx_v2'_def PR_CONST_def
by sepref
sepref_definition cmp_v_idx'_impl [llvm_inline] is "uncurry2 cmp_v_idx2'" :: "(woarray_slice_assn elem_assn)⇧k *⇩a elem_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmp_v_idx2'_def PR_CONST_def
by sepref
context notes [fcomp_norm_unfold] = list_rel_id_simp option_rel_id_simp begin
sepref_decl_impl (ismop) cmp_idxs'_impl.refine[FCOMP cmp_idxs2'_refine] .
sepref_decl_impl (ismop) cmp_v_idx'_impl.refine[FCOMP cmp_v_idx2'_refine] .
sepref_decl_impl (ismop) cmp_idx_v'_impl.refine[FCOMP cmp_idx_v2'_refine] .
end
sublocale sort_impl_copy_context "(❙≤)" "(❙<)" lt_impl elem_assn Mreturn free_pure
apply unfold_locales
subgoal
apply (rule is_copy_pure_gen_algo)
by solve_constraint
subgoal using mk_free_is_pure[OF CONSTRAINT_D[OF pureA]] unfolding free_pure_def by auto
done
end
type_synonym size_t = "64"
abbreviation "size_assn ≡ snat_assn' TYPE(size_t)"
lemma unat_sort_impl_context: "pure_sort_impl_context (≤) (<) ll_icmp_ult unat_assn"
apply intro_locales
apply (rule linwo)
apply unfold_locales
apply rule
apply (rule hn_unat_ops)
apply (solve_constraint)
done
subsection ‹Parameterized Sorting›
text ‹Extension of a weak ordering with explicit carrier set is always possible,
e.g., by putting all elements not in the carrier set into one equivalence class,
which is smaller than any other class.›
locale weak_ordering_on_lt =
fixes C :: "'a set"
and less :: "'a ⇒ 'a ⇒ bool" (infix "❙<" 50)
assumes asym: "⟦ a∈C; b∈C ⟧ ⟹ a❙<b ⟹ ¬b❙<a"
assumes itrans: "⟦ a∈C; b∈C; c∈C ⟧ ⟹ a❙<c ⟹ a❙<b ∨ b❙<c"
definition "ext_lt C lt a b ≡ lt a b ∧ a∈C ∧ b∈C ∨ a∈C ∧ b∉C"
lemma weak_ordering_on_lt_extend: "weak_ordering_lt (ext_lt C lt) ⟷ weak_ordering_on_lt C lt"
unfolding weak_ordering_on_lt_def weak_ordering_lt_def ext_lt_def
by blast
definition "pslice_sort_spec cdom pless cparam xs l h ≡ doN {
ASSERT (set xs ⊆ cdom cparam);
slice_sort_spec (pless cparam) xs l h
}"
locale parameterized_weak_ordering =
fixes cdom :: "'cparam ⇒ 'a set"
and pless :: "'cparam ⇒ 'a ⇒ 'a ⇒ bool"
and pcmp :: "'cparam ⇒ 'a ⇒ 'a ⇒ bool nres"
assumes weak_ordering_on_lt: "weak_ordering_on_lt (cdom cparam) (pless cparam)"
assumes pcmp_correct[refine_vcg]: "⟦ a∈cdom cparam; b∈cdom cparam⟧
⟹ pcmp cparam a b ≤ SPEC (λr. r ⟷ pless cparam a b)"
begin
definition "cdom_rel cparam ≡ br id (λx. x∈cdom cparam)"
definition "cdom_list_rel cparam ≡ ⟨cdom_rel cparam⟩list_rel"
definition "cdom_olist_rel cparam ≡ ⟨⟨cdom_rel cparam⟩option_rel⟩list_rel"
lemma br_id_list_rel_conv: "(xs,xs')∈⟨br id I⟩list_rel ⟷ xs=xs' ∧ set xs' ⊆ Collect I"
apply (induction xs arbitrary: xs')
subgoal for xs' by (auto)
subgoal for x xs xs' by (cases xs') (auto simp: in_br_conv)
done
lemma br_id_olist_rel_conv: "(xs,xs')∈⟨⟨br id I⟩option_rel⟩list_rel ⟷ xs=xs' ∧ (∀x. Some x∈set xs' ⟶ I x)"
apply (induction xs arbitrary: xs')
subgoal for xs' by (auto)
subgoal for x xs xs' by (cases xs') (auto simp: in_br_conv option_rel_def)
done
lemma cdom_list_rel_alt: "cdom_list_rel cparam = br id (λxs. set xs ⊆ cdom cparam)"
unfolding cdom_list_rel_def cdom_rel_def
by (auto simp: in_br_conv br_id_list_rel_conv)
lemma cdom_olist_rel_alt: "cdom_olist_rel cparam = br id (λxs. ∀x. Some x ∈ set xs ⟶ x∈cdom cparam)"
unfolding cdom_olist_rel_def cdom_rel_def
by (auto simp: in_br_conv br_id_olist_rel_conv)
definition "less' cparam ≡ (ext_lt (cdom cparam) (pless cparam))"
lemma weak_ordering_lt: "weak_ordering_lt (less' cparam)"
using weak_ordering_on_lt less'_def by (simp add: weak_ordering_on_lt_extend)
lemma weak_ordering: "weak_ordering (le_by_lt (less' cparam)) (less' cparam)"
proof -
interpret weak_ordering_lt "less' cparam" by (rule weak_ordering_lt)
show ?thesis by unfold_locales
qed
sublocale WO: weak_ordering "le_by_lt (less' cparam)" "less' cparam"
by (rule weak_ordering)
lemma sorted_wrt_ext: "set xs ⊆ cdom cparam ⟹ sorted_wrt (less' cparam) xs = sorted_wrt (pless cparam) xs"
apply (intro iffI; erule sorted_wrt_mono_rel[rotated])
apply (auto simp: less'_def ext_lt_def)
done
lemma set_slice_ss: "set (slice l h xs) ⊆ set xs"
by (metis Misc.slice_def dual_order.trans set_drop_subset set_take_subset)
lemma slice_sort_spec_xfer: "⇓ (cdom_list_rel cparam) (slice_sort_spec (less' cparam) xs l h) ≤ pslice_sort_spec cdom pless cparam xs l h"
unfolding pslice_sort_spec_def cdom_list_rel_alt
apply (auto simp: pw_le_iff refine_pw_simps in_br_conv)
unfolding slice_sort_spec_alt
apply (auto simp: refine_pw_simps)
using sorted_wrt_ext
by (smt ext_lt_def le_by_lt_def less'_def set_slice_ss sorted_wrt_mono_rel subsetD)
lemma olist_to_eo_conv_refine[refine]:
"(xs',xs)∈cdom_list_rel cparam ⟹ mop_to_eo_conv xs' ≤ ⇓(cdom_olist_rel cparam) (mop_to_eo_conv xs)"
apply (rule nres_relD)
unfolding mop_to_eo_conv_def cdom_olist_rel_def cdom_list_rel_def
by (parametricity)
lemma olist_to_wo_conv_refine[refine]:
"⟦(xs',xs)∈cdom_olist_rel cparam⟧ ⟹ mop_to_wo_conv xs' ≤ ⇓(cdom_list_rel cparam) (mop_to_wo_conv xs)"
apply simp
apply refine_rcg
apply (auto simp: cdom_olist_rel_alt cdom_list_rel_alt in_br_conv)
by (metis option.collapse)
lemma [refine]: "⟦ (xs',xs)∈cdom_olist_rel cparam; (i',i)∈Id ⟧
⟹ mop_eo_extract xs' i' ≤ ⇓ ((br id (λx. x∈cdom cparam)) ×⇩r cdom_olist_rel cparam) (mop_eo_extract xs i)"
unfolding mop_eo_extract_alt
apply refine_vcg
apply (auto simp: cdom_olist_rel_alt in_br_conv)
by (metis in_set_upd_cases option.distinct(1))
lemma listo_eo_set_refine[refine]: "⟦
(xs',xs)∈cdom_olist_rel cparam;
(i',i)∈Id;
(v',v)∈Id; v∈cdom cparam
⟧ ⟹ mop_eo_set xs' i' v' ≤ ⇓ (cdom_olist_rel cparam) (mop_eo_set xs i v)"
apply simp
apply refine_vcg
apply (auto simp: cdom_olist_rel_alt in_br_conv)
by (metis in_set_upd_cases option.sel)
definition "pcmpo_idxs2 cparam xs⇩0 i j ≡ doN {
ASSERT (i ≠ j);
(vi,xs) ← mop_eo_extract xs⇩0 i;
(vj,xs) ← mop_eo_extract xs j;
r ← pcmp cparam vi vj;
xs ← mop_eo_set xs i vi;
xs ← mop_eo_set xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "pcmpo_v_idx2 cparam xs⇩0 v j ≡ doN {
(vj,xs) ← mop_eo_extract xs⇩0 j;
r ← pcmp cparam v vj;
xs ← mop_eo_set xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "pcmpo_idx_v2 cparam xs⇩0 i v ≡ doN {
(vi,xs) ← mop_eo_extract xs⇩0 i;
r ← pcmp cparam vi v;
xs ← mop_eo_set xs i vi;
unborrow xs xs⇩0;
RETURN r
}"
definition "pcmp_idxs2 cparam xs⇩0 i j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← pcmpo_idxs2 cparam xs i j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
definition "pcmp_idx_v2 cparam xs⇩0 i v ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← pcmpo_idx_v2 cparam xs i v;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
definition "pcmp_v_idx2 cparam xs⇩0 v j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← pcmpo_v_idx2 cparam xs v j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
lemma pcmpo_idxs_refine[refine]: "⟦
(xs',xs)∈ cdom_olist_rel cparam;
i≠j;
(i',i)∈Id;
(j',j)∈Id
⟧ ⟹ pcmpo_idxs2 cparam xs' i' j' ≤ ⇓ bool_rel (WO.mop_cmpo_idxs cparam xs i j)"
unfolding pcmpo_idxs2_def
apply simp
apply refine_vcg
apply (auto simp: cdom_olist_rel_alt in_br_conv less'_def ext_lt_def
list_update_swap[of i j] map_update[symmetric])
done
lemma pcmpo_v_idx_refine[refine]: "⟦
(xs',xs)∈ cdom_olist_rel cparam;
(v',v)∈Id; v∈cdom cparam;
(i',i)∈Id
⟧ ⟹ pcmpo_v_idx2 cparam xs' v' i' ≤ ⇓ bool_rel (WO.mop_cmpo_v_idx cparam xs v i)"
unfolding pcmpo_v_idx2_def
apply simp
apply refine_vcg
apply (auto simp: cdom_olist_rel_alt in_br_conv less'_def ext_lt_def)
done
lemma pcmpo_idx_v_refine[refine]: "⟦
(xs',xs)∈ cdom_olist_rel cparam;
(v',v)∈Id; v∈cdom cparam;
(i',i)∈Id
⟧ ⟹ pcmpo_idx_v2 cparam xs' i' v' ≤ ⇓ bool_rel (WO.mop_cmpo_idx_v cparam xs i v)"
unfolding pcmpo_idx_v2_def
apply simp
apply refine_vcg
apply (auto simp: cdom_olist_rel_alt in_br_conv less'_def ext_lt_def)
done
lemma pcmp_idxs_refine[refine]: "⟦
(xs',xs)∈ cdom_list_rel cparam;
i≠j;
(i',i)∈Id;
(j',j)∈Id
⟧ ⟹ pcmp_idxs2 cparam xs' i' j' ≤ ⇓ bool_rel (WO.mop_cmp_idxs cparam xs i j)"
unfolding pcmp_idxs2_def pcmpo_idxs2_def
apply simp
apply refine_vcg
apply (auto 0 3 simp: cdom_list_rel_alt in_br_conv less'_def ext_lt_def
list_update_swap[of i j] map_update[symmetric])
using nth_mem by blast
lemma pcmp_idx_v_refine[refine]: "⟦
(xs',xs)∈ cdom_list_rel cparam;
(i',i)∈Id;
(v',v)∈Id; v∈cdom cparam
⟧ ⟹ pcmp_idx_v2 cparam xs' i' v' ≤ ⇓ bool_rel (WO.mop_cmp_idx_v cparam xs i v)"
unfolding pcmp_idx_v2_def pcmpo_idx_v2_def
apply simp
apply refine_vcg
by (auto 0 3 simp: cdom_list_rel_alt in_br_conv map_update[symmetric] less'_def ext_lt_def)
lemma pcmp_v_idx_refine[refine]: "⟦
(xs',xs)∈ cdom_list_rel cparam;
(v',v)∈Id; v∈cdom cparam;
(j',j)∈Id
⟧ ⟹ pcmp_v_idx2 cparam xs' v' j' ≤ ⇓ bool_rel (WO.mop_cmp_v_idx cparam xs v j)"
unfolding pcmp_v_idx2_def pcmpo_v_idx2_def
apply simp
apply refine_vcg
by (auto 0 3 simp: cdom_list_rel_alt in_br_conv map_update[symmetric] less'_def ext_lt_def intro: nth_mem)
end
text ‹The compare function takes an external parameter.›
term mop_eo_set
locale random_access_iterator =
fixes wo_assn :: "'a list ⇒ 'oi::llvm_rep ⇒ assn"
and eo_assn :: "'a option list ⇒ 'oi ⇒ assn"
and elem_assn :: "'a ⇒ 'ai::llvm_rep ⇒ assn"
and to_eo_impl :: "'oi ⇒ 'oi llM"
and to_wo_impl :: "'oi ⇒ 'oi llM"
and extract_impl :: "'oi ⇒ 'size::len2 word ⇒ ('ai × 'oi) llM"
and set_impl :: "'oi ⇒ 'size word ⇒ 'ai ⇒ 'oi llM"
assumes
to_eo_hnr: "(to_eo_impl, mop_to_eo_conv) ∈ [λ_. True]⇩c wo_assn⇧d → (eo_assn) [λai x. x=ai]⇩c"
and to_wo_hnr: "(to_wo_impl, mop_to_wo_conv) ∈ [λ_. True]⇩c eo_assn⇧d → (wo_assn) [λai x. x=ai]⇩c"
and eo_extract_hnr_aux: "(uncurry extract_impl, uncurry mop_eo_extract) ∈ [λ_. True]⇩c eo_assn⇧d *⇩a snat_assn⇧k → (elem_assn ×⇩a eo_assn) [λ(ai,_) (_,x). x=ai]⇩c"
and eo_set_hnr_aux: "(uncurry2 set_impl, uncurry2 mop_eo_set) ∈ [λ_. True]⇩c eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d → eo_assn [λ((ai,_),_) x. x=ai]⇩c"
notes [[sepref_register_adhoc to_eo_impl to_wo_impl extract_impl set_impl]]
begin
context
notes [fcomp_norm_simps] = option_rel_id_simp list_rel_id prod_rel_id_simp hrr_comp_id_conv
begin
private method rl_mono =
(rule hfref_cons;
clarsimp_all;
clarsimp_all simp: sep_algebra_simps entails_lift_extract_simps)
lemma eo_extract_nodep_hnr_aux:
"(uncurry extract_impl, uncurry mop_eo_extract) ∈ eo_assn⇧d *⇩a snat_assn⇧k →⇩a elem_assn ×⇩a eo_assn"
using eo_extract_hnr_aux
by rl_mono
lemma eo_set_nodep_hnr_aux:
"(uncurry2 set_impl, uncurry2 mop_eo_set) ∈ eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d →⇩a eo_assn"
using eo_set_hnr_aux
by rl_mono
lemmas [sepref_fr_rules] = to_eo_hnr to_wo_hnr
lemma to_eo_nodep_hnr: "(to_eo_impl, mop_to_eo_conv) ∈ wo_assn⇧d →⇩a eo_assn"
using to_eo_hnr
by rl_mono
lemma to_wo_nodep_hnr: "(to_wo_impl, mop_to_wo_conv) ∈ eo_assn⇧d →⇩a wo_assn"
using to_wo_hnr
by rl_mono
sepref_decl_impl (ismop) eo_extract: eo_extract_hnr_aux .
sepref_decl_impl (ismop,no_register) eo_extract_nodep: eo_extract_nodep_hnr_aux .
sepref_decl_impl (ismop) eo_set: eo_set_hnr_aux .
sepref_decl_impl (ismop,no_register) eo_set_nodep: eo_set_nodep_hnr_aux .
lemmas eo_hnr_dep = eo_extract_dep_hnr eo_extract_hnr_mop eo_set_hnr eo_set_hnr_mop
to_eo_hnr to_wo_hnr
lemmas eo_hnr_nodep = eo_extract_nodep_hnr eo_extract_nodep_hnr_mop eo_set_nodep_hnr eo_set_nodep_hnr_mop
to_eo_nodep_hnr to_wo_nodep_hnr
sepref_definition swap_eo_impl_aux is "uncurry2 swap_eo"
:: "[λ_. True]⇩c wo_assn⇧d *⇩a (snat_assn' TYPE('size))⇧k *⇩a (snat_assn' TYPE('size))⇧k → wo_assn [λ((xsi,_),_) r. r=xsi]⇩c"
unfolding swap_eo_def
by sepref
end
concrete_definition (in -) swap_eo_impl[llvm_inline] is random_access_iterator.swap_eo_impl_aux_def
context
notes [fcomp_norm_simps] = option_rel_id_simp list_rel_id prod_rel_id_simp hrr_comp_id_conv
begin
sepref_decl_impl (ismop) swap_eo_impl_aux.refine[FCOMP swap_eo_refine, unfolded swap_eo_impl.refine[OF random_access_iterator_axioms]]
uses mop_list_swap.fref[where A=Id] .
end
end
definition "refines_param_relp P A R Rimpl ≡ (uncurry2 Rimpl,uncurry2 R) ∈ P⇧k*⇩aA⇧k*⇩aA⇧k→⇩abool1_assn"
lemma gen_refines_param_relpD: "GEN_ALGO Rimpl (refines_param_relp P A R)
⟹ (uncurry2 Rimpl,uncurry2 R) ∈ P⇧k*⇩aA⇧k*⇩aA⇧k→⇩abool1_assn"
by (simp add: GEN_ALGO_def refines_param_relp_def)
locale parameterized_sort_impl_context = random_access_iterator + parameterized_weak_ordering +
constrains "cdom" :: "'cparam ⇒ _" and pless :: _ and pcmp :: "'cparam ⇒ 'a ⇒ 'a ⇒ bool nres"
and elem_assn :: "'a ⇒ 'ai::llvm_rep ⇒ assn"
and wo_assn :: "'a list ⇒ 'oi::llvm_rep ⇒ assn"
and eo_assn :: "'a option list ⇒ 'oi ⇒ assn"
and elem_assn :: "'a ⇒ 'ai::llvm_rep ⇒ assn"
and to_eo_impl :: "'oi ⇒ 'oi llM"
and to_wo_impl :: "'oi ⇒ 'oi llM"
and extract_impl :: "'oi ⇒ size_t word ⇒ ('ai × 'oi) llM"
and set_impl :: "'oi ⇒ size_t word ⇒ 'ai ⇒ 'oi llM"
fixes pcmp_impl :: "'cparami ⇒ 'ai ⇒ 'ai ⇒ 1 word llM"
and cparam_assn :: "'cparam ⇒ 'cparami ⇒ assn"
assumes lt_impl: "GEN_ALGO pcmp_impl (refines_param_relp cparam_assn elem_assn pcmp)"
notes pcmp_aux_hnr[sepref_fr_rules] = gen_refines_param_relpD[OF lt_impl]
notes [[sepref_register_adhoc "pcmp"]]
begin
thm pcmp_aux_hnr
term pcmpo_v_idx2
sepref_register pcmpo_idxs2 pcmpo_v_idx2 pcmpo_idx_v2 pcmp_idxs2
sepref_def pcmpo_idxs_impl [llvm_inline] is "uncurry3 (PR_CONST pcmpo_idxs2)" ::
"cparam_assn⇧k *⇩a eo_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn"
unfolding pcmpo_idxs2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_def pcmpo_v_idx_impl [llvm_inline] is "uncurry3 (PR_CONST pcmpo_v_idx2)" ::
"cparam_assn⇧k *⇩a eo_assn⇧k *⇩a elem_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn"
unfolding pcmpo_v_idx2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_def pcmpo_idx_v_impl [llvm_inline] is "uncurry3 (PR_CONST pcmpo_idx_v2)" ::
"cparam_assn⇧k *⇩a eo_assn⇧k *⇩a size_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding pcmpo_idx_v2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_def pcmp_idxs_impl [llvm_inline] is "uncurry3 (PR_CONST pcmp_idxs2)" ::
"cparam_assn⇧k *⇩a wo_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn"
unfolding pcmp_idxs2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_def pcmp_v_idx_impl [llvm_inline] is "uncurry3 (PR_CONST pcmp_v_idx2)" ::
"cparam_assn⇧k *⇩a wo_assn⇧k *⇩a elem_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn"
unfolding pcmp_v_idx2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
sepref_def pcmp_idx_v_impl [llvm_inline] is "uncurry3 (PR_CONST pcmp_idx_v2)" ::
"cparam_assn⇧k *⇩a wo_assn⇧k *⇩a size_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding pcmp_idx_v2_def PR_CONST_def
supply [sepref_fr_rules] = eo_hnr_dep
by sepref
end
subsection ‹Additional Setup for Code Generation›
definition "map_res f m ≡ doM { x←m; Mreturn (f x) }"
lemma map_res_return[sepref_opt_simps2]: "map_res φ (Mreturn x) = Mreturn (φ x)"
unfolding map_res_def by auto
lemma map_res_bind[sepref_opt_simps2]: "map_res φ (doM {x←m; f x}) = doM {x←m; map_res φ (f x)}"
unfolding map_res_def by auto
lemma map_res_prod_case[sepref_opt_simps2]: "map_res φ (case p of (a,b) ⇒ f a b) = (case p of (a,b) ⇒ map_res φ (f a b))"
by (rule prod.case_distrib)
lemmas [sepref_opt_simps2] = prod.sel
definition [llvm_inline]: "ars_with_split_nores i a m ≡ doM {
(a⇩1,a⇩2) ← ars_split i a;
(_,_) ← m a⇩1 a⇩2;
ars_join a⇩1 a⇩2;
Mreturn a
}"
lemma ars_with_split_bind_unit[sepref_opt_simps2]: "doM {
(uu::unit,xs) ← ars_with_split i a m;
mm uu xs
} = doM {
xs←ars_with_split_nores i a (λxs1 xs2. map_res snd (m xs1 xs2));
mm () xs
}"
unfolding ars_with_split_def ars_with_split_nores_def map_res_def
apply pw
done
definition [llvm_inline]: "oidxs_with_idxs'_nores p m ≡ doM { (_,_) ← m p p; Mreturn p }"
lemma oidxs_with_idxs'_bind_unit[sepref_opt_simps2]:
" doM { (uu::unit,xs) ← oidxs_with_idxs' p m; mm uu xs }
= doM { xs ← oidxs_with_idxs'_nores p (λxs⇩1 xs⇩2. map_res snd (m xs⇩1 xs⇩2)); mm () xs }"
unfolding oidxs_with_idxs'_def oidxs_with_idxs'_nores_def map_res_def
by simp
lemma sepref_adhoc_opt_case_add_const[sepref_opt_simps]:
"(case case x of (a1c, a2c) ⇒ (c, a1c, a2c) of (uu, a, b) ⇒ m uu a b) = (case x of (a,b) ⇒ m c a b)" by simp
end