# Theory BTree

theory BTree
imports Main "HOL-Data_Structures.Sorted_Less" "HOL-Data_Structures.Cmp"
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-Tree"

subsection "Datatype definition"

text "B-trees can be considered to have all data stored interleaved
as child nodes and separating elements (also keys or indices).
We define them to either be a Node that holds a list of pairs of children
and indices or be a completely empty Leaf."

datatype 'a btree = Leaf | Node "('a btree * 'a) list" "'a btree"

type_synonym 'a btree_list =  "('a btree * 'a) list"
type_synonym 'a btree_pair =  "('a btree * '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-tree elements is defined automatically."

thm btree.set
value "set_btree (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"

text "The inorder view is defined with the help of the concat function."

fun inorder :: "'a btree ⇒ 'a list" where
"inorder Leaf = []" |
"inorder (Node ts t) = concat (map (λ (sub, sep). inorder sub @ [sep]) ts) @ inorder t"

abbreviation "inorder_pair  ≡ λ(sub,sep). inorder sub @ [sep]"
abbreviation "inorder_list ts ≡ concat (map inorder_pair ts)"

(* this abbreviation makes handling the list much nicer *)
thm inorder.simps

value "inorder (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 btree :: (type) height
begin

fun height_btree :: "'a btree ⇒ nat" where
"height Leaf = 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 btree ⇒ bool" where
"bal Leaf = 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)"

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 btrees
from k=1 onwards NOTE this is what I ended up implementing *)

fun order:: "nat ⇒ 'a btree ⇒ bool" where
"order k Leaf = True" |
"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 btree *)
fun root_order:: "nat ⇒ 'a btree ⇒ bool" where
"root_order k Leaf = True" |
"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 ⟷ t = Leaf"
by (induction t) (auto)

lemma height_btree_order:
"height (Node (ls@[a]) t) = height (Node (a#ls) t)"
by simp

lemma height_btree_sub:
"height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
by simp

lemma height_btree_last:
"height (Node ((sub,x)#ts) t) = max (height (Node ts sub)) (Suc (height t))"
by (induction ts) auto

lemma set_btree_inorder: "set (inorder t) = set_btree t"
apply(induction t)
apply(auto)
done

lemma child_subset: "p ∈ set t ⟹ set_btree (fst p) ⊆ set_btree (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 BTree.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 inorder 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)

end

# Theory BTree_Height

theory BTree_Height
imports BTree
begin

section "Maximum and minimum height"

text "Textbooks usually provide some proofs relating the maxmimum and minimum height of the BTree
for a given number of nodes. We therefore introduce this counting and show the respective proofs."

subsection "Definition of node/size"

thm BTree.btree.size
(* the automatically derived size is a bit weird for our purposes *)
value "size (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"

text "The default size function does not suit our needs as it regards the length of the list in each node.
We would like to count the number of nodes in the tree only, not regarding the number of keys."

(* we want a different counting method,
namely only the number of nodes in a tree *)

(* TODO what if we count Leafs as nodes? *)

fun nodes::"'a btree ⇒ nat" where
"nodes Leaf = 0" |
"nodes (Node ts t) = 1 + (∑t←subtrees ts. nodes t) + (nodes t)"

value "nodes (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"

(* maximum number of nodes for given height *)
subsection "Maximum number of nodes for a given height"

lemma sum_list_replicate: "sum_list (replicate n c) = n*c"
apply(induction n)
apply(auto simp add: ring_class.ring_distribs(2))
done

abbreviation "bound k h ≡ ((k+1)^h - 1)"

lemma nodes_height_upper_bound:
"⟦order k t; bal t⟧ ⟹ nodes t * (2*k) ≤ bound (2*k) (height t)"
proof(induction t rule: nodes.induct)
case (2 ts t)
let ?sub_height = "((2 * k + 1) ^ height t - 1)"
have "sum_list (map nodes (subtrees ts)) * (2*k) =
sum_list (map (λt. nodes t * (2 * k)) (subtrees ts))"
using sum_list_mult_const by metis
also have "… ≤ sum_list (map (λx.?sub_height) (subtrees ts))"
using 2
using sum_list_mono[of "subtrees ts" "λt. nodes t * (2 * k)" "λx. bound (2 * k) (height t)"]
by (metis bal.simps(2) order.simps(2))
also have "… = sum_list (replicate (length ts) ?sub_height)"
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "… = (length ts)*(?sub_height)"
using sum_list_replicate by simp
also have "… ≤ (2*k)*(?sub_height)"
using "2.prems"(1)
by simp
finally have "sum_list (map nodes (subtrees ts))*(2*k) ≤ ?sub_height*(2*k)"
by simp
moreover have "(nodes t)*(2*k) ≤ ?sub_height"
using 2 by simp
ultimately have "(nodes (Node ts t))*(2*k) ≤
2*k
+ ?sub_height * (2*k)
+ ?sub_height"
unfolding nodes.simps add_mult_distrib
by linarith
also have "… =  2*k + (2*k)*((2 * k + 1) ^ height t) - 2*k + (2 * k + 1) ^ height t - 1"
by (simp add: diff_mult_distrib2 mult.assoc mult.commute)
also have "… = (2*k)*((2 * k + 1) ^ height t) + (2 * k + 1) ^ height t - 1"
by simp
also have "… = (2*k+1)^(Suc(height t)) - 1"
by simp
finally show ?case
by (metis "2.prems"(2) height_bal_tree)
qed simp

text "To verify our lower bound is sharp, we compare it to the height of artificially constructed
full trees."

fun full_node::"nat ⇒ 'a ⇒ nat ⇒ 'a btree" where
"full_node k c 0 = Leaf"|
"full_node k c (Suc n) = (Node (replicate (2*k) ((full_node k c n),c)) (full_node k c n))"

value "let k = (2::nat) in map (λx. nodes x * 2*k) (map (full_node k (1::nat)) [0,1,2,3,4])"
value "let k = (2::nat) in map (λx. ((2*k+(1::nat))^(x)-1)) [0,1,2,3,4]"

lemma compow_comp_id: "c > 0 ⟹ f ∘ f = f ⟹ (f ^^ c) = f"
apply(induction c)
apply auto
by fastforce

(* required only for the fold definition of height *)
lemma compow_id_point: "f x = x ⟹ (f ^^ c) x = x"
apply(induction c)
apply auto
done

lemma height_full_node: "height (full_node k a h) = h"
apply(induction k a h rule: full_node.induct)
apply (auto simp add: set_replicate_conv_if)
done

lemma bal_full_node: "bal (full_node k a h)"
apply(induction k a h rule: full_node.induct)
apply auto
done

lemma order_full_node: "order k (full_node k a h)"
apply(induction k a h rule: full_node.induct)
apply auto
done

lemma full_btrees_sharp: "nodes (full_node k a h) * (2*k) = bound (2*k) h"
apply(induction k a h rule: full_node.induct)
apply (auto simp add: height_full_node algebra_simps sum_list_replicate)
done

lemma upper_bound_sharp_node:
"t = full_node k a h ⟹ height t = h ∧ order k t ∧ bal t ∧ bound (2*k) h = nodes t * (2*k)"
by (simp add: bal_full_node height_full_node order_full_node full_btrees_sharp)

(* maximum number of nodes *)
subsection "Maximum height for a given number of nodes"

lemma nodes_height_lower_bound:
"⟦order k t; bal t⟧ ⟹ bound k (height t) ≤ nodes t * k"
proof(induction t rule: nodes.induct)
case (2 ts t)
let ?sub_height = "((k + 1) ^ height t - 1)"
have "k*(?sub_height) ≤ (length ts)*(?sub_height)"
using "2.prems"(1)
by simp
also have "… = sum_list (replicate (length ts) ?sub_height)"
using sum_list_replicate by simp
also have "… = sum_list (map (λx.?sub_height) (subtrees ts))"
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "… ≤ sum_list (map (λt. nodes t * k) (subtrees ts))"
using 2
using sum_list_mono[of "subtrees ts" "λx. bound k (height t)" "λt. nodes t * k"]
by (metis bal.simps(2) order.simps(2))
also have "… = sum_list (map nodes (subtrees ts)) * k"
using sum_list_mult_const[of nodes k "subtrees ts"] by auto
finally have "sum_list (map nodes (subtrees ts))*k ≥ ?sub_height*k"
by simp
moreover have "(nodes t)*k ≥ ?sub_height"
using 2 by simp
ultimately have "(nodes (Node ts t))*k ≥
k
+ ?sub_height * k
+ ?sub_height"
unfolding nodes.simps add_mult_distrib
by linarith
also have
"k + ?sub_height * k + ?sub_height =
k + k*((k + 1) ^ height t) - k + (k + 1) ^ height t - 1"
by (simp add: diff_mult_distrib2 mult.assoc mult.commute)
also have "… = k*((k + 1) ^ height t) + (k + 1) ^ height t - 1"
by simp
also have "… = (k+1)^(Suc(height t)) - 1"
by simp
finally show ?case
by (metis "2.prems"(2) height_bal_tree)
qed simp

text "To verify our upper bound is sharp, we compare it to the height of artificially constructed
minimally filled (=slim) trees."

fun slim_node::"nat ⇒ 'a ⇒ nat ⇒ 'a btree" where
"slim_node k c 0 = Leaf"|
"slim_node k c (Suc n) = (Node (replicate k ((slim_node k c n),c)) (slim_node k c n))"

value "let k = (2::nat) in map (λx. nodes x * k) (map (slim_node k (1::nat)) [0,1,2,3,4])"
value "let k = (2::nat) in map (λx. ((k+1::nat)^(x)-1)) [0,1,2,3,4]"

lemma height_slim_node: "height (slim_node k a h) = h"
apply(induction k a h rule: full_node.induct)
apply (auto simp add: set_replicate_conv_if)
done

lemma bal_slim_node: "bal (slim_node k a h)"
apply(induction k a h rule: full_node.induct)
apply auto
done

lemma order_slim_node: "order k (slim_node k a h)"
apply(induction k a h rule: full_node.induct)
apply auto
done

lemma slim_nodes_sharp: "nodes (slim_node k a h) * k = bound k h"
apply(induction k a h rule: slim_node.induct)
apply (auto simp add: height_slim_node algebra_simps sum_list_replicate compow_id_point)
done

lemma lower_bound_sharp_node:
"t = slim_node k a h ⟹ height t = h ∧ order k t ∧ bal t ∧ bound k h = nodes t * k"
by (simp add: bal_slim_node height_slim_node order_slim_node slim_nodes_sharp)

(* TODO results for root_order/bal *)
text "Since BTrees have special roots, we need to show the overall nodes seperately"

lemma nodes_root_height_lower_bound:
assumes "root_order k t"
and "bal t"
shows "2*((k+1)^(height t - 1) - 1) + (of_bool (t ≠ Leaf))*k  ≤ nodes t * k"
proof (cases t)
case (Node ts t)
let ?sub_height = "((k + 1) ^ height t - 1)"
from Node have "?sub_height ≤ length ts * ?sub_height"
using assms
by (simp add: Suc_leI)
also have "… = sum_list (replicate (length ts) ?sub_height)"
using sum_list_replicate
by simp
also have "… = sum_list (map (λx. ?sub_height) (subtrees ts))"
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "… ≤ sum_list (map (λt. nodes t * k) (subtrees ts))"
using Node
sum_list_mono[of "subtrees ts" "λx. (k+1)^(height t) - 1" "λx. nodes x * k"]
nodes_height_lower_bound assms
by fastforce
also have "… = sum_list (map nodes (subtrees ts)) * k"
using sum_list_mult_const[of nodes k "subtrees ts"] by simp
finally have "sum_list (map nodes (subtrees ts))*k ≥ ?sub_height"
by simp

moreover have "(nodes t)*k ≥ ?sub_height"
using Node assms nodes_height_lower_bound
by auto
ultimately have "(nodes (Node ts t))*k ≥
?sub_height
+ ?sub_height + k"
unfolding nodes.simps add_mult_distrib
by linarith
then show ?thesis
using Node assms(2) height_bal_tree by fastforce
qed simp

lemma nodes_root_height_upper_bound:
assumes "root_order k t"
and "bal t"
shows "nodes t * (2*k) ≤ (2*k+1)^(height t) - 1"
proof(cases t)
case (Node ts t)
let ?sub_height = "((2 * k + 1) ^ height t - 1)"
have "sum_list (map nodes (subtrees ts)) * (2*k) =
sum_list (map (λt. nodes t * (2 * k)) (subtrees ts))"
using sum_list_mult_const by metis
also have "… ≤ sum_list (map (λx.?sub_height) (subtrees ts))"
using Node
sum_list_mono[of "subtrees ts" "λx. nodes x * (2*k)"  "λx. (2*k+1)^(height t) - 1"]
nodes_height_upper_bound assms
by fastforce
also have "… = sum_list (replicate (length ts) ?sub_height)"
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "… = (length ts)*(?sub_height)"
using sum_list_replicate by simp
also have "… ≤ (2*k)*?sub_height"
using assms Node
by simp
finally have "sum_list (map nodes (subtrees ts))*(2*k) ≤ ?sub_height*(2*k)"
by simp
moreover have "(nodes t)*(2*k) ≤ ?sub_height"
using Node assms nodes_height_upper_bound
by auto
ultimately have "(nodes (Node ts t))*(2*k) ≤
2*k
+ ?sub_height * (2*k)
+ ?sub_height"
unfolding nodes.simps add_mult_distrib
by linarith
also have "… =  2*k + (2*k)*((2 * k + 1) ^ height t) - 2*k + (2 * k + 1) ^ height t - 1"
by (simp add: diff_mult_distrib2 mult.assoc mult.commute)
also have "… = (2*k)*((2 * k + 1) ^ height t) + (2 * k + 1) ^ height t - 1"
by simp
also have "… = (2*k+1)^(Suc(height t)) - 1"
by simp
finally show ?thesis
by (metis Node assms(2) height_bal_tree)
qed simp

lemma root_order_imp_divmuleq: "root_order k t ⟹ (nodes t * k) div k = nodes t"
using root_order.elims(2) by fastforce

lemma nodes_root_height_lower_bound_simp:
assumes "root_order k t"
and "bal t"
and "k > 0"
shows "(2*((k+1)^(height t - 1) - 1)) div k + (of_bool (t ≠ Leaf)) ≤ nodes t"
proof (cases t)
case Node
have "(2*((k+1)^(height t - 1) - 1)) div k + (of_bool (t ≠ Leaf)) =
(2*((k+1)^(height t - 1) - 1) + (of_bool (t ≠ Leaf))*k) div k"
using Node assms
using div_plus_div_distrib_dvd_left[of k k "(2 * Suc k ^ (height t - Suc 0) - Suc (Suc 0))"]
by (auto simp add: algebra_simps simp del: height_btree.simps)
also have "… ≤ (nodes t * k) div k"
using nodes_root_height_lower_bound[OF assms(1,2)] div_le_mono
by blast
also have "… = nodes t"
using root_order_imp_divmuleq[OF assms(1)]
by simp
finally show ?thesis .
qed simp

lemma nodes_root_height_upper_bound_simp:
assumes "root_order k t"
and "bal t"
shows "nodes t ≤ ((2*k+1)^(height t) - 1) div (2*k)"
proof -
have "nodes t = (nodes t * (2*k)) div (2*k)"
using root_order_imp_divmuleq[OF assms(1)]
by simp
also have "… ≤ ((2*k+1)^(height t) - 1) div (2*k)"
using div_le_mono nodes_root_height_upper_bound[OF assms] by blast
finally show ?thesis .
qed

definition "full_tree = full_node"

fun slim_tree where
"slim_tree k c 0 = Leaf" |
"slim_tree k c (Suc h) = Node [(slim_node k c h, c)] (slim_node k c h)"

lemma lower_bound_sharp:
"k > 0 ⟹ t = slim_tree k a h ⟹ height t = h ∧ root_order k t ∧ bal t ∧ nodes t * k = 2*((k+1)^(height t - 1) - 1) + (of_bool (t ≠ Leaf))*k"
apply (cases h)
using slim_nodes_sharp[of k a]
apply (auto simp add: algebra_simps bal_slim_node height_slim_node order_slim_node)
done

lemma upper_bound_sharp:
"k > 0 ⟹ t = full_tree k a h ⟹ height t = h ∧ root_order k t ∧ bal t ∧ ((2*k+1)^(height t) - 1) = nodes t * (2*k)"
unfolding full_tree_def
using order_impl_root_order[of k t]
by (simp add: bal_full_node height_full_node order_full_node full_btrees_sharp)

end

# 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, hide_lams) 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."

(* TODO what if we define a function "list_split" that returns
a split list for mapping arbitrary f (separators) and g (subtrees)
s.th. f :: 'a ⇒ ('b::linorder) and g :: 'a ⇒ 'a btree
this would allow for key,pointer pairs to be inserted into the tree *)
(* TODO what if the keys are the pointers? *)
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."

datatype 'b up⇩i = T⇩i "'b btree" | Up⇩i "'b btree" 'b "'b btree"

fun order_up⇩i where
"order_up⇩i k (T⇩i sub) = order k sub" |
"order_up⇩i k (Up⇩i l a r) = (order k l ∧ order k r)"

fun root_order_up⇩i where
"root_order_up⇩i k (T⇩i sub) = root_order k sub" |
"root_order_up⇩i k (Up⇩i l a r) = (order k l ∧ order k r)"

fun height_up⇩i where
"height_up⇩i (T⇩i t) = height t" |
"height_up⇩i (Up⇩i l a r) = max (height l) (height r)"

fun bal_up⇩i where
"bal_up⇩i (T⇩i t) = bal t" |
"bal_up⇩i (Up⇩i l a r) = (height l = height r ∧ bal l ∧ bal r)"

fun inorder_up⇩i where
"inorder_up⇩i (T⇩i t) = inorder t" |
"inorder_up⇩i (Up⇩i l a r) = inorder l @ [a] @ inorder r"

text "The following function merges two nodes and returns separately split nodes
if an overflow occurs"

