Theory Examples.Sorting_Misc

theory Sorting_Misc
imports "Isabelle_LLVM.IICF" "HOL-Library.Discrete"
begin
  hide_const (open) pi Word.slice


lemma WHILEIT_unfold': "WHILEIT I b c s = doN { ASSERT (I s); if b s then doN { s←c s; WHILEIT I b c s } else RETURN s }"
  apply (rewrite in "⌑=_" WHILEIT_unfold)
  by (auto)

  
(* TODO: Move *)  
lemma WHILEIT_rule_amend_invar:
  assumes "wf R"
  assumes "I s" "I⇩0 s"
  assumes "⋀s. ⟦I s; I⇩0 s; b s⟧ ⟹ f s ≤ SPEC (λs'. I s' ∧ I⇩0 s' ∧ (s', s) ∈ R)"
  assumes "⋀s. ⟦I s; I⇩0 s; ¬ b s⟧ ⟹ Φ s"
  shows "WHILEIT I⇩0 b f s ≤ SPEC Φ"
  apply (rule order_trans)  
  apply (rule WHILEIT_weaken[where I="λs. I s ∧ I⇩0 s"])
  apply simp
  apply (rule WHILEIT_rule)
  apply fact
  using assms by auto
  

(* TODO: Move *)
abbreviation monadic_If :: "bool nres ⇒ 'a nres ⇒ 'a nres ⇒ 'a nres" ("(if⇩N (_)/ then (_)/ else (_))" [0, 0, 10] 10)
  where "monadic_If b x y ≡ doN { t ← b; if t then x else y }"
  
(* TODO: Move *)
lemma monadic_WHILEIT_rule:
  assumes "wf R"
  assumes "I s"
  assumes STEP: "⋀s. I s ⟹ b s ≤ SPEC (λr. if r then c s ≤ SPEC (λs'. I s' ∧ (s',s)∈R) else Φ s)"
  shows "monadic_WHILEIT I b c s ≤ SPEC Φ"
  using ‹wf R› ‹I s› apply (induction s rule: wf_induct_rule)
  apply (subst monadic_WHILEIT_unfold)
  apply (refine_vcg)
  apply (rule STEP[THEN order_trans], assumption)
  apply (refine_vcg)
  subgoal
    apply (split if_splits; simp)
    apply (rule order_trans, assumption)
    apply (refine_vcg)
    apply blast
    done
  subgoal
    by auto  
  done

