Theory Impl_Array_Map

section ‹\isaheader{Array-Based Maps with Natural Number Keys}›
theory Impl_Array_Map
imports 
  Automatic_Refinement.Automatic_Refinement
  "../../Lib/Diff_Array"
  "../../Iterator/Iterator"
  "../Gen/Gen_Map"
  "../Intf/Intf_Comp"
  "../Intf/Intf_Map"
begin

type_synonym 'v iam = "'v option array"

subsection ‹Definitions›

definition iam_α :: "'v iam ⇒ nat ⇀ 'v" where
  "iam_α a i ≡ if i < array_length a then array_get a i else None"

lemma [code]: "iam_α a i ≡ array_get_oo None a i"
  unfolding array_get_oo_def iam_α_def .

abbreviation iam_invar :: "'v iam ⇒ bool" where "iam_invar ≡ λ_. True"

definition iam_empty :: "unit ⇒ 'v iam" 
  where "iam_empty ≡ λ_::unit. array_of_list []"

definition iam_lookup :: "nat ⇒ 'v iam ⇀ 'v"
  where [code_unfold]: "iam_lookup k a ≡ iam_α a k"

definition "iam_increment (l::nat) idx ≡ 
  max (idx + 1 - l) (2 * l + 3)"

lemma incr_correct: "¬ idx < l ⟹ idx < l + iam_increment l idx"
  unfolding iam_increment_def by auto

definition iam_update :: "nat ⇒ 'v ⇒ 'v iam ⇒ 'v iam"
  where "iam_update k v a ≡ let
    l = array_length a;
    a = if k < l then a else array_grow a (iam_increment l k) None
  in
    array_set a k (Some v)"

lemma [code]: "iam_update k v a ≡ array_set_oo 
  (λ_. let l=array_length a in 
         array_set (array_grow a (iam_increment l k) None) k (Some v))
  a k (Some v)"
  unfolding iam_update_def array_set_oo_def
  apply (rule eq_reflection)
  by auto


definition iam_delete :: "nat ⇒ 'v iam ⇒ 'v iam"
  where "iam_delete k a ≡ 
  if k<array_length a then array_set a k None else a"

lemma [code]: "iam_delete k a ≡ array_set_oo (λ_. a) a k None"
  unfolding iam_delete_def array_set_oo_def by auto

primrec iam_iteratei_aux 
  :: "nat ⇒ ('v iam) ⇒ ('σ⇒bool) ⇒ (nat × 'v⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ" 
  where
    "iam_iteratei_aux 0 a c f σ = σ"
  | "iam_iteratei_aux (Suc i) a c f σ = (
      if c σ then   
        iam_iteratei_aux i a c f (
          case array_get a i of None ⇒ σ | Some x ⇒ f (i, x) σ
        )
      else σ)"

definition iam_iteratei :: "'v iam ⇒ (nat × 'v,'σ) set_iterator" where 
  "iam_iteratei a = iam_iteratei_aux (array_length a) a"



subsection ‹Parametricity›

definition iam_rel_def_internal: 
  "iam_rel R ≡ ⟨⟨R⟩ option_rel⟩ array_rel"
lemma iam_rel_def: "⟨R⟩ iam_rel = ⟨⟨R⟩ option_rel⟩ array_rel"
    by (simp add: iam_rel_def_internal relAPP_def)

lemma iam_rel_sv[relator_props]:
  "single_valued Rv ⟹ single_valued (⟨Rv⟩iam_rel)"
  unfolding iam_rel_def
  by tagged_solver

lemma param_iam_α[param]:
  "(iam_α, iam_α) ∈ ⟨R⟩ iam_rel → nat_rel → ⟨R⟩ option_rel"
  unfolding iam_α_def[abs_def] iam_rel_def by parametricity

lemma param_iam_invar[param]:
  "(iam_invar, iam_invar) ∈ ⟨R⟩ iam_rel → bool_rel"
  unfolding iam_rel_def by parametricity

lemma param_iam_empty[param]: 
  "(iam_empty, iam_empty) ∈ unit_rel → ⟨R⟩iam_rel"
    unfolding iam_empty_def[abs_def] iam_rel_def by parametricity

lemma param_iam_lookup[param]: 
  "(iam_lookup, iam_lookup) ∈ nat_rel → ⟨R⟩iam_rel → ⟨R⟩option_rel"
  unfolding iam_lookup_def[abs_def] 
  by parametricity

(* TODO: why does parametricity fail here? *)
lemma param_iam_increment[param]:
  "(iam_increment, iam_increment) ∈ nat_rel → nat_rel → nat_rel"
  unfolding iam_increment_def[abs_def] 
  by simp

(* TODO: The builtin "Let" rule for parametricity does some unpleasant things
         here, leading to an unprovable subgoal. Investigate this. *)
