src/HOL/Induct/Tree.thy
author wenzelm
Sat Feb 03 17:40:16 2001 +0100 (2001-02-03)
changeset 11046 b5f5942781a0
parent 7018 ae18bb3075c3
child 11649 dfb59b9954a6
permissions -rw-r--r--
Induct: converted some theories to new-style format;
     1 (*  Title:      HOL/Induct/Tree.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer,  TU Muenchen
     4     Copyright   1999  TU Muenchen
     5 *)
     6 
     7 header {* Infinitely branching trees *}
     8 
     9 theory Tree = Main:
    10 
    11 datatype 'a tree =
    12     Atom 'a
    13   | Branch "nat => 'a tree"
    14 
    15 consts
    16   map_tree :: "('a => 'b) => 'a tree => 'b tree"
    17 primrec
    18   "map_tree f (Atom a) = Atom (f a)"
    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
    25 
    26 consts
    27   exists_tree :: "('a => bool) => 'a tree => bool"
    28 primrec
    29   "exists_tree P (Atom a) = P a"
    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
    39 
    40 end