1 (**** CTT examples -- process using Doc/tout CTT-eg.txt ****) |
|
2 |
|
3 Pretty.setmargin 72; (*existing macros just allow this margin*) |
|
4 print_depth 0; |
|
5 |
|
6 |
|
7 (*** Type inference, from CTT/ex/typechk.ML ***) |
|
8 |
|
9 Goal "lam n. rec(n, 0, %x y. x) : ?A"; |
|
10 by (resolve_tac [ProdI] 1); |
|
11 by (eresolve_tac [NE] 2); |
|
12 by (resolve_tac [NI0] 2); |
|
13 by (assume_tac 2); |
|
14 by (resolve_tac [NF] 1); |
|
15 |
|
16 |
|
17 |
|
18 (*** Logical reasoning, from CTT/ex/elim.ML ***) |
|
19 |
|
20 val prems = Goal |
|
21 "[| A type; \ |
|
22 \ !!x. x:A ==> B(x) type; \ |
|
23 \ !!x. x:A ==> C(x) type; \ |
|
24 \ p: SUM x:A. B(x) + C(x) \ |
|
25 \ |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))"; |
|
26 by (resolve_tac (prems RL [SumE]) 1); |
|
27 by (eresolve_tac [PlusE] 1); |
|
28 by (resolve_tac [PlusI_inl] 1); |
|
29 by (resolve_tac [SumI] 1); |
|
30 by (assume_tac 1); |
|
31 by (assume_tac 1); |
|
32 by (typechk_tac prems); |
|
33 by (pc_tac prems 1); |
|
34 |
|
35 |
|
36 (*** Currying, from CTT/ex/elim.ML ***) |
|
37 |
|
38 val prems = Goal |
|
39 "[| A type; !!x. x:A ==> B(x) type; \ |
|
40 \ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ |
|
41 \ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ |
|
42 \ (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
|
43 by (intr_tac prems); |
|
44 by (eresolve_tac [ProdE] 1); |
|
45 by (intr_tac prems); |
|
46 |
|
47 |
|
48 (*** Axiom of Choice ***) |
|
49 |
|
50 val prems = Goal |
|
51 "[| A type; !!x. x:A ==> B(x) type; \ |
|
52 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
|
53 \ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ |
|
54 \ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
55 by (intr_tac prems); |
|
56 by (eresolve_tac [ProdE RS SumE_fst] 1); |
|
57 by (assume_tac 1); |
|
58 by (resolve_tac [replace_type] 1); |
|
59 by (resolve_tac [subst_eqtyparg] 1); |
|
60 by (resolve_tac [ProdC] 1); |
|
61 by (typechk_tac (SumE_fst::prems)); |
|
62 by (eresolve_tac [ProdE RS SumE_snd] 1); |
|
63 by (typechk_tac prems); |
|
64 |
|
65 |
|
66 |
|
67 |
|
68 |
|
69 STOP_HERE; |
|
70 |
|
71 |
|
72 > val prems = Goal |
|
73 # "[| A type; \ |
|
74 # \ !!x. x:A ==> B(x) type; \ |
|
75 # \ !!x. x:A ==> C(x) type; \ |
|
76 # \ p: SUM x:A. B(x) + C(x) \ |
|
77 # \ |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))"; |
|
78 Level 0 |
|
79 ?a : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
80 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
81 > by (resolve_tac (prems RL [SumE]) 1); |
|
82 Level 1 |
|
83 split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
84 1. !!x y. |
|
85 [| x : A; y : B(x) + C(x) |] ==> |
|
86 ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
87 > by (eresolve_tac [PlusE] 1); |
|
88 Level 2 |
|
89 split(p,%x y. when(y,?c2(x,y),?d2(x,y))) |
|
90 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
91 1. !!x y xa. |
|
92 [| x : A; xa : B(x) |] ==> |
|
93 ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
94 2. !!x y ya. |
|
95 [| x : A; ya : C(x) |] ==> |
|
96 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
97 > by (resolve_tac [PlusI_inl] 1); |
|
98 Level 3 |
|
99 split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y))) |
|
100 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
101 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x) |
|
102 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type |
|
103 3. !!x y ya. |
|
104 [| x : A; ya : C(x) |] ==> |
|
105 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
106 > by (resolve_tac [SumI] 1); |
|
107 Level 4 |
|
108 split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y))) |
|
109 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
110 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A |
|
111 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa)) |
|
112 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type |
|
113 4. !!x y ya. |
|
114 [| x : A; ya : C(x) |] ==> |
|
115 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
116 > by (assume_tac 1); |
|
117 Level 5 |
|
118 split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y))) |
|
119 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
120 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x) |
|
121 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type |
|
122 3. !!x y ya. |
|
123 [| x : A; ya : C(x) |] ==> |
|
124 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
125 > by (assume_tac 1); |
|
126 Level 6 |
|
127 split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y))) |
|
128 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
129 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type |
|
130 2. !!x y ya. |
|
131 [| x : A; ya : C(x) |] ==> |
|
132 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
133 > by (typechk_tac prems); |
|
134 Level 7 |
|
135 split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y))) |
|
136 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
137 1. !!x y ya. |
|
138 [| x : A; ya : C(x) |] ==> |
|
139 ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
140 > by (pc_tac prems 1); |
|
141 Level 8 |
|
142 split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>))) |
|
143 : (SUM x:A. B(x)) + (SUM x:A. C(x)) |
|
144 No subgoals! |
|
145 |
|
146 |
|
147 |
|
148 |
|
149 > val prems = Goal |
|
150 # "[| A type; !!x. x:A ==> B(x) type; \ |
|
151 # \ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \ |
|
152 # \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ |
|
153 # \ --> (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
|
154 Level 0 |
|
155 ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>)) |
|
156 1. ?a : (PROD z:SUM x:A. B(x). C(z)) --> |
|
157 (PROD x:A. PROD y:B(x). C(<x,y>)) |
|
158 > by (intr_tac prems); |
|
159 Level 1 |
|
160 lam x xa xb. ?b7(x,xa,xb) |
|
161 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>)) |
|
162 1. !!uu x y. |
|
163 [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==> |
|
164 ?b7(uu,x,y) : C(<x,y>) |
|
165 > by (eresolve_tac [ProdE] 1); |
|
166 Level 2 |
|
167 lam x xa xb. x ` <xa,xb> |
|
168 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>)) |
|
169 1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x) |
|
170 > by (intr_tac prems); |
|
171 Level 3 |
|
172 lam x xa xb. x ` <xa,xb> |
|
173 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>)) |
|
174 No subgoals! |
|
175 |
|
176 |
|
177 |
|
178 |
|
179 > val prems = Goal |
|
180 # "[| A type; !!x. x:A ==> B(x) type; \ |
|
181 # \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
|
182 # \ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ |
|
183 # \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
184 Level 0 |
|
185 ?a : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
186 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
187 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
188 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
189 > by (intr_tac prems); |
|
190 Level 1 |
|
191 lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)> |
|
192 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
193 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
194 1. !!uu x. |
|
195 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
196 ?b7(uu,x) : B(x) |
|
197 2. !!uu x. |
|
198 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
199 ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x) |
|
200 > by (eresolve_tac [ProdE RS SumE_fst] 1); |
|
201 Level 2 |
|
202 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
203 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
204 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
205 1. !!uu x. x : A ==> x : A |
|
206 2. !!uu x. |
|
207 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
208 ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x) |
|
209 > by (assume_tac 1); |
|
210 Level 3 |
|
211 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
212 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
213 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
214 1. !!uu x. |
|
215 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
216 ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x) |
|
217 > by (resolve_tac [replace_type] 1); |
|
218 Level 4 |
|
219 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
220 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
221 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
222 1. !!uu x. |
|
223 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
224 C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x) |
|
225 2. !!uu x. |
|
226 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
227 ?b8(uu,x) : ?A13(uu,x) |
|
228 > by (resolve_tac [subst_eqtyparg] 1); |
|
229 Level 5 |
|
230 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
231 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
232 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
233 1. !!uu x. |
|
234 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
235 (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x) |
|
236 2. !!uu x z. |
|
237 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A; |
|
238 z : ?A14(uu,x) |] ==> |
|
239 C(x,z) type |
|
240 3. !!uu x. |
|
241 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
242 ?b8(uu,x) : C(x,?c14(uu,x)) |
|
243 > by (resolve_tac [ProdC] 1); |
|
244 Level 6 |
|
245 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
246 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
247 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
248 1. !!uu x. |
|
249 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x) |
|
250 2. !!uu x xa. |
|
251 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A; |
|
252 xa : ?A15(uu,x) |] ==> |
|
253 fst(uu ` xa) : ?B15(uu,x,xa) |
|
254 3. !!uu x z. |
|
255 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A; |
|
256 z : ?B15(uu,x,x) |] ==> |
|
257 C(x,z) type |
|
258 4. !!uu x. |
|
259 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
260 ?b8(uu,x) : C(x,fst(uu ` x)) |
|
261 > by (typechk_tac (SumE_fst::prems)); |
|
262 Level 7 |
|
263 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)> |
|
264 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
265 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
266 1. !!uu x. |
|
267 [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> |
|
268 ?b8(uu,x) : C(x,fst(uu ` x)) |
|
269 > by (eresolve_tac [ProdE RS SumE_snd] 1); |
|
270 Level 8 |
|
271 lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)> |
|
272 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
273 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
274 1. !!uu x. x : A ==> x : A |
|
275 2. !!uu x. x : A ==> B(x) type |
|
276 3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type |
|
277 > by (typechk_tac prems); |
|
278 Level 9 |
|
279 lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)> |
|
280 : (PROD x:A. SUM y:B(x). C(x,y)) --> |
|
281 (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x)) |
|
282 No subgoals! |
|