Theory BPlusTree_Iter_OneWay
theory BPlusTree_Iter_OneWay
imports
BPlusTree_Imp
"HOL-Real_Asymp.Inst_Existentials"
"Separation_Logic_Imperative_HOL.Imp_List_Spec"
Flatten_Iter
Partially_Filled_Array_Iter
begin
fun leaf_nodes_assn :: "nat ⇒ ('a::heap) bplustree list ⇒ 'a btnode ref option ⇒ 'a btnode ref option ⇒ assn" where
"leaf_nodes_assn k ((Leaf xs)#lns) (Some r) z =
(∃⇩A xsi fwd.
r ↦⇩r Btleaf xsi fwd
* is_pfa (2*k) xs xsi
* leaf_nodes_assn k lns fwd z
)" |
"leaf_nodes_assn k [] r z = ↑(r = z)" |
"leaf_nodes_assn _ _ _ _ = false"
fun inner_nodes_assn :: "nat ⇒ ('a::heap) bplustree ⇒ 'a btnode ref ⇒ 'a btnode ref option ⇒ 'a btnode ref option ⇒ assn" where
"inner_nodes_assn k (Leaf xs) a r z = ↑(r = Some a)" |
"inner_nodes_assn k (Node ts t) a r z =
(∃⇩A tsi ti tsi' tsi'' rs.
a ↦⇩r Btnode tsi ti
* inner_nodes_assn k t ti (last (r#rs)) (last (rs@[z]))
* is_pfa (2*k) tsi' tsi
* ↑(length tsi' = length rs)
* ↑(tsi'' = zip (zip (map fst tsi') (zip (butlast (r#rs)) (butlast (rs@[z])))) (map snd tsi'))
* list_assn ((λ t (ti,r',z'). inner_nodes_assn k t (the ti) r' z') ×⇩a id_assn) ts tsi''
)"
lemma leaf_nodes_assn_aux_append:
"leaf_nodes_assn k (xs@ys) r z = (∃⇩Al. leaf_nodes_assn k xs r l * leaf_nodes_assn k ys l z)"
apply(induction k xs r z rule: leaf_nodes_assn.induct)
apply(sep_auto intro!: ent_iffI)+
done
declare last.simps[simp del] butlast.simps[simp del]
declare mult.left_assoc[simp add]
lemma bplustree_leaf_nodes_help:
"bplustree_assn k t ti r z ⟹⇩A leaf_nodes_assn k (leaf_nodes t) r z * inner_nodes_assn k t ti r z"
proof(induction arbitrary: r rule: bplustree_assn.induct)
case (1 k xs a r z)
then show ?case
by (sep_auto)
next
case (2 k ts t a r z ra)
show ?case
apply(auto)
apply(rule ent_ex_preI)+
proof (goal_cases)
case (1 tsi ti tsi' tsi'' rs)
have *: "
length tsi's = length rss ⟹
length rss = length tss ⟹
set tsi's ⊆ set tsi' ⟹
set rss ⊆ set rs ⟹
set tss ⊆ set ts ⟹
bplustree_assn k t ti (last (ra # rss)) z *
blist_assn k tss
(zip (zip (subtrees tsi's) (zip (butlast (ra # rss)) rss)) (separators tsi's)) ⟹⇩A
leaf_nodes_assn k (concat (map (leaf_nodes ∘ fst) tss) @ leaf_nodes t) ra z *
inner_nodes_assn k t ti (last (ra#rss)) z *
list_assn ((λ t (ti,r',z'). inner_nodes_assn k t (the ti) r' z') ×⇩a id_assn) tss
(zip (zip (subtrees tsi's) (zip (butlast (ra # rss)) rss)) (separators tsi's))
"
for rss tsi's tss
proof (induct arbitrary: ra rule: list_induct3)
case (Nil r)
then show ?case
apply sep_auto
using 2(1)[of ti r "[]"]
apply (simp add: last.simps butlast.simps)
done
next
case (Cons subsepi tsi's subleaf rss subsep tss r)
show ?case
apply (sep_auto
simp add: butlast_double_Cons last_double_Cons)
apply(subst prod_assn_def)
apply(simp split!: prod.splits add: mult.left_assoc)
apply(subst leaf_nodes_assn_aux_append)
apply simp
apply(inst_ex_assn subleaf)
proof (goal_cases)
case (1 sub sep)
have "(sub,sep) ∈ set ts"
using "1" Cons.prems(3) by force
moreover have "set tsi's ⊆ set tsi' ∧ set rss ⊆ set rs ∧ set tss ⊆ set ts"
by (meson Cons.prems set_subset_Cons subset_trans)
moreover obtain temp1 temp2 where "((fst subsepi, (temp1:: 'a btnode ref option), subleaf), (temp2::'a)) ∈ set [((fst subsepi, temp1, subleaf), temp2)]"
by auto
ultimately show ?case
using
Cons(3)[of subleaf]
"2.IH"(2)[of "(sub,sep)"
"((fst subsepi, (temp1, subleaf)),temp2)" "[((fst subsepi, (temp1, subleaf)),temp2)]"
"fst subsepi" "(temp1, subleaf)" temp1 subleaf r]
apply auto
thm mult.commute
thm star_aci
apply(subst mult.commute)
thm mult.commute[where b="inner_nodes_assn k sub (the (fst subsepi)) r subleaf"]
apply(subst mult.commute[where b="inner_nodes_assn k sub (the (fst subsepi)) r subleaf"])
find_theorems "_ * _ = _ * _"
apply(simp)
thm ent_star_mono
supply R=ent_star_mono[where
P="bplustree_assn k sub (the (fst subsepi)) r subleaf" and P'="inner_nodes_assn k sub (the (fst subsepi)) r subleaf *
leaf_nodes_assn k (leaf_nodes sub) r subleaf"
and Q="bplustree_assn k t ti (last (subleaf # rss)) z *
id_assn sep (snd subsepi) *
blist_assn k tss
(zip (zip (subtrees tsi's) (zip (butlast (subleaf # rss)) rss)) (separators tsi's))"
and Q'="leaf_nodes_assn k (concat (map (λa. leaf_nodes (fst a)) tss) @ leaf_nodes t) subleaf
z *
inner_nodes_assn k t ti (last (subleaf # rss)) z *
id_assn sep (snd subsepi) *
list_assn ((λt (ti, x, y). inner_nodes_assn k t (the ti) x y) ×⇩a id_assn) tss
(zip (zip (subtrees tsi's) (zip (butlast (subleaf # rss)) rss)) (separators tsi's))"
,simplified]
thm R
apply(rule R)
subgoal
apply(subst mult.commute)
by simp
subgoal
thm mult.commute
apply(subst mult.commute[where b="id_assn _ _"], simp)+
find_theorems "_ * _ = _* _"
apply(subst mult.commute)
supply R = ent_star_mono[where
P="id_assn sep (snd subsepi)" and P'="id_assn sep (snd subsepi)"
and Q="bplustree_assn k t ti (last (subleaf # rss)) z *
blist_assn k tss
(zip (zip (subtrees tsi's) (zip (butlast (subleaf # rss)) rss))
(separators tsi's))" and
Q'="leaf_nodes_assn k (concat (map (λa. leaf_nodes (fst a)) tss) @ leaf_nodes t) subleaf
z *
inner_nodes_assn k t ti (last (subleaf # rss)) z *
list_assn ((λt (ti, x, y). inner_nodes_assn k t (the ti) x y) ×⇩a id_assn) tss
(zip (zip (subtrees tsi's) (zip (butlast (subleaf # rss)) rss))
(separators tsi's))"
, simplified]
thm R
apply(rule R)
apply simp
done
done
qed
qed
show ?case
apply(rule entails_preI)
using 1 apply (auto dest!: mod_starD list_assn_len)
using *[of tsi' rs ts, simplified]
apply(inst_ex_assn tsi ti tsi' tsi'' rs)
by (smt (z3) assn_aci(10) assn_times_comm fr_refl mult.right_neutral pure_true)
qed
qed
declare last.simps[simp add] butlast.simps[simp add]
declare mult.left_assoc[simp del]
lemma bplustree_leaf_nodes:
"bplustree_assn k t ti r z ⟹⇩A leaf_nodes_assn k (leaf_nodes t) r z * inner_nodes_assn k t ti r z"
using bplustree_leaf_nodes_help[of k t ti r z] by simp
fun leaf_node:: "('a::heap) bplustree ⇒ 'a list ⇒ assn" where
"leaf_node (Leaf xs) xsi = ↑(xs = xsi)" |
"leaf_node _ _ = false"
fun leafs_assn :: "('a::heap) pfarray list ⇒ 'a btnode ref option ⇒ 'a btnode ref option ⇒ assn" where
"leafs_assn (ln#lns) (Some r) z =
(∃⇩A fwd.
r ↦⇩r Btleaf ln fwd
* leafs_assn lns fwd z
)" |
"leafs_assn [] r z = ↑(r = z)" |
"leafs_assn _ _ _ = false"
lemma leafs_assn_aux_append:
"leafs_assn (xs@ys) r z = (∃⇩Al. leafs_assn xs r l * leafs_assn ys l z)"
apply(induction xs r z rule: leafs_assn.induct)
apply(sep_auto intro!: ent_iffI)+
done
lemma leaf_nodes_assn_split:
"leaf_nodes_assn k ts r z = (∃⇩Aps. list_assn leaf_node ts (map bplustree.vals ts) * list_assn (is_pfa (2*k)) (map bplustree.vals ts) ps * leafs_assn ps r z)"
proof (induction ts arbitrary: r)
case Nil
then show ?case
apply(intro ent_iffI)
subgoal by sep_auto
subgoal by sep_auto
done
next
case (Cons a xs)
then show ?case
proof(intro ent_iffI, goal_cases)
case 1
show ?case
apply(cases r; cases a)
apply simp_all
find_theorems "∃⇩A_._ ⟹⇩A_"
apply(rule ent_ex_preI)+
subgoal for aa x1 xsi fwd
apply (subst "Cons.IH"[of fwd])
apply simp
apply(rule ent_ex_preI)+
subgoal for ps
apply(inst_ex_assn "xsi#ps")
apply simp_all
apply(inst_ex_assn fwd)
apply (sep_auto)
done
done
done
next
case 2
have *: "list_assn leaf_node xs (map bplustree.vals xs) * list_assn (is_pfa (2 * k)) (map bplustree.vals xs) ps' * leafs_assn ps' r' z
⟹⇩A leaf_nodes_assn k xs r' z"
for ps' r'
using assn_eq_split(1)[OF sym[OF "Cons.IH"[of r']]]
ent_ex_inst[where Q="leaf_nodes_assn k xs r' z" and y=ps']
by blast
show ?case
apply(rule ent_ex_preI)+
subgoal for ps
apply(cases ps; cases r; cases a)
apply simp_all
apply(rule ent_ex_preI)+
subgoal for aa list aaa x1 fwd
apply(inst_ex_assn aa fwd)
apply sep_auto
using *[of list fwd]
by (smt (z3) assn_aci(9) assn_times_comm fr_refl)
done
done
qed
qed
lemma inst_same: "(⋀x. P x = Q x) ⟹ (∃⇩A x. P x) = (∃⇩A x. Q x)"
by simp
lemma inst_same2: "(⋀x. P = Q x) ⟹ P = (∃⇩A x. Q x)"
by simp
lemma pure_eq_pre: "(P ⟹ Q = R) ⟹ (Q * ↑P = R * ↑P)"
by fastforce
lemma bplustree_leaf_nodes_sep:
"leaf_nodes_assn k (leaf_nodes t) r z * (leaf_nodes_assn k (leaf_nodes t) r z -* bplustree_assn k t ti r z) ⟹⇩A bplustree_assn k t ti r z"
by (simp add: ent_mp)
declare last.simps[simp del] butlast.simps[simp del]
lemma bplustree_leaf_nodes_sep:
"bplustree_assn k t ti r z = leaf_nodes_assn k (leaf_nodes t) r z * (leaf_nodes_assn k (leaf_nodes t) r z -* bplustree_assn k t ti r z)"
oops
lemma leaf_nodes_assn_split_spec: "leaf_nodes_assn k
(leaf_nodes x @ ys) r z *
inner_nodes_assn k x a r m =
leaf_nodes_assn k (leaf_nodes x) r m * leaf_nodes_assn k ys m z *
inner_nodes_assn k x a r m"
oops
declare last.simps[simp del] butlast.simps[simp del]
lemma bplustree_leaf_nodes_sep:
"bplustree_assn k t ti r z = leaf_nodes_assn k (leaf_nodes t) r z * inner_nodes_assn k t ti r z"
oops
subsection "Iterator"
partial_function (heap) first_leaf :: "('a::heap) btnode ref ⇒ 'a btnode ref option Heap"
where
"first_leaf p = do {
node ← !p;
(case node of
Btleaf _ _ ⇒ do { return (Some p) } |
Btnode tsi ti ⇒ do {
s ← pfa_get tsi 0;
let (sub,sep) = s in do {
first_leaf (the sub)
}
}
)}"
partial_function (heap) last_leaf :: "('a::heap) btnode ref ⇒ 'a btnode ref option Heap"
where
"last_leaf p = do {
node ← !p;
(case node of
Btleaf _ z ⇒ do { return z } |
Btnode tsi ti ⇒ do {
last_leaf ti
}
)}"
declare last.simps[simp del] butlast.simps[simp del]
lemma first_leaf_rule[sep_heap_rules]:
assumes "k > 0" "root_order k t"
shows "<bplustree_assn k t ti r z>
first_leaf ti
<λu. bplustree_assn k t ti r z * ↑(u = r)>⇩t"
using assms
proof(induction t arbitrary: ti z)
case (Leaf x)
then show ?case
apply(subst first_leaf.simps)
apply (sep_auto dest!: mod_starD)
done
next
case (Node ts t)
then obtain sub sep tts where Cons: "ts = (sub,sep)#tts"
apply(cases ts) by auto
then show ?case
apply(subst first_leaf.simps)
apply (sep_auto simp add: butlast.simps)
subgoal for tsia tsil ti tsi' rs subi sepi
apply(cases rs; cases tsi')
apply simp_all
subgoal for subleaf rrs _ ttsi'
supply R = "Node.IH"(1)[of "(sub,sep)" sub "(the subi)" subleaf]
thm R
using "Node.prems"(1)
apply (sep_auto heap add: R)
subgoal by (metis Node.prems(2) assms(1) bplustree.inject(2) bplustree.simps(4) Cons list.set_intros(1) order_impl_root_order root_order.elims(2) some_child_sub(1))
apply (sep_auto eintros del: exI)
apply(inst_existentials tsia tsil ti "(subi, sepi) # ttsi'" "((subi, (r, subleaf)),sepi)#(zip (zip (subtrees ttsi') (zip (butlast (subleaf # rrs)) rrs)) (separators ttsi'))" "subleaf # rrs")
apply (sep_auto simp add: last.simps butlast.simps)+
done
done
done
qed
declare last.simps[simp add] butlast.simps[simp add]
declare last.simps[simp del] butlast.simps[simp del]
lemma last_leaf_rule[sep_heap_rules]:
assumes "k > 0" "root_order k t"
shows "<bplustree_assn k t ti r z>
last_leaf ti
<λu. bplustree_assn k t ti r z * ↑(u = z)>⇩t"
using assms
proof(induction t arbitrary: ti r)
case (Leaf x)
then show ?case
apply(subst last_leaf.simps)
apply (sep_auto dest!: mod_starD)
done
next
case (Node ts t)
show ?case
apply(subst last_leaf.simps)
supply R = "Node.IH"(2)
apply (sep_auto heap add: R)
subgoal using "Node.prems" by simp
subgoal by (metis Node.prems(2) assms(1) bplustree.inject(2) bplustree.simps(4) Cons list.set_intros(1) order_impl_root_order root_order.elims(2) some_child_sub(1))
apply (sep_auto eintros del: exI)
subgoal for tsia tsil ti tsi' rs
apply(inst_existentials tsia tsil ti "tsi'" " (zip (zip (subtrees tsi') (zip (butlast (r # rs)) rs)) (separators tsi'))" rs)
apply (sep_auto simp add: last.simps butlast.simps)+
done
done
qed
declare last.simps[simp add] butlast.simps[simp add]
definition tree_leaf_iter_init where
"tree_leaf_iter_init p = do {
r ← first_leaf (the p);
z ← last_leaf (the p);
return (r, z)
}"
lemma tree_leaf_iter_init_rule:
assumes "k > 0" "root_order k t"
shows "<bplustree_assn k t ti r z>
tree_leaf_iter_init (Some ti)
<λ(u,v). leaf_nodes_assn k (leaf_nodes t) u v * inner_nodes_assn k t ti r z * ↑(u = r ∧ v = z)>⇩t"
using assms
using bplustree_leaf_nodes_help[of k t ti r z]
unfolding tree_leaf_iter_init_def
apply (sep_auto)
using ent_star_mono ent_true by blast
definition leaf_iter_next where
"leaf_iter_next = (λ(r,z). do {
p ← !(the r);
return (vals p, (fwd p, z))
})"
lemma leaf_iter_next_rule_help:
"<leafs_assn (x#xs) r z>
leaf_iter_next (r,z)
<λ(p,(n,z')). leafs_assn [x] r n * leafs_assn xs n z' * ↑(p = x) * ↑(z=z')>"
apply(subst leaf_iter_next_def)
apply(cases r; cases x)
apply(sep_auto)+
done
definition leaf_iter_assn where "leaf_iter_assn xs r xs2 = (λ(n,z).
(∃⇩Axs1. ↑(xs = xs1@xs2) * leafs_assn xs1 r n * leafs_assn xs2 n z * ↑(z=None)))"
lemma leaf_nodes_assn_imp_iter_assn: "leafs_assn xs r None ⟹⇩A leaf_iter_assn xs r xs (r,None)"
unfolding leaf_iter_assn_def
by sep_auto
definition leaf_iter_init where
"leaf_iter_init p = do {
return (p, None)
}"
lemma leaf_iter_init_rule:
shows "<leafs_assn xs r None>
leaf_iter_init r
<λu. leaf_iter_assn xs r xs u>"
unfolding leaf_iter_init_def
using leaf_nodes_assn_imp_iter_assn
by (sep_auto)
lemma leaf_iter_next_rule: "<leaf_iter_assn xs r (x#xs2) it>
leaf_iter_next it
<λ(p, it'). leaf_iter_assn xs r xs2 it' * ↑(p = x)>"
unfolding leaf_iter_assn_def
apply(cases it)
by (sep_auto heap add: leaf_iter_next_rule_help simp add: leafs_assn_aux_append)
definition leaf_iter_has_next where
"leaf_iter_has_next = (λ(r,z). return (r ≠ z))"
lemma leaf_iter_has_next_rule:
"<leaf_iter_assn xs r xs2 it> leaf_iter_has_next it <λu. leaf_iter_assn xs r xs2 it * ↑(u ⟷ xs2 ≠ [])>"
unfolding leaf_iter_has_next_def
apply(cases it)
apply(sep_auto simp add: leaf_iter_assn_def split!: prod.splits dest!: mod_starD)
subgoal for a
apply(cases xs2; cases a)
by auto
done
declare mult.left_commute[simp add]
lemma leafs_assn_prec2:
"∀l l'. (h⊨
(leafs_assn l p None * F1) ∧⇩A (leafs_assn l' p None * F2))
⟶ l=l'"
apply (intro allI)
subgoal for l l'
proof (induct l arbitrary: p l' F1 F2)
case Nil thus ?case
apply simp_all
apply (cases l')
apply simp
apply (cases p)
apply auto
done
next
case (Cons y l)
from Cons.prems show ?case
apply (cases p)
apply simp
apply (cases l')
apply (auto) []
apply (clarsimp)
apply (rule)
apply (drule_tac p=a in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
subgoal for a aa b list fwd fwda
apply(subgoal_tac "fwd=fwda")
using Cons.hyps[of fwd "a ↦⇩r Btleaf y fwda * F1" list "a ↦⇩r Btleaf (aa, b) fwd * F2", simplified]
apply (simp add: mult.left_assoc mod_and_dist)
apply (simp add: ab_semigroup_mult_class.mult.commute)
apply (drule_tac p=a in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
done
qed
done
declare mult.left_commute[simp del]
interpretation leaf_node_it: imp_list_iterate
"λx y. leafs_assn x y None"
leaf_iter_assn
leaf_iter_init
leaf_iter_has_next
leaf_iter_next
apply(unfold_locales)
subgoal
by (simp add: leafs_assn_prec2 precise_def)
subgoal for l p
by (sep_auto heap add: leaf_iter_init_rule)
subgoal for l' l p it
thm leaf_iter_next_rule
apply(cases l'; cases it)
by (sep_auto heap add: leaf_iter_next_rule)+
subgoal for l p l' it'
thm leaf_iter_has_next_rule
apply(cases it')
apply(rule hoare_triple_preI)
apply(sep_auto heap add: leaf_iter_has_next_rule)
done
subgoal for l p l' it
unfolding leaf_iter_assn_def
apply(cases it)
apply simp_all
apply(rule ent_ex_preI)
by (sep_auto simp add: leafs_assn_aux_append)
done
interpretation leaf_elements_iter: flatten_iter
"λx y. leafs_assn x y None" leaf_iter_assn leaf_iter_init leaf_iter_has_next leaf_iter_next
"is_pfa (2*k)" "pfa_is_it (2*k)" pfa_it_init pfa_it_has_next pfa_it_next
by (unfold_locales)
thm leaf_elements_iter.is_flatten_list.simps
thm leaf_elements_iter.is_flatten_it.simps
thm tree_leaf_iter_init_def
thm leaf_elements_iter.flatten_it_init_def
print_theorems
fun leaf_elements_iter_init :: "('a::heap) btnode ref ⇒ _" where
"leaf_elements_iter_init ti = do {
rz ← tree_leaf_iter_init (Some ti);
it ← leaf_elements_iter.flatten_it_init (fst rz);
return it
}"
lemma leaf_nodes_imp_flatten_list:
"leaf_nodes_assn k ts r None ⟹⇩A
list_assn leaf_node ts (map bplustree.vals ts) *
leaf_elements_iter.is_flatten_list k (concat (map bplustree.vals ts)) r"
apply(simp add: leaf_nodes_assn_split)
apply(rule ent_ex_preI)+
subgoal for ps
apply(inst_ex_assn ps "map bplustree.vals ts")
apply sep_auto
done
done
lemma concat_leaf_nodes_leaves: "(concat (map bplustree.vals (leaf_nodes t))) = leaves t"
apply(induction t rule: leaf_nodes.induct)
subgoal by auto
subgoal for ts t
apply(induction ts)
subgoal by simp
subgoal by auto
done
done
lemma leaf_elements_iter_init_rule:
assumes "k > 0" "root_order k t"
shows "<bplustree_assn k t ti r None>
leaf_elements_iter_init ti
<leaf_elements_iter.is_flatten_it k (leaves t) r (leaves t)>⇩t"
unfolding leaf_elements_iter_init.simps
using assms
apply (sep_auto heap add:
tree_leaf_iter_init_rule
)
supply R = Hoare_Triple.cons_pre_rule[OF leaf_nodes_imp_flatten_list[of k "leaf_nodes t" r],
where Q="λit. leaf_elements_iter.is_flatten_it k (leaves t) r (leaves t) it * true"
and c="leaf_elements_iter.flatten_it_init r"]
thm R
apply(sep_auto heap add: R)
subgoal
apply(simp add: concat_leaf_nodes_leaves)
apply sep_auto
done
subgoal by sep_auto
done
end