Theory Tree234_Set

theory Tree234_Set
imports Tree234 Cmp Set_by_Ordered
(* Author: Tobias Nipkow *)

section ‹2-3-4 Tree Implementation of Sets›

theory Tree234_Set
imports
  Tree234
  Cmp
  "../Data_Structures/Set_by_Ordered"
begin

subsection ‹Set operations on 2-3-4 trees›

fun isin :: "'a::linorder tree234 ⇒ 'a ⇒ bool" where
"isin Leaf x = False" |
"isin (Node2 l a r) x =
  (case cmp x a of LT ⇒ isin l x | EQ ⇒ True | GT ⇒ isin r x)" |
"isin (Node3 l a m b r) x =
  (case cmp x a of LT ⇒ isin l x | EQ ⇒ True | GT ⇒ (case cmp x b of
   LT ⇒ isin m x | EQ ⇒ True | GT ⇒ isin r x))" |
"isin (Node4 t1 a t2 b t3 c t4) x =
  (case cmp x b of
     LT ⇒
       (case cmp x a of
          LT ⇒ isin t1 x |
          EQ ⇒ True |
          GT ⇒ isin t2 x) |
     EQ ⇒ True |
     GT ⇒
       (case cmp x c of
          LT ⇒ isin t3 x |
          EQ ⇒ True |
          GT ⇒ isin t4 x))"

datatype 'a upi = Ti "'a tree234" | Upi "'a tree234" 'a "'a tree234"

fun treei :: "'a upi ⇒ 'a tree234" where
"treei (Ti t) = t" |
"treei (Upi l a r) = Node2 l a r"

fun ins :: "'a::linorder ⇒ 'a tree234 ⇒ 'a upi" where
"ins x Leaf = Upi Leaf x Leaf" |
"ins x (Node2 l a r) =
   (case cmp x a of
      LT ⇒ (case ins x l of
              Ti l' => Ti (Node2 l' a r)
            | Upi l1 b l2 => Ti (Node3 l1 b l2 a r)) |
      EQ ⇒ Ti (Node2 l x r) |
      GT ⇒ (case ins x r of
              Ti r' => Ti (Node2 l a r')
            | Upi r1 b r2 => Ti (Node3 l a r1 b r2)))" |
"ins x (Node3 l a m b r) =
   (case cmp x a of
      LT ⇒ (case ins x l of
              Ti l' => Ti (Node3 l' a m b r)
            | Upi l1 c l2 => Upi (Node2 l1 c l2) a (Node2 m b r)) |
      EQ ⇒ Ti (Node3 l a m b r) |
      GT ⇒ (case cmp x b of
               GT ⇒ (case ins x r of
                       Ti r' => Ti (Node3 l a m b r')
                     | Upi r1 c r2 => Upi (Node2 l a m) b (Node2 r1 c r2)) |
               EQ ⇒ Ti (Node3 l a m b r) |
               LT ⇒ (case ins x m of
                       Ti m' => Ti (Node3 l a m' b r)
                     | Upi m1 c m2 => Upi (Node2 l a m1) c (Node2 m2 b r))))" |
"ins x (Node4 t1 a t2 b t3 c t4) =
  (case cmp x b of
     LT ⇒
       (case cmp x a of
          LT ⇒
            (case ins x t1 of
               Ti t => Ti (Node4 t a t2 b t3 c t4) |
               Upi l y r => Upi (Node2 l y r) a (Node3 t2 b t3 c t4)) |
          EQ ⇒ Ti (Node4 t1 a t2 b t3 c t4) |
          GT ⇒
            (case ins x t2 of
               Ti t => Ti (Node4 t1 a t b t3 c t4) |
               Upi l y r => Upi (Node2 t1 a l) y (Node3 r b t3 c t4))) |
     EQ ⇒ Ti (Node4 t1 a t2 b t3 c t4) |
     GT ⇒
       (case cmp x c of
          LT ⇒
            (case ins x t3 of
              Ti t => Ti (Node4 t1 a t2 b t c t4) |
              Upi l y r => Upi (Node2 t1 a t2) b (Node3 l y r c t4)) |
          EQ ⇒ Ti (Node4 t1 a t2 b t3 c t4) |
          GT ⇒
            (case ins x t4 of
              Ti t => Ti (Node4 t1 a t2 b t3 c t) |
              Upi l y r => Upi (Node2 t1 a t2) b (Node3 t3 c l y r))))"

