author | wenzelm |
Fri, 12 May 2017 16:32:53 +0200 | |
changeset 65810 | 356c2b488cf3 |
parent 63411 | e051eea34990 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
61525 | 1 |
(* |
2 |
Author: Tobias Nipkow |
|
61696 | 3 |
Function 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 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61712
diff
changeset
|
54 |
lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf | |
61581 | 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 |
|
61712 | 80 |
"is_root x t = (case t of Leaf \<Rightarrow> False | Node l a r \<Rightarrow> x = a)" |
61525 | 81 |
|
82 |
definition "isin t x = is_root x (splay x t)" |
|
83 |
||
84 |
hide_const (open) insert |
|
85 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61712
diff
changeset
|
86 |
fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
61697 | 87 |
"insert x t = |
88 |
(if t = Leaf then Node Leaf x Leaf |
|
89 |
else case splay x t of |
|
90 |
Node l a r \<Rightarrow> |
|
91 |
case cmp x a of |
|
92 |
EQ \<Rightarrow> Node l a r | |
|
93 |
LT \<Rightarrow> Node l x (Node Leaf a r) | |
|
94 |
GT \<Rightarrow> Node (Node l a Leaf) x r)" |
|
61525 | 95 |
|
96 |
||
97 |
fun splay_max :: "'a tree \<Rightarrow> 'a tree" where |
|
98 |
"splay_max Leaf = Leaf" | |
|
99 |
"splay_max (Node l b Leaf) = Node l b Leaf" | |
|
100 |
"splay_max (Node l b (Node rl c rr)) = |
|
101 |
(if rr = Leaf then Node (Node l b rl) c Leaf |
|
102 |
else case splay_max rr of |
|
103 |
Node rrl m rrr \<Rightarrow> Node (Node (Node l b rl) c rrl) m rrr)" |
|
104 |
||
105 |
||
106 |
definition delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
61697 | 107 |
"delete x t = |
108 |
(if t = Leaf then Leaf |
|
109 |
else case splay x t of Node l a r \<Rightarrow> |
|
110 |
if x = a |
|
111 |
then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r |
|
112 |
else Node l a r)" |
|
61525 | 113 |
|
114 |
||
115 |
subsection "Functional Correctness Proofs" |
|
116 |
||
117 |
lemma splay_Leaf_iff: "(splay a t = Leaf) = (t = Leaf)" |
|
118 |
by(induction a t rule: splay.induct) (auto split: tree.splits) |
|
119 |
||
120 |
lemma splay_max_Leaf_iff: "(splay_max t = Leaf) = (t = Leaf)" |
|
121 |
by(induction t rule: splay_max.induct)(auto split: tree.splits) |
|
122 |
||
123 |
||
124 |
subsubsection "Proofs for isin" |
|
125 |
||
126 |
lemma |
|
127 |
"splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow> |
|
128 |
x \<in> elems (inorder t) \<longleftrightarrow> x=a" |
|
129 |
by(induction x t arbitrary: l a r rule: splay.induct) |
|
130 |
(auto simp: elems_simps1 splay_Leaf_iff ball_Un split: tree.splits) |
|
131 |
||
132 |
lemma splay_elemsD: |
|
133 |
"splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow> |
|
134 |
x \<in> elems (inorder t) \<longleftrightarrow> x=a" |
|
135 |
by(induction x t arbitrary: l a r rule: splay.induct) |
|
136 |
(auto simp: elems_simps2 splay_Leaf_iff split: tree.splits) |
|
137 |
||
138 |
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))" |
|
139 |
by (auto simp: isin_def is_root_def splay_elemsD splay_Leaf_iff split: tree.splits) |
|
140 |
||
141 |
||
142 |
subsubsection "Proofs for insert" |
|
143 |
||
144 |
lemma inorder_splay: "inorder(splay x t) = inorder t" |
|
145 |
by(induction x t rule: splay.induct) |
|
146 |
(auto simp: neq_Leaf_iff split: tree.split) |
|
147 |
||
148 |
lemma sorted_splay: |
|
149 |
"sorted(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow> |
|
150 |
sorted(inorder l @ x # inorder r)" |
|
151 |
unfolding inorder_splay[of x t, symmetric] |
|
152 |
by(induction x t arbitrary: l a r rule: splay.induct) |
|
153 |
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits) |
|
154 |
||
155 |
lemma inorder_insert: |
|
156 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
|
157 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x] |
|
158 |
by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split) |
|
159 |
||
160 |
||
161 |
subsubsection "Proofs for delete" |
|
162 |
||
163 |
lemma inorder_splay_maxD: |
|
164 |
"splay_max t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow> |
|
165 |
inorder l @ [a] = inorder t \<and> r = Leaf" |
|
166 |
by(induction t arbitrary: l a r rule: splay_max.induct) |
|
167 |
(auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits) |
|
168 |
||
169 |
lemma inorder_delete: |
|
170 |
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
|
171 |
using inorder_splay[of x t, symmetric] sorted_splay[of t x] |
|
172 |
by (auto simp: del_list_simps del_list_sorted_app delete_def |
|
173 |
del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff |
|
174 |
split: tree.splits) |
|
175 |
||
176 |
||
177 |
subsubsection "Overall Correctness" |
|
178 |
||
179 |
interpretation Set_by_Ordered |
|
180 |
where empty = Leaf and isin = isin and insert = insert |
|
61588 | 181 |
and delete = delete and inorder = inorder and inv = "\<lambda>_. True" |
61525 | 182 |
proof (standard, goal_cases) |
183 |
case 2 thus ?case by(simp add: isin_set) |
|
184 |
next |
|
185 |
case 3 thus ?case by(simp add: inorder_insert del: insert.simps) |
|
186 |
next |
|
187 |
case 4 thus ?case by(simp add: inorder_delete) |
|
188 |
qed auto |
|
189 |
||
190 |
end |