Theory BTree_Set
theory BTree_Set
imports BTree
"HOL-Data_Structures.Set_Specs"
begin
section "Set interpretation"
subsection "Auxiliary functions"
fun split_half:: "('a btree×'a) list ⇒ (('a btree×'a) list × ('a btree×'a) list)" where
"split_half xs = (take (length xs div 2) xs, drop (length xs div 2) xs)"
lemma drop_not_empty: "xs ≠ [] ⟹ drop (length xs div 2) xs ≠ []"
apply(induction xs)
apply(auto split!: list.splits)
done
lemma split_half_not_empty: "length xs ≥ 1 ⟹ ∃ls sub sep rs. split_half xs = (ls,(sub,sep)#rs)"
using drop_not_empty
by (metis (no_types, opaque_lifting) drop0 drop_eq_Nil eq_snd_iff hd_Cons_tl le_trans not_one_le_zero split_half.simps)
subsection "The split function locale"
text "Here, we abstract away the inner workings of the split function
for B-tree operations."
locale split =
fixes split :: "('a btree×'a::linorder) list ⇒ 'a ⇒ (('a btree×'a) list × ('a btree×'a) list)"
assumes split_req:
"⟦split xs p = (ls,rs)⟧ ⟹ xs = ls @ rs"
"⟦split xs p = (ls@[(sub,sep)],rs); sorted_less (separators xs)⟧ ⟹ sep < p"
"⟦split xs p = (ls,(sub,sep)#rs); sorted_less (separators xs)⟧ ⟹ p ≤ sep"
begin
lemmas split_conc = split_req(1)
lemmas split_sorted = split_req(2,3)
lemma [termination_simp]:"(ls, (sub, sep) # rs) = split ts y ⟹
size sub < Suc (size_list (λx. Suc (size (fst x))) ts + size l)"
using split_conc[of ts y ls "(sub,sep)#rs"] by auto
fun invar_inorder where "invar_inorder k t = (bal t ∧ root_order k t)"
definition "empty_btree = Leaf"
subsection "Membership"
fun isin:: "'a btree ⇒ 'a ⇒ bool" where
"isin (Leaf) y = False" |
"isin (Node ts t) y = (
case split ts y of (_,(sub,sep)#rs) ⇒ (
if y = sep then
True
else
isin sub y
)
| (_,[]) ⇒ isin t y
)"
subsection "Insertion"
text "The insert function requires an auxiliary data structure
and auxiliary invariant functions."