equal
deleted
inserted
replaced
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 (equalityI :: map rew intrs) |
17 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
18 addEs [rew elim]) 1) |
|
19 end; |
18 end; |
20 qed "brouwer_unfold"; |
19 qed "brouwer_unfold"; |
21 |
20 |
22 (*A nicer induction rule than the standard one*) |
21 (*A nicer induction rule than the standard one*) |
23 val major::prems = goal Brouwer.thy |
22 val major::prems = goal Brouwer.thy |
36 |
35 |
37 (** The Martin-Löf wellordering type **) |
36 (** The Martin-Löf wellordering type **) |
38 |
37 |
39 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))"; |
40 let open Well; val rew = rewrite_rule con_defs in |
39 let open Well; val rew = rewrite_rule con_defs in |
41 by (fast_tac (!claset addSIs (equalityI :: map rew intrs) |
40 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
42 addEs [rew elim]) 1) |
|
43 end; |
41 end; |
44 qed "Well_unfold"; |
42 qed "Well_unfold"; |
45 |
43 |
46 (*A nicer induction rule than the standard one*) |
44 (*A nicer induction rule than the standard one*) |
47 val major::prems = goal Brouwer.thy |
45 val major::prems = goal Brouwer.thy |