Session BTree

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 + (tsubtrees 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 upi = Ti "'b btree" | Upi "'b btree" 'b "'b btree"

fun order_upi where
  "order_upi k (Ti sub) = order k sub" |
  "order_upi k (Upi l a r) = (order k l  order k r)"

fun root_order_upi where
  "root_order_upi k (Ti sub) = root_order k sub" |
  "root_order_upi k (Upi l a r) = (order k l  order k r)"


fun height_upi where
  "height_upi (Ti t) = height t" |
  "height_upi (Upi l a r) = max (height l) (height r)"

fun bal_upi where
  "bal_upi (Ti t) = bal t" |
  "bal_upi (Upi l a r) = (height l = height r  bal l  bal r)"

fun inorder_upi where
  "inorder_upi (Ti t) = inorder t" |
  "inorder_upi (Upi 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 nodei:: "nat  ('a btree × 'a) list  'a btree  'a upi" where
  "nodei k ts t = (
  if length ts  2*k then Ti (Node ts t)
  else (
    case split_half ts of (ls, (sub,sep)#rs) 
      Upi (Node ls sub) sep (Node rs t)
    )
  )"


fun ins:: "nat  'a  'a btree  'a upi" where
  "ins k x Leaf = (Upi Leaf x Leaf)" |
  "ins k x (Node ts t) = (
  case split ts x of
    (ls,(sub,sep)#rs) 
      (if sep = x then
        Ti (Node ts t)
      else
        (case ins k x sub of
          Upi l a r 
             nodei k (ls @ (l,a)#(r,sep)#rs) t |
          Ti a 
            Ti (Node (ls @ (a,sep) # rs) t))) |
    (ls, []) 
      (case ins k x t of
         Upi l a r 
           nodei k (ls@[(l,a)]) r |
         Ti a 
           Ti (Node ls a)
  )
)"



fun treei::"'a upi  'a btree" where
  "treei (Ti sub) = sub" |
  "treei (Upi l a r) = (Node [(l,a)] r)"

fun insert::"nat  'a  'a btree  'a btree" where
  "insert k x t = treei (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 nodei k (mts@(mt,sep)#tts) tt of
       Ti u 
        Node ls u |
       Upi l a r 
        Node (ls@[(l,a)]) r) |
    (Node rts rt,rsep)#rs  (
      case nodei k (mts@(mt,sep)#rts) rt of
      Ti u 
        Node (ls@(u,rsep)#rs) (Node tts tt) |
      Upi 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 nodei_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_treei: "root_order_upi (Suc k) t = root_order (Suc k) (treei t)"
  apply (cases t)
   apply auto
  done

lemma nodei_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_upi k (nodei k ts t)"
proof (cases "length ts  2*k")
  case True
  then show ?thesis
    using assms
    by (simp add: nodei.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: nodei.simps False split_half_ts)
qed

lemma nodei_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 (nodei k ts t) of Ti t  order k t | _  True"
proof (cases "length ts  2*k")
  case True
  then show ?thesis
    using assms
    by (simp add: nodei.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: nodei.simps)
qed


lemma nodei_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_upi k (nodei k ts t)"

  apply(cases "nodei k ts t")
  using nodei_root_order nodei_order_helper assms apply fastforce
  apply (metis nodei_root_order assms(2,3,4) le0 length_greater_0_conv
      list.size(3) nodei.simps order_upi.simps(2) root_order_upi.simps(2) upi.distinct(1))
  done

(* explicit proof *)
lemma ins_order:
  "order k t  order_upi 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_upi k (ins k x t)"
      using 2 split_res
      by simp
    then show ?thesis
      using Nil 2 split_app split_res Nil nodei_order
      by (auto split!: upi.splits simp del: nodei.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_upi 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 nodei_order a_prod split_res
        by (auto split!: upi.splits simp del: nodei.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_upi 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_upi 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 nodei_root_order
      by (auto split!: upi.splits simp del: nodei.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_upi 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 nodei_root_order a_prod split_res
        by (auto split!: upi.splits simp del: nodei.simps simp add: order_impl_root_order)
    qed
  qed
qed simp



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

lemma nodei_height: "height_upi (nodei 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 nodei_cases)
  then have "nodei k ts t = Upi (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_upi_tree: "bal_upi t = bal (treei t)"
  apply(cases t)
   apply auto
  done

lemma bal_list_split: "bal (Node (ls@(a,b)#rs) t)  bal_upi (Upi (Node ls a) b (Node rs t))"
  by (auto simp add: image_constant_conv)

lemma nodei_bal:
  assumes "bal (Node ts t)"
  shows "bal_upi (nodei 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 nodei_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_upi.simps dest!: bal_list_split[of ls sub sep rs t])
qed simp

lemma height_upi_merge: "height_upi (Upi 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_upi (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_upi (ins k x t) = height t"
      using 2 by (simp add: split_list)
    then show ?thesis
    proof (cases "ins k x t")
      case (Ti a)
      then have "height (Node ts t) = height (Node ts a)"
        using height_sub
        by simp
      then show ?thesis
        using Ti Nil split_list split_append
        by simp
    next
      case (Upi 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 Upi split_append
        by (simp del: nodei.simps add: nodei_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_upi (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 (Ti 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 Ti 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 (Upi l a r)
        then have "height (Node (ls@(sub,sep)#list) t) = height (Node (ls@(l,a)#(r,sep)#list) t)"
          using height_upi_merge height_sub
          by fastforce
        then show ?thesis
          using Upi False Cons 2 split_list a_split split_append
          by (auto simp del: nodei.simps simp add: nodei_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_upi (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 (Ti a)
      then have "bal (Node ls a)" unfolding bal.simps
        by (metis "2.IH"(1) "2.prems" append_Nil2 bal.simps(2) bal_upi.simps(1) height_upi.simps(1) ins_height local.Nil split_app split_res)
      then show ?thesis
        using Nil Ti 2 split_res
        by simp
    next
      case (Upi l a r)
      then have
        "(xset (subtrees (ls@[(l,a)])). bal x)"
        "(xset (subtrees ls). height r = height x)"
        using 2 Upi Nil split_res split_app
        by simp_all (metis height_upi.simps(2) ins_height max_def)
      then show ?thesis unfolding ins.simps
        using Upi Nil 2 split_res
        by (simp del: nodei.simps add: nodei_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_upi (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 (Ti 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_upi.simps(1) ins_height local.Cons plus_1_eq_Suc split_app)
        then show ?thesis
          using split_app Cons Ti 2 split_res a_prod
          by auto
      next
        case (Upi 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 Upi split_app Cons 2 ‹bal_upi (ins k x sub) by auto
        moreover have "x  set (subtrees (ls@(l,a)#(r,sep)#list)). height x = height t"
          using False Upi split_app Cons 2 ‹bal_upi (ins k x sub) ins_height split_res a_prod
          apply auto
          by (metis height_upi.simps(2) sup.idem sup_nat_def)
        ultimately show ?thesis using Upi Cons 2 split_res a_prod
          by (simp del: nodei.simps add: nodei_bal)
      qed
    qed
  qed
qed simp

(* ins acts as ins_list wrt inorder *)

(* "simple enough" to be automatically solved *)
lemma nodei_inorder: "inorder_upi (nodei 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 nodei_inorder_simps:
  "nodei k ts t = Ti t'  inorder t' = inorder (Node ts t)"
  "nodei k ts t = Upi l a r  inorder l @ a # inorder r = inorder (Node ts t)"
   apply (metis inorder_upi.simps(1) nodei_inorder)
  by (metis append_Cons inorder_upi.simps(2) nodei_inorder self_append_conv2)


lemma ins_sorted_inorder: "sorted_less (inorder t)  (inorder_upi (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 upi.splits simp del: nodei.simps
      simp add:  nodei_inorder nodei_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 nodei.simps [simp del]
declare nodei_inorder [simp add]

lemma ins_inorder: "sorted_less (inorder t)  (inorder_upi (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 (Ti 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_upi (ins k x (Node ts t)) = inorder_list ls @ inorder a"
        using list_split Ti 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 (Upi l a r)
      then have IH:"inorder_upi (Upi 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_upi (ins k x (Node ts t)) = inorder_list ls @ inorder_upi (Upi l a r)"
        using list_split Upi 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_upi (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 (Ti 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_upi (ins k x (Node ts t)) = inorder_list ls @ inorder a @ sep # inorder_list list @ inorder t"
          using h_split False list_split Ti 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 (Upi l a r)
        then have IH:"inorder_upi (Upi 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_upi (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 Upi 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 nodei.simps [simp add]
declare nodei_inorder [simp del]


thm ins.induct
thm btree.induct

(* wrapped up insert invariants *)

lemma treei_bal: "bal_upi u  bal (treei u)"
  apply(cases u)
   apply(auto)
  done

lemma treei_order: "k > 0; root_order_upi k u  root_order k (treei u)"
  apply(cases u)
   apply(auto simp add: order_impl_root_order)
  done

lemma treei_inorder: "inorder_upi u = inorder (treei u)"
  apply (cases u)
   apply auto
  done

lemma insert_bal: "bal t  bal (insert k x t)"
  using ins_bal
  by (simp add: treei_bal)

lemma insert_order: "k > 0; root_order k t  root_order k (insert k x t)"
  using ins_root_order
  by (simp add: treei_order)


lemma insert_inorder: "sorted_less (inorder t)  inorder (insert k x t) = ins_list x (inorder t)"
  using ins_inorder
  by (simp add: treei_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_upi (nodei k (mts@(mt,sep)#tts) tt) = height (Node (mts@(mt,sep)#tts) tt)"
        using nodei_height by blast
      also have " = max (height t) (height sub)"
        by (metis assms(1) height_upi.simps(2) height_list_split sub_node t_node)
      finally have height_max: "height_upi (nodei k (mts @ (mt, sep) # tts) tt) = max (height t) (height sub)" by simp
      then show ?thesis
      proof (cases "nodei k (mts@(mt,sep)#tts) tt")
        case (Ti 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 Ti
          by (simp add: sub_node t_node)
      next
        case (Upi 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 Upi 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_upi (nodei k (mts@(mt,sep)#rts) rt) = height (Node (mts@(mt,sep)#rts) rt)"
        using nodei_height by blast
      also have " = max (height rsub) (height sub)"
        by (metis r_node height_upi.simps(2) height_list_split max.commute sub_node)
      finally have height_max: "height_upi (nodei k (mts @ (mt, sep) # rts) rt) = max (height rsub) (height sub)" by simp
      then show ?thesis
      proof (cases "nodei k (mts@(mt,sep)#rts) rt")
        case (Ti u)
        then have "height u = max (height rsub) (height sub)"
          using height_max by simp
        then show ?thesis
          using Ti False Cons r_node a_split sub_node t_node by auto
      next
        case (Upi 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 Upi 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 upi.splits list.splits
      simp del: nodei.simps
      simp add: nodei_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_upi (Upi (Node as a) x (Node bs b))"
  shows "bal (Node (as@(a,x)#bs) b)"
proof -
  have "xset (subtrees (as @ (a, x) # bs)). bal x"
    using subtrees_split assms by auto
  moreover have "bal b"
    using assms by auto
  moreover have "xset (subtrees as)  {a}  set (subtrees bs). height x = height b"
    using assms height_bal_subtrees_merge
    unfolding bal_upi.simps
    by blast
  ultimately show ?thesis
    by auto
qed

lemma nodei_bal_upi:
  assumes "bal_upi (nodei 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 nodei_cases by blast
  then have "nodei k ts t = Upi (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_upi.simps)
qed simp

lemma nodei_bal_simp: "bal_upi (nodei k ts t) = bal (Node ts t)"
  using nodei_bal nodei_bal_upi 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_upi (nodei k (mts@(mt,sep)#tts) tt) = height (Node (mts@(mt,sep)#tts) tt)"
        using nodei_height by blast
      also have " = Suc (height tt)"
        by (metis height_bal_tree height_upi.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_upi (nodei k (mts@(mt,sep)#tts) tt) = height t" by simp
      moreover have "bal_upi (nodei k (mts@(mt,sep)#tts) tt)"
        by (metis bal_list_merge bal_upi.simps(2) nodei_bal sub_heights(1) sub_heights(2) sub_heights(3) sub_node t_node)
      ultimately show ?thesis
        apply (cases "nodei 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_upi (nodei k (mts@(mt,sep)#rts) rt) = height (Node (mts@(mt,sep)#rts) rt)"
        using nodei_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_upi.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_upi (nodei k (mts@(mt,sep)#rts) rt) = height rsub" .
      moreover have 2: "bal_upi (nodei k (mts@(mt,sep)#rts) rt)"
        by (metis bal_list_merge bal_upi.simps(2) nodei_bal r_node rsub_height(1) rsub_height(2) sub_heights(1) sub_heights(2) sub_node)
      ultimately show ?thesis
      proof (cases "nodei k (mts@(mt,sep)#rts) rt")
        case (Ti 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 Ti
          by (auto simp del: nodei.simps bal.simps)
      next
        case (Upi 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 Upi
          by (auto simp del: nodei.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_upi k (nodei k (mts@(mt,sep)#tts) tt)"
        using nodei_order[of k "mts@(mt,sep)#tts" tt] assms(1,3) t_node sub_node
        by (auto simp del: order_upi.simps nodei.simps)
      then show ?thesis
        apply(cases "nodei k (mts@(mt,sep)#tts) tt")
        using assms t_node sub_node False Nil apply (auto simp del: nodei.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_upi k (nodei k (mts@(mt,sep)#rts) rt)"
        using nodei_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_upi.simps nodei.simps)
      then show ?thesis
        apply(cases "nodei k (mts@(mt,sep)#rts) rt")
        using assms t_node sub_node False Cons r_split r_node apply (auto simp del: nodei.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_upi k (nodei k (mts@(mt,sep)#tts) tt)"
      using nodei_order[of k "mts@(mt,sep)#tts" tt] assms t_node sub_node
      by (auto simp del: order_upi.simps nodei.simps)
    then show ?thesis
      apply(cases "nodei k (mts@(mt,sep)#tts) tt")
      using assms t_node sub_node False Nil apply (auto simp del: nodei.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"
      "sset (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 nodei.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 "btreei  btree_ls_insert"
abbreviation "btreed  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
      btreei 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
      btreei k 1 (btreei 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
      btreed k 10 (btreei k 1 (btreei 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
      btreed k 3 (btreed k 10 (btreei k 1 (btreei 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 {
    lArray.len a;
    if ls 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 "
      < aala > 
        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.  xset xs; yset 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 = 
  Ti "'b btnode ref option" |
  Upi "'b btnode ref option" "'b" "'b btnode ref option"

fun btupi_assn where
  "btupi_assn k (abs_split.Ti l) (Ti li) =
   btree_assn k l li" |
  "btupi_assn k (abs_split.Upi l a r) (Upi li ai ri) =
   btree_assn k l li * id_assn a ai * btree_assn k r ri" |
  "btupi_assn _ _ _ = false"



definition nodei :: "nat  ('a btnode ref option × 'a) pfarray  'a btnode ref option  'a btupi Heap" where
  "nodei 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 (Ti (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 (Upi (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 (Upi 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 (Ti apo)
      else do {
        r  ins k x sub;
        case r of 
          (Ti lp)  do {
            pfa_set (kvs a) i (lp,sep);
            return (Ti apo)
          } |
          (Upi 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 (Ti apo)
            } else do {
              kvs'  pfa_insert_grow (kvs a) i (lp,x');
              nodei k kvs' (last a)
            }
          }
        }
      }
    else do {
      r  ins k x (last a);
      case r of 
        (Ti lp)  do {
          ap := (Btnode (kvs a) lp);
          return (Ti apo)
        } |
        (Upi lp x' rp)  
          if tsl < 2*k then do {
            kvs'  pfa_append (kvs a) (lp,x');
            ap := (Btnode kvs' rp);
            return (Ti apo)
          } else do {
            kvs'  pfa_append_grow' (kvs a) (lp,x');
            nodei k kvs' rp
        }
    }
  }
)"


(*fun treei::"'a upi ⇒ 'a btree" where
  "treei (Ti sub) = sub" |
  "treei (Upi l a r) = (Node [(l,a)] r)" 

fun insert::"nat ⇒ 'a ⇒ 'a btree ⇒ 'a btree" where
  "insert k x t = treei (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
     Ti sub  return sub |
     Upi 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_nodei  nodei k mts' (last ti);
          case res_nodei of
            Ti u  return (Btnode tsi u) |
            Upi 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_nodei  nodei k mts' (last rsub);
            case res_nodei of
             Ti u  do {
              tsi'  pfa_set tsi (i+1) (u,rsep);              
              tsi''  pfa_delete tsi' i;
              return (Btnode tsi'' r_ti)
            } |
             Upi 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.nodei.simps [simp add]
lemma nodei_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>
  nodei k (a,n) ti
  <λr. btupi_assn k (abs_split.nodei k ts t) r >t"
proof (cases "length ts  2*k")
  case [simp]: True
  then show ?thesis
    apply(subst nodei_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.nodei_cases by blast
  then show ?thesis
    apply(subst nodei_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.nodei.simps [simp del]


lemma nodei_no_split: "length ts  2*k  abs_split.nodei k ts t = abs_split.Ti (Node ts t)"
  by (simp add: abs_split.nodei.simps)


lemma nodei_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> nodei k (aa, al) ri
 <btupi_assn k (abs_split.nodei k (ls @ [(l, a)]) r)>t"
proof -
  note nodei_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 nodei_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> nodei k (aa, al)
          ti <btupi_assn k (abs_split.nodei 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 nodei_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 (Ti 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 Ti 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 (Upi 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 Upi 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: nodei_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: nodei_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 (Ti 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 Ti 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