61525
|
1 |
(*
|
|
2 |
Author: Tobias Nipkow
|
61581
|
3 |
Function defs follow AFP entry Splay_Tree, proofs are new.
|
61525
|
4 |
*)
|
|
5 |
|
|
6 |
section "Splay Tree Implementation of Sets"
|
|
7 |
|
|
8 |
theory Splay_Set
|
|
9 |
imports
|
|
10 |
"~~/src/HOL/Library/Tree"
|
|
11 |
Set_by_Ordered
|
61581
|
12 |
Cmp
|
61525
|
13 |
begin
|
|
14 |
|
|
15 |
function splay :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
|
|
16 |
"splay a Leaf = Leaf" |
|
|
17 |
"splay a (Node t1 a t2) = Node t1 a t2" |
|
|
18 |
"a<b \<Longrightarrow> splay a (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" |
|
|
19 |
"x<a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" |
|
|
20 |
"x<a \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" |
|
|
21 |
"x<a \<Longrightarrow> x<b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow>
|
|
22 |
splay x (Node (Node t1 a t2) b t3) =
|
|
23 |
(case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" |
|
|
24 |
"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" |
|
|
25 |
"a<x \<Longrightarrow> x<b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
|
|
26 |
splay x (Node (Node t1 a t2) b t3) =
|
|
27 |
(case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
|
|
28 |
"a<b \<Longrightarrow> splay b (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" |
|
|
29 |
"a<x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" |
|
|
30 |
"a<x \<Longrightarrow> x<b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
|
|
31 |
splay x (Node t1 a (Node t2 b t3)) =
|
|
32 |
(case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
|
|
33 |
"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" |
|
|
34 |
"a<x \<Longrightarrow> b<x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" |
|
|
35 |
"a<x \<Longrightarrow> b<x \<Longrightarrow> t3 \<noteq> Leaf \<Longrightarrow>
|
|
36 |
splay x (Node t1 a (Node t2 b t3)) =
|
|
37 |
(case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)"
|
|
38 |
apply(atomize_elim)
|
|
39 |
apply(auto)
|
|
40 |
(* 1 subgoal *)
|
|
41 |
apply (subst (asm) neq_Leaf_iff)
|
|
42 |
apply(auto)
|
|
43 |
apply (metis tree.exhaust less_linear)+
|
|
44 |
done
|
|
45 |
|
|
46 |
termination splay
|
|
47 |
by lexicographic_order
|
|
48 |
|
61581
|
49 |
(* no idea why this speeds things up below *)
|
|
50 |
lemma case_tree_cong:
|
|
51 |
"\<lbrakk> x = x'; y = y'; z = z' \<rbrakk> \<Longrightarrow> case_tree x y z = case_tree x' y' z'"
|
|
52 |
by auto
|
|
53 |
|
|
54 |
lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
|
|
55 |
Node al a ar \<Rightarrow> (case cmp x a of
|
|
56 |
EQ \<Rightarrow> t |
|
|
57 |
LT \<Rightarrow> (case al of
|
|
58 |
Leaf \<Rightarrow> t |
|
|
59 |
Node bl b br \<Rightarrow> (case cmp x b of
|
|
60 |
EQ \<Rightarrow> Node bl b (Node br a ar) |
|
|
61 |
LT \<Rightarrow> if bl = Leaf then Node bl b (Node br a ar)
|
|
62 |
else case splay x bl of
|
|
63 |
Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar)) |
|
|
64 |
GT \<Rightarrow> if br = Leaf then Node bl b (Node br a ar)
|
|
65 |
else case splay x br of
|
|
66 |
Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))) |
|
|
67 |
GT \<Rightarrow> (case ar of
|
|
68 |
Leaf \<Rightarrow> t |
|
|
69 |
Node bl b br \<Rightarrow> (case cmp x b of
|
|
70 |
EQ \<Rightarrow> Node (Node al a bl) b br |
|
|
71 |
LT \<Rightarrow> if bl = Leaf then Node (Node al a bl) b br
|
|
72 |
else case splay x bl of
|
|
73 |
Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br) |
|
|
74 |
GT \<Rightarrow> if br=Leaf then Node (Node al a bl) b br
|
|
75 |
else case splay x br of
|
|
76 |
Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr))))"
|
|
77 |
by(auto cong: case_tree_cong split: tree.split)
|
61525
|
78 |
|
|
79 |
definition is_root :: "'a \<Rightarrow> 'a tree \<Rightarrow> bool" where
|
|
80 |
"is_root a t = (case t of Leaf \<Rightarrow> False | Node _ x _ \<Rightarrow> x = a)"
|
|
81 |
|
|
82 |
definition "isin t x = is_root x (splay x t)"
|
|
83 |
|
|
84 |
hide_const (open) insert
|
|
85 |
|
|
86 |
fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
|
|
87 |
"insert x t = (if t = Leaf then Node Leaf x Leaf
|
|
88 |
else case splay x t of
|
|
89 |
Node l a r \<Rightarrow> if x = a then Node l a r
|
|
90 |
else if x < a then Node l x (Node Leaf a r) else Node (Node l a Leaf) x r)"
|
|
91 |
|
|
92 |
|
|
93 |
fun splay_max :: "'a tree \<Rightarrow> 'a tree" where
|
|
94 |
"splay_max Leaf = Leaf" |
|
|
95 |
"splay_max (Node l b Leaf) = Node l b Leaf" |
|
|
96 |
"splay_max (Node l b (Node rl c rr)) =
|
|
97 |
(if rr = Leaf then Node (Node l b rl) c Leaf
|
|
98 |
else case splay_max rr of
|
|
99 |
Node rrl m rrr \<Rightarrow> Node (Node (Node l b rl) c rrl) m rrr)"
|
|
100 |
|
|
101 |
|
|
102 |
definition delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
|
|
103 |
"delete x t = (if t = Leaf then Leaf
|
|
104 |
else case splay x t of Node l a r \<Rightarrow>
|
|
105 |
if x = a
|
|
106 |
then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
|
|
107 |
else Node l a r)"
|
|
108 |
|
|
109 |
|
|
110 |
subsection "Functional Correctness Proofs"
|
|
111 |
|
|
112 |
lemma splay_Leaf_iff: "(splay a t = Leaf) = (t = Leaf)"
|
|
113 |
by(induction a t rule: splay.induct) (auto split: tree.splits)
|
|
114 |
|
|
115 |
lemma splay_max_Leaf_iff: "(splay_max t = Leaf) = (t = Leaf)"
|
|
116 |
by(induction t rule: splay_max.induct)(auto split: tree.splits)
|
|
117 |
|
|
118 |
|
|
119 |
subsubsection "Proofs for isin"
|
|
120 |
|
|
121 |
lemma
|
|
122 |
"splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
|
|
123 |
x \<in> elems (inorder t) \<longleftrightarrow> x=a"
|
|
124 |
by(induction x t arbitrary: l a r rule: splay.induct)
|
|
125 |
(auto simp: elems_simps1 splay_Leaf_iff ball_Un split: tree.splits)
|
|
126 |
|
|
127 |
lemma splay_elemsD:
|
|
128 |
"splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
|
|
129 |
x \<in> elems (inorder t) \<longleftrightarrow> x=a"
|
|
130 |
by(induction x t arbitrary: l a r rule: splay.induct)
|
|
131 |
(auto simp: elems_simps2 splay_Leaf_iff split: tree.splits)
|
|
132 |
|
|
133 |
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
|
|
134 |
by (auto simp: isin_def is_root_def splay_elemsD splay_Leaf_iff split: tree.splits)
|
|
135 |
|
|
136 |
|
|
137 |
subsubsection "Proofs for insert"
|
|
138 |
|
61627
|
139 |
text\<open>Splay trees need two addition @{const sorted} lemmas:\<close>
|
61525
|
140 |
|
|
141 |
lemma sorted_snoc_le:
|
|
142 |
"ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
|
|
143 |
by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def)
|
|
144 |
|
|
145 |
lemma sorted_Cons_le:
|
|
146 |
"ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
|
|
147 |
by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def)
|
|
148 |
|
|
149 |
lemma inorder_splay: "inorder(splay x t) = inorder t"
|
|
150 |
by(induction x t rule: splay.induct)
|
|
151 |
(auto simp: neq_Leaf_iff split: tree.split)
|
|
152 |
|
|
153 |
lemma sorted_splay:
|
|
154 |
"sorted(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
|
|
155 |
sorted(inorder l @ x # inorder r)"
|
|
156 |
unfolding inorder_splay[of x t, symmetric]
|
|
157 |
by(induction x t arbitrary: l a r rule: splay.induct)
|
|
158 |
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
|
|
159 |
|
61627
|
160 |
text\<open>Splay trees need two addition @{const ins_list} lemmas:\<close>
|
|
161 |
|
61525
|
162 |
lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
|
|
163 |
by (induction xs) auto
|
|
164 |
|
|
165 |
lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]"
|
|
166 |
by(induction xs) (auto simp add: sorted_mid_iff2)
|
|
167 |
|
|
168 |
lemma inorder_insert:
|
|
169 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
|
|
170 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
|
|
171 |
by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split)
|
|
172 |
|
|
173 |
|
|
174 |
subsubsection "Proofs for delete"
|
|
175 |
|
61627
|
176 |
text\<open>Splay trees need two addition @{const del_list} lemmas:\<close>
|
61525
|
177 |
|
|
178 |
lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
|
|
179 |
by(induction xs)(auto simp: sorted_Cons_iff)
|
|
180 |
|
|
181 |
lemma del_list_sorted_app:
|
|
182 |
"sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
|
|
183 |
by (induction xs) (auto simp: sorted_mid_iff2)
|
|
184 |
|
|
185 |
lemma inorder_splay_maxD:
|
|
186 |
"splay_max t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
|
|
187 |
inorder l @ [a] = inorder t \<and> r = Leaf"
|
|
188 |
by(induction t arbitrary: l a r rule: splay_max.induct)
|
|
189 |
(auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits)
|
|
190 |
|
|
191 |
lemma inorder_delete:
|
|
192 |
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
|
|
193 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x]
|
|
194 |
by (auto simp: del_list_simps del_list_sorted_app delete_def
|
|
195 |
del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff
|
|
196 |
split: tree.splits)
|
|
197 |
|
|
198 |
|
|
199 |
subsubsection "Overall Correctness"
|
|
200 |
|
|
201 |
interpretation Set_by_Ordered
|
|
202 |
where empty = Leaf and isin = isin and insert = insert
|
61588
|
203 |
and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
|
61525
|
204 |
proof (standard, goal_cases)
|
|
205 |
case 2 thus ?case by(simp add: isin_set)
|
|
206 |
next
|
|
207 |
case 3 thus ?case by(simp add: inorder_insert del: insert.simps)
|
|
208 |
next
|
|
209 |
case 4 thus ?case by(simp add: inorder_delete)
|
|
210 |
qed auto
|
|
211 |
|
|
212 |
end
|