hide_const insert

definition insert :: "'a::linorder ⇒ 'a tree234 ⇒ 'a tree234" where
"insert x t = treei(ins x t)"

datatype 'a upd = Td "'a tree234" | Upd "'a tree234"

fun treed :: "'a upd ⇒ 'a tree234" where
"treed (Td t) = t" |
"treed (Upd t) = t"

fun node21 :: "'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node21 (Td l) a r = Td(Node2 l a r)" |
"node21 (Upd l) a (Node2 lr b rr) = Upd(Node3 l a lr b rr)" |
"node21 (Upd l) a (Node3 lr b mr c rr) = Td(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
"node21 (Upd t1) a (Node4 t2 b t3 c t4 d t5) = Td(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"

fun node22 :: "'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a upd" where
"node22 l a (Td r) = Td(Node2 l a r)" |
"node22 (Node2 ll b rl) a (Upd r) = Upd(Node3 ll b rl a r)" |
"node22 (Node3 ll b ml c rl) a (Upd r) = Td(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
"node22 (Node4 t1 a t2 b t3 c t4) d (Upd t5) = Td(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"

fun node31 :: "'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node31 (Td t1) a t2 b t3 = Td(Node3 t1 a t2 b t3)" |
"node31 (Upd t1) a (Node2 t2 b t3) c t4 = Td(Node2 (Node3 t1 a t2 b t3) c t4)" |
"node31 (Upd t1) a (Node3 t2 b t3 c t4) d t5 = Td(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
"node31 (Upd t1) a (Node4 t2 b t3 c t4 d t5) e t6 = Td(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"

fun node32 :: "'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node32 t1 a (Td t2) b t3 = Td(Node3 t1 a t2 b t3)" |
"node32 t1 a (Upd t2) b (Node2 t3 c t4) = Td(Node2 t1 a (Node3 t2 b t3 c t4))" |
"node32 t1 a (Upd t2) b (Node3 t3 c t4 d t5) = Td(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
"node32 t1 a (Upd t2) b (Node4 t3 c t4 d t5 e t6) = Td(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"

fun node33 :: "'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a upd" where
"node33 l a m b (Td r) = Td(Node3 l a m b r)" |
"node33 t1 a (Node2 t2 b t3) c (Upd t4) = Td(Node2 t1 a (Node3 t2 b t3 c t4))" |
"node33 t1 a (Node3 t2 b t3 c t4) d (Upd t5) = Td(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Upd t6) = Td(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"

fun node41 :: "'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node41 (Td t1) a t2 b t3 c t4 = Td(Node4 t1 a t2 b t3 c t4)" |
"node41 (Upd t1) a (Node2 t2 b t3) c t4 d t5 = Td(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
"node41 (Upd t1) a (Node3 t2 b t3 c t4) d t5 e t6 = Td(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
"node41 (Upd t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = Td(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"

fun node42 :: "'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node42 t1 a (Td t2) b t3 c t4 = Td(Node4 t1 a t2 b t3 c t4)" |
"node42 (Node2 t1 a t2) b (Upd t3) c t4 d t5 = Td(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
"node42 (Node3 t1 a t2 b t3) c (Upd t4) d t5 e t6 = Td(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
"node42 (Node4 t1 a t2 b t3 c t4) d (Upd t5) e t6 f t7 = Td(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"

fun node43 :: "'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a ⇒ 'a tree234 ⇒ 'a upd" where
"node43 t1 a t2 b (Td t3) c t4 = Td(Node4 t1 a t2 b t3 c t4)" |
"node43 t1 a (Node2 t2 b t3) c (Upd t4) d t5 = Td(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
"node43 t1 a (Node3 t2 b t3 c t4) d (Upd t5) e t6 = Td(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Upd t6) f t7 = Td(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"

