Infinitely branching trees.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Tree.ML	Fri Jul 16 14:03:03 1999 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Induct/Tree.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer,  TU Muenchen
+    Copyright   1999  TU Muenchen
+
+Infinitely branching trees
+*)
+
+Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
+by (induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "tree_map_compose";
+
+val prems = Goal "(!!x. P x ==> Q (f x)) ==>  \
+   \    exists_tree P ts --> exists_tree Q (map_tree f ts)";
+by (induct_tac "ts" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+by (Fast_tac 1);
+qed "exists_map";
+

--- /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