18 end; |
18 end; |
19 qed "brouwer_unfold"; |
19 qed "brouwer_unfold"; |
20 |
20 |
21 (*A nicer induction rule than the standard one*) |
21 (*A nicer induction rule than the standard one*) |
22 val major::prems = goal Brouwer.thy |
22 val major::prems = goal Brouwer.thy |
23 "[| b: brouwer; \ |
23 "[| b \\<in> brouwer; \ |
24 \ P(Zero); \ |
24 \ P(Zero); \ |
25 \ !!b. [| b: brouwer; P(b) |] ==> P(Suc(b)); \ |
25 \ !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b)); \ |
26 \ !!h. [| h: nat -> brouwer; ALL i:nat. P(h`i) \ |
26 \ !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i) \ |
27 \ |] ==> P(Lim(h)) \ |
27 \ |] ==> P(Lim(h)) \ |
28 \ |] ==> P(b)"; |
28 \ |] ==> P(b)"; |
29 by (rtac (major RS brouwer.induct) 1); |
29 by (rtac (major RS brouwer.induct) 1); |
30 by (REPEAT_SOME (ares_tac prems)); |
30 by (REPEAT_SOME (ares_tac prems)); |
31 by (fast_tac (claset() addEs [fun_weaken_type]) 1); |
31 by (fast_tac (claset() addEs [fun_weaken_type]) 1); |
33 qed "brouwer_induct2"; |
33 qed "brouwer_induct2"; |
34 |
34 |
35 |
35 |
36 (** The Martin-Löf wellordering type **) |
36 (** The Martin-Löf wellordering type **) |
37 |
37 |
38 Goal "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))"; |
38 Goal "Well(A,B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A,B))"; |
39 let open Well; val rew = rewrite_rule con_defs in |
39 let open Well; val rew = rewrite_rule con_defs in |
40 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
40 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
41 end; |
41 end; |
42 qed "Well_unfold"; |
42 qed "Well_unfold"; |
43 |
43 |
44 (*A nicer induction rule than the standard one*) |
44 (*A nicer induction rule than the standard one*) |
45 val major::prems = goal Brouwer.thy |
45 val major::prems = goal Brouwer.thy |
46 "[| w: Well(A,B); \ |
46 "[| w \\<in> Well(A,B); \ |
47 \ !!a f. [| a: A; f: B(a) -> Well(A,B); ALL y: B(a). P(f`y) \ |
47 \ !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y) \ |
48 \ |] ==> P(Sup(a,f)) \ |
48 \ |] ==> P(Sup(a,f)) \ |
49 \ |] ==> P(w)"; |
49 \ |] ==> P(w)"; |
50 by (rtac (major RS Well.induct) 1); |
50 by (rtac (major RS Well.induct) 1); |
51 by (REPEAT_SOME (ares_tac prems)); |
51 by (REPEAT_SOME (ares_tac prems)); |
52 by (fast_tac (claset() addEs [fun_weaken_type]) 1); |
52 by (fast_tac (claset() addEs [fun_weaken_type]) 1); |