fun node44 :: "'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a tree234 ⇒ 'a ⇒ 'a upd ⇒ 'a upd" where
"node44 t1 a t2 b t3 c (Td t4) = Td(Node4 t1 a t2 b t3 c t4)" |
"node44 t1 a t2 b (Node2 t3 c t4) d (Upd t5) = Td(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Upd t6) = Td(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Upd t7) = Td(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"

fun del_min :: "'a tree234 ⇒ 'a * 'a upd" where
"del_min (Node2 Leaf a Leaf) = (a, Upd Leaf)" |
"del_min (Node3 Leaf a Leaf b Leaf) = (a, Td(Node2 Leaf b Leaf))" |
"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, Td(Node3 Leaf b Leaf c Leaf))" |
"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))"

fun del :: "'a::linorder ⇒ 'a tree234 ⇒ 'a upd" where
"del k Leaf = Td Leaf" |
"del k (Node2 Leaf p Leaf) = (if k=p then Upd Leaf else Td(Node2 Leaf p Leaf))" |
"del k (Node3 Leaf p Leaf q Leaf) = Td(if k=p then Node2 Leaf q Leaf
  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
"del k (Node4 Leaf a Leaf b Leaf c Leaf) =
  Td(if k=a then Node3 Leaf b Leaf c Leaf else
     if k=b then Node3 Leaf a Leaf c Leaf else
     if k=c then Node3 Leaf a Leaf b Leaf
     else Node4 Leaf a Leaf b Leaf c Leaf)" |
"del k (Node2 l a r) = (case cmp k a of
  LT ⇒ node21 (del k l) a r |
  GT ⇒ node22 l a (del k r) |
  EQ ⇒ let (a',t) = del_min r in node22 l a' t)" |
"del k (Node3 l a m b r) = (case cmp k a of
  LT ⇒ node31 (del k l) a m b r |
  EQ ⇒ let (a',m') = del_min m in node32 l a' m' b r |
  GT ⇒ (case cmp k b of
           LT ⇒ node32 l a (del k m) b r |
           EQ ⇒ let (b',r') = del_min r in node33 l a m b' r' |
           GT ⇒ node33 l a m b (del k r)))" |
"del k (Node4 l a m b n c r) = (case cmp k b of
  LT ⇒ (case cmp k a of
          LT ⇒ node41 (del k l) a m b n c r |
          EQ ⇒ let (a',m') = del_min m in node42 l a' m' b n c r |
          GT ⇒ node42 l a (del k m) b n c r) |
  EQ ⇒ let (b',n') = del_min n in node43 l a m b' n' c r |
  GT ⇒ (case cmp k c of
           LT ⇒ node43 l a m b (del k n) c r |
           EQ ⇒ let (c',r') = del_min r in node44 l a m b n c' r' |
           GT ⇒ node44 l a m b n c (del k r)))"

definition delete :: "'a::linorder ⇒ 'a tree234 ⇒ 'a tree234" where
"delete x t = treed(del x t)"


subsection "Functional correctness"

subsubsection ‹Functional correctness of isin:›

lemma "sorted(inorder t) ⟹ isin t x = (x ∈ elems (inorder t))"
by (induction t) (auto simp: elems_simps1 ball_Un)

lemma isin_set: "sorted(inorder t) ⟹ isin t x = (x ∈ elems (inorder t))"
by (induction t) (auto simp: elems_simps2 split!: if_splits)


subsubsection ‹Functional correctness of insert:›

lemma inorder_ins:
  "sorted(inorder t) ⟹ inorder(treei(ins x t)) = ins_list x (inorder t)"
by(induction t) (auto, auto simp: ins_list_simps split!: if_splits upi.splits)

lemma inorder_insert:
  "sorted(inorder t) ⟹ inorder(insert a t) = ins_list a (inorder t)"
by(simp add: insert_def inorder_ins)


subsubsection ‹Functional correctness of delete›