fun node⇩i:: "nat ⇒ ('a btree × 'a) list ⇒ 'a btree ⇒ 'a up⇩i" where
"node⇩i k ts t = (
if length ts ≤ 2*k then T⇩i (Node ts t)
else (
case split_half ts of (ls, (sub,sep)#rs) ⇒
Up⇩i (Node ls sub) sep (Node rs t)
)
)"

fun ins:: "nat ⇒ 'a ⇒ 'a btree ⇒ 'a up⇩i" where
"ins k x Leaf = (Up⇩i Leaf x Leaf)" |
"ins k x (Node ts t) = (
case split ts x of
(ls,(sub,sep)#rs) ⇒
(if sep = x then
T⇩i (Node ts t)
else
(case ins k x sub of
Up⇩i l a r ⇒
node⇩i k (ls @ (l,a)#(r,sep)#rs) t |
T⇩i a ⇒
T⇩i (Node (ls @ (a,sep) # rs) t))) |
(ls, []) ⇒
(case ins k x t of
Up⇩i l a r ⇒
node⇩i k (ls@[(l,a)]) r |
T⇩i a ⇒
T⇩i (Node ls a)
)
)"

fun tree⇩i::"'a up⇩i ⇒ 'a btree" where
"tree⇩i (T⇩i sub) = sub" |
"tree⇩i (Up⇩i l a r) = (Node [(l,a)] r)"

fun insert::"nat ⇒ 'a ⇒ 'a btree ⇒ 'a btree" where
"insert k x t = tree⇩i (ins k x t)"

subsection "Deletion"

text "The following deletion method is inspired by Bayer (70) and Fielding (??).
Rather than stealing only a single node from the neighbour,
the neighbour is fully merged with the potentially underflowing node.
If the resulting node is still larger than allowed, the merged node is split
again, using the rules known from insertion splits.
If the resulting node has admissable size, it is simply kept in the tree."

fun rebalance_middle_tree where
"rebalance_middle_tree k ls Leaf sep rs Leaf = (
Node (ls@(Leaf,sep)#rs) Leaf
)" |
"rebalance_middle_tree k ls (Node mts mt) sep rs (Node tts tt) = (
if length mts ≥ k ∧ length tts ≥ k then
Node (ls@(Node mts mt,sep)#rs) (Node tts tt)
else (
case rs of [] ⇒ (
case node⇩i k (mts@(mt,sep)#tts) tt of
T⇩i u ⇒
Node ls u |
Up⇩i l a r ⇒
Node (ls@[(l,a)]) r) |
(Node rts rt,rsep)#rs ⇒ (
case node⇩i k (mts@(mt,sep)#rts) rt of
T⇩i u ⇒
Node (ls@(u,rsep)#rs) (Node tts tt) |
Up⇩i l a r ⇒
Node (ls@(l,a)#(r,rsep)#rs) (Node tts tt))
))"

text "Deletion"

text "All trees are merged with the right neighbour on underflow.
Obviously for the last tree this would not work since it has no right neighbour.
Therefore this tree, as the only exception, is merged with the left neighbour.
However since we it does not make a difference, we treat the situation
as if the second to last tree underflowed."

fun rebalance_last_tree where
"rebalance_last_tree k ts t = (
case last ts of (sub,sep) ⇒
rebalance_middle_tree k (butlast ts) sub sep [] t
)"

text "Rather than deleting the minimal key from the right subtree,
we remove the maximal key of the left subtree.
This is due to the fact that the last tree can easily be accessed
and the left neighbour is way easier to access than the right neighbour,
it resides in the same pair as the separating element to be removed."

fun split_max where
"split_max k (Node ts t) = (case t of Leaf ⇒ (
let (sub,sep) = last ts in
(Node (butlast ts) sub, sep)
)|
_ ⇒
case split_max k t of (sub, sep) ⇒
(rebalance_last_tree k ts sub, sep)
)"

fun del where
"del k x Leaf = Leaf" |
"del k x (Node ts t) = (
case split ts x of
(ls,[]) ⇒
rebalance_last_tree k ls (del k x t)
| (ls,(sub,sep)#rs) ⇒ (
if sep ≠ x then
rebalance_middle_tree k ls (del k x sub) sep rs t
else if sub = Leaf then
Node (ls@rs) t
else let (sub_s, max_s) = split_max k sub in
rebalance_middle_tree k ls sub_s max_s rs t
)
)"

fun reduce_root where
"reduce_root Leaf = Leaf" |
"reduce_root (Node ts t) = (case ts of
[] ⇒ t |
_ ⇒ (Node ts t)
)"

fun delete where "delete k x t = reduce_root (del k x t)"

text "An invariant for intermediate states at deletion.
In particular we allow for an underflow to 0 subtrees."

fun almost_order where
"almost_order k Leaf = True" |
"almost_order k (Node ts t) = (
(length ts ≤ 2*k) ∧
(∀s ∈ set (subtrees ts). order k s) ∧
order k t
)"

text "A recursive property of the \"spine\" we want to walk along for splitting
off the maximum of the left subtree."

fun nonempty_lasttreebal where
"nonempty_lasttreebal Leaf = True" |
"nonempty_lasttreebal (Node ts t) = (
(∃ls tsub tsep. ts = (ls@[(tsub,tsep)]) ∧ height tsub = height t) ∧
nonempty_lasttreebal t
)"

subsection "Proofs of functional correctness"

lemma split_set:
assumes "split ts z = (ls,(a,b)#rs)"
shows "(a,b) ∈ set ts"
and "(x,y) ∈ set ls ⟹ (x,y) ∈ set ts"
and "(x,y) ∈ set rs ⟹ (x,y) ∈ set ts"
and "set ls ∪ set rs ∪ {(a,b)} = set ts"
and "∃x ∈ set ts. b ∈ Basic_BNFs.snds x"
using split_conc assms by fastforce+

lemma split_length:
"split ts x = (ls, rs) ⟹ length ls + length rs = length ts"
by (auto dest: split_conc)

text "Isin proof"

thm isin_simps
(* copied from comment in List_Ins_Del *)
lemma sorted_ConsD: "sorted_less (y # xs) ⟹ x ≤ y ⟹ x ∉ set xs"
by (auto simp: sorted_Cons_iff)

lemma sorted_snocD: "sorted_less (xs @ [y]) ⟹ y ≤ x ⟹ x ∉ set xs"
by (auto simp: sorted_snoc_iff)

lemmas isin_simps2 = sorted_lems sorted_ConsD sorted_snocD
(*-----------------------------*)

lemma isin_sorted: "sorted_less (xs@a#ys) ⟹
(x ∈ set (xs@a#ys)) = (if x < a then x ∈ set xs else x ∈ set (a#ys))"
by (auto simp: isin_simps2)

(* lift to split *)

lemma isin_sorted_split:
assumes "sorted_less (inorder (Node ts t))"
and "split ts x = (ls, rs)"
shows "x ∈ set (inorder (Node ts t)) = (x ∈ set (inorder_list rs @ inorder t))"
proof (cases ls)
case Nil
then have "ts = rs"
using assms by (auto dest!: split_conc)
then show ?thesis by simp
next
case Cons
then obtain ls' sub sep where ls_tail_split: "ls = ls' @ [(sub,sep)]"
by (metis list.simps(3) rev_exhaust surj_pair)
then have "sep < x"
using split_req(2)[of ts x ls' sub sep rs]
using sorted_inorder_separators[OF assms(1)]
using assms
by simp
then show ?thesis
using assms(1) split_conc[OF assms(2)] ls_tail_split
using isin_sorted[of "inorder_list ls' @ inorder sub" sep "inorder_list rs @ inorder t" x]
by auto
qed

lemma isin_sorted_split_right:
assumes "split ts x = (ls, (sub,sep)#rs)"
and "sorted_less (inorder (Node ts t))"
and "sep ≠ x"
shows "x ∈ set (inorder_list ((sub,sep)#rs) @ inorder t) = (x ∈ set (inorder sub))"
proof -
from assms have "x < sep"
proof -
from assms have "sorted_less (separators ts)"
by (simp add: sorted_inorder_separators)
then show ?thesis
using split_req(3)
using assms
by fastforce
qed
moreover have "sorted_less (inorder_list ((sub,sep)#rs) @ inorder t)"
using assms sorted_wrt_append split_conc
by fastforce
ultimately show ?thesis
using isin_sorted[of "inorder sub" "sep" "inorder_list rs @ inorder t" x]
by simp
qed

theorem isin_set_inorder: "sorted_less (inorder t) ⟹ isin t x = (x ∈ set (inorder t))"
proof(induction t x rule: isin.induct)
case (2 ts t x)
then obtain ls rs where list_split: "split ts x = (ls, rs)"
by (meson surj_pair)
then have list_conc: "ts = ls @ rs"
using split_conc by auto
show ?case
proof (cases rs)
case Nil
then have "isin (Node ts t) x = isin t x"
by (simp add: list_split)
also have "… = (x ∈ set (inorder t))"
using "2.IH"(1) list_split Nil
using "2.prems" sorted_inorder_induct_last by auto
also have "… = (x ∈ set (inorder (Node ts t)))"
using isin_sorted_split[of ts t x ls rs]
using "2.prems" list_split list_conc Nil
by simp
finally show ?thesis .
next
case (Cons a list)
then obtain sub sep where a_split: "a = (sub,sep)"
by (cases a)
then show ?thesis
proof (cases "x = sep")
case True
then show ?thesis
using list_conc Cons a_split list_split
by auto
next
case False
then have "isin (Node ts t) x = isin sub x"
using list_split Cons a_split False
by auto
also have "… = (x ∈ set (inorder sub))"
using "2.IH"(2)
using "2.prems" False a_split list_conc list_split local.Cons sorted_inorder_induct_subtree by fastforce
also have "… = (x ∈ set (inorder (Node ts t)))"
using isin_sorted_split[OF "2.prems" list_split]
using isin_sorted_split_right "2.prems" list_split Cons a_split False
by simp
finally show ?thesis  .
qed
qed
qed auto

(* TODO way to use this for custom case distinction? *)
lemma node⇩i_cases: "length xs ≤ k ∨ (∃ls sub sep rs. split_half xs = (ls,(sub,sep)#rs))"
proof -
have "¬ length xs ≤ k ⟹ length xs ≥ 1"
by linarith
then show ?thesis
using split_half_not_empty
by blast
qed

lemma root_order_tree⇩i: "root_order_up⇩i (Suc k) t = root_order (Suc k) (tree⇩i t)"
apply (cases t)
apply auto
done

lemma node⇩i_root_order:
assumes "length ts > 0"
and "length ts ≤ 4*k+1"
and "∀x ∈ set (subtrees ts). order k x"
and "order k t"
shows "root_order_up⇩i k (node⇩i k ts t)"
proof (cases "length ts ≤ 2*k")
case True
then show ?thesis
using assms
by (simp add: node⇩i.simps)
next
case False
then obtain ls sub sep rs where split_half_ts:
"take (length ts div 2) ts = ls"
"drop (length ts div 2) ts = (sub,sep)#rs"
using split_half_not_empty[of ts]
by auto
then have length_rs: "length rs = length ts - (length ts div 2) - 1"
using length_drop
by (metis One_nat_def add_diff_cancel_right' list.size(4))
also have "… ≤ 4*k - ((4*k + 1) div 2)"
using assms(2) by simp
also have "… = 2*k"
by auto
finally have "length rs ≤ 2*k"
by simp
moreover have "length rs ≥ k"
using False length_rs by simp
moreover have "set ((sub,sep)#rs) ⊆ set ts"
by (metis split_half_ts(2) set_drop_subset)
ultimately have o_r: "order k sub" "order k (Node rs t)"
using split_half_ts assms by auto
moreover have "length ls ≥ k"
using length_take assms split_half_ts False
by auto
moreover have  "length ls ≤ 2*k"
using assms(2) split_half_ts
by auto
ultimately have o_l: "order k (Node ls sub)"
using set_take_subset assms split_half_ts
by fastforce
from o_r o_l show ?thesis
by (simp add: node⇩i.simps False split_half_ts)
qed

lemma node⇩i_order_helper:
assumes "length ts ≥ k"
and "length ts ≤ 4*k+1"
and "∀x ∈ set (subtrees ts). order k x"
and "order k t"
shows "case (node⇩i k ts t) of T⇩i t ⇒ order k t | _ ⇒ True"
proof (cases "length ts ≤ 2*k")
case True
then show ?thesis
using assms
by (simp add: node⇩i.simps)
next
case False
then obtain sub sep rs where
"drop (length ts div 2) ts = (sub,sep)#rs"
using split_half_not_empty[of ts]
by auto
then show ?thesis
using assms by (simp add: node⇩i.simps)
qed

lemma node⇩i_order:
assumes "length ts ≥ k"
and "length ts ≤ 4*k+1"
and "∀x ∈ set (subtrees ts). order k x"
and "order k t"
shows "order_up⇩i k (node⇩i k ts t)"

apply(cases "node⇩i k ts t")
using node⇩i_root_order node⇩i_order_helper assms apply fastforce
apply (metis node⇩i_root_order assms(2,3,4) le0 length_greater_0_conv
list.size(3) node⇩i.simps order_up⇩i.simps(2) root_order_up⇩i.simps(2) up⇩i.distinct(1))
done

(* explicit proof *)
lemma ins_order:
"order k t ⟹ order_up⇩i k (ins k x t)"
proof(induction k x t rule: ins.induct)
case (2 k x ts t)
then obtain ls rs where split_res: "split ts x = (ls, rs)"
by (meson surj_pair)
then have split_app: "ls@rs = ts"
using split_conc
by simp

show ?case
proof (cases rs)
case Nil
then have "order_up⇩i k (ins k x t)"
using 2 split_res
by simp
then show ?thesis
using Nil 2 split_app split_res Nil node⇩i_order
by (auto split!: up⇩i.splits simp del: node⇩i.simps)
next
case (Cons a list)
then obtain sub sep where a_prod: "a  = (sub, sep)"
by (cases a)
then show ?thesis
proof (cases "x = sep")
case True
then show ?thesis
using 2 a_prod Cons split_res
by simp
next
case False
then have "order_up⇩i k (ins k x sub)"
using "2.IH"(2) "2.prems" a_prod local.Cons split_app split_res by auto
then show ?thesis
using 2 split_app Cons length_append node⇩i_order a_prod split_res
by (auto split!: up⇩i.splits simp del: node⇩i.simps simp add: order_impl_root_order)
qed
qed
qed simp

(* notice this is almost a duplicate of ins_order *)
lemma ins_root_order:
assumes "root_order k t"
shows "root_order_up⇩i k (ins k x t)"
proof(cases t)
case (Node ts t)
then obtain ls rs where split_res: "split ts x = (ls, rs)"
by (meson surj_pair)
then have split_app: "ls@rs = ts"
using split_conc
by fastforce

show ?thesis
proof (cases rs)
case Nil
then have "order_up⇩i k (ins k x t)" using Node assms split_res
by (simp add: ins_order)
then show ?thesis
using Nil Node split_app split_res assms node⇩i_root_order
by (auto split!: up⇩i.splits simp del: node⇩i.simps simp add: order_impl_root_order)
next
case (Cons a list)
then obtain sub sep where a_prod: "a  = (sub, sep)"
by (cases a)
then show ?thesis
proof (cases "x = sep")
case True
then show ?thesis using assms Node a_prod Cons split_res
by simp
next
case False
then have "order_up⇩i k (ins k x sub)"
using Node a_prod assms ins_order local.Cons split_app by auto
then show ?thesis
using assms split_app Cons length_append Node node⇩i_root_order a_prod split_res
by (auto split!: up⇩i.splits simp del: node⇩i.simps simp add: order_impl_root_order)
qed
qed
qed simp

lemma height_list_split: "height_up⇩i (Up⇩i (Node ls a) b (Node rs t)) = height (Node (ls@(a,b)#rs) t) "
by (induction ls) (auto simp add: max.commute)

lemma node⇩i_height: "height_up⇩i (node⇩i k ts t) = height (Node ts t)"
proof(cases "length ts ≤ 2*k")
case False
then obtain ls sub sep rs where
split_half_ts: "split_half ts = (ls, (sub, sep) # rs)"
by (meson node⇩i_cases)
then have "node⇩i k ts t = Up⇩i (Node ls (sub)) sep (Node rs t)"
using False by simp
then show ?thesis
using split_half_ts
by (metis append_take_drop_id fst_conv height_list_split snd_conv split_half.elims)
qed simp

lemma bal_up⇩i_tree: "bal_up⇩i t = bal (tree⇩i t)"
apply(cases t)
apply auto
done

lemma bal_list_split: "bal (Node (ls@(a,b)#rs) t) ⟹ bal_up⇩i (Up⇩i (Node ls a) b (Node rs t))"
by (auto simp add: image_constant_conv)

lemma node⇩i_bal:
assumes "bal (Node ts t)"
shows "bal_up⇩i (node⇩i k ts t)"
using assms
proof(cases "length ts ≤ 2*k")
case False
then obtain ls sub sep rs where
split_half_ts: "split_half ts = (ls, (sub, sep) # rs)"
by (meson node⇩i_cases)
then have "bal (Node (ls@(sub,sep)#rs) t)"
using assms append_take_drop_id[where n="length ts div 2" and xs=ts]
by auto
then show ?thesis
using split_half_ts assms False
by (auto simp del: bal.simps bal_up⇩i.simps dest!: bal_list_split[of ls sub sep rs t])
qed simp

lemma height_up⇩i_merge: "height_up⇩i (Up⇩i l a r) = height t ⟹ height (Node (ls@(t,x)#rs) tt) = height (Node (ls@(l,a)#(r,x)#rs) tt)"
by simp

lemma ins_height: "height_up⇩i (ins k x t) = height t"
proof(induction k x t rule: ins.induct)
case (2 k x ts t)
then obtain ls rs where split_list: "split ts x = (ls,rs)"
by (meson surj_pair)
then have split_append: "ls@rs = ts"
using split_conc
by auto
then show ?case
proof (cases rs)
case Nil
then have height_sub: "height_up⇩i (ins k x t) = height t"
using 2 by (simp add: split_list)
then show ?thesis
proof (cases "ins k x t")
case (T⇩i a)
then have "height (Node ts t) = height (Node ts a)"
using height_sub
by simp
then show ?thesis
using T⇩i Nil split_list split_append
by simp
next
case (Up⇩i l a r)
then have "height (Node ls t) = height (Node (ls@[(l,a)]) r)"
using height_btree_order height_sub by (induction ls) auto
then show ?thesis using 2 Nil split_list Up⇩i split_append
by (simp del: node⇩i.simps add: node⇩i_height)
qed
next
case (Cons a list)
then obtain sub sep where a_split: "a = (sub,sep)"
by (cases a)
then show ?thesis
proof (cases "x = sep")
case True
then show ?thesis
using Cons a_split 2 split_list
by (simp del: height_btree.simps)
next
case False
then have height_sub: "height_up⇩i (ins k x sub) = height sub"
by (metis "2.IH"(2) a_split Cons split_list)
then show ?thesis
proof (cases "ins k x sub")
case (T⇩i a)
then have "height a = height sub"
using height_sub by auto
then have "height (Node (ls@(sub,sep)#rs) t) = height (Node (ls@(a,sep)#rs) t)"
by auto
then show ?thesis
using T⇩i height_sub False Cons 2 split_list a_split split_append
by (auto simp add: image_Un max.commute finite_set_ins_swap)
next
case (Up⇩i l a r)
then have "height (Node (ls@(sub,sep)#list) t) = height (Node (ls@(l,a)#(r,sep)#list) t)"
using height_up⇩i_merge height_sub
by fastforce
then show ?thesis
using Up⇩i False Cons 2 split_list a_split split_append
by (auto simp del: node⇩i.simps simp add: node⇩i_height image_Un max.commute finite_set_ins_swap)
qed
qed
qed
qed simp

(* the below proof is overly complicated as a number of lemmas regarding height are missing *)
lemma ins_bal: "bal t ⟹ bal_up⇩i (ins k x t)"
proof(induction k x t rule: ins.induct)
case (2 k x ts t)
then obtain ls rs where split_res: "split ts x = (ls, rs)"
by (meson surj_pair)
then have split_app: "ls@rs = ts"
using split_conc
by fastforce

show ?case
proof (cases rs)
case Nil
then show ?thesis
proof (cases "ins k x t")
case (T⇩i a)
then have "bal (Node ls a)" unfolding bal.simps
by (metis "2.IH"(1) "2.prems" append_Nil2 bal.simps(2) bal_up⇩i.simps(1) height_up⇩i.simps(1) ins_height local.Nil split_app split_res)
then show ?thesis
using Nil T⇩i 2 split_res
by simp
next
case (Up⇩i l a r)
then have
"(∀x∈set (subtrees (ls@[(l,a)])). bal x)"
"(∀x∈set (subtrees ls). height r = height x)"
using 2 Up⇩i Nil split_res split_app
by simp_all (metis height_up⇩i.simps(2) ins_height max_def)
then show ?thesis unfolding ins.simps
using Up⇩i Nil 2 split_res
by (simp del: node⇩i.simps add: node⇩i_bal)
qed
next
case (Cons a list)
then obtain sub sep where a_prod: "a  = (sub, sep)" by (cases a)
then show ?thesis
proof (cases "x = sep")
case True
then show ?thesis
using a_prod 2 split_res Cons by simp
next
case False
then have "bal_up⇩i (ins k x sub)" using 2 split_res
using a_prod local.Cons split_app by auto
show ?thesis
proof (cases "ins k x sub")
case (T⇩i x1)
then have  "height x1 = height t"
by (metis "2.prems" a_prod add_diff_cancel_left' bal_split_left(1) bal_split_left(2) height_bal_tree height_up⇩i.simps(1) ins_height local.Cons plus_1_eq_Suc split_app)
then show ?thesis
using split_app Cons T⇩i 2 split_res a_prod
by auto
next
case (Up⇩i l a r)
(* The only case where explicit reasoning is required - likely due to the insertion of 2 elements in the list *)
then have
"∀x ∈ set (subtrees (ls@(l,a)#(r,sep)#list)). bal x"
using Up⇩i split_app Cons 2 ‹bal_up⇩i (ins k x sub)› by auto
moreover have "∀x ∈ set (subtrees (ls@(l,a)#(r,sep)#list)). height x = height t"
using False Up⇩i split_app Cons 2 ‹bal_up⇩i (ins k x sub)› ins_height split_res a_prod
apply auto
by (metis height_up⇩i.simps(2) sup.idem sup_nat_def)
ultimately show ?thesis using Up⇩i Cons 2 split_res a_prod
by (simp del: node⇩i.simps add: node⇩i_bal)
qed
qed
qed
qed simp

(* ins acts as ins_list wrt inorder *)

(* "simple enough" to be automatically solved *)
lemma node⇩i_inorder: "inorder_up⇩i (node⇩i k ts t) = inorder (Node ts t)"
apply(cases "length ts ≤ 2*k")
apply (auto split!: list.splits)
(* we want to only transform in one direction here.. *)
supply R = sym[OF append_take_drop_id, of "map _ ts" "(length ts div 2)"]
thm R
apply(subst R)
apply (simp del: append_take_drop_id add: take_map drop_map)
done

corollary node⇩i_inorder_simps:
"node⇩i k ts t = T⇩i t' ⟹ inorder t' = inorder (Node ts t)"
"node⇩i k ts t = Up⇩i l a r ⟹ inorder l @ a # inorder r = inorder (Node ts t)"
apply (metis inorder_up⇩i.simps(1) node⇩i_inorder)
by (metis append_Cons inorder_up⇩i.simps(2) node⇩i_inorder self_append_conv2)

lemma ins_sorted_inorder: "sorted_less (inorder t) ⟹ (inorder_up⇩i (ins k (x::('a::linorder)) t)) = ins_list x (inorder t)"
apply(induction k x t rule: ins.induct)
using split_axioms apply (auto split!: prod.splits list.splits up⇩i.splits simp del: node⇩i.simps
simp add:  node⇩i_inorder node⇩i_inorder_simps)
(* from here on we prefer an explicit proof, showing how to apply the IH  *)
oops

(* specialize ins_list_sorted since it is cumbersome to express
"inorder_list ts" as "xs @ [a]" and always having to use the implicit properties of split*)

lemma ins_list_split:
assumes "split ts x = (ls, rs)"
and "sorted_less (inorder (Node ts t))"
shows "ins_list x (inorder (Node ts t)) = inorder_list ls @ ins_list x (inorder_list rs @ inorder t)"
proof (cases ls)
case Nil
then show ?thesis
using assms by (auto dest!: split_conc)
next
case Cons
then obtain ls' sub sep where ls_tail_split: "ls = ls' @ [(sub,sep)]"
by (metis list.distinct(1) rev_exhaust surj_pair)
moreover have "sep < x"
using split_req(2)[of ts x ls' sub sep rs]
using sorted_inorder_separators
using assms(1) assms(2) ls_tail_split
by auto
moreover have "sorted_less (inorder_list ls)"
using assms sorted_wrt_append split_conc by fastforce
ultimately show ?thesis using assms(2) split_conc[OF assms(1)]
using ins_list_sorted[of "inorder_list ls' @ inorder sub" sep]
by auto
qed

lemma ins_list_split_right_general:
assumes "split ts x = (ls, (sub,sep)#rs)"
and "sorted_less (inorder_list ts)"
and "sep ≠ x"
shows "ins_list x (inorder_list ((sub,sep)#rs) @ zs) = ins_list x (inorder sub) @ sep # inorder_list rs @ zs"
proof -
from assms have "x < sep"
proof -
from assms have "sorted_less (separators ts)"
by (simp add: sorted_inorder_list_separators)
then show ?thesis
using split_req(3)
using assms
by fastforce
qed
moreover have "sorted_less (inorder_pair (sub,sep))"
by (metis (no_types, lifting) assms(1) assms(2) concat.simps(2) concat_append list.simps(9) map_append sorted_wrt_append split_conc)
ultimately show ?thesis
using ins_list_sorted[of "inorder sub" "sep"]
by auto
qed

(* this fits the actual use cases better *)
corollary ins_list_split_right:
assumes "split ts x = (ls, (sub,sep)#rs)"
and "sorted_less (inorder (Node ts t))"
and "sep ≠ x"
shows "ins_list x (inorder_list ((sub,sep)#rs) @ inorder t) = ins_list x (inorder sub) @ sep # inorder_list rs @ inorder t"
using assms sorted_wrt_append split.ins_list_split_right_general split_axioms by fastforce

(* a simple lemma, missing from the standard as of now *)
lemma ins_list_idem_eq_isin: "sorted_less xs ⟹ x ∈ set xs ⟷ (ins_list x xs = xs)"
apply(induction xs)
apply auto
done

lemma ins_list_contains_idem: "⟦sorted_less xs; x ∈ set xs⟧ ⟹ (ins_list x xs = xs)"
using ins_list_idem_eq_isin by auto

declare node⇩i.simps [simp del]
declare node⇩i_inorder [simp add]

lemma ins_inorder: "sorted_less (inorder t) ⟹ (inorder_up⇩i (ins k x t)) = ins_list x (inorder t)"
proof(induction k x t rule: ins.induct)
case (1 k x)
then show ?case by auto
next
case (2 k x ts t)
then obtain ls rs where list_split: "split ts x = (ls,rs)"
by (cases "split ts x")
then have list_conc: "ts = ls@rs"
using split.split_conc split_axioms by blast
then show ?case
proof (cases rs)
case Nil
then show ?thesis
proof (cases "ins k x t")
case (T⇩i a)
then have IH:"inorder a = ins_list x (inorder t)"
using "2.IH"(1) "2.prems" list_split local.Nil sorted_inorder_induct_last
by auto

have "inorder_up⇩i (ins k x (Node ts t)) = inorder_list ls @ inorder a"
using list_split T⇩i Nil by (auto simp add: list_conc)
also have "… = inorder_list ls @ (ins_list x (inorder t))"
by (simp add: IH)
also have "… = ins_list x (inorder (Node ts t))"
using ins_list_split
using "2.prems" list_split Nil by auto
finally show ?thesis .
next
case (Up⇩i l a r)
then have IH:"inorder_up⇩i (Up⇩i l a r) = ins_list x (inorder t)"
using "2.IH"(1) "2.prems" list_split local.Nil sorted_inorder_induct_last by auto

have "inorder_up⇩i (ins k x (Node ts t)) = inorder_list ls @ inorder_up⇩i (Up⇩i l a r)"
using list_split Up⇩i Nil by (auto simp add: list_conc)
also have "… = inorder_list ls @ ins_list x (inorder t)"
using IH by simp
also have "… = ins_list x (inorder (Node ts t))"
using ins_list_split
using "2.prems" list_split local.Nil by auto
finally show ?thesis .
qed
next
case (Cons h list)
then obtain sub sep where h_split: "h = (sub,sep)"
by (cases h)

then have sorted_inorder_sub: "sorted_less (inorder sub)"
using "2.prems" list_conc local.Cons sorted_inorder_induct_subtree
by fastforce
then show ?thesis
proof(cases "x = sep")
case True
then have "x ∈ set (inorder (Node ts t))"
using list_conc h_split Cons by simp
then have "ins_list x (inorder (Node ts t)) = inorder (Node ts t)"
using "2.prems" ins_list_contains_idem by blast
also have "… = inorder_up⇩i (ins k x (Node ts t))"
using list_split h_split Cons True by auto
finally show ?thesis by simp
next
case False
then show ?thesis
proof (cases "ins k x sub")
case (T⇩i a)
then have IH:"inorder a = ins_list x (inorder sub)"
using "2.IH"(2) "2.prems" list_split Cons sorted_inorder_sub h_split False
by auto
have "inorder_up⇩i (ins k x (Node ts t)) = inorder_list ls @ inorder a @ sep # inorder_list list @ inorder t"
using h_split False list_split T⇩i Cons by simp
also have "… = inorder_list ls @ ins_list x (inorder sub) @ sep # inorder_list list @ inorder t"
using IH by simp
also have "… = ins_list x (inorder (Node ts t))"
using ins_list_split ins_list_split_right
using list_split "2.prems" Cons h_split False by auto
finally show ?thesis .
next
case (Up⇩i l a r)
then have IH:"inorder_up⇩i (Up⇩i l a r) = ins_list x (inorder sub)"
using "2.IH"(2) False h_split list_split local.Cons sorted_inorder_sub
by auto
have "inorder_up⇩i (ins k x (Node ts t)) = inorder_list ls @ inorder l @ a # inorder r  @ sep # inorder_list list @ inorder t"
using h_split False list_split Up⇩i Cons by simp
also have "… = inorder_list ls @ ins_list x (inorder sub) @ sep # inorder_list list @ inorder t"
using IH by simp
also have "… = ins_list x (inorder (Node ts t))"
using ins_list_split ins_list_split_right
using list_split "2.prems" Cons h_split False by auto
finally show ?thesis .
qed
qed
qed
qed

declare node⇩i.simps [simp add]
declare node⇩i_inorder [simp del]

thm ins.induct
thm btree.induct

(* wrapped up insert invariants *)

lemma tree⇩i_bal: "bal_up⇩i u ⟹ bal (tree⇩i u)"
apply(cases u)
apply(auto)
done

lemma tree⇩i_order: "⟦k > 0; root_order_up⇩i k u⟧ ⟹ root_order k (tree⇩i u)"
apply(cases u)
apply(auto simp add: order_impl_root_order)
done

lemma tree⇩i_inorder: "inorder_up⇩i u = inorder (tree⇩i u)"
apply (cases u)
apply auto
done

lemma insert_bal: "bal t ⟹ bal (insert k x t)"
using ins_bal
by (simp add: tree⇩i_bal)

lemma insert_order: "⟦k > 0; root_order k t⟧ ⟹ root_order k (insert k x t)"
using ins_root_order
by (simp add: tree⇩i_order)

lemma insert_inorder: "sorted_less (inorder t) ⟹ inorder (insert k x t) = ins_list x (inorder t)"
using ins_inorder
by (simp add: tree⇩i_inorder)

text "Deletion proofs"

thm list.simps

lemma rebalance_middle_tree_height:
assumes "height t = height sub"
and "case rs of (rsub,rsep) # list ⇒ height rsub = height t | [] ⇒ True"
shows "height (rebalance_middle_tree k ls sub sep rs t) = height (Node (ls@(sub,sep)#rs) t)"
proof (cases "height t")
case 0
then have "t = Leaf" "sub = Leaf" using height_Leaf assms by auto
then show ?thesis by simp
next
case (Suc nat)
then obtain tts tt where t_node: "t = Node tts tt"
using height_Leaf by (cases t) simp
then obtain mts mt where sub_node: "sub = Node mts mt"
using assms by (cases sub) simp
then show ?thesis
proof (cases "length mts ≥ k ∧ length tts ≥ k")
case False
then show ?thesis
proof (cases rs)
case Nil
then have "height_up⇩i (node⇩i k (mts@(mt,sep)#tts) tt) = height (Node (mts@(mt,sep)#tts) tt)"
using node⇩i_height by blast
also have "… = max (height t) (height sub)"
by (metis assms(1) height_up⇩i.simps(2) height_list_split sub_node t_node)
finally have height_max: "height_up⇩i (node⇩i k (mts @ (mt, sep) # tts) tt) = max (height t) (height sub)" by simp
then show ?thesis
proof (cases "node⇩i k (mts@(mt,sep)#tts) tt")
case (T⇩i u)
then have "height u = max (height t) (height sub)" using height_max by simp
then have "height (Node ls u) = height (Node (ls@[(sub,sep)]) t)"
by (induction ls) (auto simp add: max.commute)
then show ?thesis using Nil False T⇩i
by (simp add: sub_node t_node)
next
case (Up⇩i l a r)
then have "height (Node (ls@[(sub,sep)]) t) =  height (Node (ls@[(l,a)]) r)"
using assms(1) height_max by (induction ls) auto
then show ?thesis
using Up⇩i Nil sub_node t_node by auto
qed
next
case (Cons a list)
then obtain rsub rsep where a_split: "a = (rsub, rsep)"
by (cases a)
then obtain rts rt where r_node: "rsub = Node rts rt"
using assms(2) Cons height_Leaf Suc by (cases rsub) simp_all

then have "height_up⇩i (node⇩i k (mts@(mt,sep)#rts) rt) = height (Node (mts@(mt,sep)#rts) rt)"
using node⇩i_height by blast
also have "… = max (height rsub) (height sub)"
by (metis r_node height_up⇩i.simps(2) height_list_split max.commute sub_node)
finally have height_max: "height_up⇩i (node⇩i k (mts @ (mt, sep) # rts) rt) = max (height rsub) (height sub)" by simp
then show ?thesis
proof (cases "node⇩i k (mts@(mt,sep)#rts) rt")
case (T⇩i u)
then have "height u = max (height rsub) (height sub)"
using height_max by simp
then show ?thesis
using T⇩i False Cons r_node a_split sub_node t_node by auto
next
case (Up⇩i l a r)
then have height_max: "max (height l) (height r) = max (height rsub) (height sub)"
using height_max by auto
then show ?thesis
using Cons a_split r_node Up⇩i sub_node t_node by auto
qed
qed
qed (simp add: sub_node t_node)
qed

lemma rebalance_last_tree_height:
assumes "height t = height sub"
and "ts = list@[(sub,sep)]"
shows "height (rebalance_last_tree k ts t) = height (Node ts t)"
using rebalance_middle_tree_height assms by auto

lemma split_max_height:
assumes "split_max k t = (sub,sep)"
and "nonempty_lasttreebal t"
and "t ≠ Leaf"
shows "height sub = height t"
using assms
proof(induction t arbitrary: k sub sep)
case Node1: (Node tts tt)
then obtain ls tsub tsep where tts_split: "tts = ls@[(tsub,tsep)]" by auto
then show ?case
proof (cases tt)
case Leaf
then have "height (Node (ls@[(tsub,tsep)]) tt) = max (height (Node ls tsub)) (Suc (height tt))"
using height_btree_last height_btree_order by metis
moreover have "split_max k (Node tts tt) = (Node ls tsub, tsep)"
using Leaf Node1 tts_split by auto
ultimately show ?thesis
using Leaf Node1 height_Leaf max_def by auto
next
case Node2: (Node l a)
then obtain subsub subsep where sub_split: "split_max k tt = (subsub,subsep)" by (cases "split_max k tt")
then have "height subsub = height tt" using Node1 Node2 by auto
moreover have "split_max k (Node tts tt) = (rebalance_last_tree k tts subsub, subsep)"
using Node1 Node2 tts_split sub_split by auto
ultimately show ?thesis using rebalance_last_tree_height Node1 Node2 by auto
qed
qed auto

lemma order_bal_nonempty_lasttreebal: "⟦k > 0; root_order k t; bal t⟧ ⟹ nonempty_lasttreebal t"
proof(induction k t rule: order.induct)
case (2 k ts t)
then have "length ts > 0" by auto
then obtain ls tsub tsep where ts_split: "ts = (ls@[(tsub,tsep)])"
by (metis eq_fst_iff length_greater_0_conv snoc_eq_iff_butlast)
moreover have "height tsub = height t"
using "2.prems"(3) ts_split by auto
moreover have "nonempty_lasttreebal t" using 2 order_impl_root_order by auto
ultimately show ?case by simp
qed simp

lemma bal_sub_height: "bal (Node (ls@a#rs) t) ⟹ (case rs of [] ⇒ True | (sub,sep)#_ ⇒ height sub = height t)"
by (cases rs) (auto)

lemma del_height: "⟦k > 0; root_order k t; bal t⟧ ⟹ height (del k x t) = height t"
proof(induction k x t rule: del.induct)
case (2 k x ts t)
then obtain ls list where list_split: "split ts x = (ls, list)" by (cases "split ts x")
then show ?case
proof(cases list)
case Nil
then have "height (del k x t) = height t"
using 2 list_split order_bal_nonempty_lasttreebal
by (simp add: order_impl_root_order)
moreover obtain lls sub sep where "ls = lls@[(sub,sep)]"
using split_conc 2 list_split Nil
by (metis append_Nil2 nonempty_lasttreebal.simps(2) order_bal_nonempty_lasttreebal)
moreover have "Node ls t = Node ts t" using split_conc Nil list_split by auto
ultimately show ?thesis
using rebalance_last_tree_height 2 list_split Nil split_conc
by (auto simp add: max.assoc sup_nat_def max_def)
next
case (Cons a rs)
then have rs_height: "case rs of [] ⇒ True | (rsub,rsep)#_ ⇒ height rsub = height t" (* notice the difference if rsub and t are switched *)
using "2.prems"(3) bal_sub_height list_split split_conc by blast
from Cons obtain sub sep where a_split: "a = (sub,sep)" by (cases a)
consider (sep_n_x) "sep ≠ x" |
(sep_x_Leaf) "sep = x ∧ sub = Leaf" |
(sep_x_Node) "sep = x ∧ (∃ts t. sub = Node ts t)"
using btree.exhaust by blast
then show ?thesis
proof cases
case sep_n_x
have height_t_sub: "height t = height sub"
using "2.prems"(3) a_split list_split local.Cons split.split_set(1) split_axioms by fastforce
have height_t_del: "height (del k x sub) = height t"
by (metis "2.IH"(2) "2.prems"(1) "2.prems"(2) "2.prems"(3) a_split bal.simps(2) list_split local.Cons order_impl_root_order root_order.simps(2) sep_n_x some_child_sub(1) split_set(1))
then have "height (rebalance_middle_tree k ls (del k x sub) sep rs t) = height (Node (ls@((del k x sub),sep)#rs) t)"
using rs_height rebalance_middle_tree_height by simp
also have "… = height (Node (ls@(sub,sep)#rs) t)"
using height_t_sub "2.prems" height_t_del
by auto
also have "… = height (Node ts t)"
using 2 a_split sep_n_x list_split Cons split_set(1) split_conc
by auto
finally show ?thesis
using sep_n_x Cons a_split list_split 2
by simp
next
case sep_x_Leaf
then have "height (Node ts t) = height (Node (ls@rs) t)"
using bal_split_last(2) "2.prems"(3) a_split list_split Cons split_conc
by metis
then show ?thesis
using a_split list_split Cons sep_x_Leaf 2 by auto
next
case sep_x_Node
then obtain sts st where sub_node: "sub = Node sts st" by blast
obtain sub_s max_s where sub_split: "split_max k sub = (sub_s, max_s)"
by (cases "split_max k sub")
then have "height sub_s = height t"
by (metis "2.prems"(1) "2.prems"(2) "2.prems"(3) a_split bal.simps(2) btree.distinct(1) list_split Cons order_bal_nonempty_lasttreebal order_impl_root_order root_order.simps(2) some_child_sub(1) split_set(1) split_max_height sub_node)
then have "height (rebalance_middle_tree k ls sub_s max_s rs t) = height (Node (ls@(sub_s,sep)#rs) t)"
using rs_height rebalance_middle_tree_height by simp
also have "… = height (Node ts t)"
using 2 a_split sep_x_Node list_split Cons split_set(1) ‹height sub_s = height t›
by (auto simp add: split_conc[of ts])
finally show ?thesis using sep_x_Node Cons a_split list_split 2 sub_node sub_split
by auto
qed
qed
qed simp

(* proof for inorders *)

(* note: this works (as it should, since there is not even recursion involved)
automatically. *yay* *)
lemma rebalance_middle_tree_inorder:
assumes "height t = height sub"
and "case rs of (rsub,rsep) # list ⇒ height rsub = height t | [] ⇒ True"
shows "inorder (rebalance_middle_tree k ls sub sep rs t) = inorder (Node (ls@(sub,sep)#rs) t)"
apply(cases sub; cases t)
using assms
apply (auto
split!: btree.splits up⇩i.splits list.splits
simp del: node⇩i.simps
simp add: node⇩i_inorder_simps
)
done

lemma rebalance_last_tree_inorder:
assumes "height t = height sub"
and "ts = list@[(sub,sep)]"
shows "inorder (rebalance_last_tree k ts t) = inorder (Node ts t)"
using rebalance_middle_tree_inorder assms by auto

lemma butlast_inorder_app_id: "xs = xs' @ [(sub,sep)] ⟹ inorder_list xs' @ inorder sub @ [sep] = inorder_list xs"
by simp

lemma split_max_inorder:
assumes "nonempty_lasttreebal t"
and "t ≠ Leaf"
shows "inorder_pair (split_max k t) = inorder t"
using assms
proof (induction k t rule: split_max.induct)
case (1 k ts t)
then show ?case
proof (cases t)
case Leaf
then have "ts = butlast ts @ [last ts]"
using "1.prems"(1) by auto
moreover obtain sub sep where "last ts = (sub,sep)"
by fastforce
ultimately show ?thesis
using Leaf
apply (auto split!: prod.splits btree.splits)
by (simp add: butlast_inorder_app_id)
next
case (Node tts tt)
then have IH: "inorder_pair (split_max k t) = inorder t"
using "1.IH" "1.prems"(1) by auto
obtain sub sep where split_sub_sep: "split_max k t = (sub,sep)"
by fastforce
then have height_sub: "height sub = height t"
by (metis "1.prems"(1) Node btree.distinct(1) nonempty_lasttreebal.simps(2) split_max_height)
have "inorder_pair (split_max k (Node ts t)) = inorder (rebalance_last_tree k ts sub) @ [sep]"
using Node 1 split_sub_sep by auto
also have "… = inorder_list ts @ inorder sub @ [sep]"
using rebalance_last_tree_inorder height_sub "1.prems"
by (auto simp del: rebalance_last_tree.simps)
also have "… = inorder (Node ts t)"
using IH split_sub_sep by simp
finally show ?thesis .
qed
qed simp

lemma height_bal_subtrees_merge: "⟦height (Node as a) = height (Node bs b); bal (Node as a); bal (Node bs b)⟧
⟹ ∀x ∈ set (subtrees as) ∪ {a}. height x = height b"
by (metis Suc_inject Un_iff bal.simps(2) height_bal_tree singletonD)

lemma bal_list_merge:
assumes "bal_up⇩i (Up⇩i (Node as a) x (Node bs b))"
shows "bal (Node (as@(a,x)#bs) b)"
proof -
have "∀x∈set (subtrees (as @ (a, x) # bs)). bal x"
using subtrees_split assms by auto
moreover have "bal b"
using assms by auto
moreover have "∀x∈set (subtrees as) ∪ {a} ∪ set (subtrees bs). height x = height b"
using assms height_bal_subtrees_merge
unfolding bal_up⇩i.simps
by blast
ultimately show ?thesis
by auto
qed

lemma node⇩i_bal_up⇩i:
assumes "bal_up⇩i (node⇩i k ts t)"
shows "bal (Node ts t)"
using assms
proof(cases "length ts ≤ 2*k")
case False
then obtain ls sub sep rs where split_list: "split_half ts = (ls, (sub,sep)#rs)"
using node⇩i_cases by blast
then have "node⇩i k ts t = Up⇩i (Node ls sub) sep (Node rs t)"
using False by auto
moreover have "ts = ls@(sub,sep)#rs"
by (metis append_take_drop_id fst_conv local.split_list snd_conv split_half.elims)
ultimately show ?thesis
using bal_list_merge[of ls sub sep rs t] assms
by (simp del: bal.simps bal_up⇩i.simps)
qed simp

lemma node⇩i_bal_simp: "bal_up⇩i (node⇩i k ts t) = bal (Node ts t)"
using node⇩i_bal node⇩i_bal_up⇩i by blast

lemma rebalance_middle_tree_bal: "bal (Node (ls@(sub,sep)#rs) t) ⟹ bal (rebalance_middle_tree k ls sub sep rs t)"
proof (cases t)
case t_node: (Node tts tt)
assume assms: "bal (Node (ls @ (sub, sep) # rs) t)"
then obtain mts mt where sub_node: "sub = Node mts mt"
by (cases sub) (auto simp add: t_node)
have sub_heights: "height sub = height t" "bal sub" "bal t"
using assms by auto
show ?thesis
proof (cases "length mts ≥ k ∧ length tts ≥ k")
case True
then show ?thesis
using t_node sub_node assms
by (auto simp del: bal.simps)
next
case False
then show ?thesis
proof (cases rs)
case Nil
have "height_up⇩i (node⇩i k (mts@(mt,sep)#tts) tt) = height (Node (mts@(mt,sep)#tts) tt)"
using node⇩i_height by blast
also have "… = Suc (height tt)"
by (metis height_bal_tree height_up⇩i.simps(2) height_list_split max.idem sub_heights(1) sub_heights(3) sub_node t_node)
also have "… = height t"
using height_bal_tree sub_heights(3) t_node by fastforce
finally have "height_up⇩i (node⇩i k (mts@(mt,sep)#tts) tt) = height t" by simp
moreover have "bal_up⇩i (node⇩i k (mts@(mt,sep)#tts) tt)"
by (metis bal_list_merge bal_up⇩i.simps(2) node⇩i_bal sub_heights(1) sub_heights(2) sub_heights(3) sub_node t_node)
ultimately show ?thesis
apply (cases "node⇩i k (mts@(mt,sep)#tts) tt")
using assms Nil sub_node t_node by auto
next
case (Cons r rs)
then obtain rsub rsep where r_split: "r = (rsub,rsep)" by (cases r)
then have rsub_height: "height rsub = height t" "bal rsub"
using assms Cons by auto
then obtain rts rt where r_node: "rsub = (Node rts rt)"
apply(cases rsub) using t_node by simp
have "height_up⇩i (node⇩i k (mts@(mt,sep)#rts) rt) = height (Node (mts@(mt,sep)#rts) rt)"
using node⇩i_height by blast
also have "… = Suc (height rt)"
by (metis Un_iff  ‹height rsub = height t› assms bal.simps(2) bal_split_last(1) height_bal_tree height_up⇩i.simps(2) height_list_split list.set_intros(1) Cons max.idem r_node r_split set_append some_child_sub(1) sub_heights(1) sub_node)
also have "… = height rsub"
using height_bal_tree r_node rsub_height(2) by fastforce
finally have 1: "height_up⇩i (node⇩i k (mts@(mt,sep)#rts) rt) = height rsub" .
moreover have 2: "bal_up⇩i (node⇩i k (mts@(mt,sep)#rts) rt)"
by (metis bal_list_merge bal_up⇩i.simps(2) node⇩i_bal r_node rsub_height(1) rsub_height(2) sub_heights(1) sub_heights(2) sub_node)
ultimately show ?thesis
proof (cases "node⇩i k (mts@(mt,sep)#rts) rt")
case (T⇩i u)
then have "bal (Node (ls@(u,rsep)#rs) t)"
using 1 2 Cons assms t_node subtrees_split sub_heights r_split rsub_height
unfolding bal.simps by (auto simp del: height_btree.simps)
then show ?thesis
using Cons assms t_node sub_node r_split r_node False T⇩i
by (auto simp del: node⇩i.simps bal.simps)
next
case (Up⇩i l a r)
then have "bal (Node (ls@(l,a)#(r,rsep)#rs) t)"
using 1 2 Cons assms t_node subtrees_split sub_heights r_split rsub_height
unfolding bal.simps by (auto simp del: height_btree.simps)
then show ?thesis
using Cons assms t_node sub_node r_split r_node False Up⇩i
by (auto simp del: node⇩i.simps bal.simps)
qed
qed
qed
qed (simp add: height_Leaf)

lemma rebalance_last_tree_bal: "⟦bal (Node ts t); ts ≠ []⟧ ⟹ bal (rebalance_last_tree k ts t)"
using rebalance_middle_tree_bal append_butlast_last_id[of ts]
apply(cases "last ts")
apply(auto simp del: bal.simps rebalance_middle_tree.simps)
done

lemma split_max_bal:
assumes "bal t"
and "t ≠ Leaf"
and "nonempty_lasttreebal t"
shows "bal (fst (split_max k t))"
using assms
proof(induction k t rule: split_max.induct)
case (1 k ts t)
then show ?case
proof (cases t)
case Leaf
then obtain sub sep where last_split: "last ts = (sub,sep)"
using 1 by auto
then have "height sub = height t" using 1 by auto
then have "bal (Node (butlast ts) sub)" using 1 last_split by auto
then show ?thesis using 1 Leaf last_split by auto
next
case (Node tts tt)
then obtain sub sep where t_split: "split_max k t = (sub,sep)" by (cases "split_max k t")
then have "height sub = height t" using 1 Node
by (metis btree.distinct(1) nonempty_lasttreebal.simps(2) split_max_height)
moreover have "bal sub"
using "1.IH" "1.prems"(1) "1.prems"(3) Node t_split by fastforce
ultimately have "bal (Node ts sub)"
using 1 t_split Node by auto
then show ?thesis
using rebalance_last_tree_bal t_split Node 1
by (auto simp del: bal.simps rebalance_middle_tree.simps)
qed
qed simp

lemma del_bal:
assumes "k > 0"
and "root_order k t"
and "bal t"
shows "bal (del k x t)"
using assms
proof(induction k x t rule: del.induct)
case (2 k x ts t)
then obtain ls rs where list_split: "split ts x = (ls,rs)"
by (cases "split ts x")
then show ?case
proof (cases rs)
case Nil
then have "bal (del k x t)" using 2 list_split
by (simp add: order_impl_root_order)
moreover have "height (del k x t) = height t"
using 2 del_height by (simp add: order_impl_root_order)
moreover have "ts ≠ []" using 2 by auto
ultimately have "bal (rebalance_last_tree k ts (del k x t))"
using 2 Nil order_bal_nonempty_lasttreebal rebalance_last_tree_bal
by simp
then have "bal (rebalance_last_tree k ls (del k x t))"
using list_split split_conc Nil by fastforce
then show ?thesis
using 2 list_split Nil
by auto
next
case (Cons r rs)
then obtain sub sep where r_split: "r = (sub,sep)" by (cases r)
then have sub_height: "height sub = height t" "bal sub"
using 2 Cons list_split split_set(1) by fastforce+
consider (sep_n_x) "sep ≠ x" |
(sep_x_Leaf) "sep = x ∧ sub = Leaf" |
(sep_x_Node) "sep = x ∧ (∃ts t. sub = Node ts t)"
using btree.exhaust by blast
then show ?thesis
proof cases
case sep_n_x
then have "bal (del k x sub)" "height (del k x sub) = height sub" using sub_height
apply (metis "2.IH"(2) "2.prems"(1) "2.prems"(2) list_split local.Cons order_impl_root_order r_split root_order.simps(2) some_child_sub(1) split_set(1))
by (metis "2.prems"(1) "2.prems"(2) list_split Cons order_impl_root_order r_split root_order.simps(2) some_child_sub(1) del_height split_set(1) sub_height(2))
moreover have "bal (Node (ls@(sub,sep)#rs) t)"
using "2.prems"(3) list_split Cons r_split split_conc by blast
ultimately have "bal (Node (ls@(del k x sub,sep)#rs) t)"
using bal_substitute_subtree[of ls sub sep rs t "del k x sub"] by metis
then have "bal (rebalance_middle_tree k ls (del k x sub) sep rs t)"
using rebalance_middle_tree_bal[of ls "del k x sub" sep rs t k] by metis
then show ?thesis
using 2 list_split Cons r_split sep_n_x by auto
next
case sep_x_Leaf
moreover have "bal (Node (ls@rs) t)"
using bal_split_last(1) list_split split_conc r_split
by (metis "2.prems"(3) Cons)
ultimately show ?thesis
using 2 list_split Cons r_split by auto
next
case sep_x_Node
then obtain sts st where sub_node: "sub = Node sts st" by auto
then obtain sub_s max_s where sub_split: "split_max k sub = (sub_s, max_s)"
by (cases "split_max k sub")
then have "height sub_s = height sub"
using split_max_height
by (metis "2.prems"(1) "2.prems"(2) btree.distinct(1) list_split Cons order_bal_nonempty_lasttreebal order_impl_root_order r_split root_order.simps(2) some_child_sub(1) split_set(1) sub_height(2) sub_node)
moreover have "bal sub_s"
using split_max_bal
by (metis "2.prems"(1) "2.prems"(2) btree.distinct(1) fst_conv list_split local.Cons order_bal_nonempty_lasttreebal order_impl_root_order r_split root_order.simps(2) some_child_sub(1) split_set(1) sub_height(2) sub_node sub_split)
moreover have "bal (Node (ls@(sub,sep)#rs) t)"
using "2.prems"(3) list_split Cons r_split split_conc by blast
ultimately have "bal (Node (ls@(sub_s,sep)#rs) t)"
using bal_substitute_subtree[of ls sub sep rs t "sub_s"] by metis
then have "bal (Node (ls@(sub_s,max_s)#rs) t)"
using bal_substitute_separator by metis
then have "bal (rebalance_middle_tree k ls sub_s max_s rs t)"
using rebalance_middle_tree_bal[of ls sub_s max_s rs t k] by metis
then show ?thesis
using 2 list_split Cons r_split sep_x_Node sub_node sub_split by auto
qed
qed
qed simp

lemma rebalance_middle_tree_order:
assumes "almost_order k sub"
and "∀s ∈ set (subtrees (ls@rs)). order k s" "order k t"
and "case rs of (rsub,rsep) # list ⇒ height rsub = height t | [] ⇒ True"
and "length (ls@(sub,sep)#rs) ≤ 2*k"
and "height sub = height t"
shows "almost_order k (rebalance_middle_tree k ls sub sep rs t)"
proof(cases t)
case Leaf
then have "sub = Leaf" using height_Leaf assms by auto
then show ?thesis using Leaf assms by auto
next
case t_node: (Node tts tt)
then obtain mts mt where sub_node: "sub = Node mts mt"
using assms by (cases sub) (auto)
then show ?thesis
proof(cases "length mts ≥ k ∧ length tts ≥ k")
case True
then have "order k sub" using assms
by (simp add: sub_node)
then show ?thesis
using True t_node sub_node assms by auto
next
case False
then show ?thesis
proof (cases rs)
case Nil
have "order_up⇩i k (node⇩i k (mts@(mt,sep)#tts) tt)"
using node⇩i_order[of k "mts@(mt,sep)#tts" tt] assms(1,3) t_node sub_node
by (auto simp del: order_up⇩i.simps node⇩i.simps)
then show ?thesis
apply(cases "node⇩i k (mts@(mt,sep)#tts) tt")
using assms t_node sub_node False Nil apply (auto simp del: node⇩i.simps)
done
next
case (Cons r rs)
then obtain rsub rsep where r_split: "r = (rsub,rsep)" by (cases r)
then have rsub_height: "height rsub = height t"
using assms Cons by auto
then obtain rts rt where r_node: "rsub = (Node rts rt)"
apply(cases rsub) using t_node by simp
have "order_up⇩i k (node⇩i k (mts@(mt,sep)#rts) rt)"
using node⇩i_order[of k "mts@(mt,sep)#rts" rt] assms(1,2) t_node sub_node r_node r_split Cons
by (auto simp del: order_up⇩i.simps node⇩i.simps)
then show ?thesis
apply(cases "node⇩i k (mts@(mt,sep)#rts) rt")
using assms t_node sub_node False Cons r_split r_node apply (auto simp del: node⇩i.simps)
done
qed
qed
qed

(* we have to proof the order invariant once for an underflowing last tree *)
lemma rebalance_middle_tree_last_order:
assumes "almost_order k t"
and  "∀s ∈ set (subtrees (ls@(sub,sep)#rs)). order k s"
and "rs = []"
and "length (ls@(sub,sep)#rs) ≤ 2*k"
and "height sub = height t"
shows "almost_order k (rebalance_middle_tree k ls sub sep rs t)"
proof (cases t)
case Leaf
then have "sub = Leaf" using height_Leaf assms by auto
then show ?thesis using Leaf assms by auto
next
case t_node: (Node tts tt)
then obtain mts mt where sub_node: "sub = Node mts mt"
using assms by (cases sub) (auto)
then show ?thesis
proof(cases "length mts ≥ k ∧ length tts ≥ k")
case True
then have "order k sub" using assms
by (simp add: sub_node)
then show ?thesis
using True t_node sub_node assms by auto
next
case False
have "order_up⇩i k (node⇩i k (mts@(mt,sep)#tts) tt)"
using node⇩i_order[of k "mts@(mt,sep)#tts" tt] assms t_node sub_node
by (auto simp del: order_up⇩i.simps node⇩i.simps)
then show ?thesis
apply(cases "node⇩i k (mts@(mt,sep)#tts) tt")
using assms t_node sub_node False Nil apply (auto simp del: node⇩i.simps)
done
qed
qed

lemma rebalance_last_tree_order:
assumes "ts = ls@[(sub,sep)]"
and "∀s ∈ set (subtrees (ts)). order k s" "almost_order k t"
and "length ts ≤ 2*k"
and "height sub = height t"
shows "almost_order k (rebalance_last_tree k ts t)"
using rebalance_middle_tree_last_order assms by auto

lemma split_max_order:
assumes "order k t"
and "t ≠ Leaf"
and "nonempty_lasttreebal t"
shows "almost_order k (fst (split_max k t))"
using assms
proof(induction k t rule: split_max.induct)
case (1 k ts t)
then obtain ls sub sep where ts_not_empty: "ts = ls@[(sub,sep)]"
by auto
then show ?case
proof (cases t)
case Leaf
then show ?thesis using ts_not_empty 1 by auto
next
case (Node)
then obtain s_sub s_max where sub_split: "split_max k t = (s_sub, s_max)"
by (cases "split_max k t")
moreover have "height sub = height s_sub"
by (metis "1.prems"(3) Node Pair_inject append1_eq_conv btree.distinct(1) nonempty_lasttreebal.simps(2) split_max_height sub_split ts_not_empty)
ultimately have "almost_order k (rebalance_last_tree k ts s_sub)"
using rebalance_last_tree_order[of ts ls sub sep k s_sub]
1 ts_not_empty Node sub_split
by force
then show ?thesis
using Node 1 sub_split by auto
qed
qed simp

lemma del_order:
assumes "k > 0"
and "root_order k t"
and "bal t"
shows "almost_order k (del k x t)"
using assms
proof (induction k x t rule: del.induct)
case (2 k x ts t)
then obtain ls list where list_split: "split ts x = (ls, list)" by (cases "split ts x")
then show ?case
proof (cases list)
case Nil
then have "almost_order k (del k x t)" using 2 list_split
by (simp add: order_impl_root_order)
moreover obtain lls lsub lsep where ls_split: "ls = lls@[(lsub,lsep)]"
using 2 Nil list_split
by (metis append_Nil2 nonempty_lasttreebal.simps(2) order_bal_nonempty_lasttreebal split_conc)
moreover have "height t = height (del k x t)" using del_height 2
by (simp add: order_impl_root_order)
moreover have "length ls = length ts"
using Nil list_split
by (auto dest: split_length)
ultimately have "almost_order k (rebalance_last_tree k ls (del k x t))"
using rebalance_last_tree_order[of ls lls lsub lsep k "del k x t"]
by (metis "2.prems"(2) "2.prems"(3) Un_iff append_Nil2 bal.simps(2) list_split Nil root_order.simps(2) singletonI split_conc subtrees_split)
then show ?thesis
using 2 list_split Nil by auto
next
case (Cons r rs)

from Cons obtain sub sep where r_split: "r = (sub,sep)" by (cases r)

have inductive_help:
"case rs of [] ⇒ True | (rsub,rsep)#_ ⇒ height rsub = height t"
"∀s∈set (subtrees (ls @ rs)). order k s"
"Suc (length (ls @ rs)) ≤ 2 * k"
"order k t"
using Cons r_split "2.prems" list_split split_set
by (auto dest: split_conc split!: list.splits)

consider (sep_n_x) "sep ≠ x" |
(sep_x_Leaf) "sep = x ∧ sub = Leaf" |
(sep_x_Node) "sep = x ∧ (∃ts t. sub = Node ts t)"
using btree.exhaust by blast
then show ?thesis
proof cases
case sep_n_x
then have "almost_order k (del k x sub)" using 2 list_split Cons r_split order_impl_root_order
by (metis bal.simps(2) root_order.simps(2) some_child_sub(1) split_set(1))
moreover have "height (del k x sub) = height t"
by (metis "2.prems"(1) "2.prems"(2) "2.prems"(3) bal.simps(2) list_split Cons order_impl_root_order r_split root_order.simps(2) some_child_sub(1) del_height split_set(1))
ultimately have "almost_order k (rebalance_middle_tree k ls (del k x sub) sep rs t)"
using rebalance_middle_tree_order[of k "del k x sub" ls rs t sep]
using inductive_help
using Cons r_split sep_n_x list_split by auto
then show ?thesis using 2 Cons r_split sep_n_x list_split by auto
next
case sep_x_Leaf
then have "almost_order k (Node (ls@rs) t)" using inductive_help by auto
then show ?thesis using 2 Cons r_split sep_x_Leaf list_split by auto
next
case sep_x_Node
then obtain sts st where sub_node: "sub = Node sts st" by auto
then obtain sub_s max_s where sub_split: "split_max k sub = (sub_s, max_s)"
by (cases "split_max k sub")
then have "height sub_s = height t" using split_max_height
by (metis "2.prems"(1) "2.prems"(2) "2.prems"(3) bal.simps(2) btree.distinct(1) list_split Cons order_bal_nonempty_lasttreebal order_impl_root_order r_split root_order.simps(2) some_child_sub(1) split_set(1) sub_node)
moreover have "almost_order k sub_s" using split_max_order
by (metis "2.prems"(1) "2.prems"(2) "2.prems"(3) bal.simps(2) btree.distinct(1) fst_conv list_split local.Cons order_bal_nonempty_lasttreebal order_impl_root_order r_split root_order.simps(2) some_child_sub(1) split_set(1)  sub_node sub_split)
ultimately have "almost_order k (rebalance_middle_tree k ls sub_s max_s rs t)"
using rebalance_middle_tree_order[of k sub_s ls rs t max_s] inductive_help
by auto
then show ?thesis
using 2 Cons r_split list_split sep_x_Node sub_split by auto
qed
qed
qed simp

(* sortedness of delete by inorder *)
(* generalize del_list_sorted since its cumbersome to express inorder_list ts as xs @ [a]
note that the proof scheme is almost identical to ins_list_sorted
*)
thm del_list_sorted

lemma del_list_split:
assumes "split ts x = (ls, rs)"
and "sorted_less (inorder (Node ts t))"
shows "del_list x (inorder (Node ts t)) = inorder_list ls @ del_list x (inorder_list rs @ inorder t)"
proof (cases ls)
case Nil
then show ?thesis
using assms by (auto dest!: split_conc)
next
case Cons
then obtain ls' sub sep where ls_tail_split: "ls = ls' @ [(sub,sep)]"
by (metis list.distinct(1) rev_exhaust surj_pair)
moreover have "sep < x"
using split_req(2)[of ts x ls' sub sep rs]
using assms(1) assms(2) ls_tail_split sorted_inorder_separators
by blast
moreover have "sorted_less (inorder_list ls)"
using assms sorted_wrt_append split_conc by fastforce
ultimately show ?thesis using assms(2) split_conc[OF assms(1)]
using del_list_sorted[of "inorder_list ls' @ inorder sub" sep]
by auto
qed

(* del sorted requires sortedness of the full list so we need to change the right specialization a bit *)

lemma del_list_split_right:
assumes "split ts x = (ls, (sub,sep)#rs)"
and "sorted_less (inorder (Node ts t))"
and "sep ≠ x"
shows "del_list x (inorder_list ((sub,sep)#rs) @ inorder t) = del_list x (inorder sub) @ sep # inorder_list rs @ inorder t"
proof -
from assms have "x < sep"
proof -
from assms have "sorted_less (separators ts)"
using sorted_inorder_separators by blast
then show ?thesis
using split_req(3)
using assms
by fastforce
qed
moreover have "sorted_less (inorder sub @ sep # inorder_list rs @ inorder t)"
using assms sorted_wrt_append[where xs="inorder_list ls"]
by (auto dest!: split_conc)
ultimately show ?thesis
using del_list_sorted[of "inorder sub" "sep"]
by auto
qed

thm del_list_idem

lemma del_inorder:
assumes "k > 0"
and "root_order k t"
and "bal t"
and "sorted_less (inorder t)"
shows "inorder (del k x t) = del_list x (inorder t)"
using assms
proof (induction k x t rule: del.induct)
case (2 k x ts t)
then obtain ls rs where list_split: "split ts x = (ls, rs)"
by (meson surj_pair)
then have list_conc: "ts = ls @ rs"
using split.split_conc split_axioms by blast
show ?case
proof (cases rs)
case Nil
then have IH: "inorder (del k x t) = del_list x (inorder t)"
by (metis "2.IH"(1) "2.prems" bal.simps(2) list_split order_impl_root_order root_order.simps(2) sorted_inorder_induct_last)
have "inorder (del k x (Node ts t)) = inorder (rebalance_last_tree k ts (del k x t))"
using list_split Nil list_conc by auto
also have "… = inorder_list ts @ inorder (del k x t)"
proof -
obtain ts' sub sep where ts_split: "ts = ts' @ [(sub, sep)]"
by (meson "2.prems"(1) "2.prems"(2) "2.prems"(3) nonempty_lasttreebal.simps(2) order_bal_nonempty_lasttreebal)
then have "height sub = height t"
using "2.prems"(3) by auto
moreover have "height t = height (del k x t)"
by (metis "2.prems"(1) "2.prems"(2) "2.prems"(3) bal.simps(2) del_height order_impl_root_order root_order.simps(2))
ultimately show ?thesis
using rebalance_last_tree_inorder
using ts_split by auto
qed
also have "… = inorder_list ts @ del_list x (inorder t)"
using IH by blast
also have "… = del_list x (inorder (Node ts t))"
using "2.prems"(4) list_conc list_split Nil del_list_split
by auto
finally show ?thesis .
next
case (Cons h rs)
then obtain sub sep where h_split: "h = (sub,sep)"
by (cases h)
then have node_sorted_split:
"sorted_less (inorder (Node (ls@(sub,sep)#rs) t))"
"root_order k (Node (ls@(sub,sep)#rs) t)"
"bal (Node (ls@(sub,sep)#rs) t)"
using "2.prems" h_split list_conc Cons by blast+
consider (sep_n_x) "sep ≠ x" | (sep_x_Leaf) "sep = x ∧ sub = Leaf" |  (sep_x_Node) "sep = x ∧ (∃ts t. sub = Node ts t)"
using btree.exhaust by blast
then show ?thesis
proof cases
case sep_n_x
then have IH: "inorder (del k x sub) = del_list x (inorder sub)"
by (metis "2.IH"(2) "2.prems"(1) "2.prems"(2) bal.simps(2) bal_split_left(1) h_split list_split local.Cons node_sorted_split(1) node_sorted_split(3) order_impl_root_order root_order.simps(2) some_child_sub(1) sorted_inorder_induct_subtree split_set(1))
from sep_n_x have "inorder (del k x (Node ts t)) = inorder (rebalance_middle_tree k ls (del k x sub) sep rs t)"
using list_split Cons h_split by auto
also have "… = inorder (Node (ls@(del k x sub, sep)#rs) t)"
proof -
have "height t = height (del k x sub)"
using del_height
using order_impl_root_order "2.prems"
by (auto simp add: order_impl_root_order Cons list_conc h_split)
moreover have "case rs of [] ⇒ True | (rsub, rsep) # list ⇒ height rsub = height t"
using "2.prems"(3) bal_sub_height list_conc Cons by blast
ultimately show ?thesis
using rebalance_middle_tree_inorder
by simp
qed
also have "… = inorder_list ls @ del_list x (inorder sub) @ sep # inorder_list rs @ inorder t"
using IH by simp
also have "… = del_list x (inorder (Node ts t))"
using del_list_split[of ts x ls "(sub,sep)#rs" t]
using del_list_split_right[of ts x ls sub sep rs t]
using list_split list_conc h_split Cons "2.prems"(4) sep_n_x
by auto
finally show ?thesis .
next
case sep_x_Leaf
then have "del_list x (inorder (Node ts t)) = inorder (Node (ls@rs) t)"
using list_conc h_split Cons
using del_list_split[OF list_split "2.prems"(4)]
by simp
also have "… = inorder (del k x (Node ts t))"
using list_split sep_x_Leaf list_conc h_split Cons
by auto
finally show ?thesis by simp
next
case sep_x_Node
obtain ssub ssep where split_split: "split_max k sub = (ssub, ssep)"
by fastforce
from sep_x_Node have "x = sep"
by simp
then have "del_list x (inorder (Node ts t)) = inorder_list ls @ inorder sub @ inorder_list rs @ inorder t"
using list_split list_conc h_split Cons "2.prems"(4)
using del_list_split[OF list_split "2.prems"(4)]
using del_list_sorted1[of "inorder sub" sep "inorder_list rs @ inorder t" x]
sorted_wrt_append
by auto
also have "… = inorder_list ls @ inorder_pair (split_max k sub) @ inorder_list rs @ inorder t"
using sym[OF split_max_inorder[of sub k]]
using order_bal_nonempty_lasttreebal[of k sub] "2.prems"
list_conc h_split Cons sep_x_Node
by (auto simp del: split_max.simps simp add: order_impl_root_order)
also have "… = inorder_list ls @ inorder ssub @ ssep # inorder_list rs @ inorder t"
using split_split by auto
also have "… = inorder (rebalance_middle_tree k ls ssub ssep rs t)"
proof -
have "height t = height ssub"
using split_max_height
by (metis "2.prems"(1,2,3) bal.simps(2) btree.distinct(1) h_split list_split local.Cons order_bal_nonempty_lasttreebal order_impl_root_order root_order.simps(2) sep_x_Node some_child_sub(1) split_set(1) split_split)
moreover have "case rs of [] ⇒ True | (rsub, rsep) # list ⇒ height rsub = height t"
using "2.prems"(3) bal_sub_height list_conc local.Cons
by blast
ultimately show ?thesis
using rebalance_middle_tree_inorder
by auto
qed
also have "… = inorder (del k x (Node ts t))"
using list_split sep_x_Node list_conc h_split Cons split_split
by auto
finally show ?thesis by simp
qed
qed
qed auto

lemma reduce_root_order: "⟦k > 0; almost_order k t⟧ ⟹ root_order k (reduce_root t)"
apply(cases t)
apply(auto split!: list.splits simp add: order_impl_root_order)
done

lemma reduce_root_bal: "bal (reduce_root t) = bal t"
apply(cases t)
apply(auto split!: list.splits)
done

lemma reduce_root_inorder: "inorder (reduce_root t) = inorder t"
apply (cases t)
apply (auto split!: list.splits)
done

lemma delete_order: "⟦k > 0; bal t; root_order k t⟧ ⟹ root_order k (delete k x t)"
using del_order
by (simp add: reduce_root_order)

lemma delete_bal: "⟦k > 0; bal t; root_order k t⟧ ⟹ bal (delete k x t)"
using del_bal
by (simp add: reduce_root_bal)

lemma delete_inorder: "⟦k > 0; bal t; root_order k t; sorted_less (inorder t)⟧ ⟹ inorder (delete k x t) = del_list x (inorder t)"
using del_inorder
by (simp add: reduce_root_inorder)

(* TODO (opt) runtime wrt runtime of split *)

(* we are interested in a) number of comparisons b) number of fetches c) number of writes *)
(* a) is dependent on t_split, the remainder is not (we assume the number of fetches and writes
for split fun is 0 *)

(* TODO simpler induction schemes /less boilerplate isabelle/src/HOL/ex/Induction_Schema *)

subsection "Set specification by inorder"

interpretation S_ordered: Set_by_Ordered where
empty = empty_btree and
insert = "insert (Suc k)" and
delete = "delete (Suc k)" and
isin = "isin" and
inorder = "inorder"   and
inv = "invar_inorder (Suc k)"
proof (standard, goal_cases)
case (2 s x)
then show ?case
by (simp add: isin_set_inorder)
next
case (3 s x)
then show ?case using insert_inorder
by simp
next
case (4 s x)
then show ?case using delete_inorder
by auto
next
case (6 s x)
then show ?case using insert_order insert_bal
by auto
next
case (7 s x)
then show ?case using delete_order delete_bal
by auto
qed (simp add: empty_btree_def)+

(* if we remove this, it is not possible to remove the simp rules in subsequent contexts... *)
declare node⇩i.simps[simp del]

end

end


# Theory BTree_Split

theory BTree_Split
imports BTree_Set
begin

section "Abstract split functions"

subsection "Linear split"

text "Finally we show that the split axioms are feasible
by providing an example split function"

(*TODO: at some point this better be replaced with something binary search like *)
fun linear_split_help:: "(_×'a::linorder) list ⇒ _ ⇒ (_×_) list ⇒  ((_×_) list × (_×_) list)" where
"linear_split_help [] x prev = (prev, [])" |
"linear_split_help ((sub, sep)#xs) x prev = (if sep < x then linear_split_help xs x (prev @ [(sub, sep)]) else (prev, (sub,sep)#xs))"

fun linear_split:: "(_×'a::linorder) list ⇒ _ ⇒ ((_×_) list × (_×_) list)" where
"linear_split xs x = linear_split_help xs x []"

text "Linear split is similar to well known functions, therefore a quick proof can be done."

lemma linear_split_alt: "linear_split xs x = (takeWhile (λ(_,s). s<x) xs, dropWhile (λ(_,s). s<x) xs)"
proof -

have "linear_split_help xs x prev = (prev @ takeWhile (λ(_, s). s < x) xs, dropWhile (λ(_, s). s < x) xs)"
for prev
apply (induction xs arbitrary: prev)
apply auto
done
thus ?thesis by auto
qed

global_interpretation btree_linear_search: split linear_split
(* the below definitions are required to be set here for evaluating example code... *)
defines btree_ls_isin = btree_linear_search.isin
and btree_ls_ins = btree_linear_search.ins
and btree_ls_insert = btree_linear_search.insert
and btree_ls_del = btree_linear_search.del
and btree_ls_delete = btree_linear_search.delete
apply unfold_locales
unfolding linear_split_alt
apply (auto split: list.splits)
subgoal
by (metis (no_types, lifting) case_prodD in_set_conv_decomp takeWhile_eq_all_conv takeWhile_idem)
subgoal
by (metis case_prod_conv hd_dropWhile le_less_linear list.sel(1) list.simps(3))
done

text "Some examples follow to show that the implementation works
and the above lemmas make sense. The examples are visualized in the thesis."

abbreviation "btree⇩i ≡ btree_ls_insert"
abbreviation "btree⇩d ≡ btree_ls_delete"

value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
root_order k x"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
bal x"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
sorted_less (inorder x)"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
x"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
btree⇩i k 9 x"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
btree⇩i k 1 (btree⇩i k 9 x)"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
btree⇩d k 10 (btree⇩i k 1 (btree⇩i k 9 x))"
value "let k=2::nat; x::nat btree = (Node [(Node [(Leaf, 3),(Leaf, 5),(Leaf, 6)] Leaf, 10)] (Node [(Leaf, 14), (Leaf, 20)] Leaf)) in
btree⇩d k 3 (btree⇩d k 10 (btree⇩i k 1 (btree⇩i k 9 x)))"

text "For completeness, we also proved an explicit proof of the locale
requirements."

lemma some_child_sm: "linear_split_help t y xs = (ls,(sub,sep)#rs) ⟹ y ≤ sep"
apply(induction t y xs rule: linear_split_help.induct)
apply(simp_all)
by (metis Pair_inject le_less_linear list.inject)

lemma linear_split_append: "linear_split_help xs p ys = (ls,rs) ⟹ ls@rs = ys@xs"
apply(induction xs p ys rule: linear_split_help.induct)
apply(simp_all)
by (metis Pair_inject)

lemma linear_split_sm: "⟦linear_split_help xs p ys = (ls,rs); sorted_less (separators (ys@xs)); ∀sep ∈ set (separators ys). p > sep⟧ ⟹ ∀sep ∈ set (separators ls). p > sep"
apply(induction xs p ys rule: linear_split_help.induct)
apply(simp_all)
by (metis prod.inject)+

value "linear_split [((Leaf::nat btree), 2)] (1::nat)"

(* TODO still has format for older proof *)
lemma linear_split_gr:
"⟦linear_split_help xs p ys = (ls,rs); sorted_less (separators (ys@xs)); ∀(sub,sep) ∈ set ys. p > sep⟧ ⟹
(case rs of [] ⇒ True | (_,sep)#_ ⇒ p ≤ sep)"
apply(cases rs)
by (auto simp add: some_child_sm)

lemma linear_split_req:
assumes  "linear_split xs p = (ls,(sub,sep)#rs)"
and "sorted_less (separators xs)"
shows  "p ≤ sep"
using assms linear_split_gr by fastforce

lemma linear_split_req2:
assumes  "linear_split xs p = (ls@[(sub,sep)],rs)"
and "sorted_less (separators xs)"
shows  "sep < p"
using linear_split_sm[of xs p "[]" "ls@[(sub,sep)]" rs]
using assms(1) assms(2)
by (metis Nil_is_map_conv Un_iff append_self_conv2 empty_iff empty_set linear_split.elims prod_set_simps(2) separators_split snd_eqD snds.intros)

interpretation split linear_split
by (simp add: linear_split_req linear_split_req2 linear_split_append split_def)

subsection "Binary split"

text "It is possible to define a binary split predicate.
However, even proving that it terminates is uncomfortable."

function (sequential) binary_split_help:: "(_×'a::linorder) list ⇒ (_×'a) list ⇒ (_×'a) list ⇒ 'a ⇒  ((_×_) list × (_×_) list)" where
"binary_split_help ls [] rs x = (ls,rs)" |
"binary_split_help ls as rs x = (let (mls, mrs) = split_half as in (
case mrs of (sub,sep)#mrrs ⇒ (
if x < sep then binary_split_help ls mls (mrs@rs) x
else if x > sep then binary_split_help (ls@mls@[(sub,sep)]) mrrs rs x
else (ls@mls, mrs@rs)
)
)
)"
by pat_completeness auto
termination
apply(relation "measure (λ(ls,xs,rs,x). length xs)")
apply (auto)
by (metis append_take_drop_id length_Cons length_append lessI trans_less_add2)

fun binary_split where
"binary_split as x = binary_split_help [] as [] x"

text "We can show that it will return sublists that concatenate to
the original list again but will not show that it fulfils sortedness properties."

lemma "binary_split_help as bs cs x = (ls,rs) ⟹ (as@bs@cs) = (ls@rs)"
apply(induction as bs cs x arbitrary: ls rs rule: binary_split_help.induct)
apply (auto simp add: drop_not_empty split!: list.splits )
subgoal for ls a b va rs  x lsa rsa aa ba x22
apply(cases "cmp x ba")
apply auto
apply (metis Cons_eq_appendI append_eq_appendI append_take_drop_id)
apply (metis append_take_drop_id)
by (metis Cons_eq_appendI append_eq_appendI append_take_drop_id)
done

lemma "⟦sorted_less (separators (as@bs@cs)); binary_split_help as bs cs x = (ls,rs); ∀y ∈ set (separators as). y < x⟧
⟹ ∀y ∈ set (separators ls). y < x"
oops

end


# Theory Array_SBlit

theory Array_SBlit
imports "Separation_Logic_Imperative_HOL.Array_Blit"
begin

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 ↦⇩a lsrc  >
sblit src si di len
<λ_. src ↦⇩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

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
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 ↦⇩a lsrc
* dst ↦⇩a ldst >
rblit src si dst di len
<λ_. src ↦⇩a lsrc
* dst ↦⇩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)
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 ↦⇩a lsrc  >
srblit src si di len
<λ_. src ↦⇩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)
note [sep_heap_rules] = Suc.IH

have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
= take len (drop si lsrc)"
sledgehammer
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 ≡
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 ↦⇩a lsrc  >
safe_sblit src si di len
<λ_. src ↦⇩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.
We therefore manually handle the case where length is 0 (in which case 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 ()
)
›

definition safe_sblit' where
[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)
(integer_of_nat len)" by (simp add: safe_sblit'_def)

(* TODO: Export to other languages: OCaml, 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)
}"

export_code safe_sblit checking SML Scala

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 ↦⇩a lsrc  >
array_shr src i k
<λ_. src ↦⇩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 ↦⇩a lsrc  >
array_shr src i k
<λ_. src ↦⇩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 ↦⇩a lsrc  >
array_shl src i k
<λ_. src ↦⇩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 ↦⇩a lsrc  >
array_shl src i k
<λ_. src ↦⇩a (take (i-k) lsrc @ (drop i lsrc) @ drop (length lsrc - k) lsrc)
>"
by sep_auto

end

# Theory Partially_Filled_Array

theory Partially_Filled_Array
imports
"Refine_Imperative_HOL.IICF_Array_List"
Array_SBlit
begin

section "Partially Filled Arrays"

text ‹An array that is only partially filled.
The number of actual elements contained is kept in a second element.
This represents a weakened version of the array\_list from IICF.›

type_synonym 'a pfarray = "'a array_list"

subsection "Operations on Partly Filled Arrays"

definition is_pfa where
"is_pfa c l ≡ λ(a,n). ∃⇩A l'. a ↦⇩a l' *  ↑(c = length l' ∧ n ≤ c ∧ l = (take n l'))"

lemma is_pfa_prec[safe_constraint_rules]: "precise (is_pfa c)"
unfolding is_pfa_def[abs_def]
apply(rule preciseI)
apply(simp split: prod.splits)
using preciseD snga_prec by fastforce

definition pfa_init where
"pfa_init cap v n ≡ do {
a ← Array.new cap v;
return (a,n)
}"

