author | nipkow |
Thu, 07 Jul 2016 18:08:02 +0200 | |
changeset 63411 | e051eea34990 |
parent 61696 | ce6320b9ef9b |
permissions | -rw-r--r-- |
61525 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section "Splay Tree Implementation of Maps" |
|
4 |
||
5 |
theory Splay_Map |
|
6 |
imports |
|
7 |
Splay_Set |
|
8 |
Map_by_Ordered |
|
9 |
begin |
|
10 |
||
11 |
function splay :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
|
12 |
"splay x Leaf = Leaf" | |
|
13 |
"x = fst a \<Longrightarrow> splay x (Node t1 a t2) = Node t1 a t2" | |
|
14 |
"x = fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" | |
|
15 |
"x < fst a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" | |
|
16 |
"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" | |
|
17 |
"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow> |
|
18 |
splay x (Node (Node t1 a t2) b t3) = |
|
19 |
(case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" | |
|
20 |
"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" | |
|
21 |
"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow> |
|
22 |
splay x (Node (Node t1 a t2) b t3) = |
|
23 |
(case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" | |
|
24 |
"fst a < x \<Longrightarrow> x = fst b \<Longrightarrow> splay x (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" | |
|
25 |
"fst a < x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" | |
|
26 |
"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow> |
|
27 |
splay x (Node t1 a (Node t2 b t3)) = |
|
28 |
(case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" | |
|
29 |
"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" | |
|
30 |
"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" | |
|
31 |
"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> t3 \<noteq> Leaf \<Longrightarrow> |
|
32 |
splay x (Node t1 a (Node t2 b t3)) = |
|
33 |
(case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)" |
|
34 |
apply(atomize_elim) |
|
35 |
apply(auto) |
|
36 |
(* 1 subgoal *) |
|
37 |
apply (subst (asm) neq_Leaf_iff) |
|
38 |
apply(auto) |
|
39 |
apply (metis tree.exhaust surj_pair less_linear)+ |
|
40 |
done |
|
41 |
||
42 |
termination splay |
|
43 |
by lexicographic_order |
|
44 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61696
diff
changeset
|
45 |
lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf | |
61581 | 46 |
Node al a ar \<Rightarrow> (case cmp x (fst a) of |
47 |
EQ \<Rightarrow> t | |
|
48 |
LT \<Rightarrow> (case al of |
|
49 |
Leaf \<Rightarrow> t | |
|
50 |
Node bl b br \<Rightarrow> (case cmp x (fst b) of |
|
51 |
EQ \<Rightarrow> Node bl b (Node br a ar) | |
|
52 |
LT \<Rightarrow> if bl = Leaf then Node bl b (Node br a ar) |
|
53 |
else case splay x bl of |
|
54 |
Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar)) | |
|
55 |
GT \<Rightarrow> if br = Leaf then Node bl b (Node br a ar) |
|
56 |
else case splay x br of |
|
57 |
Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))) | |
|
58 |
GT \<Rightarrow> (case ar of |
|
59 |
Leaf \<Rightarrow> t | |
|
60 |
Node bl b br \<Rightarrow> (case cmp x (fst b) of |
|
61 |
EQ \<Rightarrow> Node (Node al a bl) b br | |
|
62 |
LT \<Rightarrow> if bl = Leaf then Node (Node al a bl) b br |
|
63 |
else case splay x bl of |
|
64 |
Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br) | |
|
65 |
GT \<Rightarrow> if br=Leaf then Node (Node al a bl) b br |
|
66 |
else case splay x br of |
|
67 |
Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr))))" |
|
68 |
by(auto cong: case_tree_cong split: tree.split) |
|
61525 | 69 |
|
70 |
definition lookup :: "('a*'b)tree \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where "lookup t x = |
|
71 |
(case splay x t of Leaf \<Rightarrow> None | Node _ (a,b) _ \<Rightarrow> if x=a then Some b else None)" |
|
72 |
||
73 |
hide_const (open) insert |
|
74 |
||
75 |
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
|
76 |
"update x y t = (if t = Leaf then Node Leaf (x,y) Leaf |
|
77 |
else case splay x t of |
|
78 |
Node l a r \<Rightarrow> if x = fst a then Node l (x,y) r |
|
79 |
else if x < fst a then Node l (x,y) (Node Leaf a r) else Node (Node l a Leaf) (x,y) r)" |
|
80 |
||
81 |
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
|
82 |
"delete x t = (if t = Leaf then Leaf |
|
83 |
else case splay x t of Node l a r \<Rightarrow> |
|
84 |
if x = fst a |
|
85 |
then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r |
|
86 |
else Node l a r)" |
|
87 |
||
88 |
||
89 |
subsection "Functional Correctness Proofs" |
|
90 |
||
91 |
lemma splay_Leaf_iff: "(splay x t = Leaf) = (t = Leaf)" |
|
92 |
by(induction x t rule: splay.induct) (auto split: tree.splits) |
|
93 |
||
94 |
||
95 |
subsubsection "Proofs for lookup" |
|
96 |
||
97 |
lemma splay_map_of_inorder: |
|
98 |
"splay x t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> |
|
99 |
map_of (inorder t) x = (if x = fst a then Some(snd a) else None)" |
|
100 |
by(induction x t arbitrary: l a r rule: splay.induct) |
|
101 |
(auto simp: map_of_simps splay_Leaf_iff split: tree.splits) |
|
102 |
||
103 |
lemma lookup_eq: |
|
104 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
|
105 |
by(auto simp: lookup_def splay_Leaf_iff splay_map_of_inorder split: tree.split) |
|
106 |
||
107 |
||
108 |
subsubsection "Proofs for update" |
|
109 |
||
110 |
lemma inorder_splay: "inorder(splay x t) = inorder t" |
|
111 |
by(induction x t rule: splay.induct) |
|
112 |
(auto simp: neq_Leaf_iff split: tree.split) |
|
113 |
||
114 |
lemma sorted_splay: |
|
115 |
"sorted1(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow> |
|
116 |
sorted(map fst (inorder l) @ x # map fst (inorder r))" |
|
117 |
unfolding inorder_splay[of x t, symmetric] |
|
118 |
by(induction x t arbitrary: l a r rule: splay.induct) |
|
119 |
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits) |
|
120 |
||
121 |
lemma inorder_update: |
|
122 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
|
123 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x] |
|
124 |
by(auto simp: upd_list_simps upd_list_Cons upd_list_snoc neq_Leaf_iff split: tree.split) |
|
125 |
||
126 |
||
127 |
subsubsection "Proofs for delete" |
|
128 |
||
129 |
lemma inorder_splay_maxD: |
|
130 |
"splay_max t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> |
|
131 |
inorder l @ [a] = inorder t \<and> r = Leaf" |
|
132 |
by(induction t arbitrary: l a r rule: splay_max.induct) |
|
133 |
(auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits) |
|
134 |
||
135 |
lemma inorder_delete: |
|
136 |
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
|
137 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x] |
|
138 |
by (auto simp: del_list_simps del_list_sorted_app delete_def |
|
139 |
del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff |
|
140 |
split: tree.splits) |
|
141 |
||
142 |
||
143 |
subsubsection "Overall Correctness" |
|
144 |
||
145 |
interpretation Map_by_Ordered |
|
146 |
where empty = Leaf and lookup = lookup and update = update |
|
61686 | 147 |
and delete = delete and inorder = inorder and inv = "\<lambda>_. True" |
61525 | 148 |
proof (standard, goal_cases) |
149 |
case 2 thus ?case by(simp add: lookup_eq) |
|
150 |
next |
|
151 |
case 3 thus ?case by(simp add: inorder_update del: update.simps) |
|
152 |
next |
|
153 |
case 4 thus ?case by(simp add: inorder_delete) |
|
154 |
qed auto |
|
155 |
||
156 |
end |