Theory WB_Sort

(* Correctness proof contributed by Maximilian Wuttke *)
theory WB_Sort
  imports More_Sepref.WB_More_Refinement More_Sepref.WB_More_Refinement_List "HOL-Library.Rewrite"
begin

chapter Sorting

text 
  The correctness proof is due to Maximilian Wuttke.

  Remark that a more efficient can be found as part of Isabelle\_LLVM. It has a few advantages.
  First, it does fewer recursive calls (which is an issue in the SAT solver). Second, it is more
  general (see the examples of string sorting that requires ownership knowledge). Finally,
  it is as fast as C++ sorting.


  The implemented sorting is quicksort.



text Every element between termlo and termhi can be chosen as pivot element.
definition choose_pivot :: ('b  'b  bool)  ('a  'b)  'a list  nat  nat  nat nres where
  choose_pivot _ _ _ lo hi = SPEC(λk. k  lo  k  hi)

text The element at index p› partitions the subarray lo..hi›. This means that every element 
definition isPartition_wrt :: ('b  'b  bool)  'b list  nat  nat  nat  bool where
  isPartition_wrt R xs lo hi p  ( i. i  lo  i < p  R (xs!i) (xs!p))  ( j. j > p  j  hi  R (xs!p) (xs!j))

lemma isPartition_wrtI:
  ( i. i  lo; i < p  R (xs!i) (xs!p))  ( j. j > p; j  hi  R (xs!p) (xs!j))  isPartition_wrt R xs lo hi p
  by (simp add: isPartition_wrt_def)

definition isPartition :: 'a :: order list  nat  nat  nat  bool where
  isPartition xs lo hi p  isPartition_wrt (≤) xs lo hi p

abbreviation isPartition_map :: ('b  'b  bool)  ('a  'b)  'a list  nat  nat  nat  bool where
  isPartition_map R h xs i j k  isPartition_wrt (λa b. R (h a) (h b)) xs i j k

lemma isPartition_map_def':
  lo  p  p  hi  hi < length xs  isPartition_map R h xs lo hi p = isPartition_wrt R (map h xs) lo hi p
  by (auto simp add: isPartition_wrt_def conjI)


