11 subsection {* The Brouwer ordinals *} |
11 subsection {* The Brouwer ordinals *} |
12 |
12 |
13 consts |
13 consts |
14 brouwer :: i |
14 brouwer :: i |
15 |
15 |
16 datatype \\<subseteq> "Vfrom(0, csucc(nat))" |
16 datatype \<subseteq> "Vfrom(0, csucc(nat))" |
17 "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer") |
17 "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer") |
18 monos Pi_mono |
18 monos Pi_mono |
19 type_intros inf_datatype_intrs |
19 type_intros inf_datatype_intrs |
20 |
20 |
21 lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)" |
21 lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)" |
22 by (fast intro!: brouwer.intros [unfolded brouwer.con_defs] |
22 by (fast intro!: brouwer.intros [unfolded brouwer.con_defs] |
23 elim: brouwer.cases [unfolded brouwer.con_defs]) |
23 elim: brouwer.cases [unfolded brouwer.con_defs]) |
24 |
24 |
25 lemma brouwer_induct2: |
25 lemma brouwer_induct2: |
26 "[| b \\<in> brouwer; |
26 "[| b \<in> brouwer; |
27 P(Zero); |
27 P(Zero); |
28 !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b)); |
28 !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b)); |
29 !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i) |
29 !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |
30 |] ==> P(Lim(h)) |
30 |] ==> P(Lim(h)) |
31 |] ==> P(b)" |
31 |] ==> P(b)" |
32 -- {* A nicer induction rule than the standard one. *} |
32 -- {* A nicer induction rule than the standard one. *} |
33 proof - |
33 proof - |
34 case rule_context |
34 case rule_context |
35 assume "b \\<in> brouwer" |
35 assume "b \<in> brouwer" |
36 thus ?thesis |
36 thus ?thesis |
37 apply induct |
37 apply induct |
38 apply (assumption | rule rule_context)+ |
38 apply (assumption | rule rule_context)+ |
39 apply (fast elim: fun_weaken_type) |
39 apply (fast elim: fun_weaken_type) |
40 apply (fast dest: apply_type) |
40 apply (fast dest: apply_type) |
45 subsection {* The Martin-Löf wellordering type *} |
45 subsection {* The Martin-Löf wellordering type *} |
46 |
46 |
47 consts |
47 consts |
48 Well :: "[i, i => i] => i" |
48 Well :: "[i, i => i] => i" |
49 |
49 |
50 datatype \\<subseteq> "Vfrom(A \\<union> (\\<Union>x \\<in> A. B(x)), csucc(nat \\<union> |\\<Union>x \\<in> A. B(x)|))" |
50 datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))" |
51 -- {* The union with @{text nat} ensures that the cardinal is infinite. *} |
51 -- {* The union with @{text nat} ensures that the cardinal is infinite. *} |
52 "Well(A, B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A, B)") |
52 "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)") |
53 monos Pi_mono |
53 monos Pi_mono |
54 type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs |
54 type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs |
55 |
55 |
56 lemma Well_unfold: "Well(A, B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A, B))" |
56 lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))" |
57 by (fast intro!: Well.intros [unfolded Well.con_defs] |
57 by (fast intro!: Well.intros [unfolded Well.con_defs] |
58 elim: Well.cases [unfolded Well.con_defs]) |
58 elim: Well.cases [unfolded Well.con_defs]) |
59 |
59 |
60 |
60 |
61 lemma Well_induct2: |
61 lemma Well_induct2: |
62 "[| w \\<in> Well(A, B); |
62 "[| w \<in> Well(A, B); |
63 !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y) |
63 !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y) |
64 |] ==> P(Sup(a,f)) |
64 |] ==> P(Sup(a,f)) |
65 |] ==> P(w)" |
65 |] ==> P(w)" |
66 -- {* A nicer induction rule than the standard one. *} |
66 -- {* A nicer induction rule than the standard one. *} |
67 proof - |
67 proof - |
68 case rule_context |
68 case rule_context |
69 assume "w \\<in> Well(A, B)" |
69 assume "w \<in> Well(A, B)" |
70 thus ?thesis |
70 thus ?thesis |
71 apply induct |
71 apply induct |
72 apply (assumption | rule rule_context)+ |
72 apply (assumption | rule rule_context)+ |
73 apply (fast elim: fun_weaken_type) |
73 apply (fast elim: fun_weaken_type) |
74 apply (fast dest: apply_type) |
74 apply (fast dest: apply_type) |
75 done |
75 done |
76 qed |
76 qed |
77 |
77 |
78 lemma Well_bool_unfold: "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))" |
78 lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))" |
79 -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *} |
79 -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *} |
80 -- {* for @{text Well} to prove this. *} |
80 -- {* for @{text Well} to prove this. *} |
81 apply (rule Well_unfold [THEN trans]) |
81 apply (rule Well_unfold [THEN trans]) |
82 apply (simp add: Sigma_bool Pi_empty1 succ_def) |
82 apply (simp add: Sigma_bool Pi_empty1 succ_def) |
83 done |
83 done |