Theory Dynamic_Array

theory Dynamic_Array
  imports "../../sepref/Hnr_Primitives_Experiment" "../../nrest/Refine_Heuristics"
  "../../nrest/NREST_Automation" "../sorting/Sorting_Setup"
  "../../nrest/Synth_Rate"
begin



definition "hide a b = (a=b)"
lemma hideI: "a=b ⟹ hide a b" unfolding hide_def by simp
lemma hide: "hide a b ⟹ a = b" unfolding hide_def by simp


(* TODO: Move *)
lemma wfR''_zero[simp]: "wfR'' 0"
  unfolding wfR''_def by (auto simp: zero_acost_def)

(* TODO: Move *)
lemma nrest_C_relI:
  fixes a :: "(_,ecost) nrest"
  shows "a ≤ ⇓R (⇓⇩C TId b) ⟹ (a,b) ∈ ⟨R⟩nrest_rel"
  apply(rule nrest_relI) by (auto simp: timerefine_id)

(* TODO: Move *)
definition mop_list_length :: "_ ⇒ (_,ecost) nrest" where
  "mop_list_length xs = RETURNT (length xs)"


(* TODO: move *)
lemma one_time_SPECT_map[OT_intros]: "one_time (SPECT [x↦t])"
  unfolding one_time_def by auto


lemma one_time_bind_assert[OT_intros]: "one_time m ⟹ one_time (doN { ASSERT P; m})"
  unfolding one_time_def
  apply(cases P) by auto

(* TODO: Move *)
lemma one_time_uncurry[OT_intros]:
  "(⋀a b. x=(a,b) ⟹ one_time (f a b)) ⟹ one_time (uncurry f x)"
  unfolding uncurry_def 
  by (metis old.prod.case old.prod.exhaust) 

lemma one_time_mop_list_get[OT_intros]: "one_time (mop_list_get T a b)"
  unfolding mop_array_nth_def mop_list_get_def by (intro OT_intros)

lemma one_time_mop_array_nth[OT_intros]: "one_time (mop_array_nth a b)"
  unfolding mop_array_nth_def by (intro OT_intros)


lemma one_time_PR_CONST[OT_intros]: "one_time x ⟹ one_time (PR_CONST x)"
         "one_time (y b) ⟹ one_time (PR_CONST y b)"
         "one_time (z c d) ⟹ one_time (PR_CONST z c d)"
  unfolding PR_CONST_def by simp



subsection ‹Array Copy›

definition "array_copy_impl dst src n = doM {
          return dst      
      }"


definition list_copy_spec where
  "list_copy_spec T dst src n = doN {
       ASSERT (n≤length dst ∧ n≤length src);
       REST [take n src @ drop n dst ↦ T n]
    }"

definition "list_copy_body_cost = (cost ''if'' 1 + cost ''call'' 1 +  mop_array_nth_cost + 
                                         mop_array_upd_cost + cost ''add'' 1 + cost ''icmp_slt'' 1)"
