author | wenzelm |
Thu, 30 May 2013 20:38:50 +0200 | |
changeset 52252 | 81fcc11d8c65 |
parent 45605 | a89b4bc311a5 |
child 55413 | a8e96847523c |
permissions | -rw-r--r-- |
33436 | 1 |
(* Title: HOL/ex/Tree23.thy |
2 |
Author: Tobias Nipkow, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* 2-3 Trees *} |
|
6 |
||
7 |
theory Tree23 |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
11 |
text{* This is a very direct translation of some of the functions in table.ML |
|
12 |
in the Isabelle source code. That source is due to Makarius Wenzel and Stefan |
|
13 |
Berghofer. |
|
14 |
||
15 |
So far this file contains only data types and functions, but no proofs. Feel |
|
16 |
free to have a go at the latter! |
|
17 |
||
18 |
Note that because of complicated patterns and mutual recursion, these |
|
19 |
function definitions take a few minutes and can also be seen as stress tests |
|
20 |
for the function definition facility. *} |
|
21 |
||
42463 | 22 |
type_synonym key = int -- {*for simplicity, should be a type class*} |
33436 | 23 |
|
24 |
datatype ord = LESS | EQUAL | GREATER |
|
25 |
||
26 |
definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)" |
|
27 |
||
28 |
datatype 'a tree23 = |
|
29 |
Empty | |
|
30 |
Branch2 "'a tree23" "key * 'a" "'a tree23" | |
|
31 |
Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23" |
|
32 |
||
33 |
datatype 'a growth = |
|
34 |
Stay "'a tree23" | |
|
35 |
Sprout "'a tree23" "key * 'a" "'a tree23" |
|
36 |
||
37 |
fun add :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a growth" where |
|
38 |
"add key y Empty = Sprout Empty (key,y) Empty" | |
|
39 |
"add key y (Branch2 left (k,x) right) = |
|
40 |
(case ord key k of |
|
41 |
LESS => |
|
42 |
(case add key y left of |
|
43 |
Stay left' => Stay (Branch2 left' (k,x) right) |
|
44 |
| Sprout left1 q left2 |
|
45 |
=> Stay (Branch3 left1 q left2 (k,x) right)) |
|
46 |
| EQUAL => Stay (Branch2 left (k,y) right) |
|
47 |
| GREATER => |
|
48 |
(case add key y right of |
|
49 |
Stay right' => Stay (Branch2 left (k,x) right') |
|
50 |
| Sprout right1 q right2 |
|
51 |
=> Stay (Branch3 left (k,x) right1 q right2)))" | |
|
52 |
"add key y (Branch3 left (k1,x1) mid (k2,x2) right) = |
|
53 |
(case ord key k1 of |
|
54 |
LESS => |
|
55 |
(case add key y left of |
|
56 |
Stay left' => Stay (Branch3 left' (k1,x1) mid (k2,x2) right) |
|
57 |
| Sprout left1 q left2 |
|
58 |
=> Sprout (Branch2 left1 q left2) (k1,x1) (Branch2 mid (k2,x2) right)) |
|
59 |
| EQUAL => Stay (Branch3 left (k1,y) mid (k2,x2) right) |
|
60 |
| GREATER => |
|
61 |
(case ord key k2 of |
|
62 |
LESS => |
|
63 |
(case add key y mid of |
|
64 |
Stay mid' => Stay (Branch3 left (k1,x1) mid' (k2,x2) right) |
|
65 |
| Sprout mid1 q mid2 |
|
66 |
=> Sprout (Branch2 left (k1,x1) mid1) q (Branch2 mid2 (k2,x2) right)) |
|
67 |
| EQUAL => Stay (Branch3 left (k1,x1) mid (k2,y) right) |
|
68 |
| GREATER => |
|
69 |
(case add key y right of |
|
70 |
Stay right' => Stay (Branch3 left (k1,x1) mid (k2,x2) right') |
|
71 |
| Sprout right1 q right2 |
|
72 |
=> Sprout (Branch2 left (k1,x1) mid) (k2,x2) (Branch2 right1 q right2))))" |
|
73 |
||
74 |
definition add0 :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where |
|
75 |
"add0 k y t = |
|
76 |
(case add k y t of Stay t' => t' | Sprout l p r => Branch2 l p r)" |
|
77 |
||
78 |
value "add0 5 e (add0 4 d (add0 3 c (add0 2 b (add0 1 a Empty))))" |
|
79 |
||
80 |
fun compare where |
|
81 |
"compare None (k2, _) = LESS" | |
|
82 |
"compare (Some k1) (k2, _) = ord k1 k2" |
|
83 |
||
84 |
fun if_eq where |
|
85 |
"if_eq EQUAL x y = x" | |
|
86 |
"if_eq _ x y = y" |
|
87 |
||
88 |
fun del :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> ((key * 'a) * bool * 'a tree23)option" |
|
89 |
where |
|
90 |
"del (Some k) Empty = None" | |
|
91 |
"del None (Branch2 Empty p Empty) = Some(p, (True, Empty))" | |
|
92 |
"del None (Branch3 Empty p Empty q Empty) = Some(p, (False, Branch2 Empty q Empty))" | |
|
93 |
"del k (Branch2 Empty p Empty) = (case compare k p of |
|
94 |
EQUAL => Some(p, (True, Empty)) | _ => None)" | |
|
95 |
"del k (Branch3 Empty p Empty q Empty) = (case compare k p of |
|
96 |
EQUAL => Some(p, (False, Branch2 Empty q Empty)) |
|
97 |
| _ => (case compare k q of |
|
98 |
EQUAL => Some(q, (False, Branch2 Empty p Empty)) |
|
99 |
| _ => None))" | |
|
100 |
"del k (Branch2 l p r) = (case compare k p of |
|
101 |
LESS => (case del k l of None \<Rightarrow> None | |
|
102 |
Some(p', (False, l')) => Some(p', (False, Branch2 l' p r)) |
|
103 |
| Some(p', (True, l')) => Some(p', case r of |
|
104 |
Branch2 rl rp rr => (True, Branch3 l' p rl rp rr) |
|
105 |
| Branch3 rl rp rm rq rr => (False, Branch2 |
|
106 |
(Branch2 l' p rl) rp (Branch2 rm rq rr)))) |
|
107 |
| or => (case del (if_eq or None k) r of None \<Rightarrow> None | |
|
108 |
Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r')) |
|
109 |
| Some(p', (True, r')) => Some(p', case l of |
|
110 |
Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r') |
|
111 |
| Branch3 ll lp lm lq lr => (False, Branch2 |
|
112 |
(Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" | |
|
113 |
"del k (Branch3 l p m q r) = (case compare k q of |
|
114 |
LESS => (case compare k p of |
|
115 |
LESS => (case del k l of None \<Rightarrow> None | |
|
116 |
Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r)) |
|
117 |
| Some(p', (True, l')) => Some(p', (False, case (m, r) of |
|
118 |
(Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r |
|
119 |
| (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r |
|
120 |
| (Branch2 ml mp mr, Branch3 rl rp rm rq rr) => |
|
121 |
Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr)))) |
|
122 |
| or => (case del (if_eq or None k) m of None \<Rightarrow> None | |
|
123 |
Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r)) |
|
124 |
| Some(p', (True, m')) => Some(p', (False, case (l, r) of |
|
125 |
(Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r |
|
126 |
| (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r |
|
127 |
| (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr))))) |
|
128 |
| or => (case del (if_eq or None k) r of None \<Rightarrow> None | |
|
129 |
Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r')) |
|
130 |
| Some(q', (True, r')) => Some(q', (False, case (l, m) of |
|
131 |
(Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r') |
|
132 |
| (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r') |
|
133 |
| (Branch3 ll lp lm lq lr, Branch2 ml mp mr) => |
|
134 |
Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))" |
|
135 |
||
136 |
definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where |
|
137 |
"del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')" |
|
138 |
||
45334 | 139 |
text {* Ordered trees *} |
33436 | 140 |
|
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
141 |
definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
142 |
"opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
143 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
144 |
lemma opt_less_simps [simp]: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
145 |
"opt_less None y = True" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
146 |
"opt_less x None = True" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
147 |
"opt_less (Some a) (Some b) = (a < b)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
148 |
unfolding opt_less_def by (auto simp add: ord_def split: option.split) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
149 |
|
45333
04b21922ed68
ex/Tree23.thy: simpler definition of ordered-ness predicate
huffman
parents:
45332
diff
changeset
|
150 |
primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where |
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
151 |
"ord' x Empty y = opt_less x y" | |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
152 |
"ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" | |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
153 |
"ord' x (Branch3 l p m q r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) m (Some (fst q)) & ord' (Some (fst q)) r y)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
154 |
|
45333
04b21922ed68
ex/Tree23.thy: simpler definition of ordered-ness predicate
huffman
parents:
45332
diff
changeset
|
155 |
definition ord0 :: "'a tree23 \<Rightarrow> bool" where |
04b21922ed68
ex/Tree23.thy: simpler definition of ordered-ness predicate
huffman
parents:
45332
diff
changeset
|
156 |
"ord0 t = ord' None t None" |
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
157 |
|
45334 | 158 |
text {* Balanced trees *} |
159 |
||
160 |
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where |
|
161 |
"full 0 Empty" | |
|
162 |
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" | |
|
163 |
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)" |
|
164 |
||
165 |
inductive_cases full_elims: |
|
166 |
"full n Empty" |
|
167 |
"full n (Branch2 l p r)" |
|
168 |
"full n (Branch3 l p m q r)" |
|
169 |
||
170 |
inductive_cases full_0_elim: "full 0 t" |
|
171 |
inductive_cases full_Suc_elim: "full (Suc n) t" |
|
172 |
||
173 |
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty" |
|
174 |
by (auto elim: full_0_elim intro: full.intros) |
|
175 |
||
176 |
lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0" |
|
177 |
by (auto elim: full_elims intro: full.intros) |
|
178 |
||
179 |
lemma full_Suc_Branch2_iff [simp]: |
|
180 |
"full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r" |
|
181 |
by (auto elim: full_elims intro: full.intros) |
|
182 |
||
183 |
lemma full_Suc_Branch3_iff [simp]: |
|
184 |
"full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r" |
|
185 |
by (auto elim: full_elims intro: full.intros) |
|
186 |
||
33436 | 187 |
fun height :: "'a tree23 \<Rightarrow> nat" where |
188 |
"height Empty = 0" | |
|
189 |
"height (Branch2 l _ r) = Suc(max (height l) (height r))" | |
|
190 |
"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
|
191 |
||
192 |
text{* Is a tree balanced? *} |
|
193 |
fun bal :: "'a tree23 \<Rightarrow> bool" where |
|
194 |
"bal Empty = True" | |
|
195 |
"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" | |
|
196 |
"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
|
197 |
||
45334 | 198 |
lemma full_imp_height: "full n t \<Longrightarrow> height t = n" |
199 |
by (induct set: full, simp_all) |
|
200 |
||
201 |
lemma full_imp_bal: "full n t \<Longrightarrow> bal t" |
|
202 |
by (induct set: full, auto dest: full_imp_height) |
|
203 |
||
204 |
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t" |
|
205 |
by (induct t, simp_all) |
|
206 |
||
207 |
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)" |
|
208 |
by (auto elim!: bal_imp_full full_imp_bal) |
|
209 |
||
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
210 |
text {* The @{term "add0"} function either preserves the height of the |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
211 |
tree, or increases it by one. The constructor returned by the @{term |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
212 |
"add"} function determines which: A return value of the form @{term |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
213 |
"Stay t"} indicates that the height will be the same. A value of the |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
214 |
form @{term "Sprout l p r"} indicates an increase in height. *} |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
215 |
|
45334 | 216 |
primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where |
217 |
"gfull n (Stay t) \<longleftrightarrow> full n t" | |
|
218 |
"gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r" |
|
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
219 |
|
45334 | 220 |
lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)" |
45336 | 221 |
by (induct set: full, auto split: ord.split growth.split) |
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
222 |
|
45334 | 223 |
text {* The @{term "add0"} operation preserves balance. *} |
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
224 |
|
45334 | 225 |
lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)" |
226 |
unfolding bal_iff_full add0_def |
|
227 |
apply (erule exE) |
|
228 |
apply (drule gfull_add [of _ _ k y]) |
|
229 |
apply (cases "add k y t") |
|
230 |
apply (auto intro: full.intros) |
|
231 |
done |
|
232 |
||
233 |
text {* The @{term "add0"} operation preserves order. *} |
|
234 |
||
235 |
lemma ord_cases: |
|
236 |
fixes a b :: int obtains |
|
237 |
"ord a b = LESS" and "a < b" | |
|
238 |
"ord a b = EQUAL" and "a = b" | |
|
239 |
"ord a b = GREATER" and "a > b" |
|
240 |
unfolding ord_def by (rule linorder_cases [of a b]) auto |
|
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
241 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
242 |
definition gtree :: "'a growth \<Rightarrow> 'a tree23" where |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
243 |
"gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
244 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
245 |
lemma gtree_simps [simp]: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
246 |
"gtree (Stay t) = t" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
247 |
"gtree (Sprout l p r) = Branch2 l p r" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
248 |
unfolding gtree_def by simp_all |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
249 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
250 |
lemma add0: "add0 k y t = gtree (add k y t)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
251 |
unfolding add0_def by (simp split: growth.split) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
252 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
253 |
lemma ord'_add0: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
254 |
"\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
255 |
unfolding add0 |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
256 |
apply (induct t arbitrary: k1 k2) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
257 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
258 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
259 |
apply (rule_tac a=k and b=a in ord_cases) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
260 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
261 |
apply (case_tac "add k y t1", simp, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
262 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
263 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
264 |
apply (case_tac "add k y t2", simp, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
265 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
266 |
apply (rule_tac a=k and b=a in ord_cases) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
267 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
268 |
apply (case_tac "add k y t1", simp, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
269 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
270 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
271 |
apply (rule_tac a=k and b=aa in ord_cases) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
272 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
273 |
apply (case_tac "add k y t2", simp, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
274 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
275 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
276 |
apply (case_tac "add k y t3", simp, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
277 |
done |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
278 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
279 |
lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)" |
45333
04b21922ed68
ex/Tree23.thy: simpler definition of ordered-ness predicate
huffman
parents:
45332
diff
changeset
|
280 |
by (simp add: ord0_def ord'_add0) |
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
281 |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
282 |
text {* The @{term "del"} function preserves balance. *} |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
283 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
284 |
lemma del_extra_simps: |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
285 |
"l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow> |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
286 |
del k (Branch2 l p r) = (case compare k p of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
287 |
LESS => (case del k l of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
288 |
Some(p', (False, l')) => Some(p', (False, Branch2 l' p r)) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
289 |
| Some(p', (True, l')) => Some(p', case r of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
290 |
Branch2 rl rp rr => (True, Branch3 l' p rl rp rr) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
291 |
| Branch3 rl rp rm rq rr => (False, Branch2 |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
292 |
(Branch2 l' p rl) rp (Branch2 rm rq rr)))) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
293 |
| or => (case del (if_eq or None k) r of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
294 |
Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r')) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
295 |
| Some(p', (True, r')) => Some(p', case l of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
296 |
Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r') |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
297 |
| Branch3 ll lp lm lq lr => (False, Branch2 |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
298 |
(Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
299 |
"l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow> |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
300 |
del k (Branch3 l p m q r) = (case compare k q of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
301 |
LESS => (case compare k p of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
302 |
LESS => (case del k l of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
303 |
Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r)) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
304 |
| Some(p', (True, l')) => Some(p', (False, case (m, r) of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
305 |
(Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
306 |
| (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
307 |
| (Branch2 ml mp mr, Branch3 rl rp rm rq rr) => |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
308 |
Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr)))) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
309 |
| or => (case del (if_eq or None k) m of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
310 |
Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r)) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
311 |
| Some(p', (True, m')) => Some(p', (False, case (l, r) of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
312 |
(Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
313 |
| (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
314 |
| (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr))))) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
315 |
| or => (case del (if_eq or None k) r of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
316 |
Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r')) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
317 |
| Some(q', (True, r')) => Some(q', (False, case (l, m) of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
318 |
(Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r') |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
319 |
| (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r') |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
320 |
| (Branch3 ll lp lm lq lr, Branch2 ml mp mr) => |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
321 |
Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
322 |
apply - |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
323 |
apply (cases l, cases r, simp_all only: del.simps, simp) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
324 |
apply (cases l, cases m, cases r, simp_all only: del.simps, simp) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
325 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
326 |
|
45335 | 327 |
fun dfull where |
328 |
"dfull n None \<longleftrightarrow> True" | |
|
329 |
"dfull n (Some (p, (True, t'))) \<longleftrightarrow> full n t'" | |
|
330 |
"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'" |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
331 |
|
45335 | 332 |
lemmas dfull_case_intros = |
45605 | 333 |
ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"] |
334 |
option.exhaust [where y=y and P="dfull a (option_case b c y)"] |
|
335 |
prod.exhaust [where y=y and P="dfull a (prod_case b y)"] |
|
336 |
bool.exhaust [where y=y and P="dfull a (bool_case b c y)"] |
|
337 |
tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"] |
|
338 |
tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"] |
|
339 |
for a b c d e y |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
340 |
|
45335 | 341 |
lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)" |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
342 |
proof - |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
343 |
{ fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k |
45335 | 344 |
assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)" |
345 |
and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)" |
|
346 |
and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)" |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
347 |
and "full (Suc n) (Branch2 l p r)" |
45335 | 348 |
hence "dfull n (del k (Branch2 l p r))" |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
349 |
apply clarsimp |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
350 |
apply (cases n) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
351 |
apply (cases k) |
45335 | 352 |
apply simp |
353 |
apply (simp split: ord.split) |
|
354 |
apply simp |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
355 |
apply (subst del_extra_simps, force) |
45336 | 356 |
(* This should work, but it is way too slow! |
357 |
apply (force split: ord.split option.split bool.split tree23.split) *) |
|
45335 | 358 |
apply (simp | rule dfull_case_intros)+ |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
359 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
360 |
} note A = this |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
361 |
{ fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k |
45335 | 362 |
assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)" |
363 |
and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) m)" |
|
364 |
and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) m)" |
|
365 |
and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)" |
|
366 |
and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)" |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
367 |
and "full (Suc n) (Branch3 l p m q r)" |
45335 | 368 |
hence "dfull n (del k (Branch3 l p m q r))" |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
369 |
apply clarsimp |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
370 |
apply (cases n) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
371 |
apply (cases k) |
45335 | 372 |
apply simp |
373 |
apply (simp split: ord.split) |
|
374 |
apply simp |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
375 |
apply (subst del_extra_simps, force) |
45335 | 376 |
apply (simp | rule dfull_case_intros)+ |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
377 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
378 |
} note B = this |
45335 | 379 |
show "full (Suc n) t \<Longrightarrow> dfull n (del k t)" |
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
380 |
proof (induct k t arbitrary: n rule: del.induct) |
45335 | 381 |
{ case goal1 thus "dfull n (del (Some k) Empty)" by simp } |
382 |
{ case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp } |
|
383 |
{ case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))" |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
384 |
by simp } |
45335 | 385 |
{ case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))" |
386 |
by (simp split: ord.split) } |
|
387 |
{ case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))" |
|
388 |
by (simp split: ord.split) } |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
389 |
{ case goal26 thus ?case by simp } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
390 |
qed (fact A | fact B)+ |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
391 |
qed |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
392 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
393 |
lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)" |
45335 | 394 |
unfolding bal_iff_full del0_def |
395 |
apply (erule exE) |
|
396 |
apply (case_tac n, simp, simp) |
|
397 |
apply (frule dfull_del [where k="Some k"]) |
|
398 |
apply (cases "del (Some k) t", force) |
|
399 |
apply (case_tac "a", rename_tac p b t', case_tac "b", auto) |
|
400 |
done |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
401 |
|
33436 | 402 |
text{* This is a little test harness and should be commented out once the |
403 |
above functions have been proved correct. *} |
|
404 |
||
405 |
datatype 'a act = Add int 'a | Del int |
|
406 |
||
407 |
fun exec where |
|
408 |
"exec [] t = t" | |
|
409 |
"exec (Add k x # as) t = exec as (add0 k x t)" | |
|
410 |
"exec (Del k # as) t = exec as (del0 k t)" |
|
411 |
||
412 |
text{* Some quick checks: *} |
|
413 |
||
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
414 |
lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
415 |
by (induct as t arbitrary: t rule: exec.induct, |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
416 |
simp_all add: bal_add0 bal_del0) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
417 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
418 |
lemma "bal(exec as Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
419 |
by (simp add: bal_exec) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
420 |
|
33436 | 421 |
lemma "ord0(exec as Empty)" |
422 |
quickcheck |
|
423 |
oops |
|
424 |
||
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
425 |
end |