src/HOL/Induct/Tree.thy
 changeset 11046 b5f5942781a0 parent 7018 ae18bb3075c3 child 11649 dfb59b9954a6
equal inserted replaced
11045:971a50fda146 11046:b5f5942781a0
1 (*  Title:      HOL/Induct/Tree.thy
1 (*  Title:      HOL/Induct/Tree.thy
2     ID:         \$Id\$
2     ID:         \$Id\$
3     Author:     Stefan Berghofer,  TU Muenchen
3     Author:     Stefan Berghofer,  TU Muenchen
7 *)
5 *)
8
6
9 Tree = Main +
7 header {* Infinitely branching trees *}
10
8
11 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
9 theory Tree = Main:

10

11 datatype 'a tree =

12     Atom 'a

13   | Branch "nat => 'a tree"
12
14
13 consts
15 consts
14   map_tree :: "('a => 'b) => 'a tree => 'b tree"
16   map_tree :: "('a => 'b) => 'a tree => 'b tree"
16 primrec
17 primrec
17   "map_tree f (Atom a) = Atom (f a)"
18   "map_tree f (Atom a) = Atom (f a)"
18   "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
19   "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"

20

21 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"

22   apply (induct t)

23    apply simp_all

24   done
19
25
20 consts
26 consts
21   exists_tree :: "('a => bool) => 'a tree => bool"
27   exists_tree :: "('a => bool) => 'a tree => bool"
23 primrec
28 primrec
24   "exists_tree P (Atom a) = P a"
29   "exists_tree P (Atom a) = P a"
25   "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
30   "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"

31

32 lemma exists_map:

33   "(!!x. P x ==> Q (f x)) ==>

34     exists_tree P ts ==> exists_tree Q (map_tree f ts)"

35   apply (induct ts)

36    apply simp_all

37   apply blast

38   done
26
39
27 end
40 end