lemma pfa_init_rule[sep_heap_rules]: "n ≤ N ⟹ < emp > pfa_init N x n <is_pfa N (replicate n x)>"
by (sep_auto simp: pfa_init_def is_pfa_def)

definition pfa_empty where
"pfa_empty cap ≡ pfa_init cap default 0"

lemma pfa_empty_rule[sep_heap_rules]: "< emp > pfa_empty N <is_pfa N []>"
by (sep_auto simp: pfa_empty_def is_pfa_def)

definition "pfa_length ≡ arl_length"

lemma pfa_length_rule[sep_heap_rules]: "
<is_pfa c l a>
pfa_length a
<λr. is_pfa c l a * ↑(r=length l)>"
by (sep_auto simp: pfa_length_def arl_length_def is_pfa_def)

definition "pfa_capacity ≡ λ(a,n). Array.len a
"

lemma pfa_capacity_rule[sep_heap_rules]: "
<is_pfa c l a>
pfa_capacity a
<λr. is_pfa c l a * ↑(c=r)>"
by (sep_auto simp: pfa_capacity_def arl_length_def is_pfa_def)

definition "pfa_is_empty ≡ arl_is_empty"

lemma pfa_is_empty_rule[sep_heap_rules]: "
<is_pfa c l a>
pfa_is_empty a
<λr. is_pfa c l a * ↑(r⟷(l=[]))>"
by (sep_auto simp: pfa_is_empty_def arl_is_empty_def is_pfa_def)

