6 imports |
6 imports |
7 AVL_Set |
7 AVL_Set |
8 Lookup2 |
8 Lookup2 |
9 begin |
9 begin |
10 |
10 |
11 fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
11 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
12 "update x y Leaf = Node 1 Leaf (x,y) Leaf" | |
12 "update x y Leaf = Node 1 Leaf (x,y) Leaf" | |
13 "update x y (Node h l (a,b) r) = (case cmp x a of |
13 "update x y (Node h l (a,b) r) = (case cmp x a of |
14 EQ \<Rightarrow> Node h l (x,y) r | |
14 EQ \<Rightarrow> Node h l (x,y) r | |
15 LT \<Rightarrow> balL (update x y l) (a,b) r | |
15 LT \<Rightarrow> balL (update x y l) (a,b) r | |
16 GT \<Rightarrow> balR l (a,b) (update x y r))" |
16 GT \<Rightarrow> balR l (a,b) (update x y r))" |
17 |
17 |
18 fun delete :: "'a::cmp \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
18 fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
19 "delete _ Leaf = Leaf" | |
19 "delete _ Leaf = Leaf" | |
20 "delete x (Node h l (a,b) r) = (case cmp x a of |
20 "delete x (Node h l (a,b) r) = (case cmp x a of |
21 EQ \<Rightarrow> del_root (Node h l (a,b) r) | |
21 EQ \<Rightarrow> del_root (Node h l (a,b) r) | |
22 LT \<Rightarrow> balR (delete x l) (a,b) r | |
22 LT \<Rightarrow> balR (delete x l) (a,b) r | |
23 GT \<Rightarrow> balL l (a,b) (delete x r))" |
23 GT \<Rightarrow> balL l (a,b) (delete x r))" |