Theory Impl_Array_Stack

section ‹Stack by Array›
theory Impl_Array_Stack
imports   
  Automatic_Refinement.Automatic_Refinement
  "../../Lib/Diff_Array"
begin

type_synonym 'a array_stack = "'a array × nat"

term Diff_Array.array_length

definition "as_raw_α s ≡ take (snd s) (list_of_array (fst s))"
definition "as_raw_invar s ≡ snd s ≤ array_length (fst s)"

definition as_rel_def_internal: "as_rel R ≡ br as_raw_α as_raw_invar O ⟨R⟩list_rel"
lemma as_rel_def: "⟨R⟩as_rel ≡ br as_raw_α as_raw_invar O ⟨R⟩list_rel"
  unfolding as_rel_def_internal[abs_def] by (simp add: relAPP_def)

lemma [relator_props]: "single_valued R ⟹ single_valued (⟨R⟩as_rel)"
  unfolding as_rel_def
  by tagged_solver

lemmas [autoref_rel_intf] = REL_INTFI[of as_rel i_list]


definition "as_empty (_::unit) ≡ (array_of_list [],0)"

lemma as_empty_refine[autoref_rules]: "(as_empty (),[]) ∈ ⟨R⟩as_rel"
  unfolding as_rel_def as_empty_def br_def
  unfolding as_raw_α_def as_raw_invar_def
  by auto


definition "as_push s x ≡ let
    (a,n)=s;
    a = if n = array_length a then
        array_grow a (max 4 (2*n)) x
      else a;
    a = array_set a n x
  in
    (a,n+1)"

lemma as_push_refine[autoref_rules]: 
  "(as_push,op_list_append_elem) ∈ ⟨R⟩as_rel → R → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (simp add: as_push_def op_list_append_elem_def as_rel_def br_def
    as_raw_α_def as_raw_invar_def)
  apply clarsimp
  apply safe
  apply (rule)
  apply auto []
  apply (clarsimp simp: array_length_list) []
  apply parametricity

  apply rule
  apply auto []
  apply (auto simp: take_Suc_conv_app_nth array_length_list list_update_append) []
  apply parametricity
  done

term array_shrink

definition "as_shrink s ≡ let 
    (a,n) = s;
    a = if 128*n ≤ array_length a ∧ n>4 then
        array_shrink a n
      else a
  in
    (a,n)"

lemma as_shrink_id_refine: "(as_shrink,id) ∈ ⟨R⟩as_rel → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (simp add: as_shrink_def as_rel_def br_def
    as_raw_α_def as_raw_invar_def Let_def)
  apply clarsimp
  apply safe

  apply (rule)
  apply (auto simp: array_length_list)
  done

lemma as_shrinkI:
  assumes [param]: "(s,a)∈⟨R⟩as_rel"
  shows "(as_shrink s,a)∈⟨R⟩as_rel"
  apply (subst id_apply[of a,symmetric])
  apply (parametricity add: as_shrink_id_refine)
  done

definition "as_pop s ≡ let (a,n)=s in as_shrink (a,n - 1)"

lemma as_pop_refine[autoref_rules]: "(as_pop,butlast) ∈ ⟨R⟩as_rel → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (clarsimp simp add: as_pop_def split: prod.split)
  apply (rule as_shrinkI)

  apply (simp add: as_pop_def as_rel_def br_def
    as_raw_α_def as_raw_invar_def Let_def)
  apply clarsimp

  apply rule
  apply (auto simp: array_length_list) []
  apply (clarsimp simp: array_length_list take_minus_one_conv_butlast) []
  apply parametricity
  done
  
definition "as_get s i ≡ let (a,_::nat)=s in array_get a i"

lemma as_get_refine: 
  assumes 1: "i'<length l" 
  assumes 2: "(a,l)∈⟨R⟩as_rel" 
  assumes 3[param]: "(i,i')∈nat_rel"
  shows "(as_get a i,l!i')∈R"
  using 2
  apply (clarsimp 
    simp add: as_get_def as_rel_def br_def as_raw_α_def as_raw_invar_def
    split: prod.split)
  apply (rename_tac aa bb)
  apply (case_tac aa, simp)
proof -
  fix n cl
  assume TKR[param]: "(take n cl, l) ∈ ⟨R⟩list_rel"

  have "(take n cl!i, l!i')∈R"
    by parametricity (rule 1)
  also have "take n cl!i = cl!i"
    using 1 3 list_rel_imp_same_length[OF TKR]
    by simp
  finally show "(cl!i,l!i')∈R" .