definition "pfa_append ≡ λ(a,n) x. do {
Array.upd n x a;
return (a,n+1)
}"

lemma pfa_append_rule[sep_heap_rules]: "
n < c  ⟹
< is_pfa c l (a,n) >
pfa_append (a,n) x
<λ(a',n'). is_pfa c (l@[x]) (a',n') * ↑(a' = a ∧ n' = n+1) >"
by (sep_auto
simp: pfa_append_def arl_append_def is_pfa_def take_update_last neq_Nil_conv
split: prod.splits nat.split)

definition "pfa_last ≡ arl_last"

lemma pfa_last_rule[sep_heap_rules]: "
l≠[] ⟹
<is_pfa c l a>
pfa_last a
<λr. is_pfa c l a * ↑(r=last l)>"
by (sep_auto simp: pfa_last_def arl_last_def is_pfa_def last_take_nth_conv)

definition pfa_butlast :: "'a::heap pfarray ⇒ 'a pfarray Heap" where
"pfa_butlast ≡ λ(a,n).
return (a,n-1)
"

lemma pfa_butlast_rule[sep_heap_rules]: "
<is_pfa c l (a,n)>
pfa_butlast (a,n)
<λ(a',n'). is_pfa c (butlast l) (a',n') * ↑(a' = a)>"
by (sep_auto
split: prod.splits
simp: pfa_butlast_def is_pfa_def butlast_take)

definition "pfa_get ≡ arl_get"

lemma pfa_get_rule[sep_heap_rules]: "
i < length l ⟹
< is_pfa c l a>
pfa_get a i
<λr. is_pfa c l a * ↑((l!i) = r)>"
by (sep_auto simp: is_pfa_def pfa_get_def arl_get_def  split: prod.split)

definition "pfa_set ≡ arl_set"

lemma pfa_set_rule[sep_heap_rules]: "
i<length l ⟹
<is_pfa c l a>
pfa_set a i x
<λa'. is_pfa c (l[i:=x]) a' * ↑(a' = a)>"
by (sep_auto simp: pfa_set_def arl_set_def is_pfa_def split: prod.split)

definition pfa_shrink :: "nat ⇒ 'a::heap pfarray ⇒ 'a pfarray Heap" where
"pfa_shrink k ≡ λ(a,n).
return (a,k)
"

lemma pfa_shrink_rule[sep_heap_rules]: "
k ≤ length l ⟹
< is_pfa c l (a,n) >
pfa_shrink k (a,n)
<λ(a',n'). is_pfa c (take k l) (a',n') * ↑(n' = k ∧ a'=a) >"
by (sep_auto
simp: pfa_shrink_def is_pfa_def min.absorb1
split: prod.splits nat.split)

definition pfa_shrink_cap :: "nat ⇒ 'a::heap pfarray ⇒ 'a pfarray Heap" where
"pfa_shrink_cap k ≡ λ(a,n). do {
a' ← array_shrink a k;
return (a',min k n)
}
"

lemma pfa_shrink_cap_rule_preserve[sep_heap_rules]: "
⟦n ≤ k; k ≤ c⟧ ⟹
< is_pfa c l (a,n) >
pfa_shrink_cap k (a,n)
<λa'. is_pfa k l a' >⇩t"
by (sep_auto
simp: pfa_shrink_cap_def is_pfa_def min.absorb1 min.absorb2
split: prod.splits nat.split)

lemma pfa_shrink_cap_rule: "
⟦k ≤ c⟧ ⟹
< is_pfa c l a >
pfa_shrink_cap k a
<λa'. is_pfa k (take k l) a' >⇩t"
by (sep_auto
simp: pfa_shrink_cap_def is_pfa_def min.absorb1 min.absorb2
split: prod.splits nat.split dest: mod_starD)

definition "array_ensure a s x ≡ do {
l←Array.len a;
if l≥s then
return a
else do {
a'←Array.new s x;
blit a 0 a' 0 l;
return a'
}
}"

lemma array_ensure_rule[sep_heap_rules]:
shows "
< a↦⇩ala >
array_ensure a s x
<λa'. a'↦⇩a (la @ replicate (s-length la) x)>⇩t"
unfolding array_ensure_def
by sep_auto

(* Ensure a certain capacity *)
definition pfa_ensure :: "'a::{heap,default} pfarray ⇒ nat ⇒ 'a pfarray Heap" where
"pfa_ensure ≡ λ(a,n) k. do {
a' ← array_ensure a k default;
return (a',n)
}
"

lemma pfa_ensure_rule[sep_heap_rules]: "
< is_pfa c l (a,n) >
pfa_ensure (a,n) k
<λ(a',n'). is_pfa (max c k) l (a',n') * ↑(n' = n ∧ c ≥ n)>⇩t"
by (sep_auto
simp: pfa_ensure_def is_pfa_def)

definition "pfa_copy ≡ arl_copy"

lemma pfa_copy_rule[sep_heap_rules]:
"< is_pfa c l a >
pfa_copy a
<λr. is_pfa c l a * is_pfa c l r>⇩t"
by (sep_auto simp: pfa_copy_def arl_copy_def is_pfa_def)

definition pfa_blit :: "'a::heap pfarray ⇒ nat ⇒ 'a::heap pfarray ⇒ nat ⇒ nat ⇒ unit Heap" where
"pfa_blit ≡ λ(src,sn) si (dst,dn) di l. blit src si dst di l"

lemma min_nat: "min a (a+b) = (a::nat)"
by auto

lemma pfa_blit_rule[sep_heap_rules]:
assumes LEN: "si+len ≤ sn" "di ≤ dn" "di+len ≤ dc"
shows
"< is_pfa sc src (srci,sn)
* is_pfa dc dst (dsti,dn) >
pfa_blit (srci,sn) si (dsti,dn) di len
<λ_. is_pfa sc src (srci,sn)
* is_pfa dc (take di dst @ take len (drop si src) @ drop (di+len) dst) (dsti,max (di+len) dn)
>"
using LEN apply(sep_auto simp add: min_nat is_pfa_def pfa_blit_def min.commute min.absorb1 heap: blit_rule)
apply (simp add: min.absorb1 take_drop)
apply (simp add: drop_take max_def)
done

definition pfa_drop :: "('a::heap) pfarray ⇒ nat ⇒ 'a pfarray ⇒ 'a pfarray Heap" where
"pfa_drop ≡ λ(src,sn) si (dst,dn). do {
blit src si dst 0 (sn-si);
return (dst,(sn-si))
}
"

lemma pfa_drop_rule[sep_heap_rules]:
assumes LEN: "k ≤ sn" "(sn-k) ≤ dc"
shows
"< is_pfa sc src (srci,sn)
* is_pfa dc dst (dsti,dn) >
pfa_drop (srci,sn) k (dsti,dn)
<λ(dsti',dn'). is_pfa sc src (srci,sn)
* is_pfa dc (drop k src) (dsti',dn')
* ↑(dsti' = dsti)
>"
using LEN apply (sep_auto simp add: drop_take is_pfa_def pfa_drop_def dest!: mod_starD heap: pfa_blit_rule)
done

definition "pfa_append_grow ≡ λ(a,n) x. do {
l ← pfa_capacity (a,n);
a' ← if l = n
then array_grow a (l+1) x
else Array.upd n x a;
return (a',n+1)
}"

lemma pfa_append_grow_full_rule[sep_heap_rules]: "n = c ⟹
<is_pfa c l (a,n)>
array_grow a (c+1) x
<λa'. is_pfa (c+1) (l@[x]) (a',n+1)>⇩t"
apply(sep_auto simp add: is_pfa_def
heap del: array_grow_rule)
apply(vcg heap del: array_grow_rule heap add: array_grow_rule[of l "(Suc (length l))" a x])
apply simp
apply(rule ent_ex_postI[where ?x="l@[x]"])
apply sep_auto
done

lemma pfa_append_grow_less_rule: "n < c ⟹
<is_pfa c l (a,n)>
Array.upd n x a
<λa'. is_pfa c (l@[x]) (a',n+1)>⇩t"
apply(sep_auto simp add: is_pfa_def take_update_last)
done

