Theory Refine_Imperative_HOL.IICF_Array

section ‹Plain Arrays Implementing List Interface›
theory IICF_Array
imports "../Intf/IICF_List"
begin

  text ‹Lists of fixed length are directly implemented with arrays. ›
  definition "is_array l p ≡ p↦⇩al"

  lemma is_array_precise[safe_constraint_rules]: "precise is_array"
    apply rule
    unfolding is_array_def
    apply prec_extract_eqs
    by simp

  definition array_assn where "array_assn A ≡ hr_comp is_array (⟨the_pure A⟩list_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "array_assn A" for A]

  definition [simp,code_unfold]: "heap_array_empty ≡ Array.of_list []"
  definition [simp,code_unfold]: "heap_array_set p i v ≡ Array.upd i v p" 



context 
  notes [fcomp_norm_unfold] = array_assn_def[symmetric]
  notes [intro!] = hfrefI hn_refineI[THEN hn_refine_preI]
  notes [simp] = pure_def hn_ctxt_def is_array_def invalid_assn_def
begin  

  lemma array_empty_hnr_aux: "(uncurry0 heap_array_empty,uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_array"
    by sep_auto
  sepref_decl_impl (no_register) array_empty: array_empty_hnr_aux .

  lemma array_replicate_hnr_aux: 
    "(uncurry Array.new, uncurry (RETURN oo op_list_replicate)) 
      ∈ nat_assn⇧k *⇩a id_assn⇧k →⇩a is_array"
    by (sep_auto)
  sepref_decl_impl (no_register) array_replicate: array_replicate_hnr_aux .
   
  definition [simp]: "op_array_replicate ≡ op_list_replicate"
  sepref_register op_array_replicate
  lemma array_fold_custom_replicate:
    "replicate = op_array_replicate"
    "op_list_replicate = op_array_replicate"
    "mop_list_replicate = RETURN oo op_array_replicate"
    by (auto simp: op_array_replicate_def intro!: ext)
  lemmas array_replicate_custom_hnr[sepref_fr_rules] = array_replicate_hnr[unfolded array_fold_custom_replicate]

  lemma array_of_list_hnr_aux: "(Array.of_list,RETURN o op_list_copy) ∈ (list_assn id_assn)⇧k →⇩a is_array"
    unfolding list_assn_pure_conv
    by (sep_auto)
  sepref_decl_impl (no_register) array_of_list: array_of_list_hnr_aux .

  definition [simp]: "op_array_of_list ≡ op_list_copy"
  sepref_register op_array_of_list
  lemma array_fold_custom_of_list:
    "l = op_array_of_list l"
    "op_list_copy = op_array_of_list"
    "mop_list_copy = RETURN o op_array_of_list"
    by (auto intro!: ext)
  lemmas array_of_list_custom_hnr[sepref_fr_rules] = array_of_list_hnr[folded op_array_of_list_def]

  lemma array_copy_hnr_aux: "(array_copy, RETURN o op_list_copy) ∈ is_array⇧k →⇩a is_array"
    by sep_auto
  sepref_decl_impl array_copy: array_copy_hnr_aux .


  lemma array_get_hnr_aux: "(uncurry Array.nth,uncurry (RETURN oo op_list_get)) ∈ [λ(l,i). i<length l]⇩a is_array⇧k *⇩a nat_assn⇧k → id_assn"  
    by sep_auto
  sepref_decl_impl array_get: array_get_hnr_aux .  

  lemma array_set_hnr_aux: "(uncurry2 heap_array_set,uncurry2 (RETURN ooo op_list_set)) ∈ [λ((l,i),_). i<length l]⇩a is_array⇧d *⇩a nat_assn⇧k *⇩a id_assn⇧k → is_array"  
    by sep_auto
  sepref_decl_impl array_set: array_set_hnr_aux .

  lemma array_length_hnr_aux: "(Array.len,RETURN o op_list_length) ∈ is_array⇧k →⇩a nat_assn"  
    by sep_auto
  sepref_decl_impl array_length: array_length_hnr_aux . 

end

definition [simp]: "op_array_empty ≡ op_list_empty"
interpretation array: list_custom_empty "array_assn A" heap_array_empty op_array_empty
  apply unfold_locales
  apply (rule array_empty_hnr[simplified pre_list_empty_def])
  by (auto)



end