Theory BPlusTree_ImpSet
theory BPlusTree_ImpSet
imports
BPlusTree_Set
BPlusTree_ImpSplit
"HOL-Real_Asymp.Inst_Existentials"
begin
section "Imperative Set operations"
subsection "Auxiliary operations"
text "This locale extends the abstract split locale,
assuming that we are provided with an imperative program
that refines the abstract split function."
locale split⇩i_set = abs_split_set: split_set split + split⇩i_tree split split⇩i
for split::
"('a bplustree × 'a::{heap,default,linorder,order_top}) list ⇒ 'a
⇒ ('a bplustree × 'a) list × ('a bplustree × 'a) list"
and split⇩i :: "('a btnode ref option × 'a::{heap,default,linorder,order_top}) pfarray ⇒ 'a ⇒ nat Heap" +
fixes isin_list⇩i:: "'a ⇒ ('a::{heap,default,linorder,order_top}) pfarray ⇒ bool Heap"
and ins_list⇩i:: "'a ⇒ ('a::{heap,default,linorder,order_top}) pfarray ⇒ 'a pfarray Heap"
and del_list⇩i:: "'a ⇒ ('a::{heap,default,linorder,order_top}) pfarray ⇒ 'a pfarray Heap"
assumes isin_list_rule [sep_heap_rules]:"sorted_less ks ⟹
<is_pfa c ks (a',n')>
isin_list⇩i x (a',n')
<λb.
is_pfa c ks (a',n')
* ↑(isin_list x ks = b)>⇩t"
and ins_list_rule [sep_heap_rules]:"sorted_less ks' ⟹
<is_pfa c ks' (a',n')>
ins_list⇩i x (a',n')
<λ(a'',n''). is_pfa (max c (length (insert_list x ks'))) (insert_list x ks') (a'',n'') >⇩t"
and del_list_rule [sep_heap_rules]:"sorted_less ks'' ⟹
<is_pfa c ks'' (a',n')>
del_list⇩i x (a',n')
<λ(a'',n''). is_pfa c (delete_list x ks'') (a'',n'') >⇩t"
begin
subsection "Initialization"
definition empty⇩i ::"nat ⇒ 'a btnode ref Heap"
where "empty⇩i k = do {
empty_list ← pfa_empty (2*k);
empty_leaf ← ref (Btleaf empty_list None);
return empty_leaf
}"
lemma empty⇩i_rule:
shows "<emp>
empty⇩i k
<λr. bplustree_assn k (abs_split_set.empty_bplustree) r (Some r) None>"
apply(subst empty⇩i_def)
apply(sep_auto simp add: abs_split_set.empty_bplustree_def)
done
subsection "Membership"
partial_function (heap) isin⇩i :: "'a btnode ref ⇒ 'a ⇒ bool Heap"
where
"isin⇩i p x = do {
node ← !p;
(case node of
Btleaf xs _ ⇒ isin_list⇩i x xs |
Btnode ts t ⇒ do {
i ← split⇩i ts x;
tsl ← pfa_length ts;
if i < tsl then do {
s ← pfa_get ts i;
let (sub,sep) = s in
isin⇩i (the sub) x
} else
isin⇩i t x
}
)}"
lemma nth_zip_zip:
assumes "length ys = length xs"
and "length zs = length xs"
and "zs1 @ ((suba', x), sepa') # zs2 =
zip (zip ys xs) zs"
shows "suba' = ys ! length zs1 ∧
sepa' = zs ! length zs1 ∧
x = xs ! length zs1"
proof -
obtain suba'' x' sepa'' where "zip (zip ys xs) zs ! length zs1 = ((suba'', x'), sepa'')"
by (metis surj_pair)
moreover have "((suba'', x'), sepa'') = ((suba', x), sepa')"
by (metis calculation assms(3) nth_append_length)
moreover have "length zs1 < length xs"
proof -
have "length (zip (zip ys xs) zs) = length xs"
by (simp add: assms(1,2))
then have "length zs1 + 1 + length zs2 = length xs"
by (metis assms(1,3) group_cancel.add1 length_Cons length_append plus_1_eq_Suc)
then show ?thesis
by (simp add: assms(1))
qed
ultimately show ?thesis
using assms(1,2) by auto
qed
lemma "k > 0 ⟹ root_order k t ⟹ sorted_less (inorder t) ⟹ sorted_less (leaves t) ⟹
<bplustree_assn k t ti r z>
isin⇩i ti x
<λy. bplustree_assn k t ti r z * ↑(abs_split_set.isin t x = y)>⇩t"
proof(induction t x arbitrary: ti r z rule: abs_split_set.isin.induct)
case (1 x r z)
then show ?case
apply(subst isin⇩i.simps)
apply sep_auto
done
next
case (2 ts t x ti r z)
obtain ls rs where list_split[simp]: "split ts x = (ls,rs)"
by (cases "split ts x")
moreover have ts_non_empty: "length ts > 0"
using "2.prems"(2) root_order.simps(2) by blast
moreover have "sorted_less (separators ts)"
using "2.prems"(3) sorted_inorder_separators by blast
ultimately show ?case
proof (cases rs)
case [simp]: Nil
show ?thesis
apply(subst isin⇩i.simps)
using ts_non_empty apply(sep_auto)
subgoal using ‹sorted_less (separators ts)› by blast
apply simp
apply sep_auto
apply(rule hoare_triple_preI)
apply (sep_auto)
subgoal for a b ti tsi' rs x sub sep
apply(auto simp add: split_relation_alt is_pfa_def dest!: mod_starD list_assn_len)[]
done
thm "2.IH"(1)[of ls "[]"]
using 2(3) apply(sep_auto heap: "2.IH"(1)[of ls "[]"] simp add: sorted_wrt_append)
subgoal
using "2.prems"(2) order_impl_root_order
by (auto simp add: split_relation_alt is_pfa_def dest!: mod_starD list_assn_len)[]
subgoal
using "2.prems"(3) sorted_inorder_induct_last
by (auto simp add: split_relation_alt is_pfa_def dest!: mod_starD list_assn_len)[]
subgoal using "2"(6) sorted_leaves_induct_last
by (auto simp add: split_relation_alt is_pfa_def dest!: mod_starD list_assn_len)[]
using 2(3) apply(sep_auto heap: "2.IH"(1)[of ls "[]"] simp add: sorted_wrt_append)
done
next
case [simp]: (Cons h rrs)
obtain sub sep where h_split[simp]: "h = (sub,sep)"
by (cases h)
then show ?thesis
apply(simp split: list.splits prod.splits)
apply(subst isin⇩i.simps)
using "2.prems" sorted_inorder_separators
apply(sep_auto)
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!: mod_starD list_assn_len)[]
apply(rule norm_pre_ex_rule)+
apply(rule hoare_triple_preI)
subgoal for tsi n ti tsi' pointers suba sepa zs1 z zs2
apply(cases z)
subgoal for subacomb sepa'
apply(cases subacomb)
subgoal for suba' subp subfwd
apply(subgoal_tac "z = ((suba, subp, subfwd), sepa)", simp)
thm "2.IH"(2)[of ls rs h rrs sub sep "(the suba')" subp subfwd]
using 2(3,4,5,6) apply(sep_auto
heap:"2.IH"(2)[of ls rs h rrs sub sep "the suba'" subp subfwd]
simp add: sorted_wrt_append)
using list_split Cons h_split apply simp_all
subgoal
by (meson "2.prems"(1) order_impl_root_order)
subgoal
apply(rule impI)
apply(inst_ex_assn "(tsi,n)" "ti" "tsi'" "(zs1 @ ((suba', subp, subfwd), sepa') # zs2)" "pointers" "zs1" "z" "zs2")
apply sep_auto
done
subgoal
using nth_zip_zip[of "subtrees tsi'" "zip (r # butlast pointers) pointers" "separators tsi'" zs1 suba' "(subp, subfwd)" sepa' zs2]
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!: mod_starD list_assn_len)[]
done
done
done
done
apply(rule hoare_triple_preI)
apply(auto simp add: split_relation_def dest!: mod_starD list_assn_len)[]
done
qed
qed
subsection "Insertion"