lemma pfa_append_grow_rule[sep_heap_rules]: "
<is_pfa c l (a,n)>
pfa_append_grow (a,n) x
<λ(a',n'). is_pfa (if c = n then c+1 else c) (l@[x]) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
apply(subst pfa_append_grow_def)
apply(rule hoare_triple_preI)
apply (sep_auto
heap add: pfa_append_grow_full_rule pfa_append_grow_less_rule)
apply(sep_auto simp add: is_pfa_def)
apply(sep_auto simp add: is_pfa_def)
done

(* This definition has only one access to the array length *)
definition "pfa_append_grow' ≡ λ(a,n) x. do {
a' ← pfa_ensure (a,n) (n+1);
a'' ← pfa_append a' x;
return a''
}"

lemma pfa_append_grow'_rule[sep_heap_rules]: "
<is_pfa c l (a,n)>
pfa_append_grow' (a,n) x
<λ(a',n'). is_pfa (max (n+1) c) (l@[x]) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
unfolding pfa_append_grow'_def
by (sep_auto simp add: max_def)

definition "pfa_insert ≡ λ(a,n) i x. do {
a' ← array_shr a i 1;
a'' ← Array.upd i x a;
return (a'',n+1)
}"

lemma list_update_last: "length ls = Suc i ⟹ ls[i:=x] = (take i ls)@[x]"
by (metis append_eq_conv_conj length_Suc_rev_conv list_update_length)

