src/HOL/Induct/Tree.thy
 author paulson Wed, 25 May 2005 16:14:40 +0200 changeset 16078 e1364521a250 parent 14981 e73f8140af78 child 16174 a55c796b1f79 permissions -rw-r--r--
new Brouwer ordinal example
```
(*  Title:      HOL/Induct/Tree.thy
ID:         \$Id\$
Author:     Stefan Berghofer,  TU Muenchen
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

header {* Infinitely branching trees *}

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 (\<lambda>x. map_tree f (ts x))"

lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
by (induct t) simp_all

consts
exists_tree :: "('a => bool) => 'a tree => bool"
primrec
"exists_tree P (Atom a) = P a"
"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)"
by (induct ts) auto

subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}

datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"

consts
primrec

by (induct k, auto)

text{*Multiplication of ordinals*}
consts
mult :: "[brouwer,brouwer] => brouwer"
primrec
"mult i Zero = Zero"
"mult i (Succ j) = add (mult i j) i"
"mult i (Lim f) = Lim (%n. mult i (f n))"

apply (induct k)