lemma inorder_node21: "height r > 0 ⟹
  inorder (treed (node21 l' a r)) = inorder (treed l') @ a # inorder r"
by(induct l' a r rule: node21.induct) auto

lemma inorder_node22: "height l > 0 ⟹
  inorder (treed (node22 l a r')) = inorder l @ a # inorder (treed r')"
by(induct l a r' rule: node22.induct) auto

lemma inorder_node31: "height m > 0 ⟹
  inorder (treed (node31 l' a m b r)) = inorder (treed l') @ a # inorder m @ b # inorder r"
by(induct l' a m b r rule: node31.induct) auto

lemma inorder_node32: "height r > 0 ⟹
  inorder (treed (node32 l a m' b r)) = inorder l @ a # inorder (treed m') @ b # inorder r"
by(induct l a m' b r rule: node32.induct) auto

lemma inorder_node33: "height m > 0 ⟹
  inorder (treed (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (treed r')"
by(induct l a m b r' rule: node33.induct) auto

lemma inorder_node41: "height m > 0 ⟹
  inorder (treed (node41 l' a m b n c r)) = inorder (treed l') @ a # inorder m @ b # inorder n @ c # inorder r"
by(induct l' a m b n c r rule: node41.induct) auto

lemma inorder_node42: "height l > 0 ⟹
  inorder (treed (node42 l a m b n c r)) = inorder l @ a # inorder (treed m) @ b # inorder n @ c # inorder r"
by(induct l a m b n c r rule: node42.induct) auto

lemma inorder_node43: "height m > 0 ⟹
  inorder (treed (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(treed n) @ c # inorder r"
by(induct l a m b n c r rule: node43.induct) auto

lemma inorder_node44: "height n > 0 ⟹
  inorder (treed (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (treed r)"
by(induct l a m b n c r rule: node44.induct) auto

lemmas inorder_nodes = inorder_node21 inorder_node22
  inorder_node31 inorder_node32 inorder_node33
  inorder_node41 inorder_node42 inorder_node43 inorder_node44

lemma del_minD:
  "del_min t = (x,t') ⟹ bal t ⟹ height t > 0 ⟹
  x # inorder(treed t') = inorder t"
by(induction t arbitrary: t' rule: del_min.induct)
  (auto simp: inorder_nodes split: prod.splits)

lemma inorder_del: "⟦ bal t ; sorted(inorder t) ⟧ ⟹
  inorder(treed (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
  (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
  (* 30 secs (2016) *)

lemma inorder_delete: "⟦ bal t ; sorted(inorder t) ⟧ ⟹
  inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del)


subsection ‹Balancedness›

subsubsection "Proofs for insert"

text{* First a standard proof that @{const ins} preserves @{const bal}. *}

instantiation upi :: (type)height
begin

fun height_upi :: "'a upi ⇒ nat" where
"height (Ti t) = height t" |
"height (Upi l a r) = height l"

instance ..

end

lemma bal_ins: "bal t ⟹ bal (treei(ins a t)) ∧ height(ins a t) = height t"
by (induct t) (auto split!: if_split upi.split)


text{* Now an alternative proof (by Brian Huffman) that runs faster because
two properties (balance and height) are combined in one predicate. *}

inductive full :: "nat ⇒ 'a tree234 ⇒ bool" where
"full 0 Leaf" |
"⟦full n l; full n r⟧ ⟹ full (Suc n) (Node2 l p r)" |
"⟦full n l; full n m; full n r⟧ ⟹ full (Suc n) (Node3 l p m q r)" |
"⟦full n l; full n m; full n m'; full n r⟧ ⟹ full (Suc n) (Node4 l p m q m' q' r)"

inductive_cases full_elims:
  "full n Leaf"
  "full n (Node2 l p r)"
  "full n (Node3 l p m q r)"
  "full n (Node4 l p m q m' q' r)"

inductive_cases full_0_elim: "full 0 t"
inductive_cases full_Suc_elim: "full (Suc n) t"

lemma full_0_iff [simp]: "full 0 t ⟷ t = Leaf"
  by (auto elim: full_0_elim intro: full.intros)

lemma full_Leaf_iff [simp]: "full n Leaf ⟷ n = 0"
  by (auto elim: full_elims intro: full.intros)

lemma full_Suc_Node2_iff [simp]:
  "full (Suc n) (Node2 l p r) ⟷ full n l ∧ full n r"
  by (auto elim: full_elims intro: full.intros)

lemma full_Suc_Node3_iff [simp]:
  "full (Suc n) (Node3 l p m q r) ⟷ full n l ∧ full n m ∧ full n r"
  by (auto elim: full_elims intro: full.intros)

lemma full_Suc_Node4_iff [simp]:
  "full (Suc n) (Node4 l p m q m' q' r) ⟷ full n l ∧ full n m ∧ full n m' ∧ full n r"
  by (auto elim: full_elims intro: full.intros)

lemma full_imp_height: "full n t ⟹ height t = n"
  by (induct set: full, simp_all)

lemma full_imp_bal: "full n t ⟹ bal t"
  by (induct set: full, auto dest: full_imp_height)

lemma bal_imp_full: "bal t ⟹ full (height t) t"
  by (induct t, simp_all)

lemma bal_iff_full: "bal t ⟷ (∃n. full n t)"
  by (auto elim!: bal_imp_full full_imp_bal)

text {* The @{const "insert"} function either preserves the height of the
tree, or increases it by one. The constructor returned by the @{term
"insert"} function determines which: A return value of the form @{term
"Ti t"} indicates that the height will be the same. A value of the
form @{term "Upi l p r"} indicates an increase in height. *}

primrec fulli :: "nat ⇒ 'a upi ⇒ bool" where
"fulli n (Ti t) ⟷ full n t" |
"fulli n (Upi l p r) ⟷ full n l ∧ full n r"

lemma fulli_ins: "full n t ⟹ fulli n (ins a t)"
by (induct rule: full.induct) (auto, auto split: upi.split)

text {* The @{const insert} operation preserves balance. *}

lemma bal_insert: "bal t ⟹ bal (insert a t)"
unfolding bal_iff_full insert_def
apply (erule exE)
apply (drule fulli_ins [of _ _ a])
apply (cases "ins a t")
apply (auto intro: full.intros)
done


subsubsection "Proofs for delete"

instantiation upd :: (type)height
begin

fun height_upd :: "'a upd ⇒ nat" where
"height (Td t) = height t" |
"height (Upd t) = height t + 1"

instance ..

end

lemma bal_treed_node21:
  "⟦bal r; bal (treed l); height r = height l ⟧ ⟹ bal (treed (node21 l a r))"
by(induct l a r rule: node21.induct) auto

lemma bal_treed_node22:
  "⟦bal(treed r); bal l; height r = height l ⟧ ⟹ bal (treed (node22 l a r))"
by(induct l a r rule: node22.induct) auto

lemma bal_treed_node31:
  "⟦ bal (treed l); bal m; bal r; height l = height r; height m = height r ⟧
  ⟹ bal (treed (node31 l a m b r))"
by(induct l a m b r rule: node31.induct) auto

lemma bal_treed_node32:
  "⟦ bal l; bal (treed m); bal r; height l = height r; height m = height r ⟧
  ⟹ bal (treed (node32 l a m b r))"
by(induct l a m b r rule: node32.induct) auto

lemma bal_treed_node33:
  "⟦ bal l; bal m; bal(treed r); height l = height r; height m = height r ⟧
  ⟹ bal (treed (node33 l a m b r))"
by(induct l a m b r rule: node33.induct) auto

lemma bal_treed_node41:
  "⟦ bal (treed l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r ⟧
  ⟹ bal (treed (node41 l a m b n c r))"
by(induct l a m b n c r rule: node41.induct) auto

lemma bal_treed_node42:
  "⟦ bal l; bal (treed m); bal n; bal r; height l = height r; height m = height r; height n = height r ⟧
  ⟹ bal (treed (node42 l a m b n c r))"
by(induct l a m b n c r rule: node42.induct) auto

lemma bal_treed_node43:
  "⟦ bal l; bal m; bal (treed n); bal r; height l = height r; height m = height r; height n = height r ⟧
  ⟹ bal (treed (node43 l a m b n c r))"
by(induct l a m b n c r rule: node43.induct) auto

lemma bal_treed_node44:
  "⟦ bal l; bal m; bal n; bal (treed r); height l = height r; height m = height r; height n = height r ⟧
  ⟹ bal (treed (node44 l a m b n c r))"
by(induct l a m b n c r rule: node44.induct) auto

lemmas bals = bal_treed_node21 bal_treed_node22
  bal_treed_node31 bal_treed_node32 bal_treed_node33
  bal_treed_node41 bal_treed_node42 bal_treed_node43 bal_treed_node44

lemma height_node21:
   "height r > 0 ⟹ height(node21 l a r) = max (height l) (height r) + 1"
by(induct l a r rule: node21.induct)(simp_all add: max.assoc)

lemma height_node22:
   "height l > 0 ⟹ height(node22 l a r) = max (height l) (height r) + 1"
by(induct l a r rule: node22.induct)(simp_all add: max.assoc)

lemma height_node31:
  "height m > 0 ⟹ height(node31 l a m b r) =
   max (height l) (max (height m) (height r)) + 1"
by(induct l a m b r rule: node31.induct)(simp_all add: max_def)

lemma height_node32:
  "height r > 0 ⟹ height(node32 l a m b r) =
   max (height l) (max (height m) (height r)) + 1"
by(induct l a m b r rule: node32.induct)(simp_all add: max_def)

lemma height_node33:
  "height m > 0 ⟹ height(node33 l a m b r) =
   max (height l) (max (height m) (height r)) + 1"
by(induct l a m b r rule: node33.induct)(simp_all add: max_def)

lemma height_node41:
  "height m > 0 ⟹ height(node41 l a m b n c r) =
   max (height l) (max (height m) (max (height n) (height r))) + 1"
by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)

lemma height_node42:
  "height l > 0 ⟹ height(node42 l a m b n c r) =
   max (height l) (max (height m) (max (height n) (height r))) + 1"
by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)

lemma height_node43:
  "height m > 0 ⟹ height(node43 l a m b n c r) =
   max (height l) (max (height m) (max (height n) (height r))) + 1"
by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)

lemma height_node44:
  "height n > 0 ⟹ height(node44 l a m b n c r) =
   max (height l) (max (height m) (max (height n) (height r))) + 1"
by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)

lemmas heights = height_node21 height_node22
  height_node31 height_node32 height_node33
  height_node41 height_node42 height_node43 height_node44

lemma height_del_min:
  "del_min t = (x, t') ⟹ height t > 0 ⟹ bal t ⟹ height t' = height t"
by(induct t arbitrary: x t' rule: del_min.induct)
  (auto simp: heights split: prod.splits)

lemma height_del: "bal t ⟹ height(del x t) = height t"
by(induction x t rule: del.induct)
  (auto simp add: heights height_del_min split!: if_split prod.split)

lemma bal_del_min:
  "⟦ del_min t = (x, t'); bal t; height t > 0 ⟧ ⟹ bal (treed t')"
by(induct t arbitrary: x t' rule: del_min.induct)
  (auto simp: heights height_del_min bals split: prod.splits)

lemma bal_treed_del: "bal t ⟹ bal(treed(del x t))"
by(induction x t rule: del.induct)
  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)

corollary bal_delete: "bal t ⟹ bal(delete x t)"
by(simp add: delete_def bal_treed_del)

subsection ‹Overall Correctness›

interpretation Set_by_Ordered
where empty = Leaf and isin = isin and insert = insert and delete = delete
and inorder = inorder and inv = bal
proof (standard, goal_cases)
  case 2 thus ?case by(simp add: isin_set)
next
  case 3 thus ?case by(simp add: inorder_insert)
next
  case 4 thus ?case by(simp add: inorder_delete)
next
  case 6 thus ?case by(simp add: bal_insert)
next
  case 7 thus ?case by(simp add: bal_delete)
qed simp+

end