1(*  Title:      ZF/Induct/Brouwer.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1994  University of Cambridge
4*)
5
6section \<open>Infinite branching datatype definitions\<close>
7
8theory Brouwer imports ZFC begin
9
10subsection \<open>The Brouwer ordinals\<close>
11
12consts
13  brouwer :: i
14
15datatype \<subseteq> "Vfrom(0, csucc(nat))"
16    "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
17  monos Pi_mono
18  type_intros inf_datatype_intros
19
20lemma 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
24lemma 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)"
31  \<comment> \<open>A nicer induction rule than the standard one.\<close>
32  using b
33  apply induct
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
40
41
42subsection \<open>The Martin-L��f wellordering type\<close>
43
44consts
45  Well :: "[i, i => i] => i"
46
47datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
48    \<comment> \<open>The union with \<open>nat\<close> ensures that the cardinal is infinite.\<close>
49  "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
50  monos Pi_mono
51  type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
52
53lemma Well_unfold: "Well(A, B) = (\<Sum>x \<in> A. B(x) -> Well(A, B))"
54  by (fast intro!: Well.intros [unfolded Well.con_defs]
55    elim: Well.cases [unfolded Well.con_defs])
56
57
58lemma 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)"
62  \<comment> \<open>A nicer induction rule than the standard one.\<close>
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
69
70lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
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>
73  apply (rule Well_unfold [THEN trans])
74  apply (simp add: Sigma_bool succ_def)
75  done
76
77end
78