Theory Examples.Sorting_Heapsort

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]: "lh"
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: " li; i<h   in_heap i" by prove
      
    lemma in_heap_bounds[simp]: 
      assumes "in_heap i" 
      shows "li" 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 ll<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  (hlength 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  
      (hlength xs) 
       (i. has_parent i  ij  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 "hlength 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]: "hlength 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" "ji" 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!ixs!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 
        (hlength 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 "hlength 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]: "hlength 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!jxs!lchild j; xs!jxs!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!jxs!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  hlength 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: "hlength 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  hlength 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  hlength 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!jxs!lchild j; xs!jxs!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!jxs!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]: "hlength 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]: "hlength 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]: "hlength 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 xs0 i xs 
      slice_eq_mset l h xs xs0      
     is_heap_except_up i xs"  
    
  lemma sift_up_invar_init: 
    assumes "is_heap xs" "slice_eq_mset l h xs xs0" "h<length xs" 
    shows "heap_context.sift_up_invar () l (Suc h) xs0 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 xs0 i xs; has_parent i; xs!ixs!parent i  
     sift_up_invar xs0 (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 xs0 l xs  is_heap xs  slice_eq_mset l h xs xs0"
    unfolding sift_up_invar_def
    using sift_up_term1 by blast
    
  lemma sift_up_invar_term2: "sift_up_invar xs0 i xs; xs!ixs!parent i 
     is_heap xs  slice_eq_mset l h xs xs0"
    unfolding sift_up_invar_def
    using sift_up_term2 by blast

  definition "sift_down_invar xs0 i xs 
      slice_eq_mset l h xs xs0      
     is_heap_except_down i xs"  

  lemma sift_down_invar_step:
    assumes "sift_down_invar xs0 i xs"
    shows "has_rchild i; xs!ixs!lchild i; xs!lchild i  xs!rchild i  sift_down_invar xs0 (lchild i) (swap xs i (lchild i))" 
      and "has_rchild i; xs!ixs!rchild i; xs!lchild i  xs!rchild i  sift_down_invar xs0 (rchild i) (swap xs i (rchild i))"
      and "has_lchild i; ¬has_rchild i; xs!ixs!lchild i  sift_down_invar xs0 (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 xs0 l' xs 
      slice_eq_mset l h xs xs0      
     is_heap_btu l' xs"
  
  definition "sift_down_btu_invar xs0 l' i xs  
      slice_eq_mset l h xs xs0      
     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 i0 xs  doN {
    ASSERT (in_heap i0  i0<length xs);
    (xs,i,_)  WHILEIT (λ(xs,i,ctd). in_heap i  ii0) 
      (λ(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,i0,True);
  
    ASSERT (in_heap i  ii0);
    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  hlength xs  i<length xs"
    using in_heap_bounds(2) less_le_trans by blast
  
    
    
  lemma sift_down_btu_correct:
    assumes "heapify_btu_invar xs0 l' xs" "l<l'"
    shows "sift_down (l'-Suc 0) xs  SPEC (λxs'. heapify_btu_invar xs0 (l'-Suc 0) xs')"
    unfolding sift_down_def 
    apply (refine_vcg WHILEIT_rule_amend_invar[where 
      I="λ(xs,i,ctd). 
          sift_down_btu_invar xs0 (l'-Suc 0) i xs 
           hlength xs
           (¬ctd  has_rchild i  xs!ixs!lchild i  xs!ixs!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 xs0 l xs"
    shows "sift_down l xs  SPEC (λxs'. slice_eq_mset l h xs' xs0  is_heap xs')"  
    unfolding sift_down_def
    apply (refine_vcg WHILEIT_rule_amend_invar[where 
      I="λ(xs,i,ctd). 
          sift_down_invar xs0 i xs 
           hlength xs
           (¬ctd  has_rchild i  xs!ixs!lchild i  xs!ixs!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 i0 xs  doN {
    ASSERT (in_heap i0);
    v  mop_list_get xs i0;
    (xs,i,_)  WHILEIT (λ(xs,i,ctd). in_heap i  ii0) (λ(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,i0,True);

    ASSERT (in_heap i  ii0);
    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 i0 xs Id (sift_down i0 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 i0 xs  doN {
    ASSERT (li0  i0<h);
    let i1 = i0 - l;
    
    v  mop_list_get xs (i1+l);
    
    (xs,i,_)  WHILEIT (λ(xs,i,ctd). i<h-l  ii1) (λ(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 (lcii  rcii  lcirci);
      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,i1,True);
    
    ASSERT (ii1  i+l<h);
    
    if has_lchild3 l h i then doN {
      lci  mop_lchild3 h i;
      ASSERT (lci+l<h);
      ASSERT (lcii);
      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  ih-l"
      "xi'  x-li"
    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+ih); mop_eo_extract xs (l+i) }"
  definition [simp]: "mop_seth2 xs i x  doN { ASSERT(l+ih); 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 i0 xs  doN {
    ASSERT (li0  i0<h);
    let i1 = i0 - l;
    xs  mop_to_eo_conv xs;
    (v,xs)  mop_geth3 l h xs i1;
    
    (xs,i,_)  WHILEIT (λ(xs,i,ctd). i<h-l  ii1) (λ(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,i1,True);
    
    ASSERT (ii1);
    
    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  (ji  v = xs!j)"  
    unfolding woe_eq_except_def 
    by force
    
  lemma woe_eq_except_nth: "woe_eq_except i xs' xs; j<length xs; ji  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" "ii'"
    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 xs0  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')
      })
      (xs0,h-1);
    RETURN xs
  }"    
    
  lemma heapify_btu_correct: " l<h; hlength xs0   heapify_btu xs0  SPEC (λxs. slice_eq_mset l h xs xs0  is_heap xs)"
    unfolding heapify_btu_def
    apply simp
    apply (refine_vcg WHILET_rule[where I="λ(xs,l'). heapify_btu_invar xs0 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 xs0 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 xs0 l h0  doN {
    ASSERT (lh0);
    if h0-l > 1 then doN {
      xs  heapify_btu1 (<) l h0 xs0;
      
      (xs,h)WHILEIT (λ(xs,h). 
          l<h  hh0 
         heap_context.is_heap (le_by_lt (<)) l h xs
         slice_eq_mset l h0 xs xs0
         sorted_wrt_lt (<) (slice h h0 xs)
         (aset (slice l h xs). bset (slice h h0 xs). (le_by_lt (<)) a b)
      ) 
        (λ(xs,h). Suc l < h) 
        (λ(xs,h). doN {
          ASSERT (h>0  lh-1);
          xs  mop_list_swap xs l (h-1);
          xs  sift_down4 (<) l (h-1) l xs;
          RETURN (xs,h-1)
        })
        (xs,h0);
      
      RETURN xs
    } else
      RETURN xs0
  }"
  
  
    
  lemma heapsort_correct:
    assumes "lh0" "h0length xs0"
    shows "heapsort xs0 l h0  SPEC (λxs. slice_eq_mset l h0 xs xs0  sorted_wrt_lt (<) (slice l h0 xs))"
  proof -
    interpret initial: heap_context "()" "(<)" l h0 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 xs1 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 xs0" 
          and [simp, arith]: "h0  length xs0"
        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 h0 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 h0 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 h0 xs xs0   
          finally have G1: "slice_eq_mset l h0 xs' xs0" .
  
          note [simp] = slice_eq_mset_eq_length[OF G1]
          
          have [simp]: "slice (h - Suc 0) h0 xs' = (xs'!(h-Suc 0))#slice h h0 xs'"
            apply (rule slice_extend1_left)
            using prems by (auto)
          
            
          have "slice h h0 xs' = slice h h0 (swap xs l (h - Suc 0))"
            apply (rule slice_eq_mset_eq_outside(2)[OF A]) using prems by auto
          also have " = slice h h0 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 h0 xs' = slice h h0 xs" .
            
          have [arith,simp]: "h - Suc 0 < length xs0" "l<length xs0" 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) h0 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) h0 xs'). ab" 
            thm slice_eq_mset_set_inside[OF A]
            apply (simp add: slice_eq_mset_set_inside[OF A])
            using xset (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 hh0
          apply (auto simp: aux)
          done
          
      qed
      apply clarsimp
      subgoal premises prems for xs1 xs h
      proof -
        have [simp]: "h=l+1" using prems by auto
      
        from prems have [simp]: "length xs = length xs0"
          and [simp, arith]: "l<length xs0" "h<length xs0"
          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 xs0 l h0 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_assnk *a size_assnk 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_assnk *a size_assnk 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). lh]a size_assnk *a size_assnk *a size_assnk  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_assnk *a size_assnk *a size_assnk  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_assnk *a size_assnk *a (eoarray_slice_assn elem_assn)d *a size_assnk  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_assnk *a size_assnk *a (eoarray_slice_assn elem_assn)d *a size_assnk *a elem_assnd 
       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_assnk *a size_assnk *a size_assnk *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_assnk *a size_assnk *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_assnk *a size_assnk  (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 i0 xs  doN {
    ASSERT (li0  i0<h);
    let i1 = i0 - l;
    xs  mop_to_eo_conv xs;
    (v,xs)  mop_geth3 l h xs i1;
    
    (xs,i,_)  WHILEIT (λ(xs,i,ctd). i<h-l  ii1) (λ(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,i1,True);
    
    ASSERT (ii1);
    
    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; vcdom 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; (i0',i0)Id; (xs',xs)cdom_list_rel cparam  
     sift_down_param cparam l' h' i0' xs'  (cdom_list_rel cparam) (sift_down4 (less' cparam) l h i0 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 xs0  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')
      })
      (xs0,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 xs0 l h0  doN {
    ASSERT (lh0);
    if h0-l > 1 then doN {
      xs  heapify_btu_param cparam l h0 xs0;
      
      (xs,h)WHILET
        (λ(xs,h). Suc l < h) 
        (λ(xs,h). doN {
          ASSERT (h>0  lh-1);
          xs  mop_list_swap xs l (h-1);
          xs  sift_down_param cparam l (h-1) l xs;
          RETURN (xs,h-1)
        })
        (xs,h0);
      
      RETURN xs
    } else
      RETURN xs0
  }"

  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  Idnres_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_assnk *a size_assnk *a eo_assnd *a size_assnk 
     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_assnk *a size_assnk *a eo_assnd *a size_assnk *a elem_assnd 
     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_assnk *a size_assnk *a size_assnk *a size_assnk *a wo_assnd 
       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_assnk *a size_assnk *a size_assnk *a wo_assnd  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_assnk *a wo_assnd *a size_assnk *a size_assnk  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