/[mojave]/metaprl/theories/itt/itt_comment.ml
ViewVC logotype

Contents of /metaprl/theories/itt/itt_comment.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3325 - (show annotations) (download)
Tue Jul 10 00:11:03 2001 UTC (20 years ago) by nogin
File size: 32489 byte(s)
- Rewrote the Itt_esquash theory based on my "better_tt" ideas.
- Now esquash is a primitive operator and not a defined one.
- This change also broke a few FOL and CZF theories that relied
on a bunch of invalid rules that I had to remove from Itt_esquash.

1 (*!
2 * @begin[doc]
3 * @theory[Itt_comment]
4 *
5 * Terms used for comments in the @Nuprl type theory.
6 * @end[doc]
7 *
8 * ----------------------------------------------------------------
9 *
10 * @begin[license]
11 * Copyright (C) 2000 Jason Hickey, Caltech
12 *
13 * This program is free software; you can redistribute it and/or
14 * modify it under the terms of the GNU General Public License
15 * as published by the Free Software Foundation; either version 2
16 * of the License, or (at your option) any later version.
17 *
18 * This program is distributed in the hope that it will be useful,
19 * but WITHOUT ANY WARRANTY; without even the implied warranty of
20 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
21 * GNU General Public License for more details.
22 *
23 * You should have received a copy of the GNU General Public License
24 * along with this program; if not, write to the Free Software
25 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
26 *
27 * Author: Jason Hickey
28 * @email{jyh@cs.caltech.edu}
29 * @end[license]
30 *)
31
32 include Base_theory
33
34 (************************************************************************
35 * UNIVERSES AND EQUALITY
36 ************************************************************************)
37
38 declare math_type{'a}
39 declare math_univ{'i}
40 declare math_equal{'T; 'a; 'b}
41 declare math_member{'T; 'a}
42 declare math_cumulativity{'i; 'j}
43
44 prec prec_type
45 prec prec_equal
46
47 (************************************************
48 * TeX mode.
49 *)
50 dform math_type_df1 : mode[tex] :: math_type{'t} =
51 slot{'t}
52 izone `"\\,\\mathtt{" ezone
53 `"Type"
54 izone "}" ezone
55
56 dform math_univ_df : mode[tex] :: math_univ{'i} =
57 izone `"{\\mathbb U}_{" ezone
58 slot{'i}
59 izone `"}" ezone
60
61 dform math_equal_df1 : mode[tex] :: math_equal{'T; 'a; 'b} =
62 izone `"{" ezone
63 slot{'a}
64 izone `" = " ezone
65 slot{'b}
66 izone `" \\in " ezone
67 slot{'T}
68 izone `"}" ezone
69
70 dform math_member_df1 : mode[tex] :: math_member{'T; 'a} =
71 izone `"{" ezone
72 slot{'a}
73 izone `" \\in " ezone
74 slot{'T}
75 izone `"}" ezone
76
77 dform math_cumulativity_df1 : mode[tex] :: math_cumulativity{'i; 'j} =
78 izone `"{{\\it cumulativity}[" ezone
79 slot{'i}
80 izone `", " ezone
81 slot{'j}
82 izone `"]}" ezone
83
84 (************************************************
85 * Normal mode.
86 *)
87
88 dform equal_df : except_mode[tex] :: parens :: "prec"[prec_equal] :: math_equal{'T; 'a; 'b} =
89 szone pushm slot{'a} space `"= " slot{'b} space Nuprl_font!member `" " slot{'T} popm ezone
90
91 dform member_df2 : mode[tex] :: parens :: "prec"[prec_equal] :: math_member{'T; 'a} =
92 szone pushm slot{'a} space `"IN" hspace slot{'T} popm ezone
93
94 dform type_df1 : except_mode[tex] :: parens :: "prec"[prec_type] :: math_type{'a} =
95 slot{'a} " " `"Type"
96
97 dform univ_df1 : except_mode[tex] :: math_univ{'i} =
98 mathbbU `"[" slot{'i} `"]"
99
100 dform cumulativity_df : except_mode[tex] :: math_cumulativity{'i; 'j} =
101 `"cumulativity[" slot{'i} `";" slot{'j} `"]"
102
103 (************************************************************************
104 * VOID
105 ************************************************************************)
106
107 declare math_void
108 declare math_false
109
110 dform math_Void_df1 : math_void =
111 math_i["Void"]
112
113 dform math_False_df1 : mode[tex] :: math_false =
114 izone `"{\\bot}" ezone
115
116 dform math_False_df2 : except_mode[tex] :: math_false =
117 it["False"]
118
119 (************************************************************************
120 * UNIT
121 ************************************************************************)
122
123 declare math_unit
124 declare math_true
125 declare math_it
126
127 dform math_Unit_df1 : math_unit =
128 math_i["Unit"]
129
130 dform math_True_df1 : mode[tex] :: math_true =
131 izone `"{\\top}" ezone
132
133 dform math_True_df2 : except_mode[tex] :: math_true =
134 it["True"]
135
136 dform math_it_df1 : mode[tex] :: math_it =
137 izone `"\\cdot " ezone
138
139 dform math_it_df2 : except_mode[tex] :: math_it =
140 Nuprl_font!cdot
141
142 (************************************************************************
143 * ATOM
144 ************************************************************************)
145
146 declare math_atom
147 declare math_token{'t}
148
149 dform math_Atom_df1 : math_atom =
150 math_i["Atom"]
151
152 dform math_token_df1 : math_token{'t} =
153 math_i["token"] `"(" slot{'t} `")"
154
155 (************************************************************************
156 * BOOL
157 ************************************************************************)
158
159 declare math_bool
160 declare math_btrue
161 declare math_bfalse
162 declare math_bor{'a; 'b}
163 declare math_band{'a; 'b}
164 declare math_bimplies{'a; 'b}
165 declare math_bnot{'a}
166 declare math_assert{'t}
167 declare math_if{'a; 'b; 'c}
168
169 dform math_Bool_df1 : math_bool =
170 math_i["Bool"]
171
172 dform math_btrue_df1 : math_btrue =
173 math_i["tt"]
174
175 dform math_bfalse_df1 : math_bfalse =
176 math_i["ff"]
177
178 (************************************************
179 * TeX mode
180 *)
181 dform math_bor_df1 : mode[tex] :: math_bor{'a; 'b} =
182 izone `"{" ezone
183 slot{'a}
184 izone `"\\vee_b " ezone
185 slot{'b}
186 izone `"}" ezone
187
188 dform math_band_df1 : mode[tex] :: math_band{'a; 'b} =
189 izone `"{" ezone
190 slot{'a}
191 izone `"\\wedge_b " ezone
192 slot{'b}
193 izone `"}" ezone
194
195 dform math_bimplies_df1 : mode[tex] :: math_bimplies{'a; 'b} =
196 izone `"{" ezone
197 slot{'a}
198 izone `"\\Rightarrow_b " ezone
199 slot{'b}
200 izone `"}" ezone
201
202 dform math_bnot_df1 : mode[tex] :: math_bnot{'a} =
203 izone `"{\\neg_b " ezone
204 slot{'a}
205 izone `"}" ezone
206
207 dform math_assert_df1 : mode[tex] :: math_assert{'a} =
208 izone `"{\\uparrow " ezone
209 slot{'a}
210 izone `"}" ezone
211
212 dform math_if_df1 : mode[tex] :: math_if{'a; 'b; 'c} =
213 izone `"\\mathop{\\bf if}" ezone
214 szone{'a}
215 izone `"\\mathrel{\\bf then}" ezone
216 szone{'b}
217 izone `"\\mathrel{\\bf else}" ezone
218 szone{'c}
219
220 (************************************************
221 * Normal mode.
222 *)
223 prec prec_bimplies
224 prec prec_bor
225 prec prec_band
226 prec prec_bnot
227 prec prec_assert
228
229 prec prec_bimplies < prec_bor
230 prec prec_bor < prec_band
231 prec prec_band < prec_bnot
232 prec prec_bnot < prec_assert
233
234 dform bor_df : parens :: "prec"[prec_bor] :: except_mode[tex] :: math_bor{'a; 'b} =
235 slot{'a} " " vee subb " " slot{'b}
236
237 dform band_df : parens :: "prec"[prec_band] :: except_mode[tex] :: math_band{'a; 'b} =
238 slot{'a} " " wedge subb " " slot{'b}
239
240 dform bimplies_df : parens :: "prec"[prec_bimplies] :: except_mode[tex] :: math_bimplies{'a; 'b} =
241 slot{'a} " " Rightarrow subb " " slot{'b}
242
243 dform bnot_df : parens :: "prec"[prec_bnot] :: except_mode[tex] :: math_bnot{'a} =
244 tneg subb slot{'a}
245
246 dform ifthenelse_df : parens :: "prec"[prec_bor] :: except_mode[tex] :: math_if{'e1; 'e2; 'e3} =
247 szone pushm[0] pushm[3] `"if" `" " szone{'e1} `" " `"then" hspace
248 szone{'e2} popm hspace
249 pushm[3] `"else" hspace szone{'e3} popm popm ezone
250
251 dform assert_df : parens :: "prec"[prec_assert] :: except_mode[tex] :: math_assert{'t} =
252 downarrow slot{'t}
253
254 (************************************************************************
255 * INTEGERS
256 ************************************************************************)
257
258 declare math_int
259 declare math_number{'n}
260 declare math_ind{'i; 'm; 'z; 'down; 'base; 'm; 'z; 'up}
261 declare math_add{'a; 'b}
262 declare math_sub{'a; 'b}
263 declare math_mul{'a; 'b}
264 declare math_div{'a; 'b}
265 declare math_rem{'a; 'b}
266 declare math_lt{'a; 'b}
267 declare math_le{'a; 'b}
268 declare math_ge{'a; 'b}
269 declare math_gt{'a; 'b}
270
271 dform math_int_df1 : mode[tex] :: math_int =
272 izone `"{\\mathbb Z}" ezone
273
274 dform math_number_df1 : mode[tex] :: math_number{'i} =
275 izone `"{{\\it number}[" ezone
276 slot{'i}
277 izone `"]}" ezone
278
279 dform math_ind_df1 : mode[tex] :: math_ind{'i; 'a; 'b; 'down; 'base; 'c; 'd; 'up} =
280 izone `"{{\\it ind}(" ezone
281 slot{'i}
282 izone `"; " ezone
283 slot{'a}
284 izone `", " ezone
285 slot{'b}
286 izone `". " ezone
287 slot{'down}
288 izone `"; " ezone
289 slot{'base}
290 izone `"; " ezone
291 slot{'c}
292 izone `", " ezone
293 slot{'c}
294 izone `". " ezone
295 slot{'up}
296 izone `")}" ezone
297
298 dform math_add_df1 : mode[tex] :: math_add{'i; 'j} =
299 izone `"{" ezone
300 slot{'i}
301 izone `"+" ezone
302 slot{'j}
303 izone `"}" ezone
304
305 dform math_sub_df1 : mode[tex] :: math_sub{'i; 'j} =
306 izone `"{" ezone
307 slot{'i}
308 izone `"-" ezone
309 slot{'j}
310 izone `"}" ezone
311
312 dform math_mul_df1 : mode[tex] :: math_mul{'i; 'j} =
313 izone `"{" ezone
314 slot{'i}
315 izone `"*" ezone
316 slot{'j}
317 izone `"}" ezone
318
319 dform math_div_df1 : mode[tex] :: math_div{'i; 'j} =
320 izone `"{" ezone
321 slot{'i}
322 izone `"/" ezone
323 slot{'j}
324 izone `"}" ezone
325
326 dform math_rem_df1 : mode[tex] :: math_rem{'i; 'j} =
327 izone `"{" ezone
328 slot{'i}
329 izone `"\\mathrel{\\bf rem}" ezone
330 slot{'j}
331 izone `"}" ezone
332
333 dform math_gt_df1 : mode[tex] :: math_gt{'i; 'j} =
334 izone `"{" ezone
335 slot{'i}
336 izone `">" ezone
337 slot{'j}
338 izone `"}" ezone
339
340 dform math_ge_df1 : mode[tex] :: math_ge{'i; 'j} =
341 izone `"{" ezone
342 slot{'i}
343 izone `"\\ge " ezone
344 slot{'j}
345 izone `"}" ezone
346
347 dform math_lt_df1 : mode[tex] :: math_lt{'i; 'j} =
348 izone `"{" ezone
349 slot{'i}
350 izone `"<" ezone
351 slot{'j}
352 izone `"}" ezone
353
354 dform math_le_df1 : mode[tex] :: math_le{'i; 'j} =
355 izone `"{" ezone
356 slot{'i}
357 izone `"\\le " ezone
358 slot{'j}
359 izone `"}" ezone
360
361 (************************************************
362 * Normal mode
363 *)
364
365 prec prec_compare
366 prec prec_add
367 prec prec_mul
368
369 dform int_prl_df : except_mode [doc] :: math_int = mathbbZ
370
371 dform number_df : except_mode[tex] :: math_number{'n} =
372 slot{'n}
373
374 dform add_df1 : except_mode[tex] :: parens :: "prec"[prec_add] :: math_add{'a; 'b} =
375 slot["le"]{'a} `" + " slot["lt"]{'b}
376
377 dform sub_df1 : except_mode[tex] :: parens :: "prec"[prec_add] :: math_sub{'a; 'b} =
378 slot["lt"]{'a} `" - " slot["le"]{'b}
379
380 dform mul_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_mul{'a; 'b} =
381 slot["lt"]{'a} `" * " slot["le"]{'b}
382
383 dform div_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_div{'a; 'b} =
384 slot["lt"]{'a} Nuprl_font!"div" slot["le"]{'b}
385
386 dform rem_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_rem{'a; 'b} =
387 slot["lt"]{'a} `" % " slot["le"]{'b}
388
389 dform lt_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_lt{'a; 'b} =
390 slot["lt"]{'a} `" < " slot["le"]{'b}
391
392 dform le_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_le{'a; 'b} =
393 slot["lt"]{'a} Nuprl_font!le slot["le"]{'b}
394
395 dform ge_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_ge{'a; 'b} =
396 slot["lt"]{'a} Nuprl_font!ge slot["le"]{'b}
397
398 dform gt_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_gt{'a; 'b} =
399 slot["lt"]{'a} `" > " slot["le"]{'b}
400
401 (************************************************************************
402 * UNION
403 ************************************************************************)
404
405 declare math_union{'A; 'B}
406 declare math_inl{'x}
407 declare math_inr{'x}
408 declare math_decide{'x; 'y; 'a; 'z; 'b}
409 declare math_or{'a; 'b}
410 declare math_cor{'a; 'b}
411
412 (************************************************
413 * TeX mode
414 *)
415 dform math_union_df1 : mode[tex] :: math_union{'A; 'B} =
416 izone `"{" ezone
417 slot{'A}
418 izone `"+" ezone
419 slot{'B}
420 izone `"}" ezone
421
422 dform math_inl_df1 : mode[tex] :: math_inl{'x} =
423 izone `"{{\\it inl}(" ezone
424 slot{'x}
425 izone `")}" ezone
426
427 dform math_inr_df1 : mode[tex] :: math_inr{'x} =
428 izone `"{{\\it inr}(" ezone
429 slot{'x}
430 izone `")}" ezone
431
432 dform math_decide_df1 : mode[tex] :: math_decide{'x; 'y; 'a; 'z; 'b} =
433 izone `"{\\mathop{\\bf match}" ezone
434 slot{'x}
435 izone `"\\mathrel{\\bf with}" ezone
436 math_inl{'y}
437 izone `"\\rightarrow " ezone
438 slot{'a}
439 izone `"\\mathrel{|} " ezone
440 math_inr{'z}
441 izone `"\\rightarrow " ezone
442 slot{'b}
443 izone `"}" ezone
444
445 dform math_or_df1 : mode[tex] :: math_or{'a; 'b} =
446 izone `"{" ezone
447 slot{'a}
448 izone `"\\vee " ezone
449 slot{'b}
450 izone `"}" ezone
451
452 dform math_cor_df1 : mode[tex] :: math_cor{'a; 'b} =
453 izone `"{" ezone
454 slot{'a}
455 izone `"\\vee_c " ezone
456 slot{'b}
457 izone `"}" ezone
458
459 (************************************************
460 * Normal display.
461 *)
462 prec prec_inl
463 prec prec_union
464 prec prec_or
465
466 dform union_df : except_mode[tex] :: parens :: "prec"[prec_union] :: math_union{'A; 'B} =
467 slot{'A} " " `"+" " " slot{'B}
468
469 dform inl_df : except_mode[tex] :: parens :: "prec"[prec_inl] :: math_inl{'a} =
470 `"inl" " " slot{'a}
471
472 dform inr_df : except_mode[tex] :: parens :: "prec"[prec_inl] :: math_inr{'a} =
473 `"inr" " " slot{'a}
474
475 dform decide_df : except_mode[tex] :: math_decide{'x; 'y; 'a; 'z; 'b} =
476 szone pushm[0] pushm[3] `"match" " " slot{'x} " " `"with" hspace
477 `"inl " slot{'y} `" -> " slot{'a} popm hspace
478 pushm[3] `" | inr " slot{'z} `" -> " slot{'b} popm popm ezone
479
480 declare or_df{'a}
481
482 dform or_df1 : parens :: "prec"[prec_or] :: math_or{'a; 'b} =
483 szone pushm[0] slot["le"]{'a} or_df{'b} popm ezone
484
485 dform or_df2 : or_df{math_or{'a; 'b}} =
486 or_df{'a} or_df{'b}
487
488 dform or_df3 : or_df{'a} =
489 hspace Nuprl_font!vee " " slot{'a}
490
491 declare cor_df{'a}
492
493 dform cor_df1 : except_mode[tex] :: parens :: "prec"[prec_or] :: math_cor{'a; 'b} =
494 szone pushm[0] slot["le"]{'a} cor_df{'b} popm ezone
495
496 dform cor_df2 : cor_df{math_cor{'a; 'b}} =
497 cor_df{'a} cor_df{'b}
498
499 dform cor_df3 : cor_df{'a} =
500 hspace Nuprl_font!vee `"c" " " slot{'a}
501
502 (************************************************************************
503 * FUNCTIONS
504 ************************************************************************)
505
506 declare math_rfun{'f; 'x; 'A; 'B}
507 declare math_fun{'x; 'A; 'B}
508 declare math_fun{'A; 'B}
509 declare math_lambda{'v; 'b}
510 declare math_apply{'f; 'a}
511 declare math_well_founded{'A; 'x; 'y; 'R}
512 declare math_well_founded_assum{'A; 'a1; 'a2; 'R; 'P}
513 declare math_well_founded_prop{'A}
514 declare math_well_founded_apply{'P; 'a}
515 declare math_fix{'f; 'b}
516
517 declare math_all{'x; 'A; 'B}
518 declare math_implies{'A; 'B}
519 declare math_iff{'A; 'B}
520 declare math_not{'A}
521
522 (************************************************
523 * TeX mode
524 *)
525 dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
526 izone `"{\\left\\{"
527 'f
528 izone `"\\mathrel{|}" ezone
529 'x
530 izone `"\\colon " ezone
531 'A
532 izone `"\\rightarrow " ezone
533 'B
534 izone `"\\right\\}}" ezone
535
536 dform math_dfun_df1 : mode[tex] :: math_fun{'x; 'A; 'B} =
537 izone `"{" ezone
538 'x
539 izone `"\\colon " ezone
540 'A
541 izone `"\\rightarrow " ezone
542 'B
543 izone `"}" ezone
544
545 dform math_fun_df1 : mode[tex] :: math_fun{'A; 'B} =
546 izone `"{" ezone
547 'A
548 izone `"\\rightarrow " ezone
549 'B
550 izone `"}" ezone
551
552 dform math_lambda_df1 : mode[tex] :: math_lambda{'v; 'b} =
553 izone `"{\\lambda " ezone
554 'v
555 izone `"." ezone
556 'b
557 izone `"}" ezone
558
559 dform math_lambda_df1 : mode[tex] :: math_lambda =
560 izone `"\\lambda " ezone
561
562 dform math_apply_df1 : mode[tex] :: math_apply{'f; 'a} =
563 izone `"{" ezone
564 'f
565 izone `"\\ " ezone
566 'a
567 izone `"}" ezone
568
569 dform math_well_founded_df1 : mode[tex] :: math_well_founded{'A; 'x; 'y; 'R} =
570 izone `"{{\\it well\\_founded}(" ezone
571 'A
572 izone `";" ezone
573 'x
574 izone `"," ezone
575 'y
576 izone `"." ezone
577 'R
578 izone `")}" ezone
579
580 dform math_well_founded_assum_df1 : mode[tex] :: math_well_founded_assum{'A; 'x; 'y; 'R; 'P} =
581 izone `"{{\\it well\\_founded\\_assum}(" ezone
582 'A
583 izone `";" ezone
584 'x
585 izone `"," ezone
586 'y
587 izone `"." ezone
588 'R
589 izone `";" ezone
590 'P
591 izone `")}" ezone
592
593 dform math_well_founded_prop_df1 : mode[tex] :: math_well_founded_prop{'P} =
594 izone `"{{\\it well\\_founded\\_prop}(" ezone
595 'P
596 izone `")}" ezone
597
598 dform math_well_founded_apply_df1 : mode[tex] :: math_well_founded_apply{'P; 'a} =
599 izone `"{{\\it well\\_founded\\_apply}(" ezone
600 'P
601 izone `";" ezone
602 'a
603 izone `")}" ezone
604
605 dform math_fix_df1 : mode[tex] :: math_fix{'f; 'b} =
606 izone `"{{\\it fix}(" ezone
607 'f
608 izone `"." ezone
609 'b
610 izone `")}" ezone
611
612 dform math_all_df1 : mode[tex] :: math_all{'x; 'A; 'B} =
613 izone `"{\\forall " ezone
614 'x
615 izone `"\\colon " ezone
616 'A
617 izone `"." ezone
618 'B
619 izone `"}" ezone
620
621 dform math_implies_df1 : mode[tex] :: math_implies{'A; 'B} =
622 izone `"{" ezone
623 'A
624 izone `"\\Rightarrow " ezone
625 'B
626 izone `"}" ezone
627
628 dform math_iff_df1 : mode[tex] :: math_iff{'A; 'B} =
629 izone `"{" ezone
630 'A
631 izone `"\\Leftrightarrow " ezone
632 'B
633 izone `"}" ezone
634
635 dform math_not_df1 : mode[tex] :: math_not{'A} =
636 izone `"{\\neg " ezone
637 'A
638 izone `"}" ezone
639
640 (************************************************
641 * Normal mode.
642 *)
643 prec prec_fun
644 prec prec_apply
645 prec prec_lambda
646 prec prec_lambda < prec_apply
647 prec prec_fun < prec_apply
648 prec prec_fun < prec_lambda
649
650 prec prec_not
651 prec prec_quant
652 prec prec_iff
653 prec prec_implies
654
655 dform fun_df1 : parens :: "prec"[prec_fun] :: except_mode[tex] :: math_fun{'A; 'B} =
656 slot["le"]{'A} " " rightarrow " " slot["lt"]{'B}
657
658 dform fun_df2 : parens :: "prec"[prec_fun] :: except_mode[tex] :: math_fun{'x; 'A; 'B} =
659 slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'B}
660
661 dform fun_df3 : except_mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
662 "{" " " slot{bvar{'f}} `" | " math_fun{'x; 'A; 'B} `" }"
663
664 dform apply_df1 : parens :: "prec"[prec_apply] :: except_mode[tex] :: math_apply{'f; 'a} =
665 slot["lt"]{'f} " " slot["le"]{'a}
666
667 dform lambda_df1 : parens :: "prec"[prec_lambda] :: except_mode[tex] :: math_lambda{'x; 'b} =
668 Nuprl_font!lambda slot{'x} `"." slot{'b}
669
670 dform fix_df1 : except_mode[tex] :: except_mode[tex] :: math_fix{'f; 'b} =
671 `"fix" `"(" slot{'f} `"." slot{'b} `")"
672
673 dform well_founded_prop_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_prop{'A} =
674 `"WellFounded " slot{'A} " " rightarrow `" Prop"
675
676 dform well_founded_apply_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_apply{'P; 'a} =
677 slot{'P} `"[" slot{'a} `"]"
678
679 dform well_founded_assum_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_assum{'A; 'a1; 'a2; 'R; 'P} =
680 szone pushm[3] `"WellFounded " Nuprl_font!forall slot{'a2} `":" slot{'A} `"."
681 `"(" Nuprl_font!forall slot{'a1} `":" slot{'A} `". " slot{'R} " " Rightarrow math_well_founded_apply{'P; 'a1} `")"
682 Rightarrow math_well_founded_apply{'P; 'a2} popm ezone
683
684 dform well_founded_df : except_mode[tex] :: except_mode[tex] :: math_well_founded{'A; 'a; 'b; 'R} =
685 szone pushm[3] `"WellFounded " slot{'a} `"," slot{'b} `":" slot{'A} `"." slot{'R} popm ezone
686
687 (*
688 * Quantifiers.
689 *)
690 dform not_df1 : except_mode[tex] :: parens :: "prec"[prec_not] :: math_not{'a} =
691 Nuprl_font!tneg slot["le"]{'a}
692
693 dform implies_df : except_mode[tex] :: parens :: "prec"[prec_implies] :: math_implies{'a; 'b} =
694 slot["le"]{'a} " " Nuprl_font!Rightarrow " " slot["lt"]{'b}
695
696 dform iff_df : except_mode[tex] :: parens :: "prec"[prec_iff] :: math_iff{'a; 'b} =
697 slot["le"]{'a} " " Nuprl_font!Leftrightarrow " " slot["lt"]{'b}
698
699 dform all_df1 : except_mode[tex] :: parens :: "prec"[prec_quant] :: except_mode[tex] :: math_all{'x; 'A; 'B} =
700 pushm[3] Nuprl_font!forall slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
701
702 (************************************************************************
703 * PRODUCT
704 ************************************************************************)
705
706 declare math_prod{'x; 'A; 'B}
707 declare math_prod{'A; 'B}
708 declare math_pair{'a; 'b}
709 declare math_spread{'e; 'u; 'v; 'b}
710 declare math_fst{'e}
711 declare math_snd{'e}
712 declare math_and{'a; 'b}
713 declare math_cand{'a; 'b}
714 declare math_exists{'x; 'A; 'B}
715
716 (************************************************
717 * TeX mode.
718 *)
719 dform math_prod_df1 : mode[tex] :: math_prod{'x; 'A; 'B} =
720 izone `"{" ezone
721 slot{'x}
722 izone `"\\colon " ezone
723 slot{'A}
724 izone `"\\times " ezone
725 slot{'B}
726 izone `"}" ezone
727
728 dform math_prod_df2 : mode[tex] :: math_prod{'A; 'B} =
729 izone `"{" ezone
730 slot{'A}
731 izone `"\\times " ezone
732 slot{'B}
733 izone `"}" ezone
734
735 dform math_pair_df1 : mode[tex] :: math_pair{'a; 'b} =
736 izone `"{(" ezone
737 slot{'a}
738 izone `", " ezone
739 slot{'b}
740 izone `")}" ezone
741
742 dform math_spread_df1 : mode[tex] :: math_spread{'e; 'u; 'v; 'b} =
743 izone `"{\\mathop{{\\bf match}}" ezone
744 slot{'e}
745 izone `"\\mathrel{{\\bf with}}" ezone
746 math_pair{'u; 'v}
747 izone `"\\rightarrow " ezone
748 slot{'b}
749 izone `"}" ezone
750
751 dform math_fst_df1 : mode[tex] :: math_fst{'e} =
752 izone `"{{\\it fst}(" ezone
753 slot{'e}
754 izone `")}" ezone
755
756 dform math_snd_df1 : mode[tex] :: math_snd{'e} =
757 izone `"{{\\it snd}(" ezone
758 slot{'e}
759 izone `")}" ezone
760
761 dform math_and_df1 : mode[tex] :: math_and{'a; 'b} =
762 izone `"{" ezone
763 slot{'a}
764 izone `"\\wedge " ezone
765 slot{'b}
766 izone `"}" ezone
767
768 dform math_cand_df1 : mode[tex] :: math_cand{'a; 'b} =
769 izone `"{" ezone
770 slot{'a}
771 izone `"\\wedge_c " ezone
772 slot{'b}
773 izone `"}" ezone
774
775 dform math_exists_df1 : mode[tex] :: math_exists{'x; 'A; 'B} =
776 izone `"{\\exists " ezone
777 slot{'x}
778 izone `"\\colon " ezone
779 slot{'A}
780 izone `"." ezone
781 slot{'B}
782 izone `"}" ezone
783
784 dform math_exists_df1 : mode[tex] :: math_exists =
785 izone `"\\exists " ezone
786
787 (************************************************
788 * NORMAL MODE
789 *)
790 prec prec_prod
791 prec prec_spread
792 prec prec_and
793
794 prec prec_implies < prec_iff
795 prec prec_iff < prec_or
796 prec prec_or < prec_and
797 prec prec_and < prec_not
798 prec prec_quant < prec_iff
799
800 dform prod_df : parens :: "prec"[prec_prod] :: except_mode[tex] :: math_prod{'A; 'B} =
801 pushm[0] slot{'A} " " times " " slot{'B} popm
802
803 dform prod_df2 : parens :: "prec"[prec_prod] :: except_mode[tex] :: math_prod{'x; 'A; 'B} =
804 slot{'x} `":" slot{'A} " " times " " slot{'B}
805
806 dform pair_prl_df : except_mode[tex] :: except_mode[tex] :: math_pair{'a; 'b} =
807 pushm[0] `"(" slot{'a}`"," slot{'b} `")" popm
808
809 dform spread_prl_df1 : parens :: "prec"[prec_spread] :: except_mode[tex] :: except_mode[tex] :: math_spread{'e; 'u; 'v; 'b} =
810 szone pushm[1]
811 keyword["match"] `" " slot{'e} `" " keyword["with"] hspace
812 math_pair{'u; 'v} `" " Nuprl_font!rightarrow hspace
813 slot{'b}
814 popm ezone
815
816 dform fst_df1 : except_mode[tex] :: except_mode[tex] :: math_fst{'e} =
817 slot{'e} `".1"
818
819 dform snd_df1 : except_mode[tex] :: except_mode[tex] :: math_snd{'e} =
820 slot{'e} `".2"
821
822 declare and_df{'a}
823
824 dform and_df1 : except_mode[tex] :: parens :: "prec"[prec_and] :: math_and{'a; 'b} =
825 szone pushm[0] slot["le"]{'a} and_df{'b} popm ezone
826
827 dform and_df2 : and_df{math_and{'a; 'b}} =
828 and_df{'a} and_df{'b}
829
830 dform and_df3 : and_df{'a} =
831 hspace Nuprl_font!wedge " " slot{'a}
832
833 declare cand_df{'a}
834
835 dform cand_df1 : except_mode[tex] :: parens :: "prec"[prec_and] :: math_cand{'a; 'b} =
836 szone pushm[0] slot["le"]{'a} cand_df{'b} popm ezone
837
838 dform cand_df2 : and_df{math_cand{'a; 'b}} =
839 cand_df{'a} cand_df{'b}
840
841 dform cand_df3 : cand_df{'a} =
842 hspace Nuprl_font!wedge `"c" " " slot{'a}
843
844 dform exists_df1 : except_mode[tex] :: parens :: "prec"[prec_quant] :: except_mode[tex] :: math_exists{'x; 'A; 'B} =
845 pushm[3] Nuprl_font!"exists" slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
846
847 (************************************************************************
848 * SET TYPE
849 ************************************************************************)
850
851 declare math_set{'x; 'A; 'B}
852 declare math_squash{'A}
853
854 (************************************************
855 * TeX mode
856 *)
857
858 dform math_set_df1 : mode[tex] :: math_set{'x; 'A; 'B} =
859 izone `"{\\left\\{" ezone
860 slot{'x}
861 izone `"\\colon " ezone
862 slot{'A}
863 izone `"\\mathrel{|} " ezone
864 slot{'B}
865 izone `"\\right\\}}" ezone
866
867 dform math_squash_df1 : mode[tex] :: math_squash{'A} =
868 izone `"\\sq{" ezone
869 slot{'A}
870 izone `"}" ezone
871
872 (************************************************
873 * Normal mode
874 *)
875 dform set_df1 : except_mode[tex] :: math_set{'x; 'A; 'B} =
876 pushm[3] `"{ " bvar{'x} `":" slot{'A} `" | " slot{'B} `"}" popm
877
878 dform math_squash_df2 : except_mode[tex] :: math_squash{'A} = "[" 'A "]"
879
880 (************************************************************************
881 * Decidable
882 ************************************************************************)
883
884 declare math_decidable{'P}
885
886 (************************************************
887 * TeX mode
888 *)
889
890 dform math_decidable_df1 : mode[tex] :: math_decidable{'P} =
891 izone `"{{\\it decidable}(" ezone
892 slot{'P}
893 izone `")}" ezone
894
895 (************************************************
896 * Normal mode
897 *)
898 dform decidable_df1 : except_mode[tex] :: math_decidable{'A} =
899 `"decidable(" slot{'A} `")"
900
901 (************************************************************************
902 * INTERSECTION
903 ************************************************************************)
904
905 declare math_isect{'x; 'A; 'B}
906 declare math_top
907 declare math_record{'t}
908 declare math_bisect{'A; 'B}
909
910 (************************************************
911 * TeX mode
912 *)
913
914 dform math_isect_df1 : mode[tex] :: math_isect{'x; 'A; 'B} =
915 izone `"{\\bigcap_{" ezone
916 slot{'x}
917 izone `"\\colon " ezone
918 slot{'A}
919 izone `"} " ezone
920 slot{'B}
921 izone `"}" ezone
922
923 dform math_record_df1 : mode[tex] :: math_record{'t} =
924 izone `"{\\left\\{" ezone
925 slot{'t}
926 izone `"\\right\\}}" ezone
927
928 dform math_bisect_df1 : mode[tex] :: math_bisect{'A; 'B} =
929 izone `"{" ezone
930 slot{'A}
931 izone `"\\cap " ezone
932 slot{'B}
933 izone `"}" ezone
934
935 (************************************************
936 * Normal mode
937 *)
938 dform isect_df1 : except_mode[tex] :: math_isect{'x; 'A; 'B} =
939 cap slot{'x} `":" slot{'A} `"." slot{'B}
940
941 dform top_df : math_top =
942 math_i["Top"]
943
944 dform record_df : except_mode[tex] :: math_record{'t} =
945 pushm[0] szone `"{ " pushm[0] 't popm hspace `"}" ezone popm
946
947 prec prec_bisect
948
949 dform bisect_df : except_mode[tex] :: parens :: "prec"[prec_bisect] :: math_bisect{'A; 'B} =
950 slot["le"]{'A} `" " cap space slot{'B}
951
952 (************************************************************************
953 * UNION
954 ************************************************************************)
955
956 declare math_tunion{'x; 'A; 'B}
957 declare math_bunion{'A; 'B}
958
959 (************************************************
960 * TeX mode
961 *)
962
963 dform math_tunion_df1 : mode[tex] :: math_tunion{'x; 'A; 'B} =
964 izone `"{\\bigcup_{" ezone
965 slot{'x}
966 izone `"\\colon " ezone
967 slot{'A}
968 izone `"} " ezone
969 slot{'B}
970 izone `"}" ezone
971
972 dform math_bunion_df1 : mode[tex] :: math_bunion{'A; 'B} =
973 izone `"{" ezone
974 slot{'A}
975 izone `"\\cup " ezone
976 slot{'B}
977 izone `"}" ezone
978
979 (************************************************
980 * Normal mode
981 *)
982 dform tunion_df1 : except_mode[tex] :: math_tunion{'x; 'A; 'B} =
983 cup slot{'x} `":" slot{'A} `"." slot{'B}
984
985 prec prec_bunion
986
987 dform bunion_df : except_mode[tex] :: parens :: "prec"[prec_bunion] :: math_bunion{'A; 'B} =
988 slot["le"]{'A} `" " cup space slot{'B}
989
990 (************************************************************************
991 * RECURSIVE TYPES
992 ************************************************************************)
993
994 declare math_srec{'T; 'B}
995 declare math_prec{'T; 'y; 'B; 'a}
996 declare math_srecind{'t; 'a; 'b; 'c}
997 declare math_precind{'t; 'a; 'b; 'c}
998
999 declare math_w{'x; 'A; 'B}
1000 declare math_tree{'a; 'f}
1001 declare math_treeind{'z; 'a; 'f; 'g; 'body}
1002
1003 declare math_nil
1004 declare math_cons{'a; 'b}
1005 declare math_list{'l}
1006 declare math_listind{'e; 'base; 'h; 't; 'f; 'step}
1007
1008 (************************************************
1009 * TeX mode
1010 *)
1011 dform math_srec_df1 : mode[tex] :: math_srec{'T; 'B} =
1012 izone `"{\\mu(" ezone
1013 slot{'T}
1014 izone `"." ezone
1015 slot{'B}
1016 izone `")}" ezone
1017
1018 dform math_srecind_df1 : mode[tex] :: math_srecind{'t; 'a; 'b; 'c} =
1019 izone `"{{\\it srec\\_ind}(" ezone
1020 slot{'t}
1021 izone `";" ezone
1022 slot{'a}
1023 izone `"," ezone
1024 slot{'b}
1025 izone `"." ezone
1026 slot{'c}
1027 izone `")}" ezone
1028
1029 dform math_prec_df1 : mode[tex] :: math_prec{'T; 'x; 'B; 'a} =
1030 izone `"{\\mu(" ezone
1031 slot{'T}
1032 izone `"," ezone
1033 slot{'x}
1034 izone `"." ezone
1035 slot{'B}
1036 izone `";" ezone
1037 slot{'a}
1038 izone `")}" ezone
1039
1040 dform math_precind_df1 : mode[tex] :: math_precind{'t; 'a; 'b; 'c} =
1041 izone `"{{\\it prec\\_ind}(" ezone
1042 slot{'t}
1043 izone `";" ezone
1044 slot{'a}
1045 izone `"," ezone
1046 slot{'b}
1047 izone `"." ezone
1048 slot{'c}
1049 izone `")}" ezone
1050
1051 dform math_w_df1 : mode[tex] :: math_w{'x; 'A; 'B} =
1052 izone `"{\\mathop{\\it W}(" ezone
1053 slot{'x}
1054 izone `"\\colon " ezone
1055 slot{'A}
1056 izone `"." ezone
1057 slot{'B}
1058 izone `")}" ezone
1059
1060 dform math_tree_df1 : mode[tex] :: math_tree{'A; 'B} =
1061 izone `"{{\\it tree}(" ezone
1062 slot{'A}
1063 izone `";" ezone
1064 slot{'B}
1065 izone `")}" ezone
1066
1067 dform math_treeind_df1 : mode[tex] :: math_treeind{'t; 'a; 'b; 'c; 'd} =
1068 izone `"{{\\it prec\\_ind}(" ezone
1069 slot{'t}
1070 izone `";" ezone
1071 slot{'a}
1072 izone `"," ezone
1073 slot{'b}
1074 izone `"," ezone
1075 slot{'c}
1076 izone `"." ezone
1077 slot{'d}
1078 izone `")}" ezone
1079
1080 dform math_nil_df1 : mode[tex] :: math_nil =
1081 izone `"{\\it nil}" ezone
1082
1083 dform math_cons_df1 : mode[tex] :: math_cons{'h; 't} =
1084 izone `"{{\\it cons}(" ezone
1085 slot{'h}
1086 izone `"," ezone
1087 slot{'t}
1088 izone `")}" ezone
1089
1090 dform math_list_df1 : mode[tex] :: math_list{'l} =
1091 izone `"{{\\it list}(" ezone
1092 slot{'l}
1093 izone `")}" ezone
1094
1095 dform math_listind_df1 : mode[tex] :: math_listind{'e; 'base; 'h; 't; 'f; 'step} =
1096 izone `"{\\mathop{\\bf match}" ezone
1097 slot{'e}
1098 izone `"\\mathrel{\\bf with}" ezone
1099 math_cons{'h; 't}
1100 izone `"." ezone
1101 slot{'f}
1102 izone `"\\rightarrow " ezone
1103 slot{'step}
1104 izone `"}" ezone
1105
1106 (************************************************
1107 * Normal mode
1108 *)
1109 dform srec_df : except_mode[tex] :: math_srec{'T; 'B} =
1110 szone mu `"{" slot{'T} `"." pushm[0] slot{'B} `"}" popm ezone
1111
1112 prec prec_w
1113 prec prec_tree_ind
1114
1115 dform w_df : except_mode[tex] :: parens :: "prec"[prec_w] :: math_w{'x; 'A; 'B} =
1116 mathbbW slot{'x} `":" slot{'A} `"." slot{'B}
1117
1118 dform tree_df : except_mode[tex] :: math_tree{'a; 'f} =
1119 `"tree(" slot{'a} `"," " " slot{'f} `")"
1120
1121 dform tree_ind_df : except_mode[tex] :: parens :: "prec"[prec_tree_ind] :: math_treeind{'z; 'a; 'f; 'g; 'body} =
1122 szone pushm[3] `"tree_ind(" slot{'g} `"." " "
1123 pushm[3] `"let tree(" slot{'a} `", " slot{'f} `") =" space slot{'z} space `"in" popm space
1124 slot{'body} popm ezone
1125
1126 prec prec_cons
1127 prec prec_list
1128
1129 declare search{'a; 'b}
1130 declare semicolons{'a}
1131 declare colons{'a}
1132
1133 (* Empty list *)
1134 dform nil_df : except_mode[tex] :: math_nil = `"[]"
1135
1136 (* Search for nil entry *)
1137 dform cons_df : except_mode[tex] :: math_cons{'a; 'b} =
1138 search{math_cons{'a; math_nil}; 'b}
1139
1140 (* Keep searching down the list *)
1141 dform search_df1 : search{'a; math_cons{'b; 'c}} =
1142 search{math_cons{'b; 'a}; 'c}
1143
1144 (* Found a nil terminator: use bracket notation *)
1145 dform search_df2 : search{'a; math_nil} =
1146 `"[" semicolons{'a} `"]"
1147
1148 (* No nil terminator, so use :: notation *)
1149 dform search_df3 : search{'a; 'b} =
1150 colons{'a} `"::" slot{'b}
1151
1152 (* Reverse entries and separate with ; *)
1153 dform semicolons_df1 : semicolons{math_cons{'a; math_nil}} =
1154 slot{'a}
1155
1156 dform semicolons_df2 : semicolons{math_cons{'a; 'b}} =
1157 semicolons{'b} `";" slot{'a}
1158
1159 (* Reverse entries and separate with :: *)
1160 dform colons_df1 : colons{math_cons{'a; math_nil}} =
1161 slot{'a}
1162
1163 dform colons_df2 : colons{math_cons{'a; 'b}} =
1164 colons{'b} `"::" slot{'a}
1165
1166 dform list_df1 : except_mode[tex] :: parens :: "prec"[prec_list] :: math_list{'a} =
1167 slot{'a} `" List"
1168
1169 dform list_ind_df1 : except_mode[tex] :: parens :: "prec"[prec_list] :: math_listind{'e; 'base; 'h; 't; 'f; 'step} =
1170 szone pushm[1] pushm[3]
1171 `"match " slot{'e} `" with" hspace
1172 `" [] ->" hspace slot{'base} popm hspace
1173 `"| " pushm[0] slot{'h} `"::" slot{'t} `"." slot{'f} `" ->" hspace slot{'step} popm popm ezone
1174
1175 (************************************************************************
1176 * QUOTIENT TYPE
1177 ************************************************************************)
1178
1179 declare math_quot{'T; 'x; 'y; 'E}
1180 declare math_esquash{'P}
1181
1182 (************************************************
1183 * TeX
1184 *)
1185 dform math_quot_df1 : mode[tex] :: math_quot{'T; 'x; 'y; 'E} =
1186 izone `"{" ezone
1187 slot{'x}
1188 izone `"," ezone
1189 slot{'y}
1190 izone `"\\colon " ezone
1191 slot{'T}
1192 izone `"// " ezone
1193 slot{'E}
1194 izone `"}" ezone
1195
1196 dform math_esquash_df1 : mode[tex] :: math_esquash{'P} =
1197 izone `"[\!" ezone
1198 `"[" slot{'P} `"]"
1199 izone `"\!]" ezone
1200
1201 (************************************************
1202 * Normal mode
1203 *)
1204
1205 prec prec_quot
1206
1207 dform quot_df1 : except_mode[tex] :: parens :: "prec"[prec_quot] :: math_quot{'A; 'x; 'y; 'E} =
1208 slot{'x} `", " slot{'y} `":" " " slot{'A} `" // " slot{'E}
1209
1210 dform math_esquash_df2 : except_mode[tex] :: math_esquash{'P} =
1211 `"[[" slot{'P} `"]]"
1212
1213 (*
1214 * -*-
1215 * Local Variables:
1216 * Caml-master: "compile"
1217 * End:
1218 * -*-
1219 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26