src/HOL/Induct/Tree.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Tree.thy	Fri Jul 16 14:03:03 1999 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/Induct/Tree.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer,  TU Muenchen
+    Copyright   1999  TU Muenchen
+
+Infinitely branching trees
+*)
+
+Tree = Main +
+
+datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
+
+consts
+  map_tree :: "('a => 'b) => 'a tree => 'b tree"
+
+primrec
+  "map_tree f (Atom a) = Atom (f a)"
+  "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
+
+consts
+  exists_tree :: "('a => bool) => 'a tree => bool"
+
+primrec
+  "exists_tree P (Atom a) = P a"
+  "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
+
+end