9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 datatype 'a tree = |
12 datatype 'a tree = |
13 Atom 'a |
13 Atom 'a |
14 | Branch "nat => 'a tree" |
14 | Branch "nat \<Rightarrow> 'a tree" |
15 |
15 |
16 primrec map_tree :: "('a => 'b) => 'a tree => 'b tree" |
16 primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree" |
17 where |
17 where |
18 "map_tree f (Atom a) = Atom (f a)" |
18 "map_tree f (Atom a) = Atom (f a)" |
19 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" |
19 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" |
20 |
20 |
21 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" |
21 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" |
22 by (induct t) simp_all |
22 by (induct t) simp_all |
23 |
23 |
24 primrec exists_tree :: "('a => bool) => 'a tree => bool" |
24 primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" |
25 where |
25 where |
26 "exists_tree P (Atom a) = P a" |
26 "exists_tree P (Atom a) = P a" |
27 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" |
27 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" |
28 |
28 |
29 lemma exists_map: |
29 lemma exists_map: |
30 "(!!x. P x ==> Q (f x)) ==> |
30 "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow> |
31 exists_tree P ts ==> exists_tree Q (map_tree f ts)" |
31 exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)" |
32 by (induct ts) auto |
32 by (induct ts) auto |
33 |
33 |
34 |
34 |
35 subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close> |
35 subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close> |
36 |
36 |
37 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" |
37 datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer" |
38 |
38 |
39 text\<open>Addition of ordinals\<close> |
39 text \<open>Addition of ordinals\<close> |
40 primrec add :: "[brouwer,brouwer] => brouwer" |
40 primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
41 where |
41 where |
42 "add i Zero = i" |
42 "add i Zero = i" |
43 | "add i (Succ j) = Succ (add i j)" |
43 | "add i (Succ j) = Succ (add i j)" |
44 | "add i (Lim f) = Lim (%n. add i (f n))" |
44 | "add i (Lim f) = Lim (\<lambda>n. add i (f n))" |
45 |
45 |
46 lemma add_assoc: "add (add i j) k = add i (add j k)" |
46 lemma add_assoc: "add (add i j) k = add i (add j k)" |
47 by (induct k) auto |
47 by (induct k) auto |
48 |
48 |
49 text\<open>Multiplication of ordinals\<close> |
49 text \<open>Multiplication of ordinals\<close> |
50 primrec mult :: "[brouwer,brouwer] => brouwer" |
50 primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
51 where |
51 where |
52 "mult i Zero = Zero" |
52 "mult i Zero = Zero" |
53 | "mult i (Succ j) = add (mult i j) i" |
53 | "mult i (Succ j) = add (mult i j) i" |
54 | "mult i (Lim f) = Lim (%n. mult i (f n))" |
54 | "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))" |
55 |
55 |
56 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" |
56 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" |
57 by (induct k) (auto simp add: add_assoc) |
57 by (induct k) (auto simp add: add_assoc) |
58 |
58 |
59 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" |
59 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" |
60 by (induct k) (auto simp add: add_mult_distrib) |
60 by (induct k) (auto simp add: add_mult_distrib) |
61 |
61 |
62 text\<open>We could probably instantiate some axiomatic type classes and use |
62 text \<open>We could probably instantiate some axiomatic type classes and use |
63 the standard infix operators.\<close> |
63 the standard infix operators.\<close> |
64 |
64 |
65 subsection\<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close> |
|
66 |
65 |
67 text\<open>To use the function package we need an ordering on the Brouwer |
66 subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close> |
68 ordinals. Start with a predecessor relation and form its transitive |
|
69 closure.\<close> |
|
70 |
67 |
71 definition brouwer_pred :: "(brouwer * brouwer) set" |
68 text \<open>To use the function package we need an ordering on the Brouwer |
72 where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})" |
69 ordinals. Start with a predecessor relation and form its transitive |
|
70 closure.\<close> |
73 |
71 |
74 definition brouwer_order :: "(brouwer * brouwer) set" |
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)})" |
|
74 |
|
75 definition brouwer_order :: "(brouwer \<times> brouwer) set" |
75 where "brouwer_order = brouwer_pred^+" |
76 where "brouwer_order = brouwer_pred^+" |
76 |
77 |
77 lemma wf_brouwer_pred: "wf brouwer_pred" |
78 lemma wf_brouwer_pred: "wf brouwer_pred" |
78 by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) |
79 unfolding wf_def brouwer_pred_def |
|
80 apply clarify |
|
81 apply (induct_tac x) |
|
82 apply blast+ |
|
83 done |
79 |
84 |
80 lemma wf_brouwer_order[simp]: "wf brouwer_order" |
85 lemma wf_brouwer_order[simp]: "wf brouwer_order" |
81 by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) |
86 unfolding brouwer_order_def |
|
87 by (rule wf_trancl[OF wf_brouwer_pred]) |
82 |
88 |
83 lemma [simp]: "(j, Succ j) : brouwer_order" |
89 lemma [simp]: "(j, Succ j) \<in> brouwer_order" |
84 by(auto simp add: brouwer_order_def brouwer_pred_def) |
90 by (auto simp add: brouwer_order_def brouwer_pred_def) |
85 |
91 |
86 lemma [simp]: "(f n, Lim f) : brouwer_order" |
92 lemma [simp]: "(f n, Lim f) \<in> brouwer_order" |
87 by(auto simp add: brouwer_order_def brouwer_pred_def) |
93 by (auto simp add: brouwer_order_def brouwer_pred_def) |
88 |
94 |
89 text\<open>Example of a general function\<close> |
95 text \<open>Example of a general function\<close> |
90 |
|
91 function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
96 function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" |
92 where |
97 where |
93 "add2 i Zero = i" |
98 "add2 i Zero = i" |
94 | "add2 i (Succ j) = Succ (add2 i j)" |
99 | "add2 i (Succ j) = Succ (add2 i j)" |
95 | "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))" |
100 | "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))" |