Theory Sorting_Introsort

section ‹Introsort (roughly libstdc++ version)›
theory Sorting_Introsort
imports 
  Sorting_Final_insertion_Sort Sorting_Heapsort Sorting_Log2 
  Sorting_Quicksort_Partition
  Sorting_Strings
begin


context weak_ordering begin


  (* Assemble an introsort loop, using the partitioner and heap-sort *)  
  
  definition introsort_aux4 :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ 'a list nres" where "introsort_aux4 xs l h d ≡ RECT (λintrosort_aux (xs,l,h,d). doN {
    ASSERT (l≤h);
    if h-l > is_threshold then doN {
      if d=0 then
        heapsort xs l h
      else doN {
        (xs,m)←partition_pivot xs l h;
        xs ← introsort_aux (xs,l,m,d-1);
        xs ← introsort_aux (xs,m,h,d-1);
        RETURN xs
      }
    }
    else
      RETURN xs
  }) (xs,l,h,d)"


  lemma introsort_aux4_refine: "introsort_aux4 xs l h d ≤ (introsort_aux3 xs l h d)"
    unfolding introsort_aux4_def introsort_aux3_def
    apply (rule refine_IdD)
    apply (refine_rcg heapsort_correct' partition_pivot_correct)
    apply refine_dref_type
    apply simp_all 
    done

  lemmas introsort_aux4_correct = order_trans[OF introsort_aux4_refine introsort_aux3_correct, THEN refine_IdI]

  definition "introsort4 xs l h ≡ doN {
    ASSERT(l≤h);
    if h-l>1 then doN {
      xs ← introsort_aux4 xs l h (Discrete.log (h-l)*2);
      xs ← final_insertion_sort2 xs l h;
      RETURN xs
    } else RETURN xs
  }"  

  lemma introsort4_refine: "introsort4 xs l h ≤ introsort3 xs l h"
    unfolding introsort4_def introsort3_def
    apply (rule refine_IdD)
    apply (refine_rcg introsort_aux4_correct final_insertion_sort2_correct[THEN refine_IdI])
    by auto

  lemmas introsort4_correct = order_trans[OF introsort4_refine introsort3_correct]

end

lemma introsort_depth_limit_in_bounds_aux: (* TODO: Move depth-computation into own (inline) function *)
  assumes "n < max_snat N" "1<N" shows "Discrete.log (n) * 2 < max_snat N"
proof (cases "n=0")
  case True thus ?thesis using assms by auto
next
  case [simp]: False  
  have ?thesis if "Discrete.log (n) < max_snat (N-1)"
    using that ‹1<N› unfolding max_snat_def
    by (metis nat_mult_power_less_eq pos2 semiring_normalization_rules(33))
  moreover have "Discrete.log (n) < max_snat (N-1)"
    apply (rule discrete_log_ltI)
    using assms apply (auto simp: max_snat_def)
    by (smt Suc_diff_Suc leI le_less_trans n_less_equal_power_2 nat_power_less_imp_less not_less_eq numeral_2_eq_2 numeral_2_eq_2 zero_order(3))
  ultimately show ?thesis .
qed  
  


context sort_impl_context begin

sepref_register introsort_aux4
sepref_def introsort_aux_impl is "uncurry3 (PR_CONST introsort_aux4)" 
  :: "[λ_. True]c (arr_assn)d *a size_assnk *a size_assnk *a size_assnk 
    → arr_assn [λ(((ai,_),_),_) r. r=ai]c"
  unfolding introsort_aux4_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  apply (rewrite RECT_cp_annot[where CP="λ(ai,_,_,_) r. r=ai"])
  by sepref
  
  
  
sepref_register introsort4
sepref_def introsort_impl is "uncurry2 (PR_CONST introsort4)" 
  :: "[λ_. True]c (arr_assn)d *a size_assnk *a size_assnk → arr_assn [λ((ai,_),_) r. r=ai]c"
  unfolding introsort4_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  supply [intro!] = introsort_depth_limit_in_bounds_aux 
  by sepref

  
lemma introsort4_refine_ss_spec: "(PR_CONST introsort4, slice_sort_spec (<))∈Id→Id→Id→⟨Id⟩nres_rel"  
  using introsort4_correct by (auto intro: nres_relI)
  
theorem introsort_impl_correct: "(uncurry2 introsort_impl, uncurry2 (slice_sort_spec (<))) ∈ 
  [λ_. True]c arr_assnd *a snat_assnk *a snat_assnk → arr_assn [λ((ai,_),_) r. r=ai]c"  
  using introsort_impl.refine[FCOMP introsort4_refine_ss_spec] .
  
  
