src/HOL/Induct/Tree.thy
author wenzelm
Sat Feb 03 17:40:16 2001 +0100 (2001-02-03)
changeset 11046 b5f5942781a0
parent 7018 ae18bb3075c3
child 11649 dfb59b9954a6
permissions -rw-r--r--
Induct: converted some theories to new-style format;
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
wenzelm@11046
     7
header {* Infinitely branching trees *}
wenzelm@11046
     8
wenzelm@11046
     9
theory Tree = Main:
berghofe@7018
    10
wenzelm@11046
    11
datatype 'a tree =
wenzelm@11046
    12
    Atom 'a
wenzelm@11046
    13
  | Branch "nat => 'a tree"
berghofe@7018
    14
berghofe@7018
    15
consts
berghofe@7018
    16
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
berghofe@7018
    17
primrec
berghofe@7018
    18
  "map_tree f (Atom a) = Atom (f a)"
wenzelm@11046
    19
  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
wenzelm@11046
    20
wenzelm@11046
    21
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
wenzelm@11046
    22
  apply (induct t)
wenzelm@11046
    23
   apply simp_all
wenzelm@11046
    24
  done
berghofe@7018
    25
berghofe@7018
    26
consts
berghofe@7018
    27
  exists_tree :: "('a => bool) => 'a tree => bool"
berghofe@7018
    28
primrec
berghofe@7018
    29
  "exists_tree P (Atom a) = P a"
wenzelm@11046
    30
  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
wenzelm@11046
    31
wenzelm@11046
    32
lemma exists_map:
wenzelm@11046
    33
  "(!!x. P x ==> Q (f x)) ==>
wenzelm@11046
    34
    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
wenzelm@11046
    35
  apply (induct ts)
wenzelm@11046
    36
   apply simp_all
wenzelm@11046
    37
  apply blast
wenzelm@11046
    38
  done
berghofe@7018
    39
berghofe@7018
    40
end