6 imports |
6 imports |
7 RBT_Set |
7 RBT_Set |
8 Lookup2 |
8 Lookup2 |
9 begin |
9 begin |
10 |
10 |
11 fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
11 fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
12 "upd x y Leaf = R Leaf (x,y) Leaf" | |
12 "upd x y Leaf = R Leaf (x,y) Leaf" | |
13 "upd x y (B l (a,b) r) = (case cmp x a of |
13 "upd x y (B l (a,b) r) = (case cmp x a of |
14 LT \<Rightarrow> bal (upd x y l) (a,b) r | |
14 LT \<Rightarrow> bal (upd x y l) (a,b) r | |
15 GT \<Rightarrow> bal l (a,b) (upd x y r) | |
15 GT \<Rightarrow> bal l (a,b) (upd x y r) | |
16 EQ \<Rightarrow> B l (x,y) r)" | |
16 EQ \<Rightarrow> B l (x,y) r)" | |
17 "upd x y (R l (a,b) r) = (case cmp x a of |
17 "upd x y (R l (a,b) r) = (case cmp x a of |
18 LT \<Rightarrow> R (upd x y l) (a,b) r | |
18 LT \<Rightarrow> R (upd x y l) (a,b) r | |
19 GT \<Rightarrow> R l (a,b) (upd x y r) | |
19 GT \<Rightarrow> R l (a,b) (upd x y r) | |
20 EQ \<Rightarrow> R l (x,y) r)" |
20 EQ \<Rightarrow> R l (x,y) r)" |
21 |
21 |
22 definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
22 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
23 "update x y t = paint Black (upd x y t)" |
23 "update x y t = paint Black (upd x y t)" |
24 |
24 |
25 fun del :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
25 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
26 and delL :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
26 and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
27 and delR :: "'a::cmp \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
27 and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
28 where |
28 where |
29 "del x Leaf = Leaf" | |
29 "del x Leaf = Leaf" | |
30 "del x (Node c t1 (a,b) t2) = (case cmp x a of |
30 "del x (Node c t1 (a,b) t2) = (case cmp x a of |
31 LT \<Rightarrow> delL x t1 (a,b) t2 | |
31 LT \<Rightarrow> delL x t1 (a,b) t2 | |
32 GT \<Rightarrow> delR x t1 (a,b) t2 | |
32 GT \<Rightarrow> delR x t1 (a,b) t2 | |
34 "delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" | |
34 "delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" | |
35 "delL x t1 a t2 = R (del x t1) a t2" | |
35 "delL x t1 a t2 = R (del x t1) a t2" | |
36 "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | |
36 "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | |
37 "delR x t1 a t2 = R t1 a (del x t2)" |
37 "delR x t1 a t2 = R t1 a (del x t2)" |
38 |
38 |
39 definition delete :: "'a::cmp \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
39 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
40 "delete x t = paint Black (del x t)" |
40 "delete x t = paint Black (del x t)" |
41 |
41 |
42 |
42 |
43 subsection "Functional Correctness Proofs" |
43 subsection "Functional Correctness Proofs" |
44 |
44 |