Theory Sorting_PDQ

theory Sorting_PDQ
imports Sorting_Setup Sorting_Partially_Sorted Sorting_Pdq_Insertion_Sort Sorting_Heapsort Sorting_Log2
begin

  subsection Auxiliary Definitions


  lemma slice_split_part: "lm  m<h  hlength xs  slice l h xs = slice l m xs @ xs!m # slice (Suc m) h xs"
    by (metis less_imp_le slice_append slice_split_hd)

  
  (* The set properties *)

  context weak_ordering begin
    lemma sorted_wrt_slice_iff_nth_less: " lh; hlength xs   sorted_wrt R (slice l h xs)  (i j. li  i<j  j<h  R (xs!i) (xs!j))"  
      unfolding sorted_wrt_iff_nth_less
      apply (clarsimp simp: slice_nth)      
      apply auto
      by (metis (full_types) diff_add_inverse diff_less_mono le_eq_less_or_eq le_trans nat_le_iff_add)
      

    lemma range_leq_set_slice_conv: 
      "hlength xs  (i{l..<h}. xs!i  pv)  (xset (slice l h xs). xpv)"
      "hlength xs  (i{l..<h}. xs!i  pv)  (xset (slice l h xs). xpv)"
      by (auto simp: set_slice_conv Ball_def)
      
      
  
    text Predicate to express that slice is partitioned              
    definition "partitioned pv xs l h m  
          lm  m<h  hlength xs
         (i{l..<m}. xs!i  pv)
         xs!m = pv 
         (i{m<..<h}. xs!i  pv)"

    lemma partitioned_alt: "partitioned pv xs l h m  
          lm  m<h  hlength xs
         (xset (slice l m xs). x  pv)
         xs!m = pv 
         (xset (slice (m+1) h xs). x  pv)"    
      unfolding partitioned_def
      apply (rule iffI)
      subgoal by (auto simp: in_set_conv_nth slice_nth) []
      subgoal by (auto simp: range_leq_set_slice_conv[symmetric])
      done


    text Shuffling a partition does not change partitioned property            
    lemma shuffle_pres_part:
      "partitioned pv xs1 l h m  slice_eq_mset l m xs1 xs2  partitioned pv xs2 l h m"  
      "partitioned pv xs1 l h m  slice_eq_mset (Suc m) h xs1 xs2  partitioned pv xs2 l h m"
      unfolding partitioned_alt
      (* TODO: Clean up proof *)
      apply (clarsimp_all simp: slice_eq_mset_alt )
      apply (clarsimp_all simp: slice_eq_mset_eq_length eq_outside_range_nth slice_eq_outside_range dest: mset_eq_setD)
      apply (clarsimp_all simp: slice_eq_mset_alt )
      apply (auto simp:  eq_outside_range_nth slice_eq_outside_range dest: mset_eq_setD)
      done
      

    text After sorting the partitions, the whole slice is sorted.  
    lemma parts_sorted_imp_sorted:
      assumes "partitioned pv xs l h m"
      assumes "sorted_wrt_lt (<) (slice l m xs)"
      assumes "sorted_wrt_lt (<) (slice (Suc m) h xs)"
      shows "sorted_wrt_lt (<) (slice l h xs)"
      using assms
      unfolding partitioned_def
      apply (clarsimp simp: slice_nth le_by_lt sorted_wrt_slice_iff_nth_less)
      by (metis (no_types, lifting) Suc_leI atLeastLessThan_iff greaterThanLessThan_iff linorder_neqE_nat local.trans)
      
            
  end    

  (*
    Configuration options for Pdqsort
  *)    
  abbreviation "is_threshold  16::nat"  (* TODO/FIXME: replace by pdq_is_threshold, and remove *)
  abbreviation "pdq_is_threshold  24"
    
  abbreviation "ninther_threshold  128::nat"

  context weak_ordering begin
    subsection Phases of Quicksort Scheme
    
    definition "part_range_cond xs l h  (
          i{l+1..<h}. xs!i  xs!l)
         (i{l+1..<h}. xs!i  xs!l)"

    text Pivot has been selected and moved to front      
    definition "R_PV_TO_FRONT l h xs xs'  l+1<h  hlength xs  slice_eq_mset l h xs xs'  part_range_cond xs' l h"
    
    text Slice has been partitioned
    definition "R_PART pv l h m xs xs'  lm  m<h  hlength xs  slice_eq_mset l h xs xs'  partitioned pv xs' l h m"

    text Left partition has been sorted    
    definition "R_SORT_L pv l h m xs xs'  R_PART pv l h m xs xs'  sorted_wrt_lt (<) (slice l m xs')"
    
    text Right partition has been sorted
    definition "R_SORT_R pv l h m xs xs'  R_SORT_L pv l h m xs xs'  sorted_wrt_lt (<) (slice (Suc m) h xs')"

    text When right partition has been sorted, the whole slice is already sorted.   
    lemma R_SORT_R_sorted: "R_SORT_R pv l h m xs xs'  slice_eq_mset l h xs xs'  sorted_wrt_lt (<) (slice l h xs')"
      unfolding R_SORT_R_def R_SORT_L_def R_PART_def
      by (auto simp: parts_sorted_imp_sorted)

    text Sorting the whole partition, e.g., due to heapsort fallback      
    lemma R_PART_SORT: "R_PART pv l h m xs xs'  slice_sort_spec (<) xs' l h  SPEC (λxs''. slice_eq_mset l h xs xs''  sorted_wrt_lt (<) (slice l h xs''))"  
      unfolding slice_sort_spec_sem_alt R_PART_def
      apply refine_vcg
      apply (auto simp: slice_eq_mset_eq_length dest: slice_eq_mset_trans)
      done

      
    subsection Specifications of Subroutines
      

    text Move pivot to front          
    definition "pivot_to_front_spec xs l h  doN {
      ASSERT (l + 4 < h  h  length xs);
      SPEC (λxs'. 
          slice_eq_mset l h xs xs'
         part_range_cond xs' l h
      )
    }"

    lemma pivot_to_front_spec_rl: " l + 4 < h; hlength xs   pivot_to_front_spec xs l h  SPEC (λxs'. R_PV_TO_FRONT l h xs xs')"
      unfolding pivot_to_front_spec_def R_PV_TO_FRONT_def
      by auto

    text Partition          
    definition "partition_spec xs l h  doN {
      ASSERT ( 
          l + 1 < h  h  length xs 
         part_range_cond xs l h
      );
      SPEC (λ(alrp::bool,m,xs'). 
          slice_eq_mset l h xs xs'
         lm  m<h
         partitioned (xs!l) xs' l h m
      )
    }"

    definition "partition_left_spec  partition_spec" (* No discrimination required on this abs-level *)
    
    lemma partition_spec_rl: "R_PV_TO_FRONT l h xs0 xs  partition_spec xs l h  SPEC (λ(_,m,xs'). m<h  R_PART (xs!l) l h m xs0 xs')"
      unfolding partition_spec_def R_PV_TO_FRONT_def R_PART_def 
      apply refine_vcg 
      by (auto simp: slice_eq_mset_eq_length dest: slice_eq_mset_trans)
    
      
    lemma aux1: 
      assumes BOUNDS: "l  m" "m < h" "h  length xs'"
      assumes NOT_LESS: "¬ prev < pv"
      assumes PART: "partitioned pv xs' l h m"
      assumes LPART: "xset (slice l h xs'). prev  x"
      shows "
       0 < l; part_range_cond xs l h; slice_eq_mset l h xs xs' 
        sorted_wrt_lt (<) (slice l m xs')"  
    proof -
    
      from NOT_LESS have "pv  prev" using wo_leI by blast
    
      from PART have LEFT_PART_LE: "i{l..<m}. xs'!i  pv"
        unfolding partitioned_def by auto
      
      from LPART have PREV_LE: "i{l..<h}. prev  xs'!i"
        using assms(3) range_leq_set_slice_conv(2) by blast
        
      {
        fix i j
        assume "li" "i<j" "j<m"
        hence "xs'!i  xs'!j"
        by (meson LEFT_PART_LE PREV_LE pv  prev assms(2) atLeastLessThan_iff le_less_trans less_imp_le_nat local.trans)
      }
      then show "sorted_wrt_lt (<) (slice l m xs')"
        using BOUNDS
        by (auto simp: sorted_wrt_slice_iff_nth_less le_by_lt)
    qed    
    
    text Correctness lemma for the partition-left optimization for many equal elements.      
    lemma partition_left_spec_rl: "R_PV_TO_FRONT l h xs0 xs; 0<l; ¬(xs!(l-1) < xs!l); (xset (slice l h xs0). xs0!(l-1)  x)  
       partition_left_spec xs l h  SPEC (λ(_,m,xs'). m<h  R_SORT_L (xs!l) l h m xs0 xs')"
      unfolding partition_spec_def partition_left_spec_def R_PV_TO_FRONT_def R_PART_def R_SORT_L_def
      apply refine_vcg 
      apply (auto simp: slice_eq_mset_eq_length slice_eq_mset_nth_outside slice_eq_mset_set_inside aux1 dest: slice_eq_mset_trans)
      done

    text Shuffle. We only specify that the partitions must contain the same elements.        
    definition "shuffle_spec xs l h m  doN {
      ASSERT (lm  m<h  hlength xs);
      SPEC (λ(unbal,xs'). 
        eq_outside_range xs xs' l h
       mset (slice l m xs) = mset (slice l m xs')  
       xs!m = xs'!m
       mset (slice (m+1) h xs) = mset (slice (m+1) h xs')  
      )
    }"

    lemma shuffle_rule: "R_PART pv l h m xs0 xs  shuffle_spec xs l h m  SPEC (λ(_,xs'). R_PART pv l h m xs0 xs')"
      unfolding R_PART_def shuffle_spec_def partitioned_alt
      apply refine_vcg
      apply (auto simp: slice_eq_mset_alt eq_outside_rane_lenD dest: mset_eq_setD)
      apply (simp add: slice_eq_mset_alt eq_outside_range_def)
      subgoal for xs2 
        apply (rewrite in " = _" slice_split_part; simp add: eq_outside_rane_lenD)
        apply (rewrite in "_ = " slice_split_part; simp add: eq_outside_rane_lenD)
        done
      done

    text Maybe-Sort: The specification nondeterministically decides whether to sort or not. 
      In any case, the elements are permutated.
              
    lemma maybe_sort_rule1: "R_PART pv l h m xs0 xs  maybe_sort_spec xs l m 
       SPEC (λ(r,xs'). (rR_SORT_L pv l h m xs0 xs')  R_PART pv l h m xs0 xs')"
      unfolding maybe_sort_spec_def R_PART_def R_SORT_L_def
      apply (refine_vcg)
      apply (clarsimp_all simp: slice_eq_mset_eq_length)
      subgoal by (meson eq_imp_le less_imp_le slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal using shuffle_pres_part(1) by blast
      subgoal by (meson less_or_eq_imp_le slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal using shuffle_pres_part(1) by blast
      done

      
    lemma maybe_sort_rule2: "R_SORT_L pv l h m xs0 xs  maybe_sort_spec xs (Suc m) h 
       SPEC (λ(r,xs'). (rR_SORT_R pv l h m xs0 xs')  (¬r  R_SORT_L pv l h m xs0 xs'))"
      unfolding maybe_sort_spec_def R_PART_def  R_SORT_L_def R_SORT_R_def
      apply (refine_vcg)
      apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
      subgoal
        by (meson le_SucI nat_in_between_eq(2) order.strict_implies_order slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal
        using shuffle_pres_part(2) by blast 
      subgoal
        by (meson le_SucI le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans) 
      subgoal
        using shuffle_pres_part(2) by blast 
      done
    
    lemma sort_rule1: "R_PART pv l h m xs0 xs  slice_sort_spec (<) xs l m
       SPEC (λxs'. R_SORT_L pv l h m xs0 xs')"
      unfolding slice_sort_spec_sem_alt R_PART_def  R_SORT_L_def R_SORT_R_def
      apply (refine_vcg)
      apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
      subgoal by (meson le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal using shuffle_pres_part(1) by blast
      done

      
    lemma sort_again_rule1: "R_SORT_L pv l h m xs0 xs  slice_sort_spec (<) xs l m
       SPEC (λxs'. R_SORT_L pv l h m xs0 xs')"
      unfolding slice_sort_spec_sem_alt R_PART_def  R_SORT_L_def R_SORT_R_def
      apply (refine_vcg)
      apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
      subgoal by (meson le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal using shuffle_pres_part(1) by blast
      done
            
    lemma sort_rule2: "R_SORT_L pv l h m xs0 xs  slice_sort_spec (<) xs (Suc m) h
       SPEC (λxs'. R_SORT_R pv l h m xs0 xs')"
      unfolding slice_sort_spec_sem_alt R_PART_def R_SORT_L_def R_SORT_R_def
      apply (refine_vcg)
      apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
      subgoal by (meson le_Suc_eq less_imp_le_nat nat_in_between_eq(2) slice_eq_mset_subslice slice_eq_mset_trans)
      subgoal using shuffle_pres_part(2) by blast
      done
            
      
    text Fallback sorting. Will be instantiated by Heapsort later.  
    definition "fallback_sort_spec  slice_sort_spec (<)"      
      

    subsection Abstract Pdqsort          
    text Recursive Pdqsort function.
    definition "pdqsort_aux leftmost xs l h (d::nat)  RECT (λpdqsort_aux (leftmost,xs,l,h,d). doN {
      ASSERT (lh  hlength xs  0<d);
      ASSERT (¬leftmost  l>0  (xset (slice l h xs). xs!(l-1)  x));
      
      if (h-l < pdq_is_threshold) then 
        pdq_guarded_sort_spec leftmost xs l h
      else doN {
        xs  pivot_to_front_spec xs l h;

        ASSERT (l-1<length xs  l<length xs);
        ASSERT (¬leftmost  l>0);         
        if (¬leftmost  ¬(xs!(l-1) < xs!l)) then doN {
          (_,m,xs)  partition_left_spec xs l h;
          ASSERT (m<h);
          pdqsort_aux (False,xs,m+1,h,d)
        } else doN {
          (alrp,m,xs)  partition_spec xs l h;
          (unbal,xs)  shuffle_spec xs l h m;
          
          ASSERT (0<d);
          let d = (if unbal then d-1 else d);
          
          (didsort,xs)  
            if d=0 then doN {xs  fallback_sort_spec xs l h; RETURN (True,xs)}
            else if alrp  ¬unbal then doN {
              (r,xs)  maybe_sort_spec xs l m;
              if r then doN {
                ASSERT (m<h);
                maybe_sort_spec xs (m+1) h
              } else RETURN (False,xs)
            } else RETURN (False,xs);
            
          if didsort then RETURN xs 
          else doN { ⌦‹TODO: Test optimization of not sorting left partition again, if maybe_sort sorted it›
            xs  pdqsort_aux (leftmost,xs,l,m,d);
            ASSERT (m<h);
            xs  pdqsort_aux (False,xs,m+1,h,d);
            RETURN xs
          } 
        }
      }
    
    }) (leftmost,xs,l,h,d)"
    

    (*
      The correctness proof is some manual fiddling with the VCG, 
      but essentially uses the lemmas proved above.
    *)    
    lemma pdqsort_aux_correct:
      assumes "lh" "hlength xs" "¬leftmost  l>0  (xset (slice l h xs). xs!(l-1)  x)" "d>0"  
      shows "pdqsort_aux leftmost xs l h d  slice_sort_spec (<) xs l h"
      unfolding pdqsort_aux_def fallback_sort_spec_def
      
      apply (rule order_trans)
      apply (rule RECT_rule[where 
            V="measure (λ(leftmost,xs,l,h,d). h-l)" 
        and pre="λ(leftmost,xs,l,h,d). lh  hlength xs  0<d  (¬leftmost  l>0  (xset (slice l h xs). xs!(l-1)  x))"
        and M="λ(leftmost,xs,l,h,d). slice_sort_spec (<) xs l h"
        ], refine_mono)

              
      subgoal by simp  
      subgoal using assms by auto
      subgoal premises prems for pdqsort args proof -
      
        obtain leftmost xs l h d where [simp]: "args = (leftmost, xs, l, h, d)" by (cases args)
      
        note IH = prems(1)
        note LEFTMOST = prems(2)
      
        {
          fix pv m xs xs' and d'::nat
          assume "R_SORT_L pv l h m xs xs'" and "0<d'"
          hence "pdqsort (False,xs',Suc m,h,d')  SPEC (λxs''. R_SORT_R pv l h m xs xs'')"
            apply -
            apply (rule order_trans[OF IH])
            subgoal by (simp add: R_SORT_L_def R_PART_def partitioned_alt)
            subgoal by (auto simp add: R_SORT_L_def R_PART_def partitioned_alt)
            subgoal by (simp add: sort_rule2)
            done
        } note rec_sort_r_rl = this
        
        {
          fix pv m xs' and d'::nat
          assume "R_PART pv l h m xs xs'" and "0<d'"
          hence "pdqsort (leftmost,xs',l,m,d')  SPEC (λxs''. R_SORT_L pv l h m xs xs'')"
            apply -
            apply (rule order_trans[OF IH])
            subgoal using LEFTMOST 
              apply (clarsimp simp: R_PART_def slice_eq_mset_eq_length slice_eq_mset_nth_outside slice_eq_mset_set_inside) 
              apply (drule set_rev_mp[OF _ set_slice_subsetI, of _ l m _ l h])
              by auto
            subgoal by (auto simp add: R_SORT_L_def R_PART_def partitioned_alt)
            subgoal by (simp add: sort_rule1)
            done
        } note rec_sort_l_rl = this
        
        {
          fix pv m xs' and d'::nat
          assume "R_SORT_L pv l h m xs xs'" and "0<d'"
          hence "pdqsort (leftmost,xs',l,m,d')  SPEC (λxs''. R_SORT_L pv l h m xs xs'')"
          using rec_sort_l_rl unfolding R_SORT_L_def by blast
        } note rec_sort_l_again_rl = this
              
        
        show ?thesis
          apply (rewrite in "_" slice_sort_spec_sem_alt)
          apply (cases args,simp)
          apply (refine_vcg pivot_to_front_spec_rl partition_spec_rl partition_left_spec_rl shuffle_rule; assumption?)
          using LEFTMOST
          apply (clarsimp_all simp: slice_eq_mset_eq_length eq_outside_rane_lenD)
          apply (all assumption?)
          subgoal 
            apply (simp add: slice_sort_spec_sem_alt pdq_guarded_sort_spec_def)
            apply refine_vcg
            by (auto simp: unfold_le_to_lt)
          subgoal by simp
          subgoal unfolding R_PV_TO_FRONT_def by (auto simp: slice_eq_mset_eq_length)
          subgoal unfolding R_PV_TO_FRONT_def by (auto simp: slice_eq_mset_eq_length)
          subgoal 
            apply (refine_vcg rec_sort_r_rl, assumption)
            by (clarsimp_all simp: R_SORT_R_sorted)
          subgoal by (simp add: R_PART_SORT)
          subgoal
            apply (all erule maybe_sort_rule1[THEN order_trans])
            apply (all refine_vcg)
            apply clarsimp_all
            apply (all (erule maybe_sort_rule2[THEN order_trans])?)
            apply (all (refine_vcg)?)
            apply (clarsimp_all simp: R_SORT_R_sorted)
            subgoal
              apply (refine_vcg rec_sort_l_again_rl, assumption)
              apply (refine_vcg rec_sort_r_rl, assumption)
              by (clarsimp_all simp: R_SORT_R_sorted)
            subgoal
              apply (refine_vcg rec_sort_l_rl, assumption)
              apply (refine_vcg rec_sort_r_rl, assumption)
              by (clarsimp_all simp: R_SORT_R_sorted)
            done
          subgoal
            apply (intro conjI impI)  
            subgoal
              apply (refine_vcg rec_sort_l_rl, assumption, simp)
              apply (refine_vcg rec_sort_r_rl, assumption, simp)
              by (clarsimp_all simp: R_SORT_R_sorted)
            subgoal
              apply (refine_vcg rec_sort_l_rl, assumption)
              apply (refine_vcg rec_sort_r_rl, assumption)
              by (clarsimp_all simp: R_SORT_R_sorted)
            done
          done
      qed
      subgoal by simp
      done      
      

    text Main Pdqsort function. Just a wrapper for the recursive function, 
      initializing the maximum number of bad partitions before switching to fallback sorting.        
    definition "pdqsort xs l h  doN {
      ASSERT (lh);
      let size = h-l;
      if (size>1) then pdqsort_aux True xs l h (Discrete.log size)
      else RETURN xs
    }"  
      
    lemma pdqsort_correct: "pdqsort xs l h  slice_sort_spec (<) xs l h"
    proof -
      have log_pos_aux: "1<x  0 < Discrete.log x" for x
        apply (subst log_rec) by auto 
        
      {
        assume "lh" "hlength xs"
        hence ?thesis
          unfolding pdqsort_def
          apply (cases "1 < h-l"; simp)
          subgoal by (rule pdqsort_aux_correct; simp add: log_pos_aux)
          subgoal unfolding slice_sort_spec_def sort_spec_def by refine_vcg (auto simp: sorted_wrt01)
          done
      } thus ?thesis unfolding slice_sort_spec_def by (simp only: pw_le_iff refine_pw_simps) blast
    qed    
      
    
    subsection Implementation of Subroutines
    
    
    definition "sort_two xs i j  doN {
      ASSERT (i<length xs  j<length xs  ij);
      ifN mop_cmp_idxs xs j i then mop_list_swap xs i j else RETURN xs
      
      ⌦‹if (xs!j < xs!i) then mop_list_swap xs i j else RETURN xs›
    }"              
    
    definition "sort_three xs i j k  doN {
      xs  sort_two xs i j;
      xs  sort_two xs j k;
      xs  sort_two xs i j;
      RETURN xs
    }"              

    lemma sort_three_rule: "
      {i,j,k}{l..<h}; ij; ik; jk; hlength xs
      sort_three xs i j k  SPEC (λxs'. slice_eq_mset l h xs xs'  xs'!i  xs'!j  xs'!j  xs'!k  (l-{i,j,k}. xs!l=xs'!l))"
      unfolding sort_three_def sort_two_def
      apply simp
      apply (simp add: swap_nth unfold_le_to_lt split: if_splits)
      apply (simp add: unfold_lt_to_le)
      done
      
    
    definition "three_sorted xs i j k  {i,j,k}  {0..<length xs}  xs!i  xs!j  xs!j  xs!k"

    lemma sort_three_sorted_rl: "sort_three xs1 i j k  SPEC (λxs2. length xs1=length xs2  slice_eq_mset l h xs1 xs2  three_sorted xs2 i j k)"  
      if "{i,j,k}{l..<h}" "ij" "ik" "jk" "l<h" "hlength xs1" for i j k and xs1 xs2 :: "'a list"
      using that
      apply (refine_vcg sort_three_rule[where l=l and h=h])
      apply (auto simp: slice_eq_mset_eq_length three_sorted_def)
      done
    
        
    lemma three_sorted_imp_part_range_cond: " three_sorted xs i l k; l<i; l<k; i<h; k<h   part_range_cond xs l h"
      unfolding three_sorted_def part_range_cond_def by auto

    lemma three_sorted_swap_imp_part_range_cond: " three_sorted xs i j k; ij; jk; l<i; l<j; l<k; i<h; j<h; k<h; hlength xs   part_range_cond (swap xs l j) l h"
      unfolding three_sorted_def part_range_cond_def by (auto simp: swap_nth)
          
                  
    definition "move_pivot_to_front xs l h  doN {
      ASSERT (lh  h>0);
      let size = h-l;
      let s2 = size div 2;

      if (size > ninther_threshold) then doN {
        ⌦‹ASSERT (l+s2+1<h ∧ h≥3 ∧ s2≥1 ∧ s2<h );›
        xssort_three xs l              (l + s2)       (h - 1);
        xssort_three xs (l + 1)        (l + (s2 - 1)) (h - 2);
        xssort_three xs (l + 2)        (l + (s2 + 1)) (h - 3);
        xssort_three xs (l + (s2 - 1)) (l + s2)       (l + (s2 + 1));
        xs  mop_list_swap xs l (l+s2);
        ⌦‹ASSERT (xs!l  xs!(l + (s2 + 1)) ∧ xs!(l + (s2 - 1))  xs!l);›
        RETURN xs
      } else doN {
        ⌦‹ASSERT (l+s2 ≠ h-1 ∧ l+s2<h ∧ h>0);›
        sort_three xs (l+s2) l (h-1)
      }
    }"
    
    
    lemma move_pivot_to_front_refine: "move_pivot_to_front xs l h  pivot_to_front_spec xs l h"
      unfolding move_pivot_to_front_def pivot_to_front_spec_def
      apply (refine_vcg sort_three_sorted_rl[where l=l and h=h]) 
      apply (all elim conjE; assumption?)
      supply [[linarith_split_limit = 15]]
      apply simp_all
      subgoal by (auto)
      subgoal by (auto)
      subgoal by (auto)
      subgoal by (auto)
      subgoal by (metis slice_eq_mset_trans)
      subgoal by (erule three_sorted_swap_imp_part_range_cond) auto
      subgoal by (auto)
      subgoal by (erule three_sorted_imp_part_range_cond; auto)
      done    

      
      
    definition "shuffle_left xs i j  doN {ASSERT (ij); mop_list_swap xs i j}"  
    definition "shuffle_right xs i j  doN {ASSERT (ij); mop_list_swap xs i j}"  
      
    definition "shuffle xs l h m  doN {
      ASSERT (lh  lm  m+1h);
      let size = h-l;
      let l_size = m-l;
      let r_size = h - (m+1);
      let highly_unbal = l_size < size div 8  r_size < size div 8;
    
      if highly_unbal then doN {
        xs  if l_size  is_threshold then doN {  ⌦‹FIXME: This should be pdq_is_threshold!›
⌦‹          ASSERT (l + l_size div 4 < h ∧ m>0 ∧ m≥l_size div 4);
›          xs  shuffle_left xs l (l+l_size div 4);
          xs  shuffle_left xs (m-1) (m - l_size div 4);
          
          if l_size > ninther_threshold then doN {
⌦‹            ASSERT (
                l+1≤h ∧ l_size div 4 + 1≤h ∧ l + (l_size div 4 + 1)≤h 
              ∧ l+2≤h ∧ l_size div 4 + 2≤h ∧ l + (l_size div 4 + 2)≤h
              ∧ m≥2 ∧ m≥3 ∧ m≥l_size div 4 + 1 ∧ m≥l_size div 4 + 2);
›            
            xs  shuffle_left xs (l + 1) (l + (l_size div 4 + 1));
            xs  shuffle_left xs (l + 2) (l + (l_size div 4 + 2));
            xs  shuffle_left xs (m - 2) (m - (l_size div 4 + 1));
            xs  shuffle_left xs (m - 3) (m - (l_size div 4 + 2));
            RETURN xs
          } else RETURN xs
        } else RETURN xs;
        xs  if r_size  is_threshold then doN {  ⌦‹FIXME: This should be pdq_is_threshold!›
 ⌦‹         ASSERT (m+1≤h ∧ m + 1 + r_size div 4≤h ∧ h≥1 ∧ h≥r_size div 4);
 ›         xs  shuffle_right xs (m+1) (m + 1 + r_size div 4);
          xs  shuffle_right xs (h-1) (h - r_size div 4);
          if r_size > ninther_threshold then doN {
  ⌦‹          ASSERT (m+2≤h ∧ 1 + r_size div 4≤h ∧ 2 + r_size div 4≤h ∧ 3 + r_size div 4≤h 
                  ∧ h≥2 ∧ h≥3 ∧ h≥(1 + r_size div 4) ∧ h≥(2 + r_size div 4) );
  ›          xs  shuffle_right xs (m + 2) (m + (2 + r_size div 4));
            xs  shuffle_right xs (m + 3) (m + (3 + r_size div 4));
            xs  shuffle_right xs (h - 2) (h - (1 + r_size div 4));  
            xs  shuffle_right xs (h - 3) (h - (2 + r_size div 4));          
            RETURN xs
          } else RETURN xs
        } else RETURN xs;
        RETURN (True,xs)
      } else
        RETURN (False,xs)
    }"
      
    definition "shuffled l h m xs xs'          
        lm  m<h  hlength xs 
       eq_outside_range xs xs' l h
       mset (slice l m xs) = mset (slice l m xs')  
       xs!m = xs'!m
       mset (slice (m+1) h xs) = mset (slice (m+1) h xs')"
    
      
    lemma eq_outside_range_swap: "{i,j}{l..<h}  eq_outside_range xs (swap xs' i j) l h = eq_outside_range xs xs' l h"  
      by (auto simp: eq_outside_range_def)
    
      
    lemma shuffled_left: " {i,j}{l..<m}; shuffled l h m xs xs'   shuffled l h m xs (swap xs' i j)"  
      unfolding shuffled_def
      by (auto simp: eq_outside_range_swap slice_swap eq_outside_rane_lenD slice_swap_outside)
      
    lemma shuffled_right: " {i,j}{Suc m..<h}; shuffled l h m xs xs'   shuffled l h m xs (swap xs' i j)"  
      unfolding shuffled_def
      by (auto simp: eq_outside_range_swap slice_swap eq_outside_rane_lenD slice_swap_outside)
      
    lemma shuffle_spec_alt: "shuffle_spec xs l h m = doN {ASSERT (lm  m<h  hlength xs); SPEC (λ(_,xs'). shuffled l h m xs xs')}"  
      unfolding shuffle_spec_def shuffled_def by (auto simp: pw_eq_iff refine_pw_simps)
      
    lemma shuffled_refl: "shuffled l h m xs xs  lm  m<h  hlength xs"   
      by (auto simp: shuffled_def eq_outside_range_triv)
      
    lemma shuffle_left_rl: "shuffled l h m xs xs'  ij  {i,j}{l..<m}  shuffle_left xs' i j  SPEC (λxs''. shuffled l h m xs xs'')"  
      unfolding shuffle_left_def
      apply refine_vcg
      apply (simp_all add: shuffled_left)
      by (auto simp: shuffled_def eq_outside_rane_lenD)
      
    lemma shuffle_right_rl: "shuffled l h m xs xs'  ij  {i,j}{Suc m..<h}  shuffle_right xs' i j  SPEC (λxs''. shuffled l h m xs xs'')"  
      unfolding shuffle_right_def
      apply refine_vcg
      apply (simp_all add: shuffled_right)
      by (auto simp: shuffled_def eq_outside_rane_lenD)
      
      
    
    lemma shuffle_correct: "shuffle xs l h m  shuffle_spec xs l h m"       
      unfolding shuffle_spec_alt
      apply (refine_vcg)
      unfolding shuffle_def
      apply (subgoal_tac "shuffled l h m xs xs")
      apply refine_vcg
      apply (simp_all add: shuffled_refl)
      apply (all (thin_tac "m-l < _  _")?)

      (* TODO: The splitter is probably getting in the way here! *)
      subgoal
        apply (refine_vcg shuffle_left_rl; assumption?) 
        apply (simp_all add: shuffled_refl)
        supply [[linarith_split_limit = 25]]
        apply auto [6]
        apply (refine_vcg shuffle_right_rl; assumption?) 
        apply (simp_all add: shuffled_refl)
        apply auto [6]
        apply (refine_vcg shuffle_right_rl; assumption?) 
        apply (simp_all)
        apply auto
        done
      subgoal  
        apply (refine_vcg shuffle_right_rl; assumption?) 
        apply (simp_all add: shuffled_refl)
        apply auto
        done      
      done  
    
    
      
    text 
      Some definitions to hide away propositions that would overwhelm the linarith-solver of the simplifier.
      
    (*
      Elements in between l<..i are smaller than pivot.
        * at beginning of loop, will be i-1, 
        * after swapping, will be i
    *)  
    definition "AUX_SMALLER C l h xs i  l<h  hlength xs  li  i<h  (k{l<..i}. C (xs!k) (xs!l))"  
    
    (*
      Elements in between j..<h are not smaller than pivot
      
      * at beginning of loop, will be j+1
      * after swapping, will be j
    *)
    definition "AUX_NOTSM C l h xs j    l<h  hlength xs  l<j  jh  (k{j..<h}. C (xs!k) (xs!l))"
    
    
    definition "RIGHT_GUARD C l h xs i  l<h  hlength xs  (k{i<..<h}. ¬ C (xs!k) (xs!l))"
    
    definition "LEFT_GUARD C l xs j  l<length xs  (k{l<..<j}. ¬ C (xs!k) (xs!l))"
    

    lemma AUX_SMALLER_init: " l<h; hlength xs   AUX_SMALLER C l h xs l"
      unfolding AUX_SMALLER_def by auto
        
    lemma AUX_NOTSM_init: "l<h; hlength xs  AUX_NOTSM C l h xs h"  
      unfolding AUX_NOTSM_def by auto

    lemma RIGHT_GUARD_from_prc: "part_range_cond xs l h  l<h  hlength xs  RIGHT_GUARD (<) l h xs l"  
      unfolding part_range_cond_def RIGHT_GUARD_def
      by (auto simp: unfold_le_to_lt)

    lemma LEFT_GUARD_from_prc: "part_range_cond xs l h  l<h  hlength xs  LEFT_GUARD (>) l xs h"  
      unfolding part_range_cond_def LEFT_GUARD_def
      by (auto simp: unfold_le_to_lt)
      
            
    lemma LEFT_GUARD_init: "AUX_SMALLER (Not oo C) l h xs (i - Suc 0); l < i;  Suc l < j0; i  Suc l  LEFT_GUARD C l xs j0"        
      unfolding AUX_SMALLER_def LEFT_GUARD_def
      by fastforce 
    
    lemma RIGHT_GUARD_init: " AUX_NOTSM (Not ∘∘ C) l h xs (Suc j); AUX_SMALLER C l h xs i0; Suc j  h  RIGHT_GUARD C l h xs i0"        
      unfolding AUX_NOTSM_def RIGHT_GUARD_def AUX_SMALLER_def
      by fastforce 
            
    
    lemma PV_SWAP:
      assumes "AUX_SMALLER C l h xs (i-1)" "AUX_NOTSM (Not oo C) l h xs (j+1)"
      assumes "l<i" "i<j" "¬ C(xs!i) (xs!l)" "C (xs!j) (xs!l)"
      shows "AUX_SMALLER C l h (swap xs i j) i" "AUX_NOTSM (Not oo C) l h (swap xs i j) j"
      using assms
      unfolding AUX_SMALLER_def AUX_NOTSM_def
      by (auto simp: swap_nth)
      
          
    lemma PARTITIONED_FINALLY: "¬(i<j)  ¬xs!i<xs!l  AUX_SMALLER (<) l h xs (i-1)  AUX_NOTSM (Not oo (<)) l h xs (j+1)  partitioned (xs!l) (swap xs l (i-Suc 0)) l h (i-Suc 0)"
      unfolding partitioned_def AUX_SMALLER_def AUX_NOTSM_def
      apply (auto simp: swap_nth unfold_lt_to_le)
      apply (metis Suc_leI atLeastLessThan_iff connex leD le_less_linear le_neq_implies_less le_trans nat_le_Suc_less_imp)
      by (metis atLeastLessThan_iff connex leD leI le_neq_implies_less le_trans nat_le_Suc_less_imp not_less_eq_eq)

    lemma PARTITIONED_FINALLY2: "¬(i<j)  ¬ xs!j>xs!l  AUX_SMALLER (Not oo (>)) l h xs (i-1)  AUX_NOTSM (>) l h xs (j+1)  partitioned (xs!l) (swap xs l j) l h j"
      unfolding partitioned_def AUX_SMALLER_def AUX_NOTSM_def
      apply (simp add: unfold_lt_to_le swap_nth; safe; simp)
      subgoal using connex by blast
      subgoal by (meson connex dual_order.order_iff_strict greaterThanAtMost_iff leI less_le_trans nat_le_Suc_less_imp)
      subgoal by (meson connex dual_order.order_iff_strict greaterThanAtMost_iff leI less_le_trans nat_le_Suc_less_imp)
      done
      
          
    definition "mop_C_idx C xs i j  doN { ASSERT (i<length xs  j<length xs); RETURN (C (xs!i) (xs!j)) }"           
        

    definition "find_next_unguarded C xs l h i0  doN {
      ASSERT(l<length xs  li0  i0<h  hlength xs  (si{i0<..<h}. ¬ C (xs!si) (xs!l)) );
      monadic_WHILEIT (λi. i0<i  i<h  (j{i0<..<i}. C (xs!j) (xs!l))) 
        (λi. doN { ASSERT (il); mop_C_idx C xs i l } ) 
        (λi. doN { ASSERT (i<h); RETURN (i+1)}) 
        (i0 + 1)
    }"  

    definition "find_next_guarded C xs l h i0  doN {
      ASSERT(l<length xs  li0  i0<h  hlength xs );
      monadic_WHILEIT (λi. i0<i  i<h  (j{i0<..<i}. C (xs!j) (xs!l))) 
        (λi. if i < h - 1 then doN { ASSERT (il); mop_C_idx C xs i l } else RETURN False) 
        (λi. doN { ASSERT (i<h); RETURN (i+1)}) 
        (i0 + 1)
    }"  

    definition "first_find_next C xs l j h i0  doN {
      ASSERT (j<h);    
      if j+1=h then find_next_guarded C xs l h i0
      else find_next_unguarded C xs l h i0
    }"  
    
        
    definition "find_prev_unguarded C xs l j0  doN {
      ASSERT(l<length xs  l+1<j0  j0length xs  (si{l<..<j0}. ¬C (xs!si) (xs!l))  j01 );
      monadic_WHILEIT (λj. l<j  j<j0  (k{j<..<j0}. C (xs!k) (xs!l))) 
        (λj. mop_C_idx C xs j l) 
        (λj. doN {ASSERT(j1); RETURN (j-1)}) 
        (j0 - 1)
    }"  
      
    definition "find_prev_guarded C xs l j0  doN {
      ASSERT(l<length xs  l+1<j0  j0length xs  j01 );
      monadic_WHILEIT (λj. l<j  j<j0  (k{j<..<j0}. C (xs!k) (xs!l))) 
        (λj. if l+1<j then mop_C_idx C xs j l else RETURN False ) 
        (λj. doN {ASSERT(j1); RETURN (j-1)}) 
        (j0 - 1)
    }"  
    
    definition "first_find_prev C xs l i h  doN {
      ASSERT (l<h);
      if i=l+1 then find_prev_guarded C xs l h
      else find_prev_unguarded C xs l h
    }"  

           
    lemma find_next_unguarded_rl: " AUX_SMALLER C l h xs i0; RIGHT_GUARD C l h xs i0 
       find_next_unguarded C xs l h i0  SPEC (λi. i0<i  i<h  AUX_SMALLER C l h xs (i-1)  ¬C (xs!i) (xs!l) )"  
      unfolding find_next_unguarded_def AUX_SMALLER_def RIGHT_GUARD_def mop_C_idx_def
      apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. length xs - i)"])
      apply clarsimp_all
      subgoal 
        apply safe
        apply simp_all
        subgoal by (metis Suc_lessI greaterThanLessThan_iff less_antisym)
        subgoal by (metis greaterThanLessThan_iff less_SucE)
        subgoal by auto
        done
      done

    lemma find_next_guarded_rl: " AUX_SMALLER C l h xs i0; i0+1<h 
       find_next_guarded C xs l h i0  SPEC (λi. i0<i  i<h  AUX_SMALLER C l h xs (i-1)  ( i=h-1  ¬C (xs!i) (xs!l) ) )"  
      unfolding find_next_guarded_def AUX_SMALLER_def RIGHT_GUARD_def mop_C_idx_def
      apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. length xs - i)"])
      apply clarsimp_all
      subgoal by (fastforce elim: less_SucE)
      subgoal by auto  
      done
      
   lemma first_find_next_rl: " AUX_NOTSM (Not oo C) l h xs (j+1); i0+1<h; AUX_SMALLER C l h xs i0; i0+1 < h  
      first_find_next C xs l j h i0  SPEC (λi. i0<i  i<h  AUX_SMALLER C l h xs (i-1)  ( i=h-1  ¬C (xs!i) (xs!l) ))"
      unfolding first_find_next_def
      apply (refine_vcg find_next_guarded_rl find_next_unguarded_rl) 
      apply (auto simp: RIGHT_GUARD_init)
      apply (auto simp: AUX_NOTSM_def)
      done
      
      
            
    lemma find_prev_unguarded_rl: " AUX_NOTSM C l h xs j0; LEFT_GUARD C l xs j0  
      find_prev_unguarded C xs l j0  SPEC (λj. l<j  j<j0  AUX_NOTSM C l h xs (j+1)  ¬C (xs!j) (xs!l))"
      unfolding find_prev_unguarded_def AUX_NOTSM_def LEFT_GUARD_def mop_C_idx_def
      apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. i)"])
      apply simp_all
      apply auto []
      apply auto []
      apply auto []
      subgoal
        apply safe
        apply simp_all
        subgoal by (metis (full_types) greaterThanLessThan_iff leD le_less_linear le_neq_implies_less nat_le_Suc_less_imp)
        subgoal by (metis greaterThanLessThan_iff leD linorder_neqE_nat nat_le_Suc_less_imp)
        subgoal by auto
        done
      done
      

    lemma find_prev_guarded_rl: " AUX_NOTSM C l h xs j0; l+1 < j0  
      find_prev_guarded C xs l j0  SPEC (λj. l<j  j<j0  AUX_NOTSM C l h xs (j+1)  (j = l+1  ¬C (xs!j) (xs!l)))"
      unfolding find_prev_guarded_def AUX_NOTSM_def LEFT_GUARD_def mop_C_idx_def
      apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. i)"])
      apply simp_all
      apply auto []
      apply auto []
      apply (metis Suc_le_lessD atLeastLessThan_iff atLeastSucLessThan_greaterThanLessThan 
              greaterThanLessThan_iff leD le_less_linear less_imp_diff_less nat_le_Suc_less_imp nat_neq_iff)
      apply auto []
      done
      
      
    lemma first_find_prev_rl: " AUX_SMALLER (Not oo C) l h xs (i-1); l<i; AUX_NOTSM C l h xs j0; l+1 < j0  
      first_find_prev C xs l i j0  SPEC (λj. l<j  j<j0  AUX_NOTSM C l h xs (j+1)  (j = l+1  ¬C (xs!j) (xs!l)))"
      unfolding first_find_prev_def
      apply (refine_vcg find_prev_guarded_rl find_prev_unguarded_rl; assumption?) 
      apply (auto simp: LEFT_GUARD_init)
      done
 
       
      
           
    definition "part_right_invar xs0 l h  λ(xs,i,j). 
        slice_eq_mset l h xs0 xs
       xs0!l = xs!l  
       l < h  hlength xs
       {i,j}  {l<..<h}
       AUX_SMALLER (<) l h xs (i-1)
       AUX_NOTSM (Not oo (<)) l h xs (j+1)
       ¬ xs!i < xs!l  (i<j  xs!j < xs!l)
      "

    lemma part_right_invar_boundsD:
      assumes "part_right_invar xs0 l h (xs,i,j)"  
      shows "i<length xs" "j<length xs" "length xs0 = length xs" "i - Suc 0 < length xs" "l  i-Suc 0" "i-Suc 0 < h" "xs0!l = xs!l"
      using assms unfolding part_right_invar_def AUX_SMALLER_def AUX_NOTSM_def
      apply (auto simp: slice_eq_mset_eq_length)
      done
      
    lemma part_right_invar_pres:
      assumes "part_right_invar xs0 l h (xs,i,j)" "i<j"  
      shows "AUX_SMALLER (<) l h (swap xs i j) i"
        and "RIGHT_GUARD (<) l h (swap xs i j) i"
        and "AUX_NOTSM (Not oo (<)) l h (swap xs i j) j"
        and "LEFT_GUARD (Not oo (<)) l (swap xs i j) j"
      using assms unfolding part_right_invar_def
      apply -
      subgoal by (auto simp: PV_SWAP)
      subgoal unfolding RIGHT_GUARD_def by (auto simp: swap_nth)
      subgoal by (auto simp: PV_SWAP)
      subgoal unfolding LEFT_GUARD_def by (auto simp: swap_nth)
      done
      

    lemma mop_list_safe_swap: "mop_list_swap xs i j = doN { ASSERT (i<length xs  j<length xs); if ij then mop_list_swap xs i j else RETURN xs }" 
      by (auto simp: pw_eq_iff refine_pw_simps)
            
    definition "partition_right xs l h  doN {
      ASSERT (l<h  hlength xs);
      
      i  find_next_unguarded (<) xs l h l;
      
      j  first_find_prev (Not oo (<)) xs l i h;

      let alrp = ij;
      
      (xs,i,j) 
        WHILEIT 
          (part_right_invar xs l h) 
          (λ(xs,i,j). i<j) 
          (λ(xs,i,j). doN {
            ASSERT (ij);
            xsmop_list_swap xs i j;
            ifind_next_unguarded (<) xs l h i;
            jfind_prev_unguarded (Not oo (<)) xs l j;
            RETURN (xs,i,j)
          }) 
          (xs,i,j);

      ASSERT (i1);          
      xs  mop_list_swap xs l (i-1);
      
      ASSERT (k{l..<i-1}. xs!k<xs!(i-1)); ― ‹Not required by high-level spec, but to ensure that left side contains only truly smaller elements
      
      RETURN (alrp,i-1,xs)
    }"  
      
    lemma bincond_double_neg[simp]: "Not oo (Not oo C) = C" by (intro ext) auto
    
    
    lemma partition_right_correct: "partition_right xs l h  partition_spec xs l h"            
      unfolding partition_right_def partition_spec_def
      apply (refine_vcg find_next_unguarded_rl first_find_prev_rl[where h=h] find_prev_unguarded_rl[where h=h]  WHILEIT_rule[where R="measure (λ(xs,i,j). j)"])
      apply (all (elim conjE)?, assumption?)
      apply (simp_all add: )
      
      apply (clarsimp_all simp: AUX_SMALLER_init AUX_NOTSM_init RIGHT_GUARD_from_prc part_right_invar_boundsD part_right_invar_pres)
      subgoal unfolding part_right_invar_def by auto 
      subgoal unfolding part_right_invar_def by auto 
      subgoal unfolding part_right_invar_def by auto
      subgoal unfolding part_right_invar_def AUX_SMALLER_def by (auto simp: swap_nth)
      subgoal unfolding part_right_invar_def AUX_SMALLER_def by auto
      subgoal 
        apply (erule PARTITIONED_FINALLY)
        unfolding part_right_invar_def 
        by clarsimp_all
      done  

      
      
      
    definition "part_left_invar xs0 l h  λ(xs,i,j). 
        slice_eq_mset l h xs0 xs
       xs0!l = xs!l  
       l < h  hlength xs
       {i,j}  {l<..<h}
       AUX_SMALLER (Not oo (>)) l h xs (i-1)
       AUX_NOTSM (>) l h xs (j+1)
       ¬ xs!j > xs!l  (i<j  xs!i > xs!l)
      "

    lemma part_left_invar_boundsD:
      assumes "part_left_invar xs0 l h (xs,i,j)"  
      shows "i<length xs" "j<length xs" "length xs0 = length xs" "i - Suc 0 < length xs" "l  i-Suc 0" "i-Suc 0 < h" "xs0!l = xs!l" "lj" "j<h"
      using assms unfolding part_left_invar_def AUX_SMALLER_def AUX_NOTSM_def
      apply (auto simp: slice_eq_mset_eq_length)
      done
      
    lemma part_left_invar_pres:
      assumes "part_left_invar xs0 l h (xs,i,j)" "i<j"  
      shows "AUX_SMALLER (Not oo (>)) l h (swap xs i j) i"
        and "RIGHT_GUARD (Not oo (>)) l h (swap xs i j) i"
        and "AUX_NOTSM (>) l h (swap xs i j) j"
        and "LEFT_GUARD (>) l (swap xs i j) j"
      using assms unfolding part_left_invar_def
      apply -
      subgoal by (auto simp: PV_SWAP)
      subgoal unfolding RIGHT_GUARD_def by (auto simp: swap_nth)
      subgoal using PV_SWAP by fastforce
      subgoal unfolding LEFT_GUARD_def by (auto simp: swap_nth)
      done
      
      
    definition "partition_left xs l h  doN {
      ASSERT (l<h  hlength xs);
      
      j  find_prev_unguarded (>) xs l h;
      
      i  first_find_next (Not oo (>)) xs l j h l;

      (xs,i,j) 
        WHILEIT 
          (part_left_invar xs l h) 
          (λ(xs,i,j). i<j) 
          (λ(xs,i,j). doN {
            ASSERT (ij);
            xsmop_list_swap xs i j;
            jfind_prev_unguarded (>) xs l j;
            ifind_next_unguarded (Not oo (>)) xs l h i;
            RETURN (xs,i,j)
          }) 
          (xs,i,j);
      
      ASSERT (lj);
      xs  mop_list_swap xs l j;
      
      ASSERT (k{j<..<h}. xs!k>xs!j); ― ‹Not required by high-level spec, but to ensure that right side contains only truly greater elements
      
      RETURN (False,j,xs)
    }"  
      
      
    lemma partition_left_correct: "partition_left xs l h  partition_left_spec xs l h"            
      unfolding partition_left_def partition_spec_def partition_left_spec_def
      apply (refine_vcg find_next_unguarded_rl first_find_next_rl[where h=h] find_prev_unguarded_rl[where h=h]  WHILEIT_rule[where R="measure (λ(xs,i,j). j)"])
      apply (all (elim conjE)?, assumption?)
      apply (simp_all add: )
      apply (clarsimp_all simp: AUX_SMALLER_init AUX_NOTSM_init LEFT_GUARD_from_prc part_left_invar_boundsD part_left_invar_pres)  
      subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto        
      subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto        
      subgoal unfolding part_left_invar_def AUX_NOTSM_def by (auto simp: swap_nth)
      subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto
      subgoal unfolding part_left_invar_def by auto
      subgoal 
        apply (erule PARTITIONED_FINALLY2)
        unfolding part_left_invar_def 
        by clarsimp_all
      done  
      

    text We use the guarded arithmetic operations on natural numbers, to avoid to many
      in-bounds conditions to be visible to the simplifier ... this would make the simplifier
      extremely slow when invoked from within Sepref in the next step.
      
      
    definition "shuffle2 xs l h m  doN {
      size  mop_nat_sub h l;
      l_size  mop_nat_sub m l;
      t_m1  mop_nat_add_bnd h m 1;
      r_size  mop_nat_sub h t_m1;
      t_sd8  mop_nat_div size 8;
      
      let highly_unbal = l_size < t_sd8  r_size < t_sd8;
    
      if highly_unbal then doN {
        xs  if l_size  is_threshold then doN {
          t_lsd4  mop_nat_div l_size 4;
          i_lls4  mop_nat_add_bnd h l t_lsd4; ⌦‹l + l_size div 4›
          i_mm1  mop_nat_sub m 1; ⌦‹m-1›
          i_mmls4  mop_nat_sub m t_lsd4; ⌦‹m - l_size div 4›
          
          xs  shuffle_left xs l i_lls4;
          xs  shuffle_left xs i_mm1 i_mmls4;
          
          if l_size > ninther_threshold then doN {
            i_l1  mop_nat_add_bnd h l 1;
            i_l2  mop_nat_add_bnd h l 2;
            i_mm2  mop_nat_sub m 2;
            i_mm3  mop_nat_sub m 3;
            
            i_lls41  mop_nat_add_bnd h i_lls4 1;
            i_lls42  mop_nat_add_bnd h i_lls4 2;
            i_mmls41  mop_nat_sub i_mmls4 1;             
            i_mmls42  mop_nat_sub i_mmls4 2;             
          
            xs  shuffle_left xs i_l1 i_lls41;
            xs  shuffle_left xs i_l2 i_lls42;
            xs  shuffle_left xs i_mm2 i_mmls41;
            xs  shuffle_left xs i_mm3 i_mmls42;
            RETURN xs
          } else RETURN xs
        } else RETURN xs;
        xs  if r_size  is_threshold then doN {
          i_m1  mop_nat_add_bnd h m 1;
          i_h1  mop_nat_sub h 1;
          
          t_rsd4  mop_nat_div r_size 4;
          i_mp1  mop_nat_add_bnd h i_m1 t_rsd4;
          i_hm  mop_nat_sub h t_rsd4;
        
          xs  shuffle_right xs i_m1 i_mp1;
          xs  shuffle_right xs i_h1 i_hm;
          if r_size > ninther_threshold then doN {
          
            i_m2  mop_nat_add_bnd h m 2;
            i_m3  mop_nat_add_bnd h m 3;
            i_h2  mop_nat_sub h 2;
            i_h3  mop_nat_sub h 3;
            i_hm1  mop_nat_sub i_hm 1;
            i_hm2  mop_nat_sub i_hm 2;
            i_mp2  mop_nat_add_bnd h i_mp1 1;
            i_mp3  mop_nat_add_bnd h i_mp1 2;
          
            xs  shuffle_right xs i_m2 i_mp2;
            xs  shuffle_right xs i_m3 i_mp3;
            xs  shuffle_right xs i_h2 i_hm1;  
            xs  shuffle_right xs i_h3 i_hm2;          
            RETURN xs
          } else RETURN xs
        } else RETURN xs;
        RETURN (True,xs)
      } else
        RETURN (False,xs)
    }"
      
    lemma shuffle2_aux: " ninther_threshold < m - l; l  h; l  m; m + 1  h   l + (m - l) div 4 + 1  h"
      apply simp
      done
    
    lemma mop_nat_simps:
      "a+bh  mop_nat_add_bnd h a b = RETURN (a+b)"
      "ba  mop_nat_sub a b = RETURN (a-b)"
      "b0  mop_nat_div a b = RETURN (a div b)" 
      by (simp_all add: mop_nat_defs)
      
    lemma shuffle2_refine: "shuffle2 xs l h m  shuffle xs l h m"
    proof -

      have A: 
        "(shuffle_right,shuffle_right)Id  nat_rel  nat_rel  Idnres_rel" 
        "(shuffle_left,shuffle_left)Id  nat_rel  nat_rel  Idnres_rel"
        by (auto intro!: nres_relI)
      note A = A[param_fo]  
        
        
      {
        assume "lh" "lm" "m+1h"
        then have ?thesis
          unfolding shuffle2_def
          apply (simp split del: if_split add: Let_def mop_nat_simps cong: if_cong)
          unfolding shuffle_def Let_def
          apply (simp named_ss Main_ss: split del: if_split cong: if_cong)
          apply (split if_split; intro conjI impI; simp only: if_True if_False)
          apply (split if_split; intro conjI impI; simp only: if_True if_False)
          apply (all (cases "ninther_threshold < m - l"; simp only: if_True if_False)?)
          apply (all (cases "is_threshold  h - Suc m"; simp only: if_True if_False)?)
          apply (all (cases "ninther_threshold < h - Suc m"; simp only: if_True if_False)?)
          apply (simp_all add: algebra_simps del: One_nat_def add: Suc_eq_plus1)
          apply (rule refine_IdD) 
          apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
          apply (rule refine_IdD) 
          apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
          apply (rule refine_IdD) 
          apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
          done          
      } thus ?thesis
        unfolding shuffle_def by (simp only: pw_le_iff refine_pw_simps) blast 
    qed            

    text Again, we replace the nat arithmetic by assertion-guarded operations, to avoid 
      overwhelming the simplifier.    
    definition "move_pivot_to_front2 xs l h  doN {
      ASSERT (lh  h>0);
      
      size  mop_nat_sub h l;
      s2  mop_nat_div size 2;
      
      if (size > ninther_threshold) then doN {
        ⌦‹ASSERT (l+s2+1<h ∧ h≥3 ∧ s2≥1 ∧ s2<h );›
        ASSERT (l+2h  l+s2+1h  l+s21  h3 );
        xssort_three xs l              (l + s2)      (h - 1);
        xssort_three xs (l + 1)        (l + s2 - 1) (h - 2);
        xssort_three xs (l + 2)        (l + s2 + 1) (h - 3);
        xssort_three xs (l + s2 - 1) (l + s2)       (l + s2 + 1);
        ASSERT (ll+s2);
        xs  mop_list_swap xs l (l+s2);
        ⌦‹ASSERT (xs!l  xs!(l + (s2 + 1)) ∧ xs!(l + (s2 - 1))  xs!l);›
        RETURN xs
      } else doN {
        ASSERT (l+s2h  h1);
        sort_three xs (l+s2) l (h-1)
      }
    }"
    

    lemma move_pivot_to_front2_refine: "move_pivot_to_front2 xs l h  move_pivot_to_front xs l h"    
      unfolding move_pivot_to_front2_def move_pivot_to_front_def Let_def mop_nat_defs
      apply (simp split del: if_split)
      apply (rule refine_IdD)
      apply refine_rcg
      apply refine_dref_type
      apply simp_all
      done
    

    text We explicitly introduce evaluation order of conditions that must be short-circuited.  
    definition "pdqsort_aux2 leftmost xs l h (d::nat)  RECT (λpdqsort_aux (leftmost,xs,l,h,d). doN {
      ASSERT (lh);
      
      if (h-l < pdq_is_threshold) then 
        pdq_guarded_sort_spec leftmost xs l h
      else doN {
        xs  pivot_to_front_spec xs l h;

        ASSERT (¬leftmost  l>0);         
        ifN (if leftmost then RETURN False else doN { ASSERT (l1); bmop_cmp_idxs xs (l-1) l; RETURN (¬b) } ) then doN {
          (_,m,xs)  partition_left_spec xs l h;
          ASSERT (m<h);
          pdqsort_aux (False,xs,m+1,h,d)
        } else doN {
          (alrp,m,xs)  partition_spec xs l h;
          (unbal,xs)  shuffle_spec xs l h m;
          
          ASSERT (0<d);
          let d = (if unbal then d-1 else d);
          
          (didsort,xs)  
            if d=0 then doN {xs  fallback_sort_spec xs l h; RETURN (True,xs)}
            else if alrp  ¬unbal then doN {
              (r,xs)  maybe_sort_spec xs l m;
              if r then doN {
                ASSERT (m<h);
                maybe_sort_spec xs (m+1) h
              } else RETURN (False,xs)
            } else RETURN (False,xs);
            
          if didsort then RETURN xs 
          else doN { ⌦‹TODO: Test optimization of not sorting left partition again, if maybe_sort sorted it›
            xs  pdqsort_aux (leftmost,xs,l,m,d);
            ASSERT (m<h);
            xs  pdqsort_aux (False,xs,m+1,h,d);
            RETURN xs
          } 
        }
      }
    
    }) (leftmost,xs,l,h,d)"

    (* TODO: Move. TODO: really refine2? *)      
    lemma ifN_refine[refine2]:
      assumes "bRETURN b'" "cR c'" "dR d'"
      shows "(ifN b then c else d) R (if b' then c' else d')"
      using assms if_bind_cond_refine by blast
    
    lemma pdqsort_aux2_refine: "pdqsort_aux2 leftmost xs l h d  pdqsort_aux leftmost xs l h d"
      unfolding pdqsort_aux2_def pdqsort_aux_def
      apply (rule refine_IdD if_bind_cond_refine)
      apply refine_rcg
      apply refine_dref_type
      apply (all (simp named_ss HOL_ss: prod_rel_simp pair_in_Id_conv)?)
      apply (all (elim conjE)?)
      apply simp_all
      by auto
      
          
  end
  
  
  subsection Refinement to Isabelle-LLVM

  text Some boilerplate code for every subroutine.  
  
  context sort_impl_context begin
    
    sepref_register 
      left_find_prev_ug: "find_prev_unguarded (>)"
      left_find_next_ug: "find_next_unguarded (Not oo (>))"
      left_find_next_g: "find_next_guarded (Not oo (>))"
      left_first_find_next: "first_find_next (Not oo (>))"

      
    lemma mop_C_idx_unfolds:
      "mop_C_idx (>) xs i j = mop_cmp_idxs xs j i"                                                             
      "mop_C_idx (Not oo (>)) xs i j = doN { bmop_cmp_idxs xs j i; RETURN (¬b) }"  
      "mop_C_idx (<) xs i j = mop_cmp_idxs xs i j"                                                             
      "mop_C_idx (Not oo (<)) xs i j = doN { bmop_cmp_idxs xs i j; RETURN (¬b) }"  
      unfolding mop_C_idx_def
      by (auto simp: pw_eq_iff refine_pw_simps)
      
      
      
    sepref_def left_find_prev_ug_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_unguarded (>)))" 
      :: "arr_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_prev_unguarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref

    sepref_def left_find_next_ug_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_unguarded (Not oo (>))))" 
      :: "arr_assnk *a size_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_next_unguarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref

    sepref_def left_find_next_g_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_guarded (Not oo (>))))" 
      :: "arr_assnk *a size_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_next_guarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
            
    sepref_def left_first_find_next_impl [llvm_inline] is "uncurry4 (PR_CONST (first_find_next (Not oo (>))))" 
      :: "arr_assnk *a size_assnk *a size_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding first_find_next_def PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
      

    sepref_def partition_left_impl is "uncurry2 (PR_CONST partition_left)" 
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk  bool1_assn ×a size_assn ×a arr_assn [λ((a,_),_) (_,_,r). r=a]c"
      unfolding partition_left_def PR_CONST_def
      by sepref
      

    thm partition_right_def  
      
    sepref_register 
      right_find_prev_ug: "find_prev_unguarded (Not oo (<))"
      right_find_next_ug: "find_next_unguarded (<)"
      right_find_next_g: "find_prev_guarded (Not oo (<))"
      right_first_find_next: "first_find_prev (Not oo (<))"
      
      
    sepref_def right_find_prev_ug_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_unguarded (Not oo (<))))" 
      :: "arr_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_prev_unguarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref

    sepref_def right_find_next_ug_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_unguarded (<)))" 
      :: "arr_assnk *a size_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_next_unguarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref

    sepref_def right_find_prev_g_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_guarded (Not oo (<))))" 
      :: "arr_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding find_prev_guarded_def mop_C_idx_unfolds PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
            
    sepref_def right_first_find_prev_impl [llvm_inline] is "uncurry3 (PR_CONST (first_find_prev (Not oo (<))))" 
      :: "arr_assnk *a size_assnk *a size_assnk *a size_assnk a size_assn"
      unfolding first_find_prev_def PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
      
    sepref_def partition_right_impl [llvm_inline] is "uncurry2 (PR_CONST partition_right)" 
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk  bool1_assn ×a size_assn ×a arr_assn [λ((a,_),_) (_,_,r). r=a]c"
      unfolding partition_right_def PR_CONST_def
      apply (rewrite at "mop_list_swap _ _ (_-1)" mop_list_safe_swap)
      apply (annot_snat_const "TYPE(size_t)")
      by sepref

    sepref_register shuffle2  
      
    sepref_def shuffle_impl [llvm_inline] is "uncurry3 shuffle2"   
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk *a size_assnk  bool1_assn ×a arr_assn [λ(((a,_),_),_) (_,r). r=a]c"
      unfolding shuffle2_def PR_CONST_def shuffle_left_def shuffle_right_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
            
    sepref_register sort_three  
      
    sepref_def sort_three_impl [llvm_inline] is "uncurry3 (PR_CONST sort_three)"   
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk *a size_assnk  arr_assn [λ(((a,_),_),_) r. r=a]c"
      unfolding sort_three_def sort_two_def PR_CONST_def
      by sepref
      
    sepref_def move_pivot_to_front_impl [llvm_inline] is "uncurry2 (PR_CONST move_pivot_to_front2)" 
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk  arr_assn [λ((a,_),_) r. r=a]c"
      unfolding move_pivot_to_front2_def PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
      

    sepref_register pivot_to_front_spec partition_left_spec partition_spec shuffle_spec fallback_sort_spec
    
    lemma move_pivot_to_front2_refine': "(PR_CONST move_pivot_to_front2, PR_CONST pivot_to_front_spec)IdIdIdIdnres_rel"
    proof - 
      note move_pivot_to_front2_refine also note move_pivot_to_front_refine 
      finally show ?thesis by (auto intro!: nres_relI)
    qed

    lemma partition_left_refine': "(PR_CONST partition_left, PR_CONST partition_left_spec)  IdIdIdIdnres_rel"
      using partition_left_correct by (auto intro!: nres_relI)
    
    lemma partition_right_refine': "(PR_CONST partition_right, PR_CONST partition_spec)  IdIdIdIdnres_rel"
      using partition_right_correct by (auto intro!: nres_relI)
      
    lemma shuffle_refine': "(shuffle2, shuffle_spec)  IdIdIdIdIdnres_rel"  
    proof -
      note shuffle2_refine also note shuffle_correct 
      finally show ?thesis by (auto intro!: nres_relI) 
    qed
      
    lemma heapsort_refine_fbs': "(PR_CONST heapsort,PR_CONST fallback_sort_spec)  Id  Id  Id  Idnres_rel"  
      unfolding fallback_sort_spec_def PR_CONST_def
      using heapsort_correct'[OF IdI IdI IdI] by (auto intro!: nres_relI)
            
    lemmas [sepref_fr_rules] = 
      move_pivot_to_front_impl.refine[FCOMP move_pivot_to_front2_refine']
      partition_left_impl.refine[FCOMP partition_left_refine']
      partition_right_impl.refine[FCOMP partition_right_refine']
      shuffle_impl.refine[FCOMP shuffle_refine']
      heapsort_hnr[FCOMP heapsort_refine_fbs']
    
    sepref_register pdqsort_aux
    sepref_def pdqsort_aux_impl [llvm_inline] is "uncurry4 (PR_CONST pdqsort_aux2)" 
      :: "[λ_. True]c bool1_assnk *a arr_assnd *a size_assnk *a size_assnk *a size_assnk  arr_assn [λ((((_,a),_),_),_) r. r=a]c"
      unfolding pdqsort_aux2_def PR_CONST_def
      supply [[goals_limit = 1]]
      apply (annot_snat_const "TYPE(size_t)")
      apply (rewrite RECT_cp_annot[where CP="λ(_,ai,_,_,_) r. r=ai"])
      by sepref 
                  
    lemma pdqsort_aux2_refine': "(PR_CONST pdqsort_aux2, PR_CONST pdqsort_aux)  Id  Id  Id  Id  Id  Idnres_rel"  
      using pdqsort_aux2_refine by (auto intro: nres_relI)
      
    lemmas [sepref_fr_rules] = pdqsort_aux_impl.refine[FCOMP pdqsort_aux2_refine']
      
      
      
    sepref_register pdqsort  
    sepref_def pdqsort_impl is "uncurry2 (PR_CONST pdqsort)" 
      :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk  arr_assn [λ((a,_),_) r. r=a]c"
      unfolding pdqsort_def PR_CONST_def
      apply (annot_snat_const "TYPE(size_t)")
      by sepref
  
      
      
  end

  
  
  
end