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