src/HOL/Data_Structures/Tree234_Set.thy
 author nipkow Wed Jun 13 15:24:20 2018 +0200 (10 months ago) changeset 68440 6826718f732d parent 68431 b294e095f64c child 69597 ff784d5a5bfb permissions -rw-r--r--
qualify interpretations to avoid clashes
 nipkow@61640 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61640 ` 2` nipkow@62130 ` 3` ```section \2-3-4 Tree Implementation of Sets\ ``` nipkow@61640 ` 4` nipkow@61640 ` 5` ```theory Tree234_Set ``` nipkow@61640 ` 6` ```imports ``` nipkow@61640 ` 7` ``` Tree234 ``` nipkow@61640 ` 8` ``` Cmp ``` nipkow@67965 ` 9` ``` Set_Specs ``` nipkow@61640 ` 10` ```begin ``` nipkow@61640 ` 11` nipkow@68109 ` 12` ```declare sorted_wrt.simps(2)[simp del] ``` nipkow@68109 ` 13` nipkow@61640 ` 14` ```subsection \Set operations on 2-3-4 trees\ ``` nipkow@61640 ` 15` nipkow@68431 ` 16` ```definition empty :: "'a tree234" where ``` nipkow@68431 ` 17` ```"empty = Leaf" ``` nipkow@68431 ` 18` nipkow@63411 ` 19` ```fun isin :: "'a::linorder tree234 \ 'a \ bool" where ``` nipkow@61640 ` 20` ```"isin Leaf x = False" | ``` nipkow@61640 ` 21` ```"isin (Node2 l a r) x = ``` nipkow@61640 ` 22` ``` (case cmp x a of LT \ isin l x | EQ \ True | GT \ isin r x)" | ``` nipkow@61640 ` 23` ```"isin (Node3 l a m b r) x = ``` nipkow@61640 ` 24` ``` (case cmp x a of LT \ isin l x | EQ \ True | GT \ (case cmp x b of ``` nipkow@61640 ` 25` ``` LT \ isin m x | EQ \ True | GT \ isin r x))" | ``` nipkow@61703 ` 26` ```"isin (Node4 t1 a t2 b t3 c t4) x = ``` nipkow@61703 ` 27` ``` (case cmp x b of ``` nipkow@61703 ` 28` ``` LT \ ``` nipkow@61703 ` 29` ``` (case cmp x a of ``` nipkow@61640 ` 30` ``` LT \ isin t1 x | ``` nipkow@61640 ` 31` ``` EQ \ True | ``` nipkow@61640 ` 32` ``` GT \ isin t2 x) | ``` nipkow@61703 ` 33` ``` EQ \ True | ``` nipkow@61703 ` 34` ``` GT \ ``` nipkow@61703 ` 35` ``` (case cmp x c of ``` nipkow@61640 ` 36` ``` LT \ isin t3 x | ``` nipkow@61640 ` 37` ``` EQ \ True | ``` nipkow@61640 ` 38` ``` GT \ isin t4 x))" ``` nipkow@61640 ` 39` nipkow@61640 ` 40` ```datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234" ``` nipkow@61640 ` 41` nipkow@61640 ` 42` ```fun tree\<^sub>i :: "'a up\<^sub>i \ 'a tree234" where ``` nipkow@61640 ` 43` ```"tree\<^sub>i (T\<^sub>i t) = t" | ``` nipkow@61709 ` 44` ```"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" ``` nipkow@61640 ` 45` nipkow@63411 ` 46` ```fun ins :: "'a::linorder \ 'a tree234 \ 'a up\<^sub>i" where ``` nipkow@61640 ` 47` ```"ins x Leaf = Up\<^sub>i Leaf x Leaf" | ``` nipkow@61640 ` 48` ```"ins x (Node2 l a r) = ``` nipkow@61640 ` 49` ``` (case cmp x a of ``` nipkow@61640 ` 50` ``` LT \ (case ins x l of ``` nipkow@61640 ` 51` ``` T\<^sub>i l' => T\<^sub>i (Node2 l' a r) ``` nipkow@61640 ` 52` ``` | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) | ``` nipkow@61640 ` 53` ``` EQ \ T\<^sub>i (Node2 l x r) | ``` nipkow@61640 ` 54` ``` GT \ (case ins x r of ``` nipkow@61640 ` 55` ``` T\<^sub>i r' => T\<^sub>i (Node2 l a r') ``` nipkow@61640 ` 56` ``` | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" | ``` nipkow@61640 ` 57` ```"ins x (Node3 l a m b r) = ``` nipkow@61640 ` 58` ``` (case cmp x a of ``` nipkow@61640 ` 59` ``` LT \ (case ins x l of ``` nipkow@61640 ` 60` ``` T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) ``` nipkow@61640 ` 61` ``` | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) | ``` nipkow@61640 ` 62` ``` EQ \ T\<^sub>i (Node3 l a m b r) | ``` nipkow@61640 ` 63` ``` GT \ (case cmp x b of ``` nipkow@61640 ` 64` ``` GT \ (case ins x r of ``` nipkow@61640 ` 65` ``` T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') ``` nipkow@61640 ` 66` ``` | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) | ``` nipkow@61640 ` 67` ``` EQ \ T\<^sub>i (Node3 l a m b r) | ``` nipkow@61640 ` 68` ``` LT \ (case ins x m of ``` nipkow@61640 ` 69` ``` T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) ``` nipkow@61640 ` 70` ``` | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))" | ``` nipkow@61703 ` 71` ```"ins x (Node4 t1 a t2 b t3 c t4) = ``` nipkow@61703 ` 72` ``` (case cmp x b of ``` nipkow@61703 ` 73` ``` LT \ ``` nipkow@61703 ` 74` ``` (case cmp x a of ``` nipkow@61703 ` 75` ``` LT \ ``` nipkow@61703 ` 76` ``` (case ins x t1 of ``` nipkow@61703 ` 77` ``` T\<^sub>i t => T\<^sub>i (Node4 t a t2 b t3 c t4) | ``` nipkow@61703 ` 78` ``` Up\<^sub>i l y r => Up\<^sub>i (Node2 l y r) a (Node3 t2 b t3 c t4)) | ``` nipkow@61703 ` 79` ``` EQ \ T\<^sub>i (Node4 t1 a t2 b t3 c t4) | ``` nipkow@61703 ` 80` ``` GT \ ``` nipkow@61703 ` 81` ``` (case ins x t2 of ``` nipkow@61703 ` 82` ``` T\<^sub>i t => T\<^sub>i (Node4 t1 a t b t3 c t4) | ``` nipkow@61703 ` 83` ``` Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a l) y (Node3 r b t3 c t4))) | ``` nipkow@61703 ` 84` ``` EQ \ T\<^sub>i (Node4 t1 a t2 b t3 c t4) | ``` nipkow@61703 ` 85` ``` GT \ ``` nipkow@61703 ` 86` ``` (case cmp x c of ``` nipkow@61703 ` 87` ``` LT \ ``` nipkow@61703 ` 88` ``` (case ins x t3 of ``` nipkow@61703 ` 89` ``` T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t c t4) | ``` nipkow@61703 ` 90` ``` Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 l y r c t4)) | ``` nipkow@61703 ` 91` ``` EQ \ T\<^sub>i (Node4 t1 a t2 b t3 c t4) | ``` nipkow@61703 ` 92` ``` GT \ ``` nipkow@61703 ` 93` ``` (case ins x t4 of ``` nipkow@61703 ` 94` ``` T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t3 c t) | ``` nipkow@61703 ` 95` ``` Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 t3 c l y r))))" ``` nipkow@61640 ` 96` nipkow@61640 ` 97` ```hide_const insert ``` nipkow@61640 ` 98` nipkow@63411 ` 99` ```definition insert :: "'a::linorder \ 'a tree234 \ 'a tree234" where ``` nipkow@61640 ` 100` ```"insert x t = tree\<^sub>i(ins x t)" ``` nipkow@61640 ` 101` nipkow@61640 ` 102` ```datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234" ``` nipkow@61640 ` 103` nipkow@61640 ` 104` ```fun tree\<^sub>d :: "'a up\<^sub>d \ 'a tree234" where ``` nipkow@61709 ` 105` ```"tree\<^sub>d (T\<^sub>d t) = t" | ``` nipkow@61709 ` 106` ```"tree\<^sub>d (Up\<^sub>d t) = t" ``` nipkow@61640 ` 107` nipkow@61640 ` 108` ```fun node21 :: "'a up\<^sub>d \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 109` ```"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" | ``` nipkow@61640 ` 110` ```"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" | ``` nipkow@61640 ` 111` ```"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))" | ``` nipkow@61640 ` 112` ```"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))" ``` nipkow@61640 ` 113` nipkow@61640 ` 114` ```fun node22 :: "'a tree234 \ 'a \ 'a up\<^sub>d \ 'a up\<^sub>d" where ``` nipkow@61640 ` 115` ```"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" | ``` nipkow@61640 ` 116` ```"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" | ``` nipkow@61640 ` 117` ```"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))" | ``` nipkow@61640 ` 118` ```"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))" ``` nipkow@61640 ` 119` nipkow@61640 ` 120` ```fun node31 :: "'a up\<^sub>d \ 'a \ 'a tree234 \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 121` ```"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | ``` nipkow@61640 ` 122` ```"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" | ``` nipkow@61640 ` 123` ```"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)" | ``` nipkow@61640 ` 124` ```"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)" ``` nipkow@61640 ` 125` nipkow@61640 ` 126` ```fun node32 :: "'a tree234 \ 'a \ 'a up\<^sub>d \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 127` ```"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | ``` nipkow@61640 ` 128` ```"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | ``` nipkow@61640 ` 129` ```"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))" | ``` nipkow@61640 ` 130` ```"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))" ``` nipkow@61640 ` 131` nipkow@61640 ` 132` ```fun node33 :: "'a tree234 \ 'a \ 'a tree234 \ 'a \ 'a up\<^sub>d \ 'a up\<^sub>d" where ``` nipkow@61640 ` 133` ```"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" | ``` nipkow@61640 ` 134` ```"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | ``` nipkow@61640 ` 135` ```"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))" | ``` nipkow@61640 ` 136` ```"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))" ``` nipkow@61640 ` 137` nipkow@61640 ` 138` ```fun node41 :: "'a up\<^sub>d \ 'a \ 'a tree234 \ 'a \ 'a tree234 \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 139` ```"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | ``` nipkow@61640 ` 140` ```"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)" | ``` nipkow@61640 ` 141` ```"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)" | ``` nipkow@61640 ` 142` ```"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)" ``` nipkow@61640 ` 143` nipkow@61640 ` 144` ```fun node42 :: "'a tree234 \ 'a \ 'a up\<^sub>d \ 'a \ 'a tree234 \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 145` ```"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | ``` nipkow@61640 ` 146` ```"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)" | ``` nipkow@61640 ` 147` ```"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)" | ``` nipkow@61640 ` 148` ```"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)" ``` nipkow@61640 ` 149` nipkow@61640 ` 150` ```fun node43 :: "'a tree234 \ 'a \ 'a tree234 \ 'a \ 'a up\<^sub>d \ 'a \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 151` ```"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | ``` nipkow@61640 ` 152` ```"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)" | ``` nipkow@61640 ` 153` ```"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)" | ``` nipkow@61640 ` 154` ```"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)" ``` nipkow@61640 ` 155` nipkow@61640 ` 156` ```fun node44 :: "'a tree234 \ 'a \ 'a tree234 \ 'a \ 'a tree234 \ 'a \ 'a up\<^sub>d \ 'a up\<^sub>d" where ``` nipkow@61640 ` 157` ```"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | ``` nipkow@61640 ` 158` ```"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))" | ``` nipkow@61640 ` 159` ```"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))" | ``` nipkow@61640 ` 160` ```"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))" ``` nipkow@61640 ` 161` nipkow@68020 ` 162` ```fun split_min :: "'a tree234 \ 'a * 'a up\<^sub>d" where ``` nipkow@68020 ` 163` ```"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" | ``` nipkow@68020 ` 164` ```"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" | ``` nipkow@68020 ` 165` ```"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" | ``` nipkow@68020 ` 166` ```"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" | ``` nipkow@68020 ` 167` ```"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" | ``` nipkow@68020 ` 168` ```"split_min (Node4 l a m b n c r) = (let (x,l') = split_min l in (x, node41 l' a m b n c r))" ``` nipkow@61640 ` 169` nipkow@63411 ` 170` ```fun del :: "'a::linorder \ 'a tree234 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 171` ```"del k Leaf = T\<^sub>d Leaf" | ``` nipkow@61640 ` 172` ```"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" | ``` nipkow@61640 ` 173` ```"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf ``` nipkow@61640 ` 174` ``` else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" | ``` nipkow@61640 ` 175` ```"del k (Node4 Leaf a Leaf b Leaf c Leaf) = ``` nipkow@61640 ` 176` ``` T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else ``` nipkow@61640 ` 177` ``` if k=b then Node3 Leaf a Leaf c Leaf else ``` nipkow@61640 ` 178` ``` if k=c then Node3 Leaf a Leaf b Leaf ``` nipkow@61640 ` 179` ``` else Node4 Leaf a Leaf b Leaf c Leaf)" | ``` nipkow@61640 ` 180` ```"del k (Node2 l a r) = (case cmp k a of ``` nipkow@61640 ` 181` ``` LT \ node21 (del k l) a r | ``` nipkow@61640 ` 182` ``` GT \ node22 l a (del k r) | ``` nipkow@68020 ` 183` ``` EQ \ let (a',t) = split_min r in node22 l a' t)" | ``` nipkow@61640 ` 184` ```"del k (Node3 l a m b r) = (case cmp k a of ``` nipkow@61640 ` 185` ``` LT \ node31 (del k l) a m b r | ``` nipkow@68020 ` 186` ``` EQ \ let (a',m') = split_min m in node32 l a' m' b r | ``` nipkow@61640 ` 187` ``` GT \ (case cmp k b of ``` nipkow@61640 ` 188` ``` LT \ node32 l a (del k m) b r | ``` nipkow@68020 ` 189` ``` EQ \ let (b',r') = split_min r in node33 l a m b' r' | ``` nipkow@61640 ` 190` ``` GT \ node33 l a m b (del k r)))" | ``` nipkow@61640 ` 191` ```"del k (Node4 l a m b n c r) = (case cmp k b of ``` nipkow@61640 ` 192` ``` LT \ (case cmp k a of ``` nipkow@61640 ` 193` ``` LT \ node41 (del k l) a m b n c r | ``` nipkow@68020 ` 194` ``` EQ \ let (a',m') = split_min m in node42 l a' m' b n c r | ``` nipkow@61640 ` 195` ``` GT \ node42 l a (del k m) b n c r) | ``` nipkow@68020 ` 196` ``` EQ \ let (b',n') = split_min n in node43 l a m b' n' c r | ``` nipkow@61640 ` 197` ``` GT \ (case cmp k c of ``` nipkow@61640 ` 198` ``` LT \ node43 l a m b (del k n) c r | ``` nipkow@68020 ` 199` ``` EQ \ let (c',r') = split_min r in node44 l a m b n c' r' | ``` nipkow@61640 ` 200` ``` GT \ node44 l a m b n c (del k r)))" ``` nipkow@61640 ` 201` nipkow@63411 ` 202` ```definition delete :: "'a::linorder \ 'a tree234 \ 'a tree234" where ``` nipkow@61640 ` 203` ```"delete x t = tree\<^sub>d(del x t)" ``` nipkow@61640 ` 204` nipkow@61640 ` 205` nipkow@61640 ` 206` ```subsection "Functional correctness" ``` nipkow@61640 ` 207` nipkow@61640 ` 208` ```subsubsection \Functional correctness of isin:\ ``` nipkow@61640 ` 209` nipkow@67929 ` 210` ```lemma isin_set: "sorted(inorder t) \ isin t x = (x \ set (inorder t))" ``` nipkow@67929 ` 211` ```by (induction t) (auto simp: isin_simps ball_Un) ``` nipkow@61640 ` 212` nipkow@61640 ` 213` nipkow@61640 ` 214` ```subsubsection \Functional correctness of insert:\ ``` nipkow@61640 ` 215` nipkow@61640 ` 216` ```lemma inorder_ins: ``` nipkow@61640 ` 217` ``` "sorted(inorder t) \ inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" ``` nipkow@63636 ` 218` ```by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits) ``` nipkow@61640 ` 219` nipkow@61640 ` 220` ```lemma inorder_insert: ``` nipkow@61640 ` 221` ``` "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" ``` nipkow@61640 ` 222` ```by(simp add: insert_def inorder_ins) ``` nipkow@61640 ` 223` nipkow@61640 ` 224` nipkow@61640 ` 225` ```subsubsection \Functional correctness of delete\ ``` nipkow@61640 ` 226` nipkow@61640 ` 227` ```lemma inorder_node21: "height r > 0 \ ``` nipkow@61640 ` 228` ``` inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r" ``` nipkow@61640 ` 229` ```by(induct l' a r rule: node21.induct) auto ``` nipkow@61640 ` 230` nipkow@61640 ` 231` ```lemma inorder_node22: "height l > 0 \ ``` nipkow@61640 ` 232` ``` inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')" ``` nipkow@61640 ` 233` ```by(induct l a r' rule: node22.induct) auto ``` nipkow@61640 ` 234` nipkow@61640 ` 235` ```lemma inorder_node31: "height m > 0 \ ``` nipkow@61640 ` 236` ``` inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r" ``` nipkow@61640 ` 237` ```by(induct l' a m b r rule: node31.induct) auto ``` nipkow@61640 ` 238` nipkow@61640 ` 239` ```lemma inorder_node32: "height r > 0 \ ``` nipkow@61640 ` 240` ``` inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r" ``` nipkow@61640 ` 241` ```by(induct l a m' b r rule: node32.induct) auto ``` nipkow@61640 ` 242` nipkow@61640 ` 243` ```lemma inorder_node33: "height m > 0 \ ``` nipkow@61640 ` 244` ``` inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')" ``` nipkow@61640 ` 245` ```by(induct l a m b r' rule: node33.induct) auto ``` nipkow@61640 ` 246` nipkow@61640 ` 247` ```lemma inorder_node41: "height m > 0 \ ``` nipkow@61640 ` 248` ``` 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" ``` nipkow@61640 ` 249` ```by(induct l' a m b n c r rule: node41.induct) auto ``` nipkow@61640 ` 250` nipkow@61640 ` 251` ```lemma inorder_node42: "height l > 0 \ ``` nipkow@61640 ` 252` ``` 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" ``` nipkow@61640 ` 253` ```by(induct l a m b n c r rule: node42.induct) auto ``` nipkow@61640 ` 254` nipkow@61640 ` 255` ```lemma inorder_node43: "height m > 0 \ ``` nipkow@61640 ` 256` ``` 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" ``` nipkow@61640 ` 257` ```by(induct l a m b n c r rule: node43.induct) auto ``` nipkow@61640 ` 258` nipkow@61640 ` 259` ```lemma inorder_node44: "height n > 0 \ ``` nipkow@61640 ` 260` ``` 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)" ``` nipkow@61640 ` 261` ```by(induct l a m b n c r rule: node44.induct) auto ``` nipkow@61640 ` 262` nipkow@61640 ` 263` ```lemmas inorder_nodes = inorder_node21 inorder_node22 ``` nipkow@61640 ` 264` ``` inorder_node31 inorder_node32 inorder_node33 ``` nipkow@61640 ` 265` ``` inorder_node41 inorder_node42 inorder_node43 inorder_node44 ``` nipkow@61640 ` 266` nipkow@68020 ` 267` ```lemma split_minD: ``` nipkow@68020 ` 268` ``` "split_min t = (x,t') \ bal t \ height t > 0 \ ``` nipkow@61640 ` 269` ``` x # inorder(tree\<^sub>d t') = inorder t" ``` nipkow@68020 ` 270` ```by(induction t arbitrary: t' rule: split_min.induct) ``` nipkow@61640 ` 271` ``` (auto simp: inorder_nodes split: prod.splits) ``` nipkow@61640 ` 272` nipkow@61640 ` 273` ```lemma inorder_del: "\ bal t ; sorted(inorder t) \ \ ``` nipkow@61640 ` 274` ``` inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" ``` nipkow@61640 ` 275` ```by(induction t rule: del.induct) ``` nipkow@68020 ` 276` ``` (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits) ``` nipkow@63636 ` 277` ``` (* 30 secs (2016) *) ``` nipkow@61640 ` 278` nipkow@61640 ` 279` ```lemma inorder_delete: "\ bal t ; sorted(inorder t) \ \ ``` nipkow@61640 ` 280` ``` inorder(delete x t) = del_list x (inorder t)" ``` nipkow@61640 ` 281` ```by(simp add: delete_def inorder_del) ``` nipkow@61640 ` 282` nipkow@61640 ` 283` nipkow@61640 ` 284` ```subsection \Balancedness\ ``` nipkow@61640 ` 285` nipkow@61640 ` 286` ```subsubsection "Proofs for insert" ``` nipkow@61640 ` 287` wenzelm@67406 ` 288` ```text\First a standard proof that @{const ins} preserves @{const bal}.\ ``` nipkow@61640 ` 289` nipkow@61640 ` 290` ```instantiation up\<^sub>i :: (type)height ``` nipkow@61640 ` 291` ```begin ``` nipkow@61640 ` 292` nipkow@61640 ` 293` ```fun height_up\<^sub>i :: "'a up\<^sub>i \ nat" where ``` nipkow@61640 ` 294` ```"height (T\<^sub>i t) = height t" | ``` nipkow@61640 ` 295` ```"height (Up\<^sub>i l a r) = height l" ``` nipkow@61640 ` 296` nipkow@61640 ` 297` ```instance .. ``` nipkow@61640 ` 298` nipkow@61640 ` 299` ```end ``` nipkow@61640 ` 300` nipkow@61640 ` 301` ```lemma bal_ins: "bal t \ bal (tree\<^sub>i(ins a t)) \ height(ins a t) = height t" ``` nipkow@63636 ` 302` ```by (induct t) (auto split!: if_split up\<^sub>i.split) ``` nipkow@61640 ` 303` nipkow@61640 ` 304` wenzelm@67406 ` 305` ```text\Now an alternative proof (by Brian Huffman) that runs faster because ``` wenzelm@67406 ` 306` ```two properties (balance and height) are combined in one predicate.\ ``` nipkow@61640 ` 307` nipkow@61640 ` 308` ```inductive full :: "nat \ 'a tree234 \ bool" where ``` nipkow@61640 ` 309` ```"full 0 Leaf" | ``` nipkow@61640 ` 310` ```"\full n l; full n r\ \ full (Suc n) (Node2 l p r)" | ``` nipkow@61640 ` 311` ```"\full n l; full n m; full n r\ \ full (Suc n) (Node3 l p m q r)" | ``` nipkow@61640 ` 312` ```"\full n l; full n m; full n m'; full n r\ \ full (Suc n) (Node4 l p m q m' q' r)" ``` nipkow@61640 ` 313` nipkow@61640 ` 314` ```inductive_cases full_elims: ``` nipkow@61640 ` 315` ``` "full n Leaf" ``` nipkow@61640 ` 316` ``` "full n (Node2 l p r)" ``` nipkow@61640 ` 317` ``` "full n (Node3 l p m q r)" ``` nipkow@61640 ` 318` ``` "full n (Node4 l p m q m' q' r)" ``` nipkow@61640 ` 319` nipkow@61640 ` 320` ```inductive_cases full_0_elim: "full 0 t" ``` nipkow@61640 ` 321` ```inductive_cases full_Suc_elim: "full (Suc n) t" ``` nipkow@61640 ` 322` nipkow@61640 ` 323` ```lemma full_0_iff [simp]: "full 0 t \ t = Leaf" ``` nipkow@61640 ` 324` ``` by (auto elim: full_0_elim intro: full.intros) ``` nipkow@61640 ` 325` nipkow@61640 ` 326` ```lemma full_Leaf_iff [simp]: "full n Leaf \ n = 0" ``` nipkow@61640 ` 327` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 328` nipkow@61640 ` 329` ```lemma full_Suc_Node2_iff [simp]: ``` nipkow@61640 ` 330` ``` "full (Suc n) (Node2 l p r) \ full n l \ full n r" ``` nipkow@61640 ` 331` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 332` nipkow@61640 ` 333` ```lemma full_Suc_Node3_iff [simp]: ``` nipkow@61640 ` 334` ``` "full (Suc n) (Node3 l p m q r) \ full n l \ full n m \ full n r" ``` nipkow@61640 ` 335` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 336` nipkow@61640 ` 337` ```lemma full_Suc_Node4_iff [simp]: ``` nipkow@61640 ` 338` ``` "full (Suc n) (Node4 l p m q m' q' r) \ full n l \ full n m \ full n m' \ full n r" ``` nipkow@61640 ` 339` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 340` nipkow@61640 ` 341` ```lemma full_imp_height: "full n t \ height t = n" ``` nipkow@61640 ` 342` ``` by (induct set: full, simp_all) ``` nipkow@61640 ` 343` nipkow@61640 ` 344` ```lemma full_imp_bal: "full n t \ bal t" ``` nipkow@61640 ` 345` ``` by (induct set: full, auto dest: full_imp_height) ``` nipkow@61640 ` 346` nipkow@61640 ` 347` ```lemma bal_imp_full: "bal t \ full (height t) t" ``` nipkow@61640 ` 348` ``` by (induct t, simp_all) ``` nipkow@61640 ` 349` nipkow@61640 ` 350` ```lemma bal_iff_full: "bal t \ (\n. full n t)" ``` nipkow@61640 ` 351` ``` by (auto elim!: bal_imp_full full_imp_bal) ``` nipkow@61640 ` 352` wenzelm@67406 ` 353` ```text \The @{const "insert"} function either preserves the height of the ``` nipkow@61640 ` 354` ```tree, or increases it by one. The constructor returned by the @{term ``` nipkow@61640 ` 355` ```"insert"} function determines which: A return value of the form @{term ``` nipkow@61640 ` 356` ```"T\<^sub>i t"} indicates that the height will be the same. A value of the ``` wenzelm@67406 ` 357` ```form @{term "Up\<^sub>i l p r"} indicates an increase in height.\ ``` nipkow@61640 ` 358` nipkow@61640 ` 359` ```primrec full\<^sub>i :: "nat \ 'a up\<^sub>i \ bool" where ``` nipkow@61640 ` 360` ```"full\<^sub>i n (T\<^sub>i t) \ full n t" | ``` nipkow@61640 ` 361` ```"full\<^sub>i n (Up\<^sub>i l p r) \ full n l \ full n r" ``` nipkow@61640 ` 362` nipkow@61640 ` 363` ```lemma full\<^sub>i_ins: "full n t \ full\<^sub>i n (ins a t)" ``` nipkow@61640 ` 364` ```by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split) ``` nipkow@61640 ` 365` wenzelm@67406 ` 366` ```text \The @{const insert} operation preserves balance.\ ``` nipkow@61640 ` 367` nipkow@61640 ` 368` ```lemma bal_insert: "bal t \ bal (insert a t)" ``` nipkow@61640 ` 369` ```unfolding bal_iff_full insert_def ``` nipkow@61640 ` 370` ```apply (erule exE) ``` nipkow@61640 ` 371` ```apply (drule full\<^sub>i_ins [of _ _ a]) ``` nipkow@61640 ` 372` ```apply (cases "ins a t") ``` nipkow@61640 ` 373` ```apply (auto intro: full.intros) ``` nipkow@61640 ` 374` ```done ``` nipkow@61640 ` 375` nipkow@61640 ` 376` nipkow@61640 ` 377` ```subsubsection "Proofs for delete" ``` nipkow@61640 ` 378` nipkow@61640 ` 379` ```instantiation up\<^sub>d :: (type)height ``` nipkow@61640 ` 380` ```begin ``` nipkow@61640 ` 381` nipkow@61640 ` 382` ```fun height_up\<^sub>d :: "'a up\<^sub>d \ nat" where ``` nipkow@61640 ` 383` ```"height (T\<^sub>d t) = height t" | ``` nipkow@61640 ` 384` ```"height (Up\<^sub>d t) = height t + 1" ``` nipkow@61640 ` 385` nipkow@61640 ` 386` ```instance .. ``` nipkow@61640 ` 387` nipkow@61640 ` 388` ```end ``` nipkow@61640 ` 389` nipkow@61640 ` 390` ```lemma bal_tree\<^sub>d_node21: ``` nipkow@61640 ` 391` ``` "\bal r; bal (tree\<^sub>d l); height r = height l \ \ bal (tree\<^sub>d (node21 l a r))" ``` nipkow@61640 ` 392` ```by(induct l a r rule: node21.induct) auto ``` nipkow@61640 ` 393` nipkow@61640 ` 394` ```lemma bal_tree\<^sub>d_node22: ``` nipkow@61640 ` 395` ``` "\bal(tree\<^sub>d r); bal l; height r = height l \ \ bal (tree\<^sub>d (node22 l a r))" ``` nipkow@61640 ` 396` ```by(induct l a r rule: node22.induct) auto ``` nipkow@61640 ` 397` nipkow@61640 ` 398` ```lemma bal_tree\<^sub>d_node31: ``` nipkow@61640 ` 399` ``` "\ bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \ ``` nipkow@61640 ` 400` ``` \ bal (tree\<^sub>d (node31 l a m b r))" ``` nipkow@61640 ` 401` ```by(induct l a m b r rule: node31.induct) auto ``` nipkow@61640 ` 402` nipkow@61640 ` 403` ```lemma bal_tree\<^sub>d_node32: ``` nipkow@61640 ` 404` ``` "\ bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \ ``` nipkow@61640 ` 405` ``` \ bal (tree\<^sub>d (node32 l a m b r))" ``` nipkow@61640 ` 406` ```by(induct l a m b r rule: node32.induct) auto ``` nipkow@61640 ` 407` nipkow@61640 ` 408` ```lemma bal_tree\<^sub>d_node33: ``` nipkow@61640 ` 409` ``` "\ bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \ ``` nipkow@61640 ` 410` ``` \ bal (tree\<^sub>d (node33 l a m b r))" ``` nipkow@61640 ` 411` ```by(induct l a m b r rule: node33.induct) auto ``` nipkow@61640 ` 412` nipkow@61640 ` 413` ```lemma bal_tree\<^sub>d_node41: ``` nipkow@61640 ` 414` ``` "\ bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \ ``` nipkow@61640 ` 415` ``` \ bal (tree\<^sub>d (node41 l a m b n c r))" ``` nipkow@61640 ` 416` ```by(induct l a m b n c r rule: node41.induct) auto ``` nipkow@61640 ` 417` nipkow@61640 ` 418` ```lemma bal_tree\<^sub>d_node42: ``` nipkow@61640 ` 419` ``` "\ bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \ ``` nipkow@61640 ` 420` ``` \ bal (tree\<^sub>d (node42 l a m b n c r))" ``` nipkow@61640 ` 421` ```by(induct l a m b n c r rule: node42.induct) auto ``` nipkow@61640 ` 422` nipkow@61640 ` 423` ```lemma bal_tree\<^sub>d_node43: ``` nipkow@61640 ` 424` ``` "\ bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \ ``` nipkow@61640 ` 425` ``` \ bal (tree\<^sub>d (node43 l a m b n c r))" ``` nipkow@61640 ` 426` ```by(induct l a m b n c r rule: node43.induct) auto ``` nipkow@61640 ` 427` nipkow@61640 ` 428` ```lemma bal_tree\<^sub>d_node44: ``` nipkow@61640 ` 429` ``` "\ bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \ ``` nipkow@61640 ` 430` ``` \ bal (tree\<^sub>d (node44 l a m b n c r))" ``` nipkow@61640 ` 431` ```by(induct l a m b n c r rule: node44.induct) auto ``` nipkow@61640 ` 432` nipkow@61640 ` 433` ```lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22 ``` nipkow@61640 ` 434` ``` bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33 ``` nipkow@61640 ` 435` ``` bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44 ``` nipkow@61640 ` 436` nipkow@61640 ` 437` ```lemma height_node21: ``` nipkow@61640 ` 438` ``` "height r > 0 \ height(node21 l a r) = max (height l) (height r) + 1" ``` nipkow@61640 ` 439` ```by(induct l a r rule: node21.induct)(simp_all add: max.assoc) ``` nipkow@61640 ` 440` nipkow@61640 ` 441` ```lemma height_node22: ``` nipkow@61640 ` 442` ``` "height l > 0 \ height(node22 l a r) = max (height l) (height r) + 1" ``` nipkow@61640 ` 443` ```by(induct l a r rule: node22.induct)(simp_all add: max.assoc) ``` nipkow@61640 ` 444` nipkow@61640 ` 445` ```lemma height_node31: ``` nipkow@61640 ` 446` ``` "height m > 0 \ height(node31 l a m b r) = ``` nipkow@61640 ` 447` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 448` ```by(induct l a m b r rule: node31.induct)(simp_all add: max_def) ``` nipkow@61640 ` 449` nipkow@61640 ` 450` ```lemma height_node32: ``` nipkow@61640 ` 451` ``` "height r > 0 \ height(node32 l a m b r) = ``` nipkow@61640 ` 452` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 453` ```by(induct l a m b r rule: node32.induct)(simp_all add: max_def) ``` nipkow@61640 ` 454` nipkow@61640 ` 455` ```lemma height_node33: ``` nipkow@61640 ` 456` ``` "height m > 0 \ height(node33 l a m b r) = ``` nipkow@61640 ` 457` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 458` ```by(induct l a m b r rule: node33.induct)(simp_all add: max_def) ``` nipkow@61640 ` 459` nipkow@61640 ` 460` ```lemma height_node41: ``` nipkow@61640 ` 461` ``` "height m > 0 \ height(node41 l a m b n c r) = ``` nipkow@61640 ` 462` ``` max (height l) (max (height m) (max (height n) (height r))) + 1" ``` nipkow@61640 ` 463` ```by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def) ``` nipkow@61640 ` 464` nipkow@61640 ` 465` ```lemma height_node42: ``` nipkow@61640 ` 466` ``` "height l > 0 \ height(node42 l a m b n c r) = ``` nipkow@61640 ` 467` ``` max (height l) (max (height m) (max (height n) (height r))) + 1" ``` nipkow@61640 ` 468` ```by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def) ``` nipkow@61640 ` 469` nipkow@61640 ` 470` ```lemma height_node43: ``` nipkow@61640 ` 471` ``` "height m > 0 \ height(node43 l a m b n c r) = ``` nipkow@61640 ` 472` ``` max (height l) (max (height m) (max (height n) (height r))) + 1" ``` nipkow@61640 ` 473` ```by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def) ``` nipkow@61640 ` 474` nipkow@61640 ` 475` ```lemma height_node44: ``` nipkow@61640 ` 476` ``` "height n > 0 \ height(node44 l a m b n c r) = ``` nipkow@61640 ` 477` ``` max (height l) (max (height m) (max (height n) (height r))) + 1" ``` nipkow@61640 ` 478` ```by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def) ``` nipkow@61640 ` 479` nipkow@61640 ` 480` ```lemmas heights = height_node21 height_node22 ``` nipkow@61640 ` 481` ``` height_node31 height_node32 height_node33 ``` nipkow@61640 ` 482` ``` height_node41 height_node42 height_node43 height_node44 ``` nipkow@61640 ` 483` nipkow@68020 ` 484` ```lemma height_split_min: ``` nipkow@68020 ` 485` ``` "split_min t = (x, t') \ height t > 0 \ bal t \ height t' = height t" ``` nipkow@68020 ` 486` ```by(induct t arbitrary: x t' rule: split_min.induct) ``` nipkow@61640 ` 487` ``` (auto simp: heights split: prod.splits) ``` nipkow@61640 ` 488` nipkow@61640 ` 489` ```lemma height_del: "bal t \ height(del x t) = height t" ``` nipkow@61640 ` 490` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 491` ``` (auto simp add: heights height_split_min split!: if_split prod.split) ``` nipkow@61640 ` 492` nipkow@68020 ` 493` ```lemma bal_split_min: ``` nipkow@68020 ` 494` ``` "\ split_min t = (x, t'); bal t; height t > 0 \ \ bal (tree\<^sub>d t')" ``` nipkow@68020 ` 495` ```by(induct t arbitrary: x t' rule: split_min.induct) ``` nipkow@68020 ` 496` ``` (auto simp: heights height_split_min bals split: prod.splits) ``` nipkow@61640 ` 497` nipkow@61640 ` 498` ```lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" ``` nipkow@61640 ` 499` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 500` ``` (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split) ``` nipkow@61640 ` 501` nipkow@61640 ` 502` ```corollary bal_delete: "bal t \ bal(delete x t)" ``` nipkow@61640 ` 503` ```by(simp add: delete_def bal_tree\<^sub>d_del) ``` nipkow@61640 ` 504` nipkow@61640 ` 505` ```subsection \Overall Correctness\ ``` nipkow@61640 ` 506` nipkow@68440 ` 507` ```interpretation S: Set_by_Ordered ``` nipkow@68431 ` 508` ```where empty = empty and isin = isin and insert = insert and delete = delete ``` nipkow@61640 ` 509` ```and inorder = inorder and inv = bal ``` nipkow@61640 ` 510` ```proof (standard, goal_cases) ``` nipkow@61640 ` 511` ``` case 2 thus ?case by(simp add: isin_set) ``` nipkow@61640 ` 512` ```next ``` nipkow@61640 ` 513` ``` case 3 thus ?case by(simp add: inorder_insert) ``` nipkow@61640 ` 514` ```next ``` nipkow@61640 ` 515` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61640 ` 516` ```next ``` nipkow@61640 ` 517` ``` case 6 thus ?case by(simp add: bal_insert) ``` nipkow@61640 ` 518` ```next ``` nipkow@61640 ` 519` ``` case 7 thus ?case by(simp add: bal_delete) ``` nipkow@68431 ` 520` ```qed (simp add: empty_def)+ ``` nipkow@61640 ` 521` nipkow@61640 ` 522` ```end ```