src/HOL/Induct/Tree.thy

 (*  Title:      HOL/Induct/Tree.thy
     ID:         $Id$
     Author:     Stefan Berghofer,  TU Muenchen
     Copyright   1999  TU Muenchen
-
-Infinitely branching trees
 *)
 
-Tree = Main +
+header {* Infinitely branching trees *}
 
-datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
+theory 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))"
+  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+  apply (induct t)
+   apply simp_all
+  done
 
 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))"
+  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+
+lemma exists_map:
+  "(!!x. P x ==> Q (f x)) ==>
+    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
+  apply (induct ts)
+   apply simp_all
+  apply blast
+  done
 
 end