author | haftmann |
Thu, 23 Nov 2017 17:03:27 +0000 | |
changeset 67087 | 733017b19de9 |
parent 64960 | 8be78855ee7a |
child 68413 | b56ed5010e69 |
permissions | -rw-r--r-- |
61224 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section \<open>Red-Black Tree Implementation of Maps\<close> |
|
4 |
||
5 |
theory RBT_Map |
|
6 |
imports |
|
7 |
RBT_Set |
|
61231 | 8 |
Lookup2 |
61224 | 9 |
begin |
10 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
11 |
fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
61749 | 12 |
"upd x y Leaf = R Leaf (x,y) Leaf" | |
13 |
"upd x y (B l (a,b) r) = (case cmp x a of |
|
64960 | 14 |
LT \<Rightarrow> baliL (upd x y l) (a,b) r | |
15 |
GT \<Rightarrow> baliR l (a,b) (upd x y r) | |
|
61581 | 16 |
EQ \<Rightarrow> B l (x,y) r)" | |
61749 | 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 | |
|
19 |
GT \<Rightarrow> R l (a,b) (upd x y r) | |
|
61581 | 20 |
EQ \<Rightarrow> R l (x,y) r)" |
61224 | 21 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
22 |
definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
61749 | 23 |
"update x y t = paint Black (upd x y t)" |
24 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
25 |
fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
26 |
and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
27 |
and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
61224 | 28 |
where |
61749 | 29 |
"del x Leaf = Leaf" | |
30 |
"del x (Node c t1 (a,b) t2) = (case cmp x a of |
|
31 |
LT \<Rightarrow> delL x t1 (a,b) t2 | |
|
32 |
GT \<Rightarrow> delR x t1 (a,b) t2 | |
|
61581 | 33 |
EQ \<Rightarrow> combine t1 t2)" | |
64960 | 34 |
"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" | |
61749 | 35 |
"delL x t1 a t2 = R (del x t1) a t2" | |
64960 | 36 |
"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | |
61749 | 37 |
"delR x t1 a t2 = R t1 a (del x t2)" |
38 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
39 |
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
61749 | 40 |
"delete x t = paint Black (del x t)" |
61224 | 41 |
|
42 |
||
43 |
subsection "Functional Correctness Proofs" |
|
44 |
||
61749 | 45 |
lemma inorder_upd: |
46 |
"sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)" |
|
47 |
by(induction x y t rule: upd.induct) |
|
64960 | 48 |
(auto simp: upd_list_simps inorder_baliL inorder_baliR) |
61749 | 49 |
|
61224 | 50 |
lemma inorder_update: |
51 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
|
61749 | 52 |
by(simp add: update_def inorder_upd inorder_paint) |
61224 | 53 |
|
61749 | 54 |
lemma inorder_del: |
55 |
"sorted1(inorder t1) \<Longrightarrow> inorder(del x t1) = del_list x (inorder t1)" and |
|
56 |
"sorted1(inorder t1) \<Longrightarrow> inorder(delL x t1 a t2) = |
|
57 |
del_list x (inorder t1) @ a # inorder t2" and |
|
58 |
"sorted1(inorder t2) \<Longrightarrow> inorder(delR x t1 a t2) = |
|
59 |
inorder t1 @ a # del_list x (inorder t2)" |
|
60 |
by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct) |
|
64960 | 61 |
(auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) |
61224 | 62 |
|
63 |
lemma inorder_delete: |
|
61749 | 64 |
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
65 |
by(simp add: delete_def inorder_del inorder_paint) |
|
61224 | 66 |
|
67 |
interpretation Map_by_Ordered |
|
68 |
where empty = Leaf and lookup = lookup and update = update and delete = delete |
|
61686 | 69 |
and inorder = inorder and inv = "\<lambda>_. True" |
61224 | 70 |
proof (standard, goal_cases) |
71 |
case 1 show ?case by simp |
|
72 |
next |
|
61790 | 73 |
case 2 thus ?case by(simp add: lookup_map_of) |
61224 | 74 |
next |
75 |
case 3 thus ?case by(simp add: inorder_update) |
|
76 |
next |
|
77 |
case 4 thus ?case by(simp add: inorder_delete) |
|
61686 | 78 |
qed auto |
61224 | 79 |
|
80 |
end |