diff --git a/metadata/entries/BTree.toml b/metadata/entries/BTree.toml
--- a/metadata/entries/BTree.toml
+++ b/metadata/entries/BTree.toml
@@ -1,42 +1,49 @@
title = "A Verified Imperative Implementation of B-Trees"
date = 2021-02-24
topics = [
"Computer science/Data structures",
]
abstract = """
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bayer and McCreight [ACM 1970]. The
-implementation supports set membership, insertion and deletion queries with
-efficient binary search for intra-node navigation. This is
+implementation supports set membership, insertion, deletion, iteration and range queries with efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the
Isabelle Refinement Framework . The code can be exported to
-the programming languages SML, OCaml and Scala. We examine the runtime of all
-operations indirectly by reproducing results of the logarithmic
-relationship between height and the number of nodes. The results are
-discussed in greater detail in the corresponding
+ B-Trees
+ This formalisation is discussed in greater detail in the corresponding Bachelor's
-Thesis."""
+Thesis.
+ B+-Trees:
+ This formalisation also supports range queries and is discussed in a paper published at ICTAC 2022.
+
+
+Change history:
+[2022-08-16]: Added formalisations of B+-Trees
+"""
license = "bsd"
note = ""
[authors]
[authors.muendler]
email = "muendler_email"
[contributors]
[notify]
muendler = "muendler_email"
[history]
[extra]
[related]
diff --git a/thys/BTree/Array_SBlit.thy b/thys/BTree/Array_SBlit.thy
--- a/thys/BTree/Array_SBlit.thy
+++ b/thys/BTree/Array_SBlit.thy
@@ -1,305 +1,305 @@
theory Array_SBlit
imports "Separation_Logic_Imperative_HOL.Array_Blit"
begin
(* Resolves TODO by Peter Lammich *)
(* OCaml handles the case of len=0 correctly (i.e.
as specified by the Hoare Triple in Array_Blit
-not generating an exception if si+len \ array length and such) *)
+not generating an exception if si+len \ array length and such) *)
code_printing code_module "array_blit" \ (OCaml)
\
- let array_blit src si dst di len = (
- if src=dst then
- raise (Invalid_argument "array_blit: Same arrays")
- else
- Array.blit src (Z.to_int si) dst (Z.to_int di) (Z.to_int len)
- )
+let array_blit src si dst di len = (
+ if src=dst then
+ raise (Invalid_argument "array_blit: Same arrays")
+ else
+ Array.blit src (Z.to_int si) dst (Z.to_int di) (Z.to_int len)
+);;
\
code_printing constant blit' \
- (OCaml) "(fun () -> /array'_blit _ _ _ _ _)"
+ (OCaml) "(fun () -> /array'_blit _ _ _ _ _)"
export_code blit checking OCaml
section "Same array Blit"
text "The standard framework already provides a function to copy array
elements."
term blit
thm blit_rule
thm blit.simps
(* Same array BLIT *)
definition "sblit a s d l \ blit a s a d l"
text "When copying values within arrays,
blit only works for moving elements to the left."
lemma sblit_rule[sep_heap_rules]:
assumes LEN:
"si+len \ length lsrc"
and DST_SM: "di \ si"
shows
"< src \\<^sub>a lsrc >
sblit src si di len
<\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding sblit_def
using LEN DST_SM
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
- case (Suc len)
- note [sep_heap_rules] = Suc.IH
+ case (Suc len)
+ note [sep_heap_rules] = Suc.IH
have [simp]: "\x. lsrc ! si # take len (drop (Suc si) lsrc) @ x
= take (Suc len) (drop si lsrc) @ x"
apply simp
by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc
- less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
+ less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
Nat.trans_le_add2)
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "A reverse blit"
text "The function rblit may be used to copy elements a defined offset to the right"
(* Right BLIT or Reverse BLIT *)
primrec rblit :: "_ array \ nat \ _ array \ nat \ nat \ unit Heap" where
"rblit _ _ _ _ 0 = return ()"
| "rblit src si dst di (Suc l) = do {
x \ Array.nth src (si+l);
Array.upd (di+l) x dst;
rblit src si dst di l
}"
text "For separated arrays it is equivalent to normal blit.
The proof follows similarly to the corresponding proof for blit."
lemma rblit_rule[sep_heap_rules]:
assumes LEN: "si+len \ length lsrc" "di+len \ length ldst"
shows
- "< src \\<^sub>a lsrc
+ "< src \\<^sub>a lsrc
* dst \\<^sub>a ldst >
rblit src si dst di len
- <\_. src \\<^sub>a lsrc
+ <\_. src \\<^sub>a lsrc
* dst \\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst)
>"
using LEN
proof (induction len arbitrary: ldst)
case 0 thus ?case by sep_auto
next
- case (Suc len)
+ case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "drop (di + len) (ldst[di + len := lsrc ! (si + len)])
= lsrc ! (si + len) # drop (Suc (di + len)) ldst"
by (metis Cons_nth_drop_Suc Suc.prems(2) Suc_le_eq add_Suc_right drop_upd_irrelevant length_list_update lessI nth_list_update_eq)
have "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length (drop si lsrc)"
using Suc.prems(1) by force
then show "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
by (metis (no_types) Suc.prems(1) add_leD1 nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
definition "srblit a s d l \ rblit a s a d l"
text "However, within arrays we can now copy to the right."
lemma srblit_rule[sep_heap_rules]:
assumes LEN:
"di+len \ length lsrc"
and DST_GR: "di \ si"
shows
"< src \\<^sub>a lsrc >
srblit src si di len
<\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding srblit_def
using LEN DST_GR
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
- case (Suc len)
+ case (Suc len)
note [sep_heap_rules] = Suc.IH
have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
= take len (drop si lsrc)"
by (metis Suc.prems(2) ab_semigroup_add_class.add.commute add_le_cancel_right take_drop take_update_cancel)
have [simp]: "drop (di + len) (lsrc[di + len := lsrc ! (si + len)])
= lsrc ! (si+len) # drop (Suc di + len) lsrc"
by (metis Suc.prems(1) add_Suc_right add_Suc_shift add_less_cancel_left append_take_drop_id le_imp_less_Suc le_refl plus_1_eq_Suc same_append_eq take_update_cancel upd_conv_take_nth_drop)
have "take len (drop si lsrc) @
[lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length lsrc - si"
using Suc.prems(1) Suc.prems(2) by linarith
then show ?thesis
by (metis (no_types) Suc.prems(1) Suc.prems(2) add_leD1 le_add_diff_inverse length_drop nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "Modeling target language blit"
text "For convenience, a function that is oblivious to the direction of the shift
is defined."
-definition "safe_sblit a s d l \
+definition "safe_sblit a s d l \
if s > d then
sblit a s d l
else
srblit a s d l
"
text "We obtain a heap rule similar to the one of blit,
but for copying within one array."
lemma safe_sblit_rule[sep_heap_rules]:
assumes LEN:
"len > 0 \ di+len \ length lsrc \ si+len \ length lsrc"
shows
"< src \\<^sub>a lsrc >
safe_sblit src si di len
<\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding safe_sblit_def
using LEN
apply(cases len)
apply(sep_auto simp add: sblit_def srblit_def)[]
apply sep_auto
done
(* Compare this to blit_rule *)
thm blit_rule
thm safe_sblit_rule
subsection "Code Generator Setup"
text "Note that the requirement for correctness
is even weaker here than in SML/OCaml.
In particular, if the length of the slice to copy is equal to 0,
we will never throw an exception.
We therefore manually handle this case, where nothing happens at all."
code_printing code_module "array_sblit" \ (SML)
\
fun array_sblit src si di len = (
if len > 0 then
ArraySlice.copy {
di = IntInf.toInt di,
src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
dst = src}
else ()
)
\
code_printing code_module "array_sblit" \ (OCaml)
\
- let array_sblit src si di len = (
- if len > Z.zero then
- (Array.blit src (Z.to_int si) src (Z.to_int di) (Z.to_int len))
- else ()
- )
+let array_sblit src si di len = (
+ if len > Z.zero then
+ (Array.blit src (Z.to_int si) src (Z.to_int di) (Z.to_int len))
+ else ()
+);;
\
definition safe_sblit' where
- [code del]: "safe_sblit' src si di len
- = safe_sblit src (nat_of_integer si) (nat_of_integer di)
+ [code del]: "safe_sblit' src si di len
+ = safe_sblit src (nat_of_integer si) (nat_of_integer di)
(nat_of_integer len)"
lemma [code]:
- "safe_sblit src si di len
- = safe_sblit' src (integer_of_nat si) (integer_of_nat di)
+ "safe_sblit src si di len
+ = safe_sblit' src (integer_of_nat si) (integer_of_nat di)
(integer_of_nat len)" by (simp add: safe_sblit'_def)
(* TODO: Export to other languages: Haskell *)
code_printing constant safe_sblit' \
(SML) "(fn/ ()/ => /array'_sblit _ _ _ _)"
and (Scala) "{ ('_: Unit)/=>/
def safescopy(src: Array['_], srci: Int, dsti: Int, len: Int) = {
if (len > 0)
System.arraycopy(src, srci, src, dsti, len)
else
()
}
safescopy(_.array,_.toInt,_.toInt,_.toInt)
}"
code_printing constant safe_sblit' \
- (OCaml) "(fun () -> /array'_sblit _ _ _ _)"
+ (OCaml) "(fun () -> /array'_sblit _ _ _ _)"
export_code safe_sblit checking SML Scala OCaml
subsection "Derived operations"
definition array_shr where
"array_shr a i k \ do {
l \ Array.len a;
safe_sblit a i (i+k) (l-(i+k))
}"
find_theorems "Array.len"
lemma array_shr_rule[sep_heap_rules]:
"< src \\<^sub>a lsrc >
array_shr src i k
<\_. src \\<^sub>a (take (i+k) lsrc @ take (length lsrc - (i+k)) (drop i lsrc))
>"
unfolding array_shr_def
by sep_auto
lemma array_shr_rule_alt:
"< src \\<^sub>a lsrc >
array_shr src i k
<\_. src \\<^sub>a (take (length lsrc) (take (i+k) lsrc @ (drop i lsrc)))
>"
by (sep_auto simp add: min_def)
definition array_shl where
"array_shl a i k \ do {
l \ Array.len a;
safe_sblit a i (i-k) (l-i)
}
"
lemma array_shl_rule[sep_heap_rules]:
"
< src \\<^sub>a lsrc >
array_shl src i k
<\_. src \\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (i - k + (length lsrc - i)) lsrc)
>"
unfolding array_shl_def
by sep_auto
lemma array_shl_rule_alt:
"
\i \ length lsrc; k \ i\ \
< src \\<^sub>a lsrc >
array_shl src i k
<\_. src \\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (length lsrc - k) lsrc)
>"
by sep_auto
end
\ No newline at end of file
diff --git a/thys/BTree/BPlusTree.thy b/thys/BTree/BPlusTree.thy
new file mode 100644
--- /dev/null
+++ b/thys/BTree/BPlusTree.thy
@@ -0,0 +1,652 @@
+theory BPlusTree
+ imports Main "HOL-Data_Structures.Sorted_Less" "HOL-Data_Structures.Cmp" "HOL-Library.Multiset"
+begin
+
+(* some setup to cover up the redefinition of sorted in Sorted_Less
+ but keep the lemmas *)
+hide_const (open) Sorted_Less.sorted
+abbreviation "sorted_less \ Sorted_Less.sorted"
+
+section "Definition of the B-Plus-Tree"
+
+subsection "Datatype definition"
+
+text "B-Plus-Trees are basically B-Trees, that don't have empty Leafs but Leafs that contain
+the relevant data. "
+
+
+datatype 'a bplustree = Leaf (vals: "'a list") | Node (keyvals: "('a bplustree * 'a) list") (lasttree: "'a bplustree")
+
+type_synonym 'a bplustree_list = "('a bplustree * 'a) list"
+type_synonym 'a bplustree_pair = "('a bplustree * 'a)"
+
+abbreviation subtrees where "subtrees xs \ (map fst xs)"
+abbreviation separators where "separators xs \ (map snd xs)"
+
+subsection "Inorder and Set"
+
+text "The set of B-Plus-tree needs to be manually defined, regarding only the leaves.
+This overrides the default instantiation."
+
+fun set_nodes :: "'a bplustree \ 'a set" where
+ "set_nodes (Leaf ks) = {}" |
+ "set_nodes (Node ts t) = \(set (map set_nodes (subtrees ts))) \ (set (separators ts)) \ set_nodes t"
+
+fun set_leaves :: "'a bplustree \ 'a set" where
+ "set_leaves (Leaf ks) = set ks" |
+ "set_leaves (Node ts t) = \(set (map set_leaves (subtrees ts))) \ set_leaves t"
+
+text "The inorder is a view of only internal seperators"
+
+fun inorder :: "'a bplustree \ 'a list" where
+ "inorder (Leaf ks) = []" |
+ "inorder (Node ts t) = concat (map (\ (sub, sep). inorder sub @ [sep]) ts) @ inorder t"
+
+abbreviation "inorder_list ts \ concat (map (\ (sub, sep). inorder sub @ [sep]) ts)"
+
+text "The leaves view considers only its leafs."
+
+fun leaves :: "'a bplustree \ 'a list" where
+ "leaves (Leaf ks) = ks" |
+ "leaves (Node ts t) = concat (map leaves (subtrees ts)) @ leaves t"
+
+abbreviation "leaves_list ts \ concat (map leaves (subtrees ts))"
+
+fun leaf_nodes where
+"leaf_nodes (Leaf xs) = [Leaf xs]" |
+"leaf_nodes (Node ts t) = concat (map leaf_nodes (subtrees ts)) @ leaf_nodes t"
+
+abbreviation "leaf_nodes_list ts \ concat (map leaf_nodes (subtrees ts))"
+
+
+
+text "And the elems view contains all elements of the tree"
+(* NOTE this doesn't help *)
+
+fun elems :: "'a bplustree \ 'a list" where
+ "elems (Leaf ks) = ks" |
+ "elems (Node ts t) = concat (map (\ (sub, sep). elems sub @ [sep]) ts) @ elems t"
+
+abbreviation "elems_list ts \ concat (map (\ (sub, sep). elems sub @ [sep]) ts)"
+
+(* this abbreviation makes handling the list much nicer *)
+thm leaves.simps
+thm inorder.simps
+thm elems.simps
+
+value "leaves (Node [(Leaf [], (0::nat)), (Node [(Leaf [], 1), (Leaf [], 10)] (Leaf []), 12), ((Leaf []), 30), ((Leaf []), 100)] (Leaf []))"
+
+subsection "Height and Balancedness"
+
+class height =
+ fixes height :: "'a \ nat"
+
+instantiation bplustree :: (type) height
+begin
+
+fun height_bplustree :: "'a bplustree \ nat" where
+ "height (Leaf ks) = 0" |
+ "height (Node ts t) = Suc (Max (height ` (set (subtrees ts@[t]))))"
+
+instance ..
+
+end
+
+text "Balancedness is defined is close accordance to the definition by Ernst"
+
+fun bal:: "'a bplustree \ bool" where
+ "bal (Leaf ks) = True" |
+ "bal (Node ts t) = (
+ (\sub \ set (subtrees ts). height sub = height t) \
+ (\sub \ set (subtrees ts). bal sub) \ bal t
+ )"
+
+
+value "height (Node [(Leaf [], (0::nat)), (Node [(Leaf [], 1), (Leaf [], 10)] (Leaf []), 12), ((Leaf []), 30), ((Leaf []), 100)] (Leaf []))"
+value "bal (Node [(Leaf [], (0::nat)), (Node [(Leaf [], 1), (Leaf [], 10)] (Leaf []), 12), ((Leaf []), 30), ((Leaf []), 100)] (Leaf []))"
+
+
+subsection "Order"
+
+text "The order of a B-tree is defined just as in the original paper by Bayer."
+
+(* alt1: following knuths definition to allow for any
+ natural number as order and resolve ambiguity *)
+(* alt2: use range [k,2*k] allowing for valid bplustrees
+ from k=1 onwards NOTE this is what I ended up implementing *)
+
+fun order:: "nat \ 'a bplustree \ bool" where
+ "order k (Leaf ks) = ((length ks \ k) \ (length ks \ 2*k))" |
+ "order k (Node ts t) = (
+ (length ts \ k) \
+ (length ts \ 2*k) \
+ (\sub \ set (subtrees ts). order k sub) \ order k t
+)"
+
+text \The special condition for the root is called \textit{root\_order}\
+
+(* the invariant for the root of the bplustree *)
+fun root_order:: "nat \ 'a bplustree \ bool" where
+ "root_order k (Leaf ks) = (length ks \ 2*k)" |
+ "root_order k (Node ts t) = (
+ (length ts > 0) \
+ (length ts \ 2*k) \
+ (\s \ set (subtrees ts). order k s) \ order k t
+)"
+
+
+subsection "Auxiliary Lemmas"
+
+(* auxiliary lemmas when handling sets *)
+lemma separators_split:
+ "set (separators (l@(a,b)#r)) = set (separators l) \ set (separators r) \ {b}"
+ by simp
+
+lemma subtrees_split:
+ "set (subtrees (l@(a,b)#r)) = set (subtrees l) \ set (subtrees r) \ {a}"
+ by simp
+
+(* height and set lemmas *)
+
+
+lemma finite_set_ins_swap:
+ assumes "finite A"
+ shows "max a (Max (Set.insert b A)) = max b (Max (Set.insert a A))"
+ using Max_insert assms max.commute max.left_commute by fastforce
+
+lemma finite_set_in_idem:
+ assumes "finite A"
+ shows "max a (Max (Set.insert a A)) = Max (Set.insert a A)"
+ using Max_insert assms max.commute max.left_commute by fastforce
+
+lemma height_Leaf: "height t = 0 \ (\ks. t = (Leaf ks))"
+ by (induction t) (auto)
+
+lemma height_bplustree_order:
+ "height (Node (ls@[a]) t) = height (Node (a#ls) t)"
+ by simp
+
+lemma height_bplustree_sub:
+ "height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
+ by simp
+
+lemma height_bplustree_last:
+ "height (Node ((sub,x)#ts) t) = max (height (Node ts sub)) (Suc (height t))"
+ by (induction ts) auto
+
+
+lemma set_leaves_leaves: "set (leaves t) = set_leaves t"
+ apply(induction t)
+ apply(auto)
+ done
+
+lemma set_nodes_nodes: "set (inorder t) = set_nodes t"
+ apply(induction t)
+ apply(auto simp add: rev_image_eqI)
+ done
+
+
+lemma child_subset_leaves: "p \ set t \ set_leaves (fst p) \ set_leaves (Node t n)"
+ apply(induction p arbitrary: t n)
+ apply(auto)
+ done
+
+lemma child_subset: "p \ set t \ set_nodes (fst p) \ set_nodes (Node t n)"
+ apply(induction p arbitrary: t n)
+ apply(auto)
+ done
+
+lemma some_child_sub:
+ assumes "(sub,sep) \ set t"
+ shows "sub \ set (subtrees t)"
+ and "sep \ set (separators t)"
+ using assms by force+
+
+(* balancedness lemmas *)
+
+
+lemma bal_all_subtrees_equal: "bal (Node ts t) \ (\s1 \ set (subtrees ts). \s2 \ set (subtrees ts). height s1 = height s2)"
+ by (metis BPlusTree.bal.simps(2))
+
+
+lemma fold_max_set: "\x \ set t. x = f \ fold max t f = f"
+ apply(induction t)
+ apply(auto simp add: max_def_raw)
+ done
+
+lemma height_bal_tree: "bal (Node ts t) \ height (Node ts t) = Suc (height t)"
+ by (induction ts) auto
+
+
+
+lemma bal_split_last:
+ assumes "bal (Node (ls@(sub,sep)#rs) t)"
+ shows "bal (Node (ls@rs) t)"
+ and "height (Node (ls@(sub,sep)#rs) t) = height (Node (ls@rs) t)"
+ using assms by auto
+
+
+lemma bal_split_right:
+ assumes "bal (Node (ls@rs) t)"
+ shows "bal (Node rs t)"
+ and "height (Node rs t) = height (Node (ls@rs) t)"
+ using assms by (auto simp add: image_constant_conv)
+
+lemma bal_split_left:
+ assumes "bal (Node (ls@(a,b)#rs) t)"
+ shows "bal (Node ls a)"
+ and "height (Node ls a) = height (Node (ls@(a,b)#rs) t)"
+ using assms by (auto simp add: image_constant_conv)
+
+
+lemma bal_substitute: "\bal (Node (ls@(a,b)#rs) t); height t = height c; bal c\ \ bal (Node (ls@(c,b)#rs) t)"
+ unfolding bal.simps
+ by auto
+
+lemma bal_substitute_subtree: "\bal (Node (ls@(a,b)#rs) t); height a = height c; bal c\ \ bal (Node (ls@(c,b)#rs) t)"
+ using bal_substitute
+ by auto
+
+lemma bal_substitute_separator: "bal (Node (ls@(a,b)#rs) t) \ bal (Node (ls@(a,c)#rs) t)"
+ unfolding bal.simps
+ by auto
+
+(* order lemmas *)
+
+lemma order_impl_root_order: "\k > 0; order k t\ \ root_order k t"
+ apply(cases t)
+ apply(auto)
+ done
+
+
+(* sorted leaves implies that some sublists are sorted. This can be followed directly *)
+
+lemma sorted_inorder_list_separators: "sorted_less (inorder_list ts) \ sorted_less (separators ts)"
+ apply(induction ts)
+ apply (auto simp add: sorted_lems)
+ done
+
+corollary sorted_inorder_separators: "sorted_less (inorder (Node ts t)) \ sorted_less (separators ts)"
+ using sorted_inorder_list_separators sorted_wrt_append
+ by auto
+
+
+lemma sorted_inorder_list_subtrees:
+ "sorted_less (inorder_list ts) \ \ sub \ set (subtrees ts). sorted_less (inorder sub)"
+ apply(induction ts)
+ apply (auto simp add: sorted_lems)+
+ done
+
+corollary sorted_inorder_subtrees: "sorted_less (inorder (Node ts t)) \ \ sub \ set (subtrees ts). sorted_less (inorder sub)"
+ using sorted_inorder_list_subtrees sorted_wrt_append by auto
+
+lemma sorted_inorder_list_induct_subtree:
+ "sorted_less (inorder_list (ls@(sub,sep)#rs)) \ sorted_less (inorder sub)"
+ by (simp add: sorted_wrt_append)
+
+corollary sorted_inorder_induct_subtree:
+ "sorted_less (inorder (Node (ls@(sub,sep)#rs) t)) \ sorted_less (inorder sub)"
+ by (simp add: sorted_wrt_append)
+
+lemma sorted_inorder_induct_last: "sorted_less (inorder (Node ts t)) \ sorted_less (inorder t)"
+ by (simp add: sorted_wrt_append)
+
+
+lemma sorted_leaves_list_subtrees:
+ "sorted_less (leaves_list ts) \ \ sub \ set (subtrees ts). sorted_less (leaves sub)"
+ apply(induction ts)
+ apply (auto simp add: sorted_wrt_append)+
+ done
+
+corollary sorted_leaves_subtrees: "sorted_less (leaves (Node ts t)) \ \ sub \ set (subtrees ts). sorted_less (leaves sub)"
+ using sorted_leaves_list_subtrees sorted_wrt_append by auto
+
+lemma sorted_leaves_list_induct_subtree:
+ "sorted_less (leaves_list (ls@(sub,sep)#rs)) \ sorted_less (leaves sub)"
+ by (simp add: sorted_wrt_append)
+
+corollary sorted_leaves_induct_subtree:
+ "sorted_less (leaves (Node (ls@(sub,sep)#rs) t)) \ sorted_less (leaves sub)"
+ by (simp add: sorted_wrt_append)
+
+lemma sorted_leaves_induct_last: "sorted_less (leaves (Node ts t)) \ sorted_less (leaves t)"
+ by (simp add: sorted_wrt_append)
+
+text "Additional lemmas on the sortedness of the whole tree, which is
+correct alignment of navigation structure and leave data"
+
+fun inbetween where
+"inbetween f l Nil t u = f l t u" |
+"inbetween f l ((sub,sep)#xs) t u = (f l sub sep \ inbetween f sep xs t u)"
+
+thm fold_cong
+
+lemma cong_inbetween[fundef_cong]: "
+\a = b; xs = ys; \l' u' sub sep. (sub,sep) \ set ys \ f l' sub u' = g l' sub u'; \l' u'. f l' a u' = g l' b u'\
+ \ inbetween f l xs a u = inbetween g l ys b u"
+ apply(induction ys arbitrary: l a b u xs)
+ apply auto
+ apply fastforce+
+ done
+
+(* adding l < u makes sorted_less inorder not necessary anymore *)
+fun aligned :: "'a ::linorder \ _" where
+"aligned l (Leaf ks) u = (l < u \ (\x \ set ks. l < x \ x \ u))" |
+"aligned l (Node ts t) u = (inbetween aligned l ts t u)"
+
+lemma sorted_less_merge: "sorted_less (as@[a]) \ sorted_less (a#bs) \ sorted_less (as@a#bs)"
+ using sorted_mid_iff by blast
+
+
+thm aligned.simps
+
+lemma leaves_cases: "x \ set (leaves (Node ts t)) \ (\(sub,sep) \ set ts. x \ set (leaves sub)) \ x \ set (leaves t)"
+ apply (induction ts)
+ apply auto
+ done
+
+lemma align_sub: "aligned l (Node ts t) u \ (sub,sep) \ set ts \ \l' \ set (separators ts) \ {l}. aligned l' sub sep"
+ apply(induction ts arbitrary: l)
+ apply auto
+ done
+
+lemma align_last: "aligned l (Node (ts@[(sub,sep)]) t) u \ aligned sep t u"
+ apply(induction ts arbitrary: l)
+ apply auto
+ done
+
+lemma align_last': "aligned l (Node ts t) u \ \l' \ set (separators ts) \ {l}. aligned l' t u"
+ apply(induction ts arbitrary: l)
+ apply auto
+ done
+
+lemma aligned_sorted_inorder: "aligned l t u \ sorted_less (l#(inorder t)@[u])"
+proof(induction l t u rule: aligned.induct)
+ case (2 l ts t u)
+ then show ?case
+ proof(cases ts)
+ case Nil
+ then show ?thesis
+ using 2 by auto
+ next
+ case Cons
+ then obtain ts' sub sep where ts_split: "ts = ts'@[(sub,sep)]"
+ by (metis list.distinct(1) rev_exhaust surj_pair)
+ moreover from 2 have "sorted_less (l#(inorder_list ts))"
+ proof (induction ts arbitrary: l)
+ case (Cons a ts')
+ then show ?case
+ proof (cases a)
+ case (Pair sub sep)
+ then have "aligned l sub sep" "inbetween aligned sep ts' t u"
+ using "Cons.prems" by simp+
+ then have "aligned sep (Node ts' t) u"
+ by simp
+ then have "sorted_less (sep#inorder_list ts')"
+ using Cons
+ by (metis insert_iff list.set(2))
+ moreover have "sorted_less (l#inorder sub@[sep])"
+ using Cons
+ by (metis Pair \aligned l sub sep\ list.set_intros(1))
+ ultimately show ?thesis
+ using Pair sorted_less_merge[of "l#inorder sub" sep "inorder_list ts'"]
+ by simp
+ qed
+ qed simp
+ moreover have "sorted_less (sep#inorder t@[u])"
+ proof -
+ from 2 have "aligned sep t u"
+ using align_last ts_split by blast
+ then show ?thesis
+ using "2.IH" by blast
+ qed
+ ultimately show ?thesis
+ using sorted_less_merge[of "l#inorder_list ts'@inorder sub" sep "inorder t@[u]"]
+ by simp
+ qed
+qed simp
+
+lemma separators_in_inorder_list: "set (separators ts) \ set (inorder_list ts)"
+ apply (induction ts)
+ apply auto
+ done
+
+lemma separators_in_inorder: "set (separators ts) \ set (inorder (Node ts t))"
+ by fastforce
+
+lemma aligned_sorted_separators: "aligned l (Node ts t) u \ sorted_less (l#(separators ts)@[u])"
+ by (smt (verit, ccfv_threshold) aligned_sorted_inorder separators_in_inorder sorted_inorder_separators sorted_lems(2) sorted_wrt.simps(2) sorted_wrt_append subset_eq)
+
+lemma aligned_leaves_inbetween: "aligned l t u \ \x \ set (leaves t). l < x \ x \ u"
+proof (induction l t u rule: aligned.induct)
+ case (1 l ks u)
+ then show ?case by auto
+next
+ case (2 l ts t u)
+ have *: "sorted_less (l#inorder (Node ts t)@[u])"
+ using "2.prems" aligned_sorted_inorder by blast
+ show ?case
+ proof
+ fix x assume "x \ set (leaves (Node ts t))"
+ then consider (sub) "\(sub,sep) \ set ts. x \ set (leaves sub)" | (last) "x \ set (leaves t)"
+ by fastforce
+ then show "l < x \ x \ u"
+ proof (cases)
+ case sub
+ then obtain sub sep where "(sub,sep) \ set ts" "x \ set (leaves sub)" by auto
+ then obtain l' where "aligned l' sub sep" "l' \ set (separators ts) \ {l}"
+ using "2.prems"(1) \(sub, sep) \ set ts\ align_sub by blast
+ then have "\x \ set (leaves sub). l' < x \ x \ sep"
+ using "2.IH"(1) \(sub,sep) \ set ts\ by auto
+ moreover from * have "l \ l'"
+ by (metis Un_insert_right \l' \ set (separators ts) \ {l}\ append_Cons boolean_algebra_cancel.sup0 dual_order.eq_iff insert_iff less_imp_le separators_in_inorder sorted_snoc sorted_wrt.simps(2) subset_eq)
+ moreover from * have "sep \