|
7018
|
1 |
(* Title: HOL/Induct/Tree.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
|
4 |
Copyright 1999 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Infinitely branching trees
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
|
|
|
10 |
by (induct_tac "t" 1);
|
|
|
11 |
by (ALLGOALS Asm_simp_tac);
|
|
|
12 |
qed "tree_map_compose";
|
|
|
13 |
|
|
|
14 |
val prems = Goal "(!!x. P x ==> Q (f x)) ==> \
|
|
|
15 |
\ exists_tree P ts --> exists_tree Q (map_tree f ts)";
|
|
|
16 |
by (induct_tac "ts" 1);
|
|
|
17 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
|
|
|
18 |
by (Fast_tac 1);
|
|
|
19 |
qed "exists_map";
|
|
|
20 |
|