text Example: 6 is the pivot element (with index 4); term7 is equal to the termlength xs - 1.
lemma isPartition [0,5,3,4,6,9,8,10::nat] 0 7 4
  by (auto simp add: isPartition_def isPartition_wrt_def nth_Cons')



definition sublist :: 'a list  nat  nat  'a list where
sublist xs i j  take (Suc j - i) (drop i xs)

(*take from HashMap *)
lemma take_Suc0:
  "l[]  take (Suc 0) l = [l!0]"
  "0 < length l  take (Suc 0) l = [l!0]"
  "Suc n  length l  take (Suc 0) l = [l!0]"
  by (cases l, auto)+

lemma sublist_single: i < length xs  sublist xs i i = [xs!i]
  by (cases xs) (auto simp add: sublist_def take_Suc0)

lemma insert_eq: insert a b = b  {a}
  by auto

lemma sublist_nth: lo  hi; hi < length xs; k+lo  hi  (sublist xs lo hi)!k = xs!(lo+k)
  by (simp add: sublist_def)

lemma sublist_length: i  j; j < length xs  length (sublist xs i j) = 1 + j - i
  by (simp add: sublist_def)

lemma sublist_not_empty: i  j; j < length xs; xs  []  sublist xs i j  []
  apply simp
  apply (rewrite List.length_greater_0_conv[symmetric])
  apply (rewrite sublist_length)
  by auto



lemma sublist_app: i1  i2; i2  i3  sublist xs i1 i2 @ sublist xs (Suc i2) i3 = sublist xs i1 i3
  unfolding sublist_def
  by (smt Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add)

definition sorted_sublist_wrt :: ('b  'b  bool)  'b list  nat  nat  bool where
  sorted_sublist_wrt R xs lo hi = sorted_wrt R (sublist xs lo hi)

definition sorted_sublist :: 'a :: linorder list  nat  nat  bool where
  sorted_sublist xs lo hi = sorted_sublist_wrt (≤) xs lo hi

abbreviation sorted_sublist_map :: ('b  'b  bool)  ('a  'b)  'a list  nat  nat  bool where
  sorted_sublist_map R h xs lo hi  sorted_sublist_wrt (λa b. R (h a) (h b)) xs lo hi

lemma sorted_sublist_map_def':
  lo < length xs  sorted_sublist_map R h xs lo hi  sorted_sublist_wrt R (map h xs) lo hi
  apply (simp add: sorted_sublist_wrt_def)
  by (simp add: drop_map sorted_wrt_map sublist_def take_map)

lemma sorted_sublist_wrt_refl: i < length xs  sorted_sublist_wrt R xs i i
  by (auto simp add: sorted_sublist_wrt_def sublist_single)

lemma sorted_sublist_refl: i < length xs  sorted_sublist xs i i
  by (auto simp add: sorted_sublist_def sorted_sublist_wrt_refl)

lemma sorted_sublist_map_refl: i < length xs  sorted_sublist_map R h xs i i
  by (auto simp add: sorted_sublist_wrt_refl)




lemma sublist_map: sublist (map f xs) i j = map f (sublist xs i j)
  apply (auto simp add: sublist_def)
  by (simp add: drop_map take_map)


lemma take_set: j  length xs  x  set (take j xs)  ( k. k < j  xs!k = x)
  apply (induction xs)
   apply simp
  by (meson in_set_conv_iff less_le_trans)

lemma drop_set: j  length xs  x  set (drop j xs)  (k. jkk<length xs  xs!k=x)
  by (smt Misc.in_set_drop_conv_nth) (* lemma found by sledgehammer *)

lemma sublist_el: i  j  j < length xs  x  set (sublist xs i j)  ( k. k < Suc j-i  xs!(i+k)=x)
  apply (simp add: sublist_def)
  by (auto simp add: take_set)

lemma sublist_el': i  j  j < length xs  x  set (sublist xs i j)  ( k. ikkj  xs!k=x)
  apply (simp add: sublist_el)
  by (smt Groups.add_ac(2) le_add1 le_add_diff_inverse less_Suc_eq less_diff_conv nat_less_le order_refl)


lemma sublist_lt: hi < lo  sublist xs lo hi = []
  by (auto simp add: sublist_def)

lemma nat_le_eq_or_lt: (a :: nat)  b = (a = b  a < b)
  by linarith


lemma sorted_sublist_wrt_le: hi  lo  hi < length xs  sorted_sublist_wrt R xs lo hi
  apply (auto simp add: nat_le_eq_or_lt)
  unfolding sorted_sublist_wrt_def
  subgoal apply (rewrite sublist_single) by auto
  subgoal by (auto simp add: sublist_lt)
  done

(*
text ‹A sequence consisting of maximal one element is sorted›
lemma sorted_sublist_wrt_le_Suc_Suc:
  assumes ‹lo ≤ hi› and ‹hi ≤ Suc (Suc lo)›
    and ‹lo < length xs›
  shows ‹sorted_sublist_wrt R xs lo hi›
proof -
  have ‹hi = lo ∨ hi = Suc lo ∨ hi = Suc (Suc lo)›
    using assms(1,2) by linarith
  then consider (a) ‹hi = lo› | (b) ‹hi = Suc lo› | (c) ‹hi = Suc (Suc lo)› by blast
  then show ?thesis
    oops
*)



text Elements in a sorted sublists are actually sorted
lemma sorted_sublist_wrt_nth_le:
  assumes sorted_sublist_wrt R xs lo hi and lo  hi and hi < length xs and
    lo  i and i < j and j  hi
  shows R (xs!i) (xs!j)
proof -
  have A: lo < length xs using assms(2) assms(3) by linarith
  obtain i' where I: i = lo + i' using assms(4) le_Suc_ex by auto
  obtain j' where J: j = lo + j' by (meson assms(4) assms(5) dual_order.trans le_iff_add less_imp_le_nat)
  show ?thesis
    using assms(1) apply (simp add: sorted_sublist_wrt_def I J)
    apply (rewrite sublist_nth[symmetric, where k=i', where lo=lo, where hi=hi])
    using assms apply auto subgoal using I by linarith
    apply (rewrite sublist_nth[symmetric, where k=j', where lo=lo, where hi=hi])
    using assms apply auto subgoal using J by linarith
    apply (rule sorted_wrt_nth_less)
    apply auto
    subgoal using I J nat_add_left_cancel_less by blast
    subgoal apply (simp add: sublist_length) using J by linarith
    done
qed

text We can make the assumption termi < j weaker if we have a reflexivie relation.
lemma sorted_sublist_wrt_nth_le':
  assumes ref:  x. R x x
    and sorted_sublist_wrt R xs lo hi and lo  hi and hi < length xs
    and lo  i and i  j and j  hi
  shows R (xs!i) (xs!j)
proof -
  have i < j  i = j using i  j by linarith
  then consider (a) i < j |
                (b) i = j by blast
  then show ?thesis
  proof cases
    case a
    then show ?thesis
      using assms(2-5,7) sorted_sublist_wrt_nth_le by blast
  next
    case b
    then show ?thesis
      by (simp add: ref)
  qed
qed



(*
lemma sorted_sublist_map_nth_le:
  assumes ‹sorted_sublist_map R h xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs› and
    ‹lo ≤ i› and ‹i < j› and ‹j ≤ hi›
  shows ‹R (h (xs!i)) (h (xs!j))›
proof -
  show ?thesis
    using assms by (rule sorted_sublist_wrt_nth_le)
qed
*)



lemma sorted_sublist_le: hi  lo  hi < length xs  sorted_sublist xs lo hi
  by (auto simp add: sorted_sublist_def sorted_sublist_wrt_le)

lemma sorted_sublist_map_le: hi  lo  hi < length xs  sorted_sublist_map R h xs lo hi
  by (auto simp add: sorted_sublist_wrt_le)

lemma sublist_cons: lo < hi  hi < length xs  sublist xs lo hi = xs!lo # sublist xs (Suc lo) hi
  apply (simp add: sublist_def)
  by (metis Cons_nth_drop_Suc Suc_diff_le le_trans less_imp_le_nat not_le take_Suc_Cons)

lemma sorted_sublist_wrt_cons':
  sorted_sublist_wrt R xs (lo+1) hi  lo  hi  hi < length xs  (j. lo<jjhi  R (xs!lo) (xs!j))  sorted_sublist_wrt R xs lo hi
  apply (simp add: sorted_sublist_wrt_def)
  apply (auto simp add: nat_le_eq_or_lt)
  subgoal by (simp add: sublist_single)
  apply (auto simp add: sublist_cons sublist_el)
  by (metis Suc_lessI ab_semigroup_add_class.add.commute less_add_Suc1 less_diff_conv)

lemma sorted_sublist_wrt_cons:
  assumes trans: ( x y z. R x y; R y z  R x z) and
    sorted_sublist_wrt R xs (lo+1) hi and
    lo  hi and hi < length xs  and R (xs!lo) (xs!(lo+1))
  shows sorted_sublist_wrt R xs lo hi
proof -
  show ?thesis
    apply (rule sorted_sublist_wrt_cons') using assms apply auto
    subgoal premises assms' for j
    proof -
      have A: j=lo+1  j>lo+1 using assms'(5) by linarith
      show ?thesis
        using A proof
        assume A: j=lo+1 show ?thesis
          by (simp add: A assms')
      next
        assume A: j>lo+1 show ?thesis
          apply (rule trans)
          apply (rule assms(5))
          apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=lo+1, where j=j])
          subgoal using A assms'(6) by linarith
          subgoal using assms'(3) less_imp_diff_less by blast
          subgoal using assms'(5) by auto
          subgoal using A by linarith
          subgoal by (simp add: assms'(6))
          done
      qed
    qed
    done
qed

lemma sorted_sublist_map_cons:
  ( x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z)) 
    sorted_sublist_map R h xs (lo+1) hi  lo  hi  hi < length xs  R (h (xs!lo)) (h (xs!(lo+1)))  sorted_sublist_map R h xs lo hi
  by (blast intro: sorted_sublist_wrt_cons)


lemma sublist_snoc: lo < hi  hi < length xs  sublist xs lo hi = sublist xs lo (hi-1) @ [xs!hi]
  apply (simp add: sublist_def)
proof -
  assume a1: "lo < hi"
  assume "hi < length xs"
  then have "take lo xs @ take (Suc hi - lo) (drop lo xs) = (take lo xs @ take (hi - lo) (drop lo xs)) @ [xs ! hi]"
    using a1 by (metis (no_types) Suc_diff_le add_Suc_right hd_drop_conv_nth le_add_diff_inverse less_imp_le_nat take_add take_hd_drop)
  then show "take (Suc hi - lo) (drop lo xs) = take (hi - lo) (drop lo xs) @ [xs ! hi]"
    by simp
qed

lemma sorted_sublist_wrt_snoc':
  sorted_sublist_wrt R xs lo (hi-1)  lo  hi  hi < length xs  (j. lojj<hi  R (xs!j) (xs!hi))  sorted_sublist_wrt R xs lo hi
  apply (simp add: sorted_sublist_wrt_def)
  apply (auto simp add: nat_le_eq_or_lt)
  subgoal by (simp add: sublist_single)
  apply (auto simp add: sublist_snoc sublist_el sorted_wrt_append ac_simps)
  by (metis add.commute add_cancel_right_right less_add_same_cancel1 less_diff_conv not_gr_zero)


lemma sorted_sublist_wrt_snoc:
  assumes trans: ( x y z. R x y; R y z  R x z) and
    sorted_sublist_wrt R xs lo (hi-1) and
    lo  hi and hi < length xs and (R (xs!(hi-1)) (xs!hi))
  shows sorted_sublist_wrt R xs lo hi
proof -
  show ?thesis
    apply (rule sorted_sublist_wrt_snoc') using assms apply auto
    subgoal premises assms' for j
    proof -
      have A: j=hi-1  j<hi-1 using assms'(6) by linarith
      show ?thesis
        using A proof
        assume A: j=hi-1 show ?thesis
          by (simp add: A assms')
      next
        assume A: j<hi-1 show ?thesis
          apply (rule trans)
           apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=j, where j=hi-1])
               prefer 6
               apply (rule assms(5))
              apply auto
          subgoal using A assms'(5) by linarith
          subgoal using assms'(3) less_imp_diff_less by blast
          subgoal using assms'(5) by auto
          subgoal using A by linarith
          done
      qed
    qed
    done
qed

lemma sorted_sublist_map_snoc:
  ( x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z)) 
    sorted_sublist_map R h xs lo (hi-1) 
    lo  hi  hi < length xs  (R (h (xs!(hi-1))) (h (xs!hi)))  sorted_sublist_map R h xs lo hi
  by (blast intro: sorted_sublist_wrt_snoc)




lemma sublist_split: lo  hi  lo < p  p < hi  hi < length xs  sublist xs lo p @ sublist xs (p+1) hi = sublist xs lo hi
  apply (auto simp add: sublist_def)
  by (smt Suc_leI append_assoc append_eq_append_conv diff_Suc_Suc drop_take_drop_drop le_SucI le_trans nat_less_le) (* Proof by sledgehammer!!! *)

lemma sublist_split_part: lo  hi  lo < p  p < hi  hi < length xs  sublist xs lo (p-1) @ xs!p # sublist xs (p+1) hi = sublist xs lo hi
  apply (auto simp add: sublist_split[symmetric])
  apply (rewrite sublist_snoc[where xs=xs,where lo=lo,where hi=p])
  by auto


text A property for partitions (we always assume that termR is transitive.
lemma isPartition_wrt_trans:
( x y z. R x y; R y z  R x z) 
  isPartition_wrt R xs lo hi p 
  (i j. lo  i  i < p  p < j  j  hi  R (xs!i) (xs!j))
  by (auto simp add: isPartition_wrt_def)

lemma isPartition_map_trans:
( x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z)) 
  hi < length xs 
  isPartition_map R h xs lo hi p 
  (i j. lo  i  i < p  p < j  j  hi  R (h (xs!i)) (h (xs!j)))
  by (auto simp add: isPartition_wrt_def)


lemma merge_sorted_wrt_partitions_between':
  lo  hi  lo < p  p < hi  hi < length xs 
    isPartition_wrt R xs lo hi p 
    sorted_sublist_wrt R xs lo (p-1)  sorted_sublist_wrt R xs (p+1) hi 
    (i j. lo  i  i < p  p < j  j  hi  R (xs!i) (xs!j)) 
    sorted_sublist_wrt R xs lo hi
  apply (auto simp add: isPartition_def isPartition_wrt_def sorted_sublist_def sorted_sublist_wrt_def sublist_map)
  apply (simp add: sublist_split_part[symmetric])
  apply (auto simp add: List.sorted_wrt_append)
  subgoal by (auto simp add: sublist_el)
  subgoal by (auto simp add: sublist_el)
  subgoal by (auto simp add: sublist_el')
  done

lemma merge_sorted_wrt_partitions_between:
  ( x y z. R x y; R y z  R x z) 
    isPartition_wrt R xs lo hi p 
    sorted_sublist_wrt R xs lo (p-1)  sorted_sublist_wrt R xs (p+1) hi 
    lo  hi  hi < length xs  lo < p  p < hi  hi < length xs 
    sorted_sublist_wrt R xs lo hi
  by (simp add: merge_sorted_wrt_partitions_between' isPartition_wrt_trans)


(*
lemma merge_sorted_map_partitions_between:
  ‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
    isPartition_map R h xs lo hi p ⟹
    sorted_sublist_map R h xs lo (p-1) ⟹ sorted_sublist_map R h xs (p+1) hi ⟹
    lo ≤ hi ⟹ hi < length xs ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
    sorted_sublist_map R h xs lo hi›
  by (simp add: merge_sorted_wrt_partitions_between' isPartition_map_trans)
*)




text The main theorem to merge sorted lists
lemma merge_sorted_wrt_partitions:
  isPartition_wrt R xs lo hi p 
    sorted_sublist_wrt R xs lo (p - Suc 0)  sorted_sublist_wrt R xs (Suc p) hi 
    lo  hi  lo  p  p  hi  hi < length xs 
    (i j. lo  i  i < p  p < j  j  hi  R (xs!i) (xs!j)) 
    sorted_sublist_wrt R xs lo hi
  subgoal premises assms
  proof -
    have C: lo=pp=hi  lo=pp<hi  lo<pp=hi  lo<pp<hi
      using assms by linarith
    show ?thesis
      using C apply auto
      subgoal ― ‹lo=p=hi
        apply (rule sorted_sublist_wrt_refl)
        using assms by auto
      subgoal ― ‹lo=p<hi
        using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_cons')
      subgoal ― ‹lo<p=hi
        using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_snoc')
      subgoal ― ‹lo<p<hi
        using assms
        apply (rewrite merge_sorted_wrt_partitions_between'[where p=p])
        by auto
      done
  qed
  done

theorem merge_sorted_map_partitions:
  ( x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z)) 
    isPartition_map R h xs lo hi p 
    sorted_sublist_map R h xs lo (p - Suc 0)  sorted_sublist_map R h xs (Suc p) hi 
    lo  hi  lo  p  p  hi  hi < length xs 
    sorted_sublist_map R h xs lo hi
  apply (rule merge_sorted_wrt_partitions) apply auto
  by (simp add: merge_sorted_wrt_partitions isPartition_map_trans)


lemma partition_wrt_extend:
  isPartition_wrt R xs lo' hi' p 
  hi < length xs 
  lo  lo'  lo'  hi  hi'  hi 
  lo'  p  p  hi' 
  ( i. loi  i <lo'  R (xs!i) (xs!p)) 
  ( j. hi'<j  jhi  R (xs!p) (xs!j)) 
  isPartition_wrt R xs lo hi p
  unfolding isPartition_wrt_def
  apply auto
  subgoal by (meson not_le)
  subgoal by (metis nat_le_eq_or_lt nat_le_linear)
  done

lemma partition_map_extend:
  isPartition_map R h xs lo' hi' p 
  hi < length xs 
  lo  lo'  lo'  hi  hi'  hi 
  lo'  p  p  hi' 
  ( i. loi  i <lo'  R (h (xs!i)) (h (xs!p))) 
  ( j. hi'<j  jhi  R (h (xs!p)) (h (xs!j))) 
  isPartition_map R h xs lo hi p
  by (auto simp add: partition_wrt_extend)


lemma isPartition_empty:
  ( j. lo < j; j  hi  R (xs ! lo) (xs ! j)) 
  isPartition_wrt R xs lo hi lo
  by (auto simp add: isPartition_wrt_def)



lemma take_ext:
  (i<k. xs'!i=xs!i) 
  k < length xs  k < length xs' 
  take k xs' = take k xs
  by (simp add: nth_take_lemma)

lemma drop_ext':
  (i. ik  i<length xs  xs'!i=xs!i) 
   0<k  xs[]  ― ‹These corner cases will be dealt with in the next lemma
   length xs'=length xs 
   drop k xs' = drop k xs
  apply (rewrite in drop _  = _ List.rev_rev_ident[symmetric])
  apply (rewrite in _ = drop _  List.rev_rev_ident[symmetric])
  apply (rewrite in  = _ List.drop_rev)
  apply (rewrite in _ =  List.drop_rev)
  apply simp
  apply (rule take_ext)
  by (auto simp add: nth_rev)

lemma drop_ext:
(i. ik  i<length xs  xs'!i=xs!i) 
   length xs'=length xs 
   drop k xs' = drop k xs
  apply (cases xs)
   apply auto
  apply (cases k)
  subgoal  by (simp add: nth_equalityI)
  subgoal apply (rule drop_ext') by auto
  done


lemma sublist_ext':
  (i. loiihi  xs'!i=xs!i) 
   length xs' = length xs 
   lo  hi  Suc hi < length xs 
   sublist xs' lo hi = sublist xs lo hi
  apply (simp add: sublist_def)
  apply (rule take_ext)
  by auto


lemma lt_Suc: (a < b) = (Suc a = b  Suc a < b)
  by auto

lemma sublist_until_end_eq_drop: Suc hi = length xs  sublist xs lo hi = drop lo xs
  by (simp add: sublist_def)

lemma sublist_ext:
  (i. loiihi  xs'!i=xs!i) 
   length xs' = length xs 
   lo  hi  hi < length xs 
   sublist xs' lo hi = sublist xs lo hi
  apply (auto simp add: lt_Suc[where a=hi])
  subgoal by (auto simp add: sublist_until_end_eq_drop drop_ext)
  subgoal by (auto simp add: sublist_ext')
  done

lemma sorted_wrt_lower_sublist_still_sorted:
  assumes sorted_sublist_wrt R xs lo (lo' - Suc 0) and
    lo  lo' and lo' < length xs and
    ( i. loii<lo'  xs'!i=xs!i) and length xs' = length xs
  shows sorted_sublist_wrt R xs' lo (lo' - Suc 0)
proof -
  have l: lo < lo' - 1  lo  lo'-1
    by linarith
  show ?thesis
    using l apply auto
    subgoal ― ‹lo < lo' - 1
      apply (auto simp add: sorted_sublist_wrt_def)
      apply (rewrite sublist_ext[where xs=xs])
      using assms by (auto simp add: sorted_sublist_wrt_def)
    subgoal ― ‹lo >= lo' - 1
      using assms by (auto simp add: sorted_sublist_wrt_le)
    done
qed

lemma sorted_map_lower_sublist_still_sorted:
  assumes sorted_sublist_map R h xs lo (lo' - Suc 0) and
    lo  lo' and lo' < length xs and
    ( i. loii<lo'  xs'!i=xs!i) and length xs' = length xs
  shows sorted_sublist_map R h xs' lo (lo' - Suc 0)
  using assms by (rule sorted_wrt_lower_sublist_still_sorted)

lemma sorted_wrt_upper_sublist_still_sorted:
  assumes sorted_sublist_wrt R xs (hi'+1) hi and
    lo  lo' and hi < length xs and
     j. hi'<jjhi  xs'!j=xs!j and length xs' = length xs
  shows sorted_sublist_wrt R xs' (hi'+1) hi
proof -
  have l: hi' + 1 < hi  hi' + 1  hi
    by linarith
  show ?thesis
    using l apply auto
    subgoal ― ‹hi' + 1 < h
      apply (auto simp add: sorted_sublist_wrt_def)
      apply (rewrite sublist_ext[where xs=xs])
      using assms by (auto simp add: sorted_sublist_wrt_def)
    subgoal ― ‹termhi' + 1  hi
      using assms by (auto simp add: sorted_sublist_wrt_le)
    done
qed

lemma sorted_map_upper_sublist_still_sorted:
  assumes sorted_sublist_map R h xs (hi'+1) hi and
    lo  lo' and hi < length xs and
     j. hi'<jjhi  xs'!j=xs!j and length xs' = length xs
  shows sorted_sublist_map R h xs' (hi'+1) hi
  using assms by (rule sorted_wrt_upper_sublist_still_sorted)







text The specification of the partition function
definition partition_spec :: ('b  'b  bool)  ('a  'b)  'a list  nat  nat  'a list  nat  bool where
  partition_spec R h xs lo hi xs' p 
    mset xs' = mset xs  ― ‹The list is a permutation
    isPartition_map R h xs' lo hi p  ― ‹We have a valid partition on the resulting list
    lo  p  p  hi  ― ‹The partition index is in bounds
    ( i. i<lo  xs'!i=xs!i)  ( i. hi<ii<length xs'  xs'!i=xs!i) ― ‹Everything else is unchanged.


(* Actually, I only need that ‹set (sublist xs' lo hi) = set (sublist xs lo hi)› *)
lemma mathias:
  assumes
        Perm: mset xs' = mset xs
    and I: loi ihi xs'!i=x
    and Bounds: hi < length xs
    and Fix:  i. i<lo  xs'!i = xs!i  j. hi<j; j<length xs  xs'!j = xs!j
  shows j. lojjhi  xs!j = x
proof -
  define xs1 xs2 xs3 xs1' xs2' xs3' where
     xs1 = take lo xs and
     xs2 = take (Suc hi - lo) (drop lo xs) and
     xs3 = drop (Suc hi) xs and
     xs1' = take lo xs' and
     xs2' = take (Suc hi - lo) (drop lo xs') and
     xs3' = drop (Suc hi) xs'
  have [simp]: length xs' = length xs
    using Perm by (auto dest: mset_eq_length)
  have [simp]: mset xs1 = mset xs1'
    using Fix(1) unfolding xs1_def xs1'_def
    by (metis Perm le_cases mset_eq_length nth_take_lemma take_all)
  have [simp]: mset xs3 = mset xs3'
    using Fix(2) unfolding xs3_def xs3'_def mset_drop_upto
    by (auto intro: image_mset_cong2)
  have xs = xs1 @ xs2 @ xs3 xs' = xs1' @ xs2' @ xs3'
    using I unfolding xs1_def xs2_def xs3_def xs1'_def xs2'_def xs3'_def
    by (metis append.assoc append_take_drop_id le_SucI le_add_diff_inverse order_trans take_add)+
  moreover have xs ! i = xs2 ! (i - lo) i  length xs1
    using I Bounds unfolding xs2_def xs1_def by (auto simp: nth_take min_def)
  moreover have  x  set xs2'
    using I Bounds unfolding xs2'_def
    by (auto simp: in_set_take_conv_nth
       intro!: exI[of _ i - lo])
  ultimately have x  set xs2
    using Perm I by (auto dest: mset_eq_setD)
  then obtain j where xs ! (lo + j) = x j  hi - lo
    unfolding in_set_conv_nth xs2_def
    by auto
  then show ?thesis
    using Bounds I
    by (auto intro: exI[of _ lo+j])
qed


text If we fix the left and right rest of two permutated lists, then the sublists are also permutations.
text But we only need that the sets are equal.
lemma mset_sublist_incl:
  assumes Perm: mset xs' = mset xs
    and Fix:  i. i<lo  xs'!i = xs!i  j. hi<j; j<length xs  xs'!j = xs!j
    and bounds: lo  hi hi < length xs
  shows set (sublist xs' lo hi)  set (sublist xs lo hi)
proof
  fix x
  assume x  set (sublist xs' lo hi)
  then have i. loiihi  xs'!i=x
    by (metis assms(1) bounds(1) bounds(2) size_mset sublist_el')
  then obtain i where I: loi ihi xs'!i=x by blast
  have j. lojjhi  xs!j=x
    using Perm I bounds(2) Fix by (rule mathias, auto)
  then show x  set (sublist xs lo hi)
    by (simp add: bounds(1) bounds(2) sublist_el')
qed


lemma mset_sublist_eq:
  assumes mset xs' = mset xs
    and  i. i<lo  xs'!i = xs!i
    and  j. hi<j; j<length xs  xs'!j = xs!j
    and bounds: lo  hi hi < length xs
  shows set (sublist xs' lo hi) = set (sublist xs lo hi)
proof
  show set (sublist xs' lo hi)  set (sublist xs lo hi)
    apply (rule mset_sublist_incl)
    using assms by auto
  show set (sublist xs lo hi)  set (sublist xs' lo hi)
    apply (rule mset_sublist_incl)
    by (metis assms size_mset)+
qed



text Our abstract recursive quicksort procedure. We abstract over a partition procedure.
definition quicksort :: ('b  'b  bool)  ('a  'b)  nat × nat × 'a list  'a list nres where
quicksort R h = (λ(lo,hi,xs0). do {
  RECT (λf (lo,hi,xs). do {
      ASSERT(lo  hi  hi < length xs  mset xs = mset xs0); ― ‹Premise for a partition function
      (xs, p)  SPEC(uncurry (partition_spec R h xs lo hi)); ― ‹Abstract partition function
      ASSERT(mset xs = mset xs0);
      xs  (if p-1lo then RETURN xs else f (lo, p-1, xs));
      ASSERT(mset xs = mset xs0);
      if hip+1 then RETURN xs else f (p+1, hi, xs)
    }) (lo,hi,xs0)
  })

text As premise for quicksor, we only need that the indices are ok.
definition quicksort_pre :: ('b  'b  bool)  ('a  'b)  'a list   nat  nat  'a list  bool where
  quicksort_pre R h xs0 lo hi xs  lo  hi  hi < length xs  mset xs = mset xs0

definition quicksort_post :: ('b  'b  bool)  ('a  'b)  nat  nat  'a list  'a list  bool where
  quicksort_post R h lo hi xs xs' 
    mset xs' = mset xs 
    sorted_sublist_map R h xs' lo hi 
    ( i. i<lo  xs'!i = xs!i) 
    ( j. hi<jj<length xs  xs'!j = xs!j)

text Convert Pure to HOL
lemma quicksort_postI:
  mset xs' = mset xs; sorted_sublist_map R h xs' lo hi; ( i. i<lo  xs'!i = xs!i); ( j. hi<j; j<length xs  xs'!j = xs!j)  quicksort_post R h lo hi xs xs'
  by (auto simp add: quicksort_post_def)


text The first case for the correctness proof of (abstract) quicksort: We assume that we called the partition function, and we have termp-1lo and termhip+1.
lemma quicksort_correct_case1:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
    and pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs: p-1  lo hi  p+1
  shows quicksort_post R h lo hi xs xs'
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs
    using pre by (auto simp add: quicksort_pre_def)
(*
  have part_perm: ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
    using part partition_spec_set_sublist pre(1) pre(2) by blast
*)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)


  have sorted_lower: sorted_sublist_map R h xs' lo (p - Suc 0)
  proof -
    show ?thesis
      apply (rule sorted_sublist_wrt_le)
      subgoal using ifs(1) by auto
      subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
      done
  qed

  have sorted_upper: sorted_sublist_map R h xs' (Suc p) hi
  proof -
    show ?thesis
      apply (rule sorted_sublist_wrt_le)
      subgoal using ifs(2) by auto
      subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
      done
  qed

  have sorted_middle: sorted_sublist_map R h xs' lo hi
  proof -
    show ?thesis
      apply (rule merge_sorted_map_partitions[where p=p])
      subgoal by (rule trans)
      subgoal by (rule part)
      subgoal by (rule sorted_lower)
      subgoal by (rule sorted_upper)
      subgoal using pre(1) by auto
      subgoal by (simp add: part(4))
      subgoal by (simp add: part(5))
      subgoal by (metis part(1) pre(2) size_mset)
      done
  qed

  show ?thesis
  proof (intro quicksort_postI)
    show mset xs' = mset xs
      by (simp add: part(1))
  next
    show sorted_sublist_map R h xs' lo hi
      by (rule sorted_middle)
  next
      show i. i < lo  xs' ! i = xs ! i
      using part(6) by blast
  next
    show j. hi < j; j < length xs  xs' ! j = xs ! j
      by (metis part(1) part(7) size_mset)
  qed
qed


text In the second case, we have to show that the precondition still holds for (p+1, hi, x') after the partition.
lemma quicksort_correct_case2:
  assumes
        pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs: ¬ hi  p + 1
  shows quicksort_pre R h xs0 (Suc p) hi xs'
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs mset xs = mset xs0
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)
  show ?thesis
    unfolding quicksort_pre_def
  proof (intro conjI)
    show Suc p  hi
      using ifs by linarith
    show hi < length xs'
      by (metis part(1) pre(2) size_mset)
    show mset xs' = mset xs0
      using pre(3) part(1) by (auto dest: mset_eq_setD)
  qed
qed



lemma quicksort_post_set:
  assumes quicksort_post R h lo hi xs xs'
    and bounds: lo  hi hi < length xs
  shows set (sublist xs' lo hi) = set (sublist xs lo hi)
proof -
  have mset xs' = mset xs  i. i<lo  xs'!i = xs!i  j. hi<j; j<length xs  xs'!j = xs!j
    using assms by (auto simp add: quicksort_post_def)
  then show ?thesis
    using bounds by (rule mset_sublist_eq, auto)
qed


text In the third case, we have run quicksort recursively on (p+1, hi, xs') after the partition, with hi<=p+1 and p-1<=lo.
lemma quicksort_correct_case3:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
    and pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs: p - Suc 0  lo ¬ hi  Suc p
    and IH1': quicksort_post R h (Suc p) hi xs' xs''
  shows quicksort_post R h lo hi xs xs''
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs mset xs = mset xs0
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)
  have IH1: mset xs'' = mset xs' sorted_sublist_map R h xs'' (Suc p) hi
       i. i<Suc p  xs'' ! i = xs' ! i  j. hi < j; j < length xs'  xs'' ! j = xs' ! j
    using IH1' by (auto simp add: quicksort_post_def)
  note IH1_perm = quicksort_post_set[OF IH1']

  have still_partition: isPartition_map R h xs'' lo hi p
  proof(intro isPartition_wrtI)
    fix i assume lo  i i < p
    show R (h (xs'' ! i)) (h (xs'' ! p))
      text This holds because this part hasn't changed
      using IH1(3) i < p lo  i isPartition_wrt_def part(3) by fastforce
    next
      fix j assume p < j j  hi
      text Obtain the position termposJ where termxs''!j was stored in termxs'.
      have xs''!j  set (sublist xs'' (Suc p) hi)
        by (metis IH1(1) Suc_leI j  hi p < j less_le_trans mset_eq_length part(1) pre(2) sublist_el')
      then have xs''!j  set (sublist xs' (Suc p) hi)
        by (metis IH1_perm ifs(2) nat_le_linear part(1) pre(2) size_mset)
      then have  posJ. Suc pposJposJhi  xs''!j = xs'!posJ
        by (metis Suc_leI j  hi p < j less_le_trans part(1) pre(2) size_mset sublist_el')
      then obtain posJ :: nat where PosJ: Suc pposJ posJhi xs''!j = xs'!posJ by blast

      then show R (h (xs'' ! p)) (h (xs'' ! j))
        by (metis IH1(3) Suc_le_lessD isPartition_wrt_def lessI part(3))
  qed

  have sorted_lower: sorted_sublist_map R h xs'' lo (p - Suc 0)
  proof -
    show ?thesis
      apply (rule sorted_sublist_wrt_le)
      subgoal by (simp add: ifs(1))
      subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
      done
  qed

  note sorted_upper = IH1(2)

  have sorted_middle: sorted_sublist_map R h xs'' lo hi
  proof -
    show ?thesis
      apply (rule merge_sorted_map_partitions[where p=p])
      subgoal by (rule trans)
      subgoal by (rule still_partition)
      subgoal by (rule sorted_lower)
      subgoal by (rule sorted_upper)
      subgoal using pre(1) by auto
      subgoal by (simp add: part(4))
      subgoal by (simp add: part(5))
      subgoal by (metis IH1(1) part(1) pre(2) size_mset)
      done
  qed


  show ?thesis
  proof (intro quicksort_postI)
    show mset xs'' = mset xs
      using part(1) IH1(1) by auto ― ‹I was faster than sledgehammer :-)
  next
    show sorted_sublist_map R h xs'' lo hi
      by (rule sorted_middle)
  next
    show i. i < lo  xs'' ! i = xs ! i
      using IH1(3) le_SucI part(4) part(6) by auto
  next show j. hi < j  j < length xs  xs'' ! j = xs ! j
      by (metis IH1(4) part(1) part(7) size_mset)
  qed
qed


text In the 4th case, we have to show that the premise holds for term(lo,p-1,xs'), in case term¬p-1lo
text Analogous to case 2.
lemma quicksort_correct_case4:
  assumes
        pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs: ¬ p - Suc 0  lo 
  shows quicksort_pre R h xs0 lo (p-Suc 0) xs'
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs mset xs0 = mset xs
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)

  show ?thesis
    unfolding quicksort_pre_def
  proof (intro conjI)
    show lo  p - Suc 0
      using ifs by linarith
    show p - Suc 0 < length xs'
      using mset_eq_length part(1) part(5) pre(2) by fastforce
    show mset xs' = mset xs0
      using pre(3) part(1) by (auto dest: mset_eq_setD)
  qed
qed


text In the 5th case, we have run quicksort recursively on (lo, p-1, xs').
lemma quicksort_correct_case5:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
    and pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs:  ¬ p - Suc 0  lo hi  Suc p
    and IH1': quicksort_post R h lo (p - Suc 0) xs' xs''
  shows quicksort_post R h lo hi xs xs''
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)
  have IH1: mset xs'' = mset xs' sorted_sublist_map R h xs'' lo (p - Suc 0)
     i. i<lo  xs''!i = xs'!i  j. p-Suc 0<j; j<length xs'  xs''!j = xs'!j
    using IH1' by (auto simp add: quicksort_post_def)
  note IH1_perm = quicksort_post_set[OF IH1']


 have still_partition: isPartition_map R h xs'' lo hi p
  proof(intro isPartition_wrtI)
    fix i assume lo  i i < p
      text Obtain the position termposI where termxs''!i was stored in termxs'.
      have xs''!i  set (sublist xs'' lo (p-Suc 0))
        by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred i < p lo  i le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
      then have xs''!i  set (sublist xs' lo (p-Suc 0))
        by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
      then have  posI. loposIposIp-Suc 0  xs''!i = xs'!posI
      proof - ― ‹sledgehammer
        have "p - Suc 0 < length xs"
          by (meson diff_le_self le_less_trans part(5) pre(2))
        then show ?thesis
          by (metis (no_types) xs'' ! i  set (sublist xs' lo (p - Suc 0)) ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
      qed
      then obtain posI :: nat where PosI: loposI posIp-Suc 0 xs''!i = xs'!posI by blast
      then show R (h (xs'' ! i)) (h (xs'' ! p))
        by (metis (no_types, lifting) IH1(4) i < p diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
    next
      fix j assume p < j j  hi
      then show R (h (xs'' ! p)) (h (xs'' ! j))
      text This holds because this part hasn't changed
      by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
  qed


  note sorted_lower = IH1(2)

  have sorted_upper: sorted_sublist_map R h xs'' (Suc p) hi
  proof -
    show ?thesis
      apply (rule sorted_sublist_wrt_le)
      subgoal by (simp add: ifs(2))
      subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
      done
  qed


  have sorted_middle: sorted_sublist_map R h xs'' lo hi
  proof -
    show ?thesis
      apply (rule merge_sorted_map_partitions[where p=p])
      subgoal by (rule trans)
      subgoal by (rule still_partition)
      subgoal by (rule sorted_lower)
      subgoal by (rule sorted_upper)
      subgoal using pre(1) by auto
      subgoal by (simp add: part(4))
      subgoal by (simp add: part(5))
      subgoal by (metis IH1(1) part(1) pre(2) size_mset)
      done
  qed


  show ?thesis
  proof (intro quicksort_postI)
    show mset xs'' = mset xs
      by (simp add: IH1(1) part(1))
  next
    show sorted_sublist_map R h xs'' lo hi
      by (rule sorted_middle)
  next
    show i. i < lo  xs'' ! i = xs ! i
      by (simp add: IH1(3) part(6))
  next
    show j. hi < j  j < length xs  xs'' ! j = xs ! j
      by (metis IH1(4) diff_le_self dual_order.strict_trans2 mset_eq_length part(1) part(5) part(7))
  qed
qed


text In the 6th case, we have run quicksort recursively on (lo, p-1, xs'). We show the precondition on the second call on (p+1, hi, xs'')
lemma quicksort_correct_case6:
  assumes
        pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs:  ¬ p - Suc 0  lo ¬ hi  Suc p
    and IH1: quicksort_post R h lo (p - Suc 0) xs' xs''
  shows quicksort_pre R h xs0 (Suc p) hi xs''
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs mset xs0 = mset xs
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)
  have IH1: mset xs'' = mset xs' sorted_sublist_map R h xs'' lo (p - Suc 0)
     i. i<lo  xs''!i = xs'!i  j. p-Suc 0<j; j<length xs'  xs''!j = xs'!j
    using IH1 by (auto simp add: quicksort_post_def)

  show ?thesis
    unfolding quicksort_pre_def
  proof (intro conjI)
    show Suc p  hi
      using ifs(2) by linarith
    show hi < length xs''
      using IH1(1) mset_eq_length part(1) pre(2) by fastforce
    show mset xs'' = mset xs0
      using pre(3) part(1) IH1(1) by (auto dest: mset_eq_setD)
  qed
qed


text In the 7th (and last) case, we have run quicksort recursively on (lo, p-1, xs'). We show the postcondition on the second call on (p+1, hi, xs'')
lemma quicksort_correct_case7:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
    and pre: quicksort_pre R h xs0 lo hi xs
    and part: partition_spec R h xs lo hi xs' p
    and ifs:  ¬ p - Suc 0  lo ¬ hi  Suc p
    and IH1': quicksort_post R h lo (p - Suc 0) xs' xs''
    and IH2': quicksort_post R h (Suc p) hi xs'' xs'''
  shows quicksort_post R h lo hi xs xs'''
proof -
  text First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure
  have pre: lo  hi hi < length xs
    using pre by (auto simp add: quicksort_pre_def)
  have part: mset xs' = mset xs True
    isPartition_map R h xs' lo hi p lo  p p  hi
     i. i<lo  xs'!i=xs!i  i. hi<i; i<length xs'  xs'!i=xs!i
    using part by (auto simp add: partition_spec_def)
  have IH1: mset xs'' = mset xs' sorted_sublist_map R h xs'' lo (p - Suc 0)
     i. i<lo  xs''!i = xs'!i  j. p-Suc 0<j; j<length xs'  xs''!j = xs'!j
    using IH1' by (auto simp add: quicksort_post_def)
  note IH1_perm = quicksort_post_set[OF IH1']
  have IH2: mset xs''' = mset xs'' sorted_sublist_map R h xs''' (Suc p) hi
     i. i<Suc p  xs'''!i = xs''!i  j. hi<j; j<length xs''  xs'''!j = xs''!j
    using IH2' by (auto simp add: quicksort_post_def)
  note IH2_perm = quicksort_post_set[OF IH2']


  text We still have a partition after the first call (same as in case 5)
  have still_partition1: isPartition_map R h xs'' lo hi p
  proof(intro isPartition_wrtI)
    fix i assume lo  i i < p
      text Obtain the position termposI where termxs''!i was stored in termxs'.
      have xs''!i  set (sublist xs'' lo (p-Suc 0))
        by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred i < p lo  i le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
      then have xs''!i  set (sublist xs' lo (p-Suc 0))
        by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
      then have  posI. loposIposIp-Suc 0  xs''!i = xs'!posI
      proof - ― ‹sledgehammer
        have "p - Suc 0 < length xs"
          by (meson diff_le_self le_less_trans part(5) pre(2))
        then show ?thesis
          by (metis (no_types) xs'' ! i  set (sublist xs' lo (p - Suc 0)) ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
      qed
      then obtain posI :: nat where PosI: loposI posIp-Suc 0 xs''!i = xs'!posI by blast
      then show R (h (xs'' ! i)) (h (xs'' ! p))
        by (metis (no_types, lifting) IH1(4) i < p diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
    next
      fix j assume p < j j  hi
      then show R (h (xs'' ! p)) (h (xs'' ! j))
      text This holds because this part hasn't changed
      by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
  qed


  text We still have a partition after the second call (similar as in case 3)
  have still_partition2: isPartition_map R h xs''' lo hi p
  proof(intro isPartition_wrtI)
    fix i assume lo  i i < p
    show R (h (xs''' ! i)) (h (xs''' ! p))
      text This holds because this part hasn't changed
      using IH2(3) i < p lo  i isPartition_wrt_def still_partition1 by fastforce
    next
      fix j assume p < j j  hi
      text Obtain the position termposJ where termxs'''!j was stored in termxs'''.
      have xs'''!j  set (sublist xs''' (Suc p) hi)
        by (metis IH1(1) IH2(1) Suc_leI j  hi p < j ifs(2) nat_le_linear part(1) pre(2) size_mset sublist_el')
      then have xs'''!j  set (sublist xs'' (Suc p) hi)
        by (metis IH1(1) IH2_perm ifs(2) mset_eq_length nat_le_linear part(1) pre(2))
      then have  posJ. Suc pposJposJhi  xs'''!j = xs''!posJ
        by (metis IH1(1) ifs(2) mset_eq_length nat_le_linear part(1) pre(2) sublist_el')
      then obtain posJ :: nat where PosJ: Suc pposJ posJhi xs'''!j = xs''!posJ by blast

      then show R (h (xs''' ! p)) (h (xs''' ! j))
      proof - ― ‹sledgehammer
        have "n na as p. (p (as ! na::'a) (as ! posJ)  posJ  na)  ¬ isPartition_wrt p as n hi na"
          by (metis (no_types) PosJ(2) isPartition_wrt_def not_less)
        then show ?thesis
          by (metis IH2(3) PosJ(1) PosJ(3) lessI not_less_eq_eq still_partition1)
      qed
  qed


  text We have that the lower part is sorted after the first recursive call
  note sorted_lower1 = IH1(2)

  text We show that it is still sorted after the second call.
  have sorted_lower2: sorted_sublist_map R h xs''' lo (p-Suc 0)
  proof -
    show ?thesis
      using sorted_lower1 apply (rule sorted_wrt_lower_sublist_still_sorted)
      subgoal by (rule part)
      subgoal
        using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
      subgoal
        by (simp add: IH2(3))
      subgoal
        by (metis IH2(1) size_mset)
      done
  qed

  text The second IH gives us the the upper list is sorted after the second recursive call
  note sorted_upper2 = IH2(2)

  text Finally, we have to show that the entire list is sorted after the second recursive call.
  have sorted_middle: sorted_sublist_map R h xs''' lo hi
  proof -
    show ?thesis
      apply (rule merge_sorted_map_partitions[where p=p])
      subgoal by (rule trans)
      subgoal by (rule still_partition2)
      subgoal by (rule sorted_lower2)
      subgoal by (rule sorted_upper2)
      subgoal using pre(1) by auto
      subgoal by (simp add: part(4))
      subgoal by (simp add: part(5))
      subgoal by (metis IH1(1) IH2(1) part(1) pre(2) size_mset)
      done
  qed

  show ?thesis
  proof (intro quicksort_postI)
    show mset xs''' = mset xs
      by (simp add: IH1(1) IH2(1) part(1))
  next
    show sorted_sublist_map R h xs''' lo hi
      by (rule sorted_middle)
  next
    show i. i < lo  xs''' ! i = xs ! i
      using IH1(3) IH2(3) part(4) part(6) by auto
  next
    show j. hi < j  j < length xs  xs''' ! j = xs ! j
      by (metis IH1(1) IH1(4) IH2(4) diff_le_self ifs(2) le_SucI less_le_trans nat_le_eq_or_lt not_less part(1) part(7) size_mset)
  qed

qed



text We can now show the correctness of the abstract quicksort procedure, using the refinement framework and the above case lemmas.
lemma quicksort_correct:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
     and Pre: lo0  hi0 hi0 < length xs0
  shows quicksort R h (lo0,hi0,xs0)   Id (SPEC(λxs. quicksort_post R h lo0 hi0 xs0 xs))
proof -
  have wf: wf (measure (λ(lo, hi, xs). Suc hi - lo))
    by auto
  define pre where pre = (λ(lo,hi,xs). quicksort_pre R h xs0 lo hi xs)
  define post where post = (λ(lo,hi,xs). quicksort_post R h lo hi xs)
  have pre: pre (lo0,hi0,xs0)
    unfolding quicksort_pre_def pre_def by (simp add: Pre)

  text We first generalize the goal a over all states.
  have WB_Sort.quicksort R h (lo0,hi0,xs0)   Id (SPEC (post (lo0,hi0,xs0)))
    unfolding quicksort_def prod.case
    apply (rule RECT_rule)
       apply (refine_mono)
      apply (rule wf)
    apply (rule pre)
    subgoal premises IH for f x
      apply (refine_vcg ASSERT_leI)
      unfolding pre_def post_def

      subgoal ― ‹First premise (assertion) for partition
        using IH(2) by (simp add: quicksort_pre_def pre_def)
      subgoal ― ‹Second premise (assertion) for partition
        using IH(2) by (simp add: quicksort_pre_def pre_def)
      subgoal
        using IH(2) by (auto simp add: quicksort_pre_def pre_def dest: mset_eq_setD)

	text Termination case: term(p-1  lo') and term(hi'  p+1); directly show postcondition
      subgoal unfolding partition_spec_def by (auto dest: mset_eq_setD)
      subgoal ― ‹Postcondition (after partition)
        apply -
        using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
        using trans lin apply (rule quicksort_correct_case1) by auto

      text Case term(p-1  lo') and term(hi' < p+1) (Only second recursive call)
      subgoal
        apply (rule IH(1)[THEN order_trans])

        text Show that the invariant holds for the second recursive call
        subgoal
          using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
          apply (rule quicksort_correct_case2) by auto

        text Wellfoundness (easy)
        subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

        text Show that the postcondition holds
        subgoal
          apply (simp add: Misc.subset_Collect_conv post_def, intro allI impI, elim conjE)
          using trans lin apply (rule quicksort_correct_case3)
          using IH(2) unfolding pre_def by auto
        done

      text Case: At least the first recursive call
      subgoal
        apply (rule IH(1)[THEN order_trans])

        text Show that the precondition holds for the first recursive call
        subgoal
          using IH(2) unfolding pre_def post_def apply (simp, elim conjE, split prod.splits) apply auto
          apply (rule quicksort_correct_case4) by auto

        text Wellfoundness for first recursive call (easy)
        subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

        text Simplify some refinement suff...
        apply (simp add: Misc.subset_Collect_conv ASSERT_leI, intro allI impI conjI, elim conjE)
        apply (rule ASSERT_leI)
        apply (simp_all add: Misc.subset_Collect_conv ASSERT_leI)
        subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
        text Only the first recursive call: show postcondition
        subgoal
          using trans lin apply (rule quicksort_correct_case5)
          using IH(2) unfolding pre_def post_def by auto

        apply (rule ASSERT_leI)
        subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)

        text Both recursive calls.
        subgoal
          apply (rule IH(1)[THEN order_trans])

          text Show precondition for second recursive call (after the first call)
          subgoal
            unfolding pre_def post_def
            apply auto
            apply (rule quicksort_correct_case6)
            using IH(2) unfolding pre_def post_def  by auto

          text Wellfoundedness for second recursive call (easy)
          subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

          text Show that the postcondition holds (after both recursive calls)
          subgoal
            apply (simp add: Misc.subset_Collect_conv, intro allI impI, elim conjE)
            using trans lin apply (rule quicksort_correct_case7)
            using IH(2) unfolding pre_def post_def by auto
          done
        done
      done
    done

  text Finally, apply the generalized lemma to show the thesis.
  then show ?thesis unfolding post_def  by auto
qed



(* TODO: Show that our (abstract) partition satisifies the specification *)


definition partition_main_inv :: ('b  'b  bool)  ('a  'b)  nat  nat  'a list  (nat×nat×'a list)  bool where
  partition_main_inv R h lo hi xs0 p 
    case p of (i,j,xs) 
    j < length xs  j  hi  i < length xs  lo  i  i  j  mset xs = mset xs0 
    (k. k  lo  k < i  R (h (xs!k)) (h (xs!hi)))  ― ‹All elements from termlo to termi-1 are smaller than the pivot
    (k. k  i  k < j   R (h (xs!hi)) (h (xs!k)))  ― ‹All elements from termi to termj-1 are greater than the pivot
    (k. k < lo  xs!k = xs0!k)  ― ‹Everything below termlo is unchanged
    (k. k  j  k < length xs  xs!k = xs0!k) ― ‹All elements from termj are unchanged (including everyting above termhi)
  

text The main part of the partition function. The pivot is assumed to be the last element. This is
exactly the "Lomuto partition scheme" partition function from Wikipedia.
definition partition_main :: ('b  'b  bool)  ('a  'b)  nat  nat  'a list  ('a list × nat) nres where
  partition_main R h lo hi xs0 = do {
    ASSERT(hi < length xs0);
    pivot  RETURN (h (xs0 ! hi));
    (i,j,xs)  WHILETpartition_main_inv R h lo hi xs0― ‹We loop from termj=lo to termj=hi-1.
      (λ(i,j,xs). j < hi)
      (λ(i,j,xs). do {
        ASSERT(i < length xs  j < length xs);
      	if R (h (xs!j)) pivot
      	then RETURN (i+1, j+1, swap xs i j)
      	else RETURN (i,   j+1, xs)
      })
      (lo, lo, xs0); ― ‹i and j are both initialized to lo
    ASSERT(i < length xs  j = hi  lo  i  hi < length xs  mset xs = mset xs0);
    RETURN (swap xs i hi, i)
  }

(*
definition partition_spec :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat ⇒ bool› where
  ‹partition_spec R h xs lo hi xs' p ≡
    mset xs' = mset xs ∧ ― ‹The list is a permutation›
    isPartition_map R h xs' lo hi p ∧ ― ‹We have a valid partition on the resulting list›
    lo ≤ p ∧ p ≤ hi ∧ ― ‹The partition index is in bounds›
    (∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i)› ― ‹Everything else is unchanged.›
*)

lemma partition_main_correct:
  assumes bounds: hi < length xs lo  hi and
    trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
  shows partition_main R h lo hi xs  SPEC(λ(xs', p). mset xs = mset xs' 
     lo  p  p  hi  isPartition_map R h xs' lo hi p  ( i. i<lo  xs'!i=xs!i)  ( i. hi<ii<length xs'  xs'!i=xs!i))
proof -
  have K: b  hi - Suc n  n > 0  Suc n  hi  Suc b  hi - n for b hi n
    by auto
  have L: ~ R (h x) (h y)  R (h y) (h x) for x y ― ‹Corollary of linearity
    using assms by blast
  have M: a < Suc b  a = b  a < b for a b
    by linarith
  have N: (a::nat)  b  a = b  a < b for a b
    by arith

  show ?thesis
    unfolding partition_main_def choose_pivot_def
    apply (refine_vcg WHILEIT_rule[where R = measure(λ(i,j,xs). hi-j)])
    subgoal using assms by blast ― ‹We feed our assumption to the assertion
    subgoal by auto ― ‹WF
    subgoal ― ‹Invariant holds before the first iteration
      unfolding partition_main_inv_def
      using assms apply simp by linarith
    subgoal unfolding partition_main_inv_def by simp
    subgoal unfolding partition_main_inv_def by simp
    subgoal
      unfolding partition_main_inv_def
      apply (auto dest: mset_eq_length)
      done
    subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
    subgoal
      unfolding partition_main_inv_def apply (auto dest: mset_eq_length)
      by (metis L M mset_eq_length nat_le_eq_or_lt)

    subgoal unfolding partition_main_inv_def by simp ― ‹assertions, etc
    subgoal unfolding partition_main_inv_def by simp
    subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
    subgoal unfolding partition_main_inv_def by simp
    subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
    subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
    subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
    subgoal unfolding partition_main_inv_def by simp
    subgoal unfolding partition_main_inv_def by simp

    subgoal ― ‹After the last iteration, we have a partitioning! :-)
      unfolding partition_main_inv_def by (auto simp add: isPartition_wrt_def)
    subgoal ― ‹And the lower out-of-bounds parts of the list haven't been changed
      unfolding partition_main_inv_def by auto
    subgoal ― ‹And the upper out-of-bounds parts of the list haven't been changed
      unfolding partition_main_inv_def by auto
    done
qed


definition partition_between :: ('b  'b  bool)  ('a  'b)  nat  nat  'a list  ('a list × nat) nres where
  partition_between R h lo hi xs0 = do {
    ASSERT(hi < length xs0  lo  hi);
    k  choose_pivot R h xs0 lo hi; ― ‹choice of pivot
    ASSERT(k < length xs0);
    xs  RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop
    ASSERT(length xs = length xs0);
    partition_main R h lo hi xs
  }


lemma partition_between_correct:
  assumes hi < length xs and lo  hi and
   x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and x y. R (h x) (h y)  R (h y) (h x)
  shows partition_between R h lo hi xs  SPEC(uncurry (partition_spec R h xs lo hi))
proof -
  have K: b  hi - Suc n  n > 0  Suc n  hi  Suc b  hi - n for b hi n
    by auto
  show ?thesis
    unfolding partition_between_def choose_pivot_def
    apply (refine_vcg partition_main_correct)
    using assms apply (auto dest: mset_eq_length simp add: partition_spec_def)
    by (metis dual_order.strict_trans2 less_imp_not_eq2 mset_eq_length swap_nth)
qed



text We use the median of the first, the middle, and the last element.
definition choose_pivot3 where
  choose_pivot3 R h xs lo (hi::nat) = do {
    ASSERT(lo < length xs);
    ASSERT(hi < length xs);
    let k' = (hi - lo) div 2;
    let k = lo + k';
    ASSERT(k < length xs);
    let start = h (xs ! lo);
    let mid = h (xs ! k);
    let end = h (xs ! hi);
    if (R start mid  R mid end)  (R end mid  R mid start) then RETURN k
    else if (R start end  R end mid)  (R mid end  R end start) then RETURN hi
    else RETURN lo
}

― ‹We only have to show that this procedure yields a valid index between lo› and hi›.
lemma choose_pivot3_choose_pivot:
  assumes lo < length xs hi < length xs hi  lo
  shows choose_pivot3 R h xs lo hi   Id (choose_pivot R h xs lo hi)
  unfolding choose_pivot3_def choose_pivot_def
  using assms by (auto intro!: ASSERT_leI simp: Let_def)

text The refined partion function: We use the above pivot function and fold instead of non-deterministic iteration.
definition partition_between_ref
  :: ('b  'b  bool)  ('a  'b)  nat  nat  'a list  ('a list × nat) nres
where
  partition_between_ref R h lo hi xs0 = do {
    ASSERT(hi < length xs0  hi < length xs0  lo  hi);
    k  choose_pivot3 R h xs0 lo hi; ― ‹choice of pivot
    ASSERT(k < length xs0);
    xs  RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop
    ASSERT(length xs = length xs0);
    partition_main R h lo hi xs
  }


lemma partition_main_ref':
  partition_main R h lo hi xs
      ((λ a b c d. Id) a b c d) (partition_main R h lo hi xs)
  by auto

lemma partition_between_ref_partition_between:
  partition_between_ref R h lo hi xs  (partition_between R h lo hi xs)
proof -
  have swap: (swap xs k hi, swap xs ka hi)  Id if k = ka
    for k ka
    using that by auto
  have [refine0]: (h (xsa ! hi), h (xsaa ! hi))  Id
    if (xsa, xsaa)  Id
    for xsa xsaa
    using that by auto

  show ?thesis
    apply (subst (2) Down_id_eq[symmetric])
    unfolding partition_between_ref_def
      partition_between_def
      OP_def
    apply (refine_vcg choose_pivot3_choose_pivot swap partition_main_correct)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    by (auto intro: Refine_Basic.Id_refine dest: mset_eq_length)
qed

text Technical lemma for sepref
lemma partition_between_ref_partition_between':
  (uncurry (uncurry (partition_between_ref R h)), uncurry (uncurry (partition_between R h))) 
    nat_rel ×f nat_rel ×f Idlist_rel f Idlist_rel ×r nat_relnres_rel
  by (intro frefI nres_relI)
    (auto intro: partition_between_ref_partition_between)

text Example instantiation for pivot
definition choose_pivot3_impl where
  choose_pivot3_impl = choose_pivot3 (≤) id


lemma partition_between_ref_correct:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
    and bounds: hi < length xs lo  hi
  shows partition_between_ref R h lo hi xs  SPEC (uncurry (partition_spec R h xs lo hi))
proof -
  show ?thesis
    apply (rule partition_between_ref_partition_between[THEN order_trans])
    using bounds apply (rule partition_between_correct[where h=h])
    subgoal by (rule trans)
    subgoal by (rule lin)
    done
qed



term quicksort

text Refined quicksort algorithm: We use the refined partition function.
definition quicksort_ref :: _  _  nat × nat × 'a list  'a list nres where
quicksort_ref R h = (λ(lo,hi,xs0).
  do {
  RECT (λf (lo,hi,xs). do {
      ASSERT(lo  hi  hi < length xs0  mset xs = mset xs0);
      (xs, p)  partition_between_ref R h lo hi xs; ― ‹This is the refined partition function. Note that we need the premises (trans,lin,bounds) here.
      ASSERT(mset xs = mset xs0  p  lo  p < length xs0);
      xs  (if p-1lo then RETURN xs else f (lo, p-1, xs));
      ASSERT(mset xs = mset xs0);
      if hip+1 then RETURN xs else f (p+1, hi, xs)
    }) (lo,hi,xs0)
  })


lemma quicksort_ref_quicksort:
  assumes bounds: hi < length xs lo  hi and
    trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
  shows quicksort_ref R h x0   Id (quicksort R h x0)
proof -
  have wf: wf (measure (λ(lo, hi, xs). Suc hi - lo))
    by auto
  have pre: x0 = x0'  (x0, x0')  Id ×r Id ×r Idlist_rel for x0 x0' :: nat × nat × 'b list
    by auto
  have [refine0]: (x1e = x1d)  (x1e,x1d)  Id for x1e x1d :: 'b list
    by auto

  show ?thesis
    unfolding quicksort_def quicksort_ref_def
    apply (refine_vcg pre partition_between_ref_partition_between'[THEN fref_to_Down_curry2])

    text First assertion (premise for partition)
    subgoal
      by auto
    text First assertion (premise for partition)
    subgoal
      by auto
    subgoal
      by (auto dest: mset_eq_length)
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)

    text Correctness of the concrete partition function
    subgoal
      apply (simp, rule partition_between_ref_correct)
      subgoal by (rule trans)
      subgoal by (rule lin)
      subgoal by auto ― ‹first premise
      subgoal by auto ― ‹second premise
      done
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)
    subgoal by (auto simp: partition_spec_def isPartition_wrt_def)
    subgoal by (auto simp: partition_spec_def isPartition_wrt_def dest: mset_eq_length)
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)
    subgoal
      by (auto dest: mset_eq_length mset_eq_setD)

    by simp+
qed

― ‹Sort the entire list
definition full_quicksort where
  full_quicksort R h xs  if xs = [] then RETURN xs else quicksort R h (0, length xs - 1, xs)

definition full_quicksort_ref where
  full_quicksort_ref R h xs 
    if List.null xs then RETURN xs
    else quicksort_ref R h (0, length xs - 1, xs)

definition full_quicksort_impl :: nat list  nat list nres where
  full_quicksort_impl xs = full_quicksort_ref (≤) id xs

lemma full_quicksort_ref_full_quicksort:
  assumes trans:  x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
  shows (full_quicksort_ref R h, full_quicksort R h) 
          Idlist_rel f  Idlist_relnres_rel
proof -
  show ?thesis
    unfolding full_quicksort_ref_def full_quicksort_def
    apply (intro frefI nres_relI)
    apply (auto intro!: quicksort_ref_quicksort[unfolded Down_id_eq] simp: List.null_def)
    subgoal by (rule trans)
    subgoal using lin by blast
    done
qed


lemma sublist_entire:
  sublist xs 0 (length xs - 1) = xs
  by (simp add: sublist_def)


lemma sorted_sublist_wrt_entire:
  assumes sorted_sublist_wrt R xs 0 (length xs - 1)
  shows sorted_wrt R xs
proof -
  have sorted_wrt R (sublist xs 0 (length xs - 1))
    using assms by (simp add: sorted_sublist_wrt_def )
  then show ?thesis
    by (metis sublist_entire)
qed

lemma sorted_sublist_map_entire:
  assumes sorted_sublist_map R h xs 0 (length xs - 1)
  shows sorted_wrt (λ x y. R (h x) (h y)) xs
proof -
  show ?thesis
    using assms by (rule sorted_sublist_wrt_entire)
qed


text Final correctness lemma
lemma full_quicksort_correct_sorted:
  assumes
    trans: x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and lin: x y. R (h x) (h y)  R (h y) (h x)
  shows full_quicksort R h xs   Id (SPEC(λxs'. mset xs' = mset xs  sorted_wrt (λ x y. R (h x) (h y)) xs'))
proof -
  show ?thesis
    unfolding full_quicksort_def
    apply (refine_vcg)
    subgoal by simp ― ‹case xs=[]
    subgoal by simp ― ‹case xs=[]

    apply (rule quicksort_correct[THEN order_trans])
    subgoal by (rule trans)
    subgoal by (rule lin)
    subgoal by linarith
    subgoal by simp

    apply (simp add: Misc.subset_Collect_conv, intro allI impI conjI)
    subgoal
      by (auto simp add: quicksort_post_def)
    subgoal
      apply (rule sorted_sublist_map_entire)
      by (auto simp add: quicksort_post_def dest: mset_eq_length)
    done
qed

lemma full_quicksort_correct:
  assumes
    trans: x y z. R (h x) (h y); R (h y) (h z)  R (h x) (h z) and
    lin: x y. R (h x) (h y)  R (h y) (h x)
  shows full_quicksort R h xs   Id (SPEC(λxs'. mset xs' = mset xs))
  by (rule order_trans[OF full_quicksort_correct_sorted])
    (use assms in auto)

end