equal
deleted
inserted
replaced
|
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 |