equal
deleted
inserted
replaced
1 (* Title: HOL/Induct/Tree.thy |
1 (* Title: HOL/Induct/Tree.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer, TU Muenchen |
3 Author: Stefan Berghofer, TU Muenchen |
|
4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
5 *) |
5 |
6 |
6 header {* Infinitely branching trees *} |
7 header {* Infinitely branching trees *} |
7 |
8 |
8 theory Tree = Main: |
9 theory Tree = Main: |
29 lemma exists_map: |
30 lemma exists_map: |
30 "(!!x. P x ==> Q (f x)) ==> |
31 "(!!x. P x ==> Q (f x)) ==> |
31 exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
32 exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
32 by (induct ts) auto |
33 by (induct ts) auto |
33 |
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 |
34 end |
72 end |