src/HOL/Induct/Tree.thy
author berghofe
Fri Jul 16 14:03:03 1999 +0200 (1999-07-16)
changeset 7018 ae18bb3075c3
child 11046 b5f5942781a0
permissions -rw-r--r--
Infinitely branching trees.
berghofe@7018
     1
(*  Title:      HOL/Induct/Tree.thy
berghofe@7018
     2
    ID:         $Id$
berghofe@7018
     3
    Author:     Stefan Berghofer,  TU Muenchen
berghofe@7018
     4
    Copyright   1999  TU Muenchen
berghofe@7018
     5
berghofe@7018
     6
Infinitely branching trees
berghofe@7018
     7
*)
berghofe@7018
     8
berghofe@7018
     9
Tree = Main +
berghofe@7018
    10
berghofe@7018
    11
datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
berghofe@7018
    12
berghofe@7018
    13
consts
berghofe@7018
    14
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
berghofe@7018
    15
berghofe@7018
    16
primrec
berghofe@7018
    17
  "map_tree f (Atom a) = Atom (f a)"
berghofe@7018
    18
  "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
berghofe@7018
    19
berghofe@7018
    20
consts
berghofe@7018
    21
  exists_tree :: "('a => bool) => 'a tree => bool"
berghofe@7018
    22
berghofe@7018
    23
primrec
berghofe@7018
    24
  "exists_tree P (Atom a) = P a"
berghofe@7018
    25
  "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
berghofe@7018
    26
berghofe@7018
    27
end