64 "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)" |
64 "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)" |
65 |
65 |
66 |
66 |
67 text {* \medskip BT simplification *} |
67 text {* \medskip BT simplification *} |
68 |
68 |
69 ML {*AtpThread.problem_name := "BT__n_leaves_reflect"*} |
69 ML {*AtpWrapper.problem_name := "BT__n_leaves_reflect"*} |
70 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
70 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
71 apply (induct t) |
71 apply (induct t) |
72 apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1)) |
72 apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1)) |
73 apply (metis add_commute n_leaves.simps(2) reflect.simps(2)) |
73 apply (metis add_commute n_leaves.simps(2) reflect.simps(2)) |
74 done |
74 done |
75 |
75 |
76 ML {*AtpThread.problem_name := "BT__n_nodes_reflect"*} |
76 ML {*AtpWrapper.problem_name := "BT__n_nodes_reflect"*} |
77 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
77 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
78 apply (induct t) |
78 apply (induct t) |
79 apply (metis reflect.simps(1)) |
79 apply (metis reflect.simps(1)) |
80 apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2)) |
80 apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2)) |
81 done |
81 done |
82 |
82 |
83 ML {*AtpThread.problem_name := "BT__depth_reflect"*} |
83 ML {*AtpWrapper.problem_name := "BT__depth_reflect"*} |
84 lemma depth_reflect: "depth (reflect t) = depth t" |
84 lemma depth_reflect: "depth (reflect t) = depth t" |
85 apply (induct t) |
85 apply (induct t) |
86 apply (metis depth.simps(1) reflect.simps(1)) |
86 apply (metis depth.simps(1) reflect.simps(1)) |
87 apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2)) |
87 apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2)) |
88 done |
88 done |
89 |
89 |
90 text {* |
90 text {* |
91 The famous relationship between the numbers of leaves and nodes. |
91 The famous relationship between the numbers of leaves and nodes. |
92 *} |
92 *} |
93 |
93 |
94 ML {*AtpThread.problem_name := "BT__n_leaves_nodes"*} |
94 ML {*AtpWrapper.problem_name := "BT__n_leaves_nodes"*} |
95 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
95 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
96 apply (induct t) |
96 apply (induct t) |
97 apply (metis n_leaves.simps(1) n_nodes.simps(1)) |
97 apply (metis n_leaves.simps(1) n_nodes.simps(1)) |
98 apply auto |
98 apply auto |
99 done |
99 done |
100 |
100 |
101 ML {*AtpThread.problem_name := "BT__reflect_reflect_ident"*} |
101 ML {*AtpWrapper.problem_name := "BT__reflect_reflect_ident"*} |
102 lemma reflect_reflect_ident: "reflect (reflect t) = t" |
102 lemma reflect_reflect_ident: "reflect (reflect t) = t" |
103 apply (induct t) |
103 apply (induct t) |
104 apply (metis add_right_cancel reflect.simps(1)); |
104 apply (metis add_right_cancel reflect.simps(1)); |
105 apply (metis reflect.simps(2)) |
105 apply (metis reflect.simps(2)) |
106 done |
106 done |
107 |
107 |
108 ML {*AtpThread.problem_name := "BT__bt_map_ident"*} |
108 ML {*AtpWrapper.problem_name := "BT__bt_map_ident"*} |
109 lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" |
109 lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" |
110 apply (rule ext) |
110 apply (rule ext) |
111 apply (induct_tac y) |
111 apply (induct_tac y) |
112 apply (metis bt_map.simps(1)) |
112 apply (metis bt_map.simps(1)) |
113 txt{*BUG involving flex-flex pairs*} |
113 txt{*BUG involving flex-flex pairs*} |
114 (* apply (metis bt_map.simps(2)) *) |
114 (* apply (metis bt_map.simps(2)) *) |
115 apply auto |
115 apply auto |
116 done |
116 done |
117 |
117 |
118 |
118 |
119 ML {*AtpThread.problem_name := "BT__bt_map_appnd"*} |
119 ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*} |
120 lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)" |
120 lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)" |
121 apply (induct t) |
121 apply (induct t) |
122 apply (metis appnd.simps(1) bt_map.simps(1)) |
122 apply (metis appnd.simps(1) bt_map.simps(1)) |
123 apply (metis appnd.simps(2) bt_map.simps(2)) (*slow!!*) |
123 apply (metis appnd.simps(2) bt_map.simps(2)) (*slow!!*) |
124 done |
124 done |
125 |
125 |
126 |
126 |
127 ML {*AtpThread.problem_name := "BT__bt_map_compose"*} |
127 ML {*AtpWrapper.problem_name := "BT__bt_map_compose"*} |
128 lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" |
128 lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" |
129 apply (induct t) |
129 apply (induct t) |
130 apply (metis bt_map.simps(1)) |
130 apply (metis bt_map.simps(1)) |
131 txt{*Metis runs forever*} |
131 txt{*Metis runs forever*} |
132 (* apply (metis bt_map.simps(2) o_apply)*) |
132 (* apply (metis bt_map.simps(2) o_apply)*) |
133 apply auto |
133 apply auto |
134 done |
134 done |
135 |
135 |
136 |
136 |
137 ML {*AtpThread.problem_name := "BT__bt_map_reflect"*} |
137 ML {*AtpWrapper.problem_name := "BT__bt_map_reflect"*} |
138 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
138 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
139 apply (induct t) |
139 apply (induct t) |
140 apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1)) |
140 apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1)) |
141 apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2)) |
141 apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2)) |
142 done |
142 done |
143 |
143 |
144 ML {*AtpThread.problem_name := "BT__preorder_bt_map"*} |
144 ML {*AtpWrapper.problem_name := "BT__preorder_bt_map"*} |
145 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
145 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
146 apply (induct t) |
146 apply (induct t) |
147 apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) |
147 apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) |
148 apply simp |
148 apply simp |
149 done |
149 done |
150 |
150 |
151 ML {*AtpThread.problem_name := "BT__inorder_bt_map"*} |
151 ML {*AtpWrapper.problem_name := "BT__inorder_bt_map"*} |
152 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
152 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
153 apply (induct t) |
153 apply (induct t) |
154 apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1)) |
154 apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1)) |
155 apply simp |
155 apply simp |
156 done |
156 done |
157 |
157 |
158 ML {*AtpThread.problem_name := "BT__postorder_bt_map"*} |
158 ML {*AtpWrapper.problem_name := "BT__postorder_bt_map"*} |
159 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
159 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
160 apply (induct t) |
160 apply (induct t) |
161 apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1)) |
161 apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1)) |
162 apply simp |
162 apply simp |
163 done |
163 done |
164 |
164 |
165 ML {*AtpThread.problem_name := "BT__depth_bt_map"*} |
165 ML {*AtpWrapper.problem_name := "BT__depth_bt_map"*} |
166 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
166 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
167 apply (induct t) |
167 apply (induct t) |
168 apply (metis bt_map.simps(1) depth.simps(1)) |
168 apply (metis bt_map.simps(1) depth.simps(1)) |
169 apply simp |
169 apply simp |
170 done |
170 done |
171 |
171 |
172 ML {*AtpThread.problem_name := "BT__n_leaves_bt_map"*} |
172 ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*} |
173 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
173 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
174 apply (induct t) |
174 apply (induct t) |
175 apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1)) |
175 apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1)) |
176 apply (metis bt_map.simps(2) n_leaves.simps(2)) |
176 apply (metis bt_map.simps(2) n_leaves.simps(2)) |
177 done |
177 done |
178 |
178 |
179 |
179 |
180 ML {*AtpThread.problem_name := "BT__preorder_reflect"*} |
180 ML {*AtpWrapper.problem_name := "BT__preorder_reflect"*} |
181 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
181 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
182 apply (induct t) |
182 apply (induct t) |
183 apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv) |
183 apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv) |
184 apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident) |
184 apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident) |
185 done |
185 done |
186 |
186 |
187 ML {*AtpThread.problem_name := "BT__inorder_reflect"*} |
187 ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*} |
188 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
188 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
189 apply (induct t) |
189 apply (induct t) |
190 apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1)) |
190 apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1)) |
191 apply simp |
191 apply simp |
192 done |
192 done |
193 |
193 |
194 ML {*AtpThread.problem_name := "BT__postorder_reflect"*} |
194 ML {*AtpWrapper.problem_name := "BT__postorder_reflect"*} |
195 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
195 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
196 apply (induct t) |
196 apply (induct t) |
197 apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1)) |
197 apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1)) |
198 apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2) |
198 apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2) |
199 done |
199 done |
200 |
200 |
201 text {* |
201 text {* |
202 Analogues of the standard properties of the append function for lists. |
202 Analogues of the standard properties of the append function for lists. |
203 *} |
203 *} |
204 |
204 |
205 ML {*AtpThread.problem_name := "BT__appnd_assoc"*} |
205 ML {*AtpWrapper.problem_name := "BT__appnd_assoc"*} |
206 lemma appnd_assoc [simp]: |
206 lemma appnd_assoc [simp]: |
207 "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)" |
207 "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)" |
208 apply (induct t1) |
208 apply (induct t1) |
209 apply (metis appnd.simps(1)) |
209 apply (metis appnd.simps(1)) |
210 apply (metis appnd.simps(2)) |
210 apply (metis appnd.simps(2)) |
211 done |
211 done |
212 |
212 |
213 ML {*AtpThread.problem_name := "BT__appnd_Lf2"*} |
213 ML {*AtpWrapper.problem_name := "BT__appnd_Lf2"*} |
214 lemma appnd_Lf2 [simp]: "appnd t Lf = t" |
214 lemma appnd_Lf2 [simp]: "appnd t Lf = t" |
215 apply (induct t) |
215 apply (induct t) |
216 apply (metis appnd.simps(1)) |
216 apply (metis appnd.simps(1)) |
217 apply (metis appnd.simps(2)) |
217 apply (metis appnd.simps(2)) |
218 done |
218 done |
219 |
219 |
220 ML {*AtpThread.problem_name := "BT__depth_appnd"*} |
220 ML {*AtpWrapper.problem_name := "BT__depth_appnd"*} |
221 declare max_add_distrib_left [simp] |
221 declare max_add_distrib_left [simp] |
222 lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2" |
222 lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2" |
223 apply (induct t1) |
223 apply (induct t1) |
224 apply (metis add_0 appnd.simps(1) depth.simps(1)) |
224 apply (metis add_0 appnd.simps(1) depth.simps(1)) |
225 apply (simp add: ); |
225 apply (simp add: ); |
226 done |
226 done |
227 |
227 |
228 ML {*AtpThread.problem_name := "BT__n_leaves_appnd"*} |
228 ML {*AtpWrapper.problem_name := "BT__n_leaves_appnd"*} |
229 lemma n_leaves_appnd [simp]: |
229 lemma n_leaves_appnd [simp]: |
230 "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2" |
230 "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2" |
231 apply (induct t1) |
231 apply (induct t1) |
232 apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) |
232 apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) |
233 apply (simp add: left_distrib) |
233 apply (simp add: left_distrib) |
234 done |
234 done |
235 |
235 |
236 ML {*AtpThread.problem_name := "BT__bt_map_appnd"*} |
236 ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*} |
237 lemma (*bt_map_appnd:*) |
237 lemma (*bt_map_appnd:*) |
238 "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)" |
238 "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)" |
239 apply (induct t1) |
239 apply (induct t1) |
240 apply (metis appnd.simps(1) bt_map_appnd) |
240 apply (metis appnd.simps(1) bt_map_appnd) |
241 apply (metis bt_map_appnd) |
241 apply (metis bt_map_appnd) |