Theory Sorting_Quicksort_Partition
section ‹Quicksort Partition›
theory Sorting_Quicksort_Partition
imports Sorting_Quicksort_Scheme
begin
hide_const pi
context weak_ordering begin
paragraph ‹Summary›
text ‹This theory implements @{term partition3_spec} with the Hoare Partitioning Scheme.›
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);
if⇩N mop_cmp_idxs (cost ''cmp_idxs'' 1) xs ai bi then
if⇩N mop_cmp_idxs (cost ''cmp_idxs'' 1) xs bi ci then
mop_list_swapN xs ri bi
else if⇩N mop_cmp_idxs (cost ''cmp_idxs'' 1) xs ai ci then
mop_list_swapN xs ri ci
else
mop_list_swapN xs ri ai
else
if⇩N mop_cmp_idxs (cost ''cmp_idxs'' 1) xs ai ci then
mop_list_swapN xs ri ai
else if⇩N mop_cmp_idxs (cost ''cmp_idxs'' 1) xs bi ci then
mop_list_swapN xs ri ci
else
mop_list_swapN xs ri bi
}"
definition "move_median_to_first_cost = cost ''cmp_idxs'' 3 + cost ''if'' 3 + cost ''list_swap'' 1"
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)
) (λ_. move_median_to_first_cost)"
unfolding move_median_to_first_def move_median_to_first_cost_def
unfolding SPEC_def mop_cmp_idxs_def SPECc2_def mop_list_swap_def
apply(rule gwp_specifies_I)
apply (refine_vcg ‹-› rules: If_le_Some_rule2)
apply (all ‹(sc_solve,simp;fail)?›)
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)
) (λ_. move_median_to_first_cost)"
apply (rule order_trans[OF move_median_to_first_correct])
by (auto simp: SPEC_def le_fun_def)
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)
) (λ_. move_median_to_first_cost)"
apply (rule order_trans[OF move_median_to_first_correct'])
by (auto simp: SPEC_def le_fun_def)
end
context sort_impl_context begin
definition "move_median_to_first2 ri ai bi ci (xs::'a list) ≡ doN {
ASSERT (ai≠bi ∧ ai≠ci ∧ bi≠ci ∧ ri≠ai ∧ ri≠bi ∧ ri≠ci);
if⇩N cmp_idxs2' xs ai bi then doN {
if⇩N cmp_idxs2' xs bi ci then
myswap xs ri bi
else if⇩N cmp_idxs2' xs ai ci then
myswap xs ri ci
else
myswap xs ri ai
}
else if⇩N cmp_idxs2' xs ai ci then
myswap xs ri ai
else if⇩N cmp_idxs2' xs bi ci then
myswap xs ri ci
else
myswap xs ri bi
}"
lemma cmp_idxs2'_refines_mop_cmp_idxs_with_E':
"b'≠c' ⟹ (a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹
cmp_idxs2' a b c ≤ ⇓ bool_rel (timerefine TR_cmp_swap (mop_cmp_idxs (cost ''cmp_idxs'' 1) a' b' c'))"
apply(rule cmp_idxs2'_refines_mop_cmp_idxs_with_E)
by(auto simp: timerefineA_update_apply_same_cost')
lemma move_median_to_first2_refine':
assumes "(ri,ri')∈Id" "(ai,ai')∈Id" "(bi,bi')∈Id" "(ci,ci')∈Id" "(xs,xs')∈Id"
shows "move_median_to_first2 ri ai bi ci xs ≤ ⇓ (⟨Id⟩list_rel) (timerefine TR_cmp_swap (move_median_to_first ri' ai' bi' ci' xs'))"
using assms
unfolding move_median_to_first2_def move_median_to_first_def
supply cmp_idxs2'_refines_mop_cmp_idxs_with_E'[refine]
supply SPECc2_refine[refine]
supply myswap_TR_cmp_swap_refine[refine]
apply(refine_rcg bindT_refine_conc_time_my_inres MIf_refine)
by(auto intro: struct_preservingI)
definition "move_median_to_first2_cost = 3 *m cmp_idxs2'_cost + myswap_cost + cost ''if'' 3"
lemma move_median_to_first2_correct:
"⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹
move_median_to_first2 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)
) (λ_. move_median_to_first2_cost)"
apply(rule order.trans[OF move_median_to_first2_refine'])
apply simp_all [6]
apply(rule order.trans)
apply(rule timerefine_mono2[OF _ move_median_to_first_correct])
prefer 6
subgoal apply(simp add: SPEC_timerefine_conv)
apply(rule SPEC_leq_SPEC_I) apply simp
by(auto simp: move_median_to_first_cost_def move_median_to_first2_cost_def
timerefineA_update_apply_same_cost' timerefineA_propagate add.assoc add.commute)
by auto
sepref_register move_median_to_first2
sepref_def move_median_to_first_impl [llvm_inline] is "uncurry4 (PR_CONST move_median_to_first2)" :: "size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d →⇩a arr_assn"
unfolding move_median_to_first2_def PR_CONST_def
unfolding myswap_def
by sepref
end
context weak_ordering begin
subsection ‹Hoare Partitioning Scheme›
definition "ungrd_qsp_next_l_spec T xs pi li hi0 ≡
doN {
ASSERT (pi<li ∧ pi<hi0 ∧ hi0≤length xs);
ASSERT (∃i∈{li..<hi0}. xs!i ❙≥ xs!pi);
SPEC (λli'. li≤li' ∧ li'<hi0 ∧ (∀i∈{li..<li'}. xs!i❙<xs!pi) ∧ xs!li'❙≥xs!pi) (λli'. T li li')
}"
definition "ungrd_qsp_next_h_spec T xs pi li0 hi ≡
doN {
ASSERT (pi<li0 ∧ pi<length xs ∧ hi≤length xs ∧ (∃i∈{li0..<hi}. (xs!i) ❙≤ xs!pi));
SPEC (λhi'. li0≤hi' ∧ hi'<hi ∧ (∀i∈{hi'<..<hi}. xs!i❙>xs!pi) ∧ xs!hi'❙≤xs!pi) (λhi'. T hi hi')
}"
text ‹This is a major insight, limiting the resulting hi' of ungrd_qsp_next_h_spec
to not surpass the lower limit li0. Similar argument works for the lower pointer being
limited by hi0.›
lemma "⟦∃i∈{li0..<hi}. xs ! i ❙≤ xs!pi; (∀i∈{hi'<..<hi}. xs ! pi ❙< xs! i) ⟧ ⟹ li0 ≤ hi'"
by (meson atLeastLessThan_iff greaterThanLessThan_iff leI less_le_trans wo_leD)
definition qsp_next_l :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ (nat, ecost) nrest" 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 (cost ''cmp_idxs'' 1) xs li pi}) (λli. SPECc2 ''add'' (+) li 1) li
}"
definition uqnl_body
where "uqnl_body ≡ (cost ''if'' (1) + cost ''call'' 1
+ cost ''cmp_idxs'' 1)"
definition "ungrd_qsp_next_l_cost li li' = (enat(li'-li+1)) *m uqnl_body + cost ''add'' (enat(li'-li))"
lemma qsp_next_l_refine: "(qsp_next_l,PR_CONST (ungrd_qsp_next_l_spec ungrd_qsp_next_l_cost))∈Id→Id→Id→Id→⟨Id⟩nrest_rel"
unfolding qsp_next_l_def ungrd_qsp_next_l_spec_def ungrd_qsp_next_l_cost_def PR_CONST_def
apply (intro fun_relI nrest_relI; clarsimp)
apply(rule le_acost_ASSERTI)+
unfolding SPEC_def mop_cmp_idxs_def SPECc2_def
subgoal for xs p li hi
apply(subst monadic_WHILEIET_def[symmetric, where E="λli'. (hi-li') *m (uqnl_body + cost ''add'' 1)"])
apply(rule gwp_specifies_I)
apply (refine_vcg ‹-› rules: gwp_monadic_WHILEIET If_le_rule)
subgoal
unfolding wfR2_def apply (auto simp: uqnl_body_def costmult_add_distrib costmult_cost the_acost_propagate zero_acost_def)
by(auto simp: cost_def zero_acost_def)
subgoal for li'
apply(rule loop_body_conditionI)
subgoal apply(simp add: uqnl_body_def costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
by auto
subgoal apply(simp add: uqnl_body_def costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
apply safe
subgoal apply auto
by (metis Suc_eq_plus1 Suc_n_not_le_n add.commute le_diff_iff' le_trans lift_ord lt_by_le_def lt_by_linorder not_less_eq_eq one_enat_def plus_enat_simps(1))
subgoal apply auto
by (simp add: one_enat_def)
subgoal apply auto
by (simp add: one_enat_def)
subgoal apply (auto simp add: one_enat_def)
done
done
subgoal
by (metis One_nat_def add.commute atLeastLessThan_iff less_Suc_eq less_Suc_eq_le linorder_not_le plus_1_eq_Suc wo_leD)
done
subgoal for li'
apply(rule loop_exit_conditionI)
apply(rule If_le_Some_rule2)
subgoal apply(subst costmult_minus_distrib) apply simp
unfolding uqnl_body_def apply(simp add: costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
apply safe
subgoal apply auto
by (metis Suc_diff_le add.commute eq_iff one_enat_def plus_1_eq_Suc plus_enat_simps(1))
subgoal apply auto
by (metis Suc_diff_le eq_iff one_enat_def plus_1_eq_Suc plus_enat_simps(1))
subgoal apply auto
by (metis Suc_diff_le add.commute eq_iff one_enat_def plus_1_eq_Suc plus_enat_simps(1))
subgoal by auto
done
subgoal by (auto simp: unfold_le_to_lt)
done
subgoal apply auto done
subgoal apply auto done
subgoal apply auto done
done
done
definition qsp_next_h :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ (nat, ecost) nrest" where
"qsp_next_h xs pi li0 hi ≡ doN {
ASSERT (hi>0);
hi ← SPECc2 ''sub'' (-) 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 (cost ''cmp_idxs'' 1) xs pi hi})
(λhi. doN { ASSERT(hi>0); SPECc2 ''sub'' (-) hi 1}) hi
}"
definition uqnr_body
where "uqnr_body ≡ (cost ''if'' (1) + cost ''call'' 1
+ cost ''sub'' 1 + cost ''cmp_idxs'' 1)"
definition "ungrd_qsp_next_r_cost hi hi' = (enat(hi-hi')) *m uqnr_body"
lemma qsp_next_h_refine_aux1: "hi>0 ⟹ {hi'<..hi - Suc 0} = {hi'<..<hi}" by auto
lemma qsp_next_h_refine: "(qsp_next_h,PR_CONST (ungrd_qsp_next_h_spec ungrd_qsp_next_r_cost)) ∈ Id → Id → Id → Id → ⟨Id⟩nrest_rel"
unfolding qsp_next_h_def ungrd_qsp_next_h_spec_def ungrd_qsp_next_r_cost_def PR_CONST_def
apply (intro fun_relI nrest_relI; clarsimp)
apply(rule le_acost_ASSERTI)+
unfolding SPEC_def SPECc2_def mop_cmp_idxs_def
subgoal for xs pi li0 hi
apply(subst monadic_WHILEIET_def[symmetric, where E="λhi'. (hi'-li0) *m uqnr_body"])
apply(rule gwp_specifies_I)
apply (refine_vcg ‹-› rules: gwp_monadic_WHILEIET If_le_rule split_ifI)
subgoal
unfolding wfR2_def apply (auto simp: uqnr_body_def costmult_add_distrib costmult_cost the_acost_propagate zero_acost_def)
by(auto simp: cost_def zero_acost_def)
subgoal
apply(rule loop_body_conditionI)
subgoal
apply(simp add: uqnr_body_def costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
apply safe by auto
subgoal apply(simp add: uqnr_body_def costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
apply safe
subgoal apply auto
by (metis Suc_diff_Suc eq_iff greaterThanAtMost_iff less_le_trans nat_le_Suc_less_imp nat_neq_iff one_enat_def plus_1_eq_Suc plus_enat_simps(1) wo_leD)
subgoal apply auto
by (metis Suc_diff_Suc add.commute diff_is_0_eq eq_iff greaterThanAtMost_iff le_less_trans nat_le_Suc_less_imp not_gr_zero one_enat_def plus_1_eq_Suc plus_enat_simps(1) wo_leD zero_less_diff)
subgoal apply auto
by (metis Suc_diff_Suc diff_is_0_eq eq_iff greaterThanAtMost_iff le_less_trans nat_le_Suc_less_imp not_gr_zero one_enat_def plus_1_eq_Suc plus_enat_simps(1) wo_leD zero_less_diff)
subgoal apply auto
by (metis Suc_diff_Suc add.commute diff_is_0_eq eq_iff greaterThanAtMost_iff le_less_trans nat_le_Suc_less_imp not_gr_zero one_enat_def plus_1_eq_Suc plus_enat_simps(1) wo_leD zero_less_diff)
done
subgoal apply auto
subgoal by (metis One_nat_def le_step_down_nat wo_leD)
subgoal by (metis Suc_lessI Suc_pred greaterThanAtMost_iff)
done
done
subgoal apply auto
by (metis gr0I leD wo_leD)
subgoal for hi'
apply(rule loop_exit_conditionI)
apply(rule If_le_Some_rule2)
subgoal apply(subst costmult_minus_distrib) apply simp
unfolding uqnr_body_def apply(simp add: costmult_add_distrib costmult_cost lift_acost_propagate lift_acost_cost)
apply sc_solve
apply(simp add: zero_enat_def one_enat_def) done
subgoal
apply (intro conjI)
subgoal unfolding qsp_next_h_refine_aux1 by (meson atLeastLessThan_iff greaterThanLessThan_iff leI less_le_trans wo_leD)
subgoal using nat_le_Suc_less by blast
subgoal by (simp add: nat_le_Suc_less_imp)
subgoal using wo_leI by blast
done
done
subgoal by auto
subgoal by (meson atLeastLessThan_iff dual_order.strict_trans1 greaterThanAtMost_iff nat_le_Suc_less_imp wo_leD)
subgoal apply auto
using nat_le_Suc_less_imp by blast
subgoal
using nz_le_conv_less by blast
subgoal
by auto
done
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 ungrd_qsp_next_l_cost xs⇩0 pi li⇩0 hi⇩0;
hi ← ungrd_qsp_next_h_spec ungrd_qsp_next_r_cost xs⇩0 pi li⇩0 hi⇩0;
ASSERT (li⇩0≤hi);
(xs,li,hi) ← monadic_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). SPECc2 ''icmp_slt'' (<) li hi)
(λ(xs,li,hi). doN {
ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
xs ← mop_list_swapN xs li hi;
li ← SPECc2 ''add'' (+) li 1;
li ← ungrd_qsp_next_l_spec ungrd_qsp_next_l_cost xs pi li hi⇩0;
hi ← ungrd_qsp_next_h_spec ungrd_qsp_next_r_cost xs pi li⇩0 hi;
RETURN (xs,li,hi)
})
(xs⇩0,li,hi);
RETURN (xs,li)
}"
abbreviation "qs_body_cost ≡ (cost ''add'' (1::enat) + cost ''sub'' 1
+ cost ''list_swap'' 1 + cost ''if'' 3 + cost ''call'' 3 + cost ''icmp_slt'' 1 + cost ''cmp_idxs'' 2)"
definition "qs_partition_cost xs⇩0 li hi = (enat (hi-li)) *m qs_body_cost"
lemma strict_itrans: "a < c ⟹ a < b ∨ b < c" for a b c :: "_::linorder"
by auto
lemma qs_partition_correct:
fixes xs⇩0 :: "'a list"
shows
"⟦ 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) ) (λ_. qs_partition_cost xs⇩0 li hi )"
unfolding qs_partition_def ungrd_qsp_next_l_spec_def ungrd_qsp_next_h_spec_def
unfolding SPEC_REST_emb'_conv SPECc2_def mop_list_swap_def
apply(rule gwp_specifies_I)
apply(subst monadic_WHILEIET_def[symmetric, where E="λ(xs::'a list,li'::nat,hi'::nat).
(hi-li') *m (uqnl_body+ cost ''add'' 1) + (hi'-li) *m uqnr_body + (hi'-li') *m (cost ''list_swap'' 1 + cost ''call'' 1 + cost ''icmp_slt'' 1 + cost ''if'' 1) "])
apply (refine_vcg ‹-› rules: gwp_RETURNT_I gwp_monadic_WHILEIET If_le_rule split_ifI)
subgoal unfolding wfR2_def
apply safe
apply (auto simp add: uqnl_body_def uqnr_body_def costmult_add_distrib costmult_cost the_acost_propagate)
apply (simp_all add: cost_def zero_acost_def)
done
subgoal for _ _ _ xs li' hi' li'' hi''
apply(rule loop_body_conditionI)
subgoal
unfolding ungrd_qsp_next_l_cost_def ungrd_qsp_next_r_cost_def uqnl_body_def uqnr_body_def
apply(simp add: costmult_add_distrib costmult_cost lift_acost_cost lift_acost_propagate)
apply sc_solve by auto
subgoal apply simp
unfolding ungrd_qsp_next_l_cost_def ungrd_qsp_next_r_cost_def uqnl_body_def uqnr_body_def
apply(simp add: costmult_add_distrib costmult_cost lift_acost_cost lift_acost_propagate)
apply sc_solve_debug
apply safe
subgoal unfolding sc_solve_debug_def by (simp add: zero_enat_def one_enat_def)
subgoal unfolding sc_solve_debug_def
apply(simp only: zero_enat_def one_enat_def plus_enat_simps lift_ord) done
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def)
subgoal unfolding sc_solve_debug_def
by(simp only: zero_enat_def one_enat_def plus_enat_simps lift_ord)
subgoal unfolding sc_solve_debug_def
by(simp only: zero_enat_def one_enat_def plus_enat_simps lift_ord)
subgoal unfolding sc_solve_debug_def
by (simp only: zero_enat_def one_enat_def plus_enat_simps lift_ord)
done
subgoal
apply safe
subgoal by linarith
subgoal by linarith
subgoal by (metis atLeastLessThan_iff slice_eq_mset_swap(2) swap_length)
subgoal by (metis leD swap_indep)
subgoal apply(simp only: unfold_lt_to_le) apply clarsimp
apply (smt Suc_leI atLeastLessThan_iff le_def less_le_trans less_Suc_eq swap_indep swap_length swap_nth1)
done
subgoal by (metis (full_types) linorder_not_le swap_indep)
subgoal
apply(use [[put_named_ss HOL_ss]] in ‹clarsimp›)
apply(use [[put_named_ss Main_ss]] in ‹simp_all add: slice_eq_mset_eq_length unfold_lt_to_le›)
apply clarsimp
by (metis greaterThanLessThan_iff less_le_trans linorder_neqE_nat swap_indep swap_nth2)
subgoal by (metis (full_types) linorder_not_le swap_indep)
done
done
subgoal apply safe
subgoal by linarith
subgoal by linarith
subgoal by (metis atLeastLessThan_iff linwo swap_indep swap_nth1 weak_ordering.unfold_lt_to_le)
done
subgoal by (metis atLeastLessThan_iff discrete less_not_refl linwo swap_indep swap_nth2 weak_ordering.wo_less_le_trans)
subgoal apply safe
subgoal by linarith
subgoal by (simp add: slice_eq_mset_eq_length)
done
subgoal by safe
subgoal apply safe
subgoal by (metis (full_types) less_le_trans slice_eq_mset_eq_length)
subgoal by (metis (full_types) less_le_trans slice_eq_mset_eq_length)
done
subgoal
apply(rule loop_exit_conditionI)
apply(rule gwp_RETURNT_I)
unfolding emb'_def
apply(rule If_le_Some_rule2)
subgoal
apply simp
apply(subst lift_acost_diff_to_the_right) subgoal
by(simp add: cost_zero costmult_add_distrib costmult_cost lift_acost_cost lift_acost_propagate)
unfolding ungrd_qsp_next_r_cost_def ungrd_qsp_next_l_cost_def
unfolding uqnl_body_def uqnr_body_def
apply simp
unfolding qs_partition_cost_def
apply(simp add: cost_zero costmult_add_distrib costmult_cost lift_acost_cost lift_acost_propagate)
apply sc_solve_debug
apply safe
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
subgoal unfolding sc_solve_debug_def by (simp add: one_enat_def numeral_eq_enat)
done
subgoal
apply safe
by (metis atLeastLessThan_iff greaterThanLessThan_iff le_eq_less_or_eq strict_itrans)
done
subgoal apply simp
apply safe
subgoal using unfold_lt_to_le by blast
subgoal using unfold_lt_to_le by blast
done
subgoal
by (meson atLeastLessThan_iff greaterThanLessThan_iff leI less_le_trans wo_leD)
subgoal
apply safe
subgoal by linarith
subgoal by auto
done
subgoal by blast
subgoal
using less_trans by blast
subgoal apply simp done
done
definition "partition_pivot xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0 ∧ h-l≥4);
hl ← SPECc2 ''sub'' (-) h l;
d ← SPECc2 ''udiv'' (div) hl 2;
m ← SPECc2 ''add'' (+) l d;
l' ← SPECc2 ''add'' (+) l 1;
h' ← SPECc2 ''sub'' (-) h 1;
xs⇩1 ← move_median_to_first l l' m h' xs⇩0;
ASSERT (l<length xs⇩1 ∧ length xs⇩1 = length xs⇩0);
(xs,m) ← mop_call (qs_partition l' 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_aux1: "hi>0 ⟹ {hi'..hi - Suc 0} = {hi'..<hi}" by auto
abbreviation "TR_pp ≡ (TId(''partition_c'':=qs_body_cost + move_median_to_first_cost + cost ''sub'' 2 + cost ''call'' 2 + cost ''add'' 2 + cost ''udiv'' 1))"
lemma partition_pivot_correct: "⟦(xs,xs')∈Id; (l,l')∈Id; (h,h')∈Id⟧
⟹ partition_pivot xs l h ≤ ⇓Id (timerefine TR_pp (partition3_spec xs' l' h'))"
unfolding partition_pivot_def partition3_spec_def
apply(intro ASSERT_D3_leI)
apply(subst SPEC_timerefine_conv)
unfolding SPEC_def SPECc2_def
apply simp
apply(rule gwp_specifies_I)
supply mmtf = move_median_to_first_correct''[unfolded SPEC_def, THEN gwp_specifies_rev_I, THEN gwp_conseq_0]
supply qsp = qs_partition_correct[unfolded SPEC_def, THEN gwp_specifies_rev_I, THEN gwp_conseq_0]
apply (refine_vcg ‹-› rules: mmtf qsp If_le_Some_rule2)
apply(simp_all only: handy_if_lemma)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply clarsimp
subgoal by auto
subgoal by (metis le_less_trans less_imp_diff_less linorder_not_less partition_pivot_correct_aux1 zero_less_numeral)
subgoal apply auto
unfolding move_median_to_first_cost_def qs_partition_cost_def
apply(auto simp: timerefineA_update_apply_same_cost' costmult_add_distrib costmult_cost lift_acost_cost lift_acost_propagate)
apply sc_solve
apply safe
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
subgoal by (simp add: one_enat_def numeral_eq_enat)
done
subgoal
apply safe
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)
subgoal by (auto dest: slice_eq_mset_eq_length intro!: slice_LT_I_aux)
done
subgoal
by clarsimp
subgoal apply clarsimp by (metis (full_types) Suc_leI atLeastLessThan_iff le_neq_implies_less)
subgoal
apply clarsimp
apply (subst slice_eq_mset_nth_outside, assumption)
apply (auto dest: slice_eq_mset_eq_length)
done
subgoal by auto
subgoal by (metis diff_is_0_eq' le_trans nat_less_le not_numeral_le_zero slice_eq_mset_eq_length)
subgoal by auto
done
lemma TR_pp_important:
assumes "TR ''partition_c'' = TR_pp ''partition_c''"
shows "timerefine TR (partition3_spec xs' l' h') = timerefine TR_pp (partition3_spec xs' l' h')"
unfolding partition3_spec_def
apply(cases "4 ≤ h' - l' ∧ h' ≤ length xs'"; auto)
apply(simp only: SPEC_timerefine_conv)
apply(rule SPEC_cong, simp)
apply(rule ext)
apply(simp add: norm_cost timerefineA_cost_apply_costmult)
apply(subst assms(1))
apply (simp add: norm_cost)
done
lemma partition_pivot_correct_flexible:
assumes "TR ''partition_c'' = TR_pp ''partition_c''"
shows "⟦(xs,xs')∈Id; (l,l')∈Id; (h,h')∈Id⟧
⟹ partition_pivot xs l h ≤ ⇓Id (timerefine TR (partition3_spec xs' l' h'))"
apply(subst TR_pp_important[where TR=TR, OF assms])
apply(rule partition_pivot_correct)
apply auto
done
end
context sort_impl_context begin
definition qsp_next_l2 :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ (nat, ecost) nrest" where
"qsp_next_l2 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); cmp_idxs2' xs li pi}) (λli. SPECc2 ''add'' (+) li 1) li
}"
definition qsp_next_h2 :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ (nat, ecost) nrest" where
"qsp_next_h2 xs pi li0 hi ≡ doN {
ASSERT (hi>0);
hi ← SPECc2 ''sub'' (-) 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); cmp_idxs2' xs pi hi})
(λhi. doN { ASSERT(hi>0); SPECc2 ''sub'' (-) hi 1}) hi
}"
sepref_register ungrd_qsp_next_l_spec ungrd_qsp_next_h_spec qsp_next_h2 qsp_next_l2
sepref_definition qsp_next_l_impl [llvm_inline] is "uncurry3 (PR_CONST qsp_next_l2)" :: "(arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_l2_def PR_CONST_def
apply (annot_snat_const "TYPE('size_t)")
apply sepref
done
declare qsp_next_l_impl.refine[sepref_fr_rules]
sepref_definition qsp_next_h_impl [llvm_inline] is "uncurry3 (PR_CONST qsp_next_h2)" :: "(arr_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding qsp_next_h2_def PR_CONST_def
apply (annot_snat_const "TYPE('size_t)")
by sepref
declare qsp_next_h_impl.refine[sepref_fr_rules]
lemma qsp_next_l2_refines:
"(xs⇩0,xs⇩0')∈Id ⟹ (pi,pi')∈Id ⟹ (li⇩0,li⇩0')∈Id ⟹ (hi⇩0,hi⇩0')∈Id
⟹ qsp_next_l2 xs⇩0 pi li⇩0 hi⇩0 ≤ ⇓ Id (timerefine TR_cmp_swap (ungrd_qsp_next_l_spec ungrd_qsp_next_l_cost xs⇩0' pi' li⇩0' hi⇩0'))"
apply(rule order.trans)
defer
apply(rule nrest_Rel_mono) apply(rule timerefine_mono2)
subgoal by simp
apply(rule qsp_next_l_refine[to_foparam, THEN nrest_relD, simplified])
apply simp_all [4]
unfolding qsp_next_l2_def qsp_next_l_def
apply(refine_rcg SPECc2_refine cmp_idxs2'_refines_mop_cmp_idxs_with_E')
supply conc_Id[simp del]
by (auto intro: struct_preservingI simp: cost_n_leq_TId_n)
lemma qsp_next_h2_refines:
"(xs⇩0,xs⇩0')∈Id ⟹ (pi,pi')∈Id ⟹ (li⇩0,li⇩0')∈Id ⟹ (hi⇩0,hi⇩0')∈Id
⟹ qsp_next_h2 xs⇩0 pi li⇩0 hi⇩0 ≤ ⇓ Id (timerefine TR_cmp_swap (ungrd_qsp_next_h_spec ungrd_qsp_next_r_cost xs⇩0' pi' li⇩0' hi⇩0'))"
apply(rule order.trans)
defer
apply(rule nrest_Rel_mono) apply(rule timerefine_mono2)
subgoal by simp
apply(rule qsp_next_h_refine[to_foparam, THEN nrest_relD, simplified])
apply simp_all [4]
unfolding qsp_next_h2_def qsp_next_h_def
apply(refine_rcg bindT_refine_easy SPECc2_refine cmp_idxs2'_refines_mop_cmp_idxs_with_E')
apply refine_dref_type
supply conc_Id[simp del]
by (auto intro: struct_preservingI simp: cost_n_leq_TId_n)
definition "qs_partition2 li⇩0 hi⇩0 pi xs⇩0 ≡ doN {
ASSERT (pi < li⇩0 ∧ li⇩0<hi⇩0 ∧ hi⇩0≤length xs⇩0);
li ← qsp_next_l2 xs⇩0 pi li⇩0 hi⇩0;
hi ← qsp_next_h2 xs⇩0 pi li⇩0 hi⇩0;
ASSERT (li⇩0≤hi);
(xs,li,hi) ← monadic_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). SPECc2 ''icmp_slt'' (<) li hi)
(λ(xs,li,hi). doN {
ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
xs ← myswap xs li hi;
li ← SPECc2 ''add'' (+) li 1;
li ← qsp_next_l2 xs pi li hi⇩0;
hi ← qsp_next_h2 xs pi li⇩0 hi;
RETURN (xs,li,hi)
})
(xs⇩0,li,hi);
RETURN (xs,li)
}"
lemma qs_partition2_refines:
"(xs⇩0,xs⇩0')∈Id ⟹ (pi,pi')∈Id ⟹ (li⇩0,li⇩0')∈Id ⟹ (hi⇩0,hi⇩0')∈Id
⟹ qs_partition2 li⇩0 hi⇩0 pi xs⇩0 ≤ ⇓ Id (timerefine TR_cmp_swap (qs_partition li⇩0' hi⇩0' pi' xs⇩0'))"
unfolding qs_partition2_def qs_partition_def
supply qsp_next_l2_refines[refine]
supply qsp_next_h2_refines[refine]
apply(refine_rcg bindT_refine_easy SPECc2_refine myswap_TR_cmp_swap_refine)
apply refine_dref_type
supply conc_Id[simp del]
apply (auto simp: cost_n_leq_TId_n intro: struct_preservingI)
done
sepref_register qs_partition2
sepref_def qs_partition_impl is "uncurry3 (PR_CONST qs_partition2)" :: "size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (arr_assn)⇧d →⇩a arr_assn ×⇩a size_assn"
unfolding qs_partition2_def myswap_def PR_CONST_def
apply (annot_snat_const "TYPE('size_t)")
supply [dest] = slice_eq_mset_eq_length
apply sepref
done
definition "partition_pivot2 xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0 ∧ h-l≥4);
hl ← SPECc2 ''sub'' (-) h l;
d ← SPECc2 ''udiv'' (div) hl 2;
m ← SPECc2 ''add'' (+) l d;
l' ← SPECc2 ''add'' (+) l 1;
h' ← SPECc2 ''sub'' (-) h 1;
xs⇩1 ← move_median_to_first2 l l' m h' xs⇩0;
ASSERT (l<length xs⇩1 ∧ length xs⇩1 = length xs⇩0);
(xs,m) ← mop_call (qs_partition2 l' 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 partition_pivot2_refines:
"(xs⇩0,xs⇩0')∈Id ⟹ (l,l')∈Id ⟹ (h,h')∈Id
⟹ partition_pivot2 xs⇩0 l h ≤ ⇓ Id (timerefine TR_cmp_swap (partition_pivot xs⇩0' l' h'))"
unfolding partition_pivot2_def partition_pivot_def
supply move_median_to_first2_refine'[refine]
supply qs_partition2_refines[refine]
supply mop_call_refine[refine]
apply(refine_rcg bindT_refine_easy SPECc2_refine myswap_TR_cmp_swap_refine)
apply refine_dref_type
supply conc_Id[simp del]
apply (auto simp: cost_n_leq_TId_n intro: struct_preservingI)
done
lemma partition_pivot_bounds_aux1: "⟦¬ b < ba; ∀d. b = ba + d ⟶ 4 ≤ d;
(ac, ba + (b - ba) div 2) ∈ snat_rel' TYPE('size_t) ⟧
⟹ Suc ba < max_snat LENGTH('size_t)"
apply sepref_dbg_side_bounds
by presburger
lemma partition_pivot_bounds_aux2: "⟦ ¬ b < ba; ∀d. b = ba + d ⟶ 4 ≤ d ⟧ ⟹ Suc 0 ≤ b"
by presburger
sepref_register partition_pivot2
sepref_def partition_pivot_impl [llvm_inline] is "uncurry2 (PR_CONST partition_pivot2)" :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a arr_assn ×⇩a size_assn"
unfolding partition_pivot2_def PR_CONST_def
supply [simp] = nat_diff_split_asm partition_pivot_bounds_aux1 partition_pivot_bounds_aux2
apply (annot_snat_const "TYPE('size_t)")
apply sepref
done
text ‹A way to synthesize the final Timerefinement Relation, without ever touching the constants.›
schematic_goal partition_pivot2_correct: "(xs,xs')∈Id ⟹ (l,l')∈Id ⟹ (h,h')∈Id
⟹ partition_pivot2 xs l h ≤ ⇓ Id (timerefine ?E (partition3_spec xs' l' h'))"
apply(rule order.trans)
apply(rule partition_pivot2_refines)
apply simp_all [3]
apply simp
apply(rule order.trans)
apply(rule timerefine_mono2)
apply simp
apply(rule partition_pivot_correct[simplified])
apply simp_all [3]
apply(subst timerefine_iter2)
apply auto [2]
unfolding move_median_to_first_cost_def
apply(simp only: pp_fun_upd pp_TId_absorbs_right timerefineA_propagate[OF wfR''E])
apply (simp add: cmp_idxs2'_cost_def myswap_cost_def
lift_acost_cost lift_acost_propagate timerefineA_update_cost add.assoc
timerefineA_update_apply_same_cost' costmult_add_distrib costmult_cost)
apply(simp add: add.commute add.left_commute )
apply(simp add: cost_same_curr_left_add plus_enat_simps times_enat_simps numeral_eq_enat)
apply auto done
concrete_definition partition_pivot2_TR is partition_pivot2_correct uses "_ ≤ ⇓ Id (timerefine ⌑ _) "
end
end