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
```