author | haftmann |
Tue, 13 Jul 2010 16:00:56 +0200 | |
changeset 37804 | 0145e59c1f6c |
parent 35439 | 888993948a1d |
child 39246 | 9e58f0499f57 |
permissions | -rw-r--r-- |
7018 | 1 |
(* Title: HOL/Induct/Tree.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
16078 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
7018 | 4 |
*) |
5 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
6 |
header {* Infinitely branching trees *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
7 |
|
31602 | 8 |
theory Tree |
9 |
imports Main |
|
10 |
begin |
|
7018 | 11 |
|
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
12 |
datatype 'a tree = |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
13 |
Atom 'a |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
14 |
| Branch "nat => 'a tree" |
7018 | 15 |
|
35419 | 16 |
primrec |
7018 | 17 |
map_tree :: "('a => 'b) => 'a tree => 'b tree" |
35419 | 18 |
where |
7018 | 19 |
"map_tree f (Atom a) = Atom (f a)" |
35419 | 20 |
| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
21 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
22 |
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" |
12171 | 23 |
by (induct t) simp_all |
7018 | 24 |
|
35419 | 25 |
primrec |
7018 | 26 |
exists_tree :: "('a => bool) => 'a tree => bool" |
35419 | 27 |
where |
7018 | 28 |
"exists_tree P (Atom a) = P a" |
35419 | 29 |
| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
30 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
31 |
lemma exists_map: |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
32 |
"(!!x. P x ==> Q (f x)) ==> |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
33 |
exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
12171 | 34 |
by (induct ts) auto |
7018 | 35 |
|
16078 | 36 |
|
37 |
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*} |
|
38 |
||
39 |
datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" |
|
40 |
||
41 |
text{*Addition of ordinals*} |
|
35419 | 42 |
primrec |
16078 | 43 |
add :: "[brouwer,brouwer] => brouwer" |
35419 | 44 |
where |
16078 | 45 |
"add i Zero = i" |
35419 | 46 |
| "add i (Succ j) = Succ (add i j)" |
47 |
| "add i (Lim f) = Lim (%n. add i (f n))" |
|
16078 | 48 |
|
49 |
lemma add_assoc: "add (add i j) k = add i (add j k)" |
|
18242 | 50 |
by (induct k) auto |
16078 | 51 |
|
52 |
text{*Multiplication of ordinals*} |
|
35419 | 53 |
primrec |
16078 | 54 |
mult :: "[brouwer,brouwer] => brouwer" |
35419 | 55 |
where |
16078 | 56 |
"mult i Zero = Zero" |
35419 | 57 |
| "mult i (Succ j) = add (mult i j) i" |
58 |
| "mult i (Lim f) = Lim (%n. mult i (f n))" |
|
16078 | 59 |
|
60 |
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" |
|
18242 | 61 |
by (induct k) (auto simp add: add_assoc) |
16078 | 62 |
|
63 |
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" |
|
18242 | 64 |
by (induct k) (auto simp add: add_mult_distrib) |
16078 | 65 |
|
66 |
text{*We could probably instantiate some axiomatic type classes and use |
|
67 |
the standard infix operators.*} |
|
68 |
||
16174 | 69 |
subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} |
70 |
||
35439 | 71 |
text{*To use the function package we need an ordering on the Brouwer |
16174 | 72 |
ordinals. Start with a predecessor relation and form its transitive |
73 |
closure. *} |
|
74 |
||
19736 | 75 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
76 |
brouwer_pred :: "(brouwer * brouwer) set" where |
19736 | 77 |
"brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})" |
16174 | 78 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
79 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
80 |
brouwer_order :: "(brouwer * brouwer) set" where |
19736 | 81 |
"brouwer_order = brouwer_pred^+" |
16174 | 82 |
|
83 |
lemma wf_brouwer_pred: "wf brouwer_pred" |
|
84 |
by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) |
|
85 |
||
35419 | 86 |
lemma wf_brouwer_order[simp]: "wf brouwer_order" |
16174 | 87 |
by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) |
88 |
||
89 |
lemma [simp]: "(j, Succ j) : brouwer_order" |
|
90 |
by(auto simp add: brouwer_order_def brouwer_pred_def) |
|
91 |
||
92 |
lemma [simp]: "(f n, Lim f) : brouwer_order" |
|
93 |
by(auto simp add: brouwer_order_def brouwer_pred_def) |
|
94 |
||
35419 | 95 |
text{*Example of a general function*} |
96 |
||
97 |
function |
|
16174 | 98 |
add2 :: "(brouwer*brouwer) => brouwer" |
35419 | 99 |
where |
16174 | 100 |
"add2 (i, Zero) = i" |
35419 | 101 |
| "add2 (i, (Succ j)) = Succ (add2 (i, j))" |
102 |
| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))" |
|
103 |
by pat_completeness auto |
|
104 |
termination by (relation "inv_image brouwer_order snd") auto |
|
16174 | 105 |
|
106 |
lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))" |
|
18242 | 107 |
by (induct k) auto |
16174 | 108 |
|
7018 | 109 |
end |