src/HOL/Induct/Tree.thy
author wenzelm
Tue, 13 Nov 2001 22:18:03 +0100
changeset 12171 dc87f33db447
parent 11649 dfb59b9954a6
child 14981 e73f8140af78
permissions -rw-r--r--
tuned inductions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Tree.thy
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer,  TU Muenchen
11649
wenzelm
parents: 11046
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     5
*)
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     6
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     7
header {* Infinitely branching trees *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     8
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     9
theory Tree = Main:
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    10
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    11
datatype 'a tree =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    12
    Atom 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    13
  | Branch "nat => 'a tree"
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    14
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    15
consts
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    16
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    17
primrec
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    18
  "map_tree f (Atom a) = Atom (f a)"
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    19
  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    20
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    21
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    22
  by (induct t) simp_all
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    23
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    24
consts
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    25
  exists_tree :: "('a => bool) => 'a tree => bool"
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    26
primrec
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    27
  "exists_tree P (Atom a) = P a"
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    28
  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    29
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    30
lemma exists_map:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    31
  "(!!x. P x ==> Q (f x)) ==>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    32
    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    33
  by (induct ts) auto
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    34
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    35
end