12229
|
1 |
(* Title: ZF/Induct/Brouwer.thy
|
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
3 |
Copyright 1994 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
60770
|
6 |
section \<open>Infinite branching datatype definitions\<close>
|
12229
|
7 |
|
16417
|
8 |
theory Brouwer imports Main_ZFC begin
|
12229
|
9 |
|
60770
|
10 |
subsection \<open>The Brouwer ordinals\<close>
|
12229
|
11 |
|
|
12 |
consts
|
|
13 |
brouwer :: i
|
|
14 |
|
12610
|
15 |
datatype \<subseteq> "Vfrom(0, csucc(nat))"
|
|
16 |
"brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
|
12229
|
17 |
monos Pi_mono
|
13137
|
18 |
type_intros inf_datatype_intros
|
12229
|
19 |
|
|
20 |
lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)"
|
|
21 |
by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
|
|
22 |
elim: brouwer.cases [unfolded brouwer.con_defs])
|
|
23 |
|
18372
|
24 |
lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]:
|
|
25 |
assumes b: "b \<in> brouwer"
|
|
26 |
and cases:
|
|
27 |
"P(Zero)"
|
|
28 |
"!!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b))"
|
|
29 |
"!!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
|
|
30 |
shows "P(b)"
|
61798
|
31 |
\<comment> \<open>A nicer induction rule than the standard one.\<close>
|
18372
|
32 |
using b
|
|
33 |
apply induct
|
23464
|
34 |
apply (rule cases(1))
|
|
35 |
apply (erule (1) cases(2))
|
|
36 |
apply (rule cases(3))
|
|
37 |
apply (fast elim: fun_weaken_type)
|
|
38 |
apply (fast dest: apply_type)
|
|
39 |
done
|
12229
|
40 |
|
|
41 |
|
60770
|
42 |
subsection \<open>The Martin-Löf wellordering type\<close>
|
12229
|
43 |
|
|
44 |
consts
|
|
45 |
Well :: "[i, i => i] => i"
|
|
46 |
|
12610
|
47 |
datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
|
61798
|
48 |
\<comment> \<open>The union with \<open>nat\<close> ensures that the cardinal is infinite.\<close>
|
12610
|
49 |
"Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
|
12229
|
50 |
monos Pi_mono
|
13137
|
51 |
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
|
12229
|
52 |
|
61980
|
53 |
lemma Well_unfold: "Well(A, B) = (\<Sum>x \<in> A. B(x) -> Well(A, B))"
|
12229
|
54 |
by (fast intro!: Well.intros [unfolded Well.con_defs]
|
|
55 |
elim: Well.cases [unfolded Well.con_defs])
|
|
56 |
|
|
57 |
|
18372
|
58 |
lemma Well_induct2 [consumes 1, case_names step]:
|
|
59 |
assumes w: "w \<in> Well(A, B)"
|
|
60 |
and step: "!!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
|
|
61 |
shows "P(w)"
|
61798
|
62 |
\<comment> \<open>A nicer induction rule than the standard one.\<close>
|
18372
|
63 |
using w
|
|
64 |
apply induct
|
|
65 |
apply (assumption | rule step)+
|
|
66 |
apply (fast elim: fun_weaken_type)
|
|
67 |
apply (fast dest: apply_type)
|
|
68 |
done
|
12229
|
69 |
|
12610
|
70 |
lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
|
61798
|
71 |
\<comment> \<open>In fact it's isomorphic to \<open>nat\<close>, but we need a recursion operator\<close>
|
|
72 |
\<comment> \<open>for \<open>Well\<close> to prove this.\<close>
|
12229
|
73 |
apply (rule Well_unfold [THEN trans])
|
46900
|
74 |
apply (simp add: Sigma_bool succ_def)
|
12229
|
75 |
done
|
|
76 |
|
|
77 |
end
|