17 |
17 |
18 goal thy "A:* |- A->A : ?T"; |
18 goal thy "A:* |- A->A : ?T"; |
19 by (DEPTH_SOLVE (ares_tac simple 1)); |
19 by (DEPTH_SOLVE (ares_tac simple 1)); |
20 uresult(); |
20 uresult(); |
21 |
21 |
22 goal thy "A:* |- Lam a:A.a : ?T"; |
22 goal thy "A:* |- Lam a:A. a : ?T"; |
23 by (DEPTH_SOLVE (ares_tac simple 1)); |
23 by (DEPTH_SOLVE (ares_tac simple 1)); |
24 uresult(); |
24 uresult(); |
25 |
25 |
26 goal thy "A:* B:* b:B |- Lam x:A.b : ?T"; |
26 goal thy "A:* B:* b:B |- Lam x:A. b : ?T"; |
27 by (DEPTH_SOLVE (ares_tac simple 1)); |
27 by (DEPTH_SOLVE (ares_tac simple 1)); |
28 uresult(); |
28 uresult(); |
29 |
29 |
30 goal thy "A:* b:A |- (Lam a:A.a)^b: ?T"; |
30 goal thy "A:* b:A |- (Lam a:A. a)^b: ?T"; |
31 by (DEPTH_SOLVE (ares_tac simple 1)); |
31 by (DEPTH_SOLVE (ares_tac simple 1)); |
32 uresult(); |
32 uresult(); |
33 |
33 |
34 goal thy "A:* B:* c:A b:B |- (Lam x:A.b)^ c: ?T"; |
34 goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"; |
35 by (DEPTH_SOLVE (ares_tac simple 1)); |
35 by (DEPTH_SOLVE (ares_tac simple 1)); |
36 uresult(); |
36 uresult(); |
37 |
37 |
38 goal thy "A:* B:* |- Lam a:A.Lam b:B.a : ?T"; |
38 goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T"; |
39 by (DEPTH_SOLVE (ares_tac simple 1)); |
39 by (DEPTH_SOLVE (ares_tac simple 1)); |
40 uresult(); |
40 uresult(); |
41 |
41 |
42 (* SECOND-ORDER TYPES *) |
42 (* SECOND-ORDER TYPES *) |
43 |
43 |
44 goal L2_thy "|- Lam A:*. Lam a:A.a : ?T"; |
44 goal L2_thy "|- Lam A:*. Lam a:A. a : ?T"; |
45 by (DEPTH_SOLVE (ares_tac L2 1)); |
45 by (DEPTH_SOLVE (ares_tac L2 1)); |
46 uresult(); |
46 uresult(); |
47 |
47 |
48 goal L2_thy "A:* |- (Lam B:*.Lam b:B.b)^A : ?T"; |
48 goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"; |
49 by (DEPTH_SOLVE (ares_tac L2 1)); |
49 by (DEPTH_SOLVE (ares_tac L2 1)); |
50 uresult(); |
50 uresult(); |
51 |
51 |
52 goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B.b) ^ A ^ b: ?T"; |
52 goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"; |
53 by (DEPTH_SOLVE (ares_tac L2 1)); |
53 by (DEPTH_SOLVE (ares_tac L2 1)); |
54 uresult(); |
54 uresult(); |
55 |
55 |
56 goal L2_thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"; |
56 goal L2_thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"; |
57 by (DEPTH_SOLVE (ares_tac L2 1)); |
57 by (DEPTH_SOLVE (ares_tac L2 1)); |
65 |
65 |
66 goal Lomega_thy "B:* |- (Lam A:*.A->A) ^ B : ?T"; |
66 goal Lomega_thy "B:* |- (Lam A:*.A->A) ^ B : ?T"; |
67 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
67 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
68 uresult(); |
68 uresult(); |
69 |
69 |
70 goal Lomega_thy "B:* b:B |- (Lam y:B.b): ?T"; |
70 goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T"; |
71 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
71 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
72 uresult(); |
72 uresult(); |
73 |
73 |
74 goal Lomega_thy "A:* F:*->* |- F^(F^A): ?T"; |
74 goal Lomega_thy "A:* F:*->* |- F^(F^A): ?T"; |
75 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
75 by (DEPTH_SOLVE (ares_tac Lomega 1)); |
87 |
87 |
88 goal LP_thy "A:* P:A->* a:A |- P^a: ?T"; |
88 goal LP_thy "A:* P:A->* a:A |- P^a: ?T"; |
89 by (DEPTH_SOLVE (ares_tac LP 1)); |
89 by (DEPTH_SOLVE (ares_tac LP 1)); |
90 uresult(); |
90 uresult(); |
91 |
91 |
92 goal LP_thy "A:* P:A->A->* a:A |- Pi a:A.P^a^a: ?T"; |
92 goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"; |
93 by (DEPTH_SOLVE (ares_tac LP 1)); |
93 by (DEPTH_SOLVE (ares_tac LP 1)); |
94 uresult(); |
94 uresult(); |
95 |
95 |
96 goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A.P^a -> Q^a: ?T"; |
96 goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"; |
97 by (DEPTH_SOLVE (ares_tac LP 1)); |
97 by (DEPTH_SOLVE (ares_tac LP 1)); |
98 uresult(); |
98 uresult(); |
99 |
99 |
100 goal LP_thy "A:* P:A->* |- Pi a:A.P^a -> P^a: ?T"; |
100 goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"; |
101 by (DEPTH_SOLVE (ares_tac LP 1)); |
101 by (DEPTH_SOLVE (ares_tac LP 1)); |
102 uresult(); |
102 uresult(); |
103 |
103 |
104 goal LP_thy "A:* P:A->* |- Lam a:A.Lam x:P^a.x: ?T"; |
104 goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"; |
105 by (DEPTH_SOLVE (ares_tac LP 1)); |
105 by (DEPTH_SOLVE (ares_tac LP 1)); |
106 uresult(); |
106 uresult(); |
107 |
107 |
108 goal LP_thy "A:* P:A->* Q:* |- (Pi a:A.P^a->Q) -> (Pi a:A.P^a) -> Q : ?T"; |
108 goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"; |
109 by (DEPTH_SOLVE (ares_tac LP 1)); |
109 by (DEPTH_SOLVE (ares_tac LP 1)); |
110 uresult(); |
110 uresult(); |
111 |
111 |
112 goal LP_thy "A:* P:A->* Q:* a0:A |- \ |
112 goal LP_thy "A:* P:A->* Q:* a0:A |- \ |
113 \ Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T"; |
113 \ Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T"; |
114 by (DEPTH_SOLVE (ares_tac LP 1)); |
114 by (DEPTH_SOLVE (ares_tac LP 1)); |
115 uresult(); |
115 uresult(); |
116 |
116 |
117 (* OMEGA-ORDER TYPES *) |
117 (* OMEGA-ORDER TYPES *) |
118 |
118 |
122 |
122 |
123 goal LOmega_thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"; |
123 goal LOmega_thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"; |
124 by (DEPTH_SOLVE (ares_tac LOmega 1)); |
124 by (DEPTH_SOLVE (ares_tac LOmega 1)); |
125 uresult(); |
125 uresult(); |
126 |
126 |
127 goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A.Lam y:B.x : ?T"; |
127 goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"; |
128 by (DEPTH_SOLVE (ares_tac LOmega 1)); |
128 by (DEPTH_SOLVE (ares_tac LOmega 1)); |
129 uresult(); |
129 uresult(); |
130 |
130 |
131 goal LOmega_thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"; |
131 goal LOmega_thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"; |
132 by (strip_asms_tac LOmega 1); |
132 by (strip_asms_tac LOmega 1); |
146 by (assume_tac 1); |
146 by (assume_tac 1); |
147 uresult(); |
147 uresult(); |
148 |
148 |
149 (* Second-order Predicate Logic *) |
149 (* Second-order Predicate Logic *) |
150 |
150 |
151 goal LP2_thy "A:* P:A->* |- Lam a:A.P^a->(Pi A:*.A) : ?T"; |
151 goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"; |
152 by (DEPTH_SOLVE (ares_tac LP2 1)); |
152 by (DEPTH_SOLVE (ares_tac LP2 1)); |
153 uresult(); |
153 uresult(); |
154 |
154 |
155 goal LP2_thy "A:* P:A->A->* |- \ |
155 goal LP2_thy "A:* P:A->A->* |- \ |
156 \ (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T"; |
156 \ (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P : ?T"; |
157 by (DEPTH_SOLVE (ares_tac LP2 1)); |
157 by (DEPTH_SOLVE (ares_tac LP2 1)); |
158 uresult(); |
158 uresult(); |
159 |
159 |
160 (* Antisymmetry implies irreflexivity: *) |
160 (* Antisymmetry implies irreflexivity: *) |
161 goal LP2_thy "A:* P:A->A->* |- \ |
161 goal LP2_thy "A:* P:A->A->* |- \ |
162 \ ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P"; |
162 \ ?p: (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P"; |
163 by (strip_asms_tac LP2 1); |
163 by (strip_asms_tac LP2 1); |
164 by (rtac lam_ss 1); |
164 by (rtac lam_ss 1); |
165 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
165 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
166 by (DEPTH_SOLVE_1(ares_tac LP2 2)); |
166 by (DEPTH_SOLVE_1(ares_tac LP2 2)); |
167 by (rtac lam_ss 1); |
167 by (rtac lam_ss 1); |
173 by (REPEAT(EVERY[etac pi_elim 1, assume_tac 1, TRY(assume_tac 1)])); |
173 by (REPEAT(EVERY[etac pi_elim 1, assume_tac 1, TRY(assume_tac 1)])); |
174 uresult(); |
174 uresult(); |
175 |
175 |
176 (* LPomega *) |
176 (* LPomega *) |
177 |
177 |
178 goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A.P^a^a : ?T"; |
178 goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"; |
179 by (DEPTH_SOLVE (ares_tac LPomega 1)); |
179 by (DEPTH_SOLVE (ares_tac LPomega 1)); |
180 uresult(); |
180 uresult(); |
181 |
181 |
182 goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A.P^a^a : ?T"; |
182 goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"; |
183 by (DEPTH_SOLVE (ares_tac LPomega 1)); |
183 by (DEPTH_SOLVE (ares_tac LPomega 1)); |
184 uresult(); |
184 uresult(); |
185 |
185 |
186 (* CONSTRUCTIONS *) |
186 (* CONSTRUCTIONS *) |
187 |
187 |
188 goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A.P^a->Pi P:*.P: ?T"; |
188 goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"; |
189 by (DEPTH_SOLVE (ares_tac CC 1)); |
189 by (DEPTH_SOLVE (ares_tac CC 1)); |
190 uresult(); |
190 uresult(); |
191 |
191 |
192 goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A.P^a: ?T"; |
192 goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"; |
193 by (DEPTH_SOLVE (ares_tac CC 1)); |
193 by (DEPTH_SOLVE (ares_tac CC 1)); |
194 uresult(); |
194 uresult(); |
195 |
195 |
196 goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A.P^a)->P^a"; |
196 goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"; |
197 by (strip_asms_tac CC 1); |
197 by (strip_asms_tac CC 1); |
198 by (rtac lam_ss 1); |
198 by (rtac lam_ss 1); |
199 by (DEPTH_SOLVE_1(ares_tac CC 1)); |
199 by (DEPTH_SOLVE_1(ares_tac CC 1)); |
200 by (DEPTH_SOLVE_1(ares_tac CC 2)); |
200 by (DEPTH_SOLVE_1(ares_tac CC 2)); |
201 by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]); |
201 by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]); |
206 goal LP2_thy "A:* c:A f:A->A |- \ |
206 goal LP2_thy "A:* c:A f:A->A |- \ |
207 \ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"; |
207 \ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"; |
208 by (DEPTH_SOLVE(ares_tac LP2 1)); |
208 by (DEPTH_SOLVE(ares_tac LP2 1)); |
209 uresult(); |
209 uresult(); |
210 |
210 |
211 goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \ |
211 goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \ |
212 \ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"; |
212 \ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"; |
213 by (DEPTH_SOLVE(ares_tac CC 1)); |
213 by (DEPTH_SOLVE(ares_tac CC 1)); |
214 uresult(); |
214 uresult(); |
215 |
215 |
216 (* Symmetry of Leibnitz equality *) |
216 (* Symmetry of Leibnitz equality *) |
217 goal LP2_thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)"; |
217 goal LP2_thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)"; |
218 by (strip_asms_tac LP2 1); |
218 by (strip_asms_tac LP2 1); |
219 by (rtac lam_ss 1); |
219 by (rtac lam_ss 1); |
220 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
220 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
221 by (DEPTH_SOLVE_1(ares_tac LP2 2)); |
221 by (DEPTH_SOLVE_1(ares_tac LP2 2)); |
222 by (eres_inst_tac [("a","Lam x:A.Pi Q:A->*.Q^x->Q^a")] pi_elim 1); |
222 by (eres_inst_tac [("a","Lam x:A. Pi Q:A->*.Q^x->Q^a")] pi_elim 1); |
223 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
223 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
224 by (rewtac beta); |
224 by (rewtac beta); |
225 by (etac imp_elim 1); |
225 by (etac imp_elim 1); |
226 by (rtac lam_bs 1); |
226 by (rtac lam_bs 1); |
227 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |
227 by (DEPTH_SOLVE_1(ares_tac LP2 1)); |