author | wenzelm |
Mon, 19 Apr 2010 16:04:42 +0200 | |
changeset 36204 | 16c371c6ff86 |
parent 33027 | 9cf389429f6d |
child 36484 | 134ac130a8ed |
permissions | -rw-r--r-- |
23449 | 1 |
(* Title: HOL/MetisTest/BT.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Testing the metis method |
|
5 |
*) |
|
6 |
||
7 |
header {* Binary trees *} |
|
8 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset
|
9 |
theory BT |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset
|
10 |
imports Main |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset
|
11 |
begin |
23449 | 12 |
|
13 |
||
14 |
datatype 'a bt = |
|
15 |
Lf |
|
16 |
| Br 'a "'a bt" "'a bt" |
|
17 |
||
18 |
consts |
|
19 |
n_nodes :: "'a bt => nat" |
|
20 |
n_leaves :: "'a bt => nat" |
|
21 |
depth :: "'a bt => nat" |
|
22 |
reflect :: "'a bt => 'a bt" |
|
23 |
bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
|
24 |
preorder :: "'a bt => 'a list" |
|
25 |
inorder :: "'a bt => 'a list" |
|
26 |
postorder :: "'a bt => 'a list" |
|
27 |
appnd :: "'a bt => 'a bt => 'a bt" |
|
28 |
||
29 |
primrec |
|
30 |
"n_nodes Lf = 0" |
|
31 |
"n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
|
32 |
||
33 |
primrec |
|
34 |
"n_leaves Lf = Suc 0" |
|
35 |
"n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
|
36 |
||
37 |
primrec |
|
38 |
"depth Lf = 0" |
|
39 |
"depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" |
|
40 |
||
41 |
primrec |
|
42 |
"reflect Lf = Lf" |
|
43 |
"reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
|
44 |
||
45 |
primrec |
|
46 |
"bt_map f Lf = Lf" |
|
47 |
"bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
|
48 |
||
49 |
primrec |
|
50 |
"preorder Lf = []" |
|
51 |
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
|
52 |
||
53 |
primrec |
|
54 |
"inorder Lf = []" |
|
55 |
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
|
56 |
||
57 |
primrec |
|
58 |
"postorder Lf = []" |
|
59 |
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
|
60 |
||
61 |
primrec |
|
62 |
"appnd Lf t = t" |
|
63 |
"appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)" |
|
64 |
||
65 |
||
66 |
text {* \medskip BT simplification *} |
|
67 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
68 |
declare [[ atp_problem_prefix = "BT__n_leaves_reflect" ]] |
23449 | 69 |
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
70 |
apply (induct t) |
|
71 |
apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1)) |
|
72 |
apply (metis add_commute n_leaves.simps(2) reflect.simps(2)) |
|
73 |
done |
|
74 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
75 |
declare [[ atp_problem_prefix = "BT__n_nodes_reflect" ]] |
23449 | 76 |
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
77 |
apply (induct t) |
|
78 |
apply (metis reflect.simps(1)) |
|
79 |
apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2)) |
|
80 |
done |
|
81 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
82 |
declare [[ atp_problem_prefix = "BT__depth_reflect" ]] |
23449 | 83 |
lemma depth_reflect: "depth (reflect t) = depth t" |
84 |
apply (induct t) |
|
85 |
apply (metis depth.simps(1) reflect.simps(1)) |
|
29511
7071b017cb35
migrated class package to new locale implementation
haftmann
parents:
28592
diff
changeset
|
86 |
apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2)) |
23449 | 87 |
done |
88 |
||
89 |
text {* |
|
90 |
The famous relationship between the numbers of leaves and nodes. |
|
91 |
*} |
|
92 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
93 |
declare [[ atp_problem_prefix = "BT__n_leaves_nodes" ]] |
23449 | 94 |
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
95 |
apply (induct t) |
|
96 |
apply (metis n_leaves.simps(1) n_nodes.simps(1)) |
|
97 |
apply auto |
|
98 |
done |
|
99 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
100 |
declare [[ atp_problem_prefix = "BT__reflect_reflect_ident" ]] |
23449 | 101 |
lemma reflect_reflect_ident: "reflect (reflect t) = t" |
102 |
apply (induct t) |
|
103 |
apply (metis add_right_cancel reflect.simps(1)); |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset
|
104 |
apply (metis reflect.simps(2)) |
23449 | 105 |
done |
106 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
107 |
declare [[ atp_problem_prefix = "BT__bt_map_ident" ]] |
23449 | 108 |
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" |
109 |
apply (rule ext) |
|
110 |
apply (induct_tac y) |
|
111 |
apply (metis bt_map.simps(1)) |
|
112 |
txt{*BUG involving flex-flex pairs*} |
|
113 |
(* apply (metis bt_map.simps(2)) *) |
|
114 |
apply auto |
|
115 |
done |
|
116 |
||
117 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
118 |
declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]] |
23449 | 119 |
lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)" |
120 |
apply (induct t) |
|
121 |
apply (metis appnd.simps(1) bt_map.simps(1)) |
|
122 |
apply (metis appnd.simps(2) bt_map.simps(2)) (*slow!!*) |
|
123 |
done |
|
124 |
||
125 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
126 |
declare [[ atp_problem_prefix = "BT__bt_map_compose" ]] |
23449 | 127 |
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" |
128 |
apply (induct t) |
|
129 |
apply (metis bt_map.simps(1)) |
|
130 |
txt{*Metis runs forever*} |
|
131 |
(* apply (metis bt_map.simps(2) o_apply)*) |
|
132 |
apply auto |
|
133 |
done |
|
134 |
||
135 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
136 |
declare [[ atp_problem_prefix = "BT__bt_map_reflect" ]] |
23449 | 137 |
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
138 |
apply (induct t) |
|
139 |
apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1)) |
|
140 |
apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2)) |
|
141 |
done |
|
142 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
143 |
declare [[ atp_problem_prefix = "BT__preorder_bt_map" ]] |
23449 | 144 |
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
145 |
apply (induct t) |
|
146 |
apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) |
|
147 |
apply simp |
|
148 |
done |
|
149 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
150 |
declare [[ atp_problem_prefix = "BT__inorder_bt_map" ]] |
23449 | 151 |
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
152 |
apply (induct t) |
|
153 |
apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1)) |
|
154 |
apply simp |
|
155 |
done |
|
156 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
157 |
declare [[ atp_problem_prefix = "BT__postorder_bt_map" ]] |
23449 | 158 |
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
159 |
apply (induct t) |
|
160 |
apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1)) |
|
161 |
apply simp |
|
162 |
done |
|
163 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
164 |
declare [[ atp_problem_prefix = "BT__depth_bt_map" ]] |
23449 | 165 |
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
166 |
apply (induct t) |
|
167 |
apply (metis bt_map.simps(1) depth.simps(1)) |
|
168 |
apply simp |
|
169 |
done |
|
170 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
171 |
declare [[ atp_problem_prefix = "BT__n_leaves_bt_map" ]] |
23449 | 172 |
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
173 |
apply (induct t) |
|
31790 | 174 |
apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1)) |
25457 | 175 |
apply (metis bt_map.simps(2) n_leaves.simps(2)) |
23449 | 176 |
done |
177 |
||
178 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
179 |
declare [[ atp_problem_prefix = "BT__preorder_reflect" ]] |
23449 | 180 |
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
181 |
apply (induct t) |
|
182 |
apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv) |
|
29782 | 183 |
apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident) |
23449 | 184 |
done |
185 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
186 |
declare [[ atp_problem_prefix = "BT__inorder_reflect" ]] |
23449 | 187 |
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
188 |
apply (induct t) |
|
189 |
apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1)) |
|
190 |
apply simp |
|
191 |
done |
|
192 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
193 |
declare [[ atp_problem_prefix = "BT__postorder_reflect" ]] |
23449 | 194 |
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
195 |
apply (induct t) |
|
196 |
apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1)) |
|
25457 | 197 |
apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2) |
23449 | 198 |
done |
199 |
||
200 |
text {* |
|
201 |
Analogues of the standard properties of the append function for lists. |
|
202 |
*} |
|
203 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
204 |
declare [[ atp_problem_prefix = "BT__appnd_assoc" ]] |
23449 | 205 |
lemma appnd_assoc [simp]: |
206 |
"appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)" |
|
207 |
apply (induct t1) |
|
208 |
apply (metis appnd.simps(1)) |
|
209 |
apply (metis appnd.simps(2)) |
|
210 |
done |
|
211 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
212 |
declare [[ atp_problem_prefix = "BT__appnd_Lf2" ]] |
23449 | 213 |
lemma appnd_Lf2 [simp]: "appnd t Lf = t" |
214 |
apply (induct t) |
|
215 |
apply (metis appnd.simps(1)) |
|
216 |
apply (metis appnd.simps(2)) |
|
217 |
done |
|
218 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
219 |
declare [[ atp_problem_prefix = "BT__depth_appnd" ]] |
23449 | 220 |
declare max_add_distrib_left [simp] |
221 |
lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2" |
|
222 |
apply (induct t1) |
|
223 |
apply (metis add_0 appnd.simps(1) depth.simps(1)) |
|
224 |
apply (simp add: ); |
|
225 |
done |
|
226 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
227 |
declare [[ atp_problem_prefix = "BT__n_leaves_appnd" ]] |
23449 | 228 |
lemma n_leaves_appnd [simp]: |
229 |
"n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2" |
|
230 |
apply (induct t1) |
|
231 |
apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) |
|
232 |
apply (simp add: left_distrib) |
|
233 |
done |
|
234 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31790
diff
changeset
|
235 |
declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]] |
26312 | 236 |
lemma (*bt_map_appnd:*) |
23449 | 237 |
"bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)" |
238 |
apply (induct t1) |
|
239 |
apply (metis appnd.simps(1) bt_map_appnd) |
|
240 |
apply (metis bt_map_appnd) |
|
241 |
done |
|
242 |
||
243 |
end |