12 |
12 |
13 (** The Brouwer ordinals **) |
13 (** The Brouwer ordinals **) |
14 |
14 |
15 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)"; |
15 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)"; |
16 let open brouwer; val rew = rewrite_rule con_defs in |
16 let open brouwer; val rew = rewrite_rule con_defs in |
17 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
17 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
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 |
26 \ !!h. [| h: nat -> brouwer; ALL i:nat. P(h`i) \ |
26 \ !!h. [| h: nat -> brouwer; ALL i: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); |
32 by (fast_tac (!claset addDs [apply_type]) 1); |
32 by (fast_tac (claset() addDs [apply_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 Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))"; |
38 goal Brouwer.thy "Well(A,B) = (SUM x: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 |
47 \ !!a f. [| a: A; f: B(a) -> Well(A,B); ALL y: B(a). P(f`y) \ |
47 \ !!a f. [| a: A; f: B(a) -> Well(A,B); ALL y: 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); |
53 by (fast_tac (!claset addDs [apply_type]) 1); |
53 by (fast_tac (claset() addDs [apply_type]) 1); |
54 qed "Well_induct2"; |
54 qed "Well_induct2"; |
55 |
55 |
56 |
56 |
57 (*In fact it's isomorphic to nat, but we need a recursion operator for |
57 (*In fact it's isomorphic to nat, but we need a recursion operator for |
58 Well to prove this.*) |
58 Well to prove this.*) |
59 goal Brouwer.thy "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))"; |
59 goal Brouwer.thy "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))"; |
60 by (resolve_tac [Well_unfold RS trans] 1); |
60 by (resolve_tac [Well_unfold RS trans] 1); |
61 by (simp_tac (!simpset addsimps [Sigma_bool, Pi_empty1, succ_def]) 1); |
61 by (simp_tac (simpset() addsimps [Sigma_bool, Pi_empty1, succ_def]) 1); |
62 qed "Well_bool_unfold"; |
62 qed "Well_bool_unfold"; |