Theory Collections.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 Rlist_rel"
lemma as_rel_def: "Ras_rel  br as_raw_α as_raw_invar O Rlist_rel"
  unfolding as_rel_def_internal[abs_def] by (simp add: relAPP_def)

lemma [relator_props]: "single_valued R  single_valued (Ras_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 (),[])  Ras_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)  Ras_rel  R  Ras_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)  Ras_rel  Ras_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)Ras_rel"
  shows "(as_shrink s,a)Ras_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)  Ras_rel  Ras_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)Ras_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)  Rlist_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')Ras_rel"
  assumes "(i,i')Id"
  assumes "SIDE_PRECOND (i' < length l')"
  shows "(as_get l i,(OP nth ::: Ras_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)Ras_rel  nat_rel  R  Ras_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)  Ras_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)Ras_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')Ras_rel"
  assumes "SIDE_PRECOND (l'  [])"
  shows "(as_top l,(OP last ::: Ras_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)  Ras_rel  bool_rel"
proof
  fix s l
  assume [param]: "(s,l)Ras_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  Ras_rel  Ras_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  Ras_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