author | wenzelm |
Fri, 23 Nov 2018 16:43:11 +0100 | |
changeset 69334 | 6b49700da068 |
parent 68440 | 6826718f732d |
child 70755 | 3fb16bed5d6c |
permissions | -rw-r--r-- |
61232 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section "AVL Tree Implementation of Maps" |
|
4 |
||
5 |
theory AVL_Map |
|
6 |
imports |
|
7 |
AVL_Set |
|
8 |
Lookup2 |
|
9 |
begin |
|
10 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
11 |
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
68413 | 12 |
"update x y Leaf = Node Leaf (x,y) 1 Leaf" | |
13 |
"update x y (Node l (a,b) h r) = (case cmp x a of |
|
14 |
EQ \<Rightarrow> Node l (x,y) h r | |
|
61581 | 15 |
LT \<Rightarrow> balL (update x y l) (a,b) r | |
16 |
GT \<Rightarrow> balR l (a,b) (update x y r))" |
|
61232 | 17 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
18 |
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
61232 | 19 |
"delete _ Leaf = Leaf" | |
68413 | 20 |
"delete x (Node l (a,b) h r) = (case cmp x a of |
21 |
EQ \<Rightarrow> del_root (Node l (a,b) h r) | |
|
61581 | 22 |
LT \<Rightarrow> balR (delete x l) (a,b) r | |
23 |
GT \<Rightarrow> balL l (a,b) (delete x r))" |
|
61232 | 24 |
|
25 |
||
68422 | 26 |
subsection \<open>Functional Correctness\<close> |
61232 | 27 |
|
68440 | 28 |
theorem inorder_update: |
61232 | 29 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
61581 | 30 |
by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) |
61232 | 31 |
|
32 |
||
68440 | 33 |
theorem inorder_delete: |
61232 | 34 |
"sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
35 |
by(induction t) |
|
61581 | 36 |
(auto simp: del_list_simps inorder_balL inorder_balR |
68023 | 37 |
inorder_del_root inorder_split_maxD split: prod.splits) |
61232 | 38 |
|
68422 | 39 |
|
40 |
subsection \<open>AVL invariants\<close> |
|
41 |
||
42 |
||
43 |
subsubsection \<open>Insertion maintains AVL balance\<close> |
|
44 |
||
45 |
theorem avl_update: |
|
46 |
assumes "avl t" |
|
47 |
shows "avl(update x y t)" |
|
48 |
"(height (update x y t) = height t \<or> height (update x y t) = height t + 1)" |
|
49 |
using assms |
|
50 |
proof (induction x y t rule: update.induct) |
|
51 |
case eq2: (2 x y l a b h r) |
|
52 |
case 1 |
|
53 |
show ?case |
|
54 |
proof(cases "x = a") |
|
55 |
case True with eq2 1 show ?thesis by simp |
|
56 |
next |
|
57 |
case False |
|
58 |
with eq2 1 show ?thesis |
|
59 |
proof(cases "x<a") |
|
60 |
case True with eq2 1 show ?thesis by (auto simp add:avl_balL) |
|
61 |
next |
|
62 |
case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR) |
|
63 |
qed |
|
64 |
qed |
|
65 |
case 2 |
|
66 |
show ?case |
|
67 |
proof(cases "x = a") |
|
68 |
case True with eq2 1 show ?thesis by simp |
|
69 |
next |
|
70 |
case False |
|
71 |
show ?thesis |
|
72 |
proof(cases "x<a") |
|
73 |
case True |
|
74 |
show ?thesis |
|
75 |
proof(cases "height (update x y l) = height r + 2") |
|
76 |
case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) |
|
77 |
next |
|
78 |
case True |
|
79 |
hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or> |
|
80 |
(height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B") |
|
81 |
using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all |
|
82 |
thus ?thesis |
|
83 |
proof |
|
84 |
assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) |
|
85 |
next |
|
86 |
assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith |
|
87 |
qed |
|
88 |
qed |
|
89 |
next |
|
90 |
case False |
|
91 |
show ?thesis |
|
92 |
proof(cases "height (update x y r) = height l + 2") |
|
93 |
case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) |
|
94 |
next |
|
95 |
case True |
|
96 |
hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or> |
|
97 |
(height (balR l (a,b) (update x y r)) = height l + 3)" (is "?A \<or> ?B") |
|
98 |
using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all |
|
99 |
thus ?thesis |
|
100 |
proof |
|
101 |
assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) |
|
102 |
next |
|
103 |
assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith |
|
104 |
qed |
|
105 |
qed |
|
106 |
qed |
|
107 |
qed |
|
108 |
qed simp_all |
|
109 |
||
110 |
||
111 |
subsubsection \<open>Deletion maintains AVL balance\<close> |
|
112 |
||
113 |
theorem avl_delete: |
|
114 |
assumes "avl t" |
|
115 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" |
|
116 |
using assms |
|
117 |
proof (induct t) |
|
118 |
case (Node l n h r) |
|
119 |
obtain a b where [simp]: "n = (a,b)" by fastforce |
|
120 |
case 1 |
|
121 |
show ?case |
|
122 |
proof(cases "x = a") |
|
123 |
case True with Node 1 show ?thesis by (auto simp:avl_del_root) |
|
124 |
next |
|
125 |
case False |
|
126 |
show ?thesis |
|
127 |
proof(cases "x<a") |
|
128 |
case True with Node 1 show ?thesis by (auto simp add:avl_balR) |
|
129 |
next |
|
130 |
case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL) |
|
131 |
qed |
|
132 |
qed |
|
133 |
case 2 |
|
134 |
show ?case |
|
135 |
proof(cases "x = a") |
|
136 |
case True |
|
137 |
with 1 have "height (Node l n h r) = height(del_root (Node l n h r)) |
|
138 |
\<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1" |
|
139 |
by (subst height_del_root,simp_all) |
|
140 |
with True show ?thesis by simp |
|
141 |
next |
|
142 |
case False |
|
143 |
show ?thesis |
|
144 |
proof(cases "x<a") |
|
145 |
case True |
|
146 |
show ?thesis |
|
147 |
proof(cases "height r = height (delete x l) + 2") |
|
148 |
case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def) |
|
149 |
next |
|
150 |
case True |
|
151 |
hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or> |
|
152 |
height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B") |
|
153 |
using Node 2 by (intro height_balR) auto |
|
154 |
thus ?thesis |
|
155 |
proof |
|
156 |
assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
|
157 |
next |
|
158 |
assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
|
159 |
qed |
|
160 |
qed |
|
161 |
next |
|
162 |
case False |
|
163 |
show ?thesis |
|
164 |
proof(cases "height l = height (delete x r) + 2") |
|
165 |
case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def) |
|
166 |
next |
|
167 |
case True |
|
168 |
hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or> |
|
169 |
height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B") |
|
170 |
using Node 2 by (intro height_balL) auto |
|
171 |
thus ?thesis |
|
172 |
proof |
|
173 |
assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
|
174 |
next |
|
175 |
assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
|
176 |
qed |
|
177 |
qed |
|
178 |
qed |
|
179 |
qed |
|
180 |
qed simp_all |
|
181 |
||
182 |
||
68440 | 183 |
interpretation M: Map_by_Ordered |
68431 | 184 |
where empty = empty and lookup = lookup and update = update and delete = delete |
68422 | 185 |
and inorder = inorder and inv = avl |
61232 | 186 |
proof (standard, goal_cases) |
68431 | 187 |
case 1 show ?case by (simp add: empty_def) |
61232 | 188 |
next |
61790 | 189 |
case 2 thus ?case by(simp add: lookup_map_of) |
61232 | 190 |
next |
68440 | 191 |
case 3 thus ?case by(simp add: inorder_update) |
61232 | 192 |
next |
68440 | 193 |
case 4 thus ?case by(simp add: inorder_delete) |
68422 | 194 |
next |
68431 | 195 |
case 5 show ?case by (simp add: empty_def) |
68422 | 196 |
next |
197 |
case 6 thus ?case by(simp add: avl_update(1)) |
|
198 |
next |
|
199 |
case 7 thus ?case by(simp add: avl_delete(1)) |
|
200 |
qed |
|
61232 | 201 |
|
202 |
end |