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