author | wenzelm |
Sat, 03 Feb 2001 17:40:16 +0100 | |
changeset 11046 | b5f5942781a0 |
parent 7018 | ae18bb3075c3 |
child 11649 | dfb59b9954a6 |
permissions | -rw-r--r-- |
7018 | 1 |
(* Title: HOL/Induct/Tree.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
Copyright 1999 TU Muenchen |
|
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" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
22 |
apply (induct t) |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
23 |
apply simp_all |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
24 |
done |
7018 | 25 |
|
26 |
consts |
|
27 |
exists_tree :: "('a => bool) => 'a tree => bool" |
|
28 |
primrec |
|
29 |
"exists_tree P (Atom a) = P a" |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
30 |
"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
|
31 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
32 |
lemma exists_map: |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
33 |
"(!!x. P x ==> Q (f x)) ==> |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
34 |
exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
35 |
apply (induct ts) |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
36 |
apply simp_all |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
37 |
apply blast |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
38 |
done |
7018 | 39 |
|
40 |
end |