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