src/HOL/Induct/Tree.thy
changeset 11046 b5f5942781a0
parent 7018 ae18bb3075c3
child 11649 dfb59b9954a6
     1.1 --- a/src/HOL/Induct/Tree.thy	Sat Feb 03 15:22:57 2001 +0100
     1.2 +++ b/src/HOL/Induct/Tree.thy	Sat Feb 03 17:40:16 2001 +0100
     1.3 @@ -2,26 +2,39 @@
     1.4      ID:         $Id$
     1.5      Author:     Stefan Berghofer,  TU Muenchen
     1.6      Copyright   1999  TU Muenchen
     1.7 -
     1.8 -Infinitely branching trees
     1.9  *)
    1.10  
    1.11 -Tree = Main +
    1.12 +header {* Infinitely branching trees *}
    1.13 +
    1.14 +theory Tree = Main:
    1.15  
    1.16 -datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
    1.17 +datatype 'a tree =
    1.18 +    Atom 'a
    1.19 +  | Branch "nat => 'a tree"
    1.20  
    1.21  consts
    1.22    map_tree :: "('a => 'b) => 'a tree => 'b tree"
    1.23 -
    1.24  primrec
    1.25    "map_tree f (Atom a) = Atom (f a)"
    1.26 -  "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
    1.27 +  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
    1.28 +
    1.29 +lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
    1.30 +  apply (induct t)
    1.31 +   apply simp_all
    1.32 +  done
    1.33  
    1.34  consts
    1.35    exists_tree :: "('a => bool) => 'a tree => bool"
    1.36 -
    1.37  primrec
    1.38    "exists_tree P (Atom a) = P a"
    1.39 -  "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
    1.40 +  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
    1.41 +
    1.42 +lemma exists_map:
    1.43 +  "(!!x. P x ==> Q (f x)) ==>
    1.44 +    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
    1.45 +  apply (induct ts)
    1.46 +   apply simp_all
    1.47 +  apply blast
    1.48 +  done
    1.49  
    1.50  end