qed
  
context begin interpretation autoref_syn .
lemma as_get_autoref[autoref_rules]: 
  assumes "(l,l')∈⟨R⟩as_rel"
  assumes "(i,i')∈Id"
  assumes "SIDE_PRECOND (i' < length l')"
  shows "(as_get l i,(OP nth ::: ⟨R⟩as_rel → nat_rel → R)$l'$i')∈R"
  using assms by (simp add: as_get_refine)

definition "as_set s i x ≡ let (a,n::nat)=s in (array_set a i x,n)"

lemma as_set_refine[autoref_rules]: 
  "(as_set,list_update)∈⟨R⟩as_rel → nat_rel → R → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (clarsimp 
    simp: as_set_def as_rel_def br_def as_raw_α_def as_raw_invar_def
    split: prod.split)
  apply rule
  apply auto []
  apply parametricity
  by simp

definition as_length :: "'a array_stack ⇒ nat" where 
  "as_length = snd"

lemma as_length_refine[autoref_rules]: 
  "(as_length,length) ∈ ⟨R⟩as_rel → nat_rel"
  by (auto 
    simp: as_length_def as_rel_def br_def as_raw_α_def as_raw_invar_def
      array_length_list
    dest!: list_rel_imp_same_length
  )

definition "as_top s ≡ as_get s (as_length s - 1)"

lemma as_top_code[code]: "as_top s = (let (a,n)=s in array_get a (n - 1))"
  unfolding as_top_def as_get_def as_length_def 
  by (auto split: prod.split)

lemma as_top_refine: "⟦l≠[]; (s,l)∈⟨R⟩as_rel⟧ ⟹ (as_top s,last l)∈R"
  unfolding as_top_def
  apply (simp add: last_conv_nth)
  apply (rule as_get_refine)
  apply (auto simp: as_length_def as_rel_def br_def as_raw_α_def 
    as_raw_invar_def array_length_list
    dest!: list_rel_imp_same_length)
  done

lemma as_top_autoref[autoref_rules]:
  assumes "(l,l')∈⟨R⟩as_rel"
  assumes "SIDE_PRECOND (l' ≠ [])"
  shows "(as_top l,(OP last ::: ⟨R⟩as_rel → R)$l')∈R"
  using assms by (simp add: as_top_refine)


definition "as_is_empty s ≡ as_length s = 0"
lemma as_is_empty_code[code]: "as_is_empty s = (snd s = 0)"
  unfolding as_is_empty_def as_length_def by simp

lemma as_is_empty_refine[autoref_rules]: 
  "(as_is_empty,is_Nil) ∈ ⟨R⟩as_rel → bool_rel"
proof
  fix s l
  assume [param]: "(s,l)∈⟨R⟩as_rel"
  have "(as_is_empty s,length l = 0) ∈ bool_rel"
    unfolding as_is_empty_def
    by (parametricity add: as_length_refine)
  also have "length l = 0 ⟷ is_Nil l"
    by (cases l) auto
  finally show "(as_is_empty s, is_Nil l) ∈ bool_rel" .
qed

definition "as_take m s ≡ let (a,n) = s in 
  if m<n then 
    as_shrink (a,m)
  else (a,n)"

lemma as_take_refine[autoref_rules]: 
  "(as_take,take)∈nat_rel → ⟨R⟩as_rel → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (clarsimp simp add: as_take_def, safe)

  apply (rule as_shrinkI)
  apply (simp add: as_rel_def br_def as_raw_α_def as_raw_invar_def)
  apply rule
  apply auto []
  apply clarsimp
  apply (subgoal_tac "take a' (list_of_array a) = take a' (take ba (list_of_array a))")
  apply (simp only: )
  apply (parametricity, rule IdI)
  apply simp

  apply (simp add: as_rel_def br_def as_raw_α_def as_raw_invar_def)
  apply rule
  apply auto []
  apply clarsimp
  apply (frule list_rel_imp_same_length)
  apply simp
  done

definition "as_singleton x ≡ (array_of_list [x],1)"
lemma as_singleton_refine[autoref_rules]: 
  "(as_singleton,op_list_singleton)∈R → ⟨R⟩as_rel"
  apply (intro fun_relI)
  apply (simp add: as_singleton_def as_rel_def br_def as_raw_α_def 
    as_raw_invar_def)
  apply rule
  apply (auto simp: array_length_list) []
  apply simp
  done

end

end