author | huffman |
Thu, 03 Nov 2011 17:40:50 +0100 | |
changeset 45332 | ede9dc025150 |
parent 45325 | 26b6179b5a45 |
child 45333 | 04b21922ed68 |
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 |
||
139 |
||
140 |
(* yes, this is rather slow *) |
|
141 |
fun ord0 :: "'a tree23 \<Rightarrow> bool" |
|
142 |
and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool" |
|
143 |
and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool" |
|
144 |
and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool" |
|
145 |
where |
|
146 |
"ord0 Empty = True" | |
|
147 |
"ord0 (Branch2 l p r) = (ordr l (fst p) & ordl (fst p) r)" | |
|
148 |
"ord0 (Branch3 l p m q r) = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | |
|
149 |
||
150 |
"ordl _ Empty = True" | |
|
151 |
"ordl x (Branch2 l p r) = (ordlr x l (fst p) & ordl (fst p) r)" | |
|
152 |
"ordl x (Branch3 l p m q r) = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | |
|
153 |
||
154 |
"ordr Empty _ = True" | |
|
155 |
"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" | |
|
156 |
"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" | |
|
157 |
||
158 |
"ordlr x Empty y = (x < y)" | |
|
159 |
"ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" | |
|
160 |
"ordlr x (Branch3 l p m q r) y = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r y)" |
|
161 |
||
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
162 |
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
|
163 |
"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
|
164 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
165 |
lemma opt_less_simps [simp]: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
166 |
"opt_less None y = True" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
167 |
"opt_less x None = True" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
168 |
"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
|
169 |
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
|
170 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
171 |
fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
172 |
"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
|
173 |
"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
|
174 |
"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
|
175 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
176 |
lemma ord': |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
177 |
"ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y') |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
178 |
| Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
179 |
by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
180 |
|
33436 | 181 |
fun height :: "'a tree23 \<Rightarrow> nat" where |
182 |
"height Empty = 0" | |
|
183 |
"height (Branch2 l _ r) = Suc(max (height l) (height r))" | |
|
184 |
"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" |
|
185 |
||
186 |
text{* Is a tree balanced? *} |
|
187 |
fun bal :: "'a tree23 \<Rightarrow> bool" where |
|
188 |
"bal Empty = True" | |
|
189 |
"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" | |
|
190 |
"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" |
|
191 |
||
45325
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
"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
|
195 |
"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
|
196 |
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
|
197 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
198 |
fun gheight :: "'a growth \<Rightarrow> nat" where |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
199 |
"gheight (Stay t) = height t" | |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
200 |
"gheight (Sprout l p r) = max (height l) (height r)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
201 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
202 |
lemma gheight_add: "gheight (add k y t) = height t" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
203 |
apply (induct t) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
204 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
205 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
206 |
apply (case_tac "ord k a") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
207 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
208 |
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
|
209 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
210 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
211 |
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
|
212 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
213 |
apply (case_tac "ord k a") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
214 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
215 |
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
|
216 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
217 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
218 |
apply (case_tac "ord k aa") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
219 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
220 |
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
|
221 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
222 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
223 |
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
|
224 |
done |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
225 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
226 |
lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
227 |
using gheight_add [of k y t] by simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
228 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
229 |
lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
230 |
using gheight_add [of k y t] by simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
231 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
232 |
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
|
233 |
"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
|
234 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
235 |
lemma gtree_simps [simp]: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
236 |
"gtree (Stay t) = t" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
237 |
"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
|
238 |
unfolding gtree_def by simp_all |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
239 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
240 |
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
|
241 |
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
|
242 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
243 |
text {* The @{term "add0"} operation preserves balance. *} |
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 bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
246 |
unfolding add0 |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
247 |
apply (induct t) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
248 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
249 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
250 |
apply (case_tac "ord k a") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
251 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
252 |
apply (case_tac "add k y t1") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
253 |
apply (simp, drule add_eq_Stay_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
254 |
apply (simp, drule add_eq_Sprout_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
255 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
256 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
257 |
apply (case_tac "add k y t2") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
258 |
apply (simp, drule add_eq_Stay_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
259 |
apply (simp, drule add_eq_Sprout_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
260 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
261 |
apply (case_tac "ord k a") |
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 (case_tac "add k y t1") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
264 |
apply (simp, drule add_eq_Stay_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
265 |
apply (simp, drule add_eq_Sprout_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
266 |
apply simp |
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 "ord k aa") |
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 (case_tac "add k y t2") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
271 |
apply (simp, drule add_eq_Stay_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
272 |
apply (simp, drule add_eq_Sprout_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
273 |
apply 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 (case_tac "add k y t3") |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
276 |
apply (simp, drule add_eq_Stay_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
277 |
apply (simp, drule add_eq_Sprout_dest, simp) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
278 |
done |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
279 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
280 |
text {* The @{term "add0"} operation preserves order. *} |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
281 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
282 |
lemma ord_cases: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
283 |
fixes a b :: int obtains |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
284 |
"ord a b = LESS" and "a < b" | |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
285 |
"ord a b = EQUAL" and "a = b" | |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
286 |
"ord a b = GREATER" and "a > b" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
287 |
unfolding ord_def by (rule linorder_cases [of a b]) auto |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
288 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
289 |
lemma ord'_add0: |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
290 |
"\<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
|
291 |
unfolding add0 |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
292 |
apply (induct t arbitrary: k1 k2) |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
293 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
294 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
295 |
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
|
296 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
297 |
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
|
298 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
299 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
300 |
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
|
301 |
apply clarsimp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
302 |
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
|
303 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
304 |
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
|
305 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
306 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
307 |
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
|
308 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
309 |
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
|
310 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
311 |
apply simp |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
312 |
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
|
313 |
done |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
314 |
|
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
315 |
lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)" |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
316 |
using ord'_add0 [of None t None k y] by (simp add: ord') |
26b6179b5a45
ex/Tree23.thy: prove that insertion preserves tree balance and order
huffman
parents:
42463
diff
changeset
|
317 |
|
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
318 |
text {* The @{term "del"} function preserves balance. *} |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
319 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
320 |
lemma del_extra_simps: |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
321 |
"l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow> |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
322 |
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
|
323 |
LESS => (case del k l of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
324 |
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
|
325 |
| Some(p', (True, l')) => Some(p', case r of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
326 |
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
|
327 |
| Branch3 rl rp rm rq rr => (False, Branch2 |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
328 |
(Branch2 l' p rl) rp (Branch2 rm rq rr)))) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
329 |
| 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
|
330 |
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
|
331 |
| Some(p', (True, r')) => Some(p', case l of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
332 |
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
|
333 |
| Branch3 ll lp lm lq lr => (False, Branch2 |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
334 |
(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
|
335 |
"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
|
336 |
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
|
337 |
LESS => (case compare k p of |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
338 |
LESS => (case del k l of None \<Rightarrow> None | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
339 |
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
|
340 |
| 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
|
341 |
(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
|
342 |
| (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
|
343 |
| (Branch2 ml mp mr, Branch3 rl rp rm rq rr) => |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
344 |
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
|
345 |
| 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
|
346 |
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
|
347 |
| 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
|
348 |
(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
|
349 |
| (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
|
350 |
| (_, 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
|
351 |
| 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
|
352 |
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
|
353 |
| 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
|
354 |
(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
|
355 |
| (_, 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
|
356 |
| (Branch3 ll lp lm lq lr, Branch2 ml mp mr) => |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
357 |
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
|
358 |
apply - |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
359 |
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
|
360 |
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
|
361 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
362 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
363 |
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
364 |
"full 0 Empty" | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
365 |
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" | |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
366 |
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
367 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
368 |
inductive_cases full_elims: |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
369 |
"full n Empty" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
370 |
"full n (Branch2 l p r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
371 |
"full n (Branch3 l p m q r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
372 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
373 |
inductive_cases full_0_elim: "full 0 t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
374 |
inductive_cases full_Suc_elim: "full (Suc n) t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
375 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
376 |
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
377 |
by (auto elim: full_0_elim intro: full.intros) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
378 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
379 |
lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
380 |
by (auto elim: full_elims intro: full.intros) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
381 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
382 |
lemma full_Suc_Branch2_iff [simp]: |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
383 |
"full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
384 |
by (auto elim: full_elims intro: full.intros) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
385 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
386 |
lemma full_Suc_Branch3_iff [simp]: |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
387 |
"full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
388 |
by (auto elim: full_elims intro: full.intros) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
389 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
390 |
definition |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
391 |
"full_del n k t = (case del k t of None \<Rightarrow> True | Some (p, b, t') \<Rightarrow> full (if b then n else Suc n) t')" |
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 |
lemmas ord_case = ord.exhaust [where y=y and P="ord_case a b c y", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
394 |
lemmas option_ord_case = ord.exhaust [where y=y and P="option_case a b (ord_case d e f y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
395 |
lemmas option_option_case = option.exhaust [where y=y and P="option_case a b (option_case d e y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
396 |
lemmas option_prod_case = prod.exhaust [where y=y and P="option_case a b (prod_case c y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
397 |
lemmas option_bool_case = bool.exhaust [where y=y and P="option_case a b (bool_case c d y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
398 |
lemmas prod_tree23_case = tree23.exhaust [where y=y and P="prod_case a (tree23_case b c d y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
399 |
lemmas option_case = option.exhaust [where y=y and P="option_case a b y", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
400 |
lemmas full_tree23_case = tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard] |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
401 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
402 |
lemmas case_intros = |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
403 |
option_ord_case option_option_case option_prod_case option_bool_case prod_tree23_case option_case |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
404 |
full_tree23_case |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
405 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
406 |
lemma full_del: "full (Suc n) t \<Longrightarrow> full_del n k t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
407 |
proof - |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
408 |
{ fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
409 |
assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
410 |
and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
411 |
and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
412 |
and "full (Suc n) (Branch2 l p r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
413 |
hence "full_del n k (Branch2 l p r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
414 |
apply clarsimp |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
415 |
apply (cases n) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
416 |
apply (cases k) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
417 |
apply (simp add: full_del_def) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
418 |
apply (simp add: full_del_def split: ord.split) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
419 |
apply (simp add: full_del_def) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
420 |
apply (subst del_extra_simps, force) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
421 |
apply (simp | rule case_intros)+ |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
422 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
423 |
} note A = this |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
424 |
{ fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
425 |
assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
426 |
and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) m" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
427 |
and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) m" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
428 |
and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
429 |
and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
430 |
and "full (Suc n) (Branch3 l p m q r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
431 |
hence "full_del n k (Branch3 l p m q r)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
432 |
apply clarsimp |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
433 |
apply (cases n) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
434 |
apply (cases k) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
435 |
apply (simp add: full_del_def) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
436 |
apply (simp add: full_del_def split: ord.split) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
437 |
apply (simp add: full_del_def) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
438 |
apply (subst del_extra_simps, force) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
439 |
apply (simp | rule case_intros)+ |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
440 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
441 |
} note B = this |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
442 |
show "full (Suc n) t \<Longrightarrow> full_del n k t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
443 |
proof (induct k t arbitrary: n rule: del.induct) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
444 |
{ case goal1 thus "full_del n (Some k) Empty" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
445 |
by simp } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
446 |
{ case goal2 thus "full_del n None (Branch2 Empty p Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
447 |
unfolding full_del_def by auto } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
448 |
{ case goal3 thus "full_del n None (Branch3 Empty p Empty q Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
449 |
unfolding full_del_def by auto } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
450 |
{ case goal4 thus "full_del n (Some v) (Branch2 Empty p Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
451 |
unfolding full_del_def by (auto split: ord.split) } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
452 |
{ case goal5 thus "full_del n (Some v) (Branch3 Empty p Empty q Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
453 |
unfolding full_del_def by (auto split: ord.split) } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
454 |
{ case goal26 thus ?case by simp } |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
455 |
qed (fact A | fact B)+ |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
456 |
qed |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
457 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
458 |
lemma full_imp_height: "full n t \<Longrightarrow> height t = n" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
459 |
by (induct set: full, simp_all) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
460 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
461 |
lemma full_imp_bal: "full n t \<Longrightarrow> bal t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
462 |
by (induct set: full, auto dest: full_imp_height) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
463 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
464 |
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
465 |
by (induct t, simp_all) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
466 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
467 |
lemma bal_iff_full: "bal t \<longleftrightarrow> full (height t) t" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
468 |
using bal_imp_full full_imp_bal .. |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
469 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
470 |
lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
471 |
unfolding del0_def |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
472 |
apply (drule bal_imp_full) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
473 |
apply (case_tac "height t", simp, simp) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
474 |
apply (frule full_del [where k="Some k"]) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
475 |
apply (simp add: full_del_def) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
476 |
apply (auto split: option.split elim: full_imp_bal) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
477 |
done |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
478 |
|
33436 | 479 |
text{* This is a little test harness and should be commented out once the |
480 |
above functions have been proved correct. *} |
|
481 |
||
482 |
datatype 'a act = Add int 'a | Del int |
|
483 |
||
484 |
fun exec where |
|
485 |
"exec [] t = t" | |
|
486 |
"exec (Add k x # as) t = exec as (add0 k x t)" | |
|
487 |
"exec (Del k # as) t = exec as (del0 k t)" |
|
488 |
||
489 |
text{* Some quick checks: *} |
|
490 |
||
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
491 |
lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
492 |
by (induct as t arbitrary: t rule: exec.induct, |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
493 |
simp_all add: bal_add0 bal_del0) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
494 |
|
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
495 |
lemma "bal(exec as Empty)" |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
496 |
by (simp add: bal_exec) |
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
497 |
|
33436 | 498 |
lemma "ord0(exec as Empty)" |
499 |
quickcheck |
|
500 |
oops |
|
501 |
||
45332
ede9dc025150
ex/Tree23.thy: prove that deletion preserves balance
huffman
parents:
45325
diff
changeset
|
502 |
end |