lemma pfa_insert_rule[sep_heap_rules]:
"⟦i ≤ n; n < c⟧ ⟹
<is_pfa c l (a,n)>
pfa_insert (a,n) i x
<λ(a',n'). is_pfa c (take i l@x#drop i l) (a',n') * ↑(n' = n+1 ∧ a=a')>"
unfolding pfa_insert_def is_pfa_def
by (sep_auto simp add: list_update_append1 list_update_last
Suc_diff_le drop_take min_def)

definition pfa_insert_grow ::  "'a::{heap,default} pfarray ⇒ nat ⇒ 'a ⇒ 'a pfarray Heap"
where "pfa_insert_grow ≡ λ(a,n) i x. do {
a' ← pfa_ensure (a,n) (n+1);
a'' ← pfa_insert a' i x;
return a''
}"

lemma pfa_insert_grow_rule:
"i ≤ n ⟹
<is_pfa c l (a,n)>
pfa_insert_grow (a,n) i x
<λ(a',n'). is_pfa (max c (n+1)) (take i l@x#drop i l) (a',n') * ↑(n'=n+1 ∧ c ≥ n)>⇩t"
unfolding pfa_insert_grow_def
by (sep_auto heap add: pfa_insert_rule[of i n "max c (Suc n)"])

definition pfa_extend where
"pfa_extend ≡ λ (a,n) (b,m). do{
blit b 0 a n m;
return (a,n+m)
}"

