src/HOL/Data_Structures/Tree234_Map.thy
 author nipkow Sun Oct 25 17:31:14 2015 +0100 (2015-10-25) changeset 61515 c64628dbac00 child 61581 00d9682e8dd7 permissions -rw-r--r--
 nipkow@61515 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61515 ` 2` nipkow@61515 ` 3` ```section \A 2-3-4 Tree Implementation of Maps\ ``` nipkow@61515 ` 4` nipkow@61515 ` 5` ```theory Tree234_Map ``` nipkow@61515 ` 6` ```imports ``` nipkow@61515 ` 7` ``` Tree234_Set ``` nipkow@61515 ` 8` ``` "../Data_Structures/Map_by_Ordered" ``` nipkow@61515 ` 9` ```begin ``` nipkow@61515 ` 10` nipkow@61515 ` 11` ```subsection \Map operations on 2-3-4 trees\ ``` nipkow@61515 ` 12` nipkow@61515 ` 13` ```fun lookup :: "('a::linorder * 'b) tree234 \ 'a \ 'b option" where ``` nipkow@61515 ` 14` ```"lookup Leaf x = None" | ``` nipkow@61515 ` 15` ```"lookup (Node2 l (a,b) r) x = ``` nipkow@61515 ` 16` ``` (if x < a then lookup l x else ``` nipkow@61515 ` 17` ``` if a < x then lookup r x else Some b)" | ``` nipkow@61515 ` 18` ```"lookup (Node3 l (a1,b1) m (a2,b2) r) x = ``` nipkow@61515 ` 19` ``` (if x < a1 then lookup l x else ``` nipkow@61515 ` 20` ``` if x = a1 then Some b1 else ``` nipkow@61515 ` 21` ``` if x < a2 then lookup m x else ``` nipkow@61515 ` 22` ``` if x = a2 then Some b2 ``` nipkow@61515 ` 23` ``` else lookup r x)" | ``` nipkow@61515 ` 24` ```"lookup (Node4 l (a1,b1) m (a2,b2) n (a3,b3) r) x = ``` nipkow@61515 ` 25` ``` (if x < a2 then ``` nipkow@61515 ` 26` ``` if x = a1 then Some b1 else ``` nipkow@61515 ` 27` ``` if x < a1 then lookup l x else lookup m x ``` nipkow@61515 ` 28` ``` else ``` nipkow@61515 ` 29` ``` if x = a2 then Some b2 else ``` nipkow@61515 ` 30` ``` if x = a3 then Some b3 else ``` nipkow@61515 ` 31` ``` if x < a3 then lookup n x ``` nipkow@61515 ` 32` ``` else lookup r x)" ``` nipkow@61515 ` 33` nipkow@61515 ` 34` ```fun upd :: "'a::linorder \ 'b \ ('a*'b) tree234 \ ('a*'b) up\<^sub>i" where ``` nipkow@61515 ` 35` ```"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" | ``` nipkow@61515 ` 36` ```"upd x y (Node2 l ab r) = ``` nipkow@61515 ` 37` ``` (if x < fst ab then ``` nipkow@61515 ` 38` ``` (case upd x y l of ``` nipkow@61515 ` 39` ``` T\<^sub>i l' => T\<^sub>i (Node2 l' ab r) ``` nipkow@61515 ` 40` ``` | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 ab r)) ``` nipkow@61515 ` 41` ``` else if x = fst ab then T\<^sub>i (Node2 l (x,y) r) ``` nipkow@61515 ` 42` ``` else ``` nipkow@61515 ` 43` ``` (case upd x y r of ``` nipkow@61515 ` 44` ``` T\<^sub>i r' => T\<^sub>i (Node2 l ab r') ``` nipkow@61515 ` 45` ``` | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l ab r1 q r2)))" | ``` nipkow@61515 ` 46` ```"upd x y (Node3 l ab1 m ab2 r) = ``` nipkow@61515 ` 47` ``` (if x < fst ab1 then ``` nipkow@61515 ` 48` ``` (case upd x y l of ``` nipkow@61515 ` 49` ``` T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r) ``` nipkow@61515 ` 50` ``` | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) ab1 (Node2 m ab2 r)) ``` nipkow@61515 ` 51` ``` else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r) ``` nipkow@61515 ` 52` ``` else if x < fst ab2 then ``` nipkow@61515 ` 53` ``` (case upd x y m of ``` nipkow@61515 ` 54` ``` T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r) ``` nipkow@61515 ` 55` ``` | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l ab1 m1) q (Node2 m2 ab2 r)) ``` nipkow@61515 ` 56` ``` else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r) ``` nipkow@61515 ` 57` ``` else ``` nipkow@61515 ` 58` ``` (case upd x y r of ``` nipkow@61515 ` 59` ``` T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r') ``` nipkow@61515 ` 60` ``` | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 q r2)))" | ``` nipkow@61515 ` 61` ```"upd x y (Node4 l ab1 m ab2 n ab3 r) = ``` nipkow@61515 ` 62` ``` (if x < fst ab2 then ``` nipkow@61515 ` 63` ``` if x < fst ab1 then ``` nipkow@61515 ` 64` ``` (case upd x y l of ``` nipkow@61515 ` 65` ``` T\<^sub>i l' => T\<^sub>i (Node4 l' ab1 m ab2 n ab3 r) ``` nipkow@61515 ` 66` ``` | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) ab1 (Node3 m ab2 n ab3 r)) ``` nipkow@61515 ` 67` ``` else ``` nipkow@61515 ` 68` ``` if x = fst ab1 then T\<^sub>i (Node4 l (x,y) m ab2 n ab3 r) ``` nipkow@61515 ` 69` ``` else ``` nipkow@61515 ` 70` ``` (case upd x y m of ``` nipkow@61515 ` 71` ``` T\<^sub>i m' => T\<^sub>i (Node4 l ab1 m' ab2 n ab3 r) ``` nipkow@61515 ` 72` ``` | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l ab1 m1) q (Node3 m2 ab2 n ab3 r)) ``` nipkow@61515 ` 73` ``` else ``` nipkow@61515 ` 74` ``` if x = fst ab2 then T\<^sub>i (Node4 l ab1 m (x,y) n ab3 r) else ``` nipkow@61515 ` 75` ``` if x < fst ab3 then ``` nipkow@61515 ` 76` ``` (case upd x y n of ``` nipkow@61515 ` 77` ``` T\<^sub>i n' => T\<^sub>i (Node4 l ab1 m ab2 n' ab3 r) ``` nipkow@61515 ` 78` ``` | Up\<^sub>i n1 q n2 => Up\<^sub>i (Node2 l ab1 m) ab2(*q*) (Node3 n1 q n2 ab3 r)) ``` nipkow@61515 ` 79` ``` else ``` nipkow@61515 ` 80` ``` if x = fst ab3 then T\<^sub>i (Node4 l ab1 m ab2 n (x,y) r) ``` nipkow@61515 ` 81` ``` else ``` nipkow@61515 ` 82` ``` (case upd x y r of ``` nipkow@61515 ` 83` ``` T\<^sub>i r' => T\<^sub>i (Node4 l ab1 m ab2 n ab3 r') ``` nipkow@61515 ` 84` ``` | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node3 n ab3 r1 q r2)))" ``` nipkow@61515 ` 85` nipkow@61515 ` 86` ```definition update :: "'a::linorder \ 'b \ ('a*'b) tree234 \ ('a*'b) tree234" where ``` nipkow@61515 ` 87` ```"update a b t = tree\<^sub>i(upd a b t)" ``` nipkow@61515 ` 88` nipkow@61515 ` 89` ```fun del :: "'a::linorder \ ('a*'b) tree234 \ ('a*'b) up\<^sub>d" ``` nipkow@61515 ` 90` ```where ``` nipkow@61515 ` 91` ```"del k Leaf = T\<^sub>d Leaf" | ``` nipkow@61515 ` 92` ```"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" | ``` nipkow@61515 ` 93` ```"del k (Node3 Leaf p Leaf q Leaf) = ``` nipkow@61515 ` 94` ``` T\<^sub>d(if k=fst p then Node2 Leaf q Leaf else ``` nipkow@61515 ` 95` ``` if k=fst q then Node2 Leaf p Leaf ``` nipkow@61515 ` 96` ``` else Node3 Leaf p Leaf q Leaf)" | ``` nipkow@61515 ` 97` ```"del k (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) = ``` nipkow@61515 ` 98` ``` T\<^sub>d(if k=fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else ``` nipkow@61515 ` 99` ``` if k=fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else ``` nipkow@61515 ` 100` ``` if k=fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf ``` nipkow@61515 ` 101` ``` else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" | ``` nipkow@61515 ` 102` ```"del k (Node2 l a r) = ``` nipkow@61515 ` 103` ``` (if k fst a then node22 l a (del k r) ``` nipkow@61515 ` 105` ``` else let (a',t) = del_min r in node22 l a' t)" | ``` nipkow@61515 ` 106` ```"del k (Node3 l a m b r) = ``` nipkow@61515 ` 107` ``` (if k ('a*'b) tree234 \ ('a*'b) tree234" where ``` nipkow@61515 ` 124` ```"delete k t = tree\<^sub>d(del k t)" ``` nipkow@61515 ` 125` nipkow@61515 ` 126` nipkow@61515 ` 127` ```subsection "Functional correctness" ``` nipkow@61515 ` 128` nipkow@61515 ` 129` ```lemma lookup: "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" ``` nipkow@61515 ` 130` ```by (induction t) (auto simp: map_of_simps split: option.split) ``` nipkow@61515 ` 131` nipkow@61515 ` 132` nipkow@61515 ` 133` ```lemma inorder_upd: ``` nipkow@61515 ` 134` ``` "sorted1(inorder t) \ inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)" ``` nipkow@61515 ` 135` ```by(induction t) ``` nipkow@61515 ` 136` ``` (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits) ``` nipkow@61515 ` 137` nipkow@61515 ` 138` ```lemma inorder_update: ``` nipkow@61515 ` 139` ``` "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)" ``` nipkow@61515 ` 140` ```by(simp add: update_def inorder_upd) ``` nipkow@61515 ` 141` nipkow@61515 ` 142` nipkow@61515 ` 143` ```lemma inorder_del: "\ bal t ; sorted1(inorder t) \ \ ``` nipkow@61515 ` 144` ``` inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" ``` nipkow@61515 ` 145` ```by(induction t rule: del.induct) ``` nipkow@61515 ` 146` ``` ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+ ``` nipkow@61515 ` 147` ```(* 290 secs (2015) *) ``` nipkow@61515 ` 148` nipkow@61515 ` 149` ```lemma inorder_delete: "\ bal t ; sorted1(inorder t) \ \ ``` nipkow@61515 ` 150` ``` inorder(delete x t) = del_list x (inorder t)" ``` nipkow@61515 ` 151` ```by(simp add: delete_def inorder_del) ``` nipkow@61515 ` 152` nipkow@61515 ` 153` nipkow@61515 ` 154` ```subsection \Balancedness\ ``` nipkow@61515 ` 155` nipkow@61515 ` 156` ```lemma bal_upd: "bal t \ bal (tree\<^sub>i(upd x y t)) \ height(upd x y t) = height t" ``` nipkow@61515 ` 157` ```by (induct t) (auto, auto split: up\<^sub>i.split) (* 33 secs (2015) *) ``` nipkow@61515 ` 158` nipkow@61515 ` 159` ```lemma bal_update: "bal t \ bal (update x y t)" ``` nipkow@61515 ` 160` ```by (simp add: update_def bal_upd) ``` nipkow@61515 ` 161` nipkow@61515 ` 162` nipkow@61515 ` 163` ```lemma height_del: "bal t \ height(del x t) = height t" ``` nipkow@61515 ` 164` ```by(induction x t rule: del.induct) ``` nipkow@61515 ` 165` ``` (auto simp add: heights height_del_min split: prod.split) ``` nipkow@61515 ` 166` nipkow@61515 ` 167` ```lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" ``` nipkow@61515 ` 168` ```by(induction x t rule: del.induct) ``` nipkow@61515 ` 169` ``` (auto simp: bals bal_del_min height_del height_del_min split: prod.split) ``` nipkow@61515 ` 170` ```(* 110 secs (2015) *) ``` nipkow@61515 ` 171` nipkow@61515 ` 172` ```corollary bal_delete: "bal t \ bal(delete x t)" ``` nipkow@61515 ` 173` ```by(simp add: delete_def bal_tree\<^sub>d_del) ``` nipkow@61515 ` 174` nipkow@61515 ` 175` nipkow@61515 ` 176` ```subsection \Overall Correctness\ ``` nipkow@61515 ` 177` nipkow@61515 ` 178` ```interpretation T234_Map: Map_by_Ordered ``` nipkow@61515 ` 179` ```where empty = Leaf and lookup = lookup and update = update and delete = delete ``` nipkow@61515 ` 180` ```and inorder = inorder and wf = bal ``` nipkow@61515 ` 181` ```proof (standard, goal_cases) ``` nipkow@61515 ` 182` ``` case 2 thus ?case by(simp add: lookup) ``` nipkow@61515 ` 183` ```next ``` nipkow@61515 ` 184` ``` case 3 thus ?case by(simp add: inorder_update) ``` nipkow@61515 ` 185` ```next ``` nipkow@61515 ` 186` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61515 ` 187` ```next ``` nipkow@61515 ` 188` ``` case 6 thus ?case by(simp add: bal_update) ``` nipkow@61515 ` 189` ```next ``` nipkow@61515 ` 190` ``` case 7 thus ?case by(simp add: bal_delete) ``` nipkow@61515 ` 191` ```qed simp+ ``` nipkow@61515 ` 192` nipkow@61515 ` 193` ```end ```