author | wenzelm |
Tue, 13 Nov 2001 22:18:03 +0100 | |
changeset 12171 | dc87f33db447 |
parent 11649 | dfb59b9954a6 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
7018 | 1 |
(* Title: HOL/Induct/Tree.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
11649 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
7018 | 5 |
*) |
6 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
7 |
header {* Infinitely branching trees *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
8 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
9 |
theory Tree = Main: |
7018 | 10 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
11 |
datatype 'a tree = |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
12 |
Atom 'a |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
13 |
| Branch "nat => 'a tree" |
7018 | 14 |
|
15 |
consts |
|
16 |
map_tree :: "('a => 'b) => 'a tree => 'b tree" |
|
17 |
primrec |
|
18 |
"map_tree f (Atom a) = Atom (f a)" |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
19 |
"map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
20 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
21 |
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" |
12171 | 22 |
by (induct t) simp_all |
7018 | 23 |
|
24 |
consts |
|
25 |
exists_tree :: "('a => bool) => 'a tree => bool" |
|
26 |
primrec |
|
27 |
"exists_tree P (Atom a) = P a" |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
28 |
"exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
29 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
30 |
lemma exists_map: |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
31 |
"(!!x. P x ==> Q (f x)) ==> |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
32 |
exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
12171 | 33 |
by (induct ts) auto |
7018 | 34 |
|
35 |
end |