added 234-trees (slow)
authornipkow
Sun Oct 25 17:31:14 2015 +0100 (2015-10-25)
changeset 61515c64628dbac00
parent 61514 213556e498c2
child 61516 8e3705d91cfa
child 61518 ff12606337e9
added 234-trees (slow)
src/HOL/Data_Structures/Tree234.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Tree234.thy	Sun Oct 25 17:31:14 2015 +0100
     1.3 @@ -0,0 +1,45 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section {* 2-3-4 Trees *}
     1.7 +
     1.8 +theory Tree234
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +class height =
    1.13 +fixes height :: "'a \<Rightarrow> nat"
    1.14 +
    1.15 +datatype 'a tree234 =
    1.16 +  Leaf |
    1.17 +  Node2 "'a tree234" 'a "'a tree234" |
    1.18 +  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
    1.19 +  Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
    1.20 +
    1.21 +fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
    1.22 +"inorder Leaf = []" |
    1.23 +"inorder(Node2 l a r) = inorder l @ a # inorder r" |
    1.24 +"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
    1.25 +"inorder(Node4 l a m b n c r) = inorder l @ a # inorder m @ b # inorder n @ c # inorder r"
    1.26 +
    1.27 +
    1.28 +instantiation tree234 :: (type)height
    1.29 +begin
    1.30 +
    1.31 +fun height_tree234 :: "'a tree234 \<Rightarrow> nat" where
    1.32 +"height Leaf = 0" |
    1.33 +"height (Node2 l _ r) = Suc(max (height l) (height r))" |
    1.34 +"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
    1.35 +"height (Node4 l _ m _ n _ r) = Suc(max (height l) (max (height m) (max (height n) (height r))))"
    1.36 +
    1.37 +instance ..
    1.38 +
    1.39 +end
    1.40 +
    1.41 +text{* Balanced: *}
    1.42 +fun bal :: "'a tree234 \<Rightarrow> bool" where
    1.43 +"bal Leaf = True" |
    1.44 +"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    1.45 +"bal (Node3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
    1.46 +"bal (Node4 l _ m _ n _ r) = (bal l & bal m & bal n & bal r & height l = height m & height m = height n & height n = height r)"
    1.47 +
    1.48 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sun Oct 25 17:31:14 2015 +0100
     2.3 @@ -0,0 +1,193 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +section \<open>A 2-3-4 Tree Implementation of Maps\<close>
     2.7 +
     2.8 +theory Tree234_Map
     2.9 +imports
    2.10 +  Tree234_Set
    2.11 +  "../Data_Structures/Map_by_Ordered"
    2.12 +begin
    2.13 +
    2.14 +subsection \<open>Map operations on 2-3-4 trees\<close>
    2.15 +
    2.16 +fun lookup :: "('a::linorder * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    2.17 +"lookup Leaf x = None" |
    2.18 +"lookup (Node2 l (a,b) r) x =
    2.19 +  (if x < a then lookup l x else
    2.20 +  if a < x then lookup r x else Some b)" |
    2.21 +"lookup (Node3 l (a1,b1) m (a2,b2) r) x =
    2.22 +  (if x < a1 then lookup l x else
    2.23 +   if x = a1 then Some b1 else
    2.24 +   if x < a2 then lookup m x else
    2.25 +   if x = a2 then Some b2
    2.26 +   else lookup r x)" |
    2.27 +"lookup (Node4 l (a1,b1) m (a2,b2) n (a3,b3) r) x =
    2.28 +  (if x < a2 then
    2.29 +     if x = a1 then Some b1 else
    2.30 +     if x < a1 then lookup l x else lookup m x
    2.31 +   else
    2.32 +     if x = a2 then Some b2 else
    2.33 +     if x = a3 then Some b3 else
    2.34 +     if x < a3 then lookup n x
    2.35 +     else lookup r x)"
    2.36 +
    2.37 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
    2.38 +"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
    2.39 +"upd x y (Node2 l ab r) =
    2.40 +   (if x < fst ab then
    2.41 +        (case upd x y l of
    2.42 +           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
    2.43 +         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 ab r))
    2.44 +    else if x = fst ab then T\<^sub>i (Node2 l (x,y) r)
    2.45 +    else
    2.46 +        (case upd x y r of
    2.47 +           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
    2.48 +         | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l ab r1 q r2)))" |
    2.49 +"upd x y (Node3 l ab1 m ab2 r) =
    2.50 +   (if x < fst ab1 then
    2.51 +        (case upd x y l of
    2.52 +           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
    2.53 +         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) ab1 (Node2 m ab2 r))
    2.54 +    else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r)
    2.55 +    else if x < fst ab2 then
    2.56 +             (case upd x y m of
    2.57 +                T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
    2.58 +              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l ab1 m1) q (Node2 m2 ab2 r))
    2.59 +         else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r)
    2.60 +         else
    2.61 +             (case upd x y r of
    2.62 +                T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
    2.63 +              | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 q r2)))" |
    2.64 +"upd x y (Node4 l ab1 m ab2 n ab3 r) =
    2.65 +   (if x < fst ab2 then
    2.66 +      if x < fst ab1 then
    2.67 +        (case upd x y l of
    2.68 +           T\<^sub>i l' => T\<^sub>i (Node4 l' ab1 m ab2 n ab3 r)
    2.69 +         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) ab1 (Node3 m ab2 n ab3 r))
    2.70 +      else
    2.71 +      if x = fst ab1 then T\<^sub>i (Node4 l (x,y) m ab2 n ab3 r)
    2.72 +      else
    2.73 +        (case upd x y m of
    2.74 +           T\<^sub>i m' => T\<^sub>i (Node4 l ab1 m' ab2 n ab3 r)
    2.75 +         | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l ab1 m1) q (Node3 m2 ab2 n ab3 r))
    2.76 +    else
    2.77 +    if x = fst ab2 then T\<^sub>i (Node4 l ab1 m (x,y) n ab3 r) else
    2.78 +    if x < fst ab3 then
    2.79 +      (case upd x y n of
    2.80 +         T\<^sub>i n' => T\<^sub>i (Node4 l ab1 m ab2 n' ab3 r)
    2.81 +       | Up\<^sub>i n1 q n2 => Up\<^sub>i (Node2 l ab1 m) ab2(*q*) (Node3 n1 q n2 ab3 r))
    2.82 +    else
    2.83 +    if x = fst ab3 then T\<^sub>i (Node4 l ab1 m ab2 n (x,y) r)
    2.84 +    else
    2.85 +      (case upd x y r of
    2.86 +         T\<^sub>i r' => T\<^sub>i (Node4 l ab1 m ab2 n ab3 r')
    2.87 +       | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node3 n ab3 r1 q r2)))"
    2.88 +
    2.89 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
    2.90 +"update a b t = tree\<^sub>i(upd a b t)"
    2.91 +
    2.92 +fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d"
    2.93 +where
    2.94 +"del k Leaf = T\<^sub>d Leaf" |
    2.95 +"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
    2.96 +"del k (Node3 Leaf p Leaf q Leaf) =
    2.97 +  T\<^sub>d(if k=fst p then Node2 Leaf q Leaf else
    2.98 +     if k=fst q then Node2 Leaf p Leaf
    2.99 +     else Node3 Leaf p Leaf q Leaf)" |
   2.100 +"del k (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
   2.101 +  T\<^sub>d(if k=fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
   2.102 +     if k=fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
   2.103 +     if k=fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
   2.104 +     else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
   2.105 +"del k (Node2 l a r) =
   2.106 +  (if k<fst a then node21 (del k l) a r else
   2.107 +   if k > fst a then node22 l a (del k r)
   2.108 +   else let (a',t) = del_min r in node22 l a' t)" |
   2.109 +"del k (Node3 l a m b r) =
   2.110 +  (if k<fst a then node31 (del k l) a m b r else
   2.111 +   if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else
   2.112 +   if k < fst b then node32 l a (del k m) b r else
   2.113 +   if k = fst b then let (b',r') = del_min r in node33 l a m b' r'
   2.114 +   else node33 l a m b (del k r))" |
   2.115 +"del x (Node4 l ab1 m ab2 n ab3 r) =
   2.116 +  (if x < fst ab2 then
   2.117 +     if x < fst ab1 then node41 (del x l) ab1 m ab2 n ab3 r else
   2.118 +     if x = fst ab1 then let (ab',m') = del_min m in node42 l ab' m' ab2 n ab3 r
   2.119 +     else node42 l ab1 (del x m) ab2 n ab3 r
   2.120 +   else
   2.121 +     if x = fst ab2 then let (ab',n') = del_min n in node43 l ab1 m ab' n' ab3 r else
   2.122 +     if x < fst ab3 then node43 l ab1 m ab2 (del x n) ab3 r else
   2.123 +     if x = fst ab3 then let (ab',r') = del_min r in node44 l ab1 m ab2 n ab' r'
   2.124 +     else node44 l ab1 m ab2 n ab3 (del x r))"
   2.125 +
   2.126 +definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   2.127 +"delete k t = tree\<^sub>d(del k t)"
   2.128 +
   2.129 +
   2.130 +subsection "Functional correctness"
   2.131 +
   2.132 +lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
   2.133 +by (induction t) (auto simp: map_of_simps split: option.split)
   2.134 +
   2.135 +
   2.136 +lemma inorder_upd:
   2.137 +  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
   2.138 +by(induction t)
   2.139 +  (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
   2.140 +
   2.141 +lemma inorder_update:
   2.142 +  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
   2.143 +by(simp add: update_def inorder_upd)
   2.144 +
   2.145 +
   2.146 +lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   2.147 +  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   2.148 +by(induction t rule: del.induct)
   2.149 +  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
   2.150 +(* 290 secs (2015) *)
   2.151 +
   2.152 +lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   2.153 +  inorder(delete x t) = del_list x (inorder t)"
   2.154 +by(simp add: delete_def inorder_del)
   2.155 +
   2.156 +
   2.157 +subsection \<open>Balancedness\<close>
   2.158 +
   2.159 +lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
   2.160 +by (induct t) (auto, auto split: up\<^sub>i.split) (* 33 secs (2015) *)
   2.161 +
   2.162 +lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
   2.163 +by (simp add: update_def bal_upd)
   2.164 +
   2.165 +
   2.166 +lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   2.167 +by(induction x t rule: del.induct)
   2.168 +  (auto simp add: heights height_del_min split: prod.split)
   2.169 +
   2.170 +lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   2.171 +by(induction x t rule: del.induct)
   2.172 +  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
   2.173 +(* 110 secs (2015) *)
   2.174 +
   2.175 +corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   2.176 +by(simp add: delete_def bal_tree\<^sub>d_del)
   2.177 +
   2.178 +
   2.179 +subsection \<open>Overall Correctness\<close>
   2.180 +
   2.181 +interpretation T234_Map: Map_by_Ordered
   2.182 +where empty = Leaf and lookup = lookup and update = update and delete = delete
   2.183 +and inorder = inorder and wf = bal
   2.184 +proof (standard, goal_cases)
   2.185 +  case 2 thus ?case by(simp add: lookup)
   2.186 +next
   2.187 +  case 3 thus ?case by(simp add: inorder_update)
   2.188 +next
   2.189 +  case 4 thus ?case by(simp add: inorder_delete)
   2.190 +next
   2.191 +  case 6 thus ?case by(simp add: bal_update)
   2.192 +next
   2.193 +  case 7 thus ?case by(simp add: bal_delete)
   2.194 +qed simp+
   2.195 +
   2.196 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sun Oct 25 17:31:14 2015 +0100
     3.3 @@ -0,0 +1,509 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +section \<open>A 2-3-4 Tree Implementation of Sets\<close>
     3.7 +
     3.8 +theory Tree234_Set
     3.9 +imports
    3.10 +  Tree234
    3.11 +  "../Data_Structures/Set_by_Ordered"
    3.12 +begin
    3.13 +
    3.14 +subsection \<open>Set operations on 2-3-4 trees\<close>
    3.15 +
    3.16 +fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
    3.17 +"isin Leaf x = False" |
    3.18 +"isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" |
    3.19 +"isin (Node3 l a m b r) x =
    3.20 +  (x < a \<and> isin l x \<or> x = a \<or> x < b \<and> isin m x \<or> x = b \<or> isin r x)" |
    3.21 +"isin (Node4 l a m b n c r) x =
    3.22 +  (x < b \<and> (x < a \<and> isin l x \<or> x = a \<or> isin m x) \<or> x = b \<or>
    3.23 +   x > b \<and> (x < c \<and> isin n x \<or> x=c \<or> isin r x))"
    3.24 +
    3.25 +datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234"
    3.26 +
    3.27 +fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where
    3.28 +"tree\<^sub>i (T\<^sub>i t) = t" |
    3.29 +"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
    3.30 +
    3.31 +fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
    3.32 +"ins a Leaf = Up\<^sub>i Leaf a Leaf" |
    3.33 +"ins a (Node2 l x r) =
    3.34 +   (if a < x then
    3.35 +        (case ins a l of
    3.36 +           T\<^sub>i l' => T\<^sub>i (Node2 l' x r)
    3.37 +         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r))
    3.38 +    else if a=x then T\<^sub>i (Node2 l x r)
    3.39 +    else
    3.40 +        (case ins a r of
    3.41 +           T\<^sub>i r' => T\<^sub>i (Node2 l x r')
    3.42 +         | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2)))" |
    3.43 +"ins a (Node3 l x1 m x2 r) =
    3.44 +   (if a < x1 then
    3.45 +        (case ins a l of
    3.46 +           T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r)
    3.47 +         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node4 l1 q l2 x1 m x2 r))
    3.48 +    else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r)
    3.49 +    else if a < x2 then
    3.50 +             (case ins a m of
    3.51 +                T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r)
    3.52 +              | Up\<^sub>i m1 q m2 => T\<^sub>i (Node4 l x1 m1 q m2 x2 r))
    3.53 +         else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r)
    3.54 +         else
    3.55 +             (case ins a r of
    3.56 +                T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r')
    3.57 +              | Up\<^sub>i r1 q r2 => T\<^sub>i (Node4 l x1 m x2 r1 q r2)))" |
    3.58 +"ins a (Node4 l x1 m x2 n x3 r) =
    3.59 +   (if a < x2 then
    3.60 +      if a < x1 then
    3.61 +        (case ins a l of
    3.62 +           T\<^sub>i l' => T\<^sub>i (Node4 l' x1 m x2 n x3 r)
    3.63 +         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node3 m x2 n x3 r))
    3.64 +      else if a=x1 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
    3.65 +      else (case ins a m of
    3.66 +                T\<^sub>i m' => T\<^sub>i (Node4 l x1 m' x2 n x3 r)
    3.67 +              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node3 m2 x2 n x3 r))
    3.68 +    else if a=x2 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
    3.69 +    else if a < x3 then
    3.70 +           (case ins a n of
    3.71 +              T\<^sub>i n' => T\<^sub>i (Node4 l x1 m x2 n' x3 r)
    3.72 +            | Up\<^sub>i n1 q n2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n1 q n2 x3 r))
    3.73 +         else if a=x3 then T\<^sub>i (Node4 l x1 m x2 n x3 r)
    3.74 +         else (case ins a r of
    3.75 +              T\<^sub>i r' => T\<^sub>i (Node4 l x1 m x2 n x3 r')
    3.76 +            | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node3 n x3 r1 q r2))
    3.77 +)"
    3.78 +
    3.79 +hide_const insert
    3.80 +
    3.81 +definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
    3.82 +"insert a t = tree\<^sub>i(ins a t)"
    3.83 +
    3.84 +datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
    3.85 +
    3.86 +fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where
    3.87 +"tree\<^sub>d (T\<^sub>d x) = x" |
    3.88 +"tree\<^sub>d (Up\<^sub>d x) = x"
    3.89 +
    3.90 +fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
    3.91 +"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
    3.92 +"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" |
    3.93 +"node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
    3.94 +"node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
    3.95 +
    3.96 +fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
    3.97 +"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" |
    3.98 +"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" |
    3.99 +"node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
   3.100 +"node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
   3.101 +
   3.102 +fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.103 +"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   3.104 +"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
   3.105 +"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
   3.106 +"node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"
   3.107 +
   3.108 +fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.109 +"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   3.110 +"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   3.111 +"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
   3.112 +"node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
   3.113 +
   3.114 +fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   3.115 +"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
   3.116 +"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   3.117 +"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
   3.118 +"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
   3.119 +
   3.120 +fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.121 +"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   3.122 +"node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
   3.123 +"node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
   3.124 +"node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
   3.125 +
   3.126 +fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.127 +"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   3.128 +"node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
   3.129 +"node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
   3.130 +"node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
   3.131 +
   3.132 +fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.133 +"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   3.134 +"node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
   3.135 +"node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
   3.136 +"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"
   3.137 +
   3.138 +fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   3.139 +"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   3.140 +"node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
   3.141 +"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
   3.142 +"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
   3.143 +
   3.144 +fun del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
   3.145 +"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
   3.146 +"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
   3.147 +"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
   3.148 +"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
   3.149 +"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
   3.150 +"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))"
   3.151 +
   3.152 +fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   3.153 +"del k Leaf = T\<^sub>d Leaf" |
   3.154 +"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
   3.155 +"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
   3.156 +  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
   3.157 +"del k (Node4 Leaf a Leaf b Leaf c Leaf) =
   3.158 +  T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else
   3.159 +     if k=b then Node3 Leaf a Leaf c Leaf else
   3.160 +     if k=c then Node3 Leaf a Leaf b Leaf
   3.161 +     else Node4 Leaf a Leaf b Leaf c Leaf)" |
   3.162 +"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else
   3.163 +  if k > a then node22 l a (del k r) else
   3.164 +  let (a',t) = del_min r in node22 l a' t)" |
   3.165 +"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else
   3.166 +  if k = a then let (a',m') = del_min m in node32 l a' m' b r else
   3.167 +  if k < b then node32 l a (del k m) b r else
   3.168 +  if k = b then let (b',r') = del_min r in node33 l a m b' r'
   3.169 +  else node33 l a m b (del k r))" |
   3.170 +"del k (Node4 l a m b n c r) =
   3.171 +  (if k < b then
   3.172 +     if k < a then node41 (del k l) a m b n c r else
   3.173 +     if k = a then let (a',m') = del_min m in node42 l a' m' b n c r
   3.174 +     else node42 l a (del k m) b n c r
   3.175 +   else
   3.176 +     if k = b then let (b',n') = del_min n in node43 l a m b' n' c r else
   3.177 +     if k < c then node43 l a m b (del k n) c r else
   3.178 +     if k = c then let (c',r') = del_min r in node44 l a m b n c' r'
   3.179 +     else node44 l a m b n c (del k r))"
   3.180 +
   3.181 +definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   3.182 +"delete k t = tree\<^sub>d(del k t)"
   3.183 +
   3.184 +
   3.185 +subsection "Functional correctness"
   3.186 +
   3.187 +
   3.188 +subsubsection \<open>Functional correctness of isin:\<close>
   3.189 +
   3.190 +lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
   3.191 +by (induction t) (auto simp: elems_simps1)
   3.192 +
   3.193 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
   3.194 +by (induction t) (auto simp: elems_simps2)
   3.195 +
   3.196 +
   3.197 +subsubsection \<open>Functional correctness of insert:\<close>
   3.198 +
   3.199 +lemma inorder_ins:
   3.200 +  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   3.201 +by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits)
   3.202 +
   3.203 +lemma inorder_insert:
   3.204 +  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   3.205 +by(simp add: insert_def inorder_ins)
   3.206 +
   3.207 +
   3.208 +subsubsection \<open>Functional correctness of delete\<close>
   3.209 +
   3.210 +lemma inorder_node21: "height r > 0 \<Longrightarrow>
   3.211 +  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
   3.212 +by(induct l' a r rule: node21.induct) auto
   3.213 +
   3.214 +lemma inorder_node22: "height l > 0 \<Longrightarrow>
   3.215 +  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
   3.216 +by(induct l a r' rule: node22.induct) auto
   3.217 +
   3.218 +lemma inorder_node31: "height m > 0 \<Longrightarrow>
   3.219 +  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
   3.220 +by(induct l' a m b r rule: node31.induct) auto
   3.221 +
   3.222 +lemma inorder_node32: "height r > 0 \<Longrightarrow>
   3.223 +  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
   3.224 +by(induct l a m' b r rule: node32.induct) auto
   3.225 +
   3.226 +lemma inorder_node33: "height m > 0 \<Longrightarrow>
   3.227 +  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
   3.228 +by(induct l a m b r' rule: node33.induct) auto
   3.229 +
   3.230 +lemma inorder_node41: "height m > 0 \<Longrightarrow>
   3.231 +  inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r"
   3.232 +by(induct l' a m b n c r rule: node41.induct) auto
   3.233 +
   3.234 +lemma inorder_node42: "height l > 0 \<Longrightarrow>
   3.235 +  inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r"
   3.236 +by(induct l a m b n c r rule: node42.induct) auto
   3.237 +
   3.238 +lemma inorder_node43: "height m > 0 \<Longrightarrow>
   3.239 +  inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r"
   3.240 +by(induct l a m b n c r rule: node43.induct) auto
   3.241 +
   3.242 +lemma inorder_node44: "height n > 0 \<Longrightarrow>
   3.243 +  inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)"
   3.244 +by(induct l a m b n c r rule: node44.induct) auto
   3.245 +
   3.246 +lemmas inorder_nodes = inorder_node21 inorder_node22
   3.247 +  inorder_node31 inorder_node32 inorder_node33
   3.248 +  inorder_node41 inorder_node42 inorder_node43 inorder_node44
   3.249 +
   3.250 +lemma del_minD:
   3.251 +  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   3.252 +  x # inorder(tree\<^sub>d t') = inorder t"
   3.253 +by(induction t arbitrary: t' rule: del_min.induct)
   3.254 +  (auto simp: inorder_nodes split: prod.splits)
   3.255 +
   3.256 +lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   3.257 +  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   3.258 +apply(induction t rule: del.induct)
   3.259 +apply(simp_all add: del_list_simps inorder_nodes)
   3.260 +apply(auto simp: del_list_simps;
   3.261 +      auto simp: inorder_nodes del_list_simps del_minD split: prod.splits)+
   3.262 +(* takes 285 s (2015); the last line alone would do it but takes hours *)
   3.263 +done
   3.264 +
   3.265 +lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   3.266 +  inorder(delete x t) = del_list x (inorder t)"
   3.267 +by(simp add: delete_def inorder_del)
   3.268 +
   3.269 +
   3.270 +subsection \<open>Balancedness\<close>
   3.271 +
   3.272 +subsubsection "Proofs for insert"
   3.273 +
   3.274 +text{* First a standard proof that @{const ins} preserves @{const bal}. *}
   3.275 +
   3.276 +instantiation up\<^sub>i :: (type)height
   3.277 +begin
   3.278 +
   3.279 +fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
   3.280 +"height (T\<^sub>i t) = height t" |
   3.281 +"height (Up\<^sub>i l a r) = height l"
   3.282 +
   3.283 +instance ..
   3.284 +
   3.285 +end
   3.286 +
   3.287 +lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   3.288 +by (induct t) (auto, auto split: up\<^sub>i.split) (* 29 secs (2015) *)
   3.289 +
   3.290 +
   3.291 +text{* Now an alternative proof (by Brian Huffman) that runs faster because
   3.292 +two properties (balance and height) are combined in one predicate. *}
   3.293 +
   3.294 +inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where
   3.295 +"full 0 Leaf" |
   3.296 +"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
   3.297 +"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" |
   3.298 +"\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)"
   3.299 +
   3.300 +inductive_cases full_elims:
   3.301 +  "full n Leaf"
   3.302 +  "full n (Node2 l p r)"
   3.303 +  "full n (Node3 l p m q r)"
   3.304 +  "full n (Node4 l p m q m' q' r)"
   3.305 +
   3.306 +inductive_cases full_0_elim: "full 0 t"
   3.307 +inductive_cases full_Suc_elim: "full (Suc n) t"
   3.308 +
   3.309 +lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
   3.310 +  by (auto elim: full_0_elim intro: full.intros)
   3.311 +
   3.312 +lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
   3.313 +  by (auto elim: full_elims intro: full.intros)
   3.314 +
   3.315 +lemma full_Suc_Node2_iff [simp]:
   3.316 +  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   3.317 +  by (auto elim: full_elims intro: full.intros)
   3.318 +
   3.319 +lemma full_Suc_Node3_iff [simp]:
   3.320 +  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   3.321 +  by (auto elim: full_elims intro: full.intros)
   3.322 +
   3.323 +lemma full_Suc_Node4_iff [simp]:
   3.324 +  "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r"
   3.325 +  by (auto elim: full_elims intro: full.intros)
   3.326 +
   3.327 +lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   3.328 +  by (induct set: full, simp_all)
   3.329 +
   3.330 +lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   3.331 +  by (induct set: full, auto dest: full_imp_height)
   3.332 +
   3.333 +lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   3.334 +  by (induct t, simp_all)
   3.335 +
   3.336 +lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   3.337 +  by (auto elim!: bal_imp_full full_imp_bal)
   3.338 +
   3.339 +text {* The @{const "insert"} function either preserves the height of the
   3.340 +tree, or increases it by one. The constructor returned by the @{term
   3.341 +"insert"} function determines which: A return value of the form @{term
   3.342 +"T\<^sub>i t"} indicates that the height will be the same. A value of the
   3.343 +form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
   3.344 +
   3.345 +primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
   3.346 +"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
   3.347 +"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
   3.348 +
   3.349 +lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
   3.350 +apply (induct rule: full.induct)
   3.351 +apply (auto, auto split: up\<^sub>i.split)
   3.352 +done
   3.353 +
   3.354 +text {* The @{const insert} operation preserves balance. *}
   3.355 +
   3.356 +lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
   3.357 +unfolding bal_iff_full insert_def
   3.358 +apply (erule exE)
   3.359 +apply (drule full\<^sub>i_ins [of _ _ a])
   3.360 +apply (cases "ins a t")
   3.361 +apply (auto intro: full.intros)
   3.362 +done
   3.363 +
   3.364 +
   3.365 +subsubsection "Proofs for delete"
   3.366 +
   3.367 +instantiation up\<^sub>d :: (type)height
   3.368 +begin
   3.369 +
   3.370 +fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
   3.371 +"height (T\<^sub>d t) = height t" |
   3.372 +"height (Up\<^sub>d t) = height t + 1"
   3.373 +
   3.374 +instance ..
   3.375 +
   3.376 +end
   3.377 +
   3.378 +lemma bal_tree\<^sub>d_node21:
   3.379 +  "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))"
   3.380 +by(induct l a r rule: node21.induct) auto
   3.381 +
   3.382 +lemma bal_tree\<^sub>d_node22:
   3.383 +  "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))"
   3.384 +by(induct l a r rule: node22.induct) auto
   3.385 +
   3.386 +lemma bal_tree\<^sub>d_node31:
   3.387 +  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk>
   3.388 +  \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))"
   3.389 +by(induct l a m b r rule: node31.induct) auto
   3.390 +
   3.391 +lemma bal_tree\<^sub>d_node32:
   3.392 +  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk>
   3.393 +  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))"
   3.394 +by(induct l a m b r rule: node32.induct) auto
   3.395 +
   3.396 +lemma bal_tree\<^sub>d_node33:
   3.397 +  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk>
   3.398 +  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))"
   3.399 +by(induct l a m b r rule: node33.induct) auto
   3.400 +
   3.401 +lemma bal_tree\<^sub>d_node41:
   3.402 +  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   3.403 +  \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))"
   3.404 +by(induct l a m b n c r rule: node41.induct) auto
   3.405 +
   3.406 +lemma bal_tree\<^sub>d_node42:
   3.407 +  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   3.408 +  \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))"
   3.409 +by(induct l a m b n c r rule: node42.induct) auto
   3.410 +
   3.411 +lemma bal_tree\<^sub>d_node43:
   3.412 +  "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   3.413 +  \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))"
   3.414 +by(induct l a m b n c r rule: node43.induct) auto
   3.415 +
   3.416 +lemma bal_tree\<^sub>d_node44:
   3.417 +  "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk>
   3.418 +  \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))"
   3.419 +by(induct l a m b n c r rule: node44.induct) auto
   3.420 +
   3.421 +lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
   3.422 +  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
   3.423 +  bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44
   3.424 +
   3.425 +lemma height_node21:
   3.426 +   "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1"
   3.427 +by(induct l a r rule: node21.induct)(simp_all add: max.assoc)
   3.428 +
   3.429 +lemma height_node22:
   3.430 +   "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1"
   3.431 +by(induct l a r rule: node22.induct)(simp_all add: max.assoc)
   3.432 +
   3.433 +lemma height_node31:
   3.434 +  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
   3.435 +   max (height l) (max (height m) (height r)) + 1"
   3.436 +by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
   3.437 +
   3.438 +lemma height_node32:
   3.439 +  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
   3.440 +   max (height l) (max (height m) (height r)) + 1"
   3.441 +by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
   3.442 +
   3.443 +lemma height_node33:
   3.444 +  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
   3.445 +   max (height l) (max (height m) (height r)) + 1"
   3.446 +by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
   3.447 +
   3.448 +lemma height_node41:
   3.449 +  "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) =
   3.450 +   max (height l) (max (height m) (max (height n) (height r))) + 1"
   3.451 +by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)
   3.452 +
   3.453 +lemma height_node42:
   3.454 +  "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) =
   3.455 +   max (height l) (max (height m) (max (height n) (height r))) + 1"
   3.456 +by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)
   3.457 +
   3.458 +lemma height_node43:
   3.459 +  "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) =
   3.460 +   max (height l) (max (height m) (max (height n) (height r))) + 1"
   3.461 +by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)
   3.462 +
   3.463 +lemma height_node44:
   3.464 +  "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) =
   3.465 +   max (height l) (max (height m) (max (height n) (height r))) + 1"
   3.466 +by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)
   3.467 +
   3.468 +lemmas heights = height_node21 height_node22
   3.469 +  height_node31 height_node32 height_node33
   3.470 +  height_node41 height_node42 height_node43 height_node44
   3.471 +
   3.472 +lemma height_del_min:
   3.473 +  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
   3.474 +by(induct t arbitrary: x t' rule: del_min.induct)
   3.475 +  (auto simp: heights split: prod.splits)
   3.476 +
   3.477 +lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   3.478 +by(induction x t rule: del.induct)
   3.479 +  (auto simp add: heights height_del_min split: prod.split)
   3.480 +
   3.481 +lemma bal_del_min:
   3.482 +  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
   3.483 +by(induct t arbitrary: x t' rule: del_min.induct)
   3.484 +  (auto simp: heights height_del_min bals split: prod.splits)
   3.485 +
   3.486 +lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   3.487 +by(induction x t rule: del.induct)
   3.488 +  ((auto simp: bals bal_del_min height_del height_del_min split: prod.split)[1])+
   3.489 +(* 64 secs (2015) *)
   3.490 +
   3.491 +corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   3.492 +by(simp add: delete_def bal_tree\<^sub>d_del)
   3.493 +
   3.494 +
   3.495 +subsection \<open>Overall Correctness\<close>
   3.496 +
   3.497 +interpretation Set_by_Ordered
   3.498 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   3.499 +and inorder = inorder and wf = bal
   3.500 +proof (standard, goal_cases)
   3.501 +  case 2 thus ?case by(simp add: isin_set)
   3.502 +next
   3.503 +  case 3 thus ?case by(simp add: inorder_insert)
   3.504 +next
   3.505 +  case 4 thus ?case by(simp add: inorder_delete)
   3.506 +next
   3.507 +  case 6 thus ?case by(simp add: bal_insert)
   3.508 +next
   3.509 +  case 7 thus ?case by(simp add: bal_delete)
   3.510 +qed simp+
   3.511 +
   3.512 +end