definition list_copy :: "'a list ⇒ 'a list ⇒ nat ⇒ ('a list, ecost) nrest" where
  "list_copy dst src n = doN {
          (dst,_) ← monadic_WHILEIET (λ(dst',n'). n'≤n ∧ length dst' = length dst ∧ dst' = take n' src @ drop n' dst)
              (λ(_::'a list,n'). (n-n') *m list_copy_body_cost )
            (λ(_,n'). SPECc2 ''icmp_slt'' (<) n' n)
            (λ(dst',n'). doN {
              x ← mop_array_nth src n';
              dst'' ← mop_array_upd dst' n' x;
              ASSERT (n'+1≤n);
              n'' ← SPECc2 ''add'' (+) n' 1;
              RETURNT (dst'',n'')
            })
          (dst,0);
          RETURNT dst
      }"

definition "list_copy_spec_time n = (enat (n)) *m (lift_acost list_copy_body_cost)
           + cost ''if'' 1 + cost ''call'' 1 + cost ''icmp_slt'' 1"

lemma list_copy_correct: "(uncurry2 list_copy, uncurry2 (list_copy_spec list_copy_spec_time))
       ∈ Id ×⇩r Id →⇩f ⟨Id⟩nrest_rel"
  apply rule
  apply (rule nrest_relI)    
  unfolding uncurry_def 
  unfolding list_copy_spec_def 
  apply (auto simp add: le_fun_def)    
  apply(rule le_acost_ASSERTI) 
  unfolding list_copy_def
  unfolding list_copy_body_cost_def
  unfolding SPECc2_def mop_array_nth_def mop_list_get_def mop_array_upd_def  mop_list_set_def
  apply(rule gwp_specifies_I)
  apply(refine_vcg ‹-› rules: gwp_monadic_WHILEIET If_le_rule)
  subgoal
    unfolding wfR2_def
    apply (auto simp:  costmult_add_distrib costmult_cost the_acost_propagate zero_acost_def)
      by(auto simp: cost_def zero_acost_def)
  subgoal apply(rule loop_body_conditionI)
    subgoal apply (auto simp: norm_cost) apply(sc_solve) by auto
    subgoal apply (auto simp: norm_cost) apply(sc_solve) by (auto simp: one_enat_def)
    subgoal apply (auto simp: norm_cost) by(simp add: upd_conv_take_nth_drop take_Suc_conv_app_nth)
    done
  subgoal apply auto done
  subgoal apply auto done
  subgoal apply auto done
  subgoal
    apply(rule loop_exit_conditionI)
    apply(refine_vcg ‹-› rules:)
    unfolding list_copy_spec_time_def list_copy_body_cost_def
    apply (auto simp: norm_cost lift_acost_propagate cost_zero)
    apply(sc_solve) by auto
  subgoal apply auto done
  done


(*
declare hnr_array_upd[sepref_fr_rules del] 
lemma hnr_array_upd_ohne_sc[sepref_fr_rules]:
  "CONSTRAINT is_pure A ⟹(uncurry2 array_upd, uncurry2 mop_array_upd) ∈ (array_assn A)⇧d *⇩a snat_assn⇧k *⇩a A⇧k →⇩a array_assn A"
  apply(rule hnr_array_upd)
   apply simp 
  unfolding SC_attains_sup_def
  apply safe
  apply(rule one_time_attains_sup)
  unfolding mop_array_upd_def mop_list_set_def
  unfolding uncurry_def apply simp
  by(intro OT_intros) *)


context size_t_context
begin

  thm hnr_array_upd
  thm hnr_eoarray_upd'

  thm hnr_array_upd

lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "array_assn A" for A]

   sepref_def list_copy_impl is "uncurry2 list_copy"  
     :: "(array_assn (pure R))⇧d *⇩a (array_assn (pure R))⇧k *⇩a size_assn⇧k  →⇩a array_assn (pure R)"
     unfolding  list_copy_def PR_CONST_def  
     unfolding monadic_WHILEIET_def
     apply (annot_snat_const "TYPE('size_t)")
     by sepref 


lemmas list_copy_impl_refine = list_copy_impl.refine 

  thm list_copy_impl.refine

end

thm size_t_context.list_copy_impl_refine
thm size_t_context.list_copy_impl_def

section ‹Misc›




lemma timerefineA_mono:
    assumes "wfR'' R"
    shows "t ≤ t' ⟹ timerefineA R t ≤ timerefineA R (t'::ecost)"
  apply (auto simp: less_eq_acost_def timerefineA_def split: nrest.splits option.splits simp: le_fun_def)
  proof (goal_cases)
    case (1 ac)
    then have l: "⋀ac. the_acost t ac ≤  the_acost t' ac"
      apply(cases t; cases t') unfolding less_eq_acost_def  
      by auto
    show ?case
      apply(rule Sum_any_mono)
      subgoal using l apply(rule ordered_semiring_class.mult_right_mono) by (simp add: needname_nonneg)
      apply(rule wfR_finite_mult_left2) by fact
  qed 



lemma SPECT_assign_emb': "SPECT [x↦t] = SPECT (emb' (λy. y=x) (λ_.t))"
  unfolding emb'_def apply auto done

lemma 
  SPEC_leq_SPEC_I_even_stronger:
  "A ≤ A' ⟹ (⋀x. A x ⟹ B x ≤ (B' x)) ⟹ SPEC A B ≤ (SPEC A' B')"
  apply(auto simp: SPEC_def)
  by (simp add: le_fun_def)  


lemma consume_SPEC_eq: "consume (SPEC Φ T) (t::ecost)= SPEC Φ (λx. T x + t)"
  unfolding SPEC_def consume_def
  apply auto
  apply(rule ext) apply auto 
  using ecost_add_commute by blast

 
lemma meh_special: "b ≥ lift_acost a ⟹ Ca ≤ b - lift_acost a⟹ Ca + lift_acost a ≤ b"
  apply(cases b; cases Ca; cases a) apply auto
  using plus_minus_adjoint_ecost by blast 


lemma plus_minus_adjoint_ecost_I: "b ≥ (a::ecost) ⟹ Ca ≤ b - a⟹ Ca + a ≤ b"
  apply(subst plus_minus_adjoint_ecost[symmetric]) by simp_all

lemma enat_minusrule: "b<∞ ⟹ (a+b)-b = (a::enat)"
  by(cases a; cases b; auto simp: ) 

lemma zz: "(⋀x. the_acost b x < ∞) ⟹ (a+b)-b = (a::ecost)"
  apply(cases a; cases b; auto simp: )
  apply(rule ext) apply(rule enat_minusrule)
  by auto

lemma acost_move_sub_le: "b≥c ⟹ (a+b)-c ≥ (a::(string,nat) acost)"
  apply(cases a; cases b; cases c) apply (auto simp: less_eq_acost_def)
  by (simp add: nat_move_sub_le)


lemma zz3: "b≥c ⟹ (b+a)-c ≥ (a::(string,nat) acost)"
  apply(cases a; cases b; cases c) apply (auto simp: less_eq_acost_def)
  by (simp add: nat_move_sub_le)


lemma add_diff_assoc_ncost: "b≥c ⟹ (a+b)-c = (a::(string,nat) acost) + (b-c)"
  apply(cases a; cases b; cases c) 
  by (auto simp: less_eq_acost_def)


lemma costmult_add_distrib_left:
  fixes a :: "'b::semiring"
  shows "a *m A + b *m A = (a+b) *m A "
  apply(cases A) by (auto simp: costmult_def plus_acost_alt ring_distribs)

lemma costmult_right_mono:
  fixes a :: nat
  shows "a ≤ a' ⟹ a *m c ≤ a' *m c"
  unfolding costmult_def less_eq_acost_def
  by (auto simp add: mult_right_mono)  


lemma cost_mult_zero_enat[simp]:"(0::enat) *m m = (0) "
  by(auto simp: zero_acost_def costmult_def) 
lemma cost_mult_zero_nat[simp]: "(0::nat) *m m = (0) "
  by(auto simp: zero_acost_def costmult_def) 
 


lemma costmult_left_cong: "a=b ⟹ a *m A = b *m A"
  by simp

subsection ‹Stuff about Sum_any›


lemma finite_nonzero_minus: "finite {a. g a ≠ 0} ⟹ finite {a. h a ≠ (0::enat)} ⟹ finite {a. g a - h a ≠ 0}"
  by (metis (mono_tags, lifting) Collect_mono_iff idiff_0 rev_finite_subset)

lemma sum_minus_distrib_enat:
  assumes "⋀a. g a ≥ (h a::enat)"
  shows "finite A ⟹ sum (λa. g a - h a) A = sum g A - sum h A" 
proof (induct rule: finite_induct)
  case (insert x F)
  have *: "sum g F ≥ sum h F"
    apply(rule sum_mono) using assms by auto
  have "(∑a∈insert x F. g a - h a)
      = (g x - h x) + (∑a∈F. g a - h a)"  
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have "… = (g x - h x) + (sum g F - sum h F)"
    by (simp add: insert.hyps(3))
  also have "… = (g x + sum g F) - (h x + sum h F)"
    using assms[of x] * 
    by (metis add.commute add_diff_assoc_enat assms minus_plus_assoc2) 
  also have "… = sum g (insert x F) - sum h (insert x F)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  finally show ?case .
qed simp  

lemma Sum_any_minus_distrib_enat:
  assumes "finite {a. g a ≠ 0}" "finite {a. h a ≠ 0}"
  assumes "⋀a. g a ≥ (h a :: enat)"
  shows "Sum_any (λa. g a - h a) = Sum_any g - Sum_any h"
proof -
  have z: "{a. g a - h a ≠ 0} ⊆ {a. g a ≠ (0::enat)}"
    by auto

  have "Sum_any (λa. g a - h a) = sum (λa. g a - h a)  {a. g a ≠ 0}"
    apply  (rule Sum_any.expand_superset) 
    apply(rule assms(1))
    apply(rule z)
    done
  also have "… = sum g {a. g a ≠ 0} - sum h {a. g a ≠ 0}"
    apply(subst sum_minus_distrib_enat) 
      apply(rule assms(3))
    apply(rule assms(1))
    apply simp done 
  also have "… = Sum_any g - Sum_any h"
    apply(subst Sum_any.expand_set)
    apply(subst Sum_any.expand_superset[OF assms(1)])
    subgoal using assms(3)  apply auto 
      by (metis ile0_eq) 
    apply simp 
    done
  finally show ?thesis .
qed    

lemma diff_mult_sub_distrib_enat:
  shows "(a - b) * (c::enat) ≤ a * c - b * c"
  apply(cases a; cases b; cases c; auto)
  using diff_mult_distrib by simp


(* TODO: move improved version upstream *)
lemma wfR''_finite_mult_left:
  assumes "wfR'' R"
  shows "finite {ac. x ac * the_acost (R ac) cc ≠ 0}"
proof - 
  from assms have "finite {s. the_acost (R s) cc ≠ 0}" unfolding wfR''_def by auto
  show ?thesis
    apply(rule finite_subset[where B="{ac. the_acost (R ac) cc ≠ 0}"])
    subgoal by auto
    subgoal apply fact done
    done
qed 

lemma timerefineA_propagate_minus:
  assumes "wfR'' E"
  fixes a b :: "('a, enat) acost"
  assumes "a≥b"
  shows "timerefineA E (a - b) ≤ timerefineA E a - timerefineA E b"
  unfolding timerefineA_def
  apply(auto simp: less_eq_acost_def minus_acost_alt timerefine_def consume_def timerefineA_def split: nrest.splits option.splits)
  apply(cases a, cases b) 
  apply auto
  unfolding  ring_distribs 
  apply(rule order.trans)
   apply(rule Sum_any_mono)
    apply(rule diff_mult_sub_distrib_enat) 
   apply(rule finite_nonzero_minus)
  subgoal apply(rule wfR''_finite_mult_left) by(rule assms(1))
  subgoal apply(rule wfR''_finite_mult_left) by(rule assms(1))
  apply(subst Sum_any_minus_distrib_enat)
  subgoal apply(rule wfR''_finite_mult_left) by(rule assms(1))
  subgoal apply(rule wfR''_finite_mult_left) by(rule assms(1))
  subgoal apply(rule mult_right_mono) using assms(2) unfolding le_fun_def  by (auto simp: less_eq_acost_def  )
  apply simp
  done

lemma add_increasing2_nat_acost: "(a::(_,nat)acost)≤b ⟹ a≤b+c" 
  apply(cases a; cases b; cases c) apply (auto simp: less_eq_acost_def)  
  by (simp add: add_increasing2)  
lemma add_increasing2_ecost: "(a::ecost)≤b ⟹ a≤b+c" 
  apply(cases a; cases b; cases c) apply (auto simp: less_eq_acost_def)  
  by (simp add: add_increasing2)  


subsection ‹reclaim›


fun reclaim where
  "reclaim FAILi t = FAILT"
| "reclaim (SPECT M) t = Sup { if t'≥t x then SPECT [x↦t' - t x] else FAILT | t' x. M x = Some t' }"




lemma reclaim_nofailT[simp]: "reclaim FAILT t = FAILT"
  unfolding top_nrest_def apply(subst reclaim.simps) by simp

lemma blaD1: "nofailT (reclaim m t) ⟹ nofailT m ∧ (∀M. m=SPECT M ⟶ (∀x t'. M x = Some t' ⟶ t' ≥ t x))"
  apply(cases m)
   apply auto
  unfolding pw_Sup_nofail 
  by force 

lemma blaD2: " nofailT m ∧ (∀M. m=SPECT M ⟶ (∀x t'. M x = Some t' ⟶ t' ≥ t x)) ⟹ nofailT (reclaim m t)"
  apply(cases m)
   apply auto
  unfolding pw_Sup_nofail  
  by auto

lemma nofailT_reclaim:
 "nofailT (reclaim m t) ⟷ (nofailT m ∧ (∀M. m=SPECT M ⟶ (∀x t'. M x = Some t' ⟶ t' ≥ t x)))"
  apply(cases m)
   apply auto
  unfolding pw_Sup_nofail  
  apply force
  by auto
 

lemma reclaim_SPEC: "(⋀x. Q x ⟹ T x ≥ Φ x) ⟹ reclaim (SPEC Q T) (Φ::_⇒ecost) = SPEC Q (λx. T x - Φ x)"
  apply(rule antisym)
  subgoal
    by (auto simp: le_fun_def SPEC_def split: if_splits intro!: Sup_least)
  subgoal    
    by (auto simp: SPEC_def Sup_nrest_def le_fun_def intro!: Sup_upper2)
  done

lemma reclaim_SPEC_le: "SPEC Q (λx. T x - Φ x) ≤ reclaim (SPEC Q T) (Φ::_⇒ecost)"
  apply(cases "nofailT (reclaim (SPEC Q T) (Φ::_⇒ecost))")
  subgoal
    apply(subst (asm) nofailT_reclaim)
    apply (auto simp: nofailT_SPEC )
    apply(subst (asm) SPEC_def) apply (auto split: if_splits) 
    subgoal    
      by (auto simp: SPEC_def Sup_nrest_def le_fun_def intro!: Sup_upper2)
    done
  subgoal unfolding nofailT_def by auto
  done



lemma pull_timerefine_through_reclaim:
  fixes TR :: "_⇒ecost"
  assumes *: "wfR'' TR"
      and ineq: "⋀x. Ψ x ⟹ Φ' x ≤ T x + Φ"
  shows "⇓⇩C TR (reclaim (consume (SPEC Ψ (T::_⇒ecost)) Φ) Φ') ≤
         (reclaim (consume (SPEC Ψ (λx. timerefineA TR ((T::_⇒ecost) x))) (timerefineA TR Φ)) (timerefineA TR o Φ'))"
  apply(subst consume_SPEC_eq)
  apply(subst consume_SPEC_eq)  
  apply(subst reclaim_SPEC) 
    subgoal apply(rule ineq) by simp
  apply(subst reclaim_SPEC) 
    subgoal
     apply(subst timerefineA_propagate[symmetric])
       apply(rule *)     apply simp
      apply(rule timerefineA_mono)
      subgoal by(rule *)   
    subgoal apply(rule ineq) by simp
      done
  apply(subst SPEC_timerefine_conv)
  apply(rule SPEC_leq_SPEC_I_even_stronger)
  subgoal apply auto done
  subgoal apply (subst timerefineA_propagate[symmetric])
     apply(rule *)       apply simp
    apply(rule order.trans[rotated])
     apply(rule timerefineA_propagate_minus)
    subgoal by(rule *)     
    subgoal apply(rule ineq) by simp
    subgoal 
      apply(rule timerefineA_mono)
      subgoal by(rule *)     
      apply simp
      done
    done
  done   

subsection ‹augment_amor_assn›

definition "augment_amor_assn Φ A = (λra r. $Φ ra ** A ra r)"
lemma amor_orthogonal:
  assumes "(C, A) ∈ (assn)⇧k *⇩a S →⇩a R"
  shows "(C, A) ∈ (augment_amor_assn PHI assn)⇧k *⇩a S →⇩a R"
  unfolding augment_amor_assn_def
  apply(rule hfrefI)
  apply (auto)
  apply(rule hn_refine_frame'') 
  using assms[THEN hfrefD] by auto


lemma amor_orthogonal_empt:
  assumes "(C, A) ∈ (assn)⇧k →⇩a R"
  shows "(C, A) ∈ (augment_amor_assn PHI assn)⇧k →⇩a R"
  unfolding augment_amor_assn_def
  apply(rule hfrefI)
  apply (auto)
  apply(rule hn_refine_frame'') 
  using assms[THEN hfrefD] by auto


lemma invalid_assn_augment_amor_assn: "invalid_assn (augment_amor_assn Φ A) = invalid_assn A"
  unfolding augment_amor_assn_def invalid_assn_def
  unfolding pure_part_def 
  apply auto apply(rule ext) apply(rule ext)
  apply auto
  subgoal  
    using hnr_vcg_aux3 by blast
  subgoal
    by (metis hnr_vcg_aux1 sep_conj_commute) 
  done

subsection ‹finite cost›

definition "finite_cost t ≡ ∀x. the_acost t x < ∞"

lemma finite_costD: "finite_cost t ⟹ the_acost t x < ∞"
  unfolding finite_cost_def by auto
   
lemma finite_costI: "(⋀x. the_acost t x < ∞) ⟹ finite_cost t"
  unfolding finite_cost_def by auto


lemma finite_cost_lift_acost: "finite_cost (lift_acost x)"
  unfolding finite_cost_def lift_acost_def by auto

lemma extract_lift_acost_if_less_infinity:
  assumes
    less_infinity: "finite_cost t" 
  obtains t' where "lift_acost t' = t"
proof 
  show "lift_acost (acostC (λx. the_enat (the_acost t x))) = t"
    unfolding lift_acost_def
    apply(cases t)
    apply simp
    using less_infinity[THEN finite_costD]
    by (metis (mono_tags) acost.sel acost_eq_I comp_apply less_infinityE the_enat.simps)
qed


subsection ‹wp can frame time through›


text ‹Is this property specific to wp of LLVM, or is this general?›

thm wp_time_mono text ‹is this morally the same lemma? it was also proven with unfolding mwp›

lemma wp_time_frame: "wp c (λr s. (G r) (ll_α s)) (s,tc)
  ⟹ wp c (λr s. ($t ** G r) (ll_α s)) (s,tc+t)"
  unfolding wp_def apply auto
  unfolding mwp_def apply(cases "run c s")
     apply auto
  unfolding ll_α_def
  subgoal for x y z
    apply(rule sep_conjI[where x="(0,t)" and y="(lift_α_cost llvm_α (z, minus_ecost_cost tc y))"]) 
    subgoal unfolding time_credits_assn_def SND_def by auto 
    subgoal apply simp done
    subgoal by (simp add: sep_disj_acost_def sep_disj_enat_def sep_disj_prod_def) 
    subgoal
      by (smt ‹⟦run c s = SUCC x y z; G x (lift_α_cost llvm_α (z, minus_ecost_cost tc y)); le_cost_ecost y tc⟧ ⟹ (0, t) ## lift_α_cost llvm_α (z, minus_ecost_cost tc y)›
              add.commute cost_ecost_minus_add_assoc2 lift_α_cost_def old.prod.case plus_prod_eqI prod.sel(1) sep_disj_prod_def unique_zero_simps(3))
    done
  subgoal
    using cost_ecost_add_increasing2 by blast
  done

subsection ‹more HNR rules›

lemma hn_refineI2: 
  assumes "⋀F s cr M. ⟦ nofailT m ; m = REST M; (Γ**F) (ll_α(s,cr)) ⟧
          ⟹ (∃ra Ca. M ra ≥ Some Ca ∧
                     (wp c (λr s.  (Γ' ** R ra r ** F ** GC) (ll_α s)) (s,cr+Ca)))"
  shows "hn_refine Γ c Γ' R m"  
  apply (auto simp add: hn_refine_def STATE_alt)  
  apply(rule assms) by auto

lemma hn_refine_payday_reverse_alt:
  fixes m :: " ('d, (char list, enat) acost) nrest"
  assumes 
    a: "finite_cost t" 
  and "hn_refine Γ c Γ' R (consume m t)"
  shows "hn_refine ($t ∧* Γ) c Γ' R m"
proof -
  from extract_lift_acost_if_less_infinity[OF a]
  obtain t' where t: "t = lift_acost t'" by blast


  show ?thesis
    unfolding t apply(rule hn_refine_payday_reverse)
    apply(fold t)
    apply(fact)
    done
qed



lemma hn_refine_reclaimday: 
   assumes
     nofail: "nofailT m ⟹ nofailT (reclaim m Φ)"
     and as: "hn_refine Γ c Γ' G (reclaim m Φ)"
   shows "hn_refine Γ c Γ' (augment_amor_assn Φ G) m"
proof (rule hn_refineI2)
  fix F s cr M
  assume n: "nofailT m"
      and m: "m = SPECT M" and H: "(Γ ∧* F) (ll_α (s, cr))"

  from n nofail have z: "nofailT (reclaim m Φ)" by simp
  then obtain M' where kl: " (reclaim m Φ) = SPECT M'"   
    unfolding nofailT_def 
    by force

  from z m have Z: "(∀x t'. M x = Some t' ⟶ Φ x ≤ t')" apply(simp only: nofailT_reclaim) by auto

  from as[unfolded hn_refine_def STATE_def, rule_format, OF z, OF kl H] obtain ra Ca where
    ff: "Some Ca ≤ M' ra" and wp: "wp c (λr s. (Γ' ∧* G ra r ∧* F ∧* GC) (ll_α s)) (s, cr + Ca)" by blast

  from ff have "M' ra ≠ None"
    by (metis less_eq_option_Some_None)
  with kl[symmetric] have mra: "M ra ≠ None" unfolding m
    apply(cases "M ra") apply auto unfolding Sup_nrest_def apply (auto split: if_splits) 
    by (smt SUP_bot_conv(2) Sup_empty empty_Sup fun_upd_apply mem_Collect_eq option.distinct(1))

  then obtain mra where Mra: "M ra = Some mra" by auto

  have nene: "M' ra ≤ Some (mra - Φ ra)"
    using kl unfolding m  apply (auto split: if_splits)
    unfolding Sup_nrest_def apply (auto split: if_splits)
    apply(rule Sup_least) apply auto 
    by (simp add: Mra) 

  with ff have ff': " Some Ca ≤Some (mra - Φ ra)" by(rule order.trans)

  show "∃ra Ca. Some Ca ≤ M ra ∧ wp c (λr s. (Γ' ∧* augment_amor_assn Φ G ra r ∧* F ∧* GC) (ll_α s)) (s, cr + Ca)"
    apply(rule exI[where x=ra])
    apply(rule exI[where x="Ca+Φ ra"])
    apply safe
    subgoal        
      using ff' unfolding Mra apply simp
      apply(rule plus_minus_adjoint_ecost_I) 
      using Z[rule_format, of ra mra] Mra
      by simp
    subgoal using wp_time_frame[OF wp, where t="Φ ra"] unfolding augment_amor_assn_def
      by (auto simp:  sep_conj_left_commute sep_conj_commute add.assoc add.left_commute add.commute)
    done
qed


lemma hn_refine_amortization: 
   assumes
     nofail: "⋀x r. nofailT (m x r) ⟹ nofailT (reclaim (consume (m x r) (Φ x)) Φ)"
  and finite: "⋀x. finite_cost (Φ x)" 
     and as: "hn_refine (G x x' ** F' r r') (c x' r') (invalid_assn G x x' ** F' r r') G (reclaim (consume (m x r) (Φ x)) Φ)"
   shows
  "hn_refine ((augment_amor_assn Φ G) x x' ** F' r r') (c x' r') (invalid_assn (augment_amor_assn Φ G) x x' ** F' r r') (augment_amor_assn Φ G) (m x r)"
  unfolding invalid_assn_augment_amor_assn
  unfolding augment_amor_assn_def
  apply(subst sep_conj_assoc) apply simp
  apply(fold augment_amor_assn_def)
  apply(rule hn_refine_payday_reverse_alt[OF finite])
  apply(rule hn_refine_reclaimday)
  subgoal apply (simp add: nofailT_consume) using nofail by simp
  subgoal using as by simp
  done





section ‹Specification of List Operations›


(* TODO: it is not append but snoc ! *)

context fixes T :: ecost begin
definition mop_list_snoc where
 [simp]: "mop_list_snoc  xs x = SPECT [xs @ [x] ↦ T]"
sepref_register mop_list_snoc


definition mop_list_emptylist where
  [simp]: "mop_list_emptylist = SPECT [ [] ↦ T ]"
sepref_register mop_list_emptylist

end



text ‹The abstract program A for empty list:›






section ‹Dynamic Lists›

subsection ‹Dynamic Lists refine lists›

definition "dyn_list_rel = {( ((bs,l,c)) , as) | bs l c  as. take l bs = as ∧ l ≤ c ∧ c = length bs ∧ length bs > 0 }"


lemma dyn_list_rel_alt: "dyn_list_rel = br (λ(bs,l,c). take l bs) (λ(bs,l,c). l ≤ c ∧ c = length bs ∧ length bs > 0)"
  unfolding dyn_list_rel_def br_def by auto


lemma dyn_list_rel_sv[relator_props]: "single_valued dyn_list_rel"
  unfolding dyn_list_rel_alt by(rule br_sv)  


subsection ‹Specification of Dynamic List Operations›

definition "dyn_list_empty_spec T = SPEC (λ(ls,l,c). l=0 ∧ c=8 ∧ c = length ls) (λ_. T)"

context
  fixes  T :: "(nat × nat) ⇒ (char list, enat) acost"
begin
  definition dyn_list_get_spec  :: "('a list*_*_) ⇒ nat ⇒ ('a, _) nrest"
    where [simp]: "dyn_list_get_spec ≡ λ(xs,l,_) i. do { ASSERT (i<length xs); consume (RETURNT (xs!i)) (T (l,i)) }"
  sepref_register "dyn_list_get_spec"
end


definition dyn_list_push_spec where
  "dyn_list_push_spec T ≡ λ(bs,l,c) x. SPEC (λ(bs',l',c'). l'≤c' ∧ c'=length bs' ∧ l'=l+1 ∧ length bs' ≥ length bs
                                                          ∧ take l bs' = take l bs ∧ bs' ! l = x) (λ_. T)"



text ‹timerefine commutes with specifications›

lemma timerefine_dyn_list_empty_spec: "timerefine TR (dyn_list_empty_spec T) = dyn_list_empty_spec (timerefineA TR T)"
  unfolding dyn_list_empty_spec_def
  by (auto split: prod.splits simp: SPEC_timerefine_conv)

lemma timerefine_dyn_list_push_spec: "timerefine TR (dyn_list_push_spec T dl x) = dyn_list_push_spec (timerefineA TR T) dl x"
  unfolding dyn_list_push_spec_def
  by (auto split: prod.splits simp: SPEC_timerefine_conv)

text ‹dynamic list opertions refine the list operations›
 

lemma 
  shows "(uncurry (dyn_list_get_spec T), uncurry (mop_list_get T)) ∈ dyn_list_rel ×⇩r Id  →⇩f ⟨Id⟩nrest_rel"
  apply(rule frefI)
  apply(rule nrest_relI)
  unfolding uncurry_def dyn_list_get_spec_def mop_list_get_def dyn_list_rel_alt 
  apply (auto simp: in_br_conv consume_RETURNT)
  apply(rule le_acost_ASSERTI)
  apply(rule gwp_specifies_I)
  apply(refine_vcg ‹-›)
  by auto 





lemma "((bs,l,c),as)∈dyn_list_rel ⟹ (x',x) ∈ Id
 ⟹ dyn_list_push_spec T (bs,l,c) x'
         ≤ ⇓dyn_list_rel (timerefine (0(''list_append'':=T)) (mop_list_snoc (cost ''list_append'' 1) as x))"
  unfolding dyn_list_push_spec_def mop_list_snoc_def
  apply(subst timerefine_SPECT_map)
  apply(subst SPECT_assign_emb')
  unfolding dyn_list_rel_alt
    apply(subst conc_fun_br)
  apply(subst SPEC_REST_emb'_conv[symmetric])
  apply safe
  apply(rule SPEC_leq_SPEC_I_even_stronger)
  subgoal by (auto simp: in_br_conv take_Suc_conv_app_nth)
  subgoal apply auto 
    by(simp add: norm_cost ) 
  done



lemma dyn_list_push_spec_refines_one_step: 
  "((bs,l,c),as)∈ dyn_list_rel ⟹ (r',r)∈Id
   ⟹ dyn_list_push_spec T (bs, l, c) r' ≤ ⇓dyn_list_rel (mop_list_snoc T  as r)"
  unfolding mop_list_snoc_def dyn_list_rel_alt
  apply(subst SPECT_assign_emb')
  unfolding conc_fun_br
  apply(subst SPEC_REST_emb'_conv[symmetric])
  unfolding dyn_list_push_spec_def  apply simp
  apply(rule SPEC_leq_SPEC_I_even_stronger)
  unfolding in_br_conv
  by (auto simp add: take_Suc_conv_app_nth norm_cost) 

lemma dyn_list_push_spec_refines_fref: "(uncurry (PR_CONST (dyn_list_push_spec T)), uncurry (PR_CONST (mop_list_snoc T)))
        ∈ dyn_list_rel ×⇩r Id →⇩f ⟨dyn_list_rel⟩nrest_rel" 
  apply(rule frefI)
  apply(rule nrest_relI)
  apply(auto split: prod.splits simp del: mop_list_snoc_def simp add: PR_CONST_def uncurry_def)
  apply(rule dyn_list_push_spec_refines_one_step) by auto



subsection ‹Raw Refinements Dynamic List Operations›


subsubsection ‹dynamic List init›

text ‹The abstract program B for empty dynamic list, (in dynamic array currencies) :›

definition dyn_list_new_raw where
  "dyn_list_new_raw = do {
       dst ← mop_list_init_raw (λn. cost ''list_init_c'' 8) 8;
       RETURNT (dst,0,8)
    }"

definition dyn_list_new where
  "dyn_list_new ini = do {
       dst ← mop_list_init (λn. cost ''list_init_c'' 8) ini 8;
       RETURNT (dst,0,8)
    }"

text ‹Refinement THEOREM A-B›

abbreviation "TR_dyn_list_new ==  (0(''list_empty'':=cost ''list_init_c'' 8))"

lemma dyn_list_new_refines:
 "dyn_list_new ini ≤ ⇓dyn_list_rel (⇓⇩C TR_dyn_list_new (mop_list_emptylist (cost ''list_empty'' 1)))"
  unfolding mop_list_emptylist_def dyn_list_new_def dyn_list_rel_alt
  apply (simp add: timerefine_SPECT_map norm_cost )                   
  apply (simp add: SPECT_assign_emb' conc_fun_br)
  apply(rule gwp_specifies_I)
  apply(refine_vcg ‹-›)    by(auto simp: emb'_def)

subsubsection ‹dynamic list lookup›

definition dyn_list_get where
  "dyn_list_get ≡ λ(bs,l,c) i. doN {
    mop_list_get (λ_. cost ''list_get'' 1) bs i
  }"

lemma "( (bs,l,c), as)∈dyn_list_rel ⟹ dyn_list_get (bs,l,c) i ≤ mop_list_get (λ_. cost ''list_get'' 1) as i"
  oops


subsubsection ‹Refinement of dynamic List push›

paragraph ‹Specification of Dynamic List Double›

term mop_list_init
term mop_list_init_raw
thm hnr_raw_array_new refine_mop_list_init_raw
term mop_array_new
thm hnr_array_new
thm hnr_array_new


text ‹an dynamic list is a triple (bs,l,c) with the carrier list bs which has capacity ‹c›, 
      and length ‹l›, i.e. the first ‹l› elements are valid. ›

definition dyn_list_double_spec where
  "dyn_list_double_spec ≡ λ(bs,l,c). doN {
       ASSERT (l≤c ∧ c=length bs);
       SPEC (λ(bs',l',c'). take l bs' = take l bs ∧ 
              length bs' = 2 * length bs ∧ l' = l ∧ l≤c' ∧ c'=length bs')
        (λ(bs',l',c'). cost ''dyn_list_double_c'' (enat c)) 
  }"


paragraph ‹Specification of dynamic List basic append›

definition dyn_list_push_basic_spec where
  "dyn_list_push_basic_spec ≡ λ(bs,l,c) x. doN {
      ASSERT (l < length bs ∧ length bs = c);
      bs' ← mop_list_set (λ_. cost ''list_set'' 1) bs l x;
      l' ← SPECc2 ''add'' (+) l 1;
      RETURNT (bs',l',c)
  }"


paragraph ‹Implementation Sketch for dynamic List append:›

definition dyn_list_push where
  "dyn_list_push ≡ λ(bs,l,c) x. doN {
      ASSERT (l≤c ∧ c=length bs ∧ 0<length bs);
      if⇩N SPECc2 ''less'' (<) l c then doN {
        dyn_list_push_basic_spec (bs,l,c) x
      } else doN {          
        (bs',l',c') ← dyn_list_double_spec (bs,l,c);
        ASSERT (l'=l ∧ l<c' ∧ c'=length bs' ∧ take l bs = take l bs' );
        dyn_list_push_basic_spec (bs',l',c') x
      }
  }"



paragraph ‹Amortization proof›
  

definition "push_amortized_cost ≡ cost ''dyn_list_double_c'' (1::nat)"
definition "push_overhead_cost ≡ cost ''add'' 1 + (cost ''list_set'' 1 + (cost ''if'' 1 + (cost ''less'' 1 + cost ''list_length'' 1)))"
definition "Φ_push ≡ (λ(xs,l,c). (((2*l -length xs)) *m push_amortized_cost))"
abbreviation "Φ_push' ≡ lift_acost o Φ_push"

text ‹The program @{term dyn_list_push} has two cases,
       either the capacity is reached, then we have to resize (at @{term push_amortized_cost} cost per element in the list)
       and push (with cost bounded by @{term push_overhead_cost}),
       or there is still space, then we can push right away (with cost bounded by @{term push_overhead_cost}). 

      We now level out the advertised cost of push by introducing a potential. We will lower the `advertised cost`
      of the resize-case, and increase the `advertised cost` of the push-case.
      The potential is @{term "(λ(xs,l,c). (((2*l -length xs)) *m push_amortized_cost))"}, which is positive
      if the dynamic list is more than half full. Then we collect @{term push_amortized_cost} credits with
      each push, until we reach capacity, when @{term Φ_push} will get @{term "length xs *m push_amortized_cost"}
      and can be used to pay for the resize.

      To fill up the potential we have to pay 2 x @{term push_amortized_cost} in the advertised cost of all pushs,
      additional to the @{term push_overhead_cost} for inserting an element.

      Note, in this operation the overhead cost is in both cases @{term push_overhead_cost}. If it was not, one has to
      chose the supremum over both to incorporate into the advertised cost.
    ›


text‹The amortization inequality is: 
  RAW COST ≤     (  PREPOTENTIAL + ADVERTISED COST ) - POSTPOTENTIAL

  we now prove:
      raw_operation ≤ reclaim ( consume advertised_opertion PREPOTENTIAL) POSTPOTENTIAL
 ›


lemma  dyn_list_push_spec_refines_sketch:
    ― ‹This lemma collects the inequalities of the advertised cost ACC and the potential Φ›
  assumes a: "l ≤ c" "c=length bs" "0<length bs"
  shows "dyn_list_push (bs,l,c) x ≤ reclaim (consume (dyn_list_push_spec ACC (bs,l,c) x) (Φ (bs,l,c))) Φ"
  unfolding dyn_list_push_spec_def
  unfolding dyn_list_push_def
  apply simp
  apply(subst consume_SPEC_eq)
  apply(rule order.trans[rotated])
  apply(rule reclaim_SPEC_le)
  unfolding SPEC_def
  apply(rule gwp_specifies_I)
  unfolding SPECc2_alt dyn_list_push_basic_spec_def mop_list_set_def
    dyn_list_double_spec_def SPEC_REST_emb'_conv
  apply(refine_vcg ‹-›)
  using a
          defer
         apply auto[1]
         apply auto [1]
  defer
      apply auto [1]
     apply auto [1]
  subgoal by force
  using assms  
   apply auto    
  oops


lemma  dyn_list_push_spec_refines:
  assumes a: "l ≤ c" "c=length bs" "0<length bs"
  shows "dyn_list_push (bs,l,c) x ≤ reclaim (consume (dyn_list_push_spec (lift_acost (2 *m push_amortized_cost + push_overhead_cost)) (bs,l,c) x) (Φ_push' (bs,l,c))) Φ_push'"
  unfolding dyn_list_push_spec_def
  unfolding dyn_list_push_def
  apply simp
  apply(subst consume_SPEC_eq)
  apply(subst reclaim_SPEC)
  subgoal
    unfolding Φ_push_def push_amortized_cost_def push_overhead_cost_def
    apply (auto simp: norm_cost) apply(subst add.commute) apply(subst (2) add.assoc) apply(subst cost_same_curr_add)
    apply(simp add: add.assoc)  
      apply sc_solve  by auto
  unfolding SPEC_def
  apply(rule gwp_specifies_I)
  unfolding SPECc2_alt dyn_list_push_basic_spec_def mop_list_set_def
        dyn_list_double_spec_def SPEC_REST_emb'_conv
  apply(refine_vcg ‹-›)
  using a 
  subgoal apply auto
    unfolding Φ_push_def apply (simp add: lift_acost_propagate[symmetric] lift_acost_minus)
    apply(subst (4) add.commute)
    apply(subst add.assoc)
    apply(subst costmult_add_distrib_left)  
    apply(rule order.trans[rotated])
     apply(rule lift_acost_mono)
     apply(rule acost_move_sub_le)
     apply(rule costmult_right_mono) apply simp 
    unfolding push_overhead_cost_def  apply(simp add: norm_cost) apply(sc_solve) by (simp add: one_enat_def)
         apply auto[1]
        apply auto [1]
  subgoal apply simp (* can't see why auto would loop here *)
    unfolding Φ_push_def apply (simp add: lift_acost_propagate[symmetric] lift_acost_minus add.assoc)
    apply(subst (5) add.commute)
    apply(subst add.assoc)
    apply(subst costmult_add_distrib_left)
    apply(subst add_diff_assoc_ncost)
    subgoal apply(rule costmult_right_mono) by auto

    apply(subst costmult_minus_distrib)
    apply simp
    unfolding push_overhead_cost_def push_amortized_cost_def
    apply(simp add: norm_cost)
    apply sc_solve  by(simp add: one_enat_def)
      apply auto [1]
     apply auto [1]
  subgoal by force
  using assms  
   apply auto 
  done


subsubsection ‹Refinement of dynamic List emptylist›

definition "E_dlas ≡ cost ''list_init_c'' 8" (* the cost to initialize the empty list *)

lemma  dyn_list_new_raw_refines:
  shows "dyn_list_new_raw ≤ reclaim (consume (dyn_list_empty_spec (lift_acost E_dlas)) 0) Φ_push'"
  unfolding dyn_list_new_raw_def mop_list_init_raw_def
  unfolding dyn_list_empty_spec_def
  apply(subst consume_SPEC_eq)
  apply(subst reclaim_SPEC)
  subgoal unfolding Φ_push_def  by (auto simp: lift_acost_def less_eq_acost_def zero_acost_def)
  unfolding SPEC_def
  unfolding autoref_tag_defs
  apply(rule gwp_specifies_I)
  apply(refine_vcg ‹-›)
  subgoal 
    unfolding Φ_push_def  apply (auto simp: lift_acost_zero E_dlas_def lift_acost_cost needname_minus_absorb) 
    apply sc_solve by auto
  subgoal by simp
  done


section ‹Implementing Dynamic Lists›

text ‹We introduce a locale that expects implementations of the operations of dynamic lists,
    then composes this, to obtain amortized implementations of list operations ›


locale dyn_list_assn = 
  fixes 
    TR_dynarray :: "string ⇒ ecost"
    and dyn_array_raw_assn :: " 'e list × nat × nat ⇒ 'f ⇒ assn"
begin


text ‹We lift the raw_assn to contain the Potential Time Credits.›

abbreviation "Φ_d == λx. timerefineA TR_dynarray  (Φ_push' x)"

definition dyn_array_raw_armor_assn where
  "dyn_array_raw_armor_assn ≡ λ(bs, l, c) da'.  $Φ_d (bs, l, c) ∧* dyn_array_raw_assn (bs, l, c) da'"

lemma dyn_array_raw_armor_assn_alt: "dyn_array_raw_armor_assn = augment_amor_assn Φ_d (dyn_array_raw_assn)"
  unfolding augment_amor_assn_def dyn_array_raw_armor_assn_def 
  apply (rule ext) 
  apply (rule ext) by simp


text ‹and combining it with the refinement relation between dynamic lists and lists›

definition "dyn_array_assn A = hr_comp (hr_comp (dyn_array_raw_armor_assn) dyn_list_rel) (⟨the_pure A⟩list_rel)"

definition "b_aux = hr_comp (dyn_array_raw_armor_assn) dyn_list_rel"
lemma b_aux_unf: "hr_comp (dyn_array_raw_armor_assn) dyn_list_rel = b_aux"
  unfolding b_aux_def by auto
declare b_aux_unf[fcomp_norm_unfold]
thm b_aux_unf
lemma dyn_array_raw_armor_aux: "hr_comp (b_aux) (⟨the_pure A⟩list_rel)
           = dyn_array_assn A"
  unfolding b_aux_def dyn_array_assn_def by auto
declare dyn_array_raw_armor_aux[fcomp_norm_unfold]
thm dyn_array_raw_armor_aux
lemma dyn_array_raw_armor_: "hr_comp (hr_comp (dyn_array_raw_armor_assn) dyn_list_rel) (⟨the_pure A⟩list_rel)
           = dyn_array_assn A"
  unfolding dyn_array_assn_def by auto
 (*TODO: is this the right way to instrument FCOMP in order to fold the hr_comp ?*)
declare dyn_array_raw_armor_[fcomp_norm_unfold]

end

locale dyn_list_impl = dyn_list_assn TR_dynarray dyn_array_raw_assn 
    for TR_dynarray and dyn_array_raw_assn :: "('e::llvm_rep) list × nat × nat ⇒ 'f ⇒ assn" + 
    fixes
      push_size_bound  :: "nat ⇒ bool"
    and  dyn_array_push
    and dyn_array_push_impl :: "'f ⇒ 'e ⇒ 'f llM" 

    and dynamiclist_empty2 :: "((('e) list × nat × nat),ecost) nrest"
    and dynamiclist_empty_impl :: "'f llM"

  assumes 
        wfR_TR_dynarray: "wfR'' TR_dynarray"                           
    and TR_dynarray_keeps_finite: "⋀Φ. finite {x. the_acost Φ x ≠0} ⟹ finite_cost Φ ⟹ finite_cost (timerefineA TR_dynarray Φ)"
    and dyn_array_push_refine: "dyn_array_push dl x ≤ ⇓⇩C TR_dynarray (dyn_list_push dl x)"

    and dyn_array_push_impl_refines: "push_size_bound l ⟹ hn_refine (dyn_array_raw_assn (bs,l,c) da' ** id_assn x x')
                        (dyn_array_push_impl da' x')
                      (invalid_assn (dyn_array_raw_assn) (bs,l,c) da' ** id_assn x x')
                        (dyn_array_raw_assn) (dyn_array_push (bs,l,c) x)"

    and emptylist2_real: "(uncurry0 dynamiclist_empty_impl, uncurry0 dynamiclist_empty2) ∈ unit_assn⇧k →⇩a  dyn_array_raw_assn"
    and emptylist2_refine: "dynamiclist_empty2 ≤ ⇓⇩C TR_dynarray dyn_list_new_raw"
begin 




subsection ‹Combining the Push operation›

abbreviation "push_abstract_advertised_cost == lift_acost (2 *m push_amortized_cost + push_overhead_cost)"
abbreviation "push_concrete_advertised_cost == timerefineA TR_dynarray push_abstract_advertised_cost"


text ‹this is the operation that is used in abstract programs when already decided which 
      data structure to use here: array_lists›
definition "dyn_array_push_spec = mop_list_snoc push_concrete_advertised_cost"



lemma dyn_list_push_spec_leq_pull_TR:
  fixes TR :: "_⇒ecost"
  assumes *: "wfR'' TR"
  shows "⇓⇩C TR (reclaim (NREST.consume (dyn_list_push_spec push_abstract_advertised_cost (bs, l, c) x) (Φ_push' (bs, l, c))) Φ_push') ≤
         (reclaim (NREST.consume ((dyn_list_push_spec (timerefineA TR push_abstract_advertised_cost) (bs, l, c) x)) (timerefineA TR (Φ_push' (bs, l, c)))) (timerefineA TR o Φ_push'))"
  unfolding dyn_list_push_spec_def
  apply simp
  supply [[unify_trace_failure]]
  apply(rule pull_timerefine_through_reclaim)
   apply(rule *) 
  subgoal apply(auto simp: Φ_push_def) apply(subst lift_acost_propagate[symmetric])
    apply(rule lift_acost_mono)
    apply(subst add.commute) apply(subst add.assoc)
    apply(subst costmult_add_distrib_left)
    apply(subst add.commute)
    apply(rule add_increasing2_nat_acost) 
    apply(rule costmult_right_mono) by auto 
  done


text ‹Now we combine two refinements:
  ▪ the refinement of the dynamic list push specification @{term dyn_list_push_spec} incurring the
      advertised cost with the algorithm sketch @{term dyn_list_push} based on the real cost:
      @{thm dyn_list_push_spec_refines} contains the amortization proof. 
     Both programs use currencies of the dynamic list!
  ▪ the refinement of the algorithm sketch @{term dyn_list_push} to the NREST program @{term dyn_array_push}
     which is a timerefinement using the exchange rate @{term TR_dynarray} to exchange from currencies
     of the dynamic list into LLVM currencies›

lemma dyn_array_push_refines:
  "⟦l ≤ c; c = length bs; 0 < length bs⟧ ⟹ dyn_array_push (bs,l,c) x
    ≤ reclaim
          (NREST.consume (dyn_list_push_spec push_concrete_advertised_cost (bs, l, c) x)
            (Φ_d (bs, l, c)))
          Φ_d"
  apply(rule order.trans)   
  apply(rule dyn_array_push_refine)
  apply(rule order.trans)
   apply(rule timerefine_mono2)
  apply(rule wfR_TR_dynarray)
   apply(rule dyn_list_push_spec_refines)
     apply simp_all [3]
  apply(rule order.trans)
   apply(rule dyn_list_push_spec_leq_pull_TR)
  apply(rule wfR_TR_dynarray)
  apply(simp add: timerefine_dyn_list_push_spec)
  unfolding comp_def
  by auto

text ‹Now we combine the raw hnr-rule @{thm dyn_array_push_impl_refines} with the
  amortization refinement @{thm dyn_array_push_refines}}›

lemma dyn_array_push_impl_refines_dyn_list_push_spec: "⟦l ≤ c; c = length bs; 0 < length bs; push_size_bound l⟧
⟹ hn_refine (hn_ctxt (dyn_array_raw_armor_assn) (bs, l, c) da' ∧* hn_ctxt id_assn r r')
     (dyn_array_push_impl $ da' $ r')
     (hn_invalid (dyn_array_raw_armor_assn) (bs, l, c) da' ∧* hn_ctxt id_assn r r')
       (dyn_array_raw_armor_assn)
      (PR_CONST (dyn_list_push_spec push_concrete_advertised_cost) $ (bs, l, c) $ r) "
  unfolding hn_ctxt_def APP_def PR_CONST_def
  unfolding dyn_array_raw_armor_assn_alt apply (simp only: prod.case)        
  apply(rule hn_refine_amortization[where m="dyn_list_push_spec push_concrete_advertised_cost" and c=dyn_array_push_impl and Φ="Φ_d"])
  subgoal 
    apply(simp add: nofailT_reclaim nofailT_consume)
    unfolding dyn_list_push_spec_def apply (auto simp: SPEC_def consume_def split: prod.splits)
    unfolding Φ_push_def
    apply(subst timerefineA_propagate[OF wfR_TR_dynarray, symmetric])
    apply(rule timerefineA_mono[OF wfR_TR_dynarray])
    apply auto
    unfolding lift_acost_propagate[symmetric]
    apply(rule lift_acost_mono) 
    apply(subst add.assoc[symmetric])
    apply(subst costmult_add_distrib_left) 
    apply(rule add_increasing2_nat_acost) 
    apply(rule costmult_right_mono) by auto
  subgoal 
    apply(rule TR_dynarray_keeps_finite)
    subgoal apply (auto simp: Φ_push_def lift_acost_def push_amortized_cost_def norm_cost split: prod.splits)
      apply(rule finite_subset[where B="{''dyn_list_double_c''}"])
       apply auto
      apply(rule ccontr) unfolding cost_def zero_acost_def zero_enat_def by auto
    by(auto intro: finite_cost_lift_acost)
  apply(rule hn_refine_ref)
   apply(rule dyn_array_push_impl_refines) apply simp
  apply(rule dyn_array_push_refines)
    apply auto
  done




lemma dyn_array_push_impl_refines_dyn_list_push_spec':
"⟦(case x of (bs,l,c) ⇒ l ≤ c ∧ c = length bs ∧ 0 < length bs ∧ push_size_bound l)⟧
  ⟹ hn_refine (hn_ctxt (dyn_array_raw_armor_assn) x x' ∧* hn_ctxt id_assn r r')
     (dyn_array_push_impl $ x' $ r')
     (hn_invalid (dyn_array_raw_armor_assn) x x' ∧* hn_ctxt id_assn r r')
       (dyn_array_raw_armor_assn)
      (PR_CONST (dyn_list_push_spec push_concrete_advertised_cost) $ x $ r) "
  apply(cases x)
  apply (simp only:)
  apply(rule dyn_array_push_impl_refines_dyn_list_push_spec)
  by auto

lemmas dyn_array_push_impl_refines_dyn_list_push_spec_hfref = dyn_array_push_impl_refines_dyn_list_push_spec'[to_hfref]

thm dyn_array_push_impl_refines_dyn_list_push_spec' dyn_list_push_spec_refines_fref[where T="lift_acost (2 *m push_amortized_cost + push_overhead_cost)"]







text ‹this makes the tactic ‹solve_attains_sup› solve the supattains sidecondition, 
  because ‹tagged_solver› can then solve the single_valued goal. ›

thm auto_weaken_pre_comp_PRE_I
(*
lemma "(⋀a aa. push_size_bound (a, aa, length a)) ⟹
  comp_PRE (dyn_list_rel ×⇩r Id) (λ_. True) (λx (a, b). case a of (bs, l, c) ⇒ l ≤ c ∧ c = length bs ∧ 0 < length bs ∧ push_size_bound (bs, l, c))
   (λx. nofailT (uncurry (PR_CONST (mop_list_snoc push_concrete_advertised_cost)) x)) (a, b)"
  apply(rule auto_weaken_pre_comp_PRE_I)
   apply simp 
  apply (simp_all add: dyn_list_rel_def )
  apply safe    
  subgoal apply simp done
  subgoal apply simp done
  subgoal apply simp done
  subgoal apply simp
    oops
lemma "⟦⋀a aa. X (a, aa, length a); (((aa, aaa, ba), baa), a, b) ∈ {((bs, l, length bs), take l bs) |bs l. l ≤ length bs ∧ bs ≠ []} ×⇩r Id⟧
    ⟹ X (aa, aaa, ba)" apply simp

lemma zzz: "⟦⋀a aa. push_size_bound (a, aa, length a); ((aa, aaa, b), a) ∈ dyn_list_rel⟧ ⟹ push_size_bound (aa, aaa, b)"
  sorry

*)

 
thm dyn_array_push_impl_refines_dyn_list_push_spec_hfref dyn_list_push_spec_refines_fref

lemma XXX[fcomp_prenorm_simps]: "((as,l,c),x)∈ dyn_list_rel ⟹ push_size_bound l = push_size_bound (length x)"
  unfolding dyn_list_rel_def by auto

lemma dyn_array_push_fcomp_prenorm[fcomp_prenorm_simps]:
  "((bs,l,c),x)∈ dyn_list_rel ⟹ l ≤ c ∧ c = length bs ∧ bs ≠ []"
  by(auto simp: dyn_list_rel_def)

lemmas dyn_array_push_impl_refines_dyn_array_push_spec
  = dyn_array_push_impl_refines_dyn_list_push_spec_hfref[FCOMP dyn_list_push_spec_refines_fref, folded dyn_array_push_spec_def]


thm dyn_array_push_impl_refines_dyn_array_push_spec



lemma taaaa: "(uncurry (PR_CONST dyn_array_push_spec), uncurry (PR_CONST dyn_array_push_spec))
        ∈  ⟨R⟩list_rel ×⇩r R →⇩f ⟨⟨R⟩list_rel⟩nrest_rel" 
  apply rule
  unfolding nrest_rel_def dyn_array_push_spec_def   
  apply auto
  unfolding conc_fun_RES apply auto 
  apply (simp add: le_fun_def)  
  apply(rule Sup_upper) apply auto  
  by (meson list_rel_append2 list_rel_simp(4) refine_list(1))  


lemma one_time_dyn_array_push_spec[OT_intros]: "one_time (dyn_array_push_spec a b)"
  apply(auto simp:  dyn_array_push_spec_def) by (intro OT_intros)

(* TODO: Move! *)  
lemmas [fcomp_prenorm_simps] = list_rel_imp_same_length  
  
  
lemmas G_push =  dyn_array_push_impl_refines_dyn_array_push_spec[FCOMP taaaa] 
 





subsubsection ‹obsolete›


abbreviation "specify_cost == 0(''list_append'':= push_concrete_advertised_cost)"

lemma dyn_list_push_spec_refines: 
  "((bs,l,c),as)∈ dyn_list_rel ⟹ (r',r)∈Id
   ⟹ dyn_list_push_spec push_concrete_advertised_cost (bs, l, c) r' ≤ ⇓dyn_list_rel (⇓⇩C specify_cost  (mop_list_snoc (cost ''list_append'' 1)  as r))"
  unfolding mop_list_snoc_def dyn_list_rel_alt
  apply(subst timerefine_SPECT_map)
  apply(subst SPECT_assign_emb')
  unfolding conc_fun_br
  apply(subst SPEC_REST_emb'_conv[symmetric])
  unfolding dyn_list_push_spec_def  apply simp
  apply(rule SPEC_leq_SPEC_I_even_stronger)
  unfolding in_br_conv
  by (auto simp add: take_Suc_conv_app_nth norm_cost) 



subsection ‹Combining the Emptylist operation›

abbreviation "el_abstract_advertised_cost == lift_acost E_dlas"
abbreviation "el_concrete_advertised_cost == timerefineA TR_dynarray el_abstract_advertised_cost"

definition "dynamiclist_empty_spec = mop_list_emptylist el_concrete_advertised_cost"

lemma dyn_list_empty2_refines:
  "dynamiclist_empty2
    ≤ reclaim (dyn_list_empty_spec el_concrete_advertised_cost) Φ_d"
  apply(rule order.trans)
  apply(rule emptylist2_refine)
  apply(rule order.trans)
   apply(rule timerefine_mono2)
  apply(rule wfR_TR_dynarray)
   apply(rule dyn_list_new_raw_refines)
  apply(rule order.trans)
  unfolding dyn_list_empty_spec_def
   apply(rule pull_timerefine_through_reclaim[OF wfR_TR_dynarray])
  subgoal by (auto simp: Φ_push_def lift_acost_zero ecost_nneg)
  apply(simp add: timerefine_dyn_list_empty_spec consume_0)
  unfolding comp_def            
  by auto
  
(* declare [[unify_trace_failure]] *)

thm emptylist2_real
thm emptylist2_real[to_hnr]
thm emptylist2_refine

lemma YEAH32: "hn_refine □ dynamiclist_empty_impl □
       (dyn_array_raw_armor_assn)
      (PR_CONST (dyn_list_empty_spec el_concrete_advertised_cost) ) "
  unfolding hn_ctxt_def APP_def PR_CONST_def
  unfolding dyn_array_raw_armor_assn_alt
  apply(rule hn_refine_reclaimday)
  subgoal                                    
    apply(simp add: nofailT_reclaim nofailT_consume)
    unfolding dyn_list_empty_spec_def apply (auto simp: SPEC_def consume_def split: prod.splits)
    unfolding Φ_push_def apply auto
    apply(rule timerefineA_mono[OF wfR_TR_dynarray])
    by (auto simp: lift_acost_zero ecost_nneg) 
  apply(rule hn_refine_ref) 
   apply(rule emptylist2_real[to_hnr])
  apply(rule dyn_list_empty2_refines)
  done

lemmas RICHTIGCOOL2 = YEAH32[to_hfref]

lemma dynamiclist_empty_refines_fref: "(uncurry0 (PR_CONST (dyn_list_empty_spec (T::ecost))), uncurry0 (PR_CONST (mop_list_emptylist T)))
        ∈ unit_rel →⇩f ⟨dyn_list_rel⟩nrest_rel" 
  apply(rule frefI)
  apply(rule nrest_relI)
  unfolding mop_list_emptylist_def dyn_list_empty_spec_def dyn_list_rel_alt
  apply (simp add: timerefine_SPECT_map norm_cost )                   
  apply (simp add: SPECT_assign_emb' conc_fun_br)
  apply(subst SPEC_REST_emb'_conv[symmetric])
  apply(rule SPEC_leq_SPEC_I_even_stronger)
  by auto

lemmas GGG = RICHTIGCOOL2[FCOMP dynamiclist_empty_refines_fref, folded dynamiclist_empty_spec_def]



lemma taaaa_emp: "(uncurry0 (PR_CONST  (dynamiclist_empty_spec)), uncurry0 (PR_CONST  (dynamiclist_empty_spec)))
        ∈ unit_rel →⇩f ⟨⟨the_pure A⟩list_rel⟩nrest_rel" 
  apply rule
  unfolding nrest_rel_def dynamiclist_empty_spec_def mop_list_emptylist_def 
  apply auto
  unfolding conc_fun_RES apply auto 
  by (simp add: le_fun_def)  

lemmas GGG' = GGG[FCOMP taaaa_emp]


lemma GGG_empty: "(uncurry0 dynamiclist_empty_impl, uncurry0 (PR_CONST dynamiclist_empty_spec)) ∈ unit_assn⇧k →⇩a dyn_array_assn A"
  apply(rule GGG')
  apply(intro allI SC_attains_supI) 
  apply(rule one_time_attains_sup)
  unfolding uncurry0_def dynamiclist_empty_spec_def mop_list_emptylist_def apply simp
  apply(intro OT_intros)
  done

end

context size_t_context begin

definition dyn_array_raw_assn  :: "('x::llvm_rep) list × nat × nat ⇒ 'x ptr × ('size_t) word × 'size_t word ⇒ assn" where
  "dyn_array_raw_assn  ≡ (array_assn id_assn ×⇩a snat_assn' TYPE('size_t) ×⇩a snat_assn' TYPE('size_t))"
(*
     λ(bs,l,c) (p,l',c'). array_assn id_assn bs p ** snat_assn' TYPE('size_t) l l' ** snat_assn' TYPE('size_t) c c'"
*)





subsection ‹implement nth›


(* TODO *)

subsection  ‹implement push›


definition "TR_doublec = 0(''dyn_list_double_c'':=   cost'_narray_new 2
                               + lift_acost list_copy_body_cost
                                + cost ''icmp_slt'' 1 + cost ''call'' 1 + cost ''if'' 1
                                + cost ''mul'' 1
                                          )"

lemma wfR''_TR_doublec[simp]: "wfR'' TR_doublec"
  unfolding TR_doublec_def
  by auto 


term   dyn_list_double_spec

definition dyn_list_double :: "('x::llvm_rep) list × nat × nat ⇒ ('x list × nat × nat, (char list, enat) acost) nrest"  where
  "dyn_list_double  ≡ λ(bs,l,c). doN {
       ASSERT (l=c ∧ c=length bs);
       c' ← SPECc2 ''mul'' (*) c 2;
       bs' ← mop_array_new id_assn init c';
       bs'' ← list_copy_spec list_copy_spec_time bs' bs l;
       RETURNT (bs'',l,c')
  }"


lemma dyn_list_double_correct:
    "c>0 ⟹ l=c ⟹ dyn_list_double (bs,l,c) ≤ ⇓ Id ( ⇓⇩C TR_doublec (dyn_list_double_spec (bs,l,c)))"
  unfolding dyn_list_double_spec_def 
  apply(split prod.splits)+ apply (rule)+
  apply(rule ASSERT_D3_leI) 
  apply (auto simp add: le_fun_def SPEC_timerefine_conv split: prod.splits)  
  unfolding SPEC_def 
  apply(rule gwp_specifies_I) 
  unfolding dyn_list_double_def SPECc2_def mop_array_new_def mop_list_init_def
  unfolding list_copy_spec_def
  apply(refine_vcg ‹-› rules:)
  subgoal for a b ca
     apply(rule If_le_Some_rule2)
    unfolding list_copy_spec_time_def list_copy_body_cost_def TR_doublec_def
     apply (auto simp: norm_cost)
    apply(sc_solve) 
    apply (auto simp: numeral_eq_enat one_enat_def)
    apply(rule order.trans[where b="1+(1+1)"]) apply simp apply(rule add_mono) apply simp
      apply(rule add_mono) apply simp_all done
  subgoal by auto
  subgoal by auto
  subgoal by auto
  done


definition dyn_list_double2 :: "('x::llvm_rep) list × nat × nat ⇒ ('x list × nat × nat, (char list, enat) acost) nrest"  where
  "dyn_list_double2  ≡ λ(bs,l,c). doN {
       ASSERT (l=c ∧ c=length bs);
       c' ← SPECc2 ''mul'' (*) c 2;
       bs' ← mop_array_new id_assn init c';
       bs'' ← list_copy bs' bs l;
       mop_free bs;
       RETURNT (bs'',l,c')
  }"

 (*
lemma "(dyn_list_double2, dyn_list_double) ∈ Id →⇩f ⟨Id⟩nrest_rel"
  apply rule
  apply (rule nrest_C_relI)   
  unfolding dyn_list_double2_def dyn_list_double_def
  unfolding SPECc2_alt
    apply normalize_blocks
  apply(refine_rcg consumea_Id_refine bindT_refine_easy) *)

term "TTId {''malloc'', ''free'' , ''if'' , ''if'' , ''icmp_eq'' , ''ptrcmp_eq''}" 

lemma TTId_simps: "x ∈ S ⟹ TTId S x = cost x 1"
      "x ∉ S ⟹ TTId S x = 0"
  unfolding TTId_def by auto

lemma
  mop_array_new_minimal_Trefinement:
   "(a,a')∈Id ⟹ (b,b')∈Id ⟹ mop_array_new R a b ≤ ⇓ Id (timerefine (TTId {''malloc'', ''free'' , ''if'' , ''if'' , ''icmp_eq'' , ''ptrcmp_eq''}) (mop_array_new R a' b'))"
  unfolding mop_array_new_def mop_list_init_def 
  apply(simp del: conc_Id)
  apply(rule consume_refine)
  subgoal apply(rule wfR''_TTId_if_finite) by simp
  subgoal apply(auto simp add: norm_cost intro!: wfR''_TTId_if_finite)
    apply(subst timerefineA_propagate) apply(intro wfR''_TTId_if_finite) apply simp
    apply(subst timerefineA_propagate) apply(intro wfR''_TTId_if_finite) apply simp
    apply(subst timerefineA_propagate) apply(intro wfR''_TTId_if_finite) apply simp
    apply(subst timerefineA_propagate) apply(intro wfR''_TTId_if_finite) apply simp
    apply(subst timerefineA_propagate) apply(intro wfR''_TTId_if_finite) apply simp
    by(auto simp add: norm_cost TTId_simps)
  subgoal  apply(rule RETURNT_refine_t) by simp
  done

lemma
  mop_array_new_Trefinement:
   "(a,a')∈Id ⟹ (b,b')∈Id ⟹ mop_array_new R a b ≤ ⇓ Id (timerefine TId (mop_array_new R a' b'))"
  by (auto simp: timerefine_id)

thm selfrefine_TTId_currs_of_M_both

lemma pff: "list_copy a b c ≤  list_copy_spec list_copy_spec_time a b c"
  using list_copy_correct[THEN frefD, THEN nrest_relD, unfolded uncurry_def, simplified]
  by auto 

lemma list_copy_self_refine: "(a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id
    ⟹ list_copy a b c ≤ ⇓Id (⇓⇩C TId (list_copy_spec list_copy_spec_time a' b' c'))"
  using list_copy_correct[THEN frefD, THEN nrest_relD, unfolded uncurry_def, simplified]
  by (auto simp: timerefine_id) 

lemma zzz: "(nofailT (list_copy_spec list_copy_spec_time dst src n))
    ⟹ currs_of_M (list_copy_spec list_copy_spec_time dst src n) = currs_of (list_copy_spec_time n)"
  unfolding list_copy_spec_def 
  unfolding currs_of_M_def
  by (auto simp: nofailT_bindT_ASSERT_iff split: if_splits)

lemma currs_of_add:
  fixes a :: ecost
  shows "currs_of (a+b) = currs_of a ∪ currs_of b"
  apply(cases a; cases b)
  by (auto simp:  currs_of_def)

lemma currs_of_costmult:
  fixes b :: ecost
  shows "currs_of (a *m b) ⊆ currs_of b"
  apply(cases b)
  by (auto simp: costmult_def currs_of_def) 

lemma currs_of_costmult_gt:
  fixes b :: ecost
  shows "a>0 ⟹ currs_of (a *m b) = currs_of b"
  apply(cases b)
  by (auto simp: costmult_def currs_of_def) 

lemma uu: "(⋃n. currs_of (list_copy_spec_time n)) = currs_of (list_copy_spec_time 1)"
  unfolding list_copy_spec_time_def
  apply (auto simp: list_copy_body_cost_def norm_cost )   
  subgoal for x n
    apply(cases "n=0") 
     apply(simp add: currs_of_add cost_zero zero_enat_def[symmetric])
    by (auto simp:  currs_of_add pff2 zero_enat_def) 
  done

 
  

lemma tta: "currs_of (list_copy_spec_time n) ⊆ (⋃n. currs_of (list_copy_spec_time n))"
  unfolding list_copy_spec_time_def
  by (auto simp: list_copy_body_cost_def norm_cost )    


lemma list_copy_tight: "(dsti,dst)∈Id ⟹ (srci,src)∈Id ⟹ (ni,n)∈Id ⟹
          list_copy dsti srci ni ≤ ⇓ Id (⇓⇩C (TTId (⋃n. currs_of (list_copy_spec_time n)))
                                         (list_copy_spec list_copy_spec_time dst src n))"
  apply auto
  apply(rule order.trans)
   apply(rule pff)
  apply(rule order.trans[rotated])
   apply(rule timerefine_TTId_mono)
  apply(rule tta[where n=n]) defer
   apply(subst selfrefine_TTId_currs_of_M_both_yeah)
  supply [[show_types]]
    apply(rule zzz) apply simp apply auto 
  unfolding uu 
  unfolding list_copy_spec_time_def list_copy_body_cost_def
  by(auto simp: norm_cost currs_of_add intro: finite_subset[OF currs_cost] )
 


lemma pff3: "currs_of (cost x (i::enat)) ⊆ {x}"
  unfolding currs_of_def cost_def  by (auto simp: zero_acost_def)

lemma finite_currs_of_lcst[simp]: "finite (currs_of (list_copy_spec_time l))"
  unfolding list_copy_spec_time_def list_copy_body_cost_def
  by(auto simp add: norm_cost currs_of_add pff2 intro: finite_subset[OF pff3])    

declare RETURNT_refine_t[refine0 del]

lemma RETURNT_refine_tight[refine0]: "(c,a)∈R ⟹ RETURNT c ≤ ⇓R (⇓⇩C 0 (RETURNT a))"
  by (rule RETURNT_refine_t)

term mop_free

schematic_goal dyn_list_double2_refine_tight: 
  "(bs,bs')∈Id ⟹ (l,l')∈Id ⟹ (c,c')∈Id
    ⟹ dyn_list_double2 (bs, l, c) ≤ ⇓ Id (⇓⇩C (?E) (dyn_list_double (bs', l', c')))"
  unfolding dyn_list_double2_def dyn_list_double_def mop_free_def
  apply normalize_blocks (* TODO: rule for mop_free refine *)
  apply(refine_rcg) apply auto[1]
  apply(refine_rcg  bindT_refine_conc_time_my_inres_sup
          SPECc2_refine_exch mop_array_new_minimal_Trefinement
          list_copy_tight)
                 apply refine_dref_type 
  by (auto simp: TId_apply uu intro!: wfR''_supI wfR''_TTId_if_finite )

concrete_definition TR_dld2 is dyn_list_double2_refine_tight uses "_ ≤ ⇓ Id (⇓⇩C ⌑ _)" 
lemmas dyn_list_double2_refine = TR_dld2.refine
thm TR_dld2.refine TR_dld2_def

lemma II:
  fixes A :: "_ ⇒ ecost"
  shows "sup A 0 = A" 
  apply (auto simp: sup_fun_def sup_acost_def zero_acost_def) apply(rule ext)  
  by (simp add: complete_linorder_sup_max)  


lemma  III:
  shows "sup ( (TTId A) :: _ ⇒ ecost) (TTId B) = TTId (A∪B)" 
  unfolding TTId_def apply(auto simp: sup_acost_def sup_fun_def)
  apply(rule ext) by (auto simp: zero_acost_def complete_linorder_sup_max)

lemma h: "(λ_. 0)(''mul'' := cost ''mul'' 1) = TTId {''mul''}"
  unfolding TTId_def by auto

schematic_goal TR_dld2_alt: "TR_dld2 = ?A"
  apply(rule hide)
  unfolding TR_dld2_def
  unfolding list_copy_spec_time_def
  apply(simp only: II III h )
  apply(auto simp: currs_of_add)
  apply(subst currs_of_costmult_gt) apply (simp add: zero_enat_def)
  unfolding list_copy_body_cost_def
  apply(auto simp: currs_of_add norm_cost)
  apply(auto simp: currs_of_cost_gt zero_enat_def) 
  apply(subst currs_of_cost_gt, simp)+ 
  apply simp
  apply(rule hideI) apply simp done

(* obsolete *)
lemma dyn_list_double2_refine_coarse: "dyn_list_double2 (bs, l, c) ≤ ⇓ Id (⇓⇩C TId (dyn_list_double (bs, l, c)))"
  unfolding dyn_list_double2_def dyn_list_double_def
  unfolding mop_free_def
  apply normalize_blocks
  apply(refine_rcg bindT_refine_easy SPECc2_refine mop_array_new_Trefinement
        list_copy_self_refine
       )
  apply refine_dref_type
  by (auto simp: TId_apply)


  thm bindT_refine_conc_time_my_inres_sup

lemma wfR''_TR_dld2[simp]: "wfR'' TR_dld2"
  unfolding TR_dld2_alt apply(rule wfR''_TTId_if_finite)
  by simp


  thm dyn_list_double2_refine dyn_list_double_correct

lemma dyn_list_double2_correct:"⟦0 < c; l = c; (bs,bs')∈Id; (l,l')∈Id; (c,c')∈Id ⟧ ⟹
  dyn_list_double2 (bs', l', c') ≤ ⇓ Id (⇓⇩C (pp TR_dld2 TR_doublec) (dyn_list_double_spec (bs, l, c))) "
  apply(rule order.trans)
   apply(rule dyn_list_double2_refine) apply simp apply simp apply simp
  apply (simp add: timerefine_id timerefine_iter2[symmetric])
  apply(rule timerefine_mono2)
  subgoal  by simp 
  apply(rule order.trans[rotated])
   apply(rule dyn_list_double_correct[simplified])
  by auto


lemma "pp TR (F(x:=l)) = (pp TR F)(x:=timerefineA TR l)"
  using pp_fun_upd by metis

lemma pp_0: "pp TR 0 = (0::_ ⇒ ecost)"
  unfolding pp_def by(auto simp: zero_acost_def)

schematic_goal TR_dld2_dynaaray_simp: "(pp TR_dld2 TR_doublec) = ?gg"
  apply(rule hide)
  unfolding TR_doublec_def 
  apply(simp only: pp_fun_upd pp_0)
  unfolding list_copy_body_cost_def
  apply(auto simp: norm_cost )
  apply(auto simp: TR_dld2_alt TTId_simps)
  apply(auto simp: costmult_cost)
  apply(rule hideI)
  apply(rule refl) done

thm TR_dld2_dynaaray_simp


term dyn_list_push_basic_spec
                               
definition dyn_list_push_basic :: "'a::llvm_rep list × nat × nat ⇒ 'a ⇒ ('a list × nat × nat, (char list, enat) acost) nrest" where
  "dyn_list_push_basic ≡ λ(bs,l,c) x. doN {
      ASSERT (l < length bs ∧ length bs = c);
      bs' ← mop_array_upd  bs l x;
      l' ← SPECc2 ''add'' (+) l 1;
      RETURNT (bs',l',c)
  }"

lemma mop_array_upd_refines:
  "(bs,bs')∈Id ⟹ (l,l')∈Id ⟹ (x,x')∈Id 
     ⟹ mop_array_upd bs l x ≤  ⇓Id (⇓⇩C (0(''list_set'':=lift_acost mop_array_upd_cost)) (mop_list_setN bs' l' x'))"
  unfolding mop_array_upd_def mop_list_set_def
  apply(refine_rcg) by (auto simp: norm_cost)
  

schematic_goal dyn_list_push_basic_refine_tight:
  "(bs,bs')∈Id ⟹ (l,l')∈Id ⟹ (c,c')∈Id ⟹ (x,x')∈Id
    ⟹ dyn_list_push_basic (bs,l,c) x  ≤ ⇓Id (⇓⇩C ?TR (dyn_list_push_basic_spec (bs',l',c') x'))"
  unfolding dyn_list_push_basic_def dyn_list_push_basic_spec_def
  apply(refine_rcg) apply auto[1]
  apply(refine_rcg  bindT_refine_conc_time_my_inres_sup
          SPECc2_refine_exch mop_array_upd_refines)
                 apply refine_dref_type 
  by (auto simp: TId_apply intro!: wfR''_supI wfR''_TTId_if_finite )

concrete_definition TR_dlpc is dyn_list_push_basic_refine_tight uses "_ ≤ ⇓ Id (⇓⇩C ⌑ _)" 
thm TR_dlpc.refine
thm TR_dlpc.refine[no_vars]
lemma dyn_list_push_basic_refine: 
  "(dl,dl')∈Id ⟹ (x,x')∈Id ⟹ dyn_list_push_basic dl x ≤ ⇓ Id (⇓⇩C TR_dlpc (dyn_list_push_basic_spec dl' x'))"
  apply(cases dl; cases dl')
  apply(simp del: conc_Id) apply(rule TR_dlpc.refine) by auto

lemma wfR''_TR_dlpc[simp]: "wfR'' TR_dlpc"
  unfolding TR_dlpc_def
  apply(intro wfR''_supI wfR''_upd)
  by(auto)

definition has_enough_space  :: "('a::llvm_rep) list × nat × nat ⇒ (bool, (char list, enat) acost) nrest" where
  "has_enough_space = (λ(bs,l,c).  SPECc2 ''icmp_slt'' (<) l c)"

sepref_def has_enough_space_impl is "has_enough_space"
  :: "(dyn_array_raw_assn:: ('x::llvm_rep) list × nat × nat ⇒ 'x ptr × ('size_t) word × 'size_t word ⇒ assn)⇧k →⇩a (bool1_assn::bool⇒_⇒assn)"
  unfolding has_enough_space_def
  unfolding dyn_array_raw_assn_def
  by sepref

(* aktuelles design: if *)
(* besser: ensure_capacity ; push_back_basic *)
definition dynamiclist_append2 where
  "dynamiclist_append2 ≡ λdl x. doN {
      if⇩N has_enough_space dl then doN {
        dyn_list_push_basic dl x
      } else doN {          
        dl' ← dyn_list_double2 dl;
        dyn_list_push_basic dl' x
      }
  }"

lemma dynamiclist_append2_refines_tight_aux: 
    "(⟨Id⟩list_rel ×⇩r nat_rel ×⇩r nat_rel) = Id"
  apply simp done

schematic_goal dynamiclist_append2_refines_tight:
  "(bs,bs')∈Id ⟹ (l,l')∈Id ⟹ (c,c')∈Id ⟹ (x,x')∈Id ⟹
      dynamiclist_append2 (bs,l,c) x ≤  ⇓Id (⇓⇩C ?TR (dyn_list_push (bs',l',c') x'))"
  unfolding dynamiclist_append2_def dyn_list_push_def has_enough_space_def
  apply(refine_rcg) 
  apply(refine_rcg  bindT_refine_conc_time_my_inres_sup
          SPECc2_refine_exch mop_array_upd_refines
          MIf_refine_sup dyn_list_push_basic_refine
          dyn_list_double2_refine
        )
                apply refine_dref_type 
                     apply(auto)[2]
  apply(simp only: dynamiclist_append2_refines_tight_aux)
            apply(rule dyn_list_double2_correct)
  apply (auto simp: TId_apply   intro!: wfR''_supI wfR''_TTId_if_finite wfR''_ppI )
        apply(auto simp: inres_SPECc2)
  apply(auto intro!: wfR''_upd)
  done

concrete_definition TR_da is dynamiclist_append2_refines_tight uses "_ ≤ ⇓ Id (⇓⇩C ⌑ _)" 
thm TR_da_def
lemmas dynamiclist_append2_refines_aux = TR_da.refine
lemma wfR''_TR_da[simp]: "wfR'' TR_da"
  unfolding TR_da_def
  apply(intro wfR''_supI wfR''_upd wfR''_ppI) by simp_all

lemma dynamiclist_append2_refines:
    "dynamiclist_append2 dl x ≤ ⇓ Id (⇓⇩C TR_da (dyn_list_push dl x))"
  apply(cases dl) apply (simp del: conc_Id)
  apply(rule dynamiclist_append2_refines_aux) by auto
 


sepref_def dyn_list_double_impl is "dyn_list_double2 :: ('a::llvm_rep) list × _ ⇒ _"
  :: "[λ(ls,l,c). l * 2 < max_snat LENGTH('size_t)]⇩a
     (dyn_array_raw_assn :: ('a) list × nat × nat ⇒ ('a) ptr × 'size_t word × 'size_t word ⇒ assn)⇧d
        → (dyn_array_raw_assn :: ('a) list × _ ⇒ _)"
  unfolding dyn_list_double2_def
  unfolding dyn_array_raw_assn_def
  apply (annot_snat_const "TYPE('size_t)")  
  by sepref 

find_theorems rdomp array_assn
 

sepref_def dyn_list_push_basic_impl is "uncurry dyn_list_push_basic"
  :: "(dyn_array_raw_assn :: ('a::llvm_rep) list × nat × nat ⇒ ('a) ptr × 'size_t word × 'size_t word ⇒ assn)⇧d
          *⇩a id_assn⇧d
        →⇩a (dyn_array_raw_assn :: ('a) list × _ ⇒ _)"
  unfolding dyn_list_push_basic_def
  unfolding dyn_array_raw_assn_def
  apply (annot_snat_const "TYPE('size_t)")  
  by sepref 

sepref_def dyn_array_push_impl is "uncurry (dynamiclist_append2 :: ('a::llvm_rep) list × _ ⇒ _)"
    :: "[λ((dl,l,c),_). l * 2 < max_snat LENGTH('size_t)]⇩a
          (dyn_array_raw_assn :: ('a) list × nat × nat ⇒ ('a) ptr × 'size_t word × 'size_t word ⇒ assn)⇧d
             *⇩a id_assn⇧k → (dyn_array_raw_assn :: ('a) list × _ ⇒ _)"
  unfolding dynamiclist_append2_def 
  by sepref 

thm dyn_array_push_impl.refine[]

lemmas prepare = dyn_array_push_impl.refine[to_hnr, unfolded hn_ctxt_def APP_def]

definition "push_size_bound TYPE('size_t) l ≡ l * (2::nat) < max_snat LENGTH('size_t)"

lemma dyn_array_push_impl_refines: "
        push_size_bound TYPE('size_t) l ⟹
          hn_refine (dyn_array_raw_assn (bs,l,c) da' ** id_assn x x')
                        (dyn_array_push_impl da' x')
                      (invalid_assn (dyn_array_raw_assn) (bs,l,c) da' ** id_assn x x')
                        (dyn_array_raw_assn) (dynamiclist_append2 (bs,l,c) x)"
  apply(rule prepare)
  unfolding push_size_bound_def
  by auto


subsection  ‹implement empty›

definition  dynamiclist_empty2 :: "('a::llvm_rep list × nat × nat, ecost) nrest"   where
  "dynamiclist_empty2 = do {
       dst ← mop_array_new id_assn init 8 ;
       RETURNT (dst,0,8)
    }"

thm  hnr_raw_array_new
term "mop_list_init_raw (λn. lift_acost (cost'_narray_new n))"
 

lemma consumea_bind_return_is_SPECT: "do {
      _ ← consumea t;
      RETURNTecost x
    } = SPECT [x↦t]"
  unfolding consumea_def bindT_def by (auto simp add: RETURNT_def)

definition "TR_de = 0(''list_init_c'':=lift_acost (cost'_narray_new 1))"
lemma wfR''_TR_de[simp]: "wfR'' TR_de"
  unfolding TR_de_def
  by(auto intro!: wfR''_upd)

lemma emptylist2_refine_aux: "dynamiclist_empty2 ≤ ⇓⇩C TR_de dyn_list_new_raw"
  unfolding dyn_list_new_raw_def dynamiclist_empty2_def mop_array_new_def
  apply(rule order.trans)
   defer apply(rule timerefine_bindT_ge2)  
   apply (simp_all add: timerefine_consume timerefine_RETURNT) 
  apply normalize_blocks
  unfolding consumea_bind_return_is_SPECT  apply auto
  apply(auto simp: le_fun_def)
  unfolding TR_de_def apply (simp add: timerefineA_cost_apply_costmult costmult_add_distrib costmult_cost norm_cost)
  apply sc_solve by (auto simp: numeral_eq_enat )


definition "TR_dynarray =  sup TR_de TR_da"
lemma wfR''_TR_dynarray: "wfR'' TR_dynarray"
  unfolding TR_dynarray_def
  by(auto intro: wfR''_supI)


lemma sup_upd: "sup (F(x:=y::ecost)) G = (sup F G)(x:=sup y (G x))"
  unfolding fun_upd_def 
  by fastforce 

lemma sup_0:
  fixes x y z :: "_ ⇒ ecost"
  shows "sup 0 x = x" "sup (λ_. 0) y = y"
      "sup z 0 = z" "sup y (λ_. 0) = y"
  subgoal using II   sup.commute 
    by metis
  subgoal using II[unfolded zero_fun_def]   sup.commute 
    by metis
  subgoal using II 
    by metis
  subgoal using II[unfolded zero_fun_def] 
    by metis
  done

lemma sup_0_enat:
  fixes x y z :: "ecost"
  shows "sup 0 x = x" "sup z 0 = z" 
  by (simp_all add: needname_nonneg sup_absorb2 sup.commute)

thm TR_da_def

thm fun_upd_apply
lemma f_upd_app: "x≠y ⟹(f(x:=t)) y = f y"
    "x=y ⟹  (f(x:=t)) y = t"
  by simp_all

schematic_goal TR_dynarray_aux: "sup (pp TR_dld2 TR_doublec) TR_dlpc = ?x"
  apply(rule hide)
  unfolding TR_dld2_dynaaray_simp TR_dlpc_def 
  apply(simp add: sup_0_enat sup_upd sup_0 norm_cost f_upd_app del: fun_upd_apply )
  apply summarize_same_cost
  apply(rule hideI)
  by simp

schematic_goal TR_dynarray_aux2: "sup TR_dlpc (sup (pp TR_dld2 TR_doublec) TR_dlpc) = ?x"
  apply(rule hide)
  unfolding TR_dynarray_aux
  unfolding TR_dlpc_def 
  apply(simp add: sup_0_enat sup_upd sup_0 norm_cost f_upd_app del: fun_upd_apply )
  apply summarize_same_cost
  apply(rule hideI)
  by simp

lemma one_enat_fold: "enat (Suc 0) = 1"
  by (simp add: one_enat_def)
schematic_goal TR_dynarray_simplified: "TR_dynarray = ?x"
  apply(rule hide)
  unfolding TR_dynarray_def 
  unfolding TR_da_def   TR_dynarray_aux2 TR_de_def
  apply(simp add: sup_0_enat sup_upd sup_0 norm_cost f_upd_app del: fun_upd_apply )
  unfolding one_enat_fold  apply simp
  apply(rule hideI)
  by simp


lemma emptylist2_refine: "dynamiclist_empty2 ≤ ⇓⇩C TR_dynarray dyn_list_new_raw"
  unfolding TR_dynarray_def
  apply(rule timerefine_supI2[OF emptylist2_refine_aux])
  by simp_all


lemma dyn_array_push_refine: "dynamiclist_append2 dl x ≤ ⇓⇩C TR_dynarray (dyn_list_push dl x)"
  unfolding TR_dynarray_def
  apply(rule timerefine_supI[OF dynamiclist_append2_refines[simplified]])
  using dynamiclist_append2_refines
  by simp_all

 

 
(* declare [[show_types,show_consts]]
*)

  thm SIZE_T

  find_in_thms mop_list_init_raw hn_refine in sepref_fr_rules

sepref_def dynamiclist_empty_impl is "(uncurry0 (dynamiclist_empty2 :: ('a::llvm_rep list × nat × nat, ecost) nrest) )"
  :: "(unit_assn)⇧k →⇩a (dyn_array_raw_assn :: ('a::llvm_rep) list × nat × nat ⇒ ('a::llvm_rep) ptr × 'size_t word × 'size_t word ⇒ assn)"
  unfolding dynamiclist_empty2_def dyn_array_raw_assn_def
  apply (annot_snat_const "TYPE('size_t)")  
  by sepref 
   
 
   

thm dynamiclist_empty_impl.refine


definition finite_cost_preserves  :: "(_ ⇒ ecost) ⇒ bool" where
  "finite_cost_preserves TR = (∀Φ. finite {x. the_acost Φ x ≠ 0} ⟶ finite_cost Φ ⟶ finite_cost (timerefineA TR Φ))"   

lemma finite_cost_preservesI:
    "(⋀Φ. finite {x. the_acost Φ x ≠ 0} ⟹ finite_cost Φ ⟹ finite_cost (timerefineA TR Φ))
    ⟹ finite_cost_preserves TR "
  unfolding finite_cost_preserves_def by auto

lemma finite_cost_preservesD:
    "finite_cost_preserves TR ⟹ 
        finite {x. the_acost Φ x ≠ 0} ⟹ finite_cost Φ ⟹ finite_cost (timerefineA TR Φ)"
  unfolding finite_cost_preserves_def by auto

lemma finite_cost_preserves_sup:
  assumes "finite_cost Φ ⟹ finite_cost (timerefineA A Φ)"      
       "finite_cost Φ ⟹ finite_cost (timerefineA B Φ)"
      and f: "finite_cost Φ"
    shows "finite_cost (timerefineA (sup A B) Φ)"
  apply(rule finite_costI)
  subgoal for x
  using assms(1,2)[OF f, THEN finite_costD, of x]
  unfolding finite_cost_def timerefineA_def apply auto
  oops

lemma timerefineA_if_finite_support:
  "finite  {x. the_acost Φ x ≠ 0}
  ⟹ timerefineA TR Φ = acostC (λcc. sum (λac. the_acost Φ ac * the_acost (TR ac) cc) {x. the_acost Φ x ≠ 0})"
  unfolding timerefineA_def apply auto
  apply(rule ext)
  apply(subst Sum_any.expand_superset[of "{x. the_acost Φ x ≠ 0}"]) by auto


lemma finite_cost_sup:
  fixes A :: "ecost"
  shows "finite_cost A ⟹ finite_cost B ⟹ finite_cost (sup A B)"
  unfolding finite_cost_def apply (auto simp: sup_acost_def) 
  by (simp add: max_def sup_enat_def) 

thm wfR''_def


lemma finite_sum_iff: "finite S ⟹ sum f S < (∞::enat) ⟷ (∀x∈S. f x < ∞)"
  apply(induct S rule: finite_induct)
  apply simp apply auto
  by (metis add.commute enat.exhaust plus_enat_simps(3)) 

lemma finite_cost_timerefineA:
  assumes "finite  {x. the_acost Φ x ≠ (0::enat)}"
  shows "finite_cost (timerefineA A Φ) ⟷ (∀ac∈{x. the_acost Φ x ≠ 0}. (∀cc. the_acost Φ ac * the_acost (A ac) cc < ∞))"
  unfolding timerefineA_if_finite_support[OF assms(1)] finite_cost_def
  apply (simp del: enat_ord_simps(4))
  apply(subst finite_sum_iff) apply(subst assms(1))
  apply (simp del: enat_ord_simps(4)) by auto


lemma finite_cost_preserves_sup:
  fixes A :: "'a ⇒ ecost"
  assumes A: "finite_cost_preserves A"
  assumes B: "finite_cost_preserves B"
  shows "finite_cost_preserves (sup A B)"
proof (rule finite_cost_preservesI)
  fix Φ :: "('a, enat) acost"
  assume f: "finite {x. the_acost Φ x ≠ 0}" "finite_cost Φ"
  show "finite_cost (timerefineA (sup A B) Φ)"
    unfolding finite_cost_timerefineA[OF f(1)]
    apply safe
    subgoal premises p for ac cc 
    using A[THEN finite_cost_preservesD, OF f, unfolded  finite_cost_timerefineA[OF f(1)], rule_format, of ac cc]
    using B[THEN finite_cost_preservesD, OF f,  unfolded  finite_cost_timerefineA[OF f(1)], rule_format, of ac cc]
    using p apply simp
    by (simp add: max_def sup_acost_def sup_max)
  done
qed


lemma finite_cost_preserves_upd:
  assumes  "finite_cost_preserves F " " finite_cost a"
  shows "finite_cost_preserves (F(x:=a))"
  apply(rule finite_cost_preservesI)  
  subgoal premises p for Φ
  apply(subst finite_cost_timerefineA)
  apply (simp add: p)
  using assms(1)[THEN finite_cost_preservesD, OF p]
  apply(subst (asm) finite_cost_timerefineA)
   apply (simp add: p)
  apply auto
  using assms(2)[unfolded finite_cost_def] 
  by (metis finite_costD less_infinityE p(2) times_enat_simps(1)) 
  done

lemma finite_cost_zero: "finite_cost (0::ecost)"
  unfolding finite_cost_def by (auto simp: zero_acost_def) 

lemma timerefineA_zero_acost[simp]: "timerefineA 0 Φ = 0"
  unfolding timerefineA_def by (auto simp: zero_acost_def)
lemma timerefineA_zero_acost'[simp]: "timerefineA (λ_. 0) Φ = 0"
  unfolding timerefineA_def by (auto simp: zero_acost_def)

lemma finite_cost_cost_enat[simp]: "x < ∞ ⟹ finite_cost (cost n (x::enat))"
  apply(rule finite_costI)
  by (auto simp: cost_def zero_acost_def zero_enat_def ) 

lemma finite_cost_preserves_zero[simp]:
  "finite_cost_preserves (0::_⇒ecost)"
  apply(rule finite_cost_preservesI) 
  by (auto simp: finite_cost_zero) 
lemma finite_cost_preserves_zero'[simp]:
  "finite_cost_preserves ((λ_. 0)::_⇒ecost)"
  apply(rule finite_cost_preservesI) 
  by (auto simp: finite_cost_zero) 

(* finite_cost_preserves_pp may even be wrong 
lemma finite_Sum_any_comp: 
  fixes  R :: "'a ⇒ ecost"
  assumes "∀f. finite {s. the_acost (B s) f ≠ 0}" "finite {x. the_acost Φ x ≠ 0}"
  shows "finite {x. ((Sum_any (λac. (the_acost Mc ac * (the_acost (R ac) x)))) ≠ 0)}"
proof - 
  thm finite_cartesian_product

  have "⋀f. G ( {x. the_acost Φ x ≠ 0} × {s. the_acost (B s) f ≠ 0})" sorry

  {fix x
    have "((Sum_any (λac. ((the_acost Mc ac) * (the_acost (R ac) x)))) ≠ 0)
      ⟹ ∃ac. (the_acost Mc ac) * (the_acost (R ac) x) ≠ 0"
      using Sum_any.not_neutral_obtains_not_neutral by blast 
  } then 
  have "{x. ((Sum_any (λac. ((the_acost Mc ac) * (the_acost (R ac) x)))) ≠ 0)}
          ⊆ {x. ∃ac. ((the_acost Mc ac) * (the_acost (R ac) x)) ≠ 0}" by blast
  also have "… ⊆ snd ` {(ac,x). ((the_acost Mc ac) * (the_acost (R ac) x)) ≠ 0}" by auto 
  also have "… ⊆ snd ` {(ac,x).  (the_acost (R ac) x) ≠ 0 ∧ (the_acost Mc ac) ≠ 0}" by auto


  finally  show ?thesis 
    apply(rule finite_subset ) apply auto
    apply(rule finite_imageI) 
    apply(rule finite_subset )
    
qed 


lemma finite_cost_preserves_pp:
  fixes A :: "string ⇒ ecost"
  and  B :: "string ⇒ ecost"
  assumes A: "finite_cost_preserves A"
      and B:  "finite_cost_preserves B"
      and "wfR'' A" "wfR'' B"
      shows "finite_cost_preserves (pp A B)"
proof (rule finite_cost_preservesI)
  fix Φ :: "ecost"
  assume T: "finite {x. the_acost Φ x ≠ 0}" "finite_cost Φ"  
  have "finite {x. the_acost (timerefineA B Φ) x ≠ 0}" "finite_cost (timerefineA B Φ)"
    subgoal using assms(4)[unfolded wfR''_def] T 
      unfolding timerefineA_def
      apply simp apply(rule wfR_finite_Sum_any)
      unfolding wfR_def 
      sorry
    subgoal
      using B[THEN finite_cost_preservesD, OF T] .
    done
  from A[THEN finite_cost_preservesD, OF this]
  have "finite_cost (timerefineA A (timerefineA B Φ))" .

  show "finite_cost (timerefineA (pp A B) Φ)"
    apply(subst timerefineA_iter2[symmetric])
    by fact+ 
qed *)


lemma finite_cost_preserves_TTId:
  "finite A ⟹ finite_cost_preserves (TTId A)"
  apply(rule finite_cost_preservesI)
  unfolding finite_cost_def 
  apply(subst timerefineA_if_finite_support) apply simp
  apply (simp del: enat_ord_simps(4)) apply safe
  apply(subst finite_sum_iff)
  by (auto simp: TTId_def zero_acost_def norm_cost cost_def simp del: enat_ord_simps(4))

lemma finite_cost_addI:
  fixes a b :: ecost
  shows "finite_cost a ⟹ finite_cost b ⟹ finite_cost (a+b)"
  unfolding finite_cost_def apply (cases a; cases b; auto simp: plus_acost_alt)
  by (metis plus_enat_simps(1)) 

lemma finite_cost_preserves_TR_dlpc: "finite_cost_preserves TR_dlpc"
  unfolding TR_dlpc_def
  apply(intro finite_cost_preserves_sup)
  subgoal 
    apply(intro finite_cost_preserves_upd)
    by (simp_all add: finite_cost_lift_acost)
  subgoal 
    apply(intro finite_cost_preserves_upd)
    by (simp_all add: finite_cost_lift_acost)
  by (simp_all add: finite_cost_lift_acost)

lemma finite_cost_preserves_TR_dynarray: "finite_cost_preserves TR_dynarray"
  unfolding TR_dynarray_def
  apply(rule finite_cost_preserves_sup)
  subgoal 
    unfolding TR_de_def  
    apply(rule finite_cost_preserves_upd) by (simp_all add: finite_cost_lift_acost)
  subgoal 
    unfolding TR_da_def  
    apply(intro finite_cost_preserves_sup)
    subgoal 
      apply(rule finite_cost_preserves_upd) by (simp_all add: finite_cost_lift_acost)
    subgoal 
      apply(intro finite_cost_preserves_upd) by (simp_all add: finite_cost_lift_acost)
    subgoal  
      by (fact finite_cost_preserves_TR_dlpc)
    subgoal 
      unfolding TR_dld2_dynaaray_simp
      apply(intro finite_cost_addI finite_cost_preserves_sup finite_cost_preserves_upd finite_cost_preserves_TTId)       
      by (simp_all add: norm_cost) 
    subgoal 
      by (fact finite_cost_preserves_TR_dlpc)
    done
  done

interpretation dyn_array: dyn_list_impl TR_dynarray dyn_array_raw_assn
                            "push_size_bound TYPE('size_t)" dynamiclist_append2 dyn_array_push_impl
                            dynamiclist_empty2 dynamiclist_empty_impl
      (*                       
    defines dynamic_array_append_spec = "dyn_array.dyn_array_push_spec"
      and dynamic_array_empty_spec = "dyn_array.dynamiclist_empty_spec" 
      and dynamic_array_assn = dyn_array.dyn_array_assn *)
  apply standard (* TODO: provide the implementations *)
  subgoal by (fact wfR''_TR_dynarray)
  subgoal
    apply(rule finite_cost_preservesD) apply auto
    apply(rule finite_cost_preserves_TR_dynarray) done
  subgoal by(fact dyn_array_push_refine)
  subgoal apply(rule dyn_array_push_impl_refines) by simp
  subgoal by (fact dynamiclist_empty_impl.refine)
  subgoal by (fact emptylist2_refine) 
  done 


sepref_register dyn_array.dyn_array_push_spec
lemmas da_push_rule  = dyn_array.G_push
declare dyn_array.G_push[sepref_fr_rules]
thm dyn_array.G_push

term dynamic_array_empty_spec
sepref_register dyn_array.dynamiclist_empty_spec
lemmas da_empty_rule = dyn_array.GGG_empty 
declare dyn_array.GGG_empty[sepref_fr_rules]
thm dyn_array.GGG_empty  

lemmas dyn_array_dyn_array_push_spec_def = dyn_array.dyn_array_push_spec_def
lemmas  dyn_array_dynamiclist_empty_spec_def =  dyn_array.dynamiclist_empty_spec_def
lemmas  dyn_array_dynamic_array_assn_def =  dyn_array.dyn_array_assn_def

term dyn_array.dyn_array_assn

thm dyn_array.dyn_array_push_impl_refines_dyn_array_push_spec dyn_array.GGG


concrete_definition dynamic_array_assn2 is dyn_array_dynamic_array_assn_def

definition  "da ≡ dyn_array.dyn_array_assn"


thm FREE_array_assn(*
lemma FREE_dynarray_assn[sepref_frame_free_rules]:
  assumes PURE: "is_pure A"
  shows "MK_FREE (dyn_array.dyn_array_assn A) dynarray_free" 
  apply rule
  unfolding dyn_array.dyn_array_assn_def
  unfolding
    dyn_list_assn.dyn_array_raw_armor_assn_def
  apply(subst hr_comp_assoc)
  unfolding dyn_array_raw_assn_def
  sorry
*)
term mop_array_nth


subsection ‹Nth operation›

definition dyn_array_nth :: "('a list × nat × nat) ⇒ nat ⇒ ('a, (char list, enat) acost) nrest"
  where "dyn_array_nth = (λ(dl,_,_) n. (mop_array_nth dl n))"

sepref_def dyn_array_nth_impl is "uncurry dyn_array_nth"
     :: "(dyn_array_raw_assn :: ('a::llvm_rep) list × nat × nat ⇒ ('a) ptr × 'size_t word × 'size_t word ⇒ assn)⇧k *⇩a (snat_assn' TYPE('size_t) )⇧k →⇩a (id_assn::'a ⇒ 'a ⇒ assn)"
  unfolding dyn_array_raw_assn_def dyn_array_nth_def
  by sepref

term dyn_array.dyn_array_assn

term nrest_rel
lemma dyn_array_nth_dyn_list_refine: "(uncurry dyn_array_nth, uncurry mop_array_nth) ∈ dyn_list_rel ×⇩r Id →⇩f  ⟨Id⟩nrest_rel "
  apply(rule)
  apply(rule nrest_C_relI)
  unfolding dyn_array_nth_def mop_array_nth_def mop_list_get_def uncurry_def
  apply(refine_rcg bindT_refine_easy)
  by(auto simp: dyn_list_rel_def)  

lemma mop_array_nth_refine_R: "(uncurry mop_array_nth, uncurry mop_array_nth) ∈ ⟨R⟩list_rel ×⇩r Id →⇩f  ⟨R⟩nrest_rel"
  apply(rule)
  apply(rule nrest_C_relI)
  unfolding mop_array_nth_def mop_list_get_def uncurry_def
  apply(refine_rcg bindT_refine_easy)
  by(auto simp: param_nth list_rel_imp_same_length)

thm dyn_array_dynamic_array_assn_def
thm dyn_array.dyn_array_raw_armor_assn_def
thm dyn_array.dyn_array_raw_armor_assn_alt
(* TODO: move *) 

lemmas dyn_array_nth_aux1 = dyn_array_nth_impl.refine[THEN amor_orthogonal[where PHI=dyn_array.Φ_d], folded dyn_array.dyn_array_raw_armor_assn_alt]


thm dyn_array_nth_aux1 dyn_array_nth_dyn_list_refine
lemmas dyn_array_nth_aux2 = dyn_array_nth_aux1[FCOMP dyn_array_nth_dyn_list_refine]
thm dyn_array_nth_aux2 mop_array_nth_refine_R
thm fcomp_norm_unfold
thm fcomp_norm_norm
lemmas dyn_array_nth_rule = dyn_array_nth_aux2[FCOMP mop_array_nth_refine_R]



subsection ‹length operation›

definition dyn_array_length :: "(('a::llvm_rep) list × nat × nat) ⇒ (nat, (char list, enat) acost) nrest"
  where "dyn_array_length = (λ(_,l,_) . RETURNT l)"



sepref_def dyn_array_length_impl is "dyn_array_length"
     :: "(dyn_array_raw_assn :: ('a::llvm_rep) list × nat × nat ⇒ ('a) ptr × 'size_t word × 'size_t word ⇒ assn)⇧k →⇩a  (snat_assn' TYPE('size_t) )"
  unfolding dyn_array_raw_assn_def dyn_array_length_def
  by sepref

lemmas dyn_array_length_aux1 = dyn_array_length_impl.refine[THEN amor_orthogonal_empt[where PHI=dyn_array.Φ_d], folded dyn_array.dyn_array_raw_armor_assn_alt]

lemma dyn_array_length_dyn_list_refine: "(dyn_array_length, mop_list_length) ∈ dyn_list_rel →⇩f  ⟨nat_rel⟩nrest_rel "
  apply(rule)
  apply(rule nrest_C_relI)
  unfolding dyn_array_length_def mop_list_length_def
  apply(refine_rcg bindT_refine_easy)
  by(auto simp: dyn_list_rel_def)  

lemma mop_array_length_refine_R: "(mop_list_length, mop_list_length) ∈ ⟨R⟩list_rel →⇩f  ⟨nat_rel⟩nrest_rel"
  apply(rule)
  apply(rule nrest_C_relI)
  unfolding mop_list_length_def
  apply(refine_rcg bindT_refine_easy)
  by(auto simp: param_nth list_rel_imp_same_length)

thm mop_array_length_refine_R mop_array_nth_refine_R

lemmas dyn_array_length_aux2 = dyn_array_length_aux1[FCOMP dyn_array_length_dyn_list_refine]
thm dyn_array_length_aux2  dyn_array_nth_aux2
thm dyn_array_length_aux2 mop_array_length_refine_R

thm dyn_array.dyn_array_raw_armor_
thm dyn_array.dyn_array_raw_armor_aux
thm fcomp_norm_unfold
lemmas dyn_array_length_rule = dyn_array_length_aux2[FCOMP mop_array_length_refine_R[where R="the_pure R" for R]]
(* TODO: IDG 
lemma dyn_array_length_rule:
  "⌦‹Sepref_Constraints.CONSTRAINT Sepref_Basic.is_pure U
       ⟹ ›(dyn_array_length_impl, mop_list_length) ∈ (dyn_array.dyn_array_assn U)⇧k →⇩a snat_assn"
  sorry *)



term dyn_array.push_concrete_advertised_cost


concrete_definition dynamic_array_append_spec_cost is dyn_array_dyn_array_push_spec_def
  uses "_ = mop_list_snoc ⌑"

schematic_goal dynamic_array_append_spec_cost_simplified: "dynamic_array_append_spec_cost = ?x"
  apply(rule hide)
  unfolding dynamic_array_append_spec_cost_def 
  unfolding push_amortized_cost_def push_overhead_cost_def
  apply(simp add: norm_cost wfR''_TR_dynarray)
  unfolding TR_dynarray_simplified
  apply(simp add: norm_cost )
  apply summarize_same_cost
  apply (simp add: numeral_eq_enat )  
  apply(rule hideI)
  by simp


schematic_goal dynamic_array_append_spec_cost_simplified2: "dyn_array.push_concrete_advertised_cost = ?x"
  apply(rule hide)
  unfolding push_amortized_cost_def unfolding push_overhead_cost_def
  apply(simp add: norm_cost wfR''_TR_dynarray)
  unfolding TR_dynarray_simplified
  apply(simp add: norm_cost )
  apply summarize_same_cost
  apply (simp add: numeral_eq_enat )  
  apply(rule hideI)
  by simp


thm dynamic_array_append_spec_cost_simplified

end

 


concrete_definition dynamiclist_empty_impl is size_t_context.dynamiclist_empty_impl_def
concrete_definition dyn_array_push_impl is size_t_context.dyn_array_push_impl_def

concrete_definition dynamic_array_append_spec is size_t_context.dyn_array_dyn_array_push_spec_def

concrete_definition dynamic_array_empty_spec is size_t_context.dyn_array_dynamiclist_empty_spec_def
thm dynamic_array_empty_spec.refine

definition [simp]: "dynamic_array_empty_spec_a TYPE('l::len2)≡ dynamic_array_empty_spec"

concrete_definition dynamic_array_assn is size_t_context.dyn_array_dynamic_array_assn_def

abbreviation "al_assn' TYPE('l::len2) R ≡ dynamic_array_assn R :: (_ ⇒ _ × 'l word × 'l word ⇒ _)"

 
thm hnr_array_nth 

term "(λ((dl,_,_),n). mop_array_nth dl n)"
term "(dynamic_array_assn A)⇧k *⇩a snat_assn⇧k →⇩a A"

(* TODO: Move *)
lemma pull_cond_hfref: "(P ⟹  p ∈ x →⇩a y) ⟹ p ∈ [λ_. P]⇩a x → y"
  unfolding hfref_def by auto


concrete_definition dyn_array_nth_impl is size_t_context.dyn_array_nth_impl_def

(* TODO one could move the definition of dyn_array_nth_impl out of the size context and
  thus avoid the precondition with the length *)
sepref_register dyn_array_nth_impl
lemma dyn_array_nth[sepref_fr_rules]:
  "Sepref_Constraints.CONSTRAINT Sepref_Basic.is_pure A
  ⟹ (uncurry dyn_array_nth_impl, uncurry mop_array_nth) ∈ [λ_. 8≤LENGTH('l)]⇩a (al_assn' TYPE('l::len2) A)⇧k *⇩a snat_assn⇧k → A"
  apply(rule pull_cond_hfref)
  apply(subgoal_tac "size_t_context TYPE('l)")
  subgoal premises p
    supply f = size_t_context.dyn_array_nth_rule[where 'size_t='l, unfolded 
                    dynamic_array_assn.refine[OF p(3)]
                    dyn_array_nth_impl.refine[OF p(3)]
                   ]
    thm f
    apply(rule f) using p by auto
  apply standard apply simp done


(*
lemma dyn_array_nth_old[sepref_fr_rules]:
  "Sepref_Constraints.CONSTRAINT Sepref_Basic.is_pure A ⟹ (uncurry dyn_array_nth, uncurry mop_array_nth)
     ∈ (dynamic_array_assn A)⇧k *⇩a snat_assn⇧k →⇩a A" 
  sorry

thm dyn_array_nth dyn_array_nth_old
*)



concrete_definition dyn_array_length_impl is size_t_context.dyn_array_length_impl_def
sepref_register dyn_array_length_impl
(* TODO one could move the definition of dyn_array_nth_impl out of the size context and
  thus avoid the precondition with the length *)
lemma dyn_array_length[sepref_fr_rules]:
  "⌦‹Sepref_Constraints.CONSTRAINT Sepref_Basic.is_pure A
  ⟹› ( dyn_array_length_impl,  mop_list_length) ∈ [λ_. 8≤LENGTH('l)]⇩a (al_assn' TYPE('l::len2) A)⇧k → snat_assn"
  apply(rule pull_cond_hfref)
  apply(subgoal_tac "size_t_context TYPE('l)")
  subgoal premises p
    supply f = size_t_context.dyn_array_length_rule[where 'size_t='l, unfolded 
                    dynamic_array_assn.refine[OF p(2)]
                    dyn_array_length_impl.refine[OF p(2)]
                   ]
    thm f
    apply(rule f) using p by auto
  apply standard apply simp done




sepref_register dynamic_array_empty_spec
sepref_register "dynamic_array_empty_spec_a TYPE('l::len2)"
lemma pf: "(uncurry0 dynamiclist_empty_impl, uncurry0 (PR_CONST (dynamic_array_empty_spec_a TYPE('l::len2))))
   ∈ [λ_. 8≤LENGTH('l)]⇩a  unit_assn⇧k → al_assn' TYPE('l) A"
  apply(rule pull_cond_hfref)
  apply(subgoal_tac "size_t_context TYPE('l)")
  subgoal premises p 
    supply f= size_t_context.da_empty_rule[where 'size_t='l, unfolded 
                    dynamic_array_assn.refine[OF p(2)]
                    dynamic_array_empty_spec.refine[OF p(2)]
                    dynamiclist_empty_impl.refine[OF p(2)] ]
    unfolding dynamic_array_empty_spec_a_def
    apply(rule f) by fact
  apply standard apply simp done
declare pf[sepref_fr_rules]


lemma annot: "dynamic_array_empty_spec = dynamic_array_empty_spec_a TYPE('l::len2)"
  apply simp done
thm annot

lemma hfrefD_precond: "(f,g) ∈ [λ_. P]⇩a S → R ⟹ P  ⟹ (f,g) ∈ S →⇩a R"
  unfolding hfref_def by auto   

lemma hfrefD_precond2: "(f,g) ∈ [λ_. P]⇩a S → R⟹ True"
  by auto    


lemma weaken_cond_hfref: "(p ∈ [λa. P' a]⇩a x → y) ⟹ (⋀a. P a ⟹ P' a)   ⟹ p ∈ [λa. P a]⇩a x → y"
  unfolding hfref_def by auto


lemma pull_cond_hfref': "(⋀a. R a ⟹ P) ⟹(P ⟹ p ∈ [R]⇩a x → y) ⟹  p ∈ [R]⇩a x → y"
  unfolding hfref_def by auto

thm size_t_context.push_size_bound_def

sepref_register dynamic_array_append_spec
lemma dyn_array_push_impl_rule: "
Sepref_Constraints.CONSTRAINT Sepref_Basic.is_pure A
   ⟹ (uncurry dyn_array_push_impl, uncurry dynamic_array_append_spec)
     ∈ [λ(ls,_). 2 * length ls < max_snat LENGTH('l) ∧ 8≤LENGTH('l)]⇩a  (al_assn' TYPE('l::len2) A)⇧d *⇩a A⇧k → al_assn' TYPE('l) A"
  apply(rule pull_cond_hfref'[where P="8≤LENGTH('l)"]) apply auto[1]
  apply(subgoal_tac "size_t_context TYPE('l)")
  subgoal premises p 
    supply f= size_t_context.da_push_rule[where 'size_t='l, unfolded 
                    dynamic_array_assn.refine[OF p(3)]
                    dynamic_array_append_spec.refine[OF p(3)]
                    dyn_array_push_impl.refine[OF p(3)], unfolded PR_CONST_def ] 
    apply(rule weaken_cond_hfref[OF f] ) 
    unfolding size_t_context.push_size_bound_def size_t_context.push_size_bound_def[OF p(3)]
    using p by auto
  apply standard apply simp done 
declare dyn_array_push_impl_rule[sepref_fr_rules]


thm dynamic_array_append_spec_def


thm size_t_context.TR_dynarray_def

thm size_t_context.TR_dynarray_simplified

lemma ht_from_hnr_triv: 
  assumes "hn_refine Γ c Γ' R (SPECT (emb Q T))"
  shows " llvm_htriple ($T ** Γ) c (λr. (EXS ra. ↑(Q ra) ** R ra r) ** Γ')" 
  apply(rule ht_from_hnr[where Φ=True and E="TId", simplified timerefineA_TId_eq])
  using assms by (auto simp: timerefine_id)  



concrete_definition da_append_spec_cost is size_t_context.dynamic_array_append_spec_cost_simplified2
  uses "_ = ⌑"



lemma assumes "Sepref_Basic.is_pure A"
  and "2 * length a < max_snat LENGTH('c::len2)"
  and "8 ≤ LENGTH('c)"
shows dyn_array_push_impl_ht': "llvm_htriple ($da_append_spec_cost ∧* al_assn' TYPE('c) A a ai ∧* A b bi) (dyn_array_push_impl ai bi)
     (λr. (λs. ∃x. (↑(x = a @ [b]) ∧* dynamic_array_assn A x r) s) ∧* hn_invalid (dynamic_array_assn A) a ai ∧* A b bi)"
proof - 
  from assms(3) have S: "size_t_context TYPE('c)"
    apply unfold_locales .

  note f = size_t_context.dynamic_array_append_spec_cost_simplified2[OF S, folded da_append_spec_cost_def]

  from dyn_array_push_impl_rule[to_hnr, unfolded dynamic_array_append_spec_def f APP_def mop_list_snoc_def SPECT_assign_emb'
               , THEN  ht_from_hnr_triv]
  show ?thesis
    unfolding Sepref_Constraints.CONSTRAINT_def hn_ctxt_def using assms by fast
qed


(* TODO: Move *)
lemma sep_conj_pred_lift: "(A ∧* (pred_lift B)) s = (A s ∧ B)"
  apply(cases B) by (auto simp: pure_true_conv)

lemma introsort_final_hoare_triple:assumes "Sepref_Basic.is_pure A"
  and "2 * length a < max_snat LENGTH('c::len2)"
  and "8 ≤ LENGTH('c)"
shows dyn_array_push_impl_ht: "llvm_htriple ($da_append_spec_cost ∧* al_assn' TYPE('c) A a ai ∧* A b bi) (dyn_array_push_impl ai bi)
     (λr. (λs. ∃x. (↑(x = a @ [b]) ∧* dynamic_array_assn A x r) s) ∧* A b bi)"
  apply(rule cons_post_rule) (* TODO: very ugly proof to get rid of the invalid_assn! *)
   apply (rule dyn_array_push_impl_ht'[OF assms, unfolded hn_ctxt_def]) 
  apply(simp add: pred_lift_extract_simps  invalid_assn_def pure_part_def)
  apply(subst (asm) (2) sep_conj_commute)
  apply(subst (asm) (1) sep_conj_assoc[symmetric])
  apply(subst (asm) sep_conj_pred_lift) by simp

lemma Sum_any_cost: "Sum_any (the_acost (cost n x)) = x"
  unfolding cost_def by (simp add: zero_acost_def)
lemma sum_any_push_costmul: "Sum_any (the_acost (n *m c)) = n * (Sum_any (the_acost c))" for n :: nat 
  apply (cases c) subgoal for x
  apply (auto simp: costmult_def algebra_simps) 
  apply (cases "finite {a. x a ≠ 0}"; cases "n=0")
  apply (simp_all add: Sum_any_right_distrib)
  done done
  

schematic_goal all_da_append_spec_cost: "project_all da_append_spec_cost = ?x"
  apply (fold norm_cost_tag_def)
  unfolding da_append_spec_cost_def
  apply(subst project_all_is_Sumany_if_lifted )
  apply(simp only: lift_acost_cost[symmetric] lift_acost_propagate[symmetric]) 
  apply(simp add: the_acost_propagate add.assoc) 
  
  supply acost_finiteIs = finite_sum_nonzero_cost finite_sum_nonzero_if_summands_finite_nonzero finite_the_acost_mult_nonzeroI
  
  apply (subst Sum_any.distrib, (intro acost_finiteIs;fail), (intro acost_finiteIs;fail))+
  apply (simp only: Sum_any_cost sum_any_push_costmul)
  apply (simp add: add_ac)

  by (rule norm_cost_tagI)



definition "algorithm = doN {
    (s::nat list) ← dynamic_array_empty_spec;
    s ← dynamic_array_append_spec s (0::nat);
    s ← dynamic_array_append_spec s (1::nat);
    s ← dynamic_array_append_spec s (42::nat);
    s ← dynamic_array_append_spec s (42::nat);
    s ← dynamic_array_append_spec s (32::nat);
    s ← dynamic_array_append_spec s (31::nat);
    s ← dynamic_array_append_spec s (42::nat);
    s ← dynamic_array_append_spec s (1::nat);
    s ← dynamic_array_append_spec s (1::nat);
    len ← mop_list_length s;
    s ← dynamic_array_append_spec s len;
    s ← dynamic_array_append_spec s (1::nat);
    s ← dynamic_array_append_spec s (1::nat);
    RETURNT s
  }"


term "dynamic_array_assn (snat_assn' TYPE(32))"
term "(snat_assn' TYPE(32))"

term unat_assn'

term narray_new

thm sepref_fr_rules

(* TODO: I GUESS registering those lemmas as simp is TOO eager,
    they should help solving the size side conditions in the following sepref call *)
lemmas [simp] = dynamic_array_empty_spec_def dynamic_array_append_spec_def

lemma [simp]:
  fixes t::ecost
  shows "RETURNT x ≤ SPECT [y ↦ t] ⟷ x = y"
  by (auto simp: RETURNT_def le_fun_def  ecost_nneg)  

sepref_def algorithm_impl is "uncurry0 algorithm"
  :: "(unit_assn)⇧k →⇩a al_assn' TYPE(32) (snat_assn' TYPE(32))"
  unfolding algorithm_def
    supply [[goals_limit = 2]]
  apply (annot_snat_const "TYPE(32)")
  apply(rewrite annot[where 'l=32])
  by sepref (*
  apply sepref_dbg_trans_keep
             apply sepref_dbg_trans_step_keep 
  apply(rule sepref_fr_rules(1)[unfolded PR_CONST_def])
  using sepref_fr_rules(1)

         apply sepref_dbg_trans_step
  apply(rule sepref_fr_rules(2)[unfolded PR_CONST_def])

  oops (*
  apply sepref_dbg_preproc
  apply sepref_dbg_cons_init
  apply sepref_dbg_id
  apply sepref_dbg_monadify
  apply sepref_dbg_opt_init
  apply sepref_dbg_trans
  apply sepref_dbg_opt
  apply sepref_dbg_cons_solve
  apply sepref_dbg_cons_solve
  apply sepref_dbg_constraints
  done *)
  *)
⌦‹


section ‹Array with Length›


definition "mop_list_length T xs = SPECT [ length xs ↦ T  ]"



definition "llist_rel = br snd (λ(l,cs). l = length cs)"

definition "llist_new ini n = doN {
        cs ← mop_list_init (λn. cost ''list_init'' (enat n)) ini n;
        RETURNT (n,cs)
      }"

lemma "llist_new ini n ≤ ⇓llist_rel (mop_list_init (λn. cost ''list_init'' (enat n)) ini n)"
  sorry

definition "llist_nth T  ≡ λ(l,cs) n. doN {
              mop_list_get T cs n
          }"

lemma "llist_nth T lcs i ≤ ⇓llist_rel (mop_list_get T cs i)"


 





section ‹Implementation of Dynamic List Operations›

subsection ‹Implementation of Dynamic List Double›

definition dyn_list_double where
  "dyn_list_double ini  ≡ λ(bs,l,c). doN {
       ASSERT (l≤length bs);
       bsl ← SPECc2 ''mul'' (*) 2 c;
       dst ← mop_list_init (λn. cost ''list_init_c'' (enat n)) ini bsl;
       list_copy dst bs l; 
       RETURNT (dst,l,bsl)
      }"


lemma "dyn_list_double ini (bs,l,c) ≤ dyn_list_double_spec (bs,l,c)"
  unfolding dyn_list_double_def dyn_list_double_spec_def
  sorry


›

end