Theory Sorting_Misc

✐‹creator "Peter Lammich"›
✐‹contributor "Maximilian P. L. Haslbeck"›
section ‹Additional Basic Theorems for Verifying Sorting Algorithms›
theory Sorting_Misc
imports "../../sepref/Sepref" "../../sepref/Hnr_Primitives_Experiment" "HOL-Library.Discrete"
begin
hide_const (open) pi Word.slice

paragraph ‹Summary›
text ‹This theory introduces additional NREST Rules for Loops, refinement relations for refining
    slices of lists, and some guarded specifications of operations on nats.›


subsection ‹Additional NREST Rules for Loops›
⌦‹
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,_) nrest ⇒ ('a,_) nrest ⇒ ('a,_) nrest ⇒ ('a,_) nrest" ("(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: "mono2 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_flat_gfp_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])
    subgoal by simp
    subgoal apply (drule trimonoD_flatf_ge) by simp
    subgoal by (rule RS) simp_all 
    done


  lemma RECT'_dep_refine:
  fixes body :: "('b ⇒ ('c, (char list, enat) acost) nrest)
   ⇒ 'b ⇒ ('c, (char list, enat) acost) nrest"
    assumes M: "mono2 body"
    assumes wfRE: "wfR'' E"
    assumes spE: "struct_preserving E"
    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) (timerefine E (f' x')); (x,x')∈R arb ⟧ 
      ⟹ body f x ≤⇓(S arb x) (timerefine E (body' f' x'))"
    shows "RECT' (λf x. body f x) x ≤⇓SS (timerefine E (RECT' (λf' x'. body' f' x') x'))"
    unfolding RECT'_def
  apply(rule consume_refine[OF wfRE])
  subgoal using spE[THEN struct_preservingD(1)] by simp
  unfolding RECT_flat_gfp_def
    unfolding RECT_flat_gfp_def S0
    apply (clarsimp simp add: M[THEN RECT'_unfold_aux])
  
    apply (rule flatf_fixp_dep_transfer[where 
          fp'="flatf_gfp (λD. body (λx. NREST.consume (D x) (cost ''call'' 1)))" 
      and B'="(λD. body (λx. NREST.consume (D x) (cost ''call'' 1)))" 
      and P="λarb x x'. (x',x)∈R arb"
      and arb⇩0=arb⇩0, 
      OF _ _ flatf_ord.fixp_unfold[OF M[THEN RECT'_unfold_aux,THEN trimonoD_flatf_ge]] R0])
    subgoal by simp
    subgoal apply (drule trimonoD_flatf_ge) by simp
    subgoal  apply(rule RS)
   apply(rule consume_refine[OF wfRE])
      subgoal using spE[THEN struct_preservingD(1)] by simp
      apply simp apply simp
      done
    done


subsection ‹Refinement Relations for Slices of Lists›

  
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
  
(* WRONG with time! m may consume time!
lemma specify_left_pw: "⟦ nofailT m; ⋀v b. (∃b. inresT (project_acost b m) v t) ⟹ f v ≤ m' ⟧ ⟹ doN { v←m; f v} ≤ m'"
  apply (auto simp: pw_acost_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, hide_lams) 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 satminus_zero_if_less_zero: "satminus t x = 0 ⟹ x≤x' ⟹ satminus t x' = 0"
  by(auto simp: satminus_def split: if_splits)

lemma helpe: "x ≤ y ⟹ (the_acost (x) b::enat) ≤ the_acost (y) b"
  by(cases x; cases y; auto simp: less_eq_acost_def)

lemma slice_nth_refine':
  ― ‹only if running time of mop_list_get does not depend on its length, this theorem is true›
  assumes T_indep: "⋀x y. T x = T y" 
  shows "⟦(xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l⟧  
  ⟹ mop_list_get T xs i ≤⇓Id (mop_list_get T xs' i')"  
  apply (auto simp: pw_acost_le_iff refine_pw_simps idx_shift_rel_def)
      apply (auto simp:  slice_rel_def in_br_conv slice_nth algebra_simps)   
  by (metis assms)   
  
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':
  ― ‹only if running time of mop_list_get does not depend on its length, this theorem is true›
  assumes T_indep: "⋀x y. T x = T y" 
  shows "⟦ (xs,xs')∈slice_rel xs⇩0 l h; (i,i')∈idx_shift_rel l; (x,x')∈Id ⟧ 
  ⟹ mop_list_set T xs i x ≤⇓(slice_rel xs⇩0 l h) (mop_list_set T xs' i' x')"  
  apply (auto simp: pw_acost_le_iff refine_pw_simps)
  apply (auto simp: slice_rel_def in_br_conv slice_upd idx_shift_rel_def algebra_simps)   
  by (metis assms)   
    
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

  
  
  
  
  
  
subsection ‹Setup concerned with word length›
  
  
(* 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 [named_ss llvm_inline] = 
  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)
    by (simp add: size_fits_snat_aux take_bit_nat_eq_self)
    
end    

    
lemma LENGTH_refine[sepref_fr_rules]: 
  "LENGTH('a)>2 ⟹ (uncurry0 (return (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 ⟹ (return 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)
  


subsection ‹Monadic Operations on nats›

(* TODO: Move *)  
(* Assertion-guarded operations on nats, which are going to be refined to bounded numbers *)
    named_theorems mop_nat_defs

context
  fixes T :: "(unit * unit) ⇒ (string, enat) acost"
begin

  definition mop_sub :: "nat ⇒ nat ⇒ (nat,_) nrest" where [simp]: "mop_sub a b ≡ doN { ASSERT (a≥b); consume (RETURN (a-b)) (T ((),())) }"
  definition mop_add_bnd :: "nat ⇒ nat ⇒ nat ⇒ (nat,_) nrest" where [simp]: "mop_add_bnd h a b ≡ doN { ASSERT (a+b≤h); consume (RETURN (a+b)) (T ((),()))   }"
  definition mop_div :: "nat ⇒ nat ⇒ (nat,_) nrest" where [simp]: "mop_div a b ≡ doN { ASSERT (b≠0); consume (RETURN (a div b)) (T ((),()))  }"

end

(* TODO: move *)
lemma satminus_0_iff: "satminus t x = 0 ⟷ enat t ≤ x"
  by(auto simp: satminus_def)

definition "mop_nat_sub ≡ mop_sub (λ_. cost ''sub'' 1)"
lemma mop_nat_sub_alt[mop_nat_defs]: "mop_nat_sub a b = doN { ASSERT (a≥b); SPECc2 ''sub'' (-) a b}"
  by(auto simp: mop_nat_sub_def SPECc2_def pw_acost_eq_iff refine_pw_simps satminus_0_iff)

definition "mop_nat_add_bnd ≡ mop_add_bnd (λ_. cost ''add'' 1)"
lemma mop_nat_add_bnd_alt[mop_nat_defs]: "mop_nat_add_bnd h a b = doN { ASSERT (a+b≤h); SPECc2 ''add'' (+) a b}"
  by(auto simp: mop_nat_add_bnd_def SPECc2_def pw_acost_eq_iff refine_pw_simps satminus_0_iff)

definition "mop_nat_div ≡ mop_div (λ_. cost ''udiv'' 1)"
lemma mop_nat_div_alt[mop_nat_defs]: "mop_nat_div a b = doN { ASSERT (b≠0); SPECc2 ''udiv'' (div) a b}"
  by(auto simp: mop_nat_div_def SPECc2_def pw_acost_eq_iff refine_pw_simps satminus_0_iff)

  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)"

  thm sepref_fr_rules

    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