equal
deleted
inserted
replaced
3 section \<open>Red-Black Tree Implementation of Maps\<close> |
3 section \<open>Red-Black Tree Implementation of Maps\<close> |
4 |
4 |
5 theory RBT_Map |
5 theory RBT_Map |
6 imports |
6 imports |
7 RBT_Set |
7 RBT_Set |
8 Map_by_Ordered |
8 Lookup2 |
9 begin |
9 begin |
10 |
|
11 fun lookup :: "('a::linorder * 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b option" where |
|
12 "lookup Leaf x = None" | |
|
13 "lookup (Node _ l (a,b) r) x = |
|
14 (if x < a then lookup l x else |
|
15 if x > a then lookup r x else Some b)" |
|
16 |
10 |
17 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
11 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
18 "update x y Leaf = R Leaf (x,y) Leaf" | |
12 "update x y Leaf = R Leaf (x,y) Leaf" | |
19 "update x y (B l (a,b) r) = |
13 "update x y (B l (a,b) r) = |
20 (if x < a then bal (update x y l) (a,b) r else |
14 (if x < a then bal (update x y l) (a,b) r else |
39 "deleteR x t1 a t2 = R t1 a (delete x t2)" |
33 "deleteR x t1 a t2 = R t1 a (delete x t2)" |
40 |
34 |
41 |
35 |
42 subsection "Functional Correctness Proofs" |
36 subsection "Functional Correctness Proofs" |
43 |
37 |
44 lemma lookup_eq: |
|
45 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
|
46 by(induction t) |
|
47 (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split) |
|
48 |
|
49 |
|
50 lemma inorder_update: |
38 lemma inorder_update: |
51 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
39 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
52 by(induction x y t rule: update.induct) |
40 by(induction x y t rule: update.induct) |
53 (auto simp: upd_list_simps inorder_bal) |
41 (auto simp: upd_list_simps inorder_bal) |
54 |
42 |
58 "sorted1(inorder t1) \<Longrightarrow> inorder(deleteL x t1 a t2) = |
46 "sorted1(inorder t1) \<Longrightarrow> inorder(deleteL x t1 a t2) = |
59 del_list x (inorder t1) @ a # inorder t2" and |
47 del_list x (inorder t1) @ a # inorder t2" and |
60 "sorted1(inorder t2) \<Longrightarrow> inorder(deleteR x t1 a t2) = |
48 "sorted1(inorder t2) \<Longrightarrow> inorder(deleteR x t1 a t2) = |
61 inorder t1 @ a # del_list x (inorder t2)" |
49 inorder t1 @ a # del_list x (inorder t2)" |
62 by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct) |
50 by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct) |
63 (auto simp: del_list_sorted sorted_lems inorder_combine inorder_balL inorder_balR) |
51 (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) |
64 |
52 |
65 |
53 |
66 interpretation Map_by_Ordered |
54 interpretation Map_by_Ordered |
67 where empty = Leaf and lookup = lookup and update = update and delete = delete |
55 where empty = Leaf and lookup = lookup and update = update and delete = delete |
68 and inorder = inorder and wf = "\<lambda>_. True" |
56 and inorder = inorder and wf = "\<lambda>_. True" |