Theory Sorting_Final_insertion_Sort

theory Sorting_Final_insertion_Sort
imports Sorting_Quicksort_Scheme Sorting_Unguarded_Insertion_Sort
begin

context weak_ordering begin

  definition "final_insertion_sort xs ≡ doN {
    ASSERT (1 < length xs);
    if length xs ≤ is_threshold then
      gen_insertion_sort True 1 (length xs) xs
    else doN {
      xs ← gen_insertion_sort True 1 is_threshold xs;
      gen_insertion_sort False is_threshold (length xs) xs
    }
  }"  
  
  lemma transfer_guard_over_initial_sorting:
    assumes PS: "part_sorted_wrt (le_by_lt (❙<)) n xs"
    assumes B: "length xs' = length xs" "0<n" "n ≤ i" "i < length xs"
    assumes DEQ: "drop n xs' = drop n xs" 
    assumes SORTED: "sort_spec (❙<) (slice 0 n xs) (slice 0 n xs')" 
    assumes LT: "xs' ! i ❙< xs' ! 0" 
    shows False
  proof -
    from part_sorted_guardedI[OF PS ‹n≤i› ‹i < length xs›] have GUARD: "xs!0 ❙≤ xs!i"
      by (auto simp: le_by_lt)
  
    have [simp]: "xs!i = xs'!i" using B DEQ by (metis atLeastLessThan_iff conv_idxs_to_drop_eq)
      
    have "xs!0 ∈# mset (slice 0 n xs)" using B
      apply (auto simp: Misc.slice_def)
      by (metis atLeast0LessThan image_eqI le_less_trans lessThan_iff less_imp_le_nat nth_image)
    hence "xs!0 ∈# mset (slice 0 n xs')" using SORTED unfolding sort_spec_def by auto 
    then obtain j where "j<n" and [simp]: "xs!0=xs'!j" using B by (auto simp: in_set_conv_nth slice_nth)
    have "xs'!0 ❙≤ xs'!j" using SORTED B ‹j<n›
      apply (cases "j=0")
      apply simp
      unfolding sort_spec_def by (auto simp: le_by_lt sorted_wrt_iff_nth_less slice_nth)
    then show False using LT GUARD
      apply simp
      using local.trans wo_leD by blast
      
  qed
   

  lemma final_insertion_sort_correct: 
    "⟦part_sorted_wrt (le_by_lt (❙<)) is_threshold xs; 1 < length xs⟧ ⟹ final_insertion_sort xs ≤ SPEC (sort_spec (❙<) xs)"
    unfolding final_insertion_sort_def
    apply (refine_vcg gen_insertion_sort_correct[THEN order_trans])
    apply simp_all
    subgoal apply (rule sorted_wrt01) by auto  
    subgoal
      unfolding slice_sort_spec_def apply refine_vcg
      apply (auto simp: ) using slice_complete by metis
    subgoal apply (rule sorted_wrt01) by auto  
    subgoal
      unfolding slice_sort_spec_def 
      apply (refine_vcg gen_insertion_sort_correct[THEN order_trans])
      apply (simp_all)
      subgoal by (simp add: Misc.slice_def sort_spec_def) 
      subgoal for xs'
        apply (clarsimp)
        by (auto intro!: transfer_guard_over_initial_sorting)
      subgoal unfolding slice_sort_spec_def apply refine_vcg
        apply (auto simp: sort_spec_def)
        apply (metis Misc.slice_def append_take_drop_id drop0 drop_take slice_complete union_code)
        by (metis slice_complete)
      done                
    done    
  
  definition "final_insertion_sort2 xs l h ≡ doN {
    ASSERT (l<h);
    if h-l ≤ is_threshold then
      gen_insertion_sort2 True l (l+1) h xs
    else doN {
      xs ← gen_insertion_sort2 True l (l+1) (l+is_threshold) xs;
      gen_insertion_sort2 False l (l+is_threshold) h xs
    }
  }"  
    
  lemma final_insertion_sort2_refine: "⟦(xsi,xs) ∈ slicep_rel l h⟧ 
    ⟹ final_insertion_sort2 xsi l h ≤ ⇓(slice_rel xsi l h) (final_insertion_sort xs)"  
    unfolding final_insertion_sort2_def final_insertion_sort_def
    apply (refine_rcg gen_insertion_sort2_refine)
    apply clarsimp_all
    apply (auto simp: slicep_rel_def idx_shift_rel_def) [7]
    apply (subst slice_rel_rebase, assumption)
    apply (refine_rcg gen_insertion_sort2_refine)
    apply (auto simp: slice_rel_alt idx_shift_rel_def slicep_rel_def)
    done
  
    
    
    
  lemma final_insertion_sort2_correct: 
    assumes [simplified, simp]: "(xs',xs)∈Id" "(l',l)∈Id" "(h',h)∈Id"   
    shows "final_insertion_sort2 xs' l' h' ≤ final_sort_spec xs l h"
  proof (simp,rule le_nofailI)
    assume "nofail (final_sort_spec xs l h)"
    hence PS: "part_sorted_wrt (le_by_lt (❙<)) is_threshold (slice l h xs)"
      and LB: "h-l>1" "h ≤ length xs"
      unfolding final_sort_spec_def slice_sort_spec_def by (auto simp add: refine_pw_simps)
  
    from LB have LENGT1: "1 < length (slice l h xs)" by auto
      
    
    have SLR: "(xs, slice l h xs) ∈ slicep_rel l h" using LB
      by (auto simp: slicep_rel_def)
    
    note final_insertion_sort2_refine[OF SLR]
    also note final_insertion_sort_correct[OF PS LENGT1]
    also note slice_sort_spec_refine_sort'_sym[OF SLR refl refl refl] 
    also have "slice_sort_spec (❙<) xs l h ≤ final_sort_spec xs l h"
      unfolding final_sort_spec_def using PS LB by simp
    finally show "final_insertion_sort2 xs l h ≤ final_sort_spec xs l h" .
  qed
  
  
end
  
context sort_impl_context begin
  sepref_register final_insertion_sort2  
  sepref_def final_insertion_sort_impl is "uncurry2 (PR_CONST final_insertion_sort2)" 
    :: "[λ_. 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 final_insertion_sort2_def PR_CONST_def
    apply (annot_snat_const "TYPE(size_t)")
    by sepref

end

context parameterized_weak_ordering begin  
  definition "final_insertion_sort_param cparam xs l h ≡ doN {
    ASSERT (l<h);
    if h-l ≤ is_threshold then
      gen_insertion_sort_param True cparam l (l+1) h xs
    else doN {
      xs ← gen_insertion_sort_param True cparam l (l+1) (l+is_threshold) xs;
      gen_insertion_sort_param False cparam l (l+is_threshold) h xs
    }
  }"  

  lemma final_insertion_sort_param_refine[refine]: "⟦
    (l',l)∈Id; (h',h)∈Id; (xs',xs)∈cdom_list_rel cparam
  ⟧ ⟹ final_insertion_sort_param cparam xs' l' h' 
    ≤ ⇓(cdom_list_rel cparam) (WO.final_insertion_sort2 cparam xs l h)"  
    unfolding final_insertion_sort_param_def WO.final_insertion_sort2_def
    apply refine_rcg
    apply auto
    done
  
end

context parameterized_sort_impl_context begin

  sepref_register final_insertion_sort_param
  sepref_def final_insertion_sort_param_impl is "uncurry3 (PR_CONST final_insertion_sort_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 final_insertion_sort_param_def PR_CONST_def
    apply (annot_snat_const "TYPE(size_t)")
    by sepref

end


end