theory Array_List_Array
imports Array_Array_List
begin
subsection ‹Array of Array Lists›
text ‹There is a major difference compared to @{typ ‹'a array_list array›}: @{typ ‹'a array_list›}
is not of sort default. This means that function like @{term arl_append} cannot be used here.›
type_synonym 'a arrayO_raa = ‹'a array array_list›
type_synonym 'a list_rll = ‹'a list list›
definition arlO_assn :: ‹('a ⇒ 'b::heap ⇒ assn) ⇒ 'a list ⇒ 'b array_list ⇒ assn› where
‹arlO_assn R' xs axs ≡ ∃⇩Ap. arl_assn id_assn p axs * heap_list_all R' xs p›
definition arlO_assn_except :: ‹('a ⇒ 'b::heap ⇒ assn) ⇒ nat list ⇒ 'a list ⇒ 'b array_list ⇒ _ ⇒ assn› where
‹arlO_assn_except R' is xs axs f ≡
∃⇩A p. arl_assn id_assn p axs * heap_list_all_nth R' (fold remove1 is [0..<length xs]) xs p *
↑ (length xs = length p) * f p›
lemma arlO_assn_except_array0: ‹arlO_assn_except R [] xs asx (λ_. emp) = arlO_assn R xs asx›
proof -
have ‹(h ⊨ arl_assn id_assn p asx * heap_list_all_nth R [0..<length xs] xs p ∧ length xs = length p) =
(h ⊨ arl_assn id_assn p asx * heap_list_all R xs p)› (is ‹?a = ?b›) for h p
proof (rule iffI)
assume ?a
then show ?b
by (auto simp: heap_list_all_heap_list_all_nth)
next
assume ?b
then have ‹length xs = length p›
by (auto simp: heap_list_add_same_length mod_star_conv)
then show ?a
using ‹?b›
by (auto simp: heap_list_all_heap_list_all_nth)
qed
then show ?thesis
unfolding arlO_assn_except_def arlO_assn_def by (auto simp: ex_assn_def)
qed
lemma arlO_assn_except_array0_index:
‹i < length xs ⟹ arlO_assn_except R [i] xs asx (λp. R (xs ! i) (p ! i)) = arlO_assn R xs asx›
unfolding arlO_assn_except_array0[symmetric] arlO_assn_except_def
using heap_list_all_nth_remove1[of i ‹[0..<length xs]› R xs] by (auto simp: star_aci(2,3))
lemma arrayO_raa_nth_rule[sep_heap_rules]:
assumes i: ‹i < length a›
shows ‹ <arlO_assn (array_assn R) a ai> arl_get ai i <λr. arlO_assn_except (array_assn R) [i] a ai
(λr'. array_assn R (a ! i) r * ↑(r = r' ! i))>›
proof -
obtain t n where ai: ‹ai = (t, n)› by (cases ai)
have i_le: ‹i < Array.length h t› if ‹(h, as) ⊨ arlO_assn (array_assn R) a ai› for h as
using ai that i unfolding arlO_assn_def array_assn_def is_array_def arl_assn_def is_array_list_def
by (auto simp: run.simps tap_def arlO_assn_def
mod_star_conv array_assn_def is_array_def
Abs_assn_inverse heap_list_add_same_length length_def snga_assn_def
dest: heap_list_add_same_length)
show ?thesis
unfolding hoare_triple_def Let_def
proof (clarify, intro allI impI conjI)
fix h as σ r
assume
a: ‹(h, as) ⊨ arlO_assn (array_assn R) a ai› and
r: ‹run (arl_get ai i) (Some h) σ r›
have [simp]: ‹length a = n›
using a ai
by (auto simp: arlO_assn_def mod_star_conv arl_assn_def is_array_list_def
dest: heap_list_add_same_length)
obtain p where
p: ‹(h, as) ⊨ arl_assn id_assn p (t, n) *
heap_list_all_nth (array_assn R) (remove1 i [0..<length p]) a p *
array_assn R (a ! i) (p ! i)›
using assms a ai
by (auto simp: hoare_triple_def Let_def execute_simps relH_def in_range.simps
arlO_assn_except_array0_index[of i, symmetric] arl_get_def
arlO_assn_except_array0_index arlO_assn_except_def
elim!: run_elims
intro!: norm_pre_ex_rule)
then have ‹(Array.get h t ! i) = p ! i›
using ai i i_le unfolding arlO_assn_except_array0_index
apply (auto simp: mod_star_conv array_assn_def is_array_def snga_assn_def
Abs_assn_inverse arl_assn_def)
unfolding is_array_list_def is_array_def hr_comp_def list_rel_def
apply (auto simp: mod_star_conv array_assn_def is_array_def snga_assn_def
Abs_assn_inverse arl_assn_def from_nat_def
intro!: nth_take[symmetric])
done
moreover have ‹length p = n›
using p ai by (auto simp: arl_assn_def is_array_list_def)
ultimately show ‹(the_state σ, new_addrs h as (the_state σ)) ⊨
arlO_assn_except (array_assn R) [i] a ai (λr'. array_assn R (a ! i) r * ↑ (r = r' ! i))›
using assms ai i_le r p
by (fastforce simp: hoare_triple_def Let_def execute_simps relH_def in_range.simps
arlO_assn_except_array0_index[of i, symmetric] arl_get_def
arlO_assn_except_array0_index arlO_assn_except_def
elim!: run_elims
intro!: norm_pre_ex_rule)
qed ((solves ‹use assms ai i_le in ‹auto simp: hoare_triple_def Let_def execute_simps relH_def
in_range.simps arlO_assn_except_array0_index[of i, symmetric] arl_get_def
elim!: run_elims
intro!: norm_pre_ex_rule››)+)[3]
qed
definition length_ra :: ‹'a::heap arrayO_raa ⇒ nat Heap› where
‹length_ra xs = arl_length xs›
lemma length_ra_rule[sep_heap_rules]:
‹<arlO_assn R x xi> length_ra xi <λr. arlO_assn R x xi * ↑(r = length x)>⇩t›
by (sep_auto simp: arlO_assn_def length_ra_def mod_star_conv arl_assn_def
dest: heap_list_add_same_length)
lemma length_ra_hnr[sepref_fr_rules]:
‹(length_ra, RETURN o op_list_length) ∈ (arlO_assn R)⇧k →⇩a nat_assn›
by sepref_to_hoare sep_auto
definition length_rll :: ‹'a list_rll ⇒ nat ⇒ nat› where
‹length_rll l i = length (l!i)›
lemma le_length_rll_nemptyD: ‹b < length_rll a ba ⟹ a ! ba ≠ []›
by (auto simp: length_rll_def)
definition length_raa :: ‹'a::heap arrayO_raa ⇒ nat ⇒ nat Heap› where
‹length_raa xs i = do {
x ← arl_get xs i;
Array.len x}›
lemma length_raa_rule[sep_heap_rules]:
‹b < length xs ⟹ <arlO_assn (array_assn R) xs a> length_raa a b
<λr. arlO_assn (array_assn R) xs a * ↑ (r = length_rll xs b)>⇩t›
unfolding length_raa_def
apply (cases a)
apply sep_auto
apply (sep_auto simp: arlO_assn_except_def arl_length_def array_assn_def
eq_commute[of ‹(_, _)›] is_array_def hr_comp_def length_rll_def
dest: list_all2_lengthD)
apply (sep_auto simp: arlO_assn_except_def arl_length_def arl_assn_def
eq_commute[of ‹(_, _)›] is_array_list_def hr_comp_def length_rll_def list_rel_def
dest: list_all2_lengthD)[]
unfolding arlO_assn_def[symmetric] arl_assn_def[symmetric]
apply (subst arlO_assn_except_array0_index[symmetric, of b])
apply simp
unfolding arlO_assn_except_def arl_assn_def hr_comp_def is_array_def
apply sep_auto
done
lemma length_raa_hnr[sepref_fr_rules]: ‹(uncurry length_raa, uncurry (RETURN ∘∘ length_rll)) ∈
[λ(xs, i). i < length xs]⇩a (arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k → nat_assn›
by sepref_to_hoare sep_auto
definition nth_raa :: ‹'a::heap arrayO_raa ⇒ nat ⇒ nat ⇒ 'a Heap› where
‹nth_raa xs i j = do {
x ← arl_get xs i;
y ← Array.nth x j;
return y}›
lemma nth_raa_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k *⇩a nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have H: ‹list_all2 (λx x'. (x, x') ∈ the_pure (λa c. ↑ ((c, a) ∈ R'))) bc (a ! ba) ⟹
b < length (a ! ba) ⟹
(bc ! b, a ! ba ! b) ∈ R'› for bc a ba b
by (auto simp add: ent_refl_true list_all2_conv_all_nth is_pure_alt_def pure_app_eq[symmetric])
show ?thesis
supply nth_rule[sep_heap_rules]
apply sepref_to_hoare
apply (subst (2) arlO_assn_except_array0_index[symmetric])
apply (solves ‹auto›)[]
apply (sep_auto simp: nth_raa_def nth_rll_def length_rll_def)
apply (sep_auto simp: arlO_assn_except_def arlO_assn_def arl_assn_def hr_comp_def list_rel_def
list_all2_lengthD array_assn_def is_array_def hr_comp_def[abs_def]
star_aci(3) R R' pure_def H)
done
qed
definition update_raa :: "('a::{heap,default}) arrayO_raa ⇒ nat ⇒ nat ⇒ 'a ⇒ 'a arrayO_raa Heap" where
‹update_raa a i j y = do {
x ← arl_get a i;
a' ← Array.upd j y x;
arl_set a i a'
}›
definition update_rll :: "'a list_rll ⇒ nat ⇒ nat ⇒ 'a ⇒ 'a list list" where
‹update_rll xs i j y = xs[i:= (xs ! i)[j := y]]›
declare nth_rule[sep_heap_rules del]
declare arrayO_raa_nth_rule[sep_heap_rules]
text ‹TODO: is it possible to be more precise and not drop the \<^term>‹↑ ((aa, bc) = r' ! bb)››
lemma arlO_assn_except_arl_set[sep_heap_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap} ⇒ assn›
assumes p: ‹is_pure R› and ‹bb < length a› and
‹ba < length_rll a bb›
shows ‹
<arlO_assn_except (array_assn R) [bb] a ai (λr'. array_assn R (a ! bb) aa *
↑ (aa = r' ! bb)) * R b bi>
Array.upd ba bi aa
<λaa. arlO_assn_except (array_assn R) [bb] a ai
(λr'. array_assn R ((a ! bb)[ba := b]) aa) * R b bi * true>›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
using assms
by (cases ai)
(sep_auto simp: arlO_assn_except_def arl_assn_def hr_comp_def list_rel_imp_same_length
list_rel_update length_rll_def array_assn_def is_array_def)
qed
lemma update_raa_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_rll a bb›
shows ‹<R b bi * arlO_assn (array_assn R) a ai> update_raa ai bb ba bi
<λr. R b bi * (∃⇩Ax. arlO_assn (array_assn R) x r * ↑ (x = update_rll a bb ba b))>⇩t›
using assms
apply (sep_auto simp add: update_raa_def update_rll_def p)
apply (sep_auto simp add: update_raa_def arlO_assn_except_def array_assn_def is_array_def hr_comp_def
arl_assn_def)
apply (subst_tac i=bb in arlO_assn_except_array0_index[symmetric])
apply (solves ‹simp›)
apply (subst arlO_assn_except_def)
apply (auto simp add: update_raa_def arlO_assn_except_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p[bb := xa]› in ent_ex_postI)
apply (rule_tac x=‹bc› in ent_ex_postI)
apply (subst_tac (2)xs'=a and ys'=p in heap_list_all_nth_cong)
apply (solves ‹auto›)
apply (solves ‹auto›)
by (sep_auto simp: arl_assn_def)
lemma update_raa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_raa, uncurry3 (RETURN oooo update_rll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_rll l i]⇩a (arlO_assn (array_assn R))⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a R⇧k → (arlO_assn (array_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
definition swap_aa :: "('a::{heap,default}) arrayO_raa ⇒ nat ⇒ nat ⇒ nat ⇒ 'a arrayO_raa Heap" where
‹swap_aa xs k i j = do {
xi ← nth_raa xs k i;
xj ← nth_raa xs k j;
xs ← update_raa xs k i xj;
xs ← update_raa xs k j xi;
return xs
}›
definition swap_ll where
‹swap_ll xs k i j = list_update xs k (swap (xs!k) i j)›
lemma nth_raa_heap[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_rll aa b›
shows ‹
<arlO_assn (array_assn R) aa a>
nth_raa a b ba
<λr. ∃⇩Ax. arlO_assn (array_assn R) aa a *
(R x r *
↑ (x = nth_rll aa b ba)) *
true>›
proof -
have ‹<arlO_assn (array_assn R) aa a *
nat_assn b b *
nat_assn ba ba>
nth_raa a b ba
<λr. ∃⇩Ax. arlO_assn (array_assn R) aa a *
nat_assn b b *
nat_assn ba ba *
R x r *
true *
↑ (x = nth_rll aa b ba)>›
using p assms nth_raa_hnr[of R] unfolding hfref_def hn_refine_def
by (cases a) auto
then show ?thesis
unfolding hoare_triple_def
by (auto simp: Let_def pure_def)
qed
lemma update_raa_rule_pure:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_rll aa b› and
b: ‹(bb, be) ∈ the_pure R›
shows ‹
<arlO_assn (array_assn R) aa a>
update_raa a b ba bb
<λr. ∃⇩Ax. invalid_assn (arlO_assn (array_assn R)) aa a * arlO_assn (array_assn R) x r *
true *
↑ (x = update_rll aa b ba be)>›
proof -
obtain R' where R': ‹R' = the_pure R› and RR': ‹R = pure R'›
using p by fastforce
have bb: ‹pure R' be bb = ↑((bb, be) ∈ R')›
by (auto simp: pure_def)
have ‹ <arlO_assn (array_assn R) aa a * nat_assn b b * nat_assn ba ba * R be bb>
update_raa a b ba bb
<λr. ∃⇩Ax. invalid_assn (arlO_assn (array_assn R)) aa a * nat_assn b b * nat_assn ba ba *
R be bb *
arlO_assn (array_assn R) x r *
true *
↑ (x = update_rll aa b ba be)>›
using p assms update_raa_hnr[of R] unfolding hfref_def hn_refine_def
by (cases a) auto
then show ?thesis
using b unfolding R'[symmetric] unfolding hoare_triple_def RR' bb
by (auto simp: Let_def pure_def)
qed
lemma length_update_rll[simp]: ‹length (update_rll a bb b c) = length a›
unfolding update_rll_def by auto
lemma length_rll_update_rll:
‹bb < length a ⟹ length_rll (update_rll a bb b c) bb = length_rll a bb›
unfolding length_rll_def update_rll_def by auto
lemma swap_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 swap_aa, uncurry3 (RETURN oooo swap_ll)) ∈
[λ(((xs, k), i), j). k < length xs ∧ i < length_rll xs k ∧ j < length_rll xs k]⇩a
(arlO_assn (array_assn R))⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a nat_assn⇧k → (arlO_assn (array_assn R))›
proof -
note update_raa_rule_pure[sep_heap_rules]
obtain R' where R': ‹R' = the_pure R› and RR': ‹R = pure R'›
using assms by fastforce
have [simp]: ‹the_pure (λa b. ↑ ((b, a) ∈ R')) = R'›
unfolding pure_def[symmetric] by auto
show ?thesis
using assms unfolding R'[symmetric] unfolding RR'
apply sepref_to_hoare
apply (sep_auto simp: swap_aa_def swap_ll_def arlO_assn_except_def
length_rll_update_rll)
by (sep_auto simp: update_rll_def swap_def nth_rll_def list_update_swap)
qed
definition update_ra :: ‹'a arrayO_raa ⇒ nat ⇒ 'a array ⇒ 'a arrayO_raa Heap› where
‹update_ra xs n x = arl_set xs n x›
lemma update_ra_list_update_rules[sep_heap_rules]:
assumes ‹n < length l›
shows ‹<R y x * arlO_assn R l xs> update_ra xs n x <arlO_assn R (l[n:=y])>⇩t›
proof -
have H: ‹heap_list_all R l p = heap_list_all R l p * ↑ (n < length p)› for p
using assms by (simp add: ent_iffI heap_list_add_same_length)
have [simp]: ‹heap_list_all_nth R (remove1 n [0..<length p]) (l[n := y]) (p[n := x]) =
heap_list_all_nth R (remove1 n [0..<length p]) (l) (p)› for p
by (rule heap_list_all_nth_cong) auto
show ?thesis
using assms
apply (cases xs)
supply arl_set_rule[sep_heap_rules del]
apply (sep_auto simp: arlO_assn_def update_ra_def Let_def arl_assn_def
dest!: heap_list_add_same_length
elim!: run_elims)
apply (subst H)
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst heap_list_all_nth_remove1[where i = n])
apply (solves ‹simp›)
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst (2) heap_list_all_nth_remove1[where i = n])
apply (solves ‹simp›)
supply arl_set_rule[sep_heap_rules]
apply (sep_auto (plain))
apply (subgoal_tac ‹length (l[n := y]) = length (p[n := x])›)
apply assumption
apply auto[]
apply sep_auto
done
qed
lemma ex_assn_up_eq: ‹(∃⇩Ax. P x * ↑(x = a) * Q) = (P a * Q)›
by (smt ex_one_point_gen mod_pure_star_dist mod_starE mult.right_neutral pure_true)
lemma update_ra_list_update[sepref_fr_rules]:
‹(uncurry2 update_ra, uncurry2 (RETURN ooo list_update)) ∈
[λ((xs, n), _). n < length xs]⇩a (arlO_assn R)⇧d *⇩a nat_assn⇧k *⇩a R⇧d → (arlO_assn R)›
proof -
have [simp]: ‹(∃⇩Ax. arlO_assn R x r * true * ↑ (x = list_update a ba b)) =
arlO_assn R (a[ba := b]) r * true›
for a ba b r
apply (subst assn_aci(10))
apply (subst ex_assn_up_eq)
..
show ?thesis
by sepref_to_hoare sep_auto
qed
term arl_append
definition arrayO_raa_append where
"arrayO_raa_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;
default ← Array.new 0 default;
a ← array_grow a newcap default;
a ← Array.upd n x a;
return (a,n+1)
}
}"
lemma heap_list_all_append_Nil:
‹y ≠ [] ⟹ heap_list_all R (va @ y) [] = false›
by (cases va; cases y) auto
lemma heap_list_all_Nil_append:
‹y ≠ [] ⟹ heap_list_all R [] (va @ y) = false›
by (cases va; cases y) auto
lemma heap_list_all_append: ‹heap_list_all R (l @ [y]) (l' @ [x])
= heap_list_all R (l) (l') * R y x›
by (induction R l l' rule: heap_list_all.induct)
(auto simp: ac_simps heap_list_all_Nil_append heap_list_all_append_Nil)
term arrayO_raa
lemma arrayO_raa_append_rule[sep_heap_rules]:
‹<arlO_assn R l a * R y x> arrayO_raa_append a x <λa. arlO_assn R (l@[y]) a >⇩t›
proof -
have 1: ‹arl_assn id_assn p a * heap_list_all R l p =
arl_assn id_assn p a * heap_list_all R l p * ↑ (length l = length p)› for p
by (smt ent_iffI ent_pure_post_iff entailsI heap_list_add_same_length mult.right_neutral
pure_false pure_true star_false_right)
show ?thesis
unfolding arrayO_raa_append_def arrayO_raa_append_def arlO_assn_def
length_ra_def arl_length_def hr_comp_def
apply (subst 1)
unfolding arl_assn_def is_array_list_def hr_comp_def
apply (cases a)
apply sep_auto
apply (rule_tac psi=‹Suc (length l) ≤ length (l'[length l := x])› in asm_rl)
apply simp
apply simp
apply (sep_auto simp: take_update_last heap_list_all_append)
apply (sep_auto (plain))
apply sep_auto
apply (sep_auto (plain))
apply sep_auto
apply (sep_auto (plain))
apply sep_auto
apply (rule_tac psi = ‹Suc (length p) ≤ length ((p @ replicate (length p) xa)[length p := x])›
in asm_rl)
apply sep_auto
apply sep_auto
apply (sep_auto simp: heap_list_all_append)
done
qed
lemma arrayO_raa_append_op_list_append[sepref_fr_rules]:
‹(uncurry arrayO_raa_append, uncurry (RETURN oo op_list_append)) ∈
(arlO_assn R)⇧d *⇩a R⇧d →⇩a arlO_assn R›
apply sepref_to_hoare
apply (subst mult.commute)
apply (subst mult.assoc)
by (sep_auto simp: ex_assn_up_eq)
definition array_of_arl :: ‹'a list ⇒ 'a list› where
‹array_of_arl xs = xs›
definition array_of_arl_raa :: "'a::heap array_list ⇒ 'a array Heap" where
‹array_of_arl_raa = (λ(a, n). array_shrink a n)›
lemma array_of_arl[sepref_fr_rules]:
‹(array_of_arl_raa, RETURN o array_of_arl) ∈ (arl_assn R)⇧d →⇩a (array_assn R)›
by sepref_to_hoare
(sep_auto simp: array_of_arl_raa_def arl_assn_def is_array_list_def hr_comp_def
array_assn_def is_array_def array_of_arl_def)
definition "arrayO_raa_empty ≡ do {
a ← Array.new initial_capacity default;
return (a,0)
}"
lemma arrayO_raa_empty_rule[sep_heap_rules]: "< emp > arrayO_raa_empty <λr. arlO_assn R [] r>"
by (sep_auto simp: arrayO_raa_empty_def is_array_list_def initial_capacity_def
arlO_assn_def arl_assn_def)
definition arrayO_raa_empty_sz where
"arrayO_raa_empty_sz init_cap ≡ do {
default ← Array.new 0 default;
a ← Array.new (max init_cap minimum_capacity) default;
return (a,0)
}"
lemma arl_empty_sz_array_rule[sep_heap_rules]: "< emp > arrayO_raa_empty_sz N <λr. arlO_assn R [] r>⇩t"
proof -
have [simp]: ‹(xa ↦⇩a replicate (max N 16) x) * x ↦⇩a [] = (xa ↦⇩a (x # replicate (max N 16 - 1) x)) * x ↦⇩a []›
for xa x
by (cases N) (sep_auto simp: arrayO_raa_empty_sz_def is_array_list_def minimum_capacity_def max_def)+
show ?thesis
by (sep_auto simp: arrayO_raa_empty_sz_def is_array_list_def minimum_capacity_def
arlO_assn_def arl_assn_def)
qed
definition nth_rl :: ‹'a::heap arrayO_raa ⇒ nat ⇒ 'a array Heap› where
‹nth_rl xs n = do {x ← arl_get xs n; array_copy x}›
lemma nth_rl_op_list_get:
‹(uncurry nth_rl, uncurry (RETURN oo op_list_get)) ∈
[λ(xs, n). n < length xs]⇩a (arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k → array_assn R›
apply sepref_to_hoare
unfolding arlO_assn_def heap_list_all_heap_list_all_nth_eq
apply (subst_tac i=b in heap_list_all_nth_remove1)
apply (solves ‹simp›)
apply (subst_tac (2) i=b in heap_list_all_nth_remove1)
apply (solves ‹simp›)
by (sep_auto simp: nth_rl_def arlO_assn_def heap_list_all_heap_list_all_nth_eq array_assn_def
hr_comp_def[abs_def] is_array_def arl_assn_def)
definition arl_of_array :: "'a list list ⇒ 'a list list" where
‹arl_of_array xs = xs›
definition arl_of_array_raa :: "'a::heap array ⇒ ('a array_list) Heap" where
‹arl_of_array_raa xs = do {
n ← Array.len xs;
return (xs, n)
}›
lemma arl_of_array_raa: ‹(arl_of_array_raa, RETURN o arl_of_array) ∈
[λxs. xs ≠ []]⇩a (array_assn R)⇧d → (arl_assn R)›
by sepref_to_hoare (sep_auto simp: arl_of_array_raa_def arl_assn_def is_array_list_def hr_comp_def
array_assn_def is_array_def arl_of_array_def)
end