end



context parameterized_weak_ordering begin
  (* TODO: Move *)
  lemmas heapsort_param_refine'[refine] = heapsort_param_refine[unfolded heapsort1.refine[OF WO.weak_ordering_axioms, symmetric]]
  
  
  definition introsort_aux_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat ⇒ 'a list nres" where 
    "introsort_aux_param cparam xs l h d ≡ RECT (λintrosort_aux (xs,l,h,d). doN {
    ASSERT (l≤h);
    if h-l > is_threshold then doN {
      if d=0 then
        heapsort_param cparam xs l h
      else doN {
        (xs,m)←partition_pivot_param cparam xs l h;
        xs ← introsort_aux (xs,l,m,d-1);
        xs ← introsort_aux (xs,m,h,d-1);
        RETURN xs
      }
    }
    else
      RETURN xs
  }) (xs,l,h,d)"


  lemma introsort_aux_param_refine[refine]: 
    "⟦ (xs',xs)∈cdom_list_rel cparam; (l',l)∈Id; (h',h)∈Id; (d',d)∈Id
    ⟧ ⟹ introsort_aux_param cparam xs' l' h' d' ≤⇓(cdom_list_rel cparam) (WO.introsort_aux4 cparam xs l h d)"
    unfolding introsort_aux_param_def WO.introsort_aux4_def 
    supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"]
    apply (refine_rcg)
    apply refine_dref_type
    apply simp_all 
    done

  definition "introsort_param cparam xs l h ≡ doN {
    ASSERT(l≤h);
    if h-l>1 then doN {
      xs ← introsort_aux_param cparam xs l h (Discrete.log (h-l)*2);
      xs ← final_insertion_sort_param cparam xs l h;
      RETURN xs
    } else RETURN xs
  }"  

  lemma introsort_param_refine: 
    "⟦ (xs',xs)∈cdom_list_rel cparam; (l',l)∈Id; (h',h)∈Id
    ⟧ ⟹ introsort_param cparam xs' l' h' ≤ ⇓(cdom_list_rel cparam) (WO.introsort4 cparam xs l h)"
    unfolding introsort_param_def WO.introsort4_def
    apply (refine_rcg)
    by auto

      
  lemma introsort_param_correct: 
    assumes "(xs',xs)∈Id" "(l',l)∈Id" "(h',h)∈Id"
    shows "introsort_param cparam xs' l' h' ≤ pslice_sort_spec cdom pless cparam xs l h"
  proof -
    note introsort_param_refine
    also note WO.introsort4_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 introsort_param_correct': 
    shows "(PR_CONST introsort_param, PR_CONST (pslice_sort_spec cdom pless)) ∈ Id → Id → Id → Id → ⟨Id⟩nres_rel"
    using introsort_param_correct 
    apply (intro fun_relI nres_relI) 
    by simp
  
    
    
    
end

context parameterized_sort_impl_context begin


sepref_register introsort_aux_param
sepref_def introsort_aux_param_impl is "uncurry4 (PR_CONST introsort_aux_param)" 
  :: "[λ_. True]c cparam_assnk *a (arr_assn)d *a size_assnk *a size_assnk *a size_assnk 
    → arr_assn [λ((((_,ai),_),_),_) r. r=ai]c"
  unfolding introsort_aux_param_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  apply (rewrite RECT_cp_annot[where CP="λ(ai,_,_,_) r. r=ai"])
  by sepref
  
  
sepref_register introsort_param
sepref_def introsort_param_impl is "uncurry3 (PR_CONST introsort_param)" 
  :: "[λ_. True]c cparam_assnk *a (arr_assn)d *a size_assnk *a size_assnk → arr_assn [λ(((_,ai),_),_) r. r=ai]c"
  unfolding introsort_param_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  supply [intro!] = introsort_depth_limit_in_bounds_aux 
  by sepref


lemma introsort_param_impl_correct: "(uncurry3 introsort_param_impl, uncurry3 (PR_CONST (pslice_sort_spec cdom pless)))
        ∈ [λ_. True]c cparam_assnk *a arr_assnd *a snat_assnk *a snat_assnk → arr_assn [λ(((_,ai),_),_) r. r=ai]c"
  using introsort_param_impl.refine[FCOMP introsort_param_correct'] .
  
end



end