(* Required as VCG-rule when using monadic_WHILEIT_rule *)    
lemma split_ifI: "⟦ b⟹P; ¬b⟹Q ⟧ ⟹ If b P Q" by simp 
  

  (* TODO: Move *)  
  lemma flatf_fixp_dep_transfer:
    ― ‹Transfer rule for fixed points›
    assumes TR_BOT[simp]: "⋀x x' arb m. tr arb x x' b m"
    assumes MONO: "flatf_mono b B"
    assumes FP': "fp' = B' fp'"
    assumes R0: "P arb⇩0 x x'"
    assumes RS: "⋀f f' x x' arb.
       ⟦⋀x x' arb. P arb x x' ⟹ tr arb x x' (f x) (f' x'); P arb x x'; fp' = f'⟧
       ⟹ tr arb x x' (B f x) (B' f' x')"
    shows "tr arb⇩0 x x' (flatf_fp b B x) (fp' x')"
    supply rl=flatf_fp_induct_pointwise[where 
      pre="λ(a,x) y. P a y x" and a="(arb⇩0,_)" and
      post="λ(a,x') x fp. tr a x x' fp (fp' x')"
      , OF _ MONO]
    apply (rule rl[simplified])
    apply clarsimp
    apply (rule R0)
    apply (subst FP')
    apply clarsimp
    apply (blast intro: RS)
    done
    
  lemma RECT_dep_refine:
    assumes M: "trimono body"
    assumes R0: "(x,x')∈R arb⇩0"
    assumes S0: "SS = S arb⇩0 x"
    assumes RS: "⋀f f' x x' arb. ⟦ ⋀x x' arb. (x,x')∈R arb ⟹ f x ≤⇓(S arb x) (f' x'); (x,x')∈R arb ⟧ 
      ⟹ body f x ≤⇓(S arb x) (body' f' x')"
    shows "RECT (λf x. body f x) x ≤⇓SS (RECT (λf' x'. body' f' x') x')"
    unfolding RECT_def S0
    apply (clarsimp simp add: M)
  
    apply (rule flatf_fixp_dep_transfer[where 
          fp'="flatf_gfp body" 
      and B'=body 
      and P="λarb x x'. (x',x)∈R arb"
      and arb⇩0=arb⇩0, 
      OF _ _ flatf_ord.fixp_unfold[OF M[THEN trimonoD_flatf_ge]] R0])
    apply simp
    apply (simp add: trimonoD)
    by (rule RS)
  
  
  
lemma sorted_lelI:
  assumes "transp R"
  assumes "sorted_wrt R xs⇩1"  
  assumes "sorted_wrt R xs⇩2"  
  assumes "xs⇩1≠[] ⟹ R (last xs⇩1) x"
  assumes "∀y∈set xs⇩2. R x y"
  shows "sorted_wrt R (xs⇩1@x#xs⇩2)"
  using assms
  apply (cases xs⇩1 rule: rev_cases)
  apply (auto simp: sorted_wrt_append dest: transpD)
  done
  
(* TODO: Move *) thm specify_left
lemma specify_left_pw: "⟦ nofail m; ⋀v. inres m v ⟹ f v ≤ m' ⟧ ⟹ doN { v←m; f v} ≤ m'"
  by (auto simp: pw_le_iff refine_pw_simps)


(* TODO: Move, replace Misc.slice_Len lemma *)
declare Misc.slice_len[simp del]
lemma slice_len[simp]: "⟦ to ≤ length xs ⟧ ⟹ length (Misc.slice from to xs) = to - from"
  unfolding Misc.slice_def
  by simp

lemma slice_empty_range[simp]: "h≤l ⟹ Misc.slice l h xs = []"  
  unfolding Misc.slice_def
  by simp
  
lemma slice_upd: "⟦l < h; h ≤ length xs; i < h - l⟧ ⟹ (Misc.slice l h xs)[i:=x] = Misc.slice l h (xs[l + i := x])"
  unfolding Misc.slice_def
  by (simp add: drop_update_swap)
  
lemma slice_map: "Misc.slice l h (map f xs) = map f (Misc.slice l h xs)"
  unfolding Misc.slice_def 
  by (simp add: drop_map take_map)

lemma slice_upd_sym: "⟦l ≤i; i<h; h ≤ length xs⟧ ⟹ Misc.slice l h (xs[i := x]) = (Misc.slice l h xs)[i-l:=x]"
  unfolding Misc.slice_def
  by (simp add: drop_update_swap)
  
lemma take_slice: "take n (slice l h xs) = slice l (min h (l+n)) xs"
  apply (clarsimp simp: Misc.slice_def min_def)
  using le_add_diff_inverse by fastforce

lemma drop_slice: "drop n (slice l h xs) = slice (l+n) h xs"  
  by (auto simp: Misc.slice_def drop_take algebra_simps)
  
lemma slice_Suc_conv: "⟦l≤h; Suc h≤length xs⟧ ⟹ slice l (Suc h) xs = slice l h xs @ [xs!h]"  
  apply (auto simp add: list_eq_iff_nth_eq slice_nth nth_append)
  by (metis Nat.le_imp_diff_is_add Suc_diff_le add.commute less_antisym)
  
  
(* TODO: Move *)
lemma swap_nth1[simp]: "⟦i<length xs ⟧ ⟹ swap xs i j ! i = xs!j"
  by (auto simp: swap_def nth_list_update')

(* TODO: Move *)
lemma swap_nth2[simp]: "⟦j<length xs ⟧ ⟹ swap xs i j ! j = xs!i"
  by (auto simp: swap_def nth_list_update')

lemma swap_indep[simp]: "⟦k≠i; k≠j⟧ ⟹ swap xs i j ! k = xs!k"  
  by (auto simp: swap_def nth_list_update')

(* TODO: Move *)  
lemma slice_swap: "⟦i∈{l..<h}; j∈{l..<h}; h≤length xs⟧ ⟹ Misc.slice l h (swap xs i j) = swap (Misc.slice l h xs) (i-l) (j-l)"  
  unfolding Misc.slice_def swap_def
  by (auto simp: drop_update_swap)
  
lemma take_swap_outside[simp]: "l≤i ⟹ l≤j ⟹ take l (swap xs i j) = take l xs"  
  by (simp add: More_List.swap_def)

lemma drop_swap_outside[simp]: "i<h ⟹ j<h ⟹ drop h (swap xs i j) = drop h xs"  
  by (simp add: More_List.swap_def)

    
lemma slice_append:
  "⟦l≤m; m≤h⟧ ⟹ Misc.slice l m xs @ Misc.slice m h xs = Misc.slice l h xs"  
  apply (auto simp: Misc.slice_def)
  by (metis Nat.add_diff_assoc2 add_diff_cancel_left' drop_drop le_Suc_ex le_add_diff_inverse2 take_add)
  
    

(* TODO: Move *)  
lemma slice_extend1_left: "⟦0<l; l≤h; h≤length xs⟧ ⟹ slice (l-Suc 0) h xs = xs!(l-Suc 0) # slice l h xs"
  apply (rule nth_equalityI)
  by (auto simp: slice_nth nth_Cons split: nat.splits)
  
lemma slice_swap_outside:
  "⟦i∉{l..<h}; j∉{l..<h}⟧ ⟹ slice l h (swap xs i j) = slice l h xs"
  unfolding Misc.slice_def swap_def
  apply simp
  by (metis drop_take drop_upd_irrelevant leI take_update_cancel)
  

  
  
  
lemma set_slice_conv: "⟦ h≤length xs ⟧ ⟹ set (slice l h xs) = { xs!i | i. i∈{l..<h} }"  
  apply (safe;clarsimp simp: in_set_conv_nth)
  subgoal
    by (metis add.commute dual_order.strict_trans2 le_add2 less_diff_conv slice_nth)
  subgoal
    by (smt Misc.slice_def add_diff_inverse_nat diff_less_mono dual_order.trans leD less_imp_le_nat nth_drop nth_take)
  done
  
lemma set_slice_subsetI: "⟦ l'≤l; h≤h' ⟧ ⟹ set (slice l h xs) ⊆ set (slice l' h' xs)"
  unfolding Misc.slice_def
  apply auto
  by (metis (no_types) drop_take in_mono min.absorb1 set_drop_subset_set_drop set_take_subset subset_eq take_take)

  
lemma slice_singleton[simp]: "l<length xs ⟹ slice l (Suc l) xs = [xs!l]"  
  by (simp add: Misc.slice_def drop_Suc_nth)
  
  
lemma slice_split_hd: "⟦l<h; h≤length xs⟧ ⟹ slice l h xs = xs!l # slice (Suc l) h xs"  
  apply (auto simp: Misc.slice_def)
  by (metis Suc_diff_Suc drop_Suc_nth less_le_trans take_Suc_Cons)
  
  
    
      
definition "slice_eq_mset l h xs xs' ≡ length xs = length xs' ∧ take l xs = take l xs' ∧ mset (Misc.slice l h xs) = mset (Misc.slice l h xs') ∧ drop h xs = drop h xs'"    

lemma slice_eq_mset_refl[simp, intro!]: "slice_eq_mset l h xs xs" by (auto simp: slice_eq_mset_def)
lemma slice_eq_mset_sym[sym]: "slice_eq_mset l h xs xs' ⟹ slice_eq_mset l h xs' xs"
  unfolding slice_eq_mset_def by auto
lemma slice_eq_mset_trans[trans]: "⟦ slice_eq_mset l h xs⇩1 xs⇩2; slice_eq_mset l h xs⇩2 xs⇩3 ⟧ ⟹ slice_eq_mset l h xs⇩1 xs⇩3"
  by (auto simp: slice_eq_mset_def)

    
lemma slice_eq_mset_swapI: "⟦i∈{l..<h}; j∈{l..<h}; h≤length xs⟧ ⟹ slice_eq_mset l h (swap xs i j) xs"  
  by (auto simp: slice_eq_mset_def slice_swap)

lemma slice_eq_mset_swap[simp]: 
  "⟦i∈{l..<h}; j∈{l..<h}; h≤length ys ⟧ ⟹ slice_eq_mset l h (swap xs i j) ys ⟷ slice_eq_mset l h xs ys"  
  "⟦i∈{l..<h}; j∈{l..<h}; h≤length xs ⟧ ⟹ slice_eq_mset l h (swap xs i j) ys ⟷ slice_eq_mset l h xs ys"  
  "⟦i∈{l..<h}; j∈{l..<h}; h≤length ys ⟧ ⟹ slice_eq_mset l h xs (swap ys i j) ⟷ slice_eq_mset l h xs ys"  
  "⟦i∈{l..<h}; j∈{l..<h}; h≤length xs ⟧ ⟹ slice_eq_mset l h xs (swap ys i j) ⟷ slice_eq_mset l h xs ys"  
  by (auto simp: slice_eq_mset_def slice_swap)
  
  
  
lemma slice_eq_mset_eq_length: "slice_eq_mset l h xs xs' ⟹ length xs = length xs'"
  by (auto simp: slice_eq_mset_def)
  
lemma slice_eq_mset_eq_outside:
  assumes "slice_eq_mset l h xs xs'"  
  shows "h'≤l ⟹ slice l' h' xs = slice l' h' xs'"
    and "h≤l' ⟹ slice l' h' xs = slice l' h' xs'"
  using assms
  apply (clarsimp_all simp: slice_eq_mset_def Misc.slice_def)  
  apply (metis drop_take min.absorb1 take_take)
  by (metis drop_eq_mono)
  
lemma slice_eq_mset_nth_outside:  
  "⟦ slice_eq_mset l h xs xs'; i∉{l..<h}; i<length xs⟧ ⟹ xs!i = xs'!i"
  unfolding slice_eq_mset_def
  apply clarsimp
  by (smt drop_eq_mono hd_drop_conv_nth leI length_take list_update_id min_def nth_list_update_eq take_update)
  
lemma slice_eq_mset_set_inside: 
  "⟦ slice_eq_mset l h xs xs' ⟧ ⟹ set (slice l h xs) = set (slice l h xs')" 
  unfolding slice_eq_mset_def by (auto dest: mset_eq_setD)

lemma slice_eq_mset_subslice: "⟦ slice_eq_mset l' h' xs xs'; l≤l'; l'≤h'; h'≤h ⟧ ⟹ slice_eq_mset l h xs xs'"  
  apply (auto simp: slice_eq_mset_def)
  subgoal by (smt append_eq_append_conv le_Suc_ex length_take take_add)
  subgoal premises assms proof -
    from assms have [simp]:
      "Misc.slice l h xs = Misc.slice l l' xs @ Misc.slice l' h' xs @ Misc.slice h' h xs" 
      "Misc.slice l h xs' = Misc.slice l l' xs' @ Misc.slice l' h' xs' @ Misc.slice h' h xs'" 
      by (auto simp: slice_append)
      
    from assms have [simp]: "Misc.slice l l' xs = Misc.slice l l' xs'"  
      by (simp add: Misc.slice_def take_drop)

    from assms have [simp]: "Misc.slice h' h xs = Misc.slice h' h xs'"  
      by (simp add: Misc.slice_def take_drop)
            
    show ?thesis
      by (simp add: assms)
  qed
  subgoal using drop_eq_mono by blast
  done


(* TODO: Move *)

definition "slice_rel xs⇩0 l h ≡ br (Misc.slice l h) (λxs. l≤h ∧ h≤length xs ∧ length xs=length xs⇩0 ∧ take l xs = take l xs⇩0 ∧ drop h xs = drop h xs⇩0)"
  
definition  idx_shift_rel :: "nat ⇒ nat rel" where "idx_shift_rel s ≡ {(i,i'). i = i'+s}"

lemma idx_shift_rel_alt: "l≤ii ⟹ (ii,i)∈idx_shift_rel l ⟷ i=ii-l"
  by (auto simp: idx_shift_rel_def)


lemma slice_nth_refine: "⟦ (xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l; i<h ⟧ ⟹ xs!i = xs'!i'"  
  by (auto simp: slice_rel_def in_br_conv slice_nth idx_shift_rel_def algebra_simps)

lemma slice_nth_refine': "⟦(xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l⟧  
  ⟹ mop_list_get xs i ≤⇓Id (mop_list_get xs' i')"  
  apply (auto simp: pw_le_iff refine_pw_simps idx_shift_rel_def)
  by (auto simp: slice_rel_def in_br_conv slice_nth algebra_simps)
  
  
lemma slice_upd_refine: "⟦ (xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l; i<h; (x,x')∈Id ⟧ 
  ⟹ (xs[i:=x], xs'[i':=x'])∈slice_rel xs⇩0 l h"  
  by (auto simp: slice_rel_def in_br_conv slice_upd idx_shift_rel_def algebra_simps)

lemma slice_upd_refine': "⟦ (xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l; (x,x')∈Id ⟧ 
  ⟹ mop_list_set xs i x ≤⇓(slice_rel xs⇩0 l h) (mop_list_set xs' i' x')"  
  apply (auto simp: pw_le_iff refine_pw_simps)
  by (auto simp: slice_rel_def in_br_conv slice_upd idx_shift_rel_def algebra_simps)
    
lemma slice_in_slice_rel[simp]: "⟦l≤h; h≤length xs⟧ ⟹ (xs, Misc.slice l h xs) ∈ slice_rel xs l h"  
  unfolding slice_rel_def in_br_conv by auto

  
lemma slice_rel_rebase: "(xsi', xs) ∈ slice_rel xsi l h ⟹ slice_rel xsi l h = slice_rel xsi' l h"
  by (auto simp: slice_rel_def in_br_conv)


  
  
  
(* TODO: Move *)  
  
  definition "list_rel_on R I xs ys ≡ I⊆{0..<length ys} ∧ length xs = length ys ∧ (∀i∈I. R (xs!i) (ys!i))"

  lemma list_rel_on_gen_trans[trans]: "list_rel_on R⇩1 I⇩1 xs ys ⟹ list_rel_on R⇩2 I⇩2 ys zs ⟹ list_rel_on (R⇩1 OO R⇩2) (I⇩1∩I⇩2) xs zs"
    unfolding list_rel_on_def 
    by auto
    
  lemma list_rel_on_gen_trans'[trans]: "⟦list_rel_on R⇩1 I⇩1 xs ys; list_rel_on R⇩2 I⇩2 ys zs; R'=R⇩1 OO R⇩2; I'=I⇩1∩I⇩2⟧ ⟹ list_rel_on R' I' xs zs"
    unfolding list_rel_on_def 
    by auto
  
  lemma list_rel_on_empty: "list_rel_on R {} xs ys ⟷ length xs = length ys"  
    unfolding list_rel_on_def 
    by auto

  lemma list_rel_on_whole: "list_rel_on R {0..<length ys} xs ys ⟷ list_all2 R xs ys"      
    unfolding list_rel_on_def 
    by (auto simp: list_all2_conv_all_nth)

  lemma list_rel_on_combine: "list_rel_on R⇩1 I⇩1 xs ys ⟹ list_rel_on R⇩2 I⇩2 xs ys ⟹ list_rel_on (sup R⇩1 R⇩2) (I⇩1∪I⇩2) xs ys"  
    unfolding list_rel_on_def 
    by auto

  lemma list_rel_on_mono: "R⇩1≤R⇩2 ⟹ I⇩2⊆I⇩1 ⟹ list_rel_on R⇩1 I⇩1 ≤ list_rel_on R⇩2 I⇩2"  
    unfolding list_rel_on_def 
    by auto

  lemma list_rel_on_union: "list_rel_on R (I⇩1∪I⇩2) xs ys ⟷ list_rel_on R I⇩1 xs ys ∧ list_rel_on R I⇩2 xs ys"
    unfolding list_rel_on_def 
    by auto
      
  lemma list_rel_on_lenD: "list_rel_on R I xs ys ⟹ length xs = length ys"          
    unfolding list_rel_on_def 
    by auto
    

  definition "slicep_rel l h ≡ {(xsi,xs). xs=slice l h xsi ∧ l≤h ∧ h≤length xsi}"  
     
  definition "eq_outside_range xs xs⇩0 l h ≡ l≤h ∧ h≤length xs⇩0 ∧ length xs=length xs⇩0 ∧ take l xs = take l xs⇩0 ∧ drop h xs = drop h xs⇩0"
  lemma eq_outside_range_list_rel_on_conv: 
    "eq_outside_range xs ys l h ⟷ l≤h ∧ h≤length xs ∧ list_rel_on (=) ({0..<l}∪{h..<length ys}) xs ys"
    unfolding eq_outside_range_def list_rel_on_def
    apply clarsimp
    apply (simp only: list_eq_iff_nth_eq) 
    apply (safe; clarsimp)
    by (metis diff_less_mono le_add_diff_inverse)
  
  lemma eq_outside_rane_lenD: "eq_outside_range xs xs⇩0 l h ⟹ length xs = length xs⇩0"
    unfolding eq_outside_range_def by auto

  lemma eq_outside_range_gen_trans: "⟦eq_outside_range xs ys l h; eq_outside_range ys zs l' h'; ll=min l l'; hh=max h h'⟧ 
    ⟹ eq_outside_range xs zs ll hh"  
    unfolding eq_outside_range_list_rel_on_conv
    apply (safe; (clarsimp simp: list_rel_on_lenD)?)
    subgoal by auto
    subgoal
      apply (clarsimp simp: list_rel_on_union; intro conjI)
      apply (erule (1) list_rel_on_gen_trans'[where I⇩1="{0..<l}" and I⇩2="{0..<l'}"]; auto)
      apply (erule (1) list_rel_on_gen_trans'[where I⇩1="{h..<_}" and I⇩2="{h'..<_}"]; auto)
      done
    done  

  lemma eq_outside_range_triv: "eq_outside_range xs xs l h ⟷ l ≤ h ∧ h ≤ length xs"  
    unfolding eq_outside_range_def
    by simp
    
  
  lemma eq_outside_range_sym: "eq_outside_range xs xs' l h ⟹ eq_outside_range xs' xs l h"
    unfolding eq_outside_range_def by auto
    
          
  lemma slice_rel_alt: "(xsi,xs)∈slice_rel xs⇩0 l h ⟷ (xsi,xs)∈slicep_rel l h ∧ eq_outside_range xsi xs⇩0 l h"
    unfolding slice_rel_def slicep_rel_def eq_outside_range_def in_br_conv
    by auto
   
  lemma slice_eq_outside_range: "⟦eq_outside_range xs ys l h; {l..<h}∩{l'..<h'}={}⟧ ⟹ slice l' h' xs = slice l' h' ys"
    unfolding Misc.slice_def eq_outside_range_def
    apply simp apply (safe;clarsimp?)
    subgoal by (metis drop_take le_def min.absorb1 take_take) 
    subgoal by (metis drop_eq_mono leI) 
    subgoal by (metis append_take_drop_id)
    done
    
  lemma slicep_rel_eq_outside_range: "⟦eq_outside_range xs ys l h; {l..<h}∩{l'..<h'}={}⟧ 
    ⟹ (xs,ss)∈slicep_rel l' h' ⟷ (ys,ss)∈slicep_rel l' h'"
    unfolding slicep_rel_def
    by (auto simp add: slice_eq_outside_range eq_outside_rane_lenD)
        
  lemma slicep_rel_append: "⟦ (xs,ys⇩1)∈slicep_rel l m; (xs,ys⇩2)∈slicep_rel m h ⟧ ⟹ (xs, ys⇩1@ys⇩2)∈slicep_rel l h"
    unfolding slicep_rel_def
    by (auto simp: slice_append)
  
  lemma slicep_rel_take: "⟦(xsi, xs) ∈ slicep_rel l h; n≤length xs⟧ ⟹ (xsi, take n xs) ∈ slicep_rel l (n+l)"
    unfolding slicep_rel_def
    by (auto simp: take_slice algebra_simps)
  
  lemma slicep_rel_drop: "⟦(xsi, xs) ∈ slicep_rel l h; n≤length xs⟧ ⟹ (xsi, drop n xs) ∈ slicep_rel (n+l) h"
    unfolding slicep_rel_def
    by (auto simp: drop_slice algebra_simps)
  
  
  lemma eq_outside_range_nth:
    "eq_outside_range xs xs' l h ⟹ i<l ⟹ xs!i = xs'!i"
    "eq_outside_range xs xs' l h ⟹ h≤i ⟹ xs!i = xs'!i"
    unfolding eq_outside_range_def
    apply (clarsimp_all)
    subgoal by (metis nth_take)
    subgoal by (metis le_Suc_ex nth_drop)
    done
    
  lemma eq_outside_erange_upd_inside: "⟦ i∈{l..<h} ⟧ ⟹ eq_outside_range xs (xs'[i:=x]) l h ⟷ eq_outside_range xs xs' l h"
    unfolding eq_outside_range_def
    by auto
  
    
    
(* TODO: Unify these concepts! *)
lemma slice_eq_mset_alt: 
  "⟦l≤h; h≤length xs'⟧ ⟹ slice_eq_mset l h xs xs' ⟷ eq_outside_range xs xs' l h ∧ mset (slice l h xs) = mset (slice l h xs')"
  unfolding slice_eq_mset_def eq_outside_range_def by auto

  
  
  
  
  
  
  
  
(* TODO: Move *)
lemma unat_gtZ_prenorm[fcomp_prenorm_simps]: "(x,y)∈unat_rel ⟹ 0<x ⟷ 0<y"
  by (simp add: in_br_conv unat.rel_def unat_gt_0 unat_rel_def word_neq_0_conv)

lemma snat_gtZ_prenorm[fcomp_prenorm_simps]: "(x,y)∈snat_rel ⟹ 0<x ⟷ 0<y"
  by (simp add: in_br_conv snat.rel_def snat_eq_unat(2) unat_gt_0 snat_rel_def word_neq_0_conv)



(* TODO: Move *)
lemma word_log2_zero[simp]: "word_log2 0 = 0"
  unfolding word_log2_def word_size by auto

lemma word_clz_1[simp]: "word_clz (1::'a::len word) = LENGTH ('a) - 1"
  unfolding word_clz_def
  apply (simp add: to_bl_1)
  by (simp add: takeWhile_replicate takeWhile_tail)

  
  
(* CG-pre setup for LENGTH constants *)
lemmas [llvm_pre_simp] = len_of_numeral_defs of_nat_numeral
  
(* Sepref setup for LENGTH *)
  
sepref_register "LENGTH(_)"

context begin
  lemma size_fits_snat_aux: "x < 2^(x-Suc 0) ⟷ x=0 ∨ x>2"
    by (smt diff_Suc_1 gr0_implies_Suc le0 le_less_trans less_numeral_extra(4) less_one linorder_neqE_nat nat_neq_iff not_less_eq not_numeral_less_one numeral_2_eq_2 order_less_irrefl power_0 power_one_right suc_le_pow_2 zero_diff zero_less_one)
  
  lemma size_fits_snat_aux2: "LENGTH('a)>2 ⟹ snat_invar (of_nat LENGTH('a) :: 'a::len2 word)"
    unfolding snat_invar_alt
    apply (rule exI[where x = "LENGTH('a) - 1"])
    apply (auto simp: unat_of_nat size_fits_snat_aux)
    done
    
end    

    
lemma LENGTH_refine[sepref_fr_rules]: 
  "LENGTH('a)>2 ⟹ (uncurry0 (Mreturn (of_nat (LENGTH('a::len2))::'a word)), uncurry0 (RETURN (PR_CONST LENGTH('a)))) ∈ unit_assn⇧k →⇩a snat_assn"
  apply sepref_to_hoare
  unfolding snat_rel_def snat.rel_def 
  supply [simp] = in_br_conv word_size size_fits_snat_aux2
  apply vcg'
  by (metis n_less_equal_power_2 size_fits_snat_aux2 snat_eq_unat_aux2 unat_of_nat_len)

lemma size_refine[sepref_fr_rules]: "LENGTH('a)>2 ⟹ (Mreturn o (λ_. of_nat (LENGTH('a))), RETURN o size) ∈ (word_assn' TYPE('a::len2))⇧k →⇩a snat_assn' TYPE('a)"
  apply sepref_to_hoare
  unfolding snat_rel_def snat.rel_def 
  supply [simp] = in_br_conv word_size size_fits_snat_aux2
  apply vcg'
  by (metis n_less_equal_power_2 of_nat_inverse size_fits_snat_aux2 snat_eq_unat_aux2)
  
  
(* TODO: Move *)  
(* Assertion-guarded operations on nats, which are going to be refined to bounded numbers *)
    named_theorems mop_nat_defs

  definition mop_nat_sub :: "nat ⇒ nat ⇒ nat nres" where [mop_nat_defs]: "mop_nat_sub a b ≡ doN { ASSERT (a≥b); RETURN (a-b) }"
  definition mop_nat_add_bnd :: "nat ⇒ nat ⇒ nat ⇒ nat nres" where [mop_nat_defs]: "mop_nat_add_bnd h a b ≡ doN { ASSERT (a+b≤h); RETURN (a+b) }"
  definition mop_nat_div :: "nat ⇒ nat ⇒ nat nres" where [mop_nat_defs]: "mop_nat_div a b ≡ doN { ASSERT (b≠0); RETURN (a div b) }"
  
  sepref_register mop_nat_sub mop_nat_add_bnd mop_nat_div
  
  context fixes dummy :: "'l::len2" begin
    private abbreviation (input) "N ≡ snat_assn' TYPE('l)"
  
    sepref_def snat_sub_impl [llvm_inline] is "uncurry mop_nat_sub" :: "N⇧k*⇩aN⇧k→⇩aN"
      unfolding mop_nat_defs by sepref
  
    sepref_def snat_add_bnd_impl [llvm_inline] is "uncurry2 mop_nat_add_bnd" :: "N⇧k*⇩aN⇧k*⇩aN⇧k→⇩aN"
      unfolding mop_nat_defs by sepref
  
    sepref_def snat_div_impl [llvm_inline] is "uncurry mop_nat_div" :: "N⇧k*⇩aN⇧k→⇩aN"
      unfolding mop_nat_defs by sepref

  end    
      

  
  
  
  
  
  
  
  

end