theory Array_Array_List
imports WB_More_IICF_SML
begin
subsection ‹Array of Array Lists›
text ‹
We define here array of array lists. We need arrays owning there elements. Therefore most of the
rules introduced by ‹sep_auto› cannot lead to proofs.
›
fun heap_list_all :: "('a ⇒ 'b ⇒ assn) ⇒ 'a list ⇒ 'b list ⇒ assn" where
‹heap_list_all R [] [] = emp›
| ‹heap_list_all R (x # xs) (y # ys) = R x y * heap_list_all R xs ys›
| ‹heap_list_all R _ _ = false›
text ‹It is often useful to speak about arrays except at one index (e.g., because it is updated).›
definition heap_list_all_nth:: "('a ⇒ 'b ⇒ assn) ⇒ nat list ⇒ 'a list ⇒ 'b list ⇒ assn" where
‹heap_list_all_nth R is xs ys = foldr ((*)) (map (λi. R (xs ! i) (ys ! i)) is) emp›
lemma heap_list_all_nth_emty[simp]: ‹heap_list_all_nth R [] xs ys = emp›
unfolding heap_list_all_nth_def by auto
lemma heap_list_all_nth_Cons:
‹heap_list_all_nth R (a # is') xs ys = R (xs ! a) (ys ! a) * heap_list_all_nth R is' xs ys›
unfolding heap_list_all_nth_def by auto
lemma heap_list_all_heap_list_all_nth:
‹length xs = length ys ⟹ heap_list_all R xs ys = heap_list_all_nth R [0..< length xs] xs ys›
proof (induction R xs ys rule: heap_list_all.induct)
case (2 R x xs y ys) note IH = this
then have IH: ‹heap_list_all R xs ys = heap_list_all_nth R [0..<length xs] xs ys›
by auto
have upt: ‹[0..<length (x # xs)] = 0 # [1..<Suc (length xs)]›
by (simp add: upt_rec)
have upt_map_Suc: ‹[1..<Suc (length xs)] = map Suc [0..<length xs]›
by (induction xs) auto
have map: ‹(map (λi. R ((x # xs) ! i) ((y # ys) ! i)) [1..<Suc (length xs)]) =
(map (λi. R (xs ! i) (ys ! i)) [0..< (length xs)])›
unfolding upt_map_Suc map_map by auto
have 1: ‹heap_list_all_nth R [0..<length (x # xs)] (x # xs) (y # ys) =
R x y * heap_list_all_nth R [0..<length xs] xs ys›
unfolding heap_list_all_nth_def upt
by (simp only: list.map foldr.simps map) auto
show ?case
using IH unfolding 1 by auto
qed auto
lemma heap_list_all_nth_single: ‹heap_list_all_nth R [a] xs ys = R (xs ! a) (ys ! a)›
by (auto simp: heap_list_all_nth_def)
lemma heap_list_all_nth_mset_eq:
assumes ‹mset is = mset is'›
shows ‹heap_list_all_nth R is xs ys = heap_list_all_nth R is' xs ys›
using assms
proof (induction "is'" arbitrary: "is")
case Nil
then show ?case by auto
next
case (Cons a is') note IH = this(1) and eq_is = this(2)
from eq_is have ‹a ∈ set is›
by (fastforce dest: mset_eq_setD)
then obtain ixs iys where
"is": ‹is = ixs @ a # iys›
using eq_is by (meson split_list)
then have H: ‹heap_list_all_nth R (ixs @ iys) xs ys = heap_list_all_nth R is' xs ys›
using IH[of ‹ixs @ iys›] eq_is by auto
have H': ‹heap_list_all_nth R (ixs @ a # iys) xs ys = heap_list_all_nth R (a # ixs @ iys) xs ys›
for xs ys
by (induction ixs)(auto simp: heap_list_all_nth_Cons star_aci(3))
show ?case
using H[symmetric] by (auto simp: heap_list_all_nth_Cons "is" H')
qed
lemma heap_list_add_same_length:
‹h ⊨ heap_list_all R' xs p ⟹ length p = length xs›
by (induction R' xs p arbitrary: h rule: heap_list_all.induct) (auto elim!: mod_starE)
lemma heap_list_all_nth_Suc:
assumes a: ‹a > 1›
shows ‹heap_list_all_nth R [Suc 0..<a] (x # xs) (y # ys) =
heap_list_all_nth R [0..<a-1] xs ys›
proof -
have upt: ‹[0..< a] = 0 # [1..< a]›
using a by (simp add: upt_rec)
have upt_map_Suc: ‹[Suc 0..<a] = map Suc [0..< a-1]›
using a by (auto simp: map_Suc_upt)
have map: ‹(map (λi. R ((x # xs) ! i) ((y # ys) ! i)) [Suc 0..<a]) =
(map (λi. R (xs ! i) (ys ! i)) [0..<a-1])›
unfolding upt_map_Suc map_map by auto
show ?thesis
unfolding heap_list_all_nth_def unfolding map ..
qed
lemma heap_list_all_nth_append:
‹heap_list_all_nth R (is @ is') xs ys = heap_list_all_nth R is xs ys * heap_list_all_nth R is' xs ys›
by (induction "is") (auto simp: heap_list_all_nth_Cons star_aci)
lemma heap_list_all_heap_list_all_nth_eq:
‹heap_list_all R xs ys = heap_list_all_nth R [0..< length xs] xs ys * ↑(length xs = length ys)›
by (induction R xs ys rule: heap_list_all.induct)
(auto simp del: upt_Suc upt_Suc_append
simp: upt_rec[of 0] heap_list_all_nth_single star_aci(3)
heap_list_all_nth_Cons heap_list_all_nth_Suc)
lemma heap_list_all_nth_remove1: ‹i ∈ set is ⟹
heap_list_all_nth R is xs ys = R (xs ! i) (ys ! i) * heap_list_all_nth R (remove1 i is) xs ys›
using heap_list_all_nth_mset_eq[of ‹is› ‹i # remove1 i is›]
by (auto simp: heap_list_all_nth_Cons)
definition arrayO_assn :: ‹('a ⇒ 'b::heap ⇒ assn) ⇒ 'a list ⇒ 'b array ⇒ assn› where
‹arrayO_assn R' xs axs ≡ ∃⇩A p. array_assn id_assn p axs * heap_list_all R' xs p›
definition arrayO_except_assn:: ‹('a ⇒ 'b::heap ⇒ assn) ⇒ nat list ⇒ 'a list ⇒ 'b array ⇒ _ ⇒ assn› where
‹arrayO_except_assn R' is xs axs f ≡
∃⇩A p. array_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 arrayO_except_assn_array0: ‹arrayO_except_assn R [] xs asx (λ_. emp) = arrayO_assn R xs asx›
proof -
have ‹(h ⊨ array_assn id_assn p asx * heap_list_all_nth R [0..<length xs] xs p ∧ length xs = length p) =
(h ⊨ array_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 arrayO_except_assn_def arrayO_assn_def by (auto simp: ex_assn_def)
qed
lemma arrayO_except_assn_array0_index:
‹i < length xs ⟹ arrayO_except_assn R [i] xs asx (λp. R (xs ! i) (p ! i)) = arrayO_assn R xs asx›
unfolding arrayO_except_assn_array0[symmetric] arrayO_except_assn_def
using heap_list_all_nth_remove1[of i ‹[0..<length xs]› R xs] by (auto simp: star_aci(2,3))
lemma arrayO_nth_rule[sep_heap_rules]:
assumes i: ‹i < length a›
shows ‹ <arrayO_assn (arl_assn R) a ai> Array.nth ai i <λr. arrayO_except_assn (arl_assn R) [i] a ai
(λr'. arl_assn R (a ! i) r * ↑(r = r' ! i))>›
proof -
have i_le: ‹i < Array.length h ai› if ‹(h, as) ⊨ arrayO_assn (arl_assn R) a ai› for h as
using that i unfolding arrayO_assn_def array_assn_def is_array_def
by (auto simp: run.simps tap_def arrayO_assn_def
mod_star_conv array_assn_def is_array_def
Abs_assn_inverse heap_list_add_same_length length_def snga_assn_def)
have A: ‹Array.get h ai ! i = p ! i› if ‹(h, as) ⊨
array_assn id_assn p ai *
heap_list_all_nth (arl_assn R) (remove1 i [0..<length p]) a p *
arl_assn R (a ! i) (p ! i)›
for as p h
using that
by (auto simp: mod_star_conv array_assn_def is_array_def Array.get_def snga_assn_def
Abs_assn_inverse)
show ?thesis
unfolding hoare_triple_def Let_def
apply (clarify, intro allI impI conjI)
using assms A
apply (auto simp: hoare_triple_def Let_def i_le execute_simps relH_def in_range.simps
arrayO_except_assn_array0_index[of i, symmetric]
elim!: run_elims
intro!: norm_pre_ex_rule)
apply (auto simp: arrayO_except_assn_def)
done
qed
definition length_a :: ‹'a::heap array ⇒ nat Heap› where
‹length_a xs = Array.len xs›
lemma length_a_rule[sep_heap_rules]:
‹<arrayO_assn R x xi> length_a xi <λr. arrayO_assn R x xi * ↑(r = length x)>⇩t›
by (sep_auto simp: arrayO_assn_def length_a_def array_assn_def is_array_def mod_star_conv
dest: heap_list_add_same_length)
lemma length_a_hnr[sepref_fr_rules]:
‹(length_a, RETURN o op_list_length) ∈ (arrayO_assn R)⇧k →⇩a nat_assn›
by sepref_to_hoare sep_auto
lemma le_length_ll_nemptyD: ‹b < length_ll a ba ⟹ a ! ba ≠ []›
by (auto simp: length_ll_def)
definition length_aa :: ‹('a::heap array_list) array ⇒ nat ⇒ nat Heap› where
‹length_aa xs i = do {
x ← Array.nth xs i;
arl_length x}›
lemma length_aa_rule[sep_heap_rules]:
‹b < length xs ⟹ <arrayO_assn (arl_assn R) xs a> length_aa a b
<λr. arrayO_assn (arl_assn R) xs a * ↑ (r = length_ll xs b)>⇩t›
unfolding length_aa_def
apply sep_auto
apply (sep_auto simp: arrayO_except_assn_def arl_length_def arl_assn_def
eq_commute[of ‹(_, _)›] hr_comp_def length_ll_def)
apply (sep_auto simp: arrayO_except_assn_def arl_length_def arl_assn_def
eq_commute[of ‹(_, _)›] is_array_list_def hr_comp_def length_ll_def list_rel_def
dest: list_all2_lengthD)[]
unfolding arrayO_assn_def[symmetric] arl_assn_def[symmetric]
apply (subst arrayO_except_assn_array0_index[symmetric, of b])
apply simp
unfolding arrayO_except_assn_def arl_assn_def hr_comp_def
apply sep_auto
done
lemma length_aa_hnr[sepref_fr_rules]: ‹(uncurry length_aa, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl_assn R))⇧k *⇩a nat_assn⇧k → nat_assn›
by sepref_to_hoare sep_auto
definition nth_aa where
‹nth_aa xs i j = do {
x ← Array.nth xs i;
y ← arl_get x j;
return y}›
lemma models_heap_list_all_models_nth:
‹(h, as) ⊨ heap_list_all R a b ⟹ i < length a ⟹ ∃as'. (h, as') ⊨ R (a!i) (b!i)›
by (induction R a b arbitrary: as i rule: heap_list_all.induct)
(auto simp: mod_star_conv nth_Cons elim!: less_SucE split: nat.splits)
definition nth_ll :: "'a list list ⇒ nat ⇒ nat ⇒ 'a" where
‹nth_ll l i j = l ! i ! j›
lemma nth_aa_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa, uncurry2 (RETURN ∘∘∘ nth_ll)) ∈
[λ((l,i),j). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl_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
apply sepref_to_hoare
apply (subst (2) arrayO_except_assn_array0_index[symmetric])
apply (solves ‹auto›)[]
apply (sep_auto simp: nth_aa_def nth_ll_def length_ll_def)
apply (sep_auto simp: arrayO_except_assn_def arrayO_assn_def arl_assn_def hr_comp_def list_rel_def
list_all2_lengthD
star_aci(3) R R' pure_def H)
done
qed
definition append_el_aa :: "('a::{default,heap} array_list) array ⇒
nat ⇒ 'a ⇒ ('a array_list) array Heap"where
"append_el_aa ≡ λa i x. do {
j ← Array.nth a i;
a' ← arl_append j x;
Array.upd i a' a
}"
lemma sep_auto_is_stupid:
fixes R :: ‹'a ⇒ 'b::{heap,default} ⇒ assn›
assumes p: ‹is_pure R›
shows
‹<∃⇩Ap. R1 p * R2 p * arl_assn R l' aa * R x x' * R4 p>
arl_append aa x' <λr. (∃⇩Ap. arl_assn R (l' @ [x]) r * R1 p * R2 p * R x x' * R4 p * true) >›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have bbi: ‹(x', x) ∈ the_pure R› if
‹(aa, bb) ⊨ is_array_list (ba @ [x']) (a, baa) * R1 p * R2 p * pure R' x x' * R4 p * true›
for aa bb a ba baa p
using that by (auto simp: mod_star_conv R R')
show ?thesis
unfolding arl_assn_def hr_comp_def
by (sep_auto simp: list_rel_def R R' intro!: list_all2_appendI dest!: bbi)
qed
declare arrayO_nth_rule[sep_heap_rules]
lemma heap_list_all_nth_cong:
assumes
‹∀i ∈ set is. xs ! i = xs' ! i› and
‹∀i ∈ set is. ys ! i = ys' ! i›
shows ‹heap_list_all_nth R is xs ys = heap_list_all_nth R is xs' ys'›
using assms by (induction ‹is›) (auto simp: heap_list_all_nth_Cons)
lemma append_aa_hnr[sepref_fr_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap, default} ⇒ assn›
assumes p: ‹is_pure R›
shows
‹(uncurry2 append_el_aa, uncurry2 (RETURN ∘∘∘ append_ll)) ∈
[λ((l,i),x). i < length l]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl_assn R))›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹(∃⇩Ax. arrayO_assn (arl_assn R) a ai * R x r * true * ↑ (x = a ! ba ! b)) =
(arrayO_assn (arl_assn R) a ai * R (a ! ba ! b) r * true)› for a ai ba b r
by (auto simp: ex_assn_def)
show ?thesis
apply sepref_to_hoare
apply (sep_auto simp: append_el_aa_def)
apply (simp add: arrayO_except_assn_def)
apply (rule sep_auto_is_stupid[OF p])
apply (sep_auto simp: array_assn_def is_array_def append_ll_def)
apply (simp add: arrayO_except_assn_array0[symmetric] arrayO_except_assn_def)
apply (subst_tac (2) i = ba in heap_list_all_nth_remove1)
apply (solves ‹simp›)
apply (simp add: array_assn_def is_array_def)
apply (rule_tac x=‹p[ba := (ab, bc)]› in ent_ex_postI)
apply (subst_tac (2)xs'=a and ys'=p in heap_list_all_nth_cong)
apply (solves ‹auto›)[2]
apply (auto simp: star_aci)
done
qed
definition update_aa :: "('a::{heap} array_list) array ⇒ nat ⇒ nat ⇒ 'a ⇒ ('a array_list) array Heap" where
‹update_aa a i j y = do {
x ← Array.nth a i;
a' ← arl_set x j y;
Array.upd i a' a
}›
definition update_ll :: "'a list list ⇒ nat ⇒ nat ⇒ 'a ⇒ 'a list list" where
‹update_ll xs i j y = xs[i:= (xs ! i)[j := y]]›
declare nth_rule[sep_heap_rules del]
declare arrayO_nth_rule[sep_heap_rules]
text ‹TODO: is it possible to be more precise and not drop the \<^term>‹↑ ((aa, bc) = r' ! bb)››
lemma arrayO_except_assn_arl_set[sep_heap_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap}⇒ assn›
assumes p: ‹is_pure R› and ‹bb < length a› and
‹ba < length_ll a bb›
shows ‹
<arrayO_except_assn (arl_assn R) [bb] a ai (λr'. arl_assn R (a ! bb) (aa, bc) *
↑ ((aa, bc) = r' ! bb)) * R b bi>
arl_set (aa, bc) ba bi
<λ(aa, bc). arrayO_except_assn (arl_assn R) [bb] a ai
(λr'. arl_assn R ((a ! bb)[ba := b]) (aa, bc)) * 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
apply (sep_auto simp: arrayO_except_assn_def arl_assn_def hr_comp_def list_rel_imp_same_length
list_rel_update length_ll_def)
done
qed
lemma update_aa_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_ll a bb›
shows ‹<R b bi * arrayO_assn (arl_assn R) a ai> update_aa ai bb ba bi
<λr. R b bi * (∃⇩Ax. arrayO_assn (arl_assn R) x r * ↑ (x = update_ll a bb ba b))>⇩t›
using assms
apply (sep_auto simp add: update_aa_def update_ll_def p)
apply (sep_auto simp add: update_aa_def arrayO_except_assn_def array_assn_def is_array_def hr_comp_def)
apply (subst_tac i=bb in arrayO_except_assn_array0_index[symmetric])
apply (solves ‹simp›)
apply (subst arrayO_except_assn_def)
apply (auto simp add: update_aa_def arrayO_except_assn_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p[bb := (aa, 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›)
apply (auto simp: star_aci)
done
lemma update_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_aa, uncurry3 (RETURN oooo update_ll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
definition set_butlast_ll where
‹set_butlast_ll xs i = xs[i := butlast (xs ! i)]›
definition set_butlast_aa :: "('a::{heap} array_list) array ⇒ nat ⇒ ('a array_list) array Heap" where
‹set_butlast_aa a i = do {
x ← Array.nth a i;
a' ← arl_butlast x;
Array.upd i a' a
}›
lemma list_rel_butlast:
assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel›
shows ‹(butlast xs, butlast ys) ∈ ⟨R⟩list_rel›
proof -
have ‹length xs = length ys›
using assms list_rel_imp_same_length by blast
then show ?thesis
using rel
by (induction xs ys rule: list_induct2) (auto split: nat.splits)
qed
lemma arrayO_except_assn_arl_butlast:
assumes ‹b < length a› and
‹a ! b ≠ []›
shows
‹<arrayO_except_assn (arl_assn R) [b] a ai (λr'. arl_assn R (a ! b) (aa, ba) *
↑ ((aa, ba) = r' ! b))>
arl_butlast (aa, ba)
<λ(aa, ba). arrayO_except_assn (arl_assn R) [b] a ai (λr'. arl_assn R (butlast (a ! b)) (aa, ba)* true)>›
proof -
show ?thesis
using assms
apply (subst (1) arrayO_except_assn_def)
apply (sep_auto simp: arl_assn_def hr_comp_def list_rel_imp_same_length
list_rel_update
intro: list_rel_butlast)
apply (subst (1) arrayO_except_assn_def)
apply (rule_tac x=‹p› in ent_ex_postI)
apply (sep_auto intro: list_rel_butlast)
done
qed
lemma set_butlast_aa_rule[sep_heap_rules]:
assumes ‹is_pure R› and
‹b < length a› and
‹a ! b ≠ []›
shows ‹<arrayO_assn (arl_assn R) a ai> set_butlast_aa ai b
<λr. (∃⇩Ax. arrayO_assn (arl_assn R) x r * ↑ (x = set_butlast_ll a b))>⇩t›
proof -
note arrayO_except_assn_arl_butlast[sep_heap_rules]
note arl_butlast_rule[sep_heap_rules del]
have ‹⋀b bi.
b < length a ⟹
a ! b ≠ [] ⟹
a ::⇩i TYPE('a list list) ⟹
b ::⇩i TYPE(nat) ⟹
nofail (RETURN (set_butlast_ll a b)) ⟹
<↑ ((bi, b) ∈ nat_rel) *
arrayO_assn (arl_assn R) a
ai> set_butlast_aa ai
bi <λr. ↑ ((bi, b) ∈ nat_rel) *
true *
(∃⇩Ax.
arrayO_assn (arl_assn R) x r *
↑ (RETURN x ≤ RETURN (set_butlast_ll a b)))>⇩t›
apply (sep_auto simp add: set_butlast_aa_def set_butlast_ll_def assms)
apply (sep_auto simp add: set_butlast_aa_def arrayO_except_assn_def array_assn_def is_array_def
hr_comp_def)
apply (subst_tac i=b in arrayO_except_assn_array0_index[symmetric])
apply (solves ‹simp›)
apply (subst arrayO_except_assn_def)
apply (auto simp add: set_butlast_aa_def arrayO_except_assn_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p[b := (aa, ba)]› 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›)
apply (solves ‹auto›)
done
then show ?thesis
using assms by sep_auto
qed
lemma set_butlast_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry set_butlast_aa, uncurry (RETURN oo set_butlast_ll)) ∈
[λ(l,i). i < length l ∧ l ! i ≠ []]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a nat_assn⇧k → (arrayO_assn (arl_assn R))›
using assms by sepref_to_hoare sep_auto
definition last_aa :: "('a::heap array_list) array ⇒ nat ⇒ 'a Heap" where
‹last_aa xs i = do {
x ← Array.nth xs i;
arl_last x
}›
definition last_ll :: "'a list list ⇒ nat ⇒ 'a" where
‹last_ll xs i = last (xs ! i)›
lemma last_aa_rule[sep_heap_rules]:
assumes
p: ‹is_pure R› and
‹b < length a› and
‹a ! b ≠ []›
shows ‹
<arrayO_assn (arl_assn R) a ai>
last_aa ai b
<λr. arrayO_assn (arl_assn R) a ai * (∃⇩Ax. R x r * ↑ (x = last_ll a b))>⇩t›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
note arrayO_except_assn_arl_butlast[sep_heap_rules]
note arl_butlast_rule[sep_heap_rules del]
have ‹⋀b.
b < length a ⟹
a ! b ≠ [] ⟹
<arrayO_assn (arl_assn R) a ai>
last_aa ai b
<λr. arrayO_assn (arl_assn R) a ai * (∃⇩Ax. R x r * ↑ (x = last_ll a b))>⇩t›
apply (sep_auto simp add: last_aa_def last_ll_def assms)
apply (sep_auto simp add: last_aa_def arrayO_except_assn_def array_assn_def is_array_def
hr_comp_def arl_assn_def)
apply (subst_tac i=b in arrayO_except_assn_array0_index[symmetric])
apply (solves ‹simp›)
apply (subst arrayO_except_assn_def)
apply (auto simp add: last_aa_def arrayO_except_assn_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p› 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›)
apply (rule_tac x=‹bb› in ent_ex_postI)
unfolding R unfolding R'
apply (sep_auto simp: pure_def param_last)
done
from this[of b] show ?thesis
using assms unfolding R' by blast
qed
lemma last_aa_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows ‹(uncurry last_aa, uncurry (RETURN oo last_ll)) ∈
[λ(l,i). i < length l ∧ l ! i ≠ []]⇩a (arrayO_assn (arl_assn R))⇧k *⇩a nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
note arrayO_except_assn_arl_butlast[sep_heap_rules]
note arl_butlast_rule[sep_heap_rules del]
show ?thesis
using assms by sepref_to_hoare sep_auto
qed
definition nth_a :: ‹('a::heap array_list) array ⇒ nat ⇒ ('a array_list) Heap› where
‹nth_a xs i = do {
x ← Array.nth xs i;
arl_copy x}›
lemma nth_a_hnr[sepref_fr_rules]:
‹(uncurry nth_a, uncurry (RETURN oo op_list_get)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl_assn R))⇧k *⇩a nat_assn⇧k → arl_assn R›
unfolding nth_a_def
apply sepref_to_hoare
subgoal for b b' xs a
apply sep_auto
apply (subst arrayO_except_assn_array0_index[symmetric, of b])
apply simp
apply (sep_auto simp: arrayO_except_assn_def arl_length_def arl_assn_def
eq_commute[of ‹(_, _)›] hr_comp_def length_ll_def)
done
done
definition swap_aa :: "('a::heap array_list) array ⇒ nat ⇒ nat ⇒ nat ⇒ ('a array_list) array Heap" where
‹swap_aa xs k i j = do {
xi ← nth_aa xs k i;
xj ← nth_aa xs k j;
xs ← update_aa xs k i xj;
xs ← update_aa 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_aa_heap[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_ll aa b›
shows ‹
<arrayO_assn (arl_assn R) aa a>
nth_aa a b ba
<λr. ∃⇩Ax. arrayO_assn (arl_assn R) aa a *
(R x r *
↑ (x = nth_ll aa b ba)) *
true>›
proof -
have ‹<arrayO_assn (arl_assn R) aa a *
nat_assn b b *
nat_assn ba ba>
nth_aa a b ba
<λr. ∃⇩Ax. arrayO_assn (arl_assn R) aa a *
nat_assn b b *
nat_assn ba ba *
R x r *
true *
↑ (x = nth_ll aa b ba)>›
using p assms nth_aa_hnr[of R] unfolding hfref_def hn_refine_def
by auto
then show ?thesis
unfolding hoare_triple_def
by (auto simp: Let_def pure_def)
qed
lemma update_aa_rule_pure:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_ll aa b› and
b: ‹(bb, be) ∈ the_pure R›
shows ‹
<arrayO_assn (arl_assn R) aa a>
update_aa a b ba bb
<λr. ∃⇩Ax. invalid_assn (arrayO_assn (arl_assn R)) aa a * arrayO_assn (arl_assn R) x r *
true *
↑ (x = update_ll 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 ‹ <arrayO_assn (arl_assn R) aa a * nat_assn b b * nat_assn ba ba * R be bb>
update_aa a b ba bb
<λr. ∃⇩Ax. invalid_assn (arrayO_assn (arl_assn R)) aa a * nat_assn b b * nat_assn ba ba *
R be bb *
arrayO_assn (arl_assn R) x r *
true *
↑ (x = update_ll aa b ba be)>›
using p assms update_aa_hnr[of R] unfolding hfref_def hn_refine_def
by 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_ll[simp]: ‹length (update_ll a bb b c) = length a›
unfolding update_ll_def by auto
lemma length_ll_update_ll:
‹bb < length a ⟹ length_ll (update_ll a bb b c) bb = length_ll a bb›
unfolding length_ll_def update_ll_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_ll xs k ∧ j < length_ll xs k]⇩a
(arrayO_assn (arl_assn R))⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a nat_assn⇧k → (arrayO_assn (arl_assn R))›
proof -
note update_aa_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 arrayO_except_assn_def
length_ll_update_ll)
by (sep_auto simp: update_ll_def swap_def nth_ll_def list_update_swap)
qed
text ‹It is not possible to do a direct initialisation: there is no element that can be put
everywhere.›
definition arrayO_ara_empty_sz where
‹arrayO_ara_empty_sz n =
(let xs = fold (λ_ xs. [] # xs) [0..<n] [] in
op_list_copy xs)
›
lemma heap_list_all_list_assn: ‹heap_list_all R x y = list_assn R x y›
by (induction R x y rule: heap_list_all.induct) auto
lemma of_list_op_list_copy_arrayO[sepref_fr_rules]:
‹(Array.of_list, RETURN ∘ op_list_copy) ∈ (list_assn (arl_assn R))⇧d →⇩a arrayO_assn (arl_assn R)›
apply sepref_to_hoare
apply (sep_auto simp: arrayO_assn_def array_assn_def)
apply (rule_tac ?psi=‹xa ↦⇩a xi * list_assn (arl_assn R) x xi ⟹⇩A
is_array xi xa * heap_list_all (arl_assn R) x xi * true› in asm_rl)
by (sep_auto simp: heap_list_all_list_assn is_array_def)
sepref_definition
arrayO_ara_empty_sz_code
is "RETURN o arrayO_ara_empty_sz"
:: ‹nat_assn⇧k →⇩a arrayO_assn (arl_assn (R::'a ⇒ 'b::{heap, default} ⇒ assn))›
unfolding arrayO_ara_empty_sz_def op_list_empty_def[symmetric]
apply (rewrite at ‹(#) ⌑› op_arl_empty_def[symmetric])
apply (rewrite at ‹fold _ _ ⌑› op_HOL_list_empty_def[symmetric])
supply [[goals_limit = 1]]
by sepref
definition init_lrl :: ‹nat ⇒ 'a list list› where
‹init_lrl n = replicate n []›
lemma arrayO_ara_empty_sz_init_lrl: ‹arrayO_ara_empty_sz n = init_lrl n›
by (induction n) (auto simp: arrayO_ara_empty_sz_def init_lrl_def)
lemma arrayO_raa_empty_sz_init_lrl[sepref_fr_rules]:
‹(arrayO_ara_empty_sz_code, RETURN o init_lrl) ∈
nat_assn⇧k →⇩a arrayO_assn (arl_assn R)›
using arrayO_ara_empty_sz_code.refine unfolding arrayO_ara_empty_sz_init_lrl .
definition (in -) shorten_take_ll where
‹shorten_take_ll L j W = W[L := take j (W ! L)]›
definition (in -) shorten_take_aa where
‹shorten_take_aa L j W = do {
(a, n) ← Array.nth W L;
Array.upd L (a, j) W
}›
lemma Array_upd_arrayO_except_assn[sep_heap_rules]:
assumes
‹ba ≤ length (b ! a)› and
‹a < length b›
shows ‹<arrayO_except_assn (arl_assn R) [a] b bi
(λr'. arl_assn R (b ! a) (aaa, n) * ↑ ((aaa, n) = r' ! a))>
Array.upd a (aaa, ba) bi
<λr. ∃⇩Ax. arrayO_assn (arl_assn R) x r * true *
↑ (x = b[a := take ba (b ! a)])>›
proof -
have [simp]: ‹ba ≤ length l'›
if
‹ba ≤ length (b ! a)› and
aa: ‹(take n l', b ! a) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list›
proof -
show ?thesis
using list_rel_imp_same_length[OF aa] that
by auto
qed
have [simp]: ‹(take ba l', take ba (b ! a)) ∈ ⟨the_pure R⟩list_rel›
if
‹ba ≤ length (b ! a)› and
‹n ≤ length l'› and
take: ‹(take n l', b ! a) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list›
proof -
have [simp]: ‹n = length (b ! a)›
using list_rel_imp_same_length[OF take] that by auto
have 1: ‹take ba l' = take ba (take n l')›
using that by (auto simp: min_def)
show ?thesis
using take
unfolding 1
by (rule list_rel_take)
qed
have [simp]: ‹heap_list_all_nth (arl_assn R) (remove1 a [0..<length p])
(b[a := take ba (b ! a)]) (p[a := (aaa, ba)]) =
heap_list_all_nth (arl_assn R) (remove1 a [0..<length p]) b p›
for p :: ‹('b array × nat) list› and l' :: ‹'b list›
proof -
show ?thesis
by (rule heap_list_all_nth_cong) auto
qed
show ?thesis
using assms
unfolding arrayO_except_assn_def
apply (subst (2) arl_assn_def)
apply (subst is_array_list_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply (subst array_assn_def)
apply (subst is_array_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply sep_auto
apply (subst arrayO_except_assn_array0_index[symmetric, of a])
apply (solves simp)
unfolding arrayO_except_assn_def array_assn_def is_array_def
apply (subst (3) arl_assn_def)
apply (subst is_array_list_def[abs_def])
apply (subst (2) hr_comp_def[abs_def])
apply (subst ex_assn_move_out)+
apply (rule_tac x=‹p[a := (aaa, ba)]› in ent_ex_postI)
apply (rule_tac x=‹take ba l'› in ent_ex_postI)
by (sep_auto simp: )
qed
lemma shorten_take_aa_hnr[sepref_fr_rules]:
‹(uncurry2 shorten_take_aa, uncurry2 (RETURN ooo shorten_take_ll)) ∈
[λ((L, j), W). j ≤ length (W ! L) ∧ L < length W]⇩a
nat_assn⇧k *⇩a nat_assn⇧k *⇩a (arrayO_assn (arl_assn R))⇧d → arrayO_assn (arl_assn R)›
unfolding shorten_take_aa_def shorten_take_ll_def
by sepref_to_hoare sep_auto
end