lemma pfa_extend_rule:
"n+m ≤ c ⟹
<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_extend (a,n) (b,m)
<λ(a',n'). is_pfa c (l1@l2) (a',n') * ↑(a' = a ∧ n'=n+m) * is_pfa d l2 (b,m)>⇩t"
unfolding pfa_extend_def
by (sep_auto simp add: is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)

definition pfa_extend_grow where
"pfa_extend_grow ≡ λ (a,n) (b,m). do{
a' ← array_ensure a (n+m) default;
blit b 0 a' n m;
return (a',n+m)
}"

lemma pfa_extend_grow_rule:
"<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_extend_grow (a,n) (b,m)
<λ(a',n'). is_pfa (max c (n+m)) (l1@l2) (a',n') * ↑(n'=n+m ∧ c ≥ n) * is_pfa d l2 (b,m)>⇩t"
unfolding pfa_extend_grow_def
by (sep_auto simp add: is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)

definition pfa_append_extend_grow where
"pfa_append_extend_grow ≡ λ (a,n) x (b,m). do{
a' ← array_ensure a (n+m+1) default;
a'' ← Array.upd n x a';
blit b 0 a'' (n+1) m;
return (a'',n+m+1)
}"

lemma pfa_append_extend_grow_rule:
"<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_append_extend_grow (a,n) x (b,m)
<λ(a',n'). is_pfa (max c (n+m+1)) (l1@x#l2) (a',n') * ↑(n'=n+m+1 ∧ c ≥ n) * is_pfa d l2 (b,m)>⇩t"
unfolding pfa_append_extend_grow_def
by (sep_auto simp add: list_update_last is_pfa_def min.absorb1 min.absorb2 heap add: blit_rule)

definition "pfa_delete ≡ λ(a,n) i. do {
array_shl a (i+1) 1;
return (a,n-1)
}"

lemma pfa_delete_rule[sep_heap_rules]:
"i < n ⟹
<is_pfa c l (a,n)>
pfa_delete (a,n) i
<λ(a',n'). is_pfa c (take i l@drop (i+1) l) (a',n') * ↑(n' = n-1 ∧ a=a')>"
unfolding pfa_delete_def is_pfa_def
apply (sep_auto simp add: drop_take min_def)
by (metis Suc_diff_Suc diff_zero dual_order.strict_trans2 le_less_Suc_eq zero_le)

end

# Theory Basic_Assn

theory Basic_Assn
imports
"Refine_Imperative_HOL.Sepref_HOL_Bindings"
"Refine_Imperative_HOL.Sepref_Basic"
begin

section "Auxilary imperative assumptions"

text "The following auxiliary assertion types and lemmas were provided by Peter Lammich"

subsection ‹List-Assn›

lemma list_assn_cong[fundef_cong]:
"⟦ xs=xs'; ys=ys'; ⋀x y. ⟦ x∈set xs; y∈set ys ⟧ ⟹ A x y = A' x y ⟧ ⟹ list_assn A xs ys = list_assn A' xs' ys'"
by (induction xs ys arbitrary: xs' ys' rule: list_assn.induct) auto

lemma list_assn_app_one: "list_assn P (l1@[x]) (l1'@[y]) = list_assn P l1 l1' * P x y"
by simp

(* ------------------ ADDED by NM in course of btree_imp -------- *)

lemma list_assn_len: "h ⊨ list_assn A xs ys ⟹ length xs = length ys"
using list_assn_aux_ineq_len by fastforce

lemma list_assn_append_Cons_left: "list_assn A (xs@x#ys) zs = (∃⇩A zs1 z zs2. list_assn A xs zs1 * A x z * list_assn A ys zs2 * ↑(zs1@z#zs2 = zs))"
by (sep_auto simp add: list_assn_aux_cons_conv list_assn_aux_append_conv1 intro!: ent_iffI)

lemma list_assn_aux_append_Cons:
shows "length xs = length zsl ⟹ list_assn A (xs@x#ys) (zsl@z#zsr) = (list_assn A xs zsl * A x z * list_assn A ys zsr) "
by (sep_auto simp add: mult.assoc)

(* -------------------------------------------- *)

subsection ‹Prod-Assn›

lemma prod_assn_cong[fundef_cong]:
"⟦ p=p'; pi=pi'; A (fst p) (fst pi) = A' (fst p) (fst pi); B (snd p) (snd pi) = B' (snd p) (snd pi) ⟧
⟹ (A×⇩aB) p pi = (A'×⇩aB') p' pi'"
apply (cases p; cases pi)
by auto

end

# Theory BTree_Imp

theory BTree_Imp
imports
BTree
Partially_Filled_Array
Basic_Assn
begin

section "Imperative B-tree Definition"

text "The heap data type definition. Anything stored on the heap always contains data,
leafs are represented as None."

datatype 'a btnode =
Btnode "('a btnode ref option*'a) pfarray" "'a btnode ref option"

text ‹Selector Functions›
primrec kvs :: "'a::heap btnode ⇒ ('a btnode ref option*'a) pfarray" where
[sep_dflt_simps]: "kvs (Btnode ts _) = ts"

primrec last :: "'a::heap btnode ⇒ 'a btnode ref option" where
[sep_dflt_simps]: "last (Btnode _ t) = t"

term arrays_update

text ‹Encoding to natural numbers, as required by Imperative/HOL›
(* Note: should also work using the package "Deriving" *)
fun
btnode_encode :: "'a::heap btnode ⇒ nat"
where
"btnode_encode (Btnode ts t) = to_nat (ts, t)"

instance btnode :: (heap) heap
apply (rule heap_class.intro)
apply (rule countable_classI [of "btnode_encode"])
apply (metis btnode_encode.elims from_nat_to_nat fst_conv snd_conv)
..

text "The refinement relationship to abstract B-trees."

fun btree_assn :: "nat ⇒ 'a::heap btree ⇒ 'a btnode ref option ⇒ assn" where
"btree_assn k Leaf None = emp" |
"btree_assn k (Node ts t) (Some a) =
(∃⇩A tsi ti tsi'.
a ↦⇩r Btnode tsi ti
* btree_assn k t ti
* is_pfa (2*k) tsi' tsi
* list_assn ((btree_assn k) ×⇩a id_assn) ts tsi'
)" |
"btree_assn _ _ _ = false"

text "With the current definition of deletion, we would
also need to directly reason on nodes and not only on references
to them."

fun btnode_assn :: "nat ⇒ 'a::heap btree ⇒ 'a btnode ⇒ assn" where
"btnode_assn k (Node ts t) (Btnode tsi ti) =
(∃⇩A tsi'.
btree_assn k t ti
* is_pfa (2*k) tsi' tsi
* list_assn ((btree_assn k) ×⇩a id_assn) ts tsi'
)" |
"btnode_assn _ _ _ = false"

abbreviation "blist_assn k ≡ list_assn ((btree_assn k) ×⇩a id_assn)"

end

# 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)

(* auxiliary lemmas on assns *)
(* simp? not sure if it always makes things more easy *)
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

(* concrete *)
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"

datatype 'b btupi =
T⇩i "'b btnode ref option" |
Up⇩i "'b btnode ref option" "'b" "'b btnode ref option"

fun btupi_assn where
"btupi_assn k (abs_split.T⇩i l) (T⇩i li) =
btree_assn k l li" |
"btupi_assn k (abs_split.Up⇩i l a r) (Up⇩i li ai ri) =
btree_assn k l li * id_assn a ai * btree_assn k r ri" |
"btupi_assn _ _ _ = false"

definition node⇩i :: "nat ⇒ ('a btnode ref option × 'a) pfarray ⇒ 'a btnode ref option ⇒ 'a btupi Heap" where
"node⇩i k a ti ≡ do {
n ← pfa_length a;
if n ≤ 2*k then do {
a' ← pfa_shrink_cap (2*k) a;
l ← ref (Btnode a' ti);
return (T⇩i (Some l))
}
else do {
b ← (pfa_empty (2*k) :: ('a btnode ref option × 'a) pfarray Heap);
i ← split_half a;
m ← pfa_get a i;
b' ← pfa_drop a (i+1) b;
a' ← pfa_shrink i a;
a'' ← pfa_shrink_cap (2*k) a';
let (sub,sep) = m in do {
l ← ref (Btnode a'' sub);
r ← ref (Btnode b' ti);
return (Up⇩i (Some l) sep (Some r))
}
}
}"

partial_function (heap) ins :: "nat ⇒ 'a ⇒ 'a btnode ref option ⇒ 'a btupi Heap"
where
"ins k x apo = (case apo of
None ⇒
return (Up⇩i None x None) |
(Some ap) ⇒ do {
a ← !ap;
i ← imp_split (kvs a) x;
tsl ← pfa_length (kvs a);
if i < tsl then do {
s ← pfa_get (kvs a) i;
let (sub,sep) = s in
if sep = x then
return (T⇩i apo)
else do {
r ← ins k x sub;
case r of
(T⇩i lp) ⇒ do {
pfa_set (kvs a) i (lp,sep);
return (T⇩i apo)
} |
(Up⇩i lp x' rp) ⇒ do {
pfa_set (kvs a) i (rp,sep);
if tsl < 2*k then do {
kvs' ← pfa_insert (kvs a) i (lp,x');
ap := (Btnode kvs' (last a));
return (T⇩i apo)
} else do {
kvs' ← pfa_insert_grow (kvs a) i (lp,x');
node⇩i k kvs' (last a)
}
}
}
}
else do {
r ← ins k x (last a);
case r of
(T⇩i lp) ⇒ do {
ap := (Btnode (kvs a) lp);
return (T⇩i apo)
} |
(Up⇩i lp x' rp) ⇒
if tsl < 2*k then do {
kvs' ← pfa_append (kvs a) (lp,x');
ap := (Btnode kvs' rp);
return (T⇩i apo)
} else do {
kvs' ← pfa_append_grow' (kvs a) (lp,x');
node⇩i k kvs' rp
}
}
}
)"

(*fun tree⇩i::"'a up⇩i ⇒ 'a btree" where
"tree⇩i (T⇩i sub) = sub" |
"tree⇩i (Up⇩i l a r) = (Node [(l,a)] r)"

fun insert::"nat ⇒ 'a ⇒ 'a btree ⇒ 'a btree" where
"insert k x t = tree⇩i (ins k x t)"
*)

definition insert :: "nat ⇒ ('a::{heap,default,linorder}) ⇒ 'a btnode ref option ⇒ 'a btnode ref option Heap" where
"insert ≡ λk x ti. do {
ti' ← ins k x ti;
case ti' of
T⇩i sub ⇒ return sub |
Up⇩i l a r ⇒ do {
kvs ← pfa_init (2*k) (l,a) 1;
t' ← ref (Btnode kvs r);
return (Some t')
}
}"

subsection "Deletion"

text "Note that the below operations have not been verified to
refine the abstract set operations."

(* rebalance middle tree gets a list of trees, an index pointing to
the position of sub/sep and a last tree *)
definition rebalance_middle_tree:: "nat ⇒ (('a::{default,heap,linorder}) btnode ref option × 'a) pfarray ⇒ nat ⇒ 'a btnode ref option ⇒ 'a btnode Heap"
where
"rebalance_middle_tree ≡ λ k tsi i r_ti. (
case r_ti of
None ⇒ do {
return (Btnode tsi r_ti)
} |
Some p_t ⇒ do {
ti ← !p_t;
(r_sub,sep) ← pfa_get tsi i;
case r_sub of (Some p_sub) ⇒  do {
sub ← !p_sub;
l_sub ← pfa_length (kvs sub);
l_tts ← pfa_length (kvs ti);
if l_sub ≥ k ∧ l_tts ≥ k then do {
return (Btnode tsi r_ti)
} else do {
l_tsi ← pfa_length tsi;
if l_tsi = i then do {
mts' ← pfa_append_extend_grow (kvs sub) (last sub,sep) (kvs ti);
res_node⇩i ← node⇩i k mts' (last ti);
case res_node⇩i of
T⇩i u ⇒ return (Btnode tsi u) |
Up⇩i l a r ⇒ do {
tsi' ← pfa_append tsi (l,a);
return (Btnode tsi' r)
}
} else do {
(r_rsub,rsep) ← pfa_get tsi (i+1);
case r_rsub of Some p_rsub ⇒ do {
rsub ← !p_rsub;
mts' ← pfa_append_extend_grow (kvs sub) (last sub,sep) (kvs rsub);
res_node⇩i ← node⇩i k mts' (last rsub);
case res_node⇩i of
T⇩i u ⇒ do {
tsi' ← pfa_set tsi (i+1) (u,rsep);
tsi'' ← pfa_delete tsi' i;
return (Btnode tsi'' r_ti)
} |
Up⇩i l a r ⇒ do {
tsi' ← pfa_set tsi i (l,a);
tsi'' ← pfa_set tsi' (i+1) (r,rsep);
return (Btnode tsi'' r_ti)
}
}
}
}
}
})
"

definition rebalance_last_tree:: "nat ⇒ (('a::{default,heap,linorder}) btnode ref option × 'a) pfarray ⇒ 'a btnode ref option ⇒ 'a btnode Heap"
where
"rebalance_last_tree ≡ λk tsi ti. do {
l_tsi ← pfa_length tsi;
rebalance_middle_tree k tsi (l_tsi-1) ti
}"

