berghofe@7018: (* Title: HOL/Induct/Tree.thy 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: haftmann@31602: theory Tree haftmann@31602: imports Main haftmann@31602: begin 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 (\x. map_tree f (ts x))" wenzelm@11046: wenzelm@11046: lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \ 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) = (\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)" wenzelm@18242: 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)" wenzelm@18242: by (induct k) (auto simp add: add_assoc) paulson@16078: paulson@16078: lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" wenzelm@18242: by (induct k) (auto simp add: add_mult_distrib) paulson@16078: paulson@16078: text{*We could probably instantiate some axiomatic type classes and use paulson@16078: the standard infix operators.*} paulson@16078: paulson@16174: subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} paulson@16174: paulson@16174: text{*To define recdef style functions we need an ordering on the Brouwer paulson@16174: ordinals. Start with a predecessor relation and form its transitive paulson@16174: closure. *} paulson@16174: wenzelm@19736: definition wenzelm@21404: brouwer_pred :: "(brouwer * brouwer) set" where wenzelm@19736: "brouwer_pred = (\i. {(m,n). n = Succ m \ (EX f. n = Lim f & m = f i)})" paulson@16174: wenzelm@21404: definition wenzelm@21404: brouwer_order :: "(brouwer * brouwer) set" where wenzelm@19736: "brouwer_order = brouwer_pred^+" paulson@16174: paulson@16174: lemma wf_brouwer_pred: "wf brouwer_pred" paulson@16174: by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) paulson@16174: paulson@16174: lemma wf_brouwer_order: "wf brouwer_order" paulson@16174: by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) paulson@16174: paulson@16174: lemma [simp]: "(j, Succ j) : brouwer_order" paulson@16174: by(auto simp add: brouwer_order_def brouwer_pred_def) paulson@16174: paulson@16174: lemma [simp]: "(f n, Lim f) : brouwer_order" paulson@16174: by(auto simp add: brouwer_order_def brouwer_pred_def) paulson@16174: paulson@16174: text{*Example of a recdef*} paulson@16174: consts paulson@16174: add2 :: "(brouwer*brouwer) => brouwer" paulson@16174: recdef add2 "inv_image brouwer_order (\ (x,y). y)" paulson@16174: "add2 (i, Zero) = i" paulson@16174: "add2 (i, (Succ j)) = Succ (add2 (i, j))" paulson@16174: "add2 (i, (Lim f)) = Lim (\ n. add2 (i, (f n)))" paulson@16174: (hints recdef_wf: wf_brouwer_order) paulson@16174: paulson@16174: lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))" wenzelm@18242: by (induct k) auto paulson@16174: berghofe@7018: end