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