berghofe@7018: (*  Title:      HOL/Induct/Tree.thy
berghofe@7018:     ID:         $Id$
berghofe@7018:     Author:     Stefan Berghofer,  TU Muenchen
paulson@16078:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
berghofe@7018: *)
berghofe@7018: 
wenzelm@11046: header {* Infinitely branching trees *}
wenzelm@11046: 
wenzelm@11046: theory Tree = Main:
berghofe@7018: 
wenzelm@11046: datatype 'a tree =
wenzelm@11046:     Atom 'a
wenzelm@11046:   | Branch "nat => 'a tree"
berghofe@7018: 
berghofe@7018: consts
berghofe@7018:   map_tree :: "('a => 'b) => 'a tree => 'b tree"
berghofe@7018: primrec
berghofe@7018:   "map_tree f (Atom a) = Atom (f a)"
wenzelm@11046:   "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
wenzelm@11046: 
wenzelm@11046: lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
wenzelm@12171:   by (induct t) simp_all
berghofe@7018: 
berghofe@7018: consts
berghofe@7018:   exists_tree :: "('a => bool) => 'a tree => bool"
berghofe@7018: primrec
berghofe@7018:   "exists_tree P (Atom a) = P a"
wenzelm@11046:   "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
wenzelm@11046: 
wenzelm@11046: lemma exists_map:
wenzelm@11046:   "(!!x. P x ==> Q (f x)) ==>
wenzelm@11046:     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
wenzelm@12171:   by (induct ts) auto
berghofe@7018: 
paulson@16078: 
paulson@16078: subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
paulson@16078: 
paulson@16078: datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
paulson@16078: 
paulson@16078: text{*Addition of ordinals*}
paulson@16078: consts
paulson@16078:   add :: "[brouwer,brouwer] => brouwer"
paulson@16078: primrec
paulson@16078:   "add i Zero = i"
paulson@16078:   "add i (Succ j) = Succ (add i j)"
paulson@16078:   "add i (Lim f) = Lim (%n. add i (f n))"
paulson@16078: 
paulson@16078: lemma add_assoc: "add (add i j) k = add i (add j k)"
paulson@16078: by (induct k, auto)
paulson@16078: 
paulson@16078: text{*Multiplication of ordinals*}
paulson@16078: consts
paulson@16078:   mult :: "[brouwer,brouwer] => brouwer"
paulson@16078: primrec
paulson@16078:   "mult i Zero = Zero"
paulson@16078:   "mult i (Succ j) = add (mult i j) i"
paulson@16078:   "mult i (Lim f) = Lim (%n. mult i (f n))"
paulson@16078: 
paulson@16078: lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
paulson@16078: apply (induct k) 
paulson@16078: apply (auto simp add: add_assoc) 
paulson@16078: done
paulson@16078: 
paulson@16078: lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
paulson@16078: apply (induct k) 
paulson@16078: apply (auto simp add: add_mult_distrib) 
paulson@16078: done
paulson@16078: 
paulson@16078: text{*We could probably instantiate some axiomatic type classes and use
paulson@16078: the standard infix operators.*}
paulson@16078: 
berghofe@7018: end