lemma param_iam_update[param]:
  "(iam_update, iam_update) ∈ nat_rel → R → ⟨R⟩iam_rel → ⟨R⟩iam_rel"
unfolding iam_update_def[abs_def] iam_rel_def Let_def
apply parametricity
done

lemma param_iam_delete[param]:
  "(iam_delete, iam_delete) ∈ nat_rel → ⟨R⟩iam_rel → ⟨R⟩iam_rel"
  unfolding iam_delete_def[abs_def] iam_rel_def by parametricity 

lemma param_iam_iteratei_aux[param]:
  assumes I: "i ≤ array_length a"
  assumes IR: "(i,i') ∈ nat_rel"
  assumes AR: "(a,a') ∈ ⟨Ra⟩iam_rel"
  assumes CR: "(c,c') ∈ Rb → bool_rel"
  assumes FR: "(f,f') ∈ ⟨nat_rel,Ra⟩prod_rel → Rb → Rb"
  assumes σR: "(σ,σ') ∈ Rb"
  shows "(iam_iteratei_aux i a c f σ, iam_iteratei_aux i' a' c' f' σ') ∈ Rb"
  using assms
  unfolding iam_rel_def
  apply (induct i' arbitrary: i σ σ')
  apply (simp_all only: pair_in_Id_conv iam_iteratei_aux.simps)
  apply parametricity
  apply simp_all
  done

lemma param_iam_iteratei[param]:
  "(iam_iteratei,iam_iteratei) ∈ ⟨Ra⟩iam_rel → (Rb → bool_rel) → 
      (⟨nat_rel,Ra⟩prod_rel → Rb → Rb) → Rb → Rb"
  unfolding iam_iteratei_def[abs_def] 
  by parametricity (simp_all add: iam_rel_def)



subsection ‹Correctness›

definition "iam_rel' ≡ br iam_α iam_invar"

