src/HOL/Induct/Tree.thy
author paulson
Wed May 25 16:14:40 2005 +0200 (2005-05-25)
changeset 16078 e1364521a250
parent 14981 e73f8140af78
child 16174 a55c796b1f79
permissions -rw-r--r--
new Brouwer ordinal example
     1 (*  Title:      HOL/Induct/Tree.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer,  TU Muenchen
     4     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5 *)
     6 
     7 header {* Infinitely branching trees *}
     8 
     9 theory Tree = Main:
    10 
    11 datatype 'a tree =
    12     Atom 'a
    13   | Branch "nat => 'a tree"
    14 
    15 consts
    16   map_tree :: "('a => 'b) => 'a tree => 'b tree"
    17 primrec
    18   "map_tree f (Atom a) = Atom (f a)"
    19   "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
    20 
    21 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
    22   by (induct t) simp_all
    23 
    24 consts
    25   exists_tree :: "('a => bool) => 'a tree => bool"
    26 primrec
    27   "exists_tree P (Atom a) = P a"
    28   "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
    29 
    30 lemma exists_map:
    31   "(!!x. P x ==> Q (f x)) ==>
    32     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
    33   by (induct ts) auto
    34 
    35 
    36 subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
    37 
    38 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
    39 
    40 text{*Addition of ordinals*}
    41 consts
    42   add :: "[brouwer,brouwer] => brouwer"
    43 primrec
    44   "add i Zero = i"
    45   "add i (Succ j) = Succ (add i j)"
    46   "add i (Lim f) = Lim (%n. add i (f n))"
    47 
    48 lemma add_assoc: "add (add i j) k = add i (add j k)"
    49 by (induct k, auto)
    50 
    51 text{*Multiplication of ordinals*}
    52 consts
    53   mult :: "[brouwer,brouwer] => brouwer"
    54 primrec
    55   "mult i Zero = Zero"
    56   "mult i (Succ j) = add (mult i j) i"
    57   "mult i (Lim f) = Lim (%n. mult i (f n))"
    58 
    59 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    60 apply (induct k) 
    61 apply (auto simp add: add_assoc) 
    62 done
    63 
    64 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    65 apply (induct k) 
    66 apply (auto simp add: add_mult_distrib) 
    67 done
    68 
    69 text{*We could probably instantiate some axiomatic type classes and use
    70 the standard infix operators.*}
    71 
    72 end