--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Brouwer.thy Fri Nov 16 22:11:19 2001 +0100
@@ -0,0 +1,85 @@
+(* Title: ZF/Induct/Brouwer.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+header {* Infinite branching datatype definitions *}
+
+theory Brouwer = Main:
+
+subsection {* The Brouwer ordinals *}
+
+consts
+ brouwer :: i
+
+datatype \<subseteq> "Vfrom(0, csucc(nat))"
+ "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
+ monos Pi_mono
+ type_intros inf_datatype_intrs
+
+lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)"
+ by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
+ elim: brouwer.cases [unfolded brouwer.con_defs])
+
+lemma brouwer_induct2:
+ "[| b \<in> brouwer;
+ P(Zero);
+ !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b));
+ !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i)
+ |] ==> P(Lim(h))
+ |] ==> P(b)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "b \<in> brouwer"
+ thus ?thesis
+ apply induct
+ apply (assumption | rule rule_context)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
+qed
+
+
+subsection {* The Martin-Löf wellordering type *}
+
+consts
+ Well :: "[i, i => i] => i"
+
+datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
+ -- {* The union with @{text nat} ensures that the cardinal is infinite. *}
+ "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
+ monos Pi_mono
+ type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs
+
+lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
+ by (fast intro!: Well.intros [unfolded Well.con_defs]
+ elim: Well.cases [unfolded Well.con_defs])
+
+
+lemma Well_induct2:
+ "[| w \<in> Well(A, B);
+ !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y)
+ |] ==> P(Sup(a,f))
+ |] ==> P(w)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "w \<in> Well(A, B)"
+ thus ?thesis
+ apply induct
+ apply (assumption | rule rule_context)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
+qed
+
+lemma Well_bool_unfold: "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))"
+ -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
+ -- {* for @{text Well} to prove this. *}
+ apply (rule Well_unfold [THEN trans])
+ apply (simp add: Sigma_bool Pi_empty1 succ_def)
+ done
+
+end