lemma iam_empty_correct:
  "(iam_empty (), Map.empty) ∈  iam_rel'" 
   by (simp add: iam_rel'_def br_def iam_α_def[abs_def] iam_empty_def)

lemma iam_update_correct:
  "(iam_update,op_map_update) ∈ nat_rel → Id → iam_rel'  → iam_rel'"
   by (auto simp: iam_rel'_def br_def Let_def array_get_array_set_other 
                  incr_correct iam_α_def[abs_def] iam_update_def)

lemma iam_lookup_correct:
  "(iam_lookup,op_map_lookup) ∈ Id → iam_rel' → ⟨Id⟩option_rel"
   by (auto simp: iam_rel'_def br_def iam_lookup_def[abs_def])


lemma array_get_set_iff: "i<array_length a ⟹ 
  array_get (array_set a i x) j = (if i=j then x else array_get a j)"
  by (auto simp: array_get_array_set_other)

lemma iam_delete_correct:
  "(iam_delete,op_map_delete) ∈ Id → iam_rel' → iam_rel'"
  unfolding iam_α_def[abs_def] iam_delete_def[abs_def] iam_rel'_def br_def
  by (auto simp: Let_def array_get_set_iff)

definition iam_map_rel_def_internal: 
  "iam_map_rel Rk Rv ≡ 
    if Rk=nat_rel then ⟨Rv⟩iam_rel O iam_rel' else {}"
lemma iam_map_rel_def: 
  "⟨nat_rel,Rv⟩iam_map_rel ≡ ⟨Rv⟩iam_rel O iam_rel'" 
  unfolding iam_map_rel_def_internal relAPP_def by simp


lemmas [autoref_rel_intf] = REL_INTFI[of "iam_map_rel" i_map]

lemma iam_map_rel_sv[relator_props]:
  "single_valued Rv ⟹ single_valued (⟨nat_rel,Rv⟩iam_map_rel)"
  unfolding iam_map_rel_def iam_rel'_def by tagged_solver

lemma iam_empty_impl: 
    "(iam_empty (), op_map_empty) ∈ ⟨nat_rel,R⟩iam_map_rel"
  unfolding iam_map_rel_def op_map_empty_def
  apply (intro relcompI)
  apply (rule param_iam_empty[THEN fun_relD], simp)
  apply (rule iam_empty_correct)
  done


lemma iam_lookup_impl: 
    "(iam_lookup, op_map_lookup) 
  ∈ nat_rel → ⟨nat_rel,R⟩iam_map_rel → ⟨R⟩option_rel"
unfolding iam_map_rel_def
apply (intro fun_relI)
apply (elim relcompE)
apply (frule iam_lookup_correct[param_fo], assumption)
apply (frule param_iam_lookup[param_fo], assumption)
apply simp
done

lemma iam_update_impl:
   "(iam_update, op_map_update) ∈ 
     nat_rel → R → ⟨nat_rel,R⟩iam_map_rel → ⟨nat_rel,R⟩iam_map_rel"
  unfolding iam_map_rel_def
  apply (intro fun_relI, elim relcompEpair, intro relcompI)
  apply (erule (2) param_iam_update[param_fo])
  apply (rule iam_update_correct[param_fo])
  apply simp_all
  done

lemma iam_delete_impl: 
    "(iam_delete, op_map_delete) ∈
        nat_rel → ⟨nat_rel,R⟩iam_map_rel → ⟨nat_rel,R⟩iam_map_rel"
  unfolding iam_map_rel_def
  apply (intro fun_relI, elim relcompEpair, intro relcompI)
  apply (erule (1) param_iam_delete[param_fo])
  apply (rule iam_delete_correct[param_fo])
  by simp_all

lemmas iam_map_impl =
  iam_empty_impl
  iam_lookup_impl
  iam_update_impl
  iam_delete_impl

declare iam_map_impl[autoref_rules]



subsection ‹Iterator proofs›

abbreviation "iam_to_list a ≡ it_to_list iam_iteratei a"

lemma distinct_iam_to_list_aux:
  shows "⟦distinct xs; ∀(i,_)∈set xs. i ≥ n⟧ ⟹ 
        distinct (iam_iteratei_aux n a 
            (λ_.True) (λx y. y @ [x]) xs)" 
   (is "⟦_;_⟧ ⟹ distinct (?iam_to_list_aux n xs)")
proof (induction n arbitrary: xs)
  case (0 xs) thus ?case by simp
next
  case (Suc i xs)
    show ?case 
    proof (cases "array_get a i")
      case None
        with Suc.IH[OF Suc.prems(1)] Suc.prems(2)
            show ?thesis by force
    next
      case (Some x)
        let ?xs' = "xs @ [(i,x)]"
        from Suc.prems have "distinct ?xs'" and 
            "∀(i',x)∈set ?xs'. i' ≥ i" by force+
        from Some and Suc.IH[OF this] show ?thesis by simp
  qed
qed

lemma distinct_iam_to_list:
  "distinct (iam_to_list a)"
unfolding it_to_list_def iam_iteratei_def
  by (force intro: distinct_iam_to_list_aux)

lemma iam_to_list_set_correct_aux:
  assumes "(a, m) ∈ iam_rel'"
  shows "⟦n ≤ array_length a; map_to_set m - {(k,v). k < n} = set xs⟧
         ⟹ map_to_set m = 
             set (iam_iteratei_aux n a (λ_.True) (λx y. y @ [x]) xs)"
proof (induction n arbitrary: xs)
  case (0 xs)
    thus ?case by simp
next
  case (Suc n xs)
    with assms have [simp]: "array_get a n = m n" 
        unfolding iam_rel'_def br_def iam_α_def[abs_def] by simp
    show ?case 
    proof (cases "m n")
      case None
        with Suc.prems(2) have "map_to_set m - {(k,v). k < n} = set xs"
        unfolding map_to_set_def by (fastforce simp: less_Suc_eq)
        from None and Suc.IH[OF _ this] and Suc.prems(1) 
            show ?thesis by simp
    next
      case (Some x)
        let ?xs' = "xs @ [(n,x)]"
        from Some and Suc.prems(2)
            have "map_to_set m - {(k,v). k < n} = set ?xs'"
            unfolding map_to_set_def by (fastforce simp: less_Suc_eq)
        from Some and Suc.IH[OF _ this] and Suc.prems(1)
            show ?thesis by simp
    qed
qed

lemma iam_to_list_set_correct:
  assumes "(a, m) ∈ iam_rel'"
  shows "map_to_set m = set (iam_to_list a)"
proof-
  from assms 
      have A: "map_to_set m - {(k, v). k < array_length a} = set []"
      unfolding map_to_set_def iam_rel'_def br_def iam_α_def[abs_def]
      by (force split: if_split_asm)
  with iam_to_list_set_correct_aux[OF assms _ A] show ?thesis
    unfolding it_to_list_def iam_iteratei_def by simp
qed

lemma iam_iteratei_aux_append:
  "n ≤ length xs ⟹ iam_iteratei_aux n (Array (xs @ ys)) = 
             iam_iteratei_aux n (Array xs)"
apply (induction n)
apply force
apply (intro ext, auto split: option.split simp: nth_append)
done

lemma iam_iteratei_append: 
  "iam_iteratei (Array (xs @ [None])) c f σ =
       iam_iteratei (Array xs) c f σ"
  "iam_iteratei (Array (xs @ [Some x])) c f σ = 
       iam_iteratei (Array xs) c f 
       (if c σ then (f (length xs, x) σ) else σ)"
unfolding  iam_iteratei_def 
apply (cases "length xs")
apply (simp add: iam_iteratei_aux_append)
apply (force simp: nth_append iam_iteratei_aux_append) []
apply (cases "length xs")
apply (simp add: iam_iteratei_aux_append)
apply (force split: option.split 
             simp: nth_append iam_iteratei_aux_append) []
done


lemma iam_iteratei_aux_Cons:
  "n < array_length a ⟹
      iam_iteratei_aux n a (λ_. True) (λx l. l @ [x]) (x#xs) =
      x # iam_iteratei_aux n a (λ_. True) (λx l. l @ [x]) xs"
    by (induction n arbitrary: xs, auto split: option.split)

lemma iam_to_list_append: 
  "iam_to_list (Array (xs @ [None])) = iam_to_list (Array xs)"
  "iam_to_list (Array (xs @ [Some x])) = 
       (length xs, x) # iam_to_list (Array xs)"
unfolding  it_to_list_def iam_iteratei_def
apply (simp add: iam_iteratei_aux_append)
apply (simp add: iam_iteratei_aux_Cons)
apply (simp add: iam_iteratei_aux_append)
done
    
lemma autoref_iam_is_iterator[autoref_ga_rules]: 
  shows "is_map_to_list nat_rel Rv iam_map_rel iam_to_list"
  unfolding is_map_to_list_def is_map_to_sorted_list_def
proof (clarify)
  fix a m'
  assume "(a,m') ∈ ⟨nat_rel,Rv⟩iam_map_rel"
  then obtain a' where [param]: "(a,a')∈⟨Rv⟩iam_rel" 
    and "(a',m')∈iam_rel'" unfolding iam_map_rel_def by blast
  
  have "(iam_to_list a, iam_to_list a') 
            ∈ ⟨⟨nat_rel, Rv⟩prod_rel⟩list_rel" by parametricity

  moreover from distinct_iam_to_list and 
                iam_to_list_set_correct[OF ‹(a',m')∈iam_rel'›]
      have "RETURN (iam_to_list a') ≤ it_to_sorted_list
               (key_rel (λ_ _. True)) (map_to_set m')" 
      unfolding it_to_sorted_list_def key_rel_def[abs_def]
          by (force intro: refine_vcg)

  ultimately show "∃l'. (iam_to_list a, l') ∈ 
                            ⟨⟨nat_rel, Rv⟩prod_rel⟩list_rel
                    ∧ RETURN l' ≤ it_to_sorted_list (
                        key_rel (λ_ _. True)) (map_to_set m')" by blast
qed

(* We provide a ,,sorted'' iterator to simplify derivations of the
    generic algorithm library *)
lemmas [autoref_ga_rules] = 
  autoref_iam_is_iterator[unfolded is_map_to_list_def]

lemma iam_iteratei_altdef:
    "iam_iteratei a = foldli (iam_to_list a)" 
     (is "?f a = ?g (iam_to_list a)")
proof-
  obtain l where "a = Array l" by (cases a)
  have "?f (Array l) = ?g (iam_to_list (Array l))"
  proof (induction "length l" arbitrary: l)
    case (0 l)
      thus ?case by (intro ext, 
          simp add: iam_iteratei_def it_to_list_def)
  next
    case (Suc n l)
      hence "l ≠ []" and [simp]: "length l = Suc n" by force+
      with append_butlast_last_id have [simp]: 
          "butlast l @ [last l] = l" by simp
      with Suc have [simp]: "length (butlast l) = n" by simp
      note IH = Suc(1)[OF this[symmetric]]
      let ?l' = "iam_to_list (Array l)"

      show ?case
      proof (cases "last l")
        case None
          have "?f (Array l) = 
              ?f (Array (butlast l @ [last l]))" by simp
          also have "... = ?g (iam_to_list (Array (butlast l)))"
              by (force simp: None iam_iteratei_append IH)
          also have "iam_to_list (Array (butlast l)) = 
              iam_to_list (Array (butlast l @ [last l]))"
              using None by (simp add: iam_to_list_append)
          finally show "?f (Array l) = ?g ?l'" by simp
      next
        case (Some x)
          have "?f (Array l) = 
              ?f (Array (butlast l @ [last l]))" by simp
          also have "... = ?g (iam_to_list 
              (Array (butlast l @ [last l])))" 
              by (force simp: IH iam_iteratei_append 
                      iam_to_list_append Some)
          finally show ?thesis by simp
      qed
  qed
  thus ?thesis by (simp add: ‹a = Array l›)
qed


lemma pi_iam[icf_proper_iteratorI]: 
  "proper_it (iam_iteratei a) (iam_iteratei a)"
unfolding proper_it_def by (force simp: iam_iteratei_altdef)

lemma pi'_iam[icf_proper_iteratorI]: 
  "proper_it' iam_iteratei iam_iteratei"
  by (rule proper_it'I, rule pi_iam)

end