theory WB_Sort
imports WB_More_Refinement WB_More_Refinement_List "HOL-Library.Rewrite"
begin
text ‹Every element between \<^term>‹lo› and \<^term>‹hi› can be chosen as pivot element.›
definition choose_pivot :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat nres› where
‹choose_pivot _ _ _ lo hi = SPEC(λk. k ≥ lo ∧ k ≤ hi)›
text ‹The element at index ‹p› partitions the subarray ‹lo..hi›. This means that every element ›
definition isPartition_wrt :: ‹('b ⇒ 'b ⇒ bool) ⇒ 'b list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition_wrt R xs lo hi p ≡ (∀ i. i ≥ lo ∧ i < p ⟶ R (xs!i) (xs!p)) ∧ (∀ j. j > p ∧ j ≤ hi ⟶ R (xs!p) (xs!j))›
lemma isPartition_wrtI:
‹(⋀ i. ⟦i ≥ lo; i < p⟧ ⟹ R (xs!i) (xs!p)) ⟹ (⋀ j. ⟦j > p; j ≤ hi⟧ ⟹ R (xs!p) (xs!j)) ⟹ isPartition_wrt R xs lo hi p›
by (simp add: isPartition_wrt_def)
definition isPartition :: ‹'a :: order list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition xs lo hi p ≡ isPartition_wrt (≤) xs lo hi p›
abbreviation isPartition_map :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition_map R h xs i j k ≡ isPartition_wrt (λa b. R (h a) (h b)) xs i j k›
lemma isPartition_map_def':
‹lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹ isPartition_map R h xs lo hi p = isPartition_wrt R (map h xs) lo hi p›
by (auto simp add: isPartition_wrt_def conjI)
text ‹Example: 6 is the pivot element (with index 4); \<^term>‹7› is equal to the \<^term>‹length xs - 1›.›
lemma ‹isPartition [0,5,3,4,6,9,8,10::nat] 0 7 4›
by (auto simp add: isPartition_def isPartition_wrt_def nth_Cons')
definition sublist :: ‹'a list ⇒ nat ⇒ nat ⇒ 'a list› where
‹sublist xs i j ≡ take (Suc j - i) (drop i xs)›
lemma take_Suc0:
"l≠[] ⟹ take (Suc 0) l = [l!0]"
"0 < length l ⟹ take (Suc 0) l = [l!0]"
"Suc n ≤ length l ⟹ take (Suc 0) l = [l!0]"
by (cases l, auto)+
lemma sublist_single: ‹i < length xs ⟹ sublist xs i i = [xs!i]›
by (cases xs) (auto simp add: sublist_def take_Suc0)
lemma insert_eq: ‹insert a b = b ∪ {a}›
by auto
lemma sublist_nth: ‹⟦lo ≤ hi; hi < length xs; k+lo ≤ hi⟧ ⟹ (sublist xs lo hi)!k = xs!(lo+k)›
by (simp add: sublist_def)
lemma sublist_length: ‹⟦i ≤ j; j < length xs⟧ ⟹ length (sublist xs i j) = 1 + j - i›
by (simp add: sublist_def)
lemma sublist_not_empty: ‹⟦i ≤ j; j < length xs; xs ≠ []⟧ ⟹ sublist xs i j ≠ []›
apply simp
apply (rewrite List.length_greater_0_conv[symmetric])
apply (rewrite sublist_length)
by auto
lemma sublist_app: ‹⟦i1 ≤ i2; i2 ≤ i3⟧ ⟹ sublist xs i1 i2 @ sublist xs (Suc i2) i3 = sublist xs i1 i3›
unfolding sublist_def
by (smt Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add)
definition sorted_sublist_wrt :: ‹('b ⇒ 'b ⇒ bool) ⇒ 'b list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist_wrt R xs lo hi = sorted_wrt R (sublist xs lo hi)›
definition sorted_sublist :: ‹'a :: linorder list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist xs lo hi = sorted_sublist_wrt (≤) xs lo hi›
abbreviation sorted_sublist_map :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist_map R h xs lo hi ≡ sorted_sublist_wrt (λa b. R (h a) (h b)) xs lo hi›
lemma sorted_sublist_map_def':
‹lo < length xs ⟹ sorted_sublist_map R h xs lo hi ≡ sorted_sublist_wrt R (map h xs) lo hi›
apply (simp add: sorted_sublist_wrt_def)
by (simp add: drop_map sorted_wrt_map sublist_def take_map)
lemma sorted_sublist_wrt_refl: ‹i < length xs ⟹ sorted_sublist_wrt R xs i i›
by (auto simp add: sorted_sublist_wrt_def sublist_single)
lemma sorted_sublist_refl: ‹i < length xs ⟹ sorted_sublist xs i i›
by (auto simp add: sorted_sublist_def sorted_sublist_wrt_refl)
lemma sorted_sublist_map_refl: ‹i < length xs ⟹ sorted_sublist_map R h xs i i›
by (auto simp add: sorted_sublist_wrt_refl)
lemma sublist_map: ‹sublist (map f xs) i j = map f (sublist xs i j)›
apply (auto simp add: sublist_def)
by (simp add: drop_map take_map)
lemma take_set: ‹j ≤ length xs ⟹ x ∈ set (take j xs) ≡ (∃ k. k < j ∧ xs!k = x)›
apply (induction xs)
apply simp
by (meson in_set_conv_iff less_le_trans)
lemma drop_set: ‹j ≤ length xs ⟹ x ∈ set (drop j xs) ≡ (∃k. j≤k∧k<length xs ∧ xs!k=x)›
by (smt Misc.in_set_drop_conv_nth)
lemma sublist_el: ‹i ≤ j ⟹ j < length xs ⟹ x ∈ set (sublist xs i j) ≡ (∃ k. k < Suc j-i ∧ xs!(i+k)=x)›
apply (simp add: sublist_def)
by (auto simp add: take_set)
lemma sublist_el': ‹i ≤ j ⟹ j < length xs ⟹ x ∈ set (sublist xs i j) ≡ (∃ k. i≤k∧k≤j ∧ xs!k=x)›
apply (simp add: sublist_el)
by (smt Groups.add_ac(2) le_add1 le_add_diff_inverse less_Suc_eq less_diff_conv nat_less_le order_refl)
lemma sublist_lt: ‹hi < lo ⟹ sublist xs lo hi = []›
by (auto simp add: sublist_def)
lemma nat_le_eq_or_lt: ‹(a :: nat) ≤ b = (a = b ∨ a < b)›
by linarith
lemma sorted_sublist_wrt_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist_wrt R xs lo hi›
apply (auto simp add: nat_le_eq_or_lt)
unfolding sorted_sublist_wrt_def
subgoal apply (rewrite sublist_single) by auto
subgoal by (auto simp add: sublist_lt)
done
text ‹Elements in a sorted sublists are actually sorted›
lemma sorted_sublist_wrt_nth_le:
assumes ‹sorted_sublist_wrt R xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs› and
‹lo ≤ i› and ‹i < j› and ‹j ≤ hi›
shows ‹R (xs!i) (xs!j)›
proof -
have A: ‹lo < length xs› using assms(2) assms(3) by linarith
obtain i' where I: ‹i = lo + i'› using assms(4) le_Suc_ex by auto
obtain j' where J: ‹j = lo + j'› by (meson assms(4) assms(5) dual_order.trans le_iff_add less_imp_le_nat)
show ?thesis
using assms(1) apply (simp add: sorted_sublist_wrt_def I J)
apply (rewrite sublist_nth[symmetric, where k=i', where lo=lo, where hi=hi])
using assms apply auto subgoal using I by linarith
apply (rewrite sublist_nth[symmetric, where k=j', where lo=lo, where hi=hi])
using assms apply auto subgoal using J by linarith
apply (rule sorted_wrt_nth_less)
apply auto
subgoal using I J nat_add_left_cancel_less by blast
subgoal apply (simp add: sublist_length) using J by linarith
done
qed
text ‹We can make the assumption \<^term>‹i < j› weaker if we have a reflexivie relation.›
lemma sorted_sublist_wrt_nth_le':
assumes ref: ‹⋀ x. R x x›
and ‹sorted_sublist_wrt R xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs›
and ‹lo ≤ i› and ‹i ≤ j› and ‹j ≤ hi›
shows ‹R (xs!i) (xs!j)›
proof -
have ‹i < j ∨ i = j› using ‹i ≤ j› by linarith
then consider (a) ‹i < j› |
(b) ‹i = j› by blast
then show ?thesis
proof cases
case a
then show ?thesis
using assms(2-5,7) sorted_sublist_wrt_nth_le by blast
next
case b
then show ?thesis
by (simp add: ref)
qed
qed
lemma sorted_sublist_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist xs lo hi›
by (auto simp add: sorted_sublist_def sorted_sublist_wrt_le)
lemma sorted_sublist_map_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist_map R h xs lo hi›
by (auto simp add: sorted_sublist_wrt_le)
lemma sublist_cons: ‹lo < hi ⟹ hi < length xs ⟹ sublist xs lo hi = xs!lo # sublist xs (Suc lo) hi›
apply (simp add: sublist_def)
by (metis Cons_nth_drop_Suc Suc_diff_le le_trans less_imp_le_nat not_le take_Suc_Cons)
lemma sorted_sublist_wrt_cons':
‹sorted_sublist_wrt R xs (lo+1) hi ⟹ lo ≤ hi ⟹ hi < length xs ⟹ (∀j. lo<j∧j≤hi ⟶ R (xs!lo) (xs!j)) ⟹ sorted_sublist_wrt R xs lo hi›
apply (simp add: sorted_sublist_wrt_def)
apply (auto simp add: nat_le_eq_or_lt)
subgoal by (simp add: sublist_single)
apply (auto simp add: sublist_cons sublist_el)
by (metis Suc_lessI ab_semigroup_add_class.add.commute less_add_Suc1 less_diff_conv)
lemma sorted_sublist_wrt_cons:
assumes trans: ‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z)› and
‹sorted_sublist_wrt R xs (lo+1) hi› and
‹lo ≤ hi› and ‹hi < length xs › and ‹R (xs!lo) (xs!(lo+1))›
shows ‹sorted_sublist_wrt R xs lo hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_cons') using assms apply auto
subgoal premises assms' for j
proof -
have A: ‹j=lo+1 ∨ j>lo+1› using assms'(5) by linarith
show ?thesis
using A proof
assume A: ‹j=lo+1› show ?thesis
by (simp add: A assms')
next
assume A: ‹j>lo+1› show ?thesis
apply (rule trans)
apply (rule assms(5))
apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=‹lo+1›, where j=j])
subgoal using A assms'(6) by linarith
subgoal using assms'(3) less_imp_diff_less by blast
subgoal using assms'(5) by auto
subgoal using A by linarith
subgoal by (simp add: assms'(6))
done
qed
qed
done
qed
lemma sorted_sublist_map_cons:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
sorted_sublist_map R h xs (lo+1) hi ⟹ lo ≤ hi ⟹ hi < length xs ⟹ R (h (xs!lo)) (h (xs!(lo+1))) ⟹ sorted_sublist_map R h xs lo hi›
by (blast intro: sorted_sublist_wrt_cons)
lemma sublist_snoc: ‹lo < hi ⟹ hi < length xs ⟹ sublist xs lo hi = sublist xs lo (hi-1) @ [xs!hi]›
apply (simp add: sublist_def)
proof -
assume a1: "lo < hi"
assume "hi < length xs"
then have "take lo xs @ take (Suc hi - lo) (drop lo xs) = (take lo xs @ take (hi - lo) (drop lo xs)) @ [xs ! hi]"
using a1 by (metis (no_types) Suc_diff_le add_Suc_right hd_drop_conv_nth le_add_diff_inverse less_imp_le_nat take_add take_hd_drop)
then show "take (Suc hi - lo) (drop lo xs) = take (hi - lo) (drop lo xs) @ [xs ! hi]"
by simp
qed
lemma sorted_sublist_wrt_snoc':
‹sorted_sublist_wrt R xs lo (hi-1) ⟹ lo ≤ hi ⟹ hi < length xs ⟹ (∀j. lo≤j∧j<hi ⟶ R (xs!j) (xs!hi)) ⟹ sorted_sublist_wrt R xs lo hi›
apply (simp add: sorted_sublist_wrt_def)
apply (auto simp add: nat_le_eq_or_lt)
subgoal by (simp add: sublist_single)
apply (auto simp add: sublist_snoc sublist_el sorted_wrt_append)
by (metis less_diff_conv linorder_neqE_nat linordered_field_class.sign_simps(2) not_add_less1)
lemma sorted_sublist_wrt_snoc:
assumes trans: ‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z)› and
‹sorted_sublist_wrt R xs lo (hi-1)› and
‹lo ≤ hi› and ‹hi < length xs› and ‹(R (xs!(hi-1)) (xs!hi))›
shows ‹sorted_sublist_wrt R xs lo hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_snoc') using assms apply auto
subgoal premises assms' for j
proof -
have A: ‹j=hi-1 ∨ j<hi-1› using assms'(6) by linarith
show ?thesis
using A proof
assume A: ‹j=hi-1› show ?thesis
by (simp add: A assms')
next
assume A: ‹j<hi-1› show ?thesis
apply (rule trans)
apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=j, where j=‹hi-1›])
prefer 6
apply (rule assms(5))
apply auto
subgoal using A assms'(5) by linarith
subgoal using assms'(3) less_imp_diff_less by blast
subgoal using assms'(5) by auto
subgoal using A by linarith
done
qed
qed
done
qed
lemma sorted_sublist_map_snoc:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
sorted_sublist_map R h xs lo (hi-1) ⟹
lo ≤ hi ⟹ hi < length xs ⟹ (R (h (xs!(hi-1))) (h (xs!hi))) ⟹ sorted_sublist_map R h xs lo hi›
by (blast intro: sorted_sublist_wrt_snoc)
lemma sublist_split: ‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹ sublist xs lo p @ sublist xs (p+1) hi = sublist xs lo hi›
apply (auto simp add: sublist_def)
by (smt Suc_leI append_assoc append_eq_append_conv diff_Suc_Suc drop_take_drop_drop le_SucI le_trans nat_less_le)
lemma sublist_split_part: ‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹ sublist xs lo (p-1) @ xs!p # sublist xs (p+1) hi = sublist xs lo hi›
apply (auto simp add: sublist_split[symmetric])
apply (rewrite sublist_snoc[where xs=xs,where lo=lo,where hi=p])
by auto
text ‹A property for partitions (we always assume that \<^term>‹R› is transitive.›
lemma isPartition_wrt_trans:
‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z) ⟹
isPartition_wrt R xs lo hi p ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j))›
by (auto simp add: isPartition_wrt_def)
lemma isPartition_map_trans:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
hi < length xs ⟹
isPartition_map R h xs lo hi p ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (h (xs!i)) (h (xs!j)))›
by (auto simp add: isPartition_wrt_def)
lemma merge_sorted_wrt_partitions_between':
‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p-1) ⟹ sorted_sublist_wrt R xs (p+1) hi ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j)) ⟹
sorted_sublist_wrt R xs lo hi›
apply (auto simp add: isPartition_def isPartition_wrt_def sorted_sublist_def sorted_sublist_wrt_def sublist_map)
apply (simp add: sublist_split_part[symmetric])
apply (auto simp add: List.sorted_wrt_append)
subgoal by (auto simp add: sublist_el)
subgoal by (auto simp add: sublist_el)
subgoal by (auto simp add: sublist_el')
done
lemma merge_sorted_wrt_partitions_between:
‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z) ⟹
isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p-1) ⟹ sorted_sublist_wrt R xs (p+1) hi ⟹
lo ≤ hi ⟹ hi < length xs ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
sorted_sublist_wrt R xs lo hi›
by (simp add: merge_sorted_wrt_partitions_between' isPartition_wrt_trans)
text ‹The main theorem to merge sorted lists›
lemma merge_sorted_wrt_partitions:
‹isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p - Suc 0) ⟹ sorted_sublist_wrt R xs (Suc p) hi ⟹
lo ≤ hi ⟹ lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j)) ⟹
sorted_sublist_wrt R xs lo hi›
subgoal premises assms
proof -
have C: ‹lo=p∧p=hi ∨ lo=p∧p<hi ∨ lo<p∧p=hi ∨ lo<p∧p<hi›
using assms by linarith
show ?thesis
using C apply auto
subgoal
apply (rule sorted_sublist_wrt_refl)
using assms by auto
subgoal
using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_cons')
subgoal
using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_snoc')
subgoal
using assms
apply (rewrite merge_sorted_wrt_partitions_between'[where p=p])
by auto
done
qed
done
theorem merge_sorted_map_partitions:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
isPartition_map R h xs lo hi p ⟹
sorted_sublist_map R h xs lo (p - Suc 0) ⟹ sorted_sublist_map R h xs (Suc p) hi ⟹
lo ≤ hi ⟹ lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹
sorted_sublist_map R h xs lo hi›
apply (rule merge_sorted_wrt_partitions) apply auto
by (simp add: merge_sorted_wrt_partitions isPartition_map_trans)
lemma partition_wrt_extend:
‹isPartition_wrt R xs lo' hi' p ⟹
hi < length xs ⟹
lo ≤ lo' ⟹ lo' ≤ hi ⟹ hi' ≤ hi ⟹
lo' ≤ p ⟹ p ≤ hi' ⟹
(⋀ i. lo≤i ⟹ i <lo' ⟹ R (xs!i) (xs!p)) ⟹
(⋀ j. hi'<j ⟹ j≤hi ⟹ R (xs!p) (xs!j)) ⟹
isPartition_wrt R xs lo hi p›
unfolding isPartition_wrt_def
apply auto
subgoal by (meson not_le)
subgoal by (metis nat_le_eq_or_lt nat_le_linear)
done
lemma partition_map_extend:
‹isPartition_map R h xs lo' hi' p ⟹
hi < length xs ⟹
lo ≤ lo' ⟹ lo' ≤ hi ⟹ hi' ≤ hi ⟹
lo' ≤ p ⟹ p ≤ hi' ⟹
(⋀ i. lo≤i ⟹ i <lo' ⟹ R (h (xs!i)) (h (xs!p))) ⟹
(⋀ j. hi'<j ⟹ j≤hi ⟹ R (h (xs!p)) (h (xs!j))) ⟹
isPartition_map R h xs lo hi p›
by (auto simp add: partition_wrt_extend)
lemma isPartition_empty:
‹(⋀ j. ⟦lo < j; j ≤ hi⟧ ⟹ R (xs ! lo) (xs ! j)) ⟹
isPartition_wrt R xs lo hi lo›
by (auto simp add: isPartition_wrt_def)
lemma take_ext:
‹(∀i<k. xs'!i=xs!i) ⟹
k < length xs ⟹ k < length xs' ⟹
take k xs' = take k xs›
by (simp add: nth_take_lemma)
lemma drop_ext':
‹(∀i. i≥k ∧ i<length xs ⟶ xs'!i=xs!i) ⟹
0<k ⟹ xs≠[] ⟹ ― ‹These corner cases will be dealt with in the next lemma›
length xs'=length xs ⟹
drop k xs' = drop k xs›
apply (rewrite in ‹drop _ ⌑ = _› List.rev_rev_ident[symmetric])
apply (rewrite in ‹_ = drop _ ⌑› List.rev_rev_ident[symmetric])
apply (rewrite in ‹⌑ = _› List.drop_rev)
apply (rewrite in ‹_ = ⌑› List.drop_rev)
apply simp
apply (rule take_ext)
by (auto simp add: nth_rev)
lemma drop_ext:
‹(∀i. i≥k ∧ i<length xs ⟶ xs'!i=xs!i) ⟹
length xs'=length xs ⟹
drop k xs' = drop k xs›
apply (cases xs)
apply auto
apply (cases k)
subgoal by (simp add: nth_equalityI)
subgoal apply (rule drop_ext') by auto
done
lemma sublist_ext':
‹(∀i. lo≤i∧i≤hi ⟶ xs'!i=xs!i) ⟹
length xs' = length xs ⟹
lo ≤ hi ⟹ Suc hi < length xs ⟹
sublist xs' lo hi = sublist xs lo hi›
apply (simp add: sublist_def)
apply (rule take_ext)
by auto
lemma lt_Suc: ‹(a < b) = (Suc a = b ∨ Suc a < b)›
by auto
lemma sublist_until_end_eq_drop: ‹Suc hi = length xs ⟹ sublist xs lo hi = drop lo xs›
by (simp add: sublist_def)
lemma sublist_ext:
‹(∀i. lo≤i∧i≤hi ⟶ xs'!i=xs!i) ⟹
length xs' = length xs ⟹
lo ≤ hi ⟹ hi < length xs ⟹
sublist xs' lo hi = sublist xs lo hi›
apply (auto simp add: lt_Suc[where a=hi])
subgoal by (auto simp add: sublist_until_end_eq_drop drop_ext)
subgoal by (auto simp add: sublist_ext')
done
lemma sorted_wrt_lower_sublist_still_sorted:
assumes ‹sorted_sublist_wrt R xs lo (lo' - Suc 0)› and
‹lo ≤ lo'› and ‹lo' < length xs› and
‹(∀ i. lo≤i∧i<lo' ⟶ xs'!i=xs!i)› and ‹length xs' = length xs›
shows ‹sorted_sublist_wrt R xs' lo (lo' - Suc 0)›
proof -
have l: ‹lo < lo' - 1 ∨ lo ≥ lo'-1›
by linarith
show ?thesis
using l apply auto
subgoal
apply (auto simp add: sorted_sublist_wrt_def)
apply (rewrite sublist_ext[where xs=xs])
using assms by (auto simp add: sorted_sublist_wrt_def)
subgoal
using assms by (auto simp add: sorted_sublist_wrt_le)
done
qed
lemma sorted_map_lower_sublist_still_sorted:
assumes ‹sorted_sublist_map R h xs lo (lo' - Suc 0)› and
‹lo ≤ lo'› and ‹lo' < length xs› and
‹(∀ i. lo≤i∧i<lo' ⟶ xs'!i=xs!i)› and ‹length xs' = length xs›
shows ‹sorted_sublist_map R h xs' lo (lo' - Suc 0)›
using assms by (rule sorted_wrt_lower_sublist_still_sorted)
lemma sorted_wrt_upper_sublist_still_sorted:
assumes ‹sorted_sublist_wrt R xs (hi'+1) hi› and
‹lo ≤ lo'› and ‹hi < length xs› and
‹∀ j. hi'<j∧j≤hi ⟶ xs'!j=xs!j› and ‹length xs' = length xs›
shows ‹sorted_sublist_wrt R xs' (hi'+1) hi›
proof -
have l: ‹hi' + 1 < hi ∨ hi' + 1 ≥ hi›
by linarith
show ?thesis
using l apply auto
subgoal
apply (auto simp add: sorted_sublist_wrt_def)
apply (rewrite sublist_ext[where xs=xs])
using assms by (auto simp add: sorted_sublist_wrt_def)
subgoal
using assms by (auto simp add: sorted_sublist_wrt_le)
done
qed
lemma sorted_map_upper_sublist_still_sorted:
assumes ‹sorted_sublist_map R h xs (hi'+1) hi› and
‹lo ≤ lo'› and ‹hi < length xs› and
‹∀ j. hi'<j∧j≤hi ⟶ xs'!j=xs!j› and ‹length xs' = length xs›
shows ‹sorted_sublist_map R h xs' (hi'+1) hi›
using assms by (rule sorted_wrt_upper_sublist_still_sorted)
text ‹The specification of the partition function›
definition partition_spec :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat ⇒ bool› where
‹partition_spec R h xs lo hi xs' p ≡
mset xs' = mset xs ∧ ― ‹The list is a permutation›
isPartition_map R h xs' lo hi p ∧ ― ‹We have a valid partition on the resulting list›
lo ≤ p ∧ p ≤ hi ∧ ― ‹The partition index is in bounds›
(∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i)›
lemma mathias:
assumes
Perm: ‹mset xs' = mset xs›
and I: ‹lo≤i› ‹i≤hi› ‹xs'!i=x›
and Bounds: ‹hi < length xs›
and Fix: ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
shows ‹∃j. lo≤j∧j≤hi ∧ xs!j = x›
proof -
define xs1 xs2 xs3 xs1' xs2' xs3' where
‹xs1 = take lo xs› and
‹xs2 = take (Suc hi - lo) (drop lo xs)› and
‹xs3 = drop (Suc hi) xs› and
‹xs1' = take lo xs'› and
‹xs2' = take (Suc hi - lo) (drop lo xs')› and
‹xs3' = drop (Suc hi) xs'›
have [simp]: ‹length xs' = length xs›
using Perm by (auto dest: mset_eq_length)
have [simp]: ‹mset xs1 = mset xs1'›
using Fix(1) unfolding xs1_def xs1'_def
by (metis Perm le_cases mset_eq_length nth_take_lemma take_all)
have [simp]: ‹mset xs3 = mset xs3'›
using Fix(2) unfolding xs3_def xs3'_def mset_drop_upto
by (auto intro: image_mset_cong2)
have ‹xs = xs1 @ xs2 @ xs3› ‹xs' = xs1' @ xs2' @ xs3'›
using I unfolding xs1_def xs2_def xs3_def xs1'_def xs2'_def xs3'_def
by (metis append.assoc append_take_drop_id le_SucI le_add_diff_inverse order_trans take_add)+
moreover have ‹xs ! i = xs2 ! (i - lo)› ‹i ≥ length xs1›
using I Bounds unfolding xs2_def xs1_def by (auto simp: nth_take min_def)
moreover have ‹x ∈ set xs2'›
using I Bounds unfolding xs2'_def
by (auto simp: in_set_take_conv_nth
intro!: exI[of _ ‹i - lo›])
ultimately have ‹x ∈ set xs2›
using Perm I by (auto dest: mset_eq_setD)
then obtain j where ‹xs ! (lo + j) = x› ‹j ≤ hi - lo›
unfolding in_set_conv_nth xs2_def
by auto
then show ?thesis
using Bounds I
by (auto intro: exI[of _ ‹lo+j›])
qed
text ‹If we fix the left and right rest of two permutated lists, then the sublists are also permutations.›
text ‹But we only need that the sets are equal.›
lemma mset_sublist_incl:
assumes Perm: ‹mset xs' = mset xs›
and Fix: ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) ⊆ set (sublist xs lo hi)›
proof
fix x
assume ‹x ∈ set (sublist xs' lo hi)›
then have ‹∃i. lo≤i∧i≤hi ∧ xs'!i=x›
by (metis assms(1) bounds(1) bounds(2) size_mset sublist_el')
then obtain i where I: ‹lo≤i› ‹i≤hi› ‹xs'!i=x› by blast
have ‹∃j. lo≤j∧j≤hi ∧ xs!j=x›
using Perm I bounds(2) Fix by (rule mathias, auto)
then show ‹x ∈ set (sublist xs lo hi)›
by (simp add: bounds(1) bounds(2) sublist_el')
qed
lemma mset_sublist_eq:
assumes ‹mset xs' = mset xs›
and ‹⋀ i. i<lo ⟹ xs'!i = xs!i›
and ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
proof
show ‹set (sublist xs' lo hi) ⊆ set (sublist xs lo hi)›
apply (rule mset_sublist_incl)
using assms by auto
show ‹set (sublist xs lo hi) ⊆ set (sublist xs' lo hi)›
apply (rule mset_sublist_incl)
by (metis assms size_mset)+
qed
text ‹Our abstract recursive quicksort procedure. We abstract over a partition procedure.›
definition quicksort :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat × nat × 'a list ⇒ 'a list nres› where
‹quicksort R h = (λ(lo,hi,xs0). do {
RECT (λf (lo,hi,xs). do {
ASSERT(lo ≤ hi ∧ hi < length xs ∧ mset xs = mset xs0); ― ‹Premise for a partition function›
(xs, p) ← SPEC(uncurry (partition_spec R h xs lo hi)); ― ‹Abstract partition function›
ASSERT(mset xs = mset xs0);
xs ← (if p-1≤lo then RETURN xs else f (lo, p-1, xs));
ASSERT(mset xs = mset xs0);
if hi≤p+1 then RETURN xs else f (p+1, hi, xs)
}) (lo,hi,xs0)
})›
text ‹As premise for quicksor, we only need that the indices are ok.›
definition quicksort_pre :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list ⇒ bool› where
‹quicksort_pre R h xs0 lo hi xs ≡ lo ≤ hi ∧ hi < length xs ∧ mset xs = mset xs0›
definition quicksort_post :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ 'a list ⇒ bool› where
‹quicksort_post R h lo hi xs xs' ≡
mset xs' = mset xs ∧
sorted_sublist_map R h xs' lo hi ∧
(∀ i. i<lo ⟶ xs'!i = xs!i) ∧
(∀ j. hi<j∧j<length xs ⟶ xs'!j = xs!j)›
text ‹Convert Pure to HOL›
lemma quicksort_postI:
‹⟦mset xs' = mset xs; sorted_sublist_map R h xs' lo hi; (⋀ i. ⟦i<lo⟧ ⟹ xs'!i = xs!i); (⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j)⟧ ⟹ quicksort_post R h lo hi xs xs'›
by (auto simp add: quicksort_post_def)
text ‹The first case for the correctness proof of (abstract) quicksort: We assume that we called the partition function, and we have \<^term>‹p-1≤lo› and \<^term>‹hi≤p+1›.›
lemma quicksort_correct_case1:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹p-1 ≤ lo› ‹hi ≤ p+1›
shows ‹quicksort_post R h lo hi xs xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have sorted_lower: ‹sorted_sublist_map R h xs' lo (p - Suc 0)›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal using ifs(1) by auto
subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
done
qed
have sorted_upper: ‹sorted_sublist_map R h xs' (Suc p) hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal using ifs(2) by auto
subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
done
qed
have sorted_middle: ‹sorted_sublist_map R h xs' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule part)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis part(1) pre(2) size_mset)
done
qed
show ?thesis
proof (intro quicksort_postI)
show ‹mset xs' = mset xs›
by (simp add: part(1))
next
show ‹sorted_sublist_map R h xs' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs' ! i = xs ! i›
using part(6) by blast
next
show ‹⋀j. ⟦hi < j; j < length xs⟧ ⟹ xs' ! j = xs ! j›
by (metis part(1) part(7) size_mset)
qed
qed
text ‹In the second case, we have to show that the precondition still holds for (p+1, hi, x') after the partition.›
lemma quicksort_correct_case2:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ hi ≤ p + 1›
shows ‹quicksort_pre R h xs0 (Suc p) hi xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs = mset xs0›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹Suc p ≤ hi›
using ifs by linarith
show ‹hi < length xs'›
by (metis part(1) pre(2) size_mset)
show ‹mset xs' = mset xs0›
using pre(3) part(1) by (auto dest: mset_eq_setD)
qed
qed
lemma quicksort_post_set:
assumes ‹quicksort_post R h lo hi xs xs'›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
proof -
have ‹mset xs' = mset xs› ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
using assms by (auto simp add: quicksort_post_def)
then show ?thesis
using bounds by (rule mset_sublist_eq, auto)
qed
text ‹In the third case, we have run quicksort recursively on (p+1, hi, xs') after the partition, with hi<=p+1 and p-1<=lo.›
lemma quicksort_correct_case3:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1': ‹quicksort_post R h (Suc p) hi xs' xs''›
shows ‹quicksort_post R h lo hi xs xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs = mset xs0›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' (Suc p) hi›
‹⋀ i. i<Suc p ⟹ xs'' ! i = xs' ! i› ‹⋀ j. ⟦hi < j; j < length xs'⟧ ⟹ xs'' ! j = xs' ! j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']
have still_partition: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
text ‹This holds because this part hasn't changed›
using IH1(3) ‹i < p› ‹lo ≤ i› isPartition_wrt_def part(3) by fastforce
next
fix j assume ‹p < j› ‹j ≤ hi›
text ‹Obtain the position \<^term>‹posJ› where \<^term>‹xs''!j› was stored in \<^term>‹xs'›.›
have ‹xs''!j ∈ set (sublist xs'' (Suc p) hi)›
by (metis IH1(1) Suc_leI ‹j ≤ hi› ‹p < j› less_le_trans mset_eq_length part(1) pre(2) sublist_el')
then have ‹xs''!j ∈ set (sublist xs' (Suc p) hi)›
by (metis IH1_perm ifs(2) nat_le_linear part(1) pre(2) size_mset)
then have ‹∃ posJ. Suc p≤posJ∧posJ≤hi ∧ xs''!j = xs'!posJ›
by (metis Suc_leI ‹j ≤ hi› ‹p < j› less_le_trans part(1) pre(2) size_mset sublist_el')
then obtain posJ :: nat where PosJ: ‹Suc p≤posJ› ‹posJ≤hi› ‹xs''!j = xs'!posJ› by blast
then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
by (metis IH1(3) Suc_le_lessD isPartition_wrt_def lessI part(3))
qed
have sorted_lower: ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal by (simp add: ifs(1))
subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
done
qed
note sorted_upper = IH1(2)
have sorted_middle: ‹sorted_sublist_map R h xs'' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) part(1) pre(2) size_mset)
done
qed
show ?thesis
proof (intro quicksort_postI)
show ‹mset xs'' = mset xs›
using part(1) IH1(1) by auto
next
show ‹sorted_sublist_map R h xs'' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs'' ! i = xs ! i›
using IH1(3) le_SucI part(4) part(6) by auto
next show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs'' ! j = xs ! j›
by (metis IH1(4) part(1) part(7) size_mset)
qed
qed
text ‹In the 4th case, we have to show that the premise holds for \<^term>‹(lo,p-1,xs')›, in case \<^term>‹¬p-1≤lo››
text ‹Analogous to case 2.›
lemma quicksort_correct_case4:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ p - Suc 0 ≤ lo ›
shows ‹quicksort_pre R h xs0 lo (p-Suc 0) xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs0 = mset xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹lo ≤ p - Suc 0›
using ifs by linarith
show ‹p - Suc 0 < length xs'›
using mset_eq_length part(1) part(5) pre(2) by fastforce
show ‹mset xs' = mset xs0›
using pre(3) part(1) by (auto dest: mset_eq_setD)
qed
qed
text ‹In the 5th case, we have run quicksort recursively on (lo, p-1, xs').›
lemma quicksort_correct_case5:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ p - Suc 0 ≤ lo› ‹hi ≤ Suc p›
and IH1': ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
shows ‹quicksort_post R h lo hi xs xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']
have still_partition: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
text ‹Obtain the position \<^term>‹posI› where \<^term>‹xs''!i› was stored in \<^term>‹xs'›.›
have ‹xs''!i ∈ set (sublist xs'' lo (p-Suc 0))›
by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred ‹i < p› ‹lo ≤ i› le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
then have ‹xs''!i ∈ set (sublist xs' lo (p-Suc 0))›
by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
then have ‹∃ posI. lo≤posI∧posI≤p-Suc 0 ∧ xs''!i = xs'!posI›
proof -
have "p - Suc 0 < length xs"
by (meson diff_le_self le_less_trans part(5) pre(2))
then show ?thesis
by (metis (no_types) ‹xs'' ! i ∈ set (sublist xs' lo (p - Suc 0))› ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
qed
then obtain posI :: nat where PosI: ‹lo≤posI› ‹posI≤p-Suc 0› ‹xs''!i = xs'!posI› by blast
then show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
by (metis (no_types, lifting) IH1(4) ‹i < p› diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
next
fix j assume ‹p < j› ‹j ≤ hi›
then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
text ‹This holds because this part hasn't changed›
by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
qed
note sorted_lower = IH1(2)
have sorted_upper: ‹sorted_sublist_map R h xs'' (Suc p) hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal by (simp add: ifs(2))
subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
done
qed
have sorted_middle: ‹sorted_sublist_map R h xs'' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) part(1) pre(2) size_mset)
done
qed
show ?thesis
proof (intro quicksort_postI)
show ‹mset xs'' = mset xs›
by (simp add: IH1(1) part(1))
next
show ‹sorted_sublist_map R h xs'' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs'' ! i = xs ! i›
by (simp add: IH1(3) part(6))
next
show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs'' ! j = xs ! j›
by (metis IH1(4) diff_le_self dual_order.strict_trans2 mset_eq_length part(1) part(5) part(7))
qed
qed
text ‹In the 6th case, we have run quicksort recursively on (lo, p-1, xs'). We show the precondition on the second call on (p+1, hi, xs'')›
lemma quicksort_correct_case6:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1: ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
shows ‹quicksort_pre R h xs0 (Suc p) hi xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs0 = mset xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1 by (auto simp add: quicksort_post_def)
show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹Suc p ≤ hi›
using ifs(2) by linarith
show ‹hi < length xs''›
using IH1(1) mset_eq_length part(1) pre(2) by fastforce
show ‹mset xs'' = mset xs0›
using pre(3) part(1) IH1(1) by (auto dest: mset_eq_setD)
qed
qed
text ‹In the 7th (and last) case, we have run quicksort recursively on (lo, p-1, xs'). We show the postcondition on the second call on (p+1, hi, xs'')›
lemma quicksort_correct_case7:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1': ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
and IH2': ‹quicksort_post R h (Suc p) hi xs'' xs'''›
shows ‹quicksort_post R h lo hi xs xs'''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']
have IH2: ‹mset xs''' = mset xs''› ‹sorted_sublist_map R h xs''' (Suc p) hi›
‹⋀ i. i<Suc p ⟹ xs'''!i = xs''!i› ‹⋀ j. ⟦hi<j; j<length xs''⟧ ⟹ xs'''!j = xs''!j›
using IH2' by (auto simp add: quicksort_post_def)
note IH2_perm = quicksort_post_set[OF IH2']
text ‹We still have a partition after the first call (same as in case 5)›
have still_partition1: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
text ‹Obtain the position \<^term>‹posI› where \<^term>‹xs''!i› was stored in \<^term>‹xs'›.›
have ‹xs''!i ∈ set (sublist xs'' lo (p-Suc 0))›
by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred ‹i < p› ‹lo ≤ i› le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
then have ‹xs''!i ∈ set (sublist xs' lo (p-Suc 0))›
by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
then have ‹∃ posI. lo≤posI∧posI≤p-Suc 0 ∧ xs''!i = xs'!posI›
proof -
have "p - Suc 0 < length xs"
by (meson diff_le_self le_less_trans part(5) pre(2))
then show ?thesis
by (metis (no_types) ‹xs'' ! i ∈ set (sublist xs' lo (p - Suc 0))› ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
qed
then obtain posI :: nat where PosI: ‹lo≤posI› ‹posI≤p-Suc 0› ‹xs''!i = xs'!posI› by blast
then show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
by (metis (no_types, lifting) IH1(4) ‹i < p› diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
next
fix j assume ‹p < j› ‹j ≤ hi›
then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
text ‹This holds because this part hasn't changed›
by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
qed
text ‹We still have a partition after the second call (similar as in case 3)›
have still_partition2: ‹isPartition_map R h xs''' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
show ‹R (h (xs''' ! i)) (h (xs''' ! p))›
text ‹This holds because this part hasn't changed›
using IH2(3) ‹i < p› ‹lo ≤ i› isPartition_wrt_def still_partition1 by fastforce
next
fix j assume ‹p < j› ‹j ≤ hi›
text ‹Obtain the position \<^term>‹posJ› where \<^term>‹xs'''!j› was stored in \<^term>‹xs'''›.›
have ‹xs'''!j ∈ set (sublist xs''' (Suc p) hi)›
by (metis IH1(1) IH2(1) Suc_leI ‹j ≤ hi› ‹p < j› ifs(2) nat_le_linear part(1) pre(2) size_mset sublist_el')
then have ‹xs'''!j ∈ set (sublist xs'' (Suc p) hi)›
by (metis IH1(1) IH2_perm ifs(2) mset_eq_length nat_le_linear part(1) pre(2))
then have ‹∃ posJ. Suc p≤posJ∧posJ≤hi ∧ xs'''!j = xs''!posJ›
by (metis IH1(1) ifs(2) mset_eq_length nat_le_linear part(1) pre(2) sublist_el')
then obtain posJ :: nat where PosJ: ‹Suc p≤posJ› ‹posJ≤hi› ‹xs'''!j = xs''!posJ› by blast
then show ‹R (h (xs''' ! p)) (h (xs''' ! j))›
proof -
have "∀n na as p. (p (as ! na::'a) (as ! posJ) ∨ posJ ≤ na) ∨ ¬ isPartition_wrt p as n hi na"
by (metis (no_types) PosJ(2) isPartition_wrt_def not_less)
then show ?thesis
by (metis IH2(3) PosJ(1) PosJ(3) lessI not_less_eq_eq still_partition1)
qed
qed
text ‹We have that the lower part is sorted after the first recursive call›
note sorted_lower1 = IH1(2)
text ‹We show that it is still sorted after the second call.›
have sorted_lower2: ‹sorted_sublist_map R h xs''' lo (p-Suc 0)›
proof -
show ?thesis
using sorted_lower1 apply (rule sorted_wrt_lower_sublist_still_sorted)
subgoal by (rule part)
subgoal
using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
subgoal
by (simp add: IH2(3))
subgoal
by (metis IH2(1) size_mset)
done
qed
text ‹The second IH gives us the the upper list is sorted after the second recursive call›
note sorted_upper2 = IH2(2)
text ‹Finally, we have to show that the entire list is sorted after the second recursive call.›
have sorted_middle: ‹sorted_sublist_map R h xs''' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition2)
subgoal by (rule sorted_lower2)
subgoal by (rule sorted_upper2)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) IH2(1) part(1) pre(2) size_mset)
done
qed
show ?thesis
proof (intro quicksort_postI)
show ‹mset xs''' = mset xs›
by (simp add: IH1(1) IH2(1) part(1))
next
show ‹sorted_sublist_map R h xs''' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs''' ! i = xs ! i›
using IH1(3) IH2(3) part(4) part(6) by auto
next
show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs''' ! j = xs ! j›
by (metis IH1(1) IH1(4) IH2(4) diff_le_self ifs(2) le_SucI less_le_trans nat_le_eq_or_lt not_less part(1) part(7) size_mset)
qed
qed
text ‹We can now show the correctness of the abstract quicksort procedure, using the refinement framework and the above case lemmas.›
lemma quicksort_correct:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and Pre: ‹lo0 ≤ hi0› ‹hi0 < length xs0›
shows ‹quicksort R h (lo0,hi0,xs0) ≤ ⇓ Id (SPEC(λxs. quicksort_post R h lo0 hi0 xs0 xs))›
proof -
have wf: ‹wf (measure (λ(lo, hi, xs). Suc hi - lo))›
by auto
define pre where ‹pre = (λ(lo,hi,xs). quicksort_pre R h xs0 lo hi xs)›
define post where ‹post = (λ(lo,hi,xs). quicksort_post R h lo hi xs)›
have pre: ‹pre (lo0,hi0,xs0)›
unfolding quicksort_pre_def pre_def by (simp add: Pre)
text ‹We first generalize the goal a over all states.›
have ‹WB_Sort.quicksort R h (lo0,hi0,xs0) ≤ ⇓ Id (SPEC (post (lo0,hi0,xs0)))›
unfolding quicksort_def prod.case
apply (rule RECT_rule)
apply (refine_mono)
apply (rule wf)
apply (rule pre)
subgoal premises IH for f x
apply (refine_vcg ASSERT_leI)
unfolding pre_def post_def
subgoal
using IH(2) by (simp add: quicksort_pre_def pre_def)
subgoal
using IH(2) by (simp add: quicksort_pre_def pre_def)
subgoal
using IH(2) by (auto simp add: quicksort_pre_def pre_def dest: mset_eq_setD)
text ‹Termination case: \<^term>‹(p-1 ≤ lo')› and \<^term>‹(hi' ≤ p+1)›; directly show postcondition›
subgoal unfolding partition_spec_def by (auto dest: mset_eq_setD)
subgoal
apply -
using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
using trans lin apply (rule quicksort_correct_case1) by auto
text ‹Case \<^term>‹(p-1 ≤ lo')› and \<^term>‹(hi' < p+1)› (Only second recursive call)›
subgoal
apply (rule IH(1)[THEN order_trans])
text ‹Show that the invariant holds for the second recursive call›
subgoal
using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
apply (rule quicksort_correct_case2) by auto
text ‹Wellfoundness (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
text ‹Show that the postcondition holds›
subgoal
apply (simp add: Misc.subset_Collect_conv post_def, intro allI impI, elim conjE)
using trans lin apply (rule quicksort_correct_case3)
using IH(2) unfolding pre_def by auto
done
text ‹Case: At least the first recursive call›
subgoal
apply (rule IH(1)[THEN order_trans])
text ‹Show that the precondition holds for the first recursive call›
subgoal
using IH(2) unfolding pre_def post_def apply (simp, elim conjE, split prod.splits) apply auto
apply (rule quicksort_correct_case4) by auto
text ‹Wellfoundness for first recursive call (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
text ‹Simplify some refinement suff...›
apply (simp add: Misc.subset_Collect_conv ASSERT_leI, intro allI impI conjI, elim conjE)
apply (rule ASSERT_leI)
apply (simp_all add: Misc.subset_Collect_conv ASSERT_leI)
subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
text ‹Only the first recursive call: show postcondition›
subgoal
using trans lin apply (rule quicksort_correct_case5)
using IH(2) unfolding pre_def post_def by auto
apply (rule ASSERT_leI)
subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
text ‹Both recursive calls.›
subgoal
apply (rule IH(1)[THEN order_trans])
text ‹Show precondition for second recursive call (after the first call)›
subgoal
unfolding pre_def post_def
apply auto
apply (rule quicksort_correct_case6)
using IH(2) unfolding pre_def post_def by auto
text ‹Wellfoundedness for second recursive call (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
text ‹Show that the postcondition holds (after both recursive calls)›
subgoal
apply (simp add: Misc.subset_Collect_conv, intro allI impI, elim conjE)
using trans lin apply (rule quicksort_correct_case7)
using IH(2) unfolding pre_def post_def by auto
done
done
done
done
text ‹Finally, apply the generalized lemma to show the thesis.›
then show ?thesis unfolding post_def by auto
qed
definition partition_main_inv :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ (nat×nat×'a list) ⇒ bool› where
‹partition_main_inv R h lo hi xs0 p ≡
case p of (i,j,xs) ⇒
j < length xs ∧ j ≤ hi ∧ i < length xs ∧ lo ≤ i ∧ i ≤ j ∧ mset xs = mset xs0 ∧
(∀k. k ≥ lo ∧ k < i ⟶ R (h (xs!k)) (h (xs!hi))) ∧ ― ‹All elements from \<^term>‹lo› to \<^term>‹i-1› are smaller than the pivot›
(∀k. k ≥ i ∧ k < j ⟶ R (h (xs!hi)) (h (xs!k))) ∧ ― ‹All elements from \<^term>‹i› to \<^term>‹j-1› are greater than the pivot›
(∀k. k < lo ⟶ xs!k = xs0!k) ∧ ― ‹Everything below \<^term>‹lo› is unchanged›
(∀k. k ≥ j ∧ k < length xs ⟶ xs!k = xs0!k) ― ‹All elements from \<^term>‹j› are unchanged (including everyting above \<^term>‹hi›)›
›
text ‹The main part of the partition function. The pivot is assumed to be the last element. This is
exactly the "Lomuto partition scheme" partition function from Wikipedia.›
definition partition_main :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres› where
‹partition_main R h lo hi xs0 = do {
ASSERT(hi < length xs0);
pivot ← RETURN (h (xs0 ! hi));
(i,j,xs) ← WHILE⇩T⇗partition_main_inv R h lo hi xs0⇖ ― ‹We loop from \<^term>‹j=lo› to \<^term>‹j=hi-1›.›
(λ(i,j,xs). j < hi)
(λ(i,j,xs). do {
ASSERT(i < length xs ∧ j < length xs);
if R (h (xs!j)) pivot
then RETURN (i+1, j+1, swap xs i j)
else RETURN (i, j+1, xs)
})
(lo, lo, xs0); ― ‹i and j are both initialized to lo›
ASSERT(i < length xs ∧ j = hi ∧ lo ≤ i ∧ hi < length xs ∧ mset xs = mset xs0);
RETURN (swap xs i hi, i)
}›
lemma partition_main_correct:
assumes bounds: ‹hi < length xs› ‹lo ≤ hi› and
trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹partition_main R h lo hi xs ≤ SPEC(λ(xs', p). mset xs = mset xs' ∧
lo ≤ p ∧ p ≤ hi ∧ isPartition_map R h xs' lo hi p ∧ (∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i))›
proof -
have K: ‹b ≤ hi - Suc n ⟹ n > 0 ⟹ Suc n ≤ hi ⟹ Suc b ≤ hi - n› for b hi n
by auto
have L: ‹~ R (h x) (h y) ⟹ R (h y) (h x)› for x y
using assms by blast
have M: ‹a < Suc b ≡ a = b ∨ a < b› for a b
by linarith
have N: ‹(a::nat) ≤ b ≡ a = b ∨ a < b› for a b
by arith
show ?thesis
unfolding partition_main_def choose_pivot_def
apply (refine_vcg WHILEIT_rule[where R = ‹measure(λ(i,j,xs). hi-j)›])
subgoal using assms by blast
subgoal by auto
subgoal
unfolding partition_main_inv_def
using assms apply simp by linarith
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by simp
subgoal
unfolding partition_main_inv_def
apply (auto dest: mset_eq_length)
done
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal
unfolding partition_main_inv_def apply (auto dest: mset_eq_length)
by (metis L M mset_eq_length nat_le_eq_or_lt)
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by simp
subgoal
unfolding partition_main_inv_def by (auto simp add: isPartition_wrt_def)
subgoal
unfolding partition_main_inv_def by auto
subgoal
unfolding partition_main_inv_def by auto
done
qed
definition partition_between :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres› where
‹partition_between R h lo hi xs0 = do {
ASSERT(hi < length xs0 ∧ lo ≤ hi);
k ← choose_pivot R h xs0 lo hi; ― ‹choice of pivot›
ASSERT(k < length xs0);
xs ← RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop›
ASSERT(length xs = length xs0);
partition_main R h lo hi xs
}›
lemma partition_between_correct:
assumes ‹hi < length xs› and ‹lo ≤ hi› and
‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹partition_between R h lo hi xs ≤ SPEC(uncurry (partition_spec R h xs lo hi))›
proof -
have K: ‹b ≤ hi - Suc n ⟹ n > 0 ⟹ Suc n ≤ hi ⟹ Suc b ≤ hi - n› for b hi n
by auto
show ?thesis
unfolding partition_between_def choose_pivot_def
apply (refine_vcg partition_main_correct)
using assms apply (auto dest: mset_eq_length simp add: partition_spec_def)
by (metis dual_order.strict_trans2 less_imp_not_eq2 mset_eq_length swap_nth)
qed
text ‹We use the median of the first, the middle, and the last element.›
definition choose_pivot3 where
‹choose_pivot3 R h xs lo (hi::nat) = do {
ASSERT(lo < length xs);
ASSERT(hi < length xs);
let k' = (hi - lo) div 2;
let k = lo + k';
ASSERT(k < length xs);
let start = h (xs ! lo);
let mid = h (xs ! k);
let end = h (xs ! hi);
if (R start mid ∧ R mid end) ∨ (R end mid ∧ R mid start) then RETURN k
else if (R start end ∧ R end mid) ∨ (R mid end ∧ R end start) then RETURN hi
else RETURN lo
}›
lemma choose_pivot3_choose_pivot:
assumes ‹lo < length xs› ‹hi < length xs› ‹hi ≥ lo›
shows ‹choose_pivot3 R h xs lo hi ≤ ⇓ Id (choose_pivot R h xs lo hi)›
unfolding choose_pivot3_def choose_pivot_def
using assms by (auto intro!: ASSERT_leI simp: Let_def)
text ‹The refined partion function: We use the above pivot function and fold instead of non-deterministic iteration.›
definition partition_between_ref
:: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres›
where
‹partition_between_ref R h lo hi xs0 = do {
ASSERT(hi < length xs0 ∧ hi < length xs0 ∧ lo ≤ hi);
k ← choose_pivot3 R h xs0 lo hi; ― ‹choice of pivot›
ASSERT(k < length xs0);
xs ← RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop›
ASSERT(length xs = length xs0);
partition_main R h lo hi xs
}›
lemma partition_main_ref':
‹partition_main R h lo hi xs
≤ ⇓ ((λ a b c d. Id) a b c d) (partition_main R h lo hi xs)›
by auto
lemma partition_between_ref_partition_between:
‹partition_between_ref R h lo hi xs ≤ (partition_between R h lo hi xs)›
proof -
have swap: ‹(swap xs k hi, swap xs ka hi) ∈ Id› if ‹k = ka›
for k ka
using that by auto
have [refine0]: ‹(h (xsa ! hi), h (xsaa ! hi)) ∈ Id›
if ‹(xsa, xsaa) ∈ Id›
for xsa xsaa
using that by auto
show ?thesis
apply (subst (2) Down_id_eq[symmetric])
unfolding partition_between_ref_def
partition_between_def
OP_def
apply (refine_vcg choose_pivot3_choose_pivot swap partition_main_correct)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
by (auto intro: Refine_Basic.Id_refine dest: mset_eq_length)
qed
text ‹Technical lemma for sepref›
lemma partition_between_ref_partition_between':
‹(uncurry2 (partition_between_ref R h), uncurry2 (partition_between R h)) ∈
nat_rel ×⇩f nat_rel ×⇩f ⟨Id⟩list_rel →⇩f ⟨⟨Id⟩list_rel ×⇩r nat_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto intro: partition_between_ref_partition_between)
text ‹Example instantiation for pivot›
definition choose_pivot3_impl where
‹choose_pivot3_impl = choose_pivot3 (≤) id›
lemma partition_between_ref_correct:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and bounds: ‹hi < length xs› ‹lo ≤ hi›
shows ‹partition_between_ref R h lo hi xs ≤ SPEC (uncurry (partition_spec R h xs lo hi))›
proof -
show ?thesis
apply (rule partition_between_ref_partition_between[THEN order_trans])
using bounds apply (rule partition_between_correct[where h=h])
subgoal by (rule trans)
subgoal by (rule lin)
done
qed
term quicksort
text ‹Refined quicksort algorithm: We use the refined partition function.›
definition quicksort_ref :: ‹_ ⇒ _ ⇒ nat × nat × 'a list ⇒ 'a list nres› where
‹quicksort_ref R h = (λ(lo,hi,xs0).
do {
RECT (λf (lo,hi,xs). do {
ASSERT(lo ≤ hi ∧ hi < length xs0 ∧ mset xs = mset xs0);
(xs, p) ← partition_between_ref R h lo hi xs; ― ‹This is the refined partition function. Note that we need the premises (trans,lin,bounds) here.›
ASSERT(mset xs = mset xs0 ∧ p ≥ lo ∧ p < length xs0);
xs ← (if p-1≤lo then RETURN xs else f (lo, p-1, xs));
ASSERT(mset xs = mset xs0);
if hi≤p+1 then RETURN xs else f (p+1, hi, xs)
}) (lo,hi,xs0)
})›
lemma quicksort_ref_quicksort:
assumes bounds: ‹hi < length xs› ‹lo ≤ hi› and
trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹quicksort_ref R h x0 ≤ ⇓ Id (quicksort R h x0)›
proof -
have wf: ‹wf (measure (λ(lo, hi, xs). Suc hi - lo))›
by auto
have pre: ‹x0 = x0' ⟹ (x0, x0') ∈ Id ×⇩r Id ×⇩r ⟨Id⟩list_rel› for x0 x0' :: ‹nat × nat × 'b list›
by auto
have [refine0]: ‹(x1e = x1d) ⟹ (x1e,x1d) ∈ Id› for x1e x1d :: ‹'b list›
by auto
show ?thesis
unfolding quicksort_def quicksort_ref_def
apply (refine_vcg pre partition_between_ref_partition_between'[THEN fref_to_Down_curry2])
text ‹First assertion (premise for partition)›
subgoal
by auto
text ‹First assertion (premise for partition)›
subgoal
by auto
subgoal
by (auto dest: mset_eq_length)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
text ‹Correctness of the concrete partition function›
subgoal
apply (simp, rule partition_between_ref_correct)
subgoal by (rule trans)
subgoal by (rule lin)
subgoal by auto
subgoal by auto
done
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal by (auto simp: partition_spec_def isPartition_wrt_def)
subgoal by (auto simp: partition_spec_def isPartition_wrt_def dest: mset_eq_length)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
by simp+
qed
definition full_quicksort where
‹full_quicksort R h xs ≡ if xs = [] then RETURN xs else quicksort R h (0, length xs - 1, xs)›
definition full_quicksort_ref where
‹full_quicksort_ref R h xs ≡
if List.null xs then RETURN xs
else quicksort_ref R h (0, length xs - 1, xs)›
definition full_quicksort_impl :: ‹nat list ⇒ nat list nres› where
‹full_quicksort_impl xs = full_quicksort_ref (≤) id xs›
lemma full_quicksort_ref_full_quicksort:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹(full_quicksort_ref R h, full_quicksort R h) ∈
⟨Id⟩list_rel →⇩f ⟨ ⟨Id⟩list_rel⟩nres_rel›
proof -
show ?thesis
unfolding full_quicksort_ref_def full_quicksort_def
apply (intro frefI nres_relI)
apply (auto intro!: quicksort_ref_quicksort[unfolded Down_id_eq] simp: List.null_def)
subgoal by (rule trans)
subgoal using lin by blast
done
qed
lemma sublist_entire:
‹sublist xs 0 (length xs - 1) = xs›
by (simp add: sublist_def)
lemma sorted_sublist_wrt_entire:
assumes ‹sorted_sublist_wrt R xs 0 (length xs - 1)›
shows ‹sorted_wrt R xs›
proof -
have ‹sorted_wrt R (sublist xs 0 (length xs - 1))›
using assms by (simp add: sorted_sublist_wrt_def )
then show ?thesis
by (metis sublist_entire)
qed
lemma sorted_sublist_map_entire:
assumes ‹sorted_sublist_map R h xs 0 (length xs - 1)›
shows ‹sorted_wrt (λ x y. R (h x) (h y)) xs›
proof -
show ?thesis
using assms by (rule sorted_sublist_wrt_entire)
qed
text ‹Final correctness lemma›
lemma full_quicksort_correct_sorted:
assumes
trans: ‹⋀x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹full_quicksort R h xs ≤ ⇓ Id (SPEC(λxs'. mset xs' = mset xs ∧ sorted_wrt (λ x y. R (h x) (h y)) xs'))›
proof -
show ?thesis
unfolding full_quicksort_def
apply (refine_vcg)
subgoal by simp
subgoal by simp
apply (rule quicksort_correct[THEN order_trans])
subgoal by (rule trans)
subgoal by (rule lin)
subgoal by linarith
subgoal by simp
apply (simp add: Misc.subset_Collect_conv, intro allI impI conjI)
subgoal
by (auto simp add: quicksort_post_def)
subgoal
apply (rule sorted_sublist_map_entire)
by (auto simp add: quicksort_post_def dest: mset_eq_length)
done
qed
lemma full_quicksort_correct:
assumes
trans: ‹⋀x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and
lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹full_quicksort R h xs ≤ ⇓ Id (SPEC(λxs'. mset xs' = mset xs))›
by (rule order_trans[OF full_quicksort_correct_sorted])
(use assms in auto)
end