Theory Examples.Sorting

theory Sorting_Heapsort imports Sorting_Setup begin (* TODO: Fix section structure *) locale heap_range_context = fixes l h :: nat assumes ran_not_empty[arith,simp]: "l≤h" begin (*lemma l_le_h[arith,simp]: "l≤h" by simp*) 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₀ i xs ≡ slice_eq_mset l h xs xs₀ ∧ is_heap_except_up i xs" lemma sift_up_invar_init: assumes "is_heap xs" "slice_eq_mset l h xs xs₀" "h<length xs" shows "heap_context.sift_up_invar (≤) l (Suc h) xs₀ 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₀ i xs; has_parent i; xs!i≥xs!parent i ⟧ ⟹ sift_up_invar xs₀ (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₀ l xs⟧ ⟹ is_heap xs ∧ slice_eq_mset l h xs xs₀" unfolding sift_up_invar_def using sift_up_term1 by blast lemma sift_up_invar_term2: "⟦sift_up_invar xs₀ i xs; xs!i≤xs!parent i⟧ ⟹ is_heap xs ∧ slice_eq_mset l h xs xs₀" unfolding sift_up_invar_def using sift_up_term2 by blast definition "sift_down_invar xs₀ i xs ≡ slice_eq_mset l h xs xs₀ ∧ is_heap_except_down i xs" lemma sift_down_invar_step: assumes "sift_down_invar xs₀ i xs" shows "⟦has_rchild i; xs!i≤xs!lchild i; xs!lchild i ≥ xs!rchild i⟧ ⟹ sift_down_invar xs₀ (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₀ (rchild i) (swap xs i (rchild i))" and "⟦has_lchild i; ¬has_rchild i; xs!i≤xs!lchild i⟧ ⟹ sift_down_invar xs₀ (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 (*xxx, ctd here: we need to initialize from heapsort loop invariant*) 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₀ l' xs ≡ slice_eq_mset l h xs xs₀ ∧ is_heap_btu l' xs" definition "sift_down_btu_invar xs₀ l' i xs ≡ slice_eq_mset l h xs xs₀ ∧ 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₀ xs ≡ doN { ASSERT (in_heap i₀ ∧ i₀<length xs); (xs,i,_) ← WHILEIT (λ(xs,i,ctd). in_heap i ∧ i≥i₀) (λ(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₀,True); ASSERT (in_heap i ∧ i≥i₀); 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₀ l' xs" "l<l'" shows "sift_down (l'-Suc 0) xs ≤ SPEC (λxs'. heapify_btu_invar xs₀ (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₀ (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₀ l xs" shows "sift_down l xs ≤ SPEC (λxs'. slice_eq_mset l h xs' xs₀ ∧ is_heap xs')" unfolding sift_down_def apply (refine_vcg WHILEIT_rule_amend_invar[where I="λ(xs,i,ctd). sift_down_invar xs₀ 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 simp*) 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₀ xs ≡ doN { ASSERT (in_heap i₀); v ← mop_list_get xs i₀; (xs,i,_) ← WHILEIT (λ(xs,i,ctd). in_heap i ∧ i≥i₀) (λ(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₀,True); ASSERT (in_heap i ∧ i≥i₀); 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₀ xs ≤⇓Id (sift_down i₀ 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)?›) (*apply simp apply refine_rcg apply (auto simp: swap_def)*) 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₀ xs ≡ doN { ASSERT (l≤i₀ ∧ i₀<h); let i₁ = i₀ - l; v ← mop_list_get xs (i₁+l); (xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i₁) (λ(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₁,True); ASSERT (i≥i₁ ∧ 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) (** Takes loooong *) 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 (* Auxiliary definitions to reduce proof complexity in sepref-step. TODO: Without these, the sepref step gets really slow, which is another indication that we should separate the bound-proofs from the actual transfer step! *) 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₀ xs ≡ doN { ASSERT (l≤i₀ ∧ i₀<h); let i₁ = i₀ - l; xs ← mop_to_eo_conv xs; (v,xs) ← mop_geth3 l h xs i₁; (xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i₁) (λ(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₁,True); ASSERT (i≥i₁); 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 } }" (* TODO: Move. Use also in insort. Maybe generalize to index set? *) 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] (*apply (use [[put_named_ss Main_ss]] in ‹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₀ ≡ 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₀,h-1); RETURN xs }" lemma heapify_btu_correct: "⟦ l<h; h≤length xs₀ ⟧ ⟹ heapify_btu xs₀ ≤ SPEC (λxs. slice_eq_mset l h xs xs₀ ∧ is_heap xs)" unfolding heapify_btu_def apply simp apply (refine_vcg WHILET_rule[where I="λ(xs,l'). heapify_btu_invar xs₀ l' xs ∧ l'≥l" and R="measure snd"] sift_down4_btu_correct) apply (all ‹(auto;fail)?›) apply clarsimp_all (* Required to get rid of local variables that will obfuscate locale abbreviations! *) 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₀ 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 (* TODO: We keep ≤ out of the definition (although it occurs in invariants). Otherwise, getting rid of the ≤ ghost parameter is difficult! *) definition heapsort :: "'a list ⇒ nat ⇒ nat ⇒ 'a list nres" where "heapsort xs₀ l h₀ ≡ doN { ASSERT (l≤h₀); if h₀-l > 1 then doN { xs ← heapify_btu1 (<) l h₀ xs₀; (xs,h)←WHILEIT (λ(xs,h). l<h ∧ h≤h₀ ∧ heap_context.is_heap (le_by_lt (<)) l h xs ∧ slice_eq_mset l h₀ xs xs₀ ∧ sorted_wrt_lt (<) (slice h h₀ xs) ∧ (∀a∈set (slice l h xs). ∀b∈set (slice h h₀ 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₀); RETURN xs } else RETURN xs₀ }" lemma heapsort_correct: assumes "l≤h₀" "h₀≤length xs₀" shows "heapsort xs₀ l h₀ ≤ SPEC (λxs. slice_eq_mset l h₀ xs xs₀ ∧ sorted_wrt_lt (<) (slice l h₀ xs))" proof - interpret initial: heap_context "(≤)" "(<)" l h₀ 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₁ xs h proof - (* TODO: This is the argument that swapping the max-element to the end will preserve the sortedness criteria. Though apparently simple, the reasoning seems to be much too complex here. Try to improve on that! *) 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₀" and [simp, arith]: "h₀ ≤ length xs₀" 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₀ 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₀ 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₀ xs xs₀› finally have G1: "slice_eq_mset l h₀ xs' xs₀" . note [simp] = slice_eq_mset_eq_length[OF G1] have [simp]: "slice (h - Suc 0) h₀ xs' = (xs'!(h-Suc 0))#slice h h₀ xs'" apply (rule slice_extend1_left) using prems by (auto) have "slice h h₀ xs' = slice h h₀ (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₀ 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₀ xs' = slice h h₀ xs" . have [arith,simp]: "h - Suc 0 < length xs₀" "l<length xs₀" 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₀ 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₀ 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₀› apply (auto simp: aux) done qed apply clarsimp subgoal premises prems for xs₁ xs h proof - have [simp]: "h=l+1" using prems by auto from prems have [simp]: "length xs = length xs₀" and [simp, arith]: "l<length xs₀" "h<length xs₀" 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₀ l h₀ 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 (* Takes loooong! *) 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₀ xs ≡ doN { ASSERT (l≤i₀ ∧ i₀<h); let i₁ = i₀ - l; xs ← mop_to_eo_conv xs; (v,xs) ← mop_geth3 l h xs i₁; (xs,i,_) ← WHILEIT (λ(xs,i,ctd). i<h-l ∧ i≥i₁) (λ(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₁,True); ASSERT (i≥i₁); 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₀',i₀)∈Id; (xs',xs)∈cdom_list_rel cparam ⟧ ⟹ sift_down_param cparam l' h' i₀' xs' ≤ ⇓(cdom_list_rel cparam) (sift_down4 (less' cparam) l h i₀ 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 (* Note: The 3 simps below are an optimization for speed. Just a simp_all on the 65 subgoals takes too long.*) 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₀ ≡ 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₀,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₀ l h₀ ≡ doN { ASSERT (l≤h₀); if h₀-l > 1 then doN { xs ← heapify_btu_param cparam l h₀ xs₀; (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₀); RETURN xs } else RETURN xs₀ }" 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 (* TODO: inlined mop-list-swap refinement proof! *) 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 (* Takes loooong! *) 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 (* TODO: Show that this refines a param_sort_spec! lemmas heapsort_hnr[sepref_fr_rules] = heapsort_param_impl.refine[unfolded heapsort_param.refine[OF weak_ordering_axioms,symmetric]] *) lemmas heapsort_param_hnr = heapsort_param_impl.refine[FCOMP heapsort_param_correct'] end (* global_interpretation heapsort_interp: pure_sort_impl_context "(≤)" "(<)" ll_icmp_ult unat_assn defines heapsort_interp_mop_lchild_impl = heapsort_interp.mop_lchild_impl and heapsort_interp_mop_rchild_impl = heapsort_interp.mop_rchild_impl and heapsort_interp_has_rchild_impl = heapsort_interp.has_rchild_impl and heapsort_interp_has_lchild_impl = heapsort_interp.has_lchild_impl and heapsort_interp_mop_geth_impl = heapsort_interp.mop_geth_impl and heapsort_interp_mop_seth_impl = heapsort_interp.mop_seth_impl and heapsort_interp_sift_down_impl = heapsort_interp.sift_down_impl and heapsort_interp_heapify_btu_impl = heapsort_interp.heapify_btu_impl and heapsort_interp_heapsort_impl = heapsort_interp.heapsort_impl by (rule unat_sort_impl_context) export_llvm "heapsort_interp_heapsort_impl :: 64 word ptr ⇒ _" is "uint64_t* heapsort(uint64_t*, int64_t,int64_t)" file "../code/heapsort.ll" *) end

Theory Examples.Sorting_Heapsort