156 (** preorder **) |
156 (** preorder **) |
157 |
157 |
158 bind_thm ("preorder", (preorder_def RS def_term_rec)); |
158 bind_thm ("preorder", (preorder_def RS def_term_rec)); |
159 |
159 |
160 Goalw [preorder_def] |
160 Goalw [preorder_def] |
161 "!!t A. t: term(A) ==> preorder(t) : list(A)"; |
161 "t: term(A) ==> preorder(t) : list(A)"; |
162 by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1)); |
162 by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1)); |
163 qed "preorder_type"; |
163 qed "preorder_type"; |
164 |
164 |
165 |
165 |
166 (** Term simplification **) |
166 (** Term simplification **) |
180 Goal "t: term(A) ==> term_map(%u. u, t) = t"; |
180 Goal "t: term(A) ==> term_map(%u. u, t) = t"; |
181 by (etac term_induct_eqn 1); |
181 by (etac term_induct_eqn 1); |
182 by (asm_simp_tac (simpset() addsimps [map_ident]) 1); |
182 by (asm_simp_tac (simpset() addsimps [map_ident]) 1); |
183 qed "term_map_ident"; |
183 qed "term_map_ident"; |
184 |
184 |
185 Goal |
185 Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; |
186 "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; |
|
187 by (etac term_induct_eqn 1); |
186 by (etac term_induct_eqn 1); |
188 by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
187 by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
189 qed "term_map_compose"; |
188 qed "term_map_compose"; |
190 |
189 |
191 Goal |
190 Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
192 "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
|
193 by (etac term_induct_eqn 1); |
191 by (etac term_induct_eqn 1); |
194 by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1); |
192 by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1); |
195 qed "term_map_reflect"; |
193 qed "term_map_reflect"; |
196 |
194 |
197 |
195 |
198 (** theorems about term_size **) |
196 (** theorems about term_size **) |
199 |
197 |
200 Goal |
198 Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
201 "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
|
202 by (etac term_induct_eqn 1); |
199 by (etac term_induct_eqn 1); |
203 by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
200 by (asm_simp_tac (simpset() addsimps [map_compose]) 1); |
204 qed "term_size_term_map"; |
201 qed "term_size_term_map"; |
205 |
202 |
206 Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)"; |
203 Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)"; |
224 qed "reflect_reflect_ident"; |
221 qed "reflect_reflect_ident"; |
225 |
222 |
226 |
223 |
227 (** theorems about preorder **) |
224 (** theorems about preorder **) |
228 |
225 |
229 Goal |
226 Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
230 "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
|
231 by (etac term_induct_eqn 1); |
227 by (etac term_induct_eqn 1); |
232 by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1); |
228 by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1); |
233 qed "preorder_term_map"; |
229 qed "preorder_term_map"; |
234 |
230 |
235 (** preorder(reflect(t)) = rev(postorder(t)) **) |
231 (** preorder(reflect(t)) = rev(postorder(t)) **) |