src/HOL/Induct/Tree.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12171 dc87f33db447
child 16078 e1364521a250
permissions -rw-r--r--
Merged in license change from Isabelle2004
berghofe@7018
     1
(*  Title:      HOL/Induct/Tree.thy
berghofe@7018
     2
    ID:         $Id$
berghofe@7018
     3
    Author:     Stefan Berghofer,  TU Muenchen
berghofe@7018
     4
*)
berghofe@7018
     5
wenzelm@11046
     6
header {* Infinitely branching trees *}
wenzelm@11046
     7
wenzelm@11046
     8
theory Tree = Main:
berghofe@7018
     9
wenzelm@11046
    10
datatype 'a tree =
wenzelm@11046
    11
    Atom 'a
wenzelm@11046
    12
  | Branch "nat => 'a tree"
berghofe@7018
    13
berghofe@7018
    14
consts
berghofe@7018
    15
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
berghofe@7018
    16
primrec
berghofe@7018
    17
  "map_tree f (Atom a) = Atom (f a)"
wenzelm@11046
    18
  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
wenzelm@11046
    19
wenzelm@11046
    20
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
wenzelm@12171
    21
  by (induct t) simp_all
berghofe@7018
    22
berghofe@7018
    23
consts
berghofe@7018
    24
  exists_tree :: "('a => bool) => 'a tree => bool"
berghofe@7018
    25
primrec
berghofe@7018
    26
  "exists_tree P (Atom a) = P a"
wenzelm@11046
    27
  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
wenzelm@11046
    28
wenzelm@11046
    29
lemma exists_map:
wenzelm@11046
    30
  "(!!x. P x ==> Q (f x)) ==>
wenzelm@11046
    31
    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
wenzelm@12171
    32
  by (induct ts) auto
berghofe@7018
    33
berghofe@7018
    34
end