author | wenzelm |
Sat, 20 Jun 2015 16:23:56 +0200 | |
changeset 60532 | 7fb5b7dc8332 |
parent 60530 | 44f9873d6f6f |
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 |
||
60530 | 6 |
section \<open>Infinitely branching trees\<close> |
11046
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 |
|
58310 | 12 |
datatype 'a tree = |
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
13 |
Atom 'a |
60532 | 14 |
| Branch "nat \<Rightarrow> 'a tree" |
7018 | 15 |
|
60532 | 16 |
primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree" |
35419 | 17 |
where |
7018 | 18 |
"map_tree f (Atom a) = Atom (f a)" |
35419 | 19 |
| "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
|
20 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
21 |
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" |
12171 | 22 |
by (induct t) simp_all |
7018 | 23 |
|
60532 | 24 |
primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" |
35419 | 25 |
where |
7018 | 26 |
"exists_tree P (Atom a) = P a" |
35419 | 27 |
| "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
|
28 |
|
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
7018
diff
changeset
|
29 |
lemma exists_map: |
60532 | 30 |
"(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow> |
31 |
exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)" |
|
12171 | 32 |
by (induct ts) auto |
7018 | 33 |
|
16078 | 34 |
|
60530 | 35 |
subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close> |
16078 | 36 |
|
60532 | 37 |
datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer" |
16078 | 38 |
|
60532 | 39 |
text \<open>Addition of ordinals\<close> |
40 |
primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
|
35419 | 41 |
where |
16078 | 42 |
"add i Zero = i" |
35419 | 43 |
| "add i (Succ j) = Succ (add i j)" |
60532 | 44 |
| "add i (Lim f) = Lim (\<lambda>n. add i (f n))" |
16078 | 45 |
|
46 |
lemma add_assoc: "add (add i j) k = add i (add j k)" |
|
18242 | 47 |
by (induct k) auto |
16078 | 48 |
|
60532 | 49 |
text \<open>Multiplication of ordinals\<close> |
50 |
primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
|
35419 | 51 |
where |
16078 | 52 |
"mult i Zero = Zero" |
35419 | 53 |
| "mult i (Succ j) = add (mult i j) i" |
60532 | 54 |
| "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))" |
16078 | 55 |
|
56 |
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" |
|
18242 | 57 |
by (induct k) (auto simp add: add_assoc) |
16078 | 58 |
|
59 |
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" |
|
18242 | 60 |
by (induct k) (auto simp add: add_mult_distrib) |
16078 | 61 |
|
60532 | 62 |
text \<open>We could probably instantiate some axiomatic type classes and use |
63 |
the standard infix operators.\<close> |
|
16078 | 64 |
|
60532 | 65 |
|
66 |
subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close> |
|
16174 | 67 |
|
60532 | 68 |
text \<open>To use the function package we need an ordering on the Brouwer |
69 |
ordinals. Start with a predecessor relation and form its transitive |
|
70 |
closure.\<close> |
|
16174 | 71 |
|
60532 | 72 |
definition brouwer_pred :: "(brouwer \<times> brouwer) set" |
73 |
where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})" |
|
16174 | 74 |
|
60532 | 75 |
definition brouwer_order :: "(brouwer \<times> brouwer) set" |
46914 | 76 |
where "brouwer_order = brouwer_pred^+" |
16174 | 77 |
|
78 |
lemma wf_brouwer_pred: "wf brouwer_pred" |
|
60532 | 79 |
unfolding wf_def brouwer_pred_def |
80 |
apply clarify |
|
81 |
apply (induct_tac x) |
|
82 |
apply blast+ |
|
83 |
done |
|
16174 | 84 |
|
35419 | 85 |
lemma wf_brouwer_order[simp]: "wf brouwer_order" |
60532 | 86 |
unfolding brouwer_order_def |
87 |
by (rule wf_trancl[OF wf_brouwer_pred]) |
|
16174 | 88 |
|
60532 | 89 |
lemma [simp]: "(j, Succ j) \<in> brouwer_order" |
90 |
by (auto simp add: brouwer_order_def brouwer_pred_def) |
|
16174 | 91 |
|
60532 | 92 |
lemma [simp]: "(f n, Lim f) \<in> brouwer_order" |
93 |
by (auto simp add: brouwer_order_def brouwer_pred_def) |
|
35419 | 94 |
|
60532 | 95 |
text \<open>Example of a general function\<close> |
46914 | 96 |
function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
35419 | 97 |
where |
39246 | 98 |
"add2 i Zero = i" |
99 |
| "add2 i (Succ j) = Succ (add2 i j)" |
|
100 |
| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))" |
|
35419 | 101 |
by pat_completeness auto |
102 |
termination by (relation "inv_image brouwer_order snd") auto |
|
16174 | 103 |
|
39246 | 104 |
lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)" |
18242 | 105 |
by (induct k) auto |
16174 | 106 |
|
7018 | 107 |
end |