Theory Refine_Imperative_HOL.IICF_Array_List

```theory IICF_Array_List
imports
"../Intf/IICF_List"
Separation_Logic_Imperative_HOL.Array_Blit
begin

type_synonym 'a array_list = "'a Heap.array × nat"

definition "is_array_list l ≡ λ(a,n). ∃⇩Al'. a ↦⇩a l' * ↑(n ≤ length l' ∧ l = take n l' ∧ length l'>0)"

lemma is_array_list_prec[safe_constraint_rules]: "precise is_array_list"
unfolding is_array_list_def[abs_def]
apply(rule preciseI)
apply(simp split: prod.splits)
using preciseD snga_prec by fastforce

definition "initial_capacity ≡ 16::nat"
definition "minimum_capacity ≡ 16::nat"

definition "arl_empty ≡ do {
a ← Array.new initial_capacity default;
return (a,0)
}"

definition "arl_empty_sz init_cap ≡ do {
a ← Array.new (max init_cap minimum_capacity) default;
return (a,0)
}"

definition "arl_append ≡ λ(a,n) x. do {
len ← Array.len a;

if n<len then do {
a ← Array.upd n x a;
return (a,n+1)
} else do {
let newcap = 2 * len;
a ← array_grow a newcap default;
a ← Array.upd n x a;
return (a,n+1)
}
}"

definition "arl_copy ≡ λ(a,n). do {
a ← array_copy a;
return (a,n)
}"

definition arl_length :: "'a::heap array_list ⇒ nat Heap" where
"arl_length ≡ λ(a,n). return (n)"

definition arl_is_empty :: "'a::heap array_list ⇒ bool Heap" where
"arl_is_empty ≡ λ(a,n). return (n=0)"

definition arl_last :: "'a::heap array_list ⇒ 'a Heap" where
"arl_last ≡ λ(a,n). do {
Array.nth a (n - 1)
}"

definition arl_butlast :: "'a::heap array_list ⇒ 'a array_list Heap" where
"arl_butlast ≡ λ(a,n). do {
let n = n - 1;
len ← Array.len a;
if (n*4 < len ∧ n*2≥minimum_capacity) then do {
a ← array_shrink a (n*2);
return (a,n)
} else
return (a,n)
}"

definition arl_get :: "'a::heap array_list ⇒ nat ⇒ 'a Heap" where
"arl_get ≡ λ(a,n) i. Array.nth a i"

definition arl_set :: "'a::heap array_list ⇒ nat ⇒ 'a ⇒ 'a array_list Heap" where
"arl_set ≡ λ(a,n) i x. do { a ← Array.upd i x a; return (a,n)}"

lemma arl_empty_rule[sep_heap_rules]: "< emp > arl_empty <is_array_list []>"
by (sep_auto simp: arl_empty_def is_array_list_def initial_capacity_def)

lemma arl_empty_sz_rule[sep_heap_rules]: "< emp > arl_empty_sz N <is_array_list []>"
by (sep_auto simp: arl_empty_sz_def is_array_list_def minimum_capacity_def)

lemma arl_copy_rule[sep_heap_rules]: "< is_array_list l a > arl_copy a <λr. is_array_list l a * is_array_list l r>"
by (sep_auto simp: arl_copy_def is_array_list_def)

lemma arl_append_rule[sep_heap_rules]: "
< is_array_list l a >
arl_append a x
<λa. is_array_list (l@[x]) a >⇩t"
by (sep_auto
simp: arl_append_def is_array_list_def take_update_last neq_Nil_conv
split: prod.splits nat.split)

lemma arl_length_rule[sep_heap_rules]: "
<is_array_list l a>
arl_length a
<λr. is_array_list l a * ↑(r=length l)>"
by (sep_auto simp: arl_length_def is_array_list_def)

lemma arl_is_empty_rule[sep_heap_rules]: "
<is_array_list l a>
arl_is_empty a
<λr. is_array_list l a * ↑(r⟷(l=[]))>"
by (sep_auto simp: arl_is_empty_def is_array_list_def)

lemma arl_last_rule[sep_heap_rules]: "
l≠[] ⟹
<is_array_list l a>
arl_last a
<λr. is_array_list l a * ↑(r=last l)>"
by (sep_auto simp: arl_last_def is_array_list_def last_take_nth_conv)

lemma arl_butlast_rule[sep_heap_rules]: "
l≠[] ⟹
<is_array_list l a>
arl_butlast a
<is_array_list (butlast l)>⇩t"
proof -
assume [simp]: "l≠[]"

have [simp]: "⋀x. min (x-Suc 0) ((x-Suc 0)*2) = x-Suc 0" by auto

show ?thesis
by (sep_auto
split: prod.splits
simp: arl_butlast_def is_array_list_def butlast_take minimum_capacity_def)
qed

lemma arl_get_rule[sep_heap_rules]: "
i<length l ⟹
<is_array_list l a>
arl_get a i
<λr. is_array_list l a * ↑(r=l!i)>"
by (sep_auto simp: arl_get_def is_array_list_def split: prod.split)

lemma arl_set_rule[sep_heap_rules]: "
i<length l ⟹
<is_array_list l a>
arl_set a i x
<is_array_list (l[i:=x])>"
by (sep_auto simp: arl_set_def is_array_list_def split: prod.split)

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

lemma arl_assn_comp: "is_pure A ⟹ hr_comp (arl_assn A) (⟨B⟩list_rel) = arl_assn (hr_comp A B)"
unfolding arl_assn_def
by (auto simp: hr_comp_the_pure hr_comp_assoc list_rel_compp)

lemma arl_assn_comp': "hr_comp (arl_assn id_assn) (⟨B⟩list_rel) = arl_assn (pure B)"

context
notes [fcomp_norm_unfold] = arl_assn_def[symmetric] arl_assn_comp'
notes [intro!] = hfrefI hn_refineI[THEN hn_refine_preI]
notes [simp] = pure_def hn_ctxt_def invalid_assn_def
begin

lemma arl_empty_hnr_aux: "(uncurry0 arl_empty,uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_array_list"
by sep_auto
sepref_decl_impl (no_register) arl_empty: arl_empty_hnr_aux .

lemma arl_empty_sz_hnr_aux: "(uncurry0 (arl_empty_sz N),uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_array_list"
by sep_auto
sepref_decl_impl (no_register) arl_empty_sz: arl_empty_sz_hnr_aux .

definition "op_arl_empty ≡ op_list_empty"
definition "op_arl_empty_sz (N::nat) ≡ op_list_empty"

lemma arl_copy_hnr_aux: "(arl_copy,RETURN o op_list_copy) ∈ is_array_list⇧k →⇩a is_array_list"
by sep_auto
sepref_decl_impl arl_copy: arl_copy_hnr_aux .

lemma arl_append_hnr_aux: "(uncurry arl_append,uncurry (RETURN oo op_list_append)) ∈ (is_array_list⇧d *⇩a id_assn⇧k) →⇩a is_array_list"
by sep_auto
sepref_decl_impl arl_append: arl_append_hnr_aux .

lemma arl_length_hnr_aux: "(arl_length,RETURN o op_list_length) ∈ is_array_list⇧k →⇩a nat_assn"
by sep_auto
sepref_decl_impl arl_length: arl_length_hnr_aux .

lemma arl_is_empty_hnr_aux: "(arl_is_empty,RETURN o op_list_is_empty) ∈ is_array_list⇧k →⇩a bool_assn"
by sep_auto
sepref_decl_impl arl_is_empty: arl_is_empty_hnr_aux .

lemma arl_last_hnr_aux: "(arl_last,RETURN o op_list_last) ∈ [pre_list_last]⇩a is_array_list⇧k → id_assn"
by sep_auto
sepref_decl_impl arl_last: arl_last_hnr_aux .

lemma arl_butlast_hnr_aux: "(arl_butlast,RETURN o op_list_butlast) ∈ [pre_list_butlast]⇩a is_array_list⇧d → is_array_list"
by sep_auto
sepref_decl_impl arl_butlast: arl_butlast_hnr_aux .

lemma arl_get_hnr_aux: "(uncurry arl_get,uncurry (RETURN oo op_list_get)) ∈ [λ(l,i). i<length l]⇩a (is_array_list⇧k *⇩a nat_assn⇧k) → id_assn"
by sep_auto
sepref_decl_impl arl_get: arl_get_hnr_aux .

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

sepref_definition arl_swap is "uncurry2 mop_list_swap" :: "((arl_assn id_assn)⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k →⇩a arl_assn id_assn)"
unfolding gen_mop_list_swap[abs_def]
by sepref
sepref_decl_impl (ismop) arl_swap: arl_swap.refine .
end

interpretation arl: list_custom_empty "arl_assn A" arl_empty op_arl_empty
apply unfold_locales
apply (rule arl_empty_hnr)
by (auto simp: op_arl_empty_def)

lemma [def_pat_rules]: "op_arl_empty_sz\$N ≡ UNPROTECT (op_arl_empty_sz N)" by simp
interpretation arl_sz: list_custom_empty "arl_assn A" "arl_empty_sz N" "PR_CONST (op_arl_empty_sz N)"
apply unfold_locales
apply (rule arl_empty_sz_hnr)
by (auto simp: op_arl_empty_sz_def)

end
```