src/HOL/Induct/Tree.thy
 author kleing Mon Jun 21 10:25:57 2004 +0200 (2004-06-21) changeset 14981 e73f8140af78 parent 12171 dc87f33db447 child 16078 e1364521a250 permissions -rw-r--r--
Merged in license change from Isabelle2004
```     1 (*  Title:      HOL/Induct/Tree.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Stefan Berghofer,  TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Infinitely branching trees *}
```
```     7
```
```     8 theory Tree = Main:
```
```     9
```
```    10 datatype 'a tree =
```
```    11     Atom 'a
```
```    12   | Branch "nat => 'a tree"
```
```    13
```
```    14 consts
```
```    15   map_tree :: "('a => 'b) => 'a tree => 'b tree"
```
```    16 primrec
```
```    17   "map_tree f (Atom a) = Atom (f a)"
```
```    18   "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
```
```    19
```
```    20 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
```
```    21   by (induct t) simp_all
```
```    22
```
```    23 consts
```
```    24   exists_tree :: "('a => bool) => 'a tree => bool"
```
```    25 primrec
```
```    26   "exists_tree P (Atom a) = P a"
```
```    27   "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
```
```    28
```
```    29 lemma exists_map:
```
```    30   "(!!x. P x ==> Q (f x)) ==>
```
```    31     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
```
```    32   by (induct ts) auto
```
```    33
```
```    34 end
```