Theory Sorting_Results

✐‹creator "Maximilian P. L. Haslbeck"›
section ‹Final Hoare Triples for heapsort and introsort›
theory Sorting_Results
imports Sorting_Export_Code
begin

paragraph ‹Summary›
text ‹This theory collects the final Hoare Triples for heapsort and introsort.
  They do not involve the NREST monad any more. For inspecting their validity, only the
  LLVM semantics and the definitions of Hoare triples must be checked.
  By summing over all currencies, we project the fine-grained cost functions used in the
  Hoare Triples down to functions in @{typ "nat ⇒ nat"} and examine their asymptotic complexity.›


subsection ‹Heapsort›


context sort_impl_context begin

lemma "slice_sort_aux xs⇩0 xs l h ≡ (length xs = length xs⇩0 ∧ take l xs = take l xs⇩0
                    ∧ drop h xs = drop h xs⇩0 ∧ sort_spec (❙<) (slice l h xs⇩0) (slice l h xs))"
  by simp

text ‹Final correctness lemma:›
lemma 
  assumes "l ≤ h ∧ h ≤ length xs⇩0"
  shows "llvm_htriple ($heapsort_impl_cost l h ∧* arr_assn xs⇩0 p
           ∧* snat_assn l l' ∧* snat_assn h h')
        (heapsort_impl p l' h')
      (λr. (λs. ∃xs. (↑(slice_sort_aux xs⇩0 xs l h) ∧* arr_assn xs r) s)
            ∧* snat_assn l l' ∧* snat_assn h h')"
  using assms
  apply(rule heapsort_final_hoare_triple[unfolded hn_ctxt_def])
  done

(*text ‹@{term heapsort_impl_cost} projected to a function @{typ "nat ⇒ nat"} ›
lemma "heapsort3_allcost (h-l) = project_all (heapsort_impl_cost l h)"
  by (simp add: heapsort3_allcost_is_heapsort3_allcost' heapsort3_allcost'_Sum_any)
  *)

end

lemma "heapsort3_allcost n = 12 + 187 * n  + 82 * (n * Discrete.log n)"
  unfolding heapsort3_allcost_def by simp
  
lemma "(λx. real (heapsort3_allcost x)) ∈ Θ(λn. (real n)*(ln (real n)))"
  by (fact heapsort3_allcost_nlogn)


subsection ‹Introsort›

subsubsection ‹For Nats›

(*
lemma "introsort3_allcost n = 4693 + 5 *  Discrete.log n + 231 * n + 455 * (n * Discrete.log n)"
  by(fact introsort3_allcost_simplified)

  
lemma "(λx. real (introsort3_allcost x)) ∈ Θ(λn. (real n)*(ln (real n)))"
  by (fact introsort3_allcost_nlogn)
*)
(* Final results for unat_sort: *)  
thm unat_sort.introsort_final_hoare_triple[no_vars] (* Hoare triple *)

lemma "l ≤ h ∧ h ≤ length xs⇩0 ⟹
  llvm_htriple 
    ($unat_sort.introsort_impl_cost (h - l) ∧* unat_sort.arr_assn xs⇩0 p 
        ∧* snat_assn l l' ∧* snat_assn h h') 
      (unat_sort_introsort_impl p l' h')
    (λr. (λs. ∃xs. (↑unat_sort.slice_sort_aux xs⇩0 xs l h ∧* unat_sort.arr_assn xs r) s)
        ∧* snat_assn l l' ∧* snat_assn h h')"
  apply(rule unat_sort.introsort_final_hoare_triple) .

(* Cost estimation *)
  
theorem "(λn. real (project_all (unat_sort.introsort_impl_cost n)))
            ∈ Θ(λn. (real n) * (ln (real n)))"
  unfolding unat_sort_allcost_simp
  by auto2


subsubsection ‹For Strings›


thm string_sort.introsort_final_hoare_triple[no_vars]  (* Hoare triple *)
 string_sort_introsort_cost

lemma "l ≤ h ∧ h ≤ length xs⇩0 ⟹
  llvm_htriple 
    ($string_sort.introsort_impl_cost m (h - l) ∧* string_sort.arr_assn m xs⇩0 p
         ∧* snat_assn l l' ∧* snat_assn h h') 
      (string_sort_introsort_impl p l' h')
    (λr. (λs. ∃xs. (↑string_sort.slice_sort_aux xs⇩0 xs l h ∧* string_sort.arr_assn m xs r) s)
         ∧* snat_assn l l' ∧* snat_assn h h')"
  apply(rule string_sort.introsort_final_hoare_triple) .


lemma "(λ(m, n). real (project_all (string_sort.introsort_impl_cost m n)))
             ∈ Θ⇩2 (λ(m, n). real m * real n * ln (real n))"
  apply(rule string_sort_introsort_cost) .


subsection ‹Dynamic arrays›

lemma
  assumes "Sepref_Basic.is_pure A"
  and "2 * length a < max_snat LENGTH('c::len2)"
  and "8 ≤ LENGTH('c)"
shows dyn_array_push_impl_ht:
    "llvm_htriple
      ($da_append_spec_cost ∧* al_assn' TYPE('c) A a ai ∧* A b bi)
         (dyn_array_push_impl ai bi)
     (λr. (λs. ∃x. (↑(x = a @ [b]) ∧* dynamic_array_assn A x r) s) ∧* A b bi)"
  apply(rule introsort_final_hoare_triple[OF assms]) .

lemma "(λ_::nat. real (project_all da_append_spec_cost)) ∈ Θ(λ_::nat. 1::real)"
  unfolding all_da_append_spec_cost
  by auto2


end