Theory BTree_ImpSet
theory BTree_ImpSet
imports
BTree_Imp
BTree_Set
begin
section "Imperative Set operations"
subsection "Auxiliary operations"
definition "split_relation xs ≡
λ(as,bs) i. i ≤ length xs ∧ as = take i xs ∧ bs = drop i xs"
lemma split_relation_alt:
"split_relation as (ls,rs) i = (as = ls@rs ∧ i = length ls)"
by (auto simp add: split_relation_def)
lemma split_relation_length: "split_relation xs (ls,rs) (length xs) = (ls = xs ∧ rs = [])"
by (simp add: split_relation_def)
lemma list_assn_prod_map: "list_assn (A ×⇩a B) xs ys = list_assn B (map snd xs) (map snd ys) * list_assn A (map fst xs) (map fst ys)"
apply(induct "(A ×⇩a B)" xs ys rule: list_assn.induct)
apply(auto simp add: ab_semigroup_mult_class.mult.left_commute ent_star_mono star_aci(2) star_assoc)
done
lemma id_assn_list: "h ⊨ list_assn id_assn (xs::'a list) ys ⟹ xs = ys"
apply(induction "id_assn::('a ⇒ 'a ⇒ assn)" xs ys rule: list_assn.induct)
apply(auto simp add: less_Suc_eq_0_disj pure_def)
done
lemma snd_map_help:
"x ≤ length tsi ⟹
(∀j<x. snd (tsi ! j) = ((map snd tsi)!j))"
"x < length tsi ⟹ snd (tsi!x) = ((map snd tsi)!x)"
by auto
lemma split_ismeq: "((a::nat) ≤ b ∧ X) = ((a < b ∧ X) ∨ (a = b ∧ X))"
by auto
lemma split_relation_map: "split_relation as (ls,rs) i ⟹ split_relation (map f as) (map f ls, map f rs) i"
apply(induction as arbitrary: ls rs i)
apply(auto simp add: split_relation_def take_map drop_Cons')
apply(metis list.simps(9) take_map)
done
lemma split_relation_access: "⟦split_relation as (ls,rs) i; rs = r#rrs⟧ ⟹ as!i = r"
by (simp add: split_relation_alt)
lemma index_to_elem_all: "(∀j<length xs. P (xs!j)) = (∀x ∈ set xs. P x)"
by (simp add: all_set_conv_nth)
lemma index_to_elem: "n < length xs ⟹ (∀j<n. P (xs!j)) = (∀x ∈ set (take n xs). P x)"
by (simp add: all_set_conv_nth)
definition split_half :: "('a::heap × 'b::{heap}) pfarray ⇒ nat Heap"
where
"split_half a ≡ do {
l ← pfa_length a;
return (l div 2)
}"
lemma split_half_rule[sep_heap_rules]: "<
is_pfa c tsi a
* list_assn R ts tsi>
split_half a
<λi.
is_pfa c tsi a
* list_assn R ts tsi
* ↑(i = length ts div 2 ∧ split_relation ts (BTree_Set.split_half ts) i)>"
unfolding split_half_def split_relation_def
apply(rule hoare_triple_preI)
apply(sep_auto dest!: list_assn_len mod_starD)
done
subsection "The imperative split locale"
text "This locale extends the abstract split locale,
assuming that we are provided with an imperative program
that refines the abstract split function."
locale imp_split = abs_split: BTree_Set.split split
for split::
"('a btree × 'a::{heap,default,linorder}) list ⇒ 'a
⇒ ('a btree × 'a) list × ('a btree × 'a) list" +
fixes imp_split:: "('a btnode ref option × 'a::{heap,default,linorder}) pfarray ⇒ 'a ⇒ nat Heap"
assumes imp_split_rule [sep_heap_rules]:"sorted_less (separators ts) ⟹
<is_pfa c tsi (a,n)
* blist_assn k ts tsi>
imp_split (a,n) p
<λi.
is_pfa c tsi (a,n)
* blist_assn k ts tsi
* ↑(split_relation ts (split ts p) i)>⇩t"
begin
subsection "Membership"
partial_function (heap) isin :: "'a btnode ref option ⇒ 'a ⇒ bool Heap"
where
"isin p x =
(case p of
None ⇒ return False |
(Some a) ⇒ do {
node ← !a;
i ← imp_split (kvs node) x;
tsl ← pfa_length (kvs node);
if i < tsl then do {
s ← pfa_get (kvs node) i;
let (sub,sep) = s in
if x = sep then
return True
else
isin sub x
} else
isin (last node) x
}
)"
subsection "Insertion"