Theory Sorting_Quicksort_Scheme
theory Sorting_Quicksort_Scheme
imports Sorting_Setup Sorting_Partially_Sorted
begin
lemma slice_complete': "h=length xs ⟹ slice 0 h xs = xs"
by simp
lemma slice_append1': "h = length xs⇩1 ⟹ slice 0 h (xs⇩1@xs⇩2) = xs⇩1"
by (simp add: Misc.slice_def)
lemma slice_append2': "l = length xs⇩1 ⟹ h = length xs⇩1+length xs⇩2 ⟹ slice l h (xs⇩1@xs⇩2) = xs⇩2"
by (simp add: Misc.slice_def)
abbreviation "is_threshold ≡ 16::nat"
context weak_ordering begin
definition "partition1_spec xs ≡ doN {
ASSERT (length xs ≥ 4);
SPEC (λ(xs1,xs2). mset xs = mset xs1 + mset xs2 ∧ xs1≠[] ∧ xs2≠[] ∧ slice_LT (❙≤) xs1 xs2)
}"
definition introsort_aux1 :: "'a list ⇒ nat ⇒ 'a list nres" where "introsort_aux1 xs d ≡ RECT (λintrosort_aux1 (xs,d). doN {
if length xs > is_threshold then doN {
if d=0 then
SPEC (sort_spec (❙<) xs)
else doN {
(xs1,xs2)←partition1_spec xs;
xs1 ← introsort_aux1 (xs1,d-1);
xs2 ← introsort_aux1 (xs2,d-1);
RETURN (xs1@xs2)
}
}
else
RETURN xs
}) (xs,d)"
lemma slice_strict_LT_imp_LE: "slice_LT (❙<) xs ys ⟹ slice_LT (le_by_lt (❙<)) xs ys"
apply (erule slice_LT_mono)
by (meson le_by_lt_def wo_less_asym)
lemma introsort_aux1_correct: "introsort_aux1 xs d ≤ SPEC (λxs'. mset xs' = mset xs ∧ part_sorted_wrt (le_by_lt (❙<)) is_threshold xs')"
unfolding introsort_aux1_def partition1_spec_def sort_spec_def
apply (refine_vcg RECT_rule_arb[where V="measure (λ(xs,d). d+1)" and pre="λxss (xs',d). xss=xs'"])
apply (all ‹(auto intro: sorted_wrt_imp_part_sorted part_sorted_wrt_init; fail)?›)
apply (rule order_trans)
apply rprems
applyS (simp)
subgoal by auto
apply refine_vcg
subgoal
apply (rule order_trans)
apply rprems
applyS simp
subgoal by auto
apply refine_vcg
subgoal by auto
subgoal
apply clarsimp
apply (rule part_sorted_concatI; assumption?)
apply (subst slice_LT_mset_eq1, assumption)
apply (subst slice_LT_mset_eq2, assumption)
using le_by_lt by blast
done
done
definition "partition2_spec xs ≡ doN {
ASSERT (length xs ≥ 4);
SPEC (λ(xs',i). mset xs' = mset xs ∧ 0<i ∧ i<length xs ∧ slice_LT (❙≤) (take i xs') (drop i xs'))
}"
lemma partition2_spec_refine: "(xs,xs')∈Id ⟹ partition2_spec xs ≤⇓(br (λ(xs,i). (take i xs, drop i xs)) (λ(xs,i). 0<i ∧ i<length xs)) (partition1_spec xs')"
unfolding partition1_spec_def partition2_spec_def
apply (refine_vcg RES_refine)
by (auto dest: mset_eq_length simp: in_br_conv simp flip: mset_append)
definition introsort_aux2 :: "'a list ⇒ nat ⇒ 'a list nres" where "introsort_aux2 xs d ≡ RECT (λintrosort_aux (xs,d). doN {
if length xs > is_threshold then doN {
if d=0 then
SPEC (sort_spec (❙<) xs)
else doN {
(xs,m)←partition2_spec xs;
ASSERT (m≤length xs);
xs1 ← introsort_aux (take m xs,d-1);
xs2 ← introsort_aux (drop m xs,d-1);
RETURN (xs1@xs2)
}
}
else
RETURN xs
}) (xs,d)"
lemma introsort_aux2_refine: "introsort_aux2 xs d ≤⇓Id (introsort_aux1 xs d)"
unfolding introsort_aux2_def introsort_aux1_def
apply (refine_rcg partition2_spec_refine)
apply refine_dref_type
apply (auto simp: in_br_conv)
done
definition "partition3_spec xs l h ≡ doN {
ASSERT (h-l≥4 ∧ h≤length xs);
SPEC (λ(xs',i). slice_eq_mset l h xs' xs ∧ l<i ∧ i<h ∧ slice_LT (❙≤) (slice l i xs') (slice i h xs'))
}"
lemma partition3_spec_refine: "(xsi,xs) ∈ slice_rel xs⇩0 l h ⟹ partition3_spec xsi l h ≤⇓(slice_rel xs⇩0 l h ×⇩r idx_shift_rel l) (partition2_spec xs)"
unfolding partition3_spec_def partition2_spec_def
apply (refine_vcg RES_refine)
apply (auto simp: slice_rel_def in_br_conv) [2]
apply (clarsimp simp: slice_rel_def in_br_conv)
subgoal for xs'i ii
apply (rule exI[where x="slice l h xs'i"])
apply (rule conjI)
subgoal by (auto simp: slice_eq_mset_def)
apply (simp add: idx_shift_rel_alt)
by (auto simp: slice_eq_mset_def take_slice drop_slice)
done
lemma partition3_spec_refine': "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧
⟹ partition3_spec xsi l h ≤⇓(slice_rel xsi' l' h' ×⇩r idx_shift_rel l') (partition2_spec xs)"
unfolding partition3_spec_def partition2_spec_def
apply (refine_vcg RES_refine)
apply (auto simp: slicep_rel_def in_br_conv) [2]
apply (clarsimp simp: slice_rel_def slicep_rel_def in_br_conv)
subgoal for xs'i ii
apply (rule exI[where x="slice l h xs'i"])
apply (rule conjI)
subgoal by (auto simp: slice_eq_mset_def)
apply (simp add: idx_shift_rel_alt)
by (auto simp: slice_eq_mset_def take_slice drop_slice)
done
definition introsort_aux3 :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ 'a list nres" where "introsort_aux3 xs l h d
≡ RECT (λintrosort_aux (xs,l,h,d). doN {
ASSERT (l≤h);
if h-l > is_threshold then doN {
if d=0 then
slice_sort_spec (❙<) xs l h
else doN {
(xs,m)←partition3_spec xs l h;
xs ← introsort_aux (xs,l,m,d-1);
xs ← introsort_aux (xs,m,h,d-1);
RETURN xs
}
}
else
RETURN xs
}) (xs,l,h,d)"
lemma introsort_aux3_refine: "(xsi,xs)∈slicep_rel l h ⟹ introsort_aux3 xsi l h d ≤ ⇓(slice_rel xsi l h) (introsort_aux2 xs d)"
unfolding introsort_aux3_def introsort_aux2_def
supply recref = RECT_dep_refine[where
R="λ_. {((xsi::'a list, l, h, di::nat), (xs, d)). (xsi, xs) ∈ slicep_rel l h ∧ di=d}" and
S="λ_ (xsi::'a list, l, h, di::nat). slice_rel xsi l h" and
arb⇩0 = "()"
]
apply (refine_rcg
recref
partition3_spec_refine'
slice_sort_spec_refine_sort'
; (rule refl)?
)
subgoal by auto
subgoal by auto
subgoal by (auto simp: slicep_rel_def)
subgoal by (auto simp: slicep_rel_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rprems)
subgoal by (auto simp: slice_rel_alt idx_shift_rel_def slicep_rel_take)
apply rprems
subgoal by (auto simp: slice_rel_alt idx_shift_rel_def slicep_rel_eq_outside_range slicep_rel_drop)
subgoal
apply (clarsimp simp: slice_rel_alt idx_shift_rel_def)
apply (rule conjI)
subgoal
apply (rule slicep_rel_append)
apply (subst slicep_rel_eq_outside_range; assumption?)
by auto
subgoal
apply (drule (1) eq_outside_range_gen_trans[OF _ _ refl refl])
apply (erule (1) eq_outside_range_gen_trans)
apply (auto simp: max_def algebra_simps slicep_rel_def split: if_splits)
done
done
subgoal by (auto simp: slice_rel_alt eq_outside_range_triv slicep_rel_def)
done
definition "slice_part_sorted_spec xsi l h ≡ doN { ASSERT (l≤h ∧ h≤length xsi); SPEC (λxsi'.
eq_outside_range xsi' xsi l h
∧ mset (slice l h xsi') = mset (slice l h xsi)
∧ part_sorted_wrt (le_by_lt (❙<)) is_threshold (slice l h xsi'))}"
lemma introsort_aux3_correct: "introsort_aux3 xsi l h d ≤ slice_part_sorted_spec xsi l h"
proof -
have A: "⇓ (slice_rel xsi l h) (SPEC (λxs'. mset xs' = mset (slice l h xsi) ∧ part_sorted_wrt (le_by_lt (❙<)) 16 xs'))
≤ slice_part_sorted_spec xsi l h"
apply (clarsimp simp: slice_part_sorted_spec_def pw_le_iff refine_pw_simps)
apply (auto simp: slice_rel_alt slicep_rel_def)
done
note introsort_aux3_refine[of xsi "slice l h xsi" l h d]
also note introsort_aux2_refine
also note introsort_aux1_correct
also note A
finally show ?thesis
apply (clarsimp simp: slicep_rel_def slice_part_sorted_spec_def)
by (auto simp: pw_le_iff refine_pw_simps)
qed
text ‹In the paper, we summarized steps 2 and 3. Here are the relevant lemmas: ›
lemma partition3_spec_alt: "partition3_spec xs l h = ⇓(slice_rel xs l h ×⇩r Id) (doN { ASSERT (l≤h ∧ h≤length xs); (xs⇩1,xs⇩2) ← partition1_spec (slice l h xs); RETURN (xs⇩1@xs⇩2, l+length xs⇩1) })"
unfolding partition3_spec_def partition1_spec_def
apply (auto simp: pw_eq_iff refine_pw_simps)
apply (auto simp: slice_eq_mset_def slice_rel_def in_br_conv)
subgoal
by (smt Sorting_Misc.slice_len diff_is_0_eq leD le_add_diff_inverse less_imp_le_nat less_le_trans list.size(3) mset_append slice_append)
subgoal by (metis mset_append)
subgoal
by (metis Misc.slice_len add_le_cancel_left drop_all drop_append_miracle leI le_add_diff_inverse)
subgoal
by (metis Misc.slice_def add_diff_cancel_left' append_assoc append_eq_conv_conj drop_slice drop_take drop_take_drop_unsplit)
done
corollary partition3_spec_alt': "partition3_spec xs l h = ⇓({((xsi',m),(xs⇩1,xs⇩2)). (xsi',xs⇩1@xs⇩2)∈slice_rel xs l h ∧ m=l + length xs⇩1 }) (doN { ASSERT (l≤h ∧ h≤length xs); partition1_spec (slice l h xs)})"
unfolding partition3_spec_alt
apply (auto simp: pw_eq_iff refine_pw_simps)
done
corollary partition3_spec_direct_refine: "⟦ h-l≥4; (xsi,xs)∈slicep_rel l h ⟧ ⟹ partition3_spec xsi l h ≤ ⇓({((xsi',m),(xs⇩1,xs⇩2)). (xsi',xs⇩1@xs⇩2)∈slice_rel xsi l h ∧ m=l + length xs⇩1 }) (partition1_spec xs)"
unfolding partition3_spec_alt'
apply (auto simp: pw_le_iff refine_pw_simps)
apply (auto simp: slicep_rel_def)
done
lemma slice_part_sorted_spec_alt: "slice_part_sorted_spec xsi l h = ⇓ (slice_rel xsi l h) (doN { ASSERT(l≤h ∧ h≤length xsi); SPEC (λxs'. mset xs' = mset (slice l h xsi) ∧ part_sorted_wrt (le_by_lt (❙<)) 16 xs') })"
apply (clarsimp simp: slice_part_sorted_spec_def pw_eq_iff refine_pw_simps)
apply (auto simp: slice_rel_alt slicep_rel_def eq_outside_rane_lenD)
done
lemma introsort_aux3_direct_refine_aux1': "(xs', xs⇩1 @ xs⇩2) ∈ slice_rel xs l h ⟹ xs⇩1 = slice l (l + length xs⇩1) xs'"
apply (clarsimp simp: slice_rel_def in_br_conv)
by (metis Misc.slice_def add_diff_cancel_left' append.assoc append_eq_conv_conj append_take_drop_id)
lemma introsort_aux3_direct_refine_aux1: "⟦(xsi', xs⇩1 @ xs⇩2) ∈ slice_rel xsi l' h'⟧ ⟹ (xsi', xs⇩1) ∈ slicep_rel l' (l' + length xs⇩1)"
apply (simp add: slicep_rel_def introsort_aux3_direct_refine_aux1')
apply (auto simp: slice_rel_alt slicep_rel_def)
by (metis Misc.slice_len ab_semigroup_add_class.add_ac(1) le_add1 length_append ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
lemma introsort_aux3_direct_refine: "(xsi,xs)∈slicep_rel l h ⟹ introsort_aux3 xsi l h d ≤ ⇓(slice_rel xsi l h) (introsort_aux1 xs d)"
unfolding introsort_aux3_def introsort_aux1_def
supply [refine del] = RECT_refine
supply recref = RECT_dep_refine[where
R="λ_. {((xsi::'a list, l, h, di::nat), (xs, d)). (xsi, xs) ∈ slicep_rel l h ∧ di=d}" and
S="λ_ (xsi::'a list, l, h, di::nat). slice_rel xsi l h" and
arb⇩0 = "()"
]
apply (refine_rcg
recref
slice_sort_spec_refine_sort'
partition3_spec_direct_refine
; (rule refl)?
)
subgoal by auto
subgoal by auto
subgoal by (auto simp: slicep_rel_def)
subgoal by (auto simp: slicep_rel_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rprems)
subgoal by (clarsimp simp: introsort_aux3_direct_refine_aux1)
apply rprems
subgoal
apply (auto simp: slice_rel_alt slicep_rel_def)
subgoal by (metis Misc.slice_def drop_append_miracle drop_slice eq_outside_range_def)
subgoal by (metis Nat.add_diff_assoc Sorting_Misc.slice_len add_diff_cancel_left' add_le_cancel_left diff_add_zero diff_is_0_eq length_append)
subgoal by (simp add: eq_outside_rane_lenD)
done
subgoal
apply (clarsimp simp: slice_rel_alt idx_shift_rel_def)
apply (rule conjI)
subgoal
apply (rule slicep_rel_append)
apply (subst slicep_rel_eq_outside_range; assumption?)
by auto
subgoal
apply (drule (1) eq_outside_range_gen_trans[OF _ _ refl refl])
apply (erule (1) eq_outside_range_gen_trans)
apply (auto simp: max_def algebra_simps slicep_rel_def split: if_splits)
done
done
subgoal by (auto simp: slice_rel_alt eq_outside_range_triv slicep_rel_def)
done
definition "final_sort_spec xs l h ≡ doN {
ASSERT (h-l>1 ∧ part_sorted_wrt (le_by_lt (❙<)) is_threshold (slice l h xs));
slice_sort_spec (❙<) xs l h
}"
definition "introsort3 xs l h ≡ doN {
ASSERT(l≤h);
if h-l>1 then doN {
xs ← slice_part_sorted_spec xs l h;
xs ← final_sort_spec xs l h;
RETURN xs
} else RETURN xs
}"
lemma introsort3_correct: "introsort3 xs l h ≤ slice_sort_spec (❙<) xs l h"
apply (cases "l≤h ∧ h≤length xs")
subgoal
apply (cases "1<h-l")
subgoal
unfolding introsort3_def slice_part_sorted_spec_def final_sort_spec_def slice_sort_spec_alt
by (auto simp: pw_le_iff refine_pw_simps eq_outside_rane_lenD elim: eq_outside_range_gen_trans[of _ _ l h _ l h l h, simplified])
subgoal
unfolding introsort3_def slice_sort_spec_alt slice_part_sorted_spec_def final_sort_spec_def
by (simp add: eq_outside_range_triv sorted_wrt01)
done
subgoal
unfolding slice_sort_spec_alt
apply refine_vcg
by simp
done
lemma partition3_spec_for_paper: "partition3_spec xs 0 (length xs) = doN {
ASSERT (4≤length xs);
SPEC (λ(xs',m). mset xs'=mset xs ∧ 0<m ∧ m<length xs ∧ (∀i∈{0..<m}. ∀j∈{m..<length xs}. xs'!i ❙≤ xs'!j))
}"
unfolding partition3_spec_def
apply (simp add: refine_pw_simps pw_eq_iff slice_LT_def slice_eq_mset_def Ball_def in_set_conv_nth)
apply (auto)
subgoal
by (metis slice_complete)
subgoal for a m i j
apply (drule spec[where x="a!i"])
apply (auto simp add: slice_nth)
apply (drule spec[where x="a!j"])
apply (erule mp)
apply (rule exI[where x="j-m"])
apply (auto simp add: slice_nth)
done
subgoal
by (meson mset_eq_length)
subgoal
by (metis size_mset slice_complete)
subgoal
by (metis dual_order.refl mset_eq_length)
subgoal
by (metis Misc.slice_len add.commute le_add1 less_diff_conv less_or_eq_imp_le size_mset slice_nth)
done
end
end