1(* Author: Tobias Nipkow *) 2 3section \<open>2-3 Tree Implementation of Maps\<close> 4 5theory Tree23_Map 6imports 7 Tree23_Set 8 Map_Specs 9begin 10 11fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where 12"lookup Leaf x = None" | 13"lookup (Node2 l (a,b) r) x = (case cmp x a of 14 LT \<Rightarrow> lookup l x | 15 GT \<Rightarrow> lookup r x | 16 EQ \<Rightarrow> Some b)" | 17"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of 18 LT \<Rightarrow> lookup l x | 19 EQ \<Rightarrow> Some b1 | 20 GT \<Rightarrow> (case cmp x a2 of 21 LT \<Rightarrow> lookup m x | 22 EQ \<Rightarrow> Some b2 | 23 GT \<Rightarrow> lookup r x))" 24 25fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where 26"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" | 27"upd x y (Node2 l ab r) = (case cmp x (fst ab) of 28 LT \<Rightarrow> (case upd x y l of 29 T\<^sub>i l' => T\<^sub>i (Node2 l' ab r) 30 | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) | 31 EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) | 32 GT \<Rightarrow> (case upd x y r of 33 T\<^sub>i r' => T\<^sub>i (Node2 l ab r') 34 | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" | 35"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of 36 LT \<Rightarrow> (case upd x y l of 37 T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r) 38 | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) | 39 EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) | 40 GT \<Rightarrow> (case cmp x (fst ab2) of 41 LT \<Rightarrow> (case upd x y m of 42 T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r) 43 | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) | 44 EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) | 45 GT \<Rightarrow> (case upd x y r of 46 T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r') 47 | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" 48 49definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where 50"update a b t = tree\<^sub>i(upd a b t)" 51 52fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where 53"del x Leaf = T\<^sub>d Leaf" | 54"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" | 55"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf 56 else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" | 57"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of 58 LT \<Rightarrow> node21 (del x l) ab1 r | 59 GT \<Rightarrow> node22 l ab1 (del x r) | 60 EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" | 61"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of 62 LT \<Rightarrow> node31 (del x l) ab1 m ab2 r | 63 EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r | 64 GT \<Rightarrow> (case cmp x (fst ab2) of 65 LT \<Rightarrow> node32 l ab1 (del x m) ab2 r | 66 EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' | 67 GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" 68 69definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where 70"delete x t = tree\<^sub>d(del x t)" 71 72 73subsection \<open>Functional Correctness\<close> 74 75lemma lookup_map_of: 76 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" 77by (induction t) (auto simp: map_of_simps split: option.split) 78 79 80lemma inorder_upd: 81 "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)" 82by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits) 83 84corollary inorder_update: 85 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" 86by(simp add: update_def inorder_upd) 87 88 89lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> 90 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" 91by(induction t rule: del.induct) 92 (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) 93 94corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> 95 inorder(delete x t) = del_list x (inorder t)" 96by(simp add: delete_def inorder_del) 97 98 99subsection \<open>Balancedness\<close> 100 101lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t" 102by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *) 103 104corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)" 105by (simp add: update_def bal_upd) 106 107 108lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t" 109by(induction x t rule: del.induct) 110 (auto simp add: heights max_def height_split_min split: prod.split) 111 112lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))" 113by(induction x t rule: del.induct) 114 (auto simp: bals bal_split_min height_del height_split_min split: prod.split) 115 116corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)" 117by(simp add: delete_def bal_tree\<^sub>d_del) 118 119 120subsection \<open>Overall Correctness\<close> 121 122interpretation M: Map_by_Ordered 123where empty = empty and lookup = lookup and update = update and delete = delete 124and inorder = inorder and inv = bal 125proof (standard, goal_cases) 126 case 1 thus ?case by(simp add: empty_def) 127next 128 case 2 thus ?case by(simp add: lookup_map_of) 129next 130 case 3 thus ?case by(simp add: inorder_update) 131next 132 case 4 thus ?case by(simp add: inorder_delete) 133next 134 case 5 thus ?case by(simp add: empty_def) 135next 136 case 6 thus ?case by(simp add: bal_update) 137next 138 case 7 thus ?case by(simp add: bal_delete) 139qed 140 141end 142