Theory Sorting_Heapsort
theory Sorting_Heapsort
imports Sorting_Setup
begin
locale heap_range_context =
fixes l h :: nat
assumes ran_not_empty[arith,simp]: "l≤h"
begin
definition "in_heap i ≡ i∈{l..<h}"
definition parent where "parent i ≡ (i-1-l) div 2 + l"
definition lchild where "lchild i ≡ 2*(i-l) + 1 + l"
definition rchild where "rchild i ≡ 2*(i-l) + 2+ l"
definition has_parent where "has_parent i ≡ in_heap i ∧ i>l"
definition has_lchild where "has_lchild i ≡ in_heap i ∧ in_heap (lchild i)"
definition has_rchild where "has_rchild i ≡ in_heap i ∧ in_heap (rchild i)"
context begin
private method prove = (
unfold in_heap_def parent_def has_parent_def lchild_def rchild_def has_lchild_def has_rchild_def,
auto)
text ‹Optimized checks, normalize to i-l, for index shift›
lemma has_rchild_ihs: "in_heap i ⟹ has_rchild i ⟷ i-l<(h-l-1) div 2"
by prove
lemma has_lchild_ihs: "in_heap i ⟹ has_lchild i ⟷ (i-l) < (h-l) div 2"
by prove
lemma has_parent_ihs: "in_heap i ⟹ has_parent i ⟷ i-l > 0"
by prove
lemma lchild_ihs: "lchild i - l = 2*(i-l)+1"
by prove
lemma rchild_ihs: "rchild i - l = 2*(i-l)+2"
by prove
lemma parent_ihs: "parent i - l = (i-l-1) div 2"
by prove
lemma in_heapI: "⟦ l≤i; i<h ⟧ ⟹ in_heap i" by prove
lemma in_heap_bounds[simp]:
assumes "in_heap i"
shows "l≤i" and "i<h"
using assms by prove
lemma in_heap_triv[simp]:
"has_parent i ⟹ in_heap i"
"has_lchild i ⟹ in_heap i"
"has_rchild i ⟹ in_heap i"
by prove
lemma parent_in_heap[simp]:
"has_parent i ⟹ in_heap (parent i)"
"has_parent i ⟹ has_lchild (parent i)"
by prove
lemma children_in_heap[simp]:
"has_lchild i ⟹ in_heap (lchild i)"
"has_rchild i ⟹ in_heap (rchild i)"
by prove
lemmas in_heap_simps = in_heap_triv parent_in_heap children_in_heap
lemma parent_of_child[simp]:
"has_lchild i ⟹ parent (lchild i) = i"
"has_rchild i ⟹ parent (rchild i) = i"
by prove
lemma children_differ[simp]:
"lchild i ≠ rchild i"
"rchild i ≠ lchild i"
by prove
lemma parent_less[simp]: "has_parent i ⟹ parent i < i" by prove
lemma children_greater[simp]:
"lchild i > i"
"rchild i > i"
by prove
lemma children_diff_add_simps[iff]:
"lchild i ≠ i"
"i ≠ lchild i"
"rchild i ≠ i"
"i ≠ rchild i"
by prove
lemma parent_diff_add_simps[simp]:
assumes "has_parent i" shows "i ≠ parent i" and "parent i ≠ i"
using assms by prove
lemma rchild_imp_lchild[simp, intro]: "has_rchild i ⟹ has_lchild i" by prove
lemma no_parent_is_root: "in_heap i ⟹ ¬has_parent i ⟷ i=l" by prove
lemma root_no_parent[iff]: "¬has_parent l" by prove
lemma root_in_heap: "in_heap l⟷l<h" using ran_not_empty by prove
lemma child_of_parent: "has_parent i ⟹ lchild (parent i) = i ∨ has_rchild (parent i) ∧ rchild (parent i) = i" by prove
lemma children_of_parent_cases[consumes 1]:
assumes "has_parent i"
obtains (left) "has_parent i" "lchild (parent i) = i"
| (right) "has_parent i" "has_rchild (parent i)" "rchild (parent i) = i"
using assms child_of_parent by blast
lemma lchild_of_no_rchild_term: "⟦¬has_rchild i; has_lchild i⟧ ⟹ ¬has_lchild (lchild i)" by prove
end
lemmas heap_context_defs[no_atp] = in_heap_def parent_def lchild_def rchild_def has_parent_def has_lchild_def has_rchild_def
end
locale heap_context = weak_ordering + heap_range_context begin
definition is_heap :: "'a list ⇒ bool"
where "is_heap xs ≡ (h≤length xs) ∧ (∀i. has_parent i ⟶ xs!parent i ❙≥ xs!i)"
subsection ‹Heap Property implies Minimal Element at Top›
context
fixes xs
assumes H: "is_heap xs"
begin
lemma parent_el_greater[simp]: "has_parent i ⟹ xs!i ❙≤ xs!parent i"
using H
unfolding is_heap_def
by simp
lemma root_greatest:
assumes "in_heap i"
shows "xs!i ❙≤ xs!l"
using assms
proof (induction i rule: less_induct)
case (less i)
note [simp] = ‹in_heap i›
show ?case proof cases
assume [simp]: "has_parent i"
have "xs!i ❙≤ xs!parent i" by simp
also from less.IH[of "parent i"] have "xs!parent i ❙≤ xs!l" by simp
finally show ?case .
next
assume "¬has_parent i"
hence "i=l" by (simp add: no_parent_is_root)
thus ?case by simp
qed
qed
end
subsection ‹Sift-Up Lemmas›
definition is_heap_except_up :: "nat ⇒ 'a list ⇒ bool"
where "is_heap_except_up j xs ≡
(h≤length xs)
∧ (∀i. has_parent i ∧ i≠j ⟶ xs!parent i ❙≥ xs!i)
∧ (has_parent j ∧ has_lchild j ⟶ xs!parent j ❙≥ xs!lchild j)
∧ (has_parent j ∧ has_rchild j ⟶ xs!parent j ❙≥ xs!rchild j)"
lemma is_heap_except_up_len_bound[simp, intro]:
assumes "is_heap_except_up i xs"
shows "h≤length xs"
using assms unfolding is_heap_except_up_def
by auto
lemma sift_up_lemma:
assumes HP: "has_parent i"
assumes IHE: "is_heap_except_up i xs"
assumes GE: "xs!i ❙≥ xs!parent i"
shows "is_heap_except_up (parent i) (swap xs i (parent i))"
proof -
from assms(2) have [simp, arith]: "h≤length xs" unfolding is_heap_except_up_def by auto
have X[simp]: "i<length xs" if "in_heap i" for i
using in_heap_bounds(2)[OF that] by simp
have HPROP: "xs!j ❙≤ xs!parent j" if "has_parent j" "j≠i" for j
using that IHE unfolding is_heap_except_up_def by simp
show ?thesis using HP
unfolding is_heap_except_up_def
apply (clarsimp; safe)
subgoal
apply (clarsimp simp: swap_nth HPROP GE; safe)
subgoal by (metis GE HPROP trans)
by (metis IHE child_of_parent is_heap_except_up_def parent_in_heap(2))
subgoal
by (smt HPROP X children_greater(1) has_lchild_def in_heap_bounds(1) parent_of_child(1) trans nat_less_le no_parent_is_root parent_in_heap(2) parent_less less_le_trans swap_indep swap_nth)
subgoal
by (smt HPROP X children_greater(2) has_parent_def has_rchild_def parent_less parent_of_child(2) less_le trans less_trans swap_nth)
done
qed
text ‹Terminate when reached root›
lemma sift_up_term1: "is_heap_except_up l xs ⟹ is_heap xs"
unfolding is_heap_def is_heap_except_up_def by auto
text ‹Terminate when parent is greater or equal›
lemma sift_up_term2: "⟦is_heap_except_up i xs; xs!i❙≤xs!parent i⟧ ⟹ is_heap xs"
unfolding is_heap_def is_heap_except_up_def by auto
lemma grow_heap_context: "heap_range_context l (Suc h)"
apply unfold_locales using ran_not_empty by linarith
text ‹Initializes a sift-up cycle by extending the heap by one element to the right›
lemma sift_up_init:
assumes "is_heap xs"
assumes "h<length xs"
shows "heap_context.is_heap_except_up (❙≤) l (Suc h) h xs"
proof -
interpret N: heap_range_context l "Suc h" using grow_heap_context .
interpret N: heap_context "(❙≤)" "(❙<)" l "Suc h" by unfold_locales
show ?thesis
using assms
unfolding is_heap_def is_heap_except_up_def N.is_heap_except_up_def
unfolding N.heap_context_defs heap_context_defs
by auto
qed
subsection ‹Sift-Down Lemmas›
definition is_heap_except_down :: "nat ⇒ 'a list ⇒ bool"
where "is_heap_except_down j xs ≡
(h≤length xs)
∧ (∀i. has_parent i ∧ parent i ≠ j ⟶ xs!parent i ❙≥ xs!i)
∧ (∀i. has_parent i ∧ has_parent j ∧ parent i = j ⟶ xs!parent j ❙≥ xs!i)"
lemma is_heap_except_down_len_bound[simp, intro]:
assumes "is_heap_except_down i xs"
shows "h≤length xs"
using assms unfolding is_heap_except_down_def
by auto
lemma sift_down_lemma_left:
assumes HRC: "has_rchild i"
assumes IHE: "is_heap_except_down i xs"
assumes GE: "xs!lchild i ❙≥ xs!i" "xs!lchild i ❙≥ xs!rchild i"
shows "is_heap_except_down (lchild i) (swap xs i (lchild i))"
proof -
show ?thesis
using IHE HRC GE
unfolding is_heap_except_down_def
apply (clarsimp)
by (smt child_of_parent children_greater(1) children_in_heap(1) dual_order.trans has_parent_def parent_diff_add_simps(1) in_heap_bounds(2) leD order_less_le parent_of_child(1) rchild_imp_lchild swap_indep swap_nth1 swap_nth2)
qed
lemma sift_down_lemma_right:
assumes HRC: "has_rchild i"
assumes IHE: "is_heap_except_down i xs"
assumes GE: "xs!rchild i ❙≥ xs!i" "xs!lchild i ❙≤ xs!rchild i"
shows "is_heap_except_down (rchild i) (swap xs i (rchild i))"
proof -
show ?thesis
using IHE HRC GE
unfolding is_heap_except_down_def
apply (clarsimp)
by (smt child_of_parent children_greater(2) children_in_heap(2) dual_order.trans eq_iff heap_range_context.has_parent_def heap_range_context_axioms in_heap_bounds(2) less_le parent_less parent_of_child(2) swap_nth)
qed
lemma sift_down_lemma_left_no_right_child:
assumes HRC: "has_lchild i" "¬has_rchild i"
assumes IHE: "is_heap_except_down i xs"
assumes GE: "xs!lchild i ❙≥ xs!i"
shows "is_heap_except_down (lchild i) (swap xs i (lchild i))"
proof -
from IHE have [simp, arith]: "h≤length xs" unfolding is_heap_except_down_def by auto
have X[simp]: "i<length xs" if "in_heap i" for i
using in_heap_bounds(2)[OF that] by simp
show ?thesis
using IHE HRC GE
unfolding is_heap_except_down_def
apply clarsimp
by (smt X child_of_parent children_greater(1) children_in_heap(1) heap_range_context.has_parent_def heap_range_context.parent_of_child(1) heap_range_context_axioms le_less_trans less_imp_le_nat parent_in_heap(1) swap_nth)
qed
lemma sift_down_term1: "¬has_lchild j ⟹ is_heap_except_down j xs ⟷ is_heap xs"
unfolding is_heap_except_down_def is_heap_def
by auto
lemma sift_down_term2: "⟦is_heap_except_down j xs; has_rchild j; xs!j❙≥xs!lchild j; xs!j❙≥xs!rchild j ⟧ ⟹ is_heap xs"
unfolding is_heap_except_down_def is_heap_def
apply (clarsimp)
by (metis children_of_parent_cases)
lemma sift_down_term3: "⟦is_heap_except_down j xs; has_lchild j; ¬has_rchild j; xs!j❙≥xs!lchild j ⟧ ⟹ is_heap xs"
unfolding is_heap_except_down_def is_heap_def
apply (clarsimp)
by (metis children_of_parent_cases)
lemma shrink_heap_context: "Suc l<h ⟹ heap_range_context l (h-Suc 0)"
apply unfold_locales using ran_not_empty by linarith
text ‹Initializes a sift-down cycle by swapping the first and last element, and then shrinking the heap by one element›
lemma sift_down_init:
assumes "is_heap xs"
assumes LT: "Suc l < h"
shows "heap_context.is_heap_except_down (❙≤) l (h-Suc 0) l (swap xs l (h-Suc 0))"
proof -
interpret N: heap_context "(❙≤)" "(❙<)" l "h-Suc 0"
apply intro_locales
using shrink_heap_context[OF LT] .
show ?thesis
using assms
unfolding is_heap_def is_heap_except_down_def N.is_heap_except_down_def
unfolding N.heap_context_defs heap_context_defs
by (auto simp: swap_nth)
qed
subsection ‹Bottom-up Heapify›
text ‹The nodes from index ‹l'› upwards satisfy the heap criterion›
definition is_heap_btu :: "nat ⇒ 'a list ⇒ bool" where "is_heap_btu l' xs ≡
(l'≤h ∧ h≤length xs)
∧ (∀i. has_parent i ∧ parent i ≥ l' ⟶ xs!parent i ❙≥ xs!i)"
text ‹Bottom-up heapify starts with only the last element being a heap›
lemma btu_heapify_init: "h≤length xs ⟹ is_heap_btu (h-Suc 0) xs"
unfolding is_heap_btu_def
apply auto
by (meson dual_order.trans in_heap_bounds(2) in_heap_triv(1) nat_le_Suc_less_imp not_le parent_less)
text ‹When we have reached the lower index, we have a complete heap›
lemma btu_heapify_term: "is_heap_btu l xs ⟷ is_heap xs"
unfolding is_heap_btu_def is_heap_def
by (auto simp: less_imp_le_nat)
text ‹All nodes in between l' and h form a valid heap, with downwards-hole at j›
definition is_heap_except_down_btu :: "nat ⇒ nat ⇒ 'a list ⇒ bool"
where "is_heap_except_down_btu l' j xs ≡
(l'≤j ∧ j<h ∧ h≤length xs)
∧ (∀i. has_parent i ∧ parent i ≥ l' ∧ parent i ≠ j ⟶ xs!parent i ❙≥ xs!i)
∧ (∀i. has_parent i ∧ has_parent j ∧ parent j ≥l' ∧ parent i = j ⟶ xs!parent j ❙≥ xs!i)"
lemma is_heap_except_down_btu_lenD: "is_heap_except_down_btu l' j xs ⟹ h≤length xs"
unfolding is_heap_except_down_btu_def by auto
text ‹A sift-down round starts by including one more left element, and marking it as a hole›
lemma btu_sift_down_init: "⟦is_heap_btu l' xs; l'>l⟧ ⟹ is_heap_except_down_btu (l'-1) (l'-1) xs"
unfolding is_heap_except_down_btu_def is_heap_btu_def
apply auto
using leD parent_less by blast
text ‹Sift-down completed, we have a complete heap from ‹l'› upwards›
lemma btu_sift_down_term1: "¬has_lchild j ⟹ is_heap_except_down_btu l' j xs ⟹ is_heap_btu l' xs"
unfolding is_heap_except_down_btu_def is_heap_btu_def
by auto
lemma btu_sift_down_term2: "⟦is_heap_except_down_btu l' j xs; has_rchild j; xs!j❙≥xs!lchild j; xs!j❙≥xs!rchild j ⟧
⟹ is_heap_btu l' xs"
unfolding is_heap_except_down_btu_def is_heap_btu_def
apply (clarsimp)
by (smt dual_order.trans child_of_parent in_heap_bounds(2) in_heap_triv(3) le_cases not_le)
lemma btu_sift_down_term3: "⟦is_heap_except_down_btu l' j xs; has_lchild j; ¬has_rchild j; xs!j❙≥xs!lchild j ⟧ ⟹ is_heap_btu l' xs"
unfolding is_heap_except_down_btu_def is_heap_btu_def
apply (clarsimp)
by (metis child_of_parent dual_order.trans in_heap_bounds(2) in_heap_triv(2) less_imp_le)
lemma btu_heapify_down_left:
assumes HRC: "has_rchild i"
assumes IHE: "is_heap_except_down_btu l' i xs"
assumes GE: "xs!lchild i ❙≥ xs!i" "xs!lchild i ❙≥ xs!rchild i"
shows "is_heap_except_down_btu l' (lchild i) (swap xs i (lchild i))"
proof -
from IHE have [simp, arith]: "h≤length xs" unfolding is_heap_except_down_btu_def by auto
have X[simp]: "i<length xs" if "in_heap i" for i
using in_heap_bounds(2)[OF that] by simp
show ?thesis
using HRC IHE GE
unfolding is_heap_except_down_btu_def
apply (clarsimp simp: swap_nth)
by (smt child_of_parent children_greater(1) children_in_heap(1) heap_range_context.has_parent_def heap_range_context_axioms leD le_cases less_le_trans parent_of_child(1) rchild_imp_lchild)
qed
lemma btu_heapify_down_right:
assumes HRC: "has_rchild i"
assumes IHE: "is_heap_except_down_btu l' i xs"
assumes GE: "xs!rchild i ❙≥ xs!i" "xs!lchild i ❙≤ xs!rchild i"
shows "is_heap_except_down_btu l' (rchild i) (swap xs i (rchild i))"
proof -
from IHE have [simp, arith]: "h≤length xs" unfolding is_heap_except_down_btu_def by auto
have X[simp]: "i<length xs" if "in_heap i" for i
using in_heap_bounds(2)[OF that] by simp
show ?thesis
using HRC IHE GE
unfolding is_heap_except_down_btu_def
apply (clarsimp simp: swap_nth)
by (smt child_of_parent children_greater(2) children_in_heap(2) dual_order.strict_trans2 heap_range_context.has_parent_def heap_range_context_axioms less_imp_le_nat parent_of_child(2))
qed
lemma btu_heapify_down_left_no_right_child:
assumes HRC: "has_lchild i" "¬has_rchild i"
assumes IHE: "is_heap_except_down_btu l' i xs"
assumes GE: "xs!lchild i ❙≥ xs!i"
shows "is_heap_except_down_btu l' (lchild i) (swap xs i (lchild i))"
proof -
from IHE have [simp, arith]: "h≤length xs" unfolding is_heap_except_down_btu_def by auto
have X[simp]: "i<length xs" if "in_heap i" for i
using in_heap_bounds(2)[OF that] by simp
show ?thesis
using HRC IHE GE
unfolding is_heap_except_down_btu_def
apply (clarsimp simp: swap_nth)
by (smt child_of_parent children_greater(1) children_in_heap(1) heap_range_context.has_parent_def heap_range_context_axioms leD le_cases less_le_trans parent_of_child(1))
qed
definition "sift_up_invar xs⇩0 i xs ≡
slice_eq_mset l h xs xs⇩0
∧ is_heap_except_up i xs"
lemma sift_up_invar_init:
assumes "is_heap xs" "slice_eq_mset l h xs xs⇩0" "h<length xs"
shows "heap_context.sift_up_invar (❙≤) l (Suc h) xs⇩0 h xs"
proof -
interpret N: heap_context "(❙≤)" "(❙<)" l "Suc h" by intro_locales (simp add: grow_heap_context)
show ?thesis
using assms
by (meson N.sift_up_invar_def le_eq_less_or_eq nat_in_between_eq(1) ran_not_empty sift_up_init slice_eq_mset_subslice)
qed
lemma sift_up_invar_step: "⟦sift_up_invar xs⇩0 i xs; has_parent i; xs!i❙≥xs!parent i ⟧
⟹ sift_up_invar xs⇩0 (parent i) (swap xs i (parent i))"
unfolding sift_up_invar_def
by (auto simp: sift_up_lemma)
lemma sift_up_invar_term1: "⟦sift_up_invar xs⇩0 l xs⟧ ⟹ is_heap xs ∧ slice_eq_mset l h xs xs⇩0"
unfolding sift_up_invar_def
using sift_up_term1 by blast
lemma sift_up_invar_term2: "⟦sift_up_invar xs⇩0 i xs; xs!i❙≤xs!parent i⟧
⟹ is_heap xs ∧ slice_eq_mset l h xs xs⇩0"
unfolding sift_up_invar_def
using sift_up_term2 by blast
definition "sift_down_invar xs⇩0 i xs ≡
slice_eq_mset l h xs xs⇩0
∧ is_heap_except_down i xs"
lemma sift_down_invar_step:
assumes "sift_down_invar xs⇩0 i xs"
shows "⟦has_rchild i; xs!i❙≤xs!lchild i; xs!lchild i ❙≥ xs!rchild i⟧ ⟹ sift_down_invar xs⇩0 (lchild i) (swap xs i (lchild i))"
and "⟦has_rchild i; xs!i❙≤xs!rchild i; xs!lchild i ❙≤ xs!rchild i⟧ ⟹ sift_down_invar xs⇩0 (rchild i) (swap xs i (rchild i))"
and "⟦has_lchild i; ¬has_rchild i; xs!i❙≤xs!lchild i⟧ ⟹ sift_down_invar xs⇩0 (lchild i) (swap xs i (lchild i))"
using assms unfolding sift_down_invar_def
by (auto simp: sift_down_lemma_left sift_down_lemma_right sift_down_lemma_left_no_right_child)
thm sift_down_init
lemma sift_down_invar_init:
assumes "is_heap xs" "Suc l < h"
shows "heap_context.sift_down_invar (❙≤) l (h-Suc 0) (swap xs l (h-Suc 0)) l (swap xs l (h-Suc 0))"
proof -
interpret N: heap_context "(❙≤)" "(❙<)" l "h-Suc 0" apply intro_locales using assms shrink_heap_context by auto
show ?thesis using sift_down_init assms unfolding N.sift_down_invar_def
by (auto simp: sift_down_init)
qed
definition "heapify_btu_invar xs⇩0 l' xs ≡
slice_eq_mset l h xs xs⇩0
∧ is_heap_btu l' xs"
definition "sift_down_btu_invar xs⇩0 l' i xs ≡
slice_eq_mset l h xs xs⇩0
∧ is_heap_except_down_btu l' i xs"
end
context weak_ordering begin
sublocale singleton_heap_context: heap_context "(❙≤)" "(❙<)" l "(Suc l)"
by unfold_locales auto
lemma singleton_no_relatives[simp, intro!]:
"¬singleton_heap_context.has_parent l i"
"¬singleton_heap_context.has_lchild l i"
"¬singleton_heap_context.has_rchild l i"
unfolding singleton_heap_context.heap_context_defs
by auto
lemma singleton_heap: "l<length xs ⟹ singleton_heap_context.is_heap l xs"
unfolding singleton_heap_context.is_heap_def
by auto
end
context heap_context begin
definition sift_down :: "nat ⇒ 'a list ⇒ 'a list nres" where "sift_down i⇩0 xs ≡ doN {
ASSERT (in_heap i⇩0 ∧ i⇩0<length xs);
(xs,i,_) ← WHILEIT (λ(xs,i,ctd). in_heap i ∧ i≥i⇩0)
(λ(xs,i,ctd). has_rchild i ∧ ctd)
(λ(xs,i,ctd). doN {
lc ← mop_list_get xs (lchild i);
rc ← mop_list_get xs (rchild i);
v ← mop_list_get xs i;
if lc ❙< rc then
if v ❙< rc then doN {
xs ← mop_list_swap xs i (rchild i);
RETURN (xs,rchild i,True)
} else RETURN (xs,i,False)
else if v ❙< lc then doN {
xs ← mop_list_swap xs i (lchild i);
RETURN (xs,lchild i,True)
} else RETURN (xs,i,False)
})
(xs,i⇩0,True);
ASSERT (in_heap i ∧ i≥i⇩0);
ASSERT (has_lchild i ⟶ lchild i < length xs);
if has_lchild i ∧ xs!i ❙< xs!lchild i then
mop_list_swap xs i (lchild i)
else
RETURN xs
}"
lemma in_heap_len_bound: "in_heap i ⟹ h≤length xs ⟹ i<length xs"
using in_heap_bounds(2) less_le_trans by blast
lemma sift_down_btu_correct:
assumes "heapify_btu_invar xs⇩0 l' xs" "l<l'"
shows "sift_down (l'-Suc 0) xs ≤ SPEC (λxs'. heapify_btu_invar xs⇩0 (l'-Suc 0) xs')"
unfolding sift_down_def
apply (refine_vcg WHILEIT_rule_amend_invar[where
I="λ(xs,i,ctd).
sift_down_btu_invar xs⇩0 (l'-Suc 0) i xs
∧ h≤length xs
∧ (¬ctd ⟶ has_rchild i ∧ xs!i❙≥xs!lchild i ∧ xs!i❙≥xs!rchild i)"
and
R = "measure (λ(xs,i,ctd). (if ctd then 1 else 0) + h - i)"
])
using assms
unfolding heapify_btu_invar_def sift_down_btu_invar_def
apply (simp_all del: in_heap_simps)
apply (all ‹(auto simp: in_heap_len_bound diff_less_mono2 wo_leI; fail)?›)
subgoal unfolding is_heap_btu_def by (auto intro!: in_heapI)
subgoal unfolding is_heap_btu_def by auto
subgoal using btu_sift_down_init by auto
subgoal unfolding is_heap_btu_def by auto
subgoal by (force simp: asym wo_leI simp: btu_heapify_down_right)
subgoal using children_greater(2) le_trans less_imp_le_nat by blast
subgoal by (simp add: diff_less_mono2 less_Suc_eq)
subgoal by simp (metis wo_leI wo_less_trans)
subgoal by (simp add: diff_less_mono less_imp_le)
subgoal by (force simp add: btu_heapify_down_left asym wo_leI)
subgoal using children_greater(1) dual_order.strict_trans2 less_imp_le by blast
subgoal by (simp add: diff_less_mono2 less_Suc_eq)
subgoal apply simp using local.trans wo_leI by blast
subgoal by (simp add: diff_less_mono less_imp_le)
subgoal
apply clarsimp
using btu_heapify_down_left_no_right_child btu_sift_down_term1 connex lchild_of_no_rchild_term wo_leD by blast
subgoal
apply clarsimp
using btu_sift_down_term1 btu_sift_down_term2 btu_sift_down_term3 wo_leI by blast
done
lemma sift_down_restore_correct:
assumes A: "l<h" "sift_down_invar xs⇩0 l xs"
shows "sift_down l xs ≤ SPEC (λxs'. slice_eq_mset l h xs' xs⇩0 ∧ is_heap xs')"
unfolding sift_down_def
apply (refine_vcg WHILEIT_rule_amend_invar[where
I="λ(xs,i,ctd).
sift_down_invar xs⇩0 i xs
∧ h≤length xs
∧ (¬ctd ⟶ has_rchild i ∧ xs!i❙≥xs!lchild i ∧ xs!i❙≥xs!rchild i)"
and
R = "measure (λ(xs,i,ctd). (if ctd then 1 else 0) + h - i)"
])
apply clarsimp_all
apply (all ‹(auto simp: in_heap_len_bound diff_less_mono2 A sift_down_invar_step wo_leI root_in_heap; fail)?›)
subgoal using A unfolding sift_down_invar_def is_heap_except_down_def by auto
subgoal using A unfolding sift_down_invar_def is_heap_except_down_def by auto
subgoal using asym sift_down_invar_step(2) wo_leI by blast
subgoal by (simp add: diff_less_mono2 less_SucI)
subgoal using wo_less_trans wo_not_le_imp_less by blast
subgoal by (simp add: Suc_diff_le less_imp_le)
subgoal using asym sift_down_invar_step(1) wo_leI by blast
subgoal by (simp add: diff_less_mono2 less_Suc_eq)
subgoal using itrans wo_leI by blast
subgoal by (simp add: Suc_diff_le less_imp_le)
subgoal unfolding sift_down_invar_def by simp
subgoal by (meson lchild_of_no_rchild_term sift_down_invar_def sift_down_invar_step(3) sift_down_term1 wo_leD wo_leI wo_less_not_sym)
subgoal by (meson lchild_of_no_rchild_term less_imp_le not_le sift_down_invar_def sift_down_lemma_left_no_right_child sift_down_term1)
subgoal unfolding sift_down_invar_def by (meson wo_leI sift_down_term1 sift_down_term2 sift_down_term3)
done
text ‹Deferred swap optimization›
definition sift_down1 :: "nat ⇒ 'a list ⇒ 'a list nres" where "sift_down1 i⇩0 xs ≡ doN {
ASSERT (in_heap i⇩0);
v ← mop_list_get xs i⇩0;
(xs,i,_) ← WHILEIT (λ(xs,i,ctd). in_heap i ∧ i≥i⇩0) (λ(xs,i,ctd). has_rchild i ∧ ctd) (λ(xs,i,ctd). doN {
lc ← mop_list_get xs (lchild i);
rc ← mop_list_get xs (rchild i);
if lc ❙< rc then
if v ❙< rc then doN {
t ← mop_list_get xs (rchild i);
xs ← mop_list_set xs i t;
RETURN (xs,rchild i,True)
} else RETURN (xs,i,False)
else if v ❙< lc then doN {
t ← mop_list_get xs (lchild i);
xs ← mop_list_set xs i t;
RETURN (xs,lchild i,True)
} else RETURN (xs,i,False)
}) (xs,i⇩0,True);
ASSERT (in_heap i ∧ i≥i⇩0);
ASSERT (has_lchild i ⟶ lchild i < length xs);
xs ← (if has_lchild i ∧ v ❙< xs!lchild i then doN {
t ← mop_list_get xs (lchild i);
xs ← mop_list_set xs i t;
xs ← mop_list_set xs (lchild i) v;
RETURN xs
} else doN {
xs ← mop_list_set xs i v;
RETURN xs
});
RETURN xs
}"
definition "swap_opt_rel v ≡ {((xs,i,ctd),(xs',i',ctd')). xs' = xs[i:=v] ∧ i<length xs ∧ i'=i ∧ ctd'=ctd }"
lemma sift_down1_refine: "sift_down1 i⇩0 xs ≤⇓Id (sift_down i⇩0 xs)"
unfolding sift_down1_def sift_down_def
apply (intro refine0)
subgoal by simp
apply (rule specify_left_pw, simp)
subgoal for v
apply (rule refine)
apply (rule WHILEIT_refine[where R="swap_opt_rel v"])
subgoal by (auto simp: swap_opt_rel_def)
subgoal by (auto simp: swap_opt_rel_def)
subgoal by (auto simp: swap_opt_rel_def)
subgoal for s s'
apply (clarsimp simp: swap_opt_rel_def split del: if_split)
apply (intro refine0 if_refine)
apply (all ‹(auto; auto simp: swap_def;fail)?›)
done
subgoal for s s'
supply [simp del] = conc_Id
apply (clarsimp simp: swap_opt_rel_def split del: if_split)
apply (intro refine0 if_refine)
apply (all ‹(auto; auto simp: swap_def;fail)?›)
done
done
done
text ‹Index shift optimization›
definition "ihs_opt_rel ≡ {((xs,i,ctd),(xs',i',ctd')). xs' = xs ∧ i' = i+l ∧ ctd'=ctd }"
lemma ihs_opt_rel_alt: "((xs,i,ctd), (xs',i',ctd'))∈ihs_opt_rel ⟷ xs'=xs ∧ (i',i)∈idx_shift_rel l ∧ ctd'=ctd"
unfolding ihs_opt_rel_def idx_shift_rel_def by auto
definition [simp]: "mop_lchild2 i ≡ doN { ASSERT (2*i+1<h); RETURN (2*i+1) }"
definition [simp]: "mop_rchild2 i ≡ doN { ASSERT (2*i+2<h); RETURN (2*i+2) }"
definition [simp]: "has_rchild2 i ≡ i<(h-l-1) div 2"
definition [simp]: "has_lchild2 i ≡ i<(h-l) div 2"
end
concrete_definition mop_lchild3 is heap_context.mop_lchild2_def
concrete_definition mop_rchild3 is heap_context.mop_rchild2_def
concrete_definition has_rchild3 is heap_context.has_rchild2_def
concrete_definition has_lchild3 is heap_context.has_lchild2_def
lemmas h_aux_refines = mop_lchild3.refine mop_rchild3.refine has_rchild3.refine
has_lchild3.refine
context heap_context begin
definition sift_down2 :: "nat ⇒ 'a list ⇒ 'a list nres" where "sift_down2 i⇩0 xs ≡ doN {
ASSERT (l≤i⇩0 ∧ i⇩0<h);
let i⇩1 = i⇩0 - l;
v ← mop_list_get xs (i⇩1+l);
(xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i⇩1) (λ(xs,i,ctd). has_rchild3 l h i ∧ ctd) (λ(xs,i,ctd). doN {
lci ← mop_lchild3 h i;
rci ← mop_rchild3 h i;
ASSERT (lci+l<h ∧ rci+l<h);
ASSERT (lci≠i ∧ rci≠i ∧ lci≠rci);
lc ← mop_list_get xs (lci+l);
rc ← mop_list_get xs (rci+l);
ASSERT (i+l<h);
if lc ❙< rc then
if v ❙< rc then doN {
xs ← mop_list_set xs (i+l) rc;
RETURN (xs,rci,True)
} else RETURN (xs,i,False)
else if v ❙< lc then doN {
xs ← mop_list_set xs (i+l) lc;
RETURN (xs,lci,True)
} else RETURN (xs,i,False)
}) (xs,i⇩1,True);
ASSERT (i≥i⇩1 ∧ i+l<h);
if has_lchild3 l h i then doN {
lci ← mop_lchild3 h i;
ASSERT (lci+l<h);
ASSERT (lci≠i);
lc ← mop_list_get xs (lci+l);
if v ❙< lc then doN {
xs ← mop_list_set xs (i+l) lc;
xs ← mop_list_set xs (lci+l) v;
RETURN xs
} else doN {
xs ← mop_list_set xs (i+l) v;
RETURN xs
}
} else doN {
xs ← mop_list_set xs (i+l) v;
RETURN xs
}
}"
lemma idx_shift_adjust:
assumes "(i',i)∈idx_shift_rel l"
shows
"in_heap i' ⟷ i<h-l"
"has_lchild i' ⟷ i<(h-l) div 2"
"has_rchild i' ⟷ i<(h-l-1) div 2"
"lchild i' = 2*i+1+l"
"rchild i' = 2*i+2+l"
"i+l = i'"
"i'<x ⟷ i<x-l"
"i'≤h ⟷ i≤h-l"
"x≤i' ⟷ x-l≤i"
using assms
thm lchild_ihs
unfolding idx_shift_rel_def
in_heap_def
has_rchild_def rchild_def
has_lchild_def lchild_def
by auto
lemma sift_down2_refine: "sift_down2 i xs ≤ ⇓Id (sift_down1 i xs)"
unfolding sift_down1_def sift_down2_def
unfolding h_aux_refines[OF heap_context_axioms, symmetric]
supply [simp del] = conc_Id
apply (simp cong: if_cong)
apply (rewrite at "let i=i-l in _" Let_def)
apply (intro refine0)
apply (all ‹unfold in_heap_def; simp_all; fail ›) [2]
apply (rule bind_refine)
focus
apply refine_rcg
supply [refine_dref_RELATES] = RELATESI[of ihs_opt_rel]
apply refine_dref_type
apply (simp_all add: ihs_opt_rel_alt)
apply (all ‹(determ ‹elim conjE›)?; simp?›)
apply (clarsimp_all simp: idx_shift_adjust ihs_opt_rel_alt simp del: in_heap_simps)
unfolding in_heap_def idx_shift_rel_def ihs_opt_rel_alt
apply (auto simp: algebra_simps)
solved
subgoal for s s'
supply [split del] = if_split
apply (cases s; simp)
apply (cases s'; simp)
apply (intro refine0)
subgoal by (clarsimp simp: idx_shift_adjust ihs_opt_rel_alt)
apply (split if_split; intro conjI impI)
subgoal
apply refine_rcg
apply (simp_all add: ihs_opt_rel_alt)
apply (all ‹determ ‹elim conjE›; simp?›)
apply (auto simp: algebra_simps idx_shift_adjust)
done
subgoal
apply (split if_split, intro impI conjI refine0)
apply (simp_all add: ihs_opt_rel_alt)
apply (all ‹determ ‹elim conjE›; simp?›)
apply (auto simp: ihs_opt_rel_alt idx_shift_adjust algebra_simps)
done
done
done
definition [simp]: "mop_geth2 xs i ≡ doN { ASSERT(l+i≤h); mop_eo_extract xs (l+i) }"
definition [simp]: "mop_seth2 xs i x ≡ doN { ASSERT(l+i≤h); mop_eo_set xs (l+i) x }"
end
concrete_definition mop_geth3 is heap_context.mop_geth2_def
concrete_definition mop_seth3 is heap_context.mop_seth2_def
lemmas h_aux_refines2 = mop_geth3.refine mop_seth3.refine
context heap_context begin
definition sift_down3 :: "nat ⇒ 'a list ⇒ 'a list nres" where "sift_down3 i⇩0 xs ≡ doN {
ASSERT (l≤i⇩0 ∧ i⇩0<h);
let i⇩1 = i⇩0 - l;
xs ← mop_to_eo_conv xs;
(v,xs) ← mop_geth3 l h xs i⇩1;
(xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i⇩1) (λ(xs,i,ctd). has_rchild3 l h i ∧ ctd) (λ(xs,i,ctd). doN {
lci ← mop_lchild3 h i;
rci ← mop_rchild3 h i;
ASSERT (l+lci<h ∧ l+rci<h ∧ l+lci ≠ l+rci);
b ← mop_cmpo_idxs xs (l+lci) (l+rci);
if b then doN {
b ← mop_cmpo_v_idx xs v (l+rci);
if b then doN {
(rc,xs) ← mop_geth3 l h xs rci;
xs ← mop_seth3 l h xs i rc;
RETURN (xs,rci,True)
} else RETURN (xs,i,False)
} else doN {
b ← mop_cmpo_v_idx xs v (l+lci);
if b then doN {
(lc,xs) ← mop_geth3 l h xs lci;
xs ← mop_seth3 l h xs i lc;
RETURN (xs,lci,True)
} else RETURN (xs,i,False)
}
}) (xs,i⇩1,True);
ASSERT (i≥i⇩1);
if has_lchild3 l h i then doN {
lci ← mop_lchild3 h i;
ASSERT (l+lci<h);
b ← mop_cmpo_v_idx xs v (l+lci);
if b then doN {
(lc,xs) ← mop_geth3 l h xs lci;
xs ← mop_seth3 l h xs i lc;
xs ← mop_seth3 l h xs lci v;
xs ← mop_to_wo_conv xs;
RETURN xs
} else doN {
xs ← mop_seth3 l h xs i v;
xs ← mop_to_wo_conv xs;
RETURN xs
}
} else doN {
xs ← mop_seth3 l h xs i v;
xs ← mop_to_wo_conv xs;
RETURN xs
}
}"
definition "woe_eq_except i xs' xs ≡ length xs' = length xs ∧ xs'!i=None ∧ (∀j∈{0..<length xs}-{i}. xs'!j = Some (xs!j))"
lemma woe_eq_except_init: "i<length xs ⟹ woe_eq_except i ((map Some xs)[i := None]) xs"
unfolding woe_eq_except_def by auto
lemma woe_eq_except_length[simp]: "woe_eq_except i xs' xs ⟹ length xs'=length xs"
unfolding woe_eq_except_def by auto
lemma woe_eq_except_nth_eq_Some: "⟦woe_eq_except i xs' xs; j<length xs⟧ ⟹ xs'!j = Some v ⟷ (j≠i ∧ v = xs!j)"
unfolding woe_eq_except_def
by force
lemma woe_eq_except_nth: "⟦woe_eq_except i xs' xs; j<length xs; j≠i⟧ ⟹ xs'!j = Some (xs!j)"
unfolding woe_eq_except_def
by force
lemma woe_eq_except_ith[simp]: "⟦woe_eq_except i xs' xs⟧ ⟹ xs'!i = None"
unfolding woe_eq_except_def
by force
lemma woe_eq_except_upd:
assumes "woe_eq_except i xs' xs" "i'<length xs" "i<length xs" "i≠i'"
shows "woe_eq_except i' (xs'[i':=None,i:=Some v]) (xs[i:=v])"
using assms unfolding woe_eq_except_def by (auto simp: nth_list_update)
definition "sd23_rel ≡ {((xs',i',ctd'),(xs,i,ctd)). i'=i ∧ ctd'=ctd ∧ i+l<length xs ∧ woe_eq_except (i+l) xs' xs }"
lemma in_sd23_rel_conv: "((xs',i',ctd'),(xs,i,ctd))∈sd23_rel ⟷ i'=i ∧ ctd'=ctd ∧ i+l<length xs ∧ woe_eq_except (i+l) xs' xs"
by (auto simp: sd23_rel_def)
lemma sift_down3_refine: "sift_down3 i xs ≤⇓Id (sift_down2 i xs)"
unfolding sift_down3_def sift_down2_def
supply [simp del] = conc_Id
apply (simp add: Let_def mop_geth3_def cong: if_cong)
apply (intro refine0)
apply clarsimp_all [3]
apply (rule bind_refine)
apply (rule WHILEIT_refine)
apply (rule introR[where R=sd23_rel])
apply (auto simp: sd23_rel_def woe_eq_except_init) []
apply (auto simp: sd23_rel_def) []
apply (auto simp: sd23_rel_def) []
subgoal
apply clarsimp
apply (intro refine0 bind_refine')
apply refine_dref_type
supply [[put_named_ss Main_ss]]
apply (auto simp: conc_Id in_sd23_rel_conv woe_eq_except_length woe_eq_except_nth) [4]
unfolding mop_seth3_def
apply refine_vcg
apply (auto simp: in_sd23_rel_conv woe_eq_except_length woe_eq_except_nth algebra_simps woe_eq_except_ith woe_eq_except_upd)
done
subgoal
apply (clarsimp split: prod.splits split del: if_split cong: if_cong simp: mop_seth3_def)
apply refine_rcg
apply refine_dref_type
supply [[put_named_ss Main_ss]]
apply (auto simp: conc_Id in_sd23_rel_conv woe_eq_except_length woe_eq_except_nth algebra_simps woe_eq_except_ith woe_eq_except_upd in_set_conv_nth nth_list_update list_eq_iff_nth_eq)
done
done
end
concrete_definition sift_down4 is heap_context.sift_down3_def
context heap_context begin
lemma sift_down4_full_refine: "sift_down4 (❙<) l h i xs ≤ sift_down i xs"
proof -
note sift_down4.refine[OF heap_context_axioms, symmetric, THEN meta_eq_to_obj_eq]
also note sift_down3_refine
also note sift_down2_refine
also note sift_down1_refine
finally show ?thesis by simp
qed
lemmas sift_down4_btu_correct = order_trans[OF sift_down4_full_refine sift_down_btu_correct]
lemmas sift_down4_restore_correct = order_trans[OF sift_down4_full_refine sift_down_restore_correct]
definition "heapify_btu xs⇩0 ≡ doN {
ASSERT(h>0);
(xs,l') ← WHILET
(λ(xs,l'). l'>l)
(λ(xs,l'). doN {
ASSERT (l'>0);
let l'=l'-1;
xs ← sift_down4 (❙<) l h l' xs;
RETURN (xs,l')
})
(xs⇩0,h-1);
RETURN xs
}"
lemma heapify_btu_correct: "⟦ l<h; h≤length xs⇩0 ⟧ ⟹ heapify_btu xs⇩0 ≤ SPEC (λxs. slice_eq_mset l h xs xs⇩0 ∧ is_heap xs)"
unfolding heapify_btu_def
apply simp
apply (refine_vcg WHILET_rule[where I="λ(xs,l'). heapify_btu_invar xs⇩0 l' xs ∧ l'≥l" and R="measure snd"] sift_down4_btu_correct)
apply (all ‹(auto;fail)?›)
apply clarsimp_all
subgoal by (simp add: heapify_btu_invar_def btu_heapify_init)
subgoal by (auto simp: heapify_btu_invar_def)
subgoal by (auto simp: heapify_btu_invar_def btu_heapify_term)
done
end
concrete_definition heapify_btu1 for less l h xs⇩0 is heap_context.heapify_btu_def
context heap_context begin
lemmas heapify_btu1_correct = heapify_btu_correct[unfolded heapify_btu1.refine[OF heap_context_axioms]]
end
context weak_ordering begin
definition heapsort :: "'a list ⇒ nat ⇒ nat ⇒ 'a list nres" where "heapsort xs⇩0 l h⇩0 ≡ doN {
ASSERT (l≤h⇩0);
if h⇩0-l > 1 then doN {
xs ← heapify_btu1 (❙<) l h⇩0 xs⇩0;
(xs,h)←WHILEIT (λ(xs,h).
l<h ∧ h≤h⇩0
∧ heap_context.is_heap (le_by_lt (❙<)) l h xs
∧ slice_eq_mset l h⇩0 xs xs⇩0
∧ sorted_wrt_lt (❙<) (slice h h⇩0 xs)
∧ (∀a∈set (slice l h xs). ∀b∈set (slice h h⇩0 xs). (le_by_lt (❙<)) a b)
)
(λ(xs,h). Suc l < h)
(λ(xs,h). doN {
ASSERT (h>0 ∧ l≠h-1);
xs ← mop_list_swap xs l (h-1);
xs ← sift_down4 (❙<) l (h-1) l xs;
RETURN (xs,h-1)
})
(xs,h⇩0);
RETURN xs
} else
RETURN xs⇩0
}"
lemma heapsort_correct:
assumes "l≤h⇩0" "h⇩0≤length xs⇩0"
shows "heapsort xs⇩0 l h⇩0 ≤ SPEC (λxs. slice_eq_mset l h⇩0 xs xs⇩0 ∧ sorted_wrt_lt (❙<) (slice l h⇩0 xs))"
proof -
interpret initial: heap_context "(❙≤)" "(❙<)" l h⇩0 by unfold_locales fact
show ?thesis
using assms unfolding heapsort_def le_by_lt
apply (refine_vcg WHILEIT_rule[where R="measure snd"] initial.heapify_btu1_correct )
apply (all ‹(auto dest: slice_eq_mset_eq_length;fail)?›)
apply clarsimp
subgoal premises prems for xs⇩1 xs h proof -
interpret heap_context "(❙≤)" "(❙<)" l h using prems by (unfold_locales) auto
interpret N: heap_context "(❙≤)" "(❙<)" l "h-Suc 0" using prems by (unfold_locales) auto
from prems have
[simp]: "length xs = length xs⇩0"
and [simp, arith]: "h⇩0 ≤ length xs⇩0"
by (auto simp: slice_eq_mset_eq_length)
{
fix xs'
assume A: "slice_eq_mset l (h - Suc 0) xs' (swap xs l (h - Suc 0))"
hence "slice_eq_mset l h⇩0 xs' (swap xs l (h - Suc 0))"
apply (rule slice_eq_mset_subslice)
using prems by auto
from this[symmetric] have "slice_eq_mset l h⇩0 xs' xs"
apply -
apply (drule slice_eq_mset_swap(2)[THEN iffD1, rotated -1])
using prems by (auto dest: slice_eq_mset_sym)
also note ‹slice_eq_mset l h⇩0 xs xs⇩0›
finally have G1: "slice_eq_mset l h⇩0 xs' xs⇩0" .
note [simp] = slice_eq_mset_eq_length[OF G1]
have [simp]: "slice (h - Suc 0) h⇩0 xs' = (xs'!(h-Suc 0))#slice h h⇩0 xs'"
apply (rule slice_extend1_left)
using prems by (auto)
have "slice h h⇩0 xs' = slice h h⇩0 (swap xs l (h - Suc 0))"
apply (rule slice_eq_mset_eq_outside(2)[OF A]) using prems by auto
also have "… = slice h h⇩0 xs"
by (metis Suc_lessD atLeastLessThan_iff leI le_antisym le_zero_eq nat_less_le nz_le_conv_less ‹Suc l < h› slice_swap_outside)
finally have [simp]: "slice h h⇩0 xs' = slice h h⇩0 xs" .
have [arith,simp]: "h - Suc 0 < length xs⇩0" "l<length xs⇩0" using prems by (auto)
have [simp]: "xs' ! (h - Suc 0) = xs!l"
using slice_eq_mset_nth_outside[OF A, of "h-Suc 0"]
by auto
have "xs!l ∈ set (slice l h xs)" using prems by (auto simp: set_slice_conv)
then have G2: "sorted_wrt (❙≤) (slice (h - Suc 0) h⇩0 xs')"
using prems
by (auto)
have [simp]: "slice l (h - Suc 0) (swap xs l (h - Suc 0)) = xs!(h-Suc 0)#(slice (Suc l) (h-Suc 0) xs)"
apply (rule nth_equalityI)
apply (auto simp: nth_list_update slice_nth swap_nth Suc_diff_Suc ‹Suc l < h›)
done
have "in_heap (h - Suc 0)"
unfolding in_heap_def apply simp
using ‹Suc l < h› by linarith
have G3: "∀a ∈ set (slice l (h - Suc 0) xs'). ∀b ∈ set (slice (h - Suc 0) h⇩0 xs'). a❙≤b"
thm slice_eq_mset_set_inside[OF A]
apply (simp add: slice_eq_mset_set_inside[OF A])
using ‹∀x∈set (slice l h xs). ∀_∈_. _›
apply (auto simp: set_slice_conv root_greatest[OF ‹is_heap xs› ‹in_heap (h-Suc 0)›])
subgoal using N.ran_not_empty ‹in_heap (h - Suc 0)› in_heap_bounds(2) by blast
subgoal for j
apply (subgoal_tac "in_heap j")
using root_greatest[OF ‹is_heap xs›, of j] apply blast
unfolding in_heap_def by simp
subgoal by (metis Suc_le_lessD diff_le_self less_imp_le less_le_trans)
done
note G1 G2 G3
} note aux=this
note rl = N.sift_down4_restore_correct[OF _ sift_down_invar_init[OF ‹is_heap xs› ‹Suc l < h›]]
show ?thesis
apply (refine_vcg rl)
using ‹Suc l < h› ‹h≤h⇩0›
apply (auto simp: aux)
done
qed
apply clarsimp
subgoal premises prems for xs⇩1 xs h
proof -
have [simp]: "h=l+1" using prems by auto
from prems have [simp]: "length xs = length xs⇩0"
and [simp, arith]: "l<length xs⇩0" "h<length xs⇩0"
by (auto dest: slice_eq_mset_eq_length)
have "set (slice l (Suc l) xs) = {xs!l}" by simp
show ?thesis using prems
by (auto simp: slice_split_hd le_by_lt)
qed
subgoal
by (simp add: sorted_wrt01)
done
qed
lemma heapsort_correct': "⟦(xs,xs')∈Id; (l,l')∈Id; (h,h')∈Id⟧ ⟹ heapsort xs l h ≤⇓Id (slice_sort_spec (❙<) xs' l' h')"
unfolding slice_sort_spec_alt
apply (refine_vcg heapsort_correct)
apply (auto simp: slice_eq_mset_alt)
done
end
concrete_definition heapsort1 for less xs⇩0 l h⇩0 is weak_ordering.heapsort_def
context weak_ordering begin
lemmas heapsort1_correct = heapsort_correct[unfolded heapsort1.refine[OF weak_ordering_axioms]]
end
sepref_register mop_lchild3 mop_rchild3 has_rchild3 has_lchild3 mop_geth3 mop_seth3
sepref_def mop_lchild_impl [llvm_inline] is "uncurry mop_lchild3" :: "size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding mop_lchild3_def apply (annot_snat_const "TYPE (size_t)") by sepref
sepref_def mop_rchild_impl [llvm_inline] is "uncurry mop_rchild3" :: "size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding mop_rchild3_def apply (annot_snat_const "TYPE (size_t)") by sepref
sepref_def has_lchild_impl [llvm_inline] is "uncurry2 (RETURN ooo has_lchild3)" :: "[λ((l,h),i). l≤h]⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k → bool1_assn"
unfolding has_lchild3_def apply (annot_snat_const "TYPE (size_t)") by sepref
sepref_def has_rchild_impl [llvm_inline] is "uncurry2 (RETURN ooo has_rchild3)" :: "[λ((l,h),i). l<h]⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k → bool1_assn"
unfolding has_rchild3_def apply (annot_snat_const "TYPE (size_t)") by sepref
sepref_def mop_geth_impl [llvm_inline] is "uncurry3 mop_geth3"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a (eoarray_slice_assn elem_assn)⇧d *⇩a size_assn⇧k → elem_assn ×⇩a eoarray_slice_assn elem_assn [λ(((_,_),ai),_) (_,ri). ri=ai]⇩c"
unfolding mop_geth3_def by sepref
sepref_def mop_seth_impl [llvm_inline] is "uncurry4 mop_seth3"
:: "[λ_. True]⇩c
size_assn⇧k *⇩a size_assn⇧k *⇩a (eoarray_slice_assn elem_assn)⇧d *⇩a size_assn⇧k *⇩a elem_assn⇧d
→ eoarray_slice_assn elem_assn
[λ((((_,_),ai),_),_) ri. ri=ai]⇩c"
unfolding mop_seth3_def by sepref
context sort_impl_context begin
sepref_register "sift_down4 (❙<)"
sepref_def sift_down_impl is "uncurry3 (PR_CONST (sift_down4 (❙<)))"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a (woarray_slice_assn elem_assn)⇧d
→ (woarray_slice_assn elem_assn) [λ(((_,_),_),ai) ri. ri=ai]⇩c"
unfolding sift_down4_def PR_CONST_def
by sepref_dbg_keep
sepref_register "heapify_btu1 (❙<)"
sepref_def heapify_btu_impl is "uncurry2 (PR_CONST (heapify_btu1 (❙<)))"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a (woarray_slice_assn elem_assn)⇧d → (woarray_slice_assn elem_assn) [λ((_,_),ai) r. r=ai]⇩c"
unfolding heapify_btu1_def PR_CONST_def
apply (annot_snat_const "TYPE (size_t)")
by sepref
sepref_register "heapsort1 (❙<)"
sepref_def heapsort_impl is "uncurry2 (PR_CONST (heapsort1 (❙<)))" ::
"[λ_. True]⇩c (woarray_slice_assn elem_assn)⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k → (woarray_slice_assn elem_assn) [λ((ai,_),_) r. r=ai]⇩c"
unfolding heapsort1_def PR_CONST_def
apply (rewrite at "sift_down4 _ _ _ ⌑ _" fold_COPY)
apply (annot_snat_const "TYPE (size_t)")
by sepref
sepref_register heapsort
lemmas heapsort_hnr[sepref_fr_rules] = heapsort_impl.refine[unfolded heapsort1.refine[OF weak_ordering_axioms,symmetric]]
end
subsection ‹Parameterized Comparison›
context parameterized_weak_ordering begin
definition sift_down_param :: "'cparam ⇒ nat ⇒ nat ⇒ nat ⇒ 'a list ⇒ 'a list nres"
where "sift_down_param cparam l h i⇩0 xs ≡ doN {
ASSERT (l≤i⇩0 ∧ i⇩0<h);
let i⇩1 = i⇩0 - l;
xs ← mop_to_eo_conv xs;
(v,xs) ← mop_geth3 l h xs i⇩1;
(xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i⇩1) (λ(xs,i,ctd). has_rchild3 l h i ∧ ctd) (λ(xs,i,ctd). doN {
lci ← mop_lchild3 h i;
rci ← mop_rchild3 h i;
ASSERT (l+lci<h ∧ l+rci<h ∧ l+lci ≠ l+rci);
b ← pcmpo_idxs2 cparam xs (l+lci) (l+rci);
if b then doN {
b ← pcmpo_v_idx2 cparam xs v (l+rci);
if b then doN {
(rc,xs) ← mop_geth3 l h xs rci;
xs ← mop_seth3 l h xs i rc;
RETURN (xs,rci,True)
} else RETURN (xs,i,False)
} else doN {
b ← pcmpo_v_idx2 cparam xs v (l+lci);
if b then doN {
(lc,xs) ← mop_geth3 l h xs lci;
xs ← mop_seth3 l h xs i lc;
RETURN (xs,lci,True)
} else RETURN (xs,i,False)
}
}) (xs,i⇩1,True);
ASSERT (i≥i⇩1);
if has_lchild3 l h i then doN {
lci ← mop_lchild3 h i;
ASSERT (l+lci<h);
b ← pcmpo_v_idx2 cparam xs v (l+lci);
if b then doN {
(lc,xs) ← mop_geth3 l h xs lci;
xs ← mop_seth3 l h xs i lc;
xs ← mop_seth3 l h xs lci v;
xs ← mop_to_wo_conv xs;
RETURN xs
} else doN {
xs ← mop_seth3 l h xs i v;
xs ← mop_to_wo_conv xs;
RETURN xs
}
} else doN {
xs ← mop_seth3 l h xs i v;
xs ← mop_to_wo_conv xs;
RETURN xs
}
}"
lemma mop_geth3_cdom_refine: "⟦
(l',l)∈Id; (h',h)∈Id; (i',i)∈Id; (xs',xs)∈cdom_olist_rel cparam
⟧ ⟹ mop_geth3 l' h' xs' i'
≤ ⇓(br id (λx. x ∈ cdom cparam) ×⇩r cdom_olist_rel cparam) (mop_geth3 l h xs i)"
unfolding mop_geth3_def
apply refine_rcg
by auto
lemma mop_seth3_cdom_refine: "⟦
(l',l)∈Id; (h',h)∈Id; (i',i)∈Id; (xs',xs)∈cdom_olist_rel cparam; (v',v)∈Id; v∈cdom cparam
⟧ ⟹ mop_seth3 l' h' xs' i' v'
≤ ⇓(cdom_olist_rel cparam) (mop_seth3 l h xs i v)"
unfolding mop_seth3_def
apply refine_rcg
by auto
lemma sift_down_param_refine[refine]: "⟦ (l',l)∈Id; (h',h)∈Id; (i⇩0',i⇩0)∈Id; (xs',xs)∈cdom_list_rel cparam ⟧
⟹ sift_down_param cparam l' h' i⇩0' xs' ≤ ⇓(cdom_list_rel cparam) (sift_down4 (less' cparam) l h i⇩0 xs)"
unfolding sift_down_param_def sift_down4_def
apply (refine_rcg mop_geth3_cdom_refine mop_seth3_cdom_refine)
apply (all ‹(intro IdI)?;(elim conjE IdE Pair_inject)?;(assumption)?›)
supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"] RELATESI[of "cdom_olist_rel cparam"]
apply refine_dref_type
apply (simp_all named_ss HOL_ss: IdI split in_br_conv prod_rel_iff cdom_olist_rel_def id_def)
apply simp_all
apply (simp_all split: prod.splits)
done
definition "heapify_btu_param cparam l h xs⇩0 ≡ doN {
ASSERT(h>0);
(xs,l') ← WHILET
(λ(xs,l'). l'>l)
(λ(xs,l'). doN {
ASSERT (l'>0);
let l'=l'-1;
xs ← sift_down_param cparam l h l' xs;
RETURN (xs,l')
})
(xs⇩0,h-1);
RETURN xs
}"
lemma heapify_btu_param_refine[refine]:
"⟦ (l',l)∈Id; (h',h)∈Id; (xs',xs)∈cdom_list_rel cparam⟧
⟹ heapify_btu_param cparam l' h' xs' ≤ ⇓(cdom_list_rel cparam) (heapify_btu1 (less' cparam) l h xs)"
unfolding heapify_btu_param_def heapify_btu1_def
apply (refine_rcg prod_relI)
supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"]
apply refine_dref_type
by auto
term heapsort1
definition heapsort_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list nres"
where "heapsort_param cparam xs⇩0 l h⇩0 ≡ doN {
ASSERT (l≤h⇩0);
if h⇩0-l > 1 then doN {
xs ← heapify_btu_param cparam l h⇩0 xs⇩0;
(xs,h)←WHILET
(λ(xs,h). Suc l < h)
(λ(xs,h). doN {
ASSERT (h>0 ∧ l≠h-1);
xs ← mop_list_swap xs l (h-1);
xs ← sift_down_param cparam l (h-1) l xs;
RETURN (xs,h-1)
})
(xs,h⇩0);
RETURN xs
} else
RETURN xs⇩0
}"
lemma heapsort_param_refine[refine]: "⟦
(l',l)∈Id; (h',h)∈Id; (xs',xs)∈cdom_list_rel cparam
⟧ ⟹ heapsort_param cparam xs' l' h' ≤ ⇓(cdom_list_rel cparam) (heapsort1 (less' cparam) xs l h)"
unfolding heapsort_param_def heapsort1_def mop_list_swap_alt
apply refine_rcg
supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"]
apply refine_dref_type
apply (auto simp: in_br_conv cdom_list_rel_alt)
done
lemma heapsort_param_correct:
assumes "(xs',xs)∈Id" "(l',l)∈Id" "(h',h)∈Id"
shows "heapsort_param cparam xs' l' h' ≤ pslice_sort_spec cdom pless cparam xs l h"
proof -
note heapsort_param_refine[unfolded heapsort1.refine[OF WO.weak_ordering_axioms, symmetric]]
also note WO.heapsort_correct'
also note slice_sort_spec_xfer
finally show ?thesis
unfolding pslice_sort_spec_def
apply refine_vcg
using assms unfolding cdom_list_rel_alt
by (simp add: in_br_conv)
qed
lemma heapsort_param_correct':
shows "(PR_CONST heapsort_param, PR_CONST (pslice_sort_spec cdom pless)) ∈ Id → Id → Id → Id → ⟨Id⟩nres_rel"
using heapsort_param_correct
apply (intro fun_relI nres_relI)
by simp
end
context parameterized_sort_impl_context begin
sepref_def mop_geth_impl [llvm_inline] is "uncurry3 mop_geth3"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a eo_assn⇧d *⇩a size_assn⇧k
→ elem_assn ×⇩a eo_assn [λ(((_,_),ai),_) (_,r). r=ai]⇩c"
unfolding mop_geth3_def by sepref
sepref_def mop_seth_impl [llvm_inline] is "uncurry4 mop_seth3"
:: "[λ_. True]⇩c size_assn⇧k *⇩a size_assn⇧k *⇩a eo_assn⇧d *⇩a size_assn⇧k *⇩a elem_assn⇧d
→ eo_assn [λ((((_,_),ai),_),_) r. r=ai]⇩c"
unfolding mop_seth3_def by sepref
end
context parameterized_sort_impl_context
begin
sepref_register "sift_down_param"
sepref_def sift_down_impl is "uncurry4 (PR_CONST sift_down_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a wo_assn⇧d
→ wo_assn [λ((((_,_),_),_),ai) r. r=ai]⇩c"
unfolding sift_down_param_def PR_CONST_def
by sepref
sepref_register "heapify_btu_param"
sepref_def heapify_btu_impl is "uncurry3 (PR_CONST heapify_btu_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a wo_assn⇧d → wo_assn [λ(((_,_),_),ai) r. r=ai]⇩c"
unfolding heapify_btu_param_def PR_CONST_def
apply (annot_snat_const "TYPE (size_t)")
by sepref
sepref_register "heapsort_param"
sepref_def heapsort_param_impl is "uncurry3 (PR_CONST heapsort_param)"
:: "[λ_. True]⇩c cparam_assn⇧k *⇩a wo_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k → wo_assn [λ(((_,ai),_),_) r. r=ai]⇩c"
unfolding heapsort_param_def PR_CONST_def
apply (rewrite at "sift_down_param _ _ _ ⌑ _" fold_COPY)
apply (annot_snat_const "TYPE (size_t)")
by sepref
lemmas heapsort_param_hnr
= heapsort_param_impl.refine[FCOMP heapsort_param_correct']
end
end