src/HOL/Data_Structures/Tree234_Map.thy
 author nipkow Sat Apr 21 08:41:42 2018 +0200 (13 months ago) changeset 68020 6aade817bee5 parent 67965 aaa31cd0caef child 68431 b294e095f64c permissions -rw-r--r--
del_min -> split_min
 nipkow@61640 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61640 ` 2` nipkow@62130 ` 3` ```section \2-3-4 Tree Implementation of Maps\ ``` nipkow@61640 ` 4` nipkow@61640 ` 5` ```theory Tree234_Map ``` nipkow@61640 ` 6` ```imports ``` nipkow@61640 ` 7` ``` Tree234_Set ``` nipkow@67965 ` 8` ``` Map_Specs ``` nipkow@61640 ` 9` ```begin ``` nipkow@61640 ` 10` nipkow@61640 ` 11` ```subsection \Map operations on 2-3-4 trees\ ``` nipkow@61640 ` 12` nipkow@63411 ` 13` ```fun lookup :: "('a::linorder * 'b) tree234 \ 'a \ 'b option" where ``` nipkow@61640 ` 14` ```"lookup Leaf x = None" | ``` nipkow@61640 ` 15` ```"lookup (Node2 l (a,b) r) x = (case cmp x a of ``` nipkow@61640 ` 16` ``` LT \ lookup l x | ``` nipkow@61640 ` 17` ``` GT \ lookup r x | ``` nipkow@61640 ` 18` ``` EQ \ Some b)" | ``` nipkow@61640 ` 19` ```"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of ``` nipkow@61640 ` 20` ``` LT \ lookup l x | ``` nipkow@61640 ` 21` ``` EQ \ Some b1 | ``` nipkow@61640 ` 22` ``` GT \ (case cmp x a2 of ``` nipkow@61640 ` 23` ``` LT \ lookup m x | ``` nipkow@61640 ` 24` ``` EQ \ Some b2 | ``` nipkow@61640 ` 25` ``` GT \ lookup r x))" | ``` nipkow@61640 ` 26` ```"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of ``` nipkow@61640 ` 27` ``` LT \ (case cmp x a1 of ``` nipkow@61640 ` 28` ``` LT \ lookup t1 x | EQ \ Some b1 | GT \ lookup t2 x) | ``` nipkow@61640 ` 29` ``` EQ \ Some b2 | ``` nipkow@61640 ` 30` ``` GT \ (case cmp x a3 of ``` nipkow@61640 ` 31` ``` LT \ lookup t3 x | EQ \ Some b3 | GT \ lookup t4 x))" ``` nipkow@61640 ` 32` nipkow@63411 ` 33` ```fun upd :: "'a::linorder \ 'b \ ('a*'b) tree234 \ ('a*'b) up\<^sub>i" where ``` nipkow@61640 ` 34` ```"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" | ``` nipkow@61640 ` 35` ```"upd x y (Node2 l ab r) = (case cmp x (fst ab) of ``` nipkow@61640 ` 36` ``` LT \ (case upd x y l of ``` nipkow@61640 ` 37` ``` T\<^sub>i l' => T\<^sub>i (Node2 l' ab r) ``` nipkow@61640 ` 38` ``` | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) | ``` nipkow@61640 ` 39` ``` EQ \ T\<^sub>i (Node2 l (x,y) r) | ``` nipkow@61640 ` 40` ``` GT \ (case upd x y r of ``` nipkow@61640 ` 41` ``` T\<^sub>i r' => T\<^sub>i (Node2 l ab r') ``` nipkow@61640 ` 42` ``` | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" | ``` nipkow@61640 ` 43` ```"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of ``` nipkow@61640 ` 44` ``` LT \ (case upd x y l of ``` nipkow@61640 ` 45` ``` T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r) ``` nipkow@61640 ` 46` ``` | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) | ``` nipkow@61640 ` 47` ``` EQ \ T\<^sub>i (Node3 l (x,y) m ab2 r) | ``` nipkow@61640 ` 48` ``` GT \ (case cmp x (fst ab2) of ``` nipkow@61640 ` 49` ``` LT \ (case upd x y m of ``` nipkow@61640 ` 50` ``` T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r) ``` nipkow@61640 ` 51` ``` | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) | ``` nipkow@61640 ` 52` ``` EQ \ T\<^sub>i (Node3 l ab1 m (x,y) r) | ``` nipkow@61640 ` 53` ``` GT \ (case upd x y r of ``` nipkow@61640 ` 54` ``` T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r') ``` nipkow@61640 ` 55` ``` | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" | ``` nipkow@61640 ` 56` ```"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of ``` nipkow@61640 ` 57` ``` LT \ (case cmp x (fst ab1) of ``` nipkow@61640 ` 58` ``` LT \ (case upd x y t1 of ``` nipkow@61640 ` 59` ``` T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4) ``` nipkow@61640 ` 60` ``` | Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) | ``` nipkow@61640 ` 61` ``` EQ \ T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) | ``` nipkow@61640 ` 62` ``` GT \ (case upd x y t2 of ``` nipkow@61640 ` 63` ``` T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4) ``` nipkow@61640 ` 64` ``` | Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) | ``` nipkow@61640 ` 65` ``` EQ \ T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) | ``` nipkow@61640 ` 66` ``` GT \ (case cmp x (fst ab3) of ``` nipkow@61640 ` 67` ``` LT \ (case upd x y t3 of ``` nipkow@61640 ` 68` ``` T\<^sub>i t3' \ T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4) ``` nipkow@61640 ` 69` ``` | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) | ``` nipkow@61640 ` 70` ``` EQ \ T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) | ``` nipkow@61640 ` 71` ``` GT \ (case upd x y t4 of ``` nipkow@61640 ` 72` ``` T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4') ``` nipkow@61640 ` 73` ``` | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))" ``` nipkow@61640 ` 74` nipkow@63411 ` 75` ```definition update :: "'a::linorder \ 'b \ ('a*'b) tree234 \ ('a*'b) tree234" where ``` nipkow@61640 ` 76` ```"update x y t = tree\<^sub>i(upd x y t)" ``` nipkow@61640 ` 77` nipkow@63411 ` 78` ```fun del :: "'a::linorder \ ('a*'b) tree234 \ ('a*'b) up\<^sub>d" where ``` nipkow@61640 ` 79` ```"del x Leaf = T\<^sub>d Leaf" | ``` nipkow@61640 ` 80` ```"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" | ``` nipkow@61640 ` 81` ```"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf ``` nipkow@61640 ` 82` ``` else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" | ``` nipkow@61640 ` 83` ```"del x (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) = ``` nipkow@61640 ` 84` ``` T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else ``` nipkow@61640 ` 85` ``` if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else ``` nipkow@61640 ` 86` ``` if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf ``` nipkow@61640 ` 87` ``` else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" | ``` nipkow@61640 ` 88` ```"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of ``` nipkow@61640 ` 89` ``` LT \ node21 (del x l) ab1 r | ``` nipkow@61640 ` 90` ``` GT \ node22 l ab1 (del x r) | ``` nipkow@68020 ` 91` ``` EQ \ let (ab1',t) = split_min r in node22 l ab1' t)" | ``` nipkow@61640 ` 92` ```"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of ``` nipkow@61640 ` 93` ``` LT \ node31 (del x l) ab1 m ab2 r | ``` nipkow@68020 ` 94` ``` EQ \ let (ab1',m') = split_min m in node32 l ab1' m' ab2 r | ``` nipkow@61640 ` 95` ``` GT \ (case cmp x (fst ab2) of ``` nipkow@61640 ` 96` ``` LT \ node32 l ab1 (del x m) ab2 r | ``` nipkow@68020 ` 97` ``` EQ \ let (ab2',r') = split_min r in node33 l ab1 m ab2' r' | ``` nipkow@61640 ` 98` ``` GT \ node33 l ab1 m ab2 (del x r)))" | ``` nipkow@61640 ` 99` ```"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of ``` nipkow@61640 ` 100` ``` LT \ (case cmp x (fst ab1) of ``` nipkow@61640 ` 101` ``` LT \ node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 | ``` nipkow@68020 ` 102` ``` EQ \ let (ab',t2') = split_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 | ``` nipkow@61640 ` 103` ``` GT \ node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) | ``` nipkow@68020 ` 104` ``` EQ \ let (ab',t3') = split_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 | ``` nipkow@61640 ` 105` ``` GT \ (case cmp x (fst ab3) of ``` nipkow@61640 ` 106` ``` LT \ node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 | ``` nipkow@68020 ` 107` ``` EQ \ let (ab',t4') = split_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' | ``` nipkow@61640 ` 108` ``` GT \ node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))" ``` nipkow@61640 ` 109` nipkow@63411 ` 110` ```definition delete :: "'a::linorder \ ('a*'b) tree234 \ ('a*'b) tree234" where ``` nipkow@61640 ` 111` ```"delete x t = tree\<^sub>d(del x t)" ``` nipkow@61640 ` 112` nipkow@61640 ` 113` nipkow@61640 ` 114` ```subsection "Functional correctness" ``` nipkow@61640 ` 115` nipkow@61790 ` 116` ```lemma lookup_map_of: ``` nipkow@61790 ` 117` ``` "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" ``` nipkow@61640 ` 118` ```by (induction t) (auto simp: map_of_simps split: option.split) ``` nipkow@61640 ` 119` nipkow@61640 ` 120` nipkow@61640 ` 121` ```lemma inorder_upd: ``` nipkow@61640 ` 122` ``` "sorted1(inorder t) \ inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)" ``` nipkow@61640 ` 123` ```by(induction t) ``` nipkow@61640 ` 124` ``` (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits) ``` nipkow@61640 ` 125` nipkow@61640 ` 126` ```lemma inorder_update: ``` nipkow@61640 ` 127` ``` "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)" ``` nipkow@61640 ` 128` ```by(simp add: update_def inorder_upd) ``` nipkow@61640 ` 129` nipkow@61640 ` 130` ```lemma inorder_del: "\ bal t ; sorted1(inorder t) \ \ ``` nipkow@61640 ` 131` ``` inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" ``` nipkow@61640 ` 132` ```by(induction t rule: del.induct) ``` nipkow@68020 ` 133` ``` (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits) ``` nipkow@63636 ` 134` ```(* 30 secs (2016) *) ``` nipkow@61640 ` 135` nipkow@61640 ` 136` ```lemma inorder_delete: "\ bal t ; sorted1(inorder t) \ \ ``` nipkow@61640 ` 137` ``` inorder(delete x t) = del_list x (inorder t)" ``` nipkow@61640 ` 138` ```by(simp add: delete_def inorder_del) ``` nipkow@61640 ` 139` nipkow@61640 ` 140` nipkow@61640 ` 141` ```subsection \Balancedness\ ``` nipkow@61640 ` 142` nipkow@61640 ` 143` ```lemma bal_upd: "bal t \ bal (tree\<^sub>i(upd x y t)) \ height(upd x y t) = height t" ``` nipkow@63636 ` 144` ```by (induct t) (auto, auto split!: if_split up\<^sub>i.split) (* 20 secs (2015) *) ``` nipkow@61640 ` 145` nipkow@61640 ` 146` ```lemma bal_update: "bal t \ bal (update x y t)" ``` nipkow@61640 ` 147` ```by (simp add: update_def bal_upd) ``` nipkow@61640 ` 148` nipkow@61640 ` 149` ```lemma height_del: "bal t \ height(del x t) = height t" ``` nipkow@61640 ` 150` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 151` ``` (auto simp add: heights height_split_min split!: if_split prod.split) ``` nipkow@61640 ` 152` nipkow@61640 ` 153` ```lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" ``` nipkow@61640 ` 154` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 155` ``` (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split) ``` nipkow@61640 ` 156` nipkow@61640 ` 157` ```corollary bal_delete: "bal t \ bal(delete x t)" ``` nipkow@61640 ` 158` ```by(simp add: delete_def bal_tree\<^sub>d_del) ``` nipkow@61640 ` 159` nipkow@61640 ` 160` nipkow@61640 ` 161` ```subsection \Overall Correctness\ ``` nipkow@61640 ` 162` nipkow@61790 ` 163` ```interpretation Map_by_Ordered ``` nipkow@61640 ` 164` ```where empty = Leaf and lookup = lookup and update = update and delete = delete ``` nipkow@61686 ` 165` ```and inorder = inorder and inv = bal ``` nipkow@61640 ` 166` ```proof (standard, goal_cases) ``` nipkow@61790 ` 167` ``` case 2 thus ?case by(simp add: lookup_map_of) ``` nipkow@61640 ` 168` ```next ``` nipkow@61640 ` 169` ``` case 3 thus ?case by(simp add: inorder_update) ``` nipkow@61640 ` 170` ```next ``` nipkow@61640 ` 171` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61640 ` 172` ```next ``` nipkow@61640 ` 173` ``` case 6 thus ?case by(simp add: bal_update) ``` nipkow@61640 ` 174` ```next ``` nipkow@61640 ` 175` ``` case 7 thus ?case by(simp add: bal_delete) ``` nipkow@61640 ` 176` ```qed simp+ ``` nipkow@61640 ` 177` nipkow@61640 ` 178` ```end ```