partial_function (heap) split_max ::"nat ⇒ ('a::{default,heap,linorder}) btnode ref option ⇒ ('a btnode ref option × 'a) Heap"
where
"split_max k r_t = (case r_t of Some p_t ⇒ do {
t ← !p_t;
(case t of Btnode tsi r_ti ⇒
case r_ti of None ⇒ do {
(sub,sep) ← pfa_last tsi;
tsi' ← pfa_butlast tsi;
p_t := Btnode tsi' sub;
return (Some p_t, sep)
} |
_ ⇒ do {
(sub,sep) ← split_max k r_ti;
p_t' ← rebalance_last_tree k tsi sub;
p_t := p_t';
return (Some p_t, sep)
})
})
"

partial_function (heap) del ::"nat ⇒ 'a ⇒ ('a::{default,heap,linorder}) btnode ref option ⇒ 'a btnode ref option Heap"
where
"del k x ti = (case ti of None ⇒ return None |
Some p ⇒ do {
node ← !p;
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 do {
sub' ← del k x sub;
kvs' ← pfa_set (kvs node) i (sub',sep);
node' ← rebalance_middle_tree k kvs' i (last node);
ti' ← ref node';
return (Some ti')
}
else if sub = None then do{
pfa_delete (kvs node) i;
return ti
}
else do {
sm ← split_max k sub;
kvs' ← pfa_set (kvs node) i sm;
node' ← rebalance_middle_tree k kvs' i (last node);
ti' ← ref node';
return (Some ti')
}
} else do {
t' ← del k x (last node);
node' ← rebalance_last_tree k (kvs node) t';
ti' ← ref node';
return (Some ti')
}
})
"

partial_function (heap) reduce_root ::"('a::{default,heap,linorder}) btnode ref option ⇒ 'a btnode ref option Heap"
where
"reduce_root ti = (case ti of
None ⇒ return None |
Some p_t ⇒ do {
node ← !p_t;
tsl ← pfa_length (kvs node);
case tsl of 0 ⇒ return (last node) |
_ ⇒ return ti
})"

partial_function (heap) delete ::"nat ⇒ 'a ⇒ ('a::{default,heap,linorder}) btnode ref option ⇒ 'a btnode ref option Heap"
where
"delete k x ti = do {
ti' ← del k x ti;
reduce_root ti'
}"

subsection "Refinement of the abstract B-tree operations"

definition empty ::"('a::{default,heap,linorder}) btnode ref option Heap"
where "empty = return None"

lemma P_imp_Q_implies_P: "P ⟹ (Q ⟶ P)"
by simp

lemma  "sorted_less (inorder t) ⟹
<btree_assn k t ti>
isin ti x
<λr. btree_assn k t ti * ↑(abs_split.isin t x = r)>⇩t"
proof(induction t x arbitrary: ti rule: abs_split.isin.induct)
case (1 x)
then show ?case
apply(subst isin.simps)
apply (cases ti)
apply (auto simp add: return_cons_rule)
done
next
case (2 ts t x)
then obtain ls rs where list_split[simp]: "split ts x = (ls,rs)"
by (cases "split ts x")
then show ?case
proof (cases rs)
(* NOTE: induction condition trivial here *)
case [simp]: Nil
show ?thesis
apply(subst isin.simps)
apply(sep_auto)
using "2.prems" sorted_inorder_separators apply blast
apply(auto simp add: split_relation_def dest!: sym[of "[]"] mod_starD list_assn_len)[]
apply(rule hoare_triple_preI)
apply(auto simp add: split_relation_def dest!: sym[of "[]"] 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)
show ?thesis
proof (cases "sep = x")
(* NOTE: no induction required here, only vacuous counter cases generated *)
case [simp]: True
then show ?thesis
apply(simp split: list.splits prod.splits)
apply(subst isin.simps)
using "2.prems" sorted_inorder_separators apply(sep_auto)
apply(rule hoare_triple_preI)
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!: mod_starD list_assn_len)[]
apply(rule hoare_triple_preI)
apply(auto simp add: split_relation_def dest!: sym[of "[]"] mod_starD list_assn_len)[]
done
next
case [simp]: False
show ?thesis
apply(simp split: list.splits prod.splits)
apply safe
using False apply simp
apply(subst isin.simps)
using "2.prems" sorted_inorder_separators
apply(sep_auto)
(*eliminate vacuous case*)
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!:  mod_starD list_assn_len)[]
(* simplify towards induction step *)
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!: mod_starD list_assn_len)[]

(* NOTE show that z = (suba, sepa) *)
apply(rule norm_pre_ex_rule)+
apply(rule hoare_triple_preI)
subgoal for p tsi n ti xsi suba sepa zs1 z zs2 _
apply(subgoal_tac "z = (suba, sepa)", simp)
using 2(3) apply(sep_auto
heap:"2.IH"(2)[of ls rs h rrs sub sep]
simp add: sorted_wrt_append)
using list_split Cons h_split apply simp_all
(* proof that previous assumptions hold later *)
apply(rule P_imp_Q_implies_P)
apply(rule ent_ex_postI[where x="(tsi,n)"])
apply(rule ent_ex_postI[where x="ti"])
apply(rule ent_ex_postI[where x="(zs1 @ (suba, sepa) # zs2)"])
apply(rule ent_ex_postI[where x="zs1"])
apply(rule ent_ex_postI[where x="z"])
apply(rule ent_ex_postI[where x="zs2"])
apply sep_auto
(* prove subgoal_tac assumption *)
apply (metis (no_types, lifting) list_assn_aux_ineq_len list_assn_len nth_append_length star_false_left star_false_right)
done
(* eliminate last vacuous case *)
apply(rule hoare_triple_preI)
apply(auto simp add: split_relation_def dest!: mod_starD list_assn_len)[]
done
qed
qed
qed

declare abs_split.node⇩i.simps [simp add]
lemma node⇩i_rule: assumes c_cap: "2*k ≤ c" "c ≤ 4*k+1"
shows "<is_pfa c tsi (a,n) * list_assn ((btree_assn k) ×⇩a id_assn) ts tsi * btree_assn k t ti>
node⇩i k (a,n) ti
<λr. btupi_assn k (abs_split.node⇩i k ts t) r >⇩t"
proof (cases "length ts ≤ 2*k")
case [simp]: True
then show ?thesis
apply(subst node⇩i_def)
apply(rule hoare_triple_preI)
apply(sep_auto dest!: mod_starD list_assn_len)
apply(sep_auto simp add: is_pfa_def)[]
using c_cap apply(sep_auto simp add: is_pfa_def)[]
apply(sep_auto  dest!: mod_starD list_assn_len)[]
using True apply(sep_auto dest!: mod_starD list_assn_len)
done
next
case [simp]: False
then obtain ls sub sep rs where
split_half_eq: "BTree_Set.split_half ts = (ls,(sub,sep)#rs)"
using abs_split.node⇩i_cases by blast
then show ?thesis
apply(subst node⇩i_def)
apply(rule hoare_triple_preI)
apply(sep_auto dest!: mod_starD list_assn_len)
apply(sep_auto simp add:  split_relation_alt split_relation_length is_pfa_def dest!: mod_starD list_assn_len)

using False apply(sep_auto simp add: split_relation_alt )
using False  apply(sep_auto simp add: is_pfa_def)[]
apply(sep_auto)[]
apply(sep_auto simp add: is_pfa_def split_relation_alt)[]
using c_cap apply(sep_auto simp add: is_pfa_def)[]
apply(sep_auto)[]
using c_cap apply(sep_auto simp add: is_pfa_def)[]
using c_cap apply(simp)
apply(vcg)
apply(simp)
apply(rule impI)
subgoal for  _ _ _ _ rsa subi ba rn lsi al ar _
thm ent_ex_postI
thm ent_ex_postI[where x="take (length tsi div 2) tsi"]
(* instantiate right hand side *)
apply(rule ent_ex_postI[where x="(rsa,rn)"])
apply(rule ent_ex_postI[where x="ti"])
apply(rule ent_ex_postI[where x="(drop (Suc (length tsi div 2)) tsi)"])
apply(rule ent_ex_postI[where x="lsi"])
apply(rule ent_ex_postI[where x="subi"])
apply(rule ent_ex_postI[where x="take (length tsi div 2) tsi"])
(* introduce equality between equality of split tsi/ts and original lists *)
apply(simp add: split_relation_alt)
apply(subgoal_tac "tsi =
take (length tsi div 2) tsi @ (subi, ba) # drop (Suc (length tsi div 2)) tsi")
apply(rule back_subst[where a="blist_assn k ts (take (length tsi div 2) tsi @ (subi, ba) # (drop (Suc (length tsi div 2)) tsi))" and b="blist_assn k ts tsi"])
apply(rule back_subst[where a="blist_assn k (take (length tsi div 2) ts @ (sub, sep) # rs)" and b="blist_assn k ts"])
apply(subst list_assn_aux_append_Cons)
apply sep_auto
apply sep_auto
apply simp
apply simp
apply(rule back_subst[where a="tsi ! (length tsi div 2)" and b="(subi, ba)"])
apply(rule id_take_nth_drop)
apply simp
apply simp
done
done
qed
declare abs_split.node⇩i.simps [simp del]

lemma node⇩i_no_split: "length ts ≤ 2*k ⟹ abs_split.node⇩i k ts t = abs_split.T⇩i (Node ts t)"
by (simp add: abs_split.node⇩i.simps)

lemma node⇩i_rule_app: "⟦2*k ≤ c; c ≤ 4*k+1⟧ ⟹
<is_pfa c (tsi' @ [(li, ai)]) (aa, al) *
blist_assn k ls tsi' *
btree_assn k l li *
id_assn a ai *
btree_assn k r ri> node⇩i k (aa, al) ri
<btupi_assn k (abs_split.node⇩i k (ls @ [(l, a)]) r)>⇩t"
proof -
note node⇩i_rule[of k c "(tsi' @ [(li, ai)])" aa al "(ls @ [(l, a)])" r ri]
moreover assume "2*k ≤ c" "c ≤ 4*k+1"
ultimately show ?thesis
by (simp add: mult.left_assoc)
qed

lemma node⇩i_rule_ins2: "⟦2*k ≤ c; c ≤ 4*k+1; length ls = length lsi⟧ ⟹
<is_pfa c (lsi @ (li, ai) # (ri,a'i) # rsi) (aa, al) *
blist_assn k ls lsi *
btree_assn k l li *
id_assn a ai *
btree_assn k r ri *
id_assn a' a'i *
blist_assn k rs rsi *
btree_assn k t ti> node⇩i k (aa, al)
ti <btupi_assn k (abs_split.node⇩i k (ls @ (l, a) # (r,a') # rs) t)>⇩t"
proof -
assume [simp]: "2*k ≤ c" "c ≤ 4*k+1" "length ls = length lsi"
moreover note node⇩i_rule[of k c "(lsi @ (li, ai) # (ri,a'i) # rsi)" aa al "(ls @ (l, a) # (r,a') # rs)" t ti]
ultimately show ?thesis
by (simp add: mult.left_assoc list_assn_aux_append_Cons)
qed

lemma ins_rule:
"sorted_less (inorder t) ⟹ <btree_assn k t ti>
ins k x ti
<λr. btupi_assn k (abs_split.ins k x t) r>⇩t"
proof (induction k x t arbitrary: ti rule: abs_split.ins.induct)
case (1 k x)
then show ?case
apply(subst ins.simps)
apply (sep_auto simp add: pure_app_eq)
done
next
case (2 k x ts t)
obtain ls rrs where list_split: "split ts x = (ls,rrs)"
by (cases "split ts x")
have [simp]: "sorted_less (separators ts)"
using "2.prems" sorted_inorder_separators by simp
have [simp]: "sorted_less (inorder t)"
using "2.prems" sorted_inorder_induct_last by simp
show ?case
proof (cases rrs)
case Nil
then show ?thesis
proof (cases "abs_split.ins k x t")
case (T⇩i a)
then show ?thesis
apply(subst ins.simps)
apply(sep_auto)
subgoal for p tsil tsin tti
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi' i tsin' _ sub sep
apply(rule hoare_triple_preI)
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi'
thm "2.IH"(1)[of ls rrs tti]
using Nil list_split T⇩i apply(sep_auto split!: list.splits simp add: split_relation_alt
heap add: "2.IH"(1)[of ls rrs tti])
subgoal for ai
apply(cases ai)
apply sep_auto
apply sep_auto
done
done
done
next
case (Up⇩i l a r)
then show ?thesis
apply(subst ins.simps)
apply(sep_auto)
subgoal for p tsil tsin tti
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi' i tsin' _ sub sep
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi' i tsin'
thm "2.IH"(1)[of ls rrs tti]
using Nil list_split Up⇩i apply(sep_auto split!: list.splits
simp add: split_relation_alt
heap add: "2.IH"(1)[of ls rrs tti])
subgoal for ai
apply(cases ai)
apply sep_auto
apply(rule hoare_triple_preI)
apply(sep_auto)
apply(auto dest!: mod_starD simp add: is_pfa_def)[]
apply (sep_auto)
subgoal for li ai ri (* no split case *)
apply(subgoal_tac "length (ls @ [(l,a)]) ≤ 2*k")
apply(simp add: node⇩i_no_split)
apply(rule ent_ex_postI[where x="(tsil,Suc tsin)"])
apply(rule ent_ex_postI[where x="ri"])
apply(rule ent_ex_postI[where x="tsi' @ [(li, ai)]"])
apply(sep_auto)
apply (sep_auto dest!: mod_starD list_assn_len simp add: is_pfa_def)
done
(* split case*)
apply(sep_auto heap add: node⇩i_rule_app)
done
done
done
qed
next
case (Cons a rs)
obtain sub sep where a_split: "a = (sub,sep)"
by (cases a)
then have [simp]: "sorted_less (inorder sub)"
using "2.prems" abs_split.split_axioms list_split Cons sorted_inorder_induct_subtree split_def
by fastforce
then show ?thesis
proof(cases "x = sep")
case True
show ?thesis
apply(subst ins.simps)
apply(sep_auto)
subgoal for p tsil tsin tti tsi j subi
using Cons list_split a_split True
by sep_auto
subgoal for p tsil tsin tti tsi j _ _ subi sepi
apply(rule hoare_triple_preI)
using Cons list_split a_split True
apply(subgoal_tac "sepi = sep")
apply (sep_auto simp add: split_relation_alt)
apply(sep_auto simp add: list_assn_prod_map dest!: mod_starD id_assn_list)
by (metis length_map snd_conv snd_map_help(2) split_relation_access)
subgoal for p tsil tsin tti tsi j
apply(rule hoare_triple_preI)
using Cons list_split
by (sep_auto simp add: split_relation_alt dest!: mod_starD list_assn_len)
done
next
case False
then show ?thesis
proof (cases "abs_split.ins k x sub")
case (T⇩i a')
then show ?thesis
apply(auto simp add: Cons list_split a_split False)
using False apply simp
apply(subst ins.simps)
apply vcg
apply auto
apply(rule norm_pre_ex_rule)+
(* at this point, we want to introduce the split, and after that tease the
hoare triple assumptions out of the bracket, s.t. we don't split twice *)
apply vcg
apply sep_auto
using list_split Cons
apply(simp add: split_relation_alt list_assn_append_Cons_left)
apply (rule impI)
apply(rule norm_pre_ex_rule)+
apply(rule hoare_triple_preI)
apply sep_auto
(* discard wrong branch *)
subgoal for p tsil tsin ti zs1 subi sepi zs2 _ _ suba
apply(subgoal_tac "sepi  = x")
using list_split Cons a_split
apply(auto  dest!:  mod_starD )[]
apply(auto dest!:  mod_starD list_assn_len)[]
done
(* actual induction branch *)
subgoal for p tsil tsin ti zs1 subi sepi zs2 _ _ n z suba sepa
apply (cases a, simp)
apply(subgoal_tac "subi = suba", simp)
using list_split a_split T⇩i False
apply (vcg heap: 2)
apply(auto split!: btupi.splits)
(* careful progression for manual value insertion *)
apply vcg
apply simp
apply vcg
apply simp
subgoal for a'i q r
apply(rule impI)
apply(simp add: list_assn_append_Cons_lef`