20 |
20 |
21 lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)" |
21 lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)" |
22 by (fast intro!: brouwer.intros [unfolded brouwer.con_defs] |
22 by (fast intro!: brouwer.intros [unfolded brouwer.con_defs] |
23 elim: brouwer.cases [unfolded brouwer.con_defs]) |
23 elim: brouwer.cases [unfolded brouwer.con_defs]) |
24 |
24 |
25 lemma brouwer_induct2: |
25 lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]: |
26 "[| b \<in> brouwer; |
26 assumes b: "b \<in> brouwer" |
27 P(Zero); |
27 and cases: |
28 !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b)); |
28 "P(Zero)" |
29 !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |
29 "!!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b))" |
30 |] ==> P(Lim(h)) |
30 "!!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))" |
31 |] ==> P(b)" |
31 shows "P(b)" |
32 -- {* A nicer induction rule than the standard one. *} |
32 -- {* A nicer induction rule than the standard one. *} |
33 proof - |
33 using b |
34 case rule_context |
34 apply induct |
35 assume "b \<in> brouwer" |
35 apply (assumption | rule cases)+ |
36 thus ?thesis |
|
37 apply induct |
|
38 apply (assumption | rule rule_context)+ |
|
39 apply (fast elim: fun_weaken_type) |
36 apply (fast elim: fun_weaken_type) |
40 apply (fast dest: apply_type) |
37 apply (fast dest: apply_type) |
41 done |
38 done |
42 qed |
|
43 |
39 |
44 |
40 |
45 subsection {* The Martin-Löf wellordering type *} |
41 subsection {* The Martin-Löf wellordering type *} |
46 |
42 |
47 consts |
43 consts |
56 lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))" |
52 lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))" |
57 by (fast intro!: Well.intros [unfolded Well.con_defs] |
53 by (fast intro!: Well.intros [unfolded Well.con_defs] |
58 elim: Well.cases [unfolded Well.con_defs]) |
54 elim: Well.cases [unfolded Well.con_defs]) |
59 |
55 |
60 |
56 |
61 lemma Well_induct2: |
57 lemma Well_induct2 [consumes 1, case_names step]: |
62 "[| w \<in> Well(A, B); |
58 assumes w: "w \<in> Well(A, B)" |
63 !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y) |
59 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))" |
64 |] ==> P(Sup(a,f)) |
60 shows "P(w)" |
65 |] ==> P(w)" |
|
66 -- {* A nicer induction rule than the standard one. *} |
61 -- {* A nicer induction rule than the standard one. *} |
67 proof - |
62 using w |
68 case rule_context |
63 apply induct |
69 assume "w \<in> Well(A, B)" |
64 apply (assumption | rule step)+ |
70 thus ?thesis |
65 apply (fast elim: fun_weaken_type) |
71 apply induct |
66 apply (fast dest: apply_type) |
72 apply (assumption | rule rule_context)+ |
67 done |
73 apply (fast elim: fun_weaken_type) |
|
74 apply (fast dest: apply_type) |
|
75 done |
|
76 qed |
|
77 |
68 |
78 lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))" |
69 lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))" |
79 -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *} |
70 -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *} |
80 -- {* for @{text Well} to prove this. *} |
71 -- {* for @{text Well} to prove this. *} |
81 apply (rule Well_unfold [THEN trans]) |
72 apply (rule Well_unfold [THEN trans]) |