71814
|
1 |
(* Tobias Nipkow *)
|
|
2 |
|
71818
|
3 |
section "AVL Tree with Balance Factors"
|
71814
|
4 |
|
|
5 |
theory AVL_Bal_Set
|
|
6 |
imports
|
|
7 |
Cmp
|
|
8 |
Isin2
|
|
9 |
begin
|
|
10 |
|
|
11 |
datatype bal = Lh | Bal | Rh
|
|
12 |
|
|
13 |
type_synonym 'a tree_bal = "('a * bal) tree"
|
|
14 |
|
|
15 |
text \<open>Invariant:\<close>
|
|
16 |
|
|
17 |
fun avl :: "'a tree_bal \<Rightarrow> bool" where
|
|
18 |
"avl Leaf = True" |
|
|
19 |
"avl (Node l (a,b) r) =
|
|
20 |
((case b of
|
|
21 |
Bal \<Rightarrow> height r = height l |
|
|
22 |
Lh \<Rightarrow> height l = height r + 1 |
|
|
23 |
Rh \<Rightarrow> height r = height l + 1)
|
|
24 |
\<and> avl l \<and> avl r)"
|
|
25 |
|
|
26 |
|
|
27 |
subsection \<open>Code\<close>
|
|
28 |
|
71828
|
29 |
datatype 'a alt = Same 'a | Diff 'a
|
71814
|
30 |
|
71828
|
31 |
type_synonym 'a tree_bal2 = "'a tree_bal alt"
|
|
32 |
|
|
33 |
fun tree :: "'a alt \<Rightarrow> 'a" where
|
71814
|
34 |
"tree(Same t) = t" |
|
|
35 |
"tree(Diff t) = t"
|
|
36 |
|
71820
|
37 |
fun rot2 where
|
|
38 |
"rot2 A a B c C = (case B of
|
|
39 |
(Node B\<^sub>1 (b, bb) B\<^sub>2) \<Rightarrow>
|
|
40 |
let b\<^sub>1 = if bb = Rh then Lh else Bal;
|
|
41 |
b\<^sub>2 = if bb = Lh then Rh else Bal
|
|
42 |
in Node (Node A (a,b\<^sub>1) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,b\<^sub>2) C))"
|
71814
|
43 |
|
71818
|
44 |
fun balL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
|
71815
|
45 |
"balL AB' c bc C = (case AB' of
|
|
46 |
Same AB \<Rightarrow> Same (Node AB (c,bc) C) |
|
|
47 |
Diff AB \<Rightarrow> (case bc of
|
|
48 |
Bal \<Rightarrow> Diff (Node AB (c,Lh) C) |
|
|
49 |
Rh \<Rightarrow> Same (Node AB (c,Bal) C) |
|
71824
|
50 |
Lh \<Rightarrow> (case AB of
|
|
51 |
Node A (a,Lh) B \<Rightarrow> Same(Node A (a,Bal) (Node B (c,Bal) C)) |
|
|
52 |
Node A (a,Rh) B \<Rightarrow> Same(rot2 A a B c C))))"
|
71814
|
53 |
|
71818
|
54 |
fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
|
71815
|
55 |
"balR A a ba BC' = (case BC' of
|
|
56 |
Same BC \<Rightarrow> Same (Node A (a,ba) BC) |
|
|
57 |
Diff BC \<Rightarrow> (case ba of
|
|
58 |
Bal \<Rightarrow> Diff (Node A (a,Rh) BC) |
|
|
59 |
Lh \<Rightarrow> Same (Node A (a,Bal) BC) |
|
71824
|
60 |
Rh \<Rightarrow> (case BC of
|
|
61 |
Node B (c,Rh) C \<Rightarrow> Same(Node (Node A (a,Bal) B) (c,Bal) C) |
|
|
62 |
Node B (c,Lh) C \<Rightarrow> Same(rot2 A a B c C))))"
|
71814
|
63 |
|
71828
|
64 |
fun ins :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
|
|
65 |
"ins x Leaf = Diff(Node Leaf (x, Bal) Leaf)" |
|
|
66 |
"ins x (Node l (a, b) r) = (case cmp x a of
|
71814
|
67 |
EQ \<Rightarrow> Same(Node l (a, b) r) |
|
71828
|
68 |
LT \<Rightarrow> balL (ins x l) a b r |
|
|
69 |
GT \<Rightarrow> balR l a b (ins x r))"
|
|
70 |
|
|
71 |
definition insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
|
|
72 |
"insert x t = tree(ins x t)"
|
71814
|
73 |
|
71818
|
74 |
fun baldR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
|
71816
|
75 |
"baldR AB c bc C' = (case C' of
|
|
76 |
Same C \<Rightarrow> Same (Node AB (c,bc) C) |
|
|
77 |
Diff C \<Rightarrow> (case bc of
|
|
78 |
Bal \<Rightarrow> Same (Node AB (c,Lh) C) |
|
|
79 |
Rh \<Rightarrow> Diff (Node AB (c,Bal) C) |
|
71814
|
80 |
Lh \<Rightarrow> (case AB of
|
71816
|
81 |
Node A (a,Lh) B \<Rightarrow> Diff(Node A (a,Bal) (Node B (c,Bal) C)) |
|
|
82 |
Node A (a,Bal) B \<Rightarrow> Same(Node A (a,Rh) (Node B (c,Lh) C)) |
|
71820
|
83 |
Node A (a,Rh) B \<Rightarrow> Diff(rot2 A a B c C))))"
|
71814
|
84 |
|
71818
|
85 |
fun baldL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
|
71816
|
86 |
"baldL A' a ba BC = (case A' of
|
|
87 |
Same A \<Rightarrow> Same (Node A (a,ba) BC) |
|
|
88 |
Diff A \<Rightarrow> (case ba of
|
|
89 |
Bal \<Rightarrow> Same (Node A (a,Rh) BC) |
|
|
90 |
Lh \<Rightarrow> Diff (Node A (a,Bal) BC) |
|
71814
|
91 |
Rh \<Rightarrow> (case BC of
|
71816
|
92 |
Node B (c,Rh) C \<Rightarrow> Diff(Node (Node A (a,Bal) B) (c,Bal) C) |
|
|
93 |
Node B (c,Bal) C \<Rightarrow> Same(Node (Node A (a,Rh) B) (c,Lh) C) |
|
71820
|
94 |
Node B (c,Lh) C \<Rightarrow> Diff(rot2 A a B c C))))"
|
71814
|
95 |
|
71818
|
96 |
fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal2 * 'a" where
|
71814
|
97 |
"split_max (Node l (a, ba) r) =
|
|
98 |
(if r = Leaf then (Diff l,a) else let (r',a') = split_max r in (baldR l a ba r', a'))"
|
|
99 |
|
71828
|
100 |
fun del :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
|
|
101 |
"del _ Leaf = Same Leaf" |
|
|
102 |
"del x (Node l (a, ba) r) =
|
71814
|
103 |
(case cmp x a of
|
|
104 |
EQ \<Rightarrow> if l = Leaf then Diff r
|
|
105 |
else let (l', a') = split_max l in baldL l' a' ba r |
|
71828
|
106 |
LT \<Rightarrow> baldL (del x l) a ba r |
|
|
107 |
GT \<Rightarrow> baldR l a ba (del x r))"
|
|
108 |
|
|
109 |
definition delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
|
|
110 |
"delete x t = tree(del x t)"
|
71814
|
111 |
|
|
112 |
lemmas split_max_induct = split_max.induct[case_names Node Leaf]
|
|
113 |
|
71828
|
114 |
lemmas splits = if_splits tree.splits alt.splits bal.splits
|
71814
|
115 |
|
|
116 |
subsection \<open>Proofs\<close>
|
|
117 |
|
71828
|
118 |
subsubsection "Proofs about insertion"
|
71814
|
119 |
|
71828
|
120 |
lemma avl_ins_case: "avl t \<Longrightarrow> case ins x t of
|
71814
|
121 |
Same t' \<Rightarrow> avl t' \<and> height t' = height t |
|
71824
|
122 |
Diff t' \<Rightarrow> avl t' \<and> height t' = height t + 1 \<and>
|
|
123 |
(\<forall>l a r. t' = Node l (a,Bal) r \<longrightarrow> a = x \<and> l = Leaf \<and> r = Leaf)"
|
71828
|
124 |
apply(induction x t rule: ins.induct)
|
71814
|
125 |
apply(auto simp: max_absorb1 split!: splits)
|
|
126 |
done
|
|
127 |
|
71828
|
128 |
corollary avl_insert: "avl t \<Longrightarrow> avl(insert x t)"
|
|
129 |
using avl_ins_case[of t x] by (simp add: insert_def split: splits)
|
71814
|
130 |
|
71828
|
131 |
(* The following aux lemma simplifies the inorder_ins proof *)
|
71824
|
132 |
|
71828
|
133 |
lemma ins_Diff[simp]: "avl t \<Longrightarrow>
|
|
134 |
ins x t \<noteq> Diff Leaf \<and>
|
|
135 |
(ins x t = Diff (Node l (a,Bal) r) \<longleftrightarrow> t = Leaf \<and> a = x \<and> l=Leaf \<and> r=Leaf) \<and>
|
|
136 |
ins x t \<noteq> Diff (Node l (a,Rh) Leaf) \<and>
|
|
137 |
ins x t \<noteq> Diff (Node Leaf (a,Lh) r)"
|
|
138 |
by(drule avl_ins_case[of _ x]) (auto split: splits)
|
71824
|
139 |
|
71828
|
140 |
theorem inorder_ins:
|
|
141 |
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder(tree(ins x t)) = ins_list x (inorder t)"
|
71824
|
142 |
apply(induction t)
|
|
143 |
apply (auto simp: ins_list_simps split!: splits)
|
|
144 |
done
|
|
145 |
|
71814
|
146 |
|
71828
|
147 |
subsubsection "Proofs about deletion"
|
71814
|
148 |
|
|
149 |
lemma inorder_baldL:
|
|
150 |
"\<lbrakk> ba = Rh \<longrightarrow> r \<noteq> Leaf; avl r \<rbrakk>
|
|
151 |
\<Longrightarrow> inorder (tree(baldL l a ba r)) = inorder (tree l) @ a # inorder r"
|
|
152 |
by (auto split: splits)
|
|
153 |
|
|
154 |
lemma inorder_baldR:
|
|
155 |
"\<lbrakk> ba = Lh \<longrightarrow> l \<noteq> Leaf; avl l \<rbrakk>
|
|
156 |
\<Longrightarrow> inorder (tree(baldR l a ba r)) = inorder l @ a # inorder (tree r)"
|
|
157 |
by (auto split: splits)
|
|
158 |
|
|
159 |
lemma avl_split_max:
|
|
160 |
"\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> case t' of
|
|
161 |
Same t' \<Rightarrow> avl t' \<and> height t = height t' |
|
|
162 |
Diff t' \<Rightarrow> avl t' \<and> height t = height t' + 1"
|
|
163 |
apply(induction t arbitrary: t' a rule: split_max_induct)
|
|
164 |
apply(fastforce simp: max_absorb1 max_absorb2 split!: splits prod.splits)
|
|
165 |
apply simp
|
|
166 |
done
|
|
167 |
|
71828
|
168 |
lemma avl_del_case: "avl t \<Longrightarrow> case del x t of
|
71814
|
169 |
Same t' \<Rightarrow> avl t' \<and> height t = height t' |
|
|
170 |
Diff t' \<Rightarrow> avl t' \<and> height t = height t' + 1"
|
71828
|
171 |
apply(induction x t rule: del.induct)
|
71814
|
172 |
apply(auto simp: max_absorb1 max_absorb2 dest: avl_split_max split!: splits prod.splits)
|
|
173 |
done
|
|
174 |
|
71828
|
175 |
corollary avl_delete: "avl t \<Longrightarrow> avl(delete x t)"
|
|
176 |
using avl_del_case[of t x] by(simp add: delete_def split: splits)
|
71814
|
177 |
|
|
178 |
lemma inorder_split_maxD:
|
|
179 |
"\<lbrakk> split_max t = (t',a); t \<noteq> Leaf; avl t \<rbrakk> \<Longrightarrow>
|
|
180 |
inorder (tree t') @ [a] = inorder t"
|
|
181 |
apply(induction t arbitrary: t' rule: split_max.induct)
|
|
182 |
apply(fastforce split!: splits prod.splits)
|
|
183 |
apply simp
|
|
184 |
done
|
|
185 |
|
|
186 |
lemma neq_Leaf_if_height_neq_0[simp]: "height t \<noteq> 0 \<Longrightarrow> t \<noteq> Leaf"
|
|
187 |
by auto
|
|
188 |
|
71828
|
189 |
theorem inorder_del:
|
|
190 |
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder (tree(del x t)) = del_list x (inorder t)"
|
71814
|
191 |
apply(induction t rule: tree2_induct)
|
|
192 |
apply(auto simp: del_list_simps inorder_baldL inorder_baldR avl_delete inorder_split_maxD
|
|
193 |
simp del: baldR.simps baldL.simps split!: splits prod.splits)
|
|
194 |
done
|
|
195 |
|
|
196 |
|
|
197 |
subsubsection \<open>Set Implementation\<close>
|
|
198 |
|
|
199 |
interpretation S: Set_by_Ordered
|
|
200 |
where empty = Leaf and isin = isin
|
71828
|
201 |
and insert = insert
|
|
202 |
and delete = delete
|
71814
|
203 |
and inorder = inorder and inv = avl
|
|
204 |
proof (standard, goal_cases)
|
|
205 |
case 1 show ?case by (simp)
|
|
206 |
next
|
|
207 |
case 2 thus ?case by(simp add: isin_set_inorder)
|
|
208 |
next
|
71828
|
209 |
case 3 thus ?case by(simp add: inorder_ins insert_def)
|
71814
|
210 |
next
|
71828
|
211 |
case 4 thus ?case by(simp add: inorder_del delete_def)
|
71814
|
212 |
next
|
71828
|
213 |
case 5 thus ?case by (simp)
|
71814
|
214 |
next
|
|
215 |
case 6 thus ?case by (simp add: avl_insert)
|
|
216 |
next
|
|
217 |
case 7 thus ?case by (simp add: avl_delete)
|
|
218 |
qed
|
|
219 |
|
|
220 |
end
|