1 {- 2 * kernel for vts90 3 * 4 * Tue Nov 6 14:35:39 GMT 1990 5 * 6 * For information about the typing rules for the construction of 7 * term, signatures, declarations an signatures see the file 8 * doc/abstract_logic/rules3.tex 9 * 10 -} 11 12 13 module Kernel where 14 15 import Core_database 16 17 import Dcore 18 19 import Sub_Core1 20 21 import Sub_Core2 22 23 import Sub_Core3 24 25 import Sub_Core4 26 27 import Vtslib 28 29 import Core_datatype 30 31 {- for tags -- terms and theorems now defined in core_datatype -} 32 33 --data Trm = TM ITrm ITrm ISgn | {- the term, its type, and signature -} 34 -- TM_Err String 35 36 data Sgn = SG ISgn | 37 SG_Err String 38 39 data Dec = DC IDec ISgn | {- the declaration, and its signature -} 40 DC_Err String 41 42 --data Thm = TH ITrm ISgn | {- the theorem, and its signature -} 43 -- TH_Err String 44 45 {- 46 (*and Mph = MP of mapping list*) 47 -} 48 49 {- Symbol formation -} 50 51 symbol (SG sg) i j 52 = if share_map !! i == i 53 then TM (Sym i j [] []) (typ_of_sm sg i j) sg 54 else TM_Err "Malformed symbol" 55 where 56 share_map = get_share_map sg 57 58 59 60 61 62 {- Universe formation -} 63 64 universe (SG sg) i 65 | i>=0 = TM (Constant (Univ i) [] []) (Constant (Univ (i+1)) [] []) sg 66 | i<0 = TM_Err "Malformed Universe" 67 68 69 70 71 72 {- Pi formation -} 73 74 pi' (TM tm (Constant (Univ i) _ _) (Extend dc sg _)) 75 = case typ_of_trm sg (typ_of_dec dc) of 76 Constant (Univ j) _ _ 77 -> TM tm1 tm2 sg 78 where 79 tm1 = Binder Pi dc tm [] [] 80 tm2 = Constant (Univ (max i j)) [] [] 81 _ -> TM_Err "Malformed pi expression" 82 83 pi' _ = TM_Err "Sort of pi exression is not a universe" 84 85 86 87 88 89 {- Pi introduction -} 90 91 lambda (TM tm1 tm2 (Extend dc sg _)) 92 = if is_sym_dec dc 93 then 94 TM (Binder Lambda dc tm1 [] []) (Binder Pi dc tm2 [] []) sg 95 else 96 TM_Err "lambda: invalid declaration" 97 98 lambda (TM_Err mesg ) = TM_Err mesg 99 100 lambda _ = TM_Err "Malformed lambda expression" 101 102 103 104 105 106 {- PI elimination -} 107 108 appl (TM tm1 (Binder Pi dc tm2 _ _) sg1) (TM tm3 tm4 sg2) 109 = if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm4 110 then 111 TM (App tm1 tm3 [] []) (subst_trm dc tm2 tm3) sg1 112 else 113 TM_Err "Malformed application" 114 appl _ _ 115 = TM_Err "Malformed application (2)" 116 117 118 119 120 121 {- Sigma formation -} 122 123 sigma (TM tm (Constant (Univ i) _ _) (Extend dc sg _)) 124 = case typ_of_trm sg (typ_of_dec dc) of 125 Constant (Univ j) _ _ 126 -> TM tm1 tm2 sg 127 where 128 tm1 = Binder Sigma dc tm [] [] 129 tm2 = Constant (Univ (max i j)) [] [] 130 _ -> TM_Err "Malformed sigma" 131 132 sigma _ = TM_Err "Malformed sigma (2)" 133 134 135 136 137 138 {- Sigma introduction -} 139 140 pair (TM tm1 tm2 sg1) (TM tm3 tm4 sg2) (TM tm7@(Binder Sigma dc tm5 _ _) tm6 sg3) 141 = if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 && 142 eq_trm tm2 (typ_of_dec dc) && eq_trm tm4 (subst_trm dc tm5 tm1) 143 then 144 TM (Pair tm1 tm3 tm7 [] []) tm7 sg1 145 else 146 TM_Err "Malformed pair" 147 148 pair _ _ _ = TM_Err "Malformed pair (2)" 149 150 151 152 153 154 {- Subtype formation -} 155 156 subtype (TM tm (Constant Bool' _ _) (Extend dc sg _)) 157 = if eq_trm (typ_of_trm sg (typ_of_dec dc)) (Constant (Univ 0) [] []) 158 then 159 TM (Binder Subtype dc tm [] []) (Constant (Univ 0) [] []) sg 160 else 161 TM_Err "Malformed subtype" 162 163 subtype _ = TM_Err "Malformed subtype (2)" 164 165 166 167 168 169 {- Subtype introduction -} 170 171 into (TM tm1 tm2 sg1) (TM tm3@(Binder Subtype dc tm4 _ _) _ sg2) (TH tm5 sg3) 172 = if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 && 173 eq_trm (typ_of_trm sg2 (typ_of_dec dc)) (Constant (Univ 0) [] []) && 174 eq_trm tm2 (typ_of_dec dc) && eq_trm tm5 (subst_trm dc tm4 tm1) 175 then 176 TM (add_type tm1 tm3) tm3 sg1 177 else 178 TM_Err "Malformed subtype introduction " 179 180 into _ _ _ = TM_Err "Malformed subtype introduction (2)" 181 182 183 184 185 186 {- Subtype elimination -} 187 188 outof (TM tm1 (Binder Subtype dc _ _ _) sg) 189 = TM (add_type tm1 tm2) tm2 sg 190 where 191 tm2 = typ_of_dec dc 192 193 outof _ = TM_Err " outof: argument invalid" 194 195 196 197 198 199 {- Bool formation -} 200 201 bool_sm (SG sg) 202 = TM (Constant Bool' [] []) (Constant (Univ 0) [] []) sg 203 204 205 206 207 208 {- Bool introduction -} 209 210 {- true formation -} 211 212 true_sm (SG sg) = TM (Constant T [] []) (Constant Bool' [] []) sg 213 214 {- false formation -} 215 216 false_sm (SG sg) = TM (Constant F [] []) (Constant Bool' [] []) sg 217 218 219 220 221 222 {- Universal quantification formation -} 223 224 universal (TM tm (Constant Bool' _ _) (Extend dc sg _)) 225 = if is_sym_dec dc 226 then 227 TM (Binder Forall dc tm [] []) (Constant Bool' [] []) sg 228 else 229 TM_Err "Malformed universal quantification" 230 231 universal _ = TM_Err "Malformed universal quantification (2)" 232 233 234 235 236 237 {- Existential quantification formation -} 238 239 existential (TM tm (Constant Bool' _ _) (Extend dc sg _)) 240 = if is_sym_dec dc 241 then 242 TM (Binder Exists dc tm [] []) (Constant Bool' [] []) sg 243 else 244 TM_Err "Malformed existential quantification" 245 246 existential _ = TM_Err "Malformed existential quantification (2)" 247 248 249 250 251 252 {- Implication formation -} 253 254 implication (TM tm (Constant Bool' _ _) (Extend dc sg _)) 255 = if is_axm_dec dc 256 then 257 TM (Binder Imp dc tm [] []) (Constant Bool' [] []) sg 258 else 259 TM_Err "Malformed Implication" 260 261 implication _ = TM_Err "Malformed Implication (2)" 262 263 264 265 266 267 {- And formation -} 268 269 conjunction (TM tm1 (Constant Bool' _ _) sg1) (TM tm2 (Constant Bool' _ _) sg2) 270 = if eq_sgn sg1 sg2 271 then 272 TM (Binary' And tm1 tm2 [] []) (Constant Bool' [] []) sg1 273 else 274 TM_Err "Malformed conjunction" 275 276 conjunction _ _ = TM_Err "Malformed conjunction (2)" 277 278 279 280 281 282 {- Or formation -} 283 284 disjunction (TM tm1 (Constant Bool' _ _) sg1) (TM tm2 (Constant Bool' _ _) sg2) 285 = if eq_sgn sg1 sg2 286 then 287 TM (Binary' Or tm1 tm2 [] []) (Constant Bool' [] []) sg1 288 else 289 TM_Err "Malformed disjunction " 290 291 disjunction _ _ = TM_Err "Malformed disjunction (2)" 292 293 294 295 296 297 {- Not formation -} 298 299 negation (TM tm (Constant Bool' _ _) sg) 300 = TM (Unary Not tm [] []) (Constant Bool' [] []) sg 301 302 negation _ = TM_Err "Malformed negation" 303 304 305 306 307 308 {- Eq formation -} 309 310 equal (TM tm1 _ sg1) (TM tm2 _ sg2) 311 = if eq_sgn sg1 sg2 312 then 313 TM (Binary' Eq' tm1 tm2 [] []) (Constant Bool' [] []) sg1 314 else 315 TM_Err "Malformed equality" 316 317 318 319 320 321 {- Issustype formation -} 322 323 issubtype (TM tm1 (Constant (Univ 0) _ _) sg1) 324 (TM tm2 (Constant (Univ 0) _ _) sg2) 325 = if eq_sgn sg1 sg2 326 then 327 TM (Binary' Issubtype tm1 tm2 [] []) (Constant Bool' [] []) sg1 328 else 329 TM_Err "Malformed subtype" 330 331 issubtype _ _ = TM_Err "Malformed subtype (2)" 332 333 334 335 336 337 {- Bool elimination (ie Conditionals) -} 338 339 conditional (TM tm1 tm2 (Extend dc1 sg1 _)) (TM tm3 tm4 (Extend dc2 sg2 _)) 340 = if eq_sgn sg1 sg2 && 341 eq_trm tm2 tm4 && 342 eq_trm (Unary Not (typ_of_dec dc1) [] []) (typ_of_dec dc2) 343 then 344 TM (Cond dc1 tm1 tm3 [] []) tm2 sg1 345 else 346 TM_Err "Malformed conditional" 347 348 conditional _ _ = TM_Err "Malformed conditional (2)" 349 350 351 352 353 354 {- Hilbert epsilon operator introduction -} 355 356 choose (TH (Binder Exists dc tm _ _) sg) 357 = if eq_trm (typ_of_trm sg (typ_of_dec dc)) (Constant (Univ 0) [] []) 358 then 359 TM (Binder Choose dc tm [] []) (Binder Subtype dc tm [] []) sg 360 else 361 TM_Err "epsilon operator error" 362 363 choose _ = TM_Err "epsilon operator error (2)" 364 365 366 367 368 369 {- Datatype constructor formation and introduction -} 370 371 constructor (SG sg) i j k 372 = if share_map !! i == i 373 then 374 TM (Const i j k [] []) (typ_of_cn sg i j k) sg 375 else 376 TM_Err "Malformed constructor" 377 where 378 share_map = get_share_map sg 379 380 381 382 383 384 {- Datatype elimination -} 385 386 recurse tmL (TM (tm @ (Binder Pi (Symbol_dec tm1 _) _ _ _)) _ sg) 387 = if forall ok (zip tmL tyL) 388 then 389 TM (Recurse (map fst tmL) tm [] []) tm sg 390 else 391 TM_Err "recurse error" 392 where 393 (tyL,_) = clause_types sg tm1 tm 394 ok (TM _ tm1 sg1 , tm2) = eq_sgn sg sg1 && eq_trm tm1 tm2 395 fst (TM tm _ _) = tm 396 397 recurse _ _ = TM_Err "recurse error (2)" 398 399 400 401 402 403 {- Widen type -} 404 405 widen (TM tm1 tm2 sg1) (TH (Binary' Issubtype tm3 tm4 _ _) sg2) 406 = if eq_sgn sg1 sg2 && eq_trm tm2 tm3 407 then 408 TM (add_type tm1 tm4) tm4 sg1 409 else 410 TM_Err "widen: error" 411 412 widen _ _ = TM_Err "widen: error (2)" 413 414 415 416 417 418 {- Set the attributes of a term -} 419 420 set_Trm_att (TM tm1 tm2 sg) iL att 421 = TM (set_trm_att tm1 iL att) tm2 sg 422 423 set_Trm_att (TM_Err mesg) _ _ = TM_Err mesg 424 425 426 427 428 429 {- Get the attributes of a term -} 430 431 get_Trm_att (TM tm _ _) iL 432 = get_trm_att tm iL 433 434 435 436 437 {- return the internal representation of a term -} 438 439 internal_Trm (TM tm1 tm2 sg) = (tm1,tm2,sg) 440 441 442 443 444 445 446 {- Read a term in from the database -} 447 448 restore_Trm s = TM_Err "restore_Trm unimplemented" 449 450 451 452 453 454 {- The empty signature -} 455 456 empty = SG (Empty []) 457 458 459 460 461 462 {- Extend a signature with a declaration -} 463 464 extend (DC dc sg1) (SG sg2) 465 = if eq_sgn sg1 sg2 466 then 467 SG (Extend dc sg2 []) 468 else 469 SG_Err "Malformed signature extension" 470 471 extend _ _ = SG_Err "Invalid declaration in signature" 472 473 474 475 476 477 {- Combine two signatures -} 478 479 combine (SG sg1) (SG sg2) 480 = SG (Combine sg1 sg2 (len_sgn sg2) (sm2 ++ map update sm1) []) 481 where 482 sm1 = get_share_map sg1 483 sm2 = get_share_map sg2 484 offset = length sm2 485 update i = i + offset 486 487 488 489 490 491 {- Share two sub-sigantures within a signature -} 492 493 share (SG sg) i j 494 = if eq_sgn sg1 sg2 495 then 496 SG (Share sg i j (len_sgn sg2) 497 (addequivL i j (len_sgn sg2) sm) []) 498 else 499 SG_Err "sg: Share" 500 where 501 sg1 = nth_sgn i sg 502 sg2 = nth_sgn j sg 503 sm = get_share_map sg 504 505 506 507 508 509 {- Return the attributes of a signature -} 510 511 get_Sgn_att (SG sg) = get_sgn_att sg 512 513 514 515 516 517 {- Set the attributes of a signature -} 518 519 set_Sgn_att (SG sg) att = (SG (set_sgn_att sg att)) 520 521 522 523 524 525 {- Return the internal representation of a signature -} 526 527 internal_Sgn (SG sg) = sg 528 529 530 531 532 533 {- Restore a signature from the database -} 534 535 restore_Sgn s = SG_Err "restore_Sgn unimplemented" 536 537 538 539 540 541 {- declare a new symbol -} 542 543 symbol_dec (TM tm1 tm2 sg) 544 = case typ_of_trm sg tm2 of 545 Constant (Univ _) _ _ -> DC (Symbol_dec tm1 []) sg 546 _ -> DC_Err "Malformed symbol declaration" 547 548 549 550 551 552 {- declare a new axiom -} 553 554 axiom_dec (TM tm (Constant Bool' _ _) sg) 555 = DC (Axiom_dec tm []) sg 556 557 axiom_dec _ = DC_Err "Malformed axiom declaration" 558 559 560 561 562 563 {- Define a new symbol -} 564 565 def (TM tm1 tm2 sg) 566 = DC (Def tm1 tm2 []) sg 567 568 569 570 571 572 make_data tmLL (TH tm sg) 573 = if forall (forall (wf_param sg1)) tmLL 574 then 575 if exists (eq_trm tm) non_empty_thms 576 then 577 DC (Data [] (map (map fst) tmLL) []) sg 578 else 579 DC_Err "Malformed datatype" 580 else 581 DC_Err "Malformed datatype (2)" 582 where 583 non_empty_thms = map gen_proof (filter is_base tmLL) 584 wf_param sg1 (TM tm1 (Constant (Univ _) _ _) sg2) 585 = eq_trm tm1 (Sym 0 0 [] []) || not (occurs 0 tm1) 586 587 wf_param _ _ = False 588 589 mk_exists tm1 tm2 590 = Binder Exists (Symbol_dec tm3 []) tm4 [] [] 591 where 592 tm3 = shift_trm [] (-1) tm1 593 tm4 = shift_trm [] 1 tm2 594 fst (TM tm _ _) = tm 595 is_base tmL = not (exists (eq_trm (Sym 0 0 [] [])) (map fst tmL)) 596 gen_proof tmL = foldr mk_exists (Constant T [] []) 597 ( reverse (map fst tmL)) 598 sg1 = Extend (Symbol_dec (Constant (Univ 0) [] []) []) sg [] 599 600 601 602 603 604 polydata (DC (Data dcL tmLL _) (Extend dc sg _)) 605 = if is_sym_dec dc 606 then 607 DC (Data (dc:dcL) tmLL []) sg 608 else 609 DC_Err "Malformed datatype (polydata)" 610 611 polydata _ = DC_Err "Malformed datatype (polydata 2)" 612 613 614 615 616 617 {- Declaration pair formation -} 618 619 decpair (DC dc1 (Extend dc2 sg _)) 620 = DC (Decpair dc2 dc1 []) sg 621 622 decpair _ = DC_Err "Malformed declaation pair" 623 624 625 626 627 628 {- Get the attributes of a declaration -} 629 630 get_Dec_att (DC dc _) 631 = get_dec_att dc 632 633 634 635 636 637 {- Set the attributes of a declaration -} 638 639 set_Dec_att (DC dc sg) att 640 = DC (set_dec_att dc att) sg 641 642 643 644 645 646 {- Return the internal representation of a declaration -} 647 648 internal_Dec (DC dc sg) = (dc,sg) 649 650 651 652 653 654 {- Restore a declaration from the database -} 655 656 restore_Dec s = error "BadDeclaration" -- ** exn NOT IMPLEMENTED YET 657 658 659 660 661 662 {- Axiom formation -} 663 664 axiom (SG sg) i j 665 = if share_map !! i == i 666 then 667 TH (typ_of_axm sg i j) sg 668 else 669 TH_Err "Malformed Axiom" 670 where 671 share_map = get_share_map sg 672 673 674 675 676 677 {- Forall introduction -} 678 679 generalise (TH tm (Extend dc sg _)) 680 = if is_sym_dec dc 681 then 682 TH (Binder Forall dc tm [] []) sg 683 else 684 TH_Err "Malformed generalisation" 685 686 generalise _ = TH_Err "Malformed generalisation (2)" 687 688 689 690 691 692 {- Forall elimination -} 693 694 specialise (TH (Binder Forall dc tm1 _ _) sg1) (TM tm2 tm3 sg2) 695 = if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm3 696 then 697 TH (subst_trm dc tm1 tm2) sg1 698 else 699 TH_Err "Malformed specialisation" 700 701 specialise _ _ 702 = TH_Err "Malformed specialisation (2)" 703 704 705 706 707 708 {- Exists introduction -} 709 710 exists_intro (TH tm1 sg1) 711 (TM tm5@(Binder Exists dc tm2 _ _) _ sg2) 712 (TM tm3 tm4 sg3) 713 = if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 && 714 eq_trm (typ_of_dec dc) tm4 && eq_trm (subst_trm dc tm2 tm3) tm1 715 then 716 TH tm5 sg2 717 else 718 TH_Err "Malformed existential introduction" 719 720 exists_intro _ _ _ = TH_Err "Malformed existential introduction (2)" 721 722 723 724 725 726 {- Exists elimination -} 727 728 exists_elim (TH (Binder Forall dc1 (Binder Imp dc tm2 _ _) _ _) sg1) 729 (TH (Binder Exists dc2 tm3 _ _) sg2) 730 = if eq_sgn sg1 sg2 && eq_dec dc1 dc2 && 731 eq_trm ( typ_of_dec dc ) tm3 && not (occurs 0 tm2) 732 then 733 TH tm2 sg1 734 else 735 TH_Err "Invalid existential elimination" 736 737 exists_elim _ _ = TH_Err "Invalid existential elimination" 738 739 740 741 742 743 {- => introduction -} 744 745 discharge (TH tm (Extend dc sg _)) 746 = if is_axm_dec dc 747 then 748 TH (Binder Imp dc tm [] [] ) sg 749 else 750 TH_Err "Invalid implication introduction" 751 752 discharge _ = TH_Err "Invalid implication introduction (2)" 753 754 755 756 757 758 {- => elimination -} 759 760 modus_ponens (TH (Binder Imp dc tm2 _ _) sg1) (TH tm3 sg2) 761 = if eq_sgn sg1 sg2 && eq_trm ( typ_of_dec dc ) tm3 762 then 763 TH tm2 sg1 764 else 765 TH_Err "Invalid implication elimination" 766 767 modus_ponens _ _ = TH_Err "Invalid implication elimination" 768 769 770 771 772 {- Propositional tautologies -} 773 774 taut (TM tm (Constant Bool' _ _) sg) 775 = if eval tm 776 then 777 TH tm sg 778 else 779 TH_Err "term is not a tautology" 780 781 taut _ = TH_Err "argument must be a term of sort `bool'" 782 783 784 785 786 787 {- Reflexivity of equality -} 788 789 reflex (TM tm _ sg) 790 = TH (Binary' Eq' tm tm [] []) sg 791 792 793 794 795 796 {- Symmetry of equality -} 797 798 symmetry (TH (Binary' Eq' tm1 tm2 _ _) sg) 799 = TH (Binary' Eq' tm2 tm1 [] []) sg 800 801 symmetry _ = TH_Err "symmetry: argument must be an equality term" 802 803 804 805 806 807 {- Beta reduce a subterm of a theorem -} 808 809 beta_rw (TH tm sg) i 810 = case select_trm tm i of 811 (App (Binder Lambda dc tm1 _ _) tm2 _ _ ,_) 812 -> TH (replace_trm tm (subst_trm dc tm1 tm2) i) sg 813 _ -> TH_Err "Invalid beta reduction" 814 815 816 817 818 819 {- Eta reduce a subterm of a theorem -} 820 821 eta_rw (TH tm sg) i 822 = case select_trm tm i of 823 (Binder Lambda dc (App tm1 tm2 _ _) _ _ ,_) 824 -> if not (occurs 0 tm1) && eta_match dc tm2 1 825 then 826 TH (replace_trm tm (shift_trm [] (-1) tm1) i) sg 827 else 828 TH_Err "Invalid eta reduction" 829 _ -> TH_Err "Invlaid eta reduction (2)" 830 831 832 833 834 835 {- Rewrite conditional (condition is true) -} 836 837 cond_true_rw (TH tm1 sg1) (TH tm2 sg2) i 838 = case select_trm tm2 i of 839 (Cond dc tm3 tm4 _ _ ,dcL) 840 -> if eq_sgn sg1 sg3 && eq_trm tm1 (typ_of_dec dc) 841 then 842 TH (replace_trm tm2 (shift_trm [] (-1) tm3) i) sg1 843 else 844 TH_Err "cond_true_rw: error" 845 where 846 sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg2 dcL 847 848 _ -> TH_Err "cond_true_rw: error 2" 849 850 851 852 853 854 {- Rewrite conditional (condition is false) -} 855 856 cond_false_rw (TH tm1 sg1) (TH tm2 sg2) i 857 = case select_trm tm2 i of 858 (Cond dc tm3 tm4 _ _ ,dcL) 859 -> if eq_sgn sg1 sg3 && 860 eq_trm tm1 (Unary Not (typ_of_dec dc) [] []) 861 then 862 TH (replace_trm tm2 (shift_trm [] (-1) tm4) i) sg1 863 else 864 TH_Err "cond_false_rw: error" 865 where 866 sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg2 dcL 867 868 _ -> TH_Err "cond_false_rw: error 2" 869 870 871 872 873 874 {- Substutution of equal terms -} 875 876 subterm_rw (TH tm1 sg1) (TH (Binary' Eq' tm2 tm3 _ _) sg2) i 877 = if eq_sgn sg3 sg3 && eq_trm tm2 tm4 878 then 879 TH (replace_trm tm1 tm3 i) sg1 880 else 881 TH_Err "subterm_rw: terms or sigs unequal" 882 where 883 (tm4,dcL) = select_trm tm1 i 884 sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg1 dcL 885 886 subterm_rw _ _ _ = TH_Err "subterm_rw: Invalid argument" 887 888 889 890 891 892 {- Injectivity of datatypes -} 893 894 injection (TH (Binary' Eq' tm1 tm2 _ _) sg) 895 = case (reduce_app tm1 [], reduce_app tm2 []) of 896 (c1@(Const i j k _ _):tmL1 , c2@(Const _ _ _ _ _):tmL2) 897 -> case extract_dc j (nth_dec i sg) of 898 Data dcL _ _ 899 -> if length dcL < length tmL1 && 900 eq_trm c1 c2 && 901 length tmL1 == length tmL2 902 then 903 TH (foldr1 mk_and 904 (map mk_eq (zip tmL11 tmL21))) sg 905 906 else 907 TH_Err "Invalid injection" 908 where 909 tmL11 = drop (length dcL) tmL1 910 tmL21 = drop (length dcL) tmL2 911 912 _ -> TH_Err "Invalid injection: not a datatype" 913 914 _ -> TH_Err "Invalid injection (3)" 915 where 916 reduce_app (App tm1 tm2 _ _) tmL 917 = reduce_app tm1 (tm2:tmL) 918 919 reduce_app tm tmL = tm:tmL 920 921 mk_eq (tm1,tm2) = Binary' Eq' tm1 tm2 [] [] 922 mk_and tm1 tm2 = Binary' And tm1 tm2 [] [] 923 924 injection _ = TH_Err "Invalid injection (4)" 925 926 927 928 929 930 {- Induction over datatypes -} 931 932 induction (TM tm@(Const i j 0 _ _) _ sg) 933 = TH ind_axm sg 934 where 935 ind_axm = induction_trm sg tm 936 937 induction _ = TH_Err "Invalid induction" 938 939 940 941 942 943 {- Issubtype introduction -} 944 945 issubstype_intro (TH (Binder Forall dc1 tm1 _ _) sg) 946 = case tm1 of 947 Binder Exists dc2 (Binary' Eq' tm2 tm3 _ _) _ _ 948 -> case (tm2,tm3) of 949 (Sym 1 0 _ _ , Sym 0 0 _ _) 950 -> TH (Binary' Issubtype tm4 tm5 [] []) sg 951 where 952 tm4 = typ_of_dec dc1 953 tm5 = shift_trm [] (-1) (typ_of_dec dc2) 954 _ -> TH_Err "issubtype_intro error (1)" 955 956 _ -> TH_Err "issubtype_intro error (2)" 957 958 issubstype_intro _ = TH_Err "issubtype_intro error (3)" 959 960 961 962 963 964 {- Issubtype elimination -} 965 966 issubstype_elim (TH (Binary' Issubtype tm1 tm2 _ _) sg) 967 = TH (Binder Forall dc1 tm5 [] []) sg 968 where 969 dc1 = Symbol_dec tm1 [] 970 dc2 = Symbol_dec (shift_trm [] 1 tm2) [] 971 tm3 = Sym 1 0 [] [] 972 tm4 = Sym 0 0 [] [] 973 tm5 = Binder Exists dc2 (Binary' Eq' tm3 tm4 [] []) [] [] 974 975 issubstype_elim _ = TH_Err "issubtype_elim error" 976 977 978 979 980 981 {- Equality of types -} 982 983 eq_of_ty (TH (Binary' Issubtype tm1 tm2 [] []) sg1) 984 (TH (Binary' Issubtype tm3 tm4 [] []) sg2) 985 = if eq_sgn sg1 sg2 && eq_trm tm1 tm4 && eq_trm tm2 tm3 986 then 987 TH (Binary' Eq' tm1 tm2 [] []) sg1 988 else 989 TH_Err "eq_of_ty error" 990 991 eq_of_ty _ _ = TH_Err "eq_of_ty error (2)" 992 993 994 995 996 997 {- project the theorem out of a terms subtype -} 998 999 from (TM tm1 (Binder Subtype dc tm2 _ _) sg) 1000 = TH (subst_trm dc tm2 tm1) sg 1001 1002 from _ = TH_Err "from: argument must be term of subtype sort" 1003 1004 1005 1006 1007 1008 {- definition elimination -} 1009 1010 def_elim_thm (TH tm (Extend dc sg _)) 1011 = if is_def_dec dc 1012 then 1013 TH (subst_trm dc1 tm tm1) sg 1014 else 1015 TH_Err "Definition elimination error" 1016 where 1017 (dc1,tm1,_) = split_def dc 1018 1019 def_elim_thm _ = TH_Err "Definition elimination error (2)" 1020 1021 1022 1023 1024 1025 {- weaken a theorem -} 1026 1027 weaken (SG sg1) (TH tm sg2) 1028 = case is_sub_sgn sg2 sg1 of 1029 SOME i 1030 -> TH (shift_trm share_map i tm) sg1 1031 where 1032 share_map = get_share_map sg1 1033 1034 NONE -> TH_Err "Weaken error" 1035 1036 1037 1038 1039 1040 set_Thm_att (TH tm sg) iL att 1041 = TH (set_trm_att tm iL att) sg 1042 1043 1044 1045 1046 1047 get_Thm_att (TH tm sg) iL 1048 = get_trm_att tm iL 1049 1050 1051 1052 1053 1054 {- Restore a theorem from the database -} 1055 1056 restore_Thm s = error "BadTheorem" -- ** exn 1057 1058 1059 1060 1061 1062 {- return the internal representation of a theorem -} 1063 1064 internal_Thm (TH tm sg) = (tm,sg) 1065 1066 internal_Thm (TH_Err mesg ) = error "add feed to itm via extra itrm ctr" 1067 1068 1069 1070 1071 1072 {- 1073 database_magic_trm_str = "VTSTRM\^H\^H\^H\^H\^H\^H\^X\^Y" 1074 database_magic_sgn_str = "VTSSGN\^H\^H\^H\^H\^H\^H\^X\^Y" 1075 database_magic_dec_str = "VTSDEC\^H\^H\^H\^H\^H\^H\^X\^Y" 1076 database_magic_thm_str = "VTSTHM\^H\^H\^H\^H\^H\^H\^X\^Y" 1077 1078 magic_str_len = length database_magic_trm_str 1079 dbase_str = "vts90/lib/dbase/" 1080 trm_str = "Term" 1081 sgn_str = "Signature" 1082 dec_str = "Declaration" 1083 thm_str = "Theorem" 1084 1085 1086 1087 write_obj magic_str type_str obj file 1088 = if test_file full_file_name "f" 1089 then 1090 False 1091 else 1092 let val ostr = open_out full_file_name 1093 in output (ostr, magic_str); 1094 output (ostr, obj); 1095 close_out ostr; 1096 true 1097 end 1098 end 1099 let val home = get_env_var "HOME" 1100 val full_file_name = home ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file 1101 1102 1103 fun read_obj exn magic_str type_str file = 1104 let val home = get_env_var "HOME" 1105 val vtshome = get_env_var "VTS_LIB_DIR" 1106 val first_choice = home ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file 1107 val second_choice = vtshome ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file 1108 val file_name = 1109 if test_file first_choice "fr" then 1110 first_choice 1111 else if test_file second_choice "fr" then 1112 second_choice 1113 else 1114 raise exn 1115 val istr = open_in file_name 1116 val obj_magic_str = input (istr, magic_str_len) 1117 val obj_str = input_to_eof istr 1118 in close_in istr; 1119 if magic_str = obj_magic_str then 1120 obj_str 1121 else 1122 raise exn 1123 end 1124 1125 and input_to_eof istr = 1126 if end_of_stream istr then 1127 "" 1128 else 1129 let val str1 = input (istr,1024) 1130 val str2 = input_to_eof istr 1131 in (str1 ^ str2) end 1132 1133 val anon_sgn_name_header = "%" 1134 1135 fun read file = 1136 let val instr = open_in file 1137 val str = input_to_eof instr 1138 in close_in instr; 1139 str 1140 end 1141 handle Io _ => "" 1142 1143 fun write file str = 1144 let val outstr = open_out file 1145 in output (outstr, str); 1146 close_out outstr 1147 end 1148 1149 fun already_there str dir ("." :: files) = (* skip over . and .. *) 1150 already_there str dir files 1151 | already_there str dir (".." :: files) = 1152 already_there str dir files 1153 | already_there str dir (file :: files) = 1154 if read (dir ^ file) = str then 1155 SOME file 1156 else 1157 already_there str dir files 1158 | already_there str dir [] = 1159 NONE 1160 1161 fun save_sgn name sgn_rep = 1162 let val home = get_env_var "HOME" 1163 val sgn_dir = home ^ "/" ^ dbase_str ^ sgn_str ^ "/" 1164 val sgs = System.Directory.listDir sgn_dir 1165 in case already_there sgn_rep sgn_dir sgs 1166 of SOME nm => nm 1167 | NONE => (write (sgn_dir ^ anon_sgn_name_header ^ name) sgn_rep; 1168 anon_sgn_name_header ^ name) 1169 end 1170 1171 1172 val a_chr = fromEnum "a" 1173 and z_chr = fromEnum "z" 1174 and A_chr = fromEnum "A" 1175 and Z_chr = fromEnum "Z" 1176 and zero_chr = fromEnum "0" 1177 and nine_chr = fromEnum "9" 1178 and minus_chr = fromEnum "-" 1179 and underline_chr = fromEnum "_" 1180 and dot_cht = fromEnum "." 1181 1182 (* database names must be either: *) 1183 (* lower-case alphas a-z *) 1184 (* upper-case alphas A-Z *) 1185 (* numbers 0-9 *) 1186 (* or _ - . *) 1187 1188 fun ok_name name = 1189 let fun ok_ch ch = 1190 (a_chr <= ch andalso ch <= z_chr) orelse 1191 (A_chr <= ch andalso ch <= Z_chr) orelse 1192 (zero_chr <= ch andalso ch <= nine_chr) orelse 1193 (ch = minus_chr) orelse 1194 (ch = underline_chr) orelse 1195 (ch = dot_cht) 1196 in forall ok_ch (map fromEnum (explode name)) end 1197 1198 in (* local *) 1199 1200 (* STILL TO BE DONE *) 1201 (* SORT OUT SIGNATURE SHARING *) 1202 1203 fun save_Trm name (TM (tm1,tm2,sg)) = 1204 if ok_name name then 1205 let val tm1_str = trm_to_str tm1 1206 val tm2_str = trm_to_str tm2 1207 val sg_str = database_magic_sgn_str ^ sgn_to_str sg 1208 val sg_nm = save_sgn name sg_str 1209 in write_obj database_magic_trm_str trm_str (tm1_str ^ tm2_str ^ sg_nm) name end 1210 else 1211 false 1212 1213 fun save_Sgn name (SG sg) = 1214 if ok_name name then 1215 let val sg_str = database_magic_sgn_str ^ sgn_to_str sg 1216 val sg_nm = save_sgn name sg_str 1217 in write_obj database_magic_sgn_str sgn_str sg_nm name end 1218 else 1219 false 1220 1221 fun save_Dec name (DC (dc,sg)) = 1222 if ok_name name then 1223 let val dc_str = dec_to_str dc 1224 val sg_str = database_magic_sgn_str ^ sgn_to_str sg 1225 val sg_nm = save_sgn name sg_str 1226 in write_obj database_magic_dec_str dec_str (dc_str ^ sg_nm) name end 1227 else 1228 false 1229 1230 fun save_Thm name (TH (tm,sg)) = 1231 if ok_name name then 1232 let val tm_str = trm_to_str tm 1233 val sg_str = database_magic_sgn_str ^ sgn_to_str sg 1234 val sg_nm = save_sgn name sg_str 1235 in write_obj database_magic_thm_str thm_str (tm_str ^ sg_nm) name end 1236 else 1237 false 1238 1239 fun restore_Trm file = 1240 let val obj_str = read_obj BadTerm database_magic_trm_str trm_str file 1241 val (tm1, is1) = str_to_trm (mkistring obj_str) 1242 val (tm2, is2) = str_to_trm is1 1243 val sg_nm = rest_istring is2 1244 val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm 1245 val (sg, is3) = str_to_sgn (mkistring sgn_rep) 1246 in (TM (tm1,tm2,sg)) end 1247 1248 fun restore_Sgn file = 1249 if ok_name file then 1250 let val sg_nm = read_obj BadSignature database_magic_sgn_str sgn_str file 1251 val obj_str = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm 1252 val (sg, is3) = str_to_sgn (mkistring obj_str) 1253 in (SG sg) end 1254 else 1255 raise BadSignature 1256 1257 fun restore_Dec file = 1258 let val obj_str = read_obj BadDeclaration database_magic_dec_str dec_str file 1259 val (dc, is1) = str_to_dec (mkistring obj_str) 1260 val sg_nm = rest_istring is1 1261 val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm 1262 val (sg, is2) = str_to_sgn (mkistring sgn_rep) 1263 in (DC (dc,sg)) end 1264 1265 fun restore_Thm file = 1266 let val obj_str = read_obj BadTheorem database_magic_thm_str thm_str file 1267 val (tm, is1) = str_to_trm (mkistring obj_str) 1268 val sg_nm = rest_istring is1 1269 val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm 1270 val (sg, is2) = str_to_sgn (mkistring sgn_rep) 1271 in (TH (tm,sg)) end 1272 1273 end (* local *) 1274 1275 -} 1276 1277 eq_Trm (TM tm1 _ sg1 ) (TM tm2 _ sg2 ) 1278 = eq_trm tm1 tm2 && eq_sgn sg1 sg2 1279 1280 eq_Sgn (SG sg1) (SG sg2) 1281 = eq_sgn sg1 sg2 1282 1283 eq_Dec (DC dc1 sg1 ) (DC dc2 sg2 ) 1284 = eq_dec dc1 dc2 && eq_sgn sg1 sg2 1285 1286 eq_Thm (TH tm1 sg1) (TH tm2 sg2) 1287 = eq_trm tm1 tm2 && eq_sgn sg1 sg2 1288 1289 typ_of_Trm (TM _ tm sg) 1290 = TM tm ( typ_of_trm sg tm ) sg 1291 1292 typ_of_Dec ( DC dc sg ) 1293 = TM tm1 tm2 sg 1294 where 1295 tm1 = typ_of_dec dc 1296 tm2 = typ_of_trm sg tm1 1297 1298 typ_of_Thm ( TH tm sg ) 1299 = TM tm ( Constant Bool' [] [] ) sg 1300 1301 1302 1303 1304 1305 1306 shift_Trm i (SG sg1) (TM tm1 tm2 sg2) 1307 = if eq_sgn sg2 sg3 1308 then TM (shift_trm sm i tm1) (shift_trm sm i tm2) sg1 1309 else TM_Err "shift_Trm: signatures unequal" 1310 where 1311 sg3 = nth_sgn i sg1 1312 sm = get_share_map sg2 1313 1314 1315 1316 1317 1318 1319 1320 1321 subst_Trm (TM tm1 tm2 (Extend dc sg1 _)) (TM tm3 tm4 sg2) 1322 = if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm4 1323 then TM (subst_trm dc tm1 tm2) (subst_trm dc tm2 tm3) sg1 1324 else TM_Err "subst_Trm: signatures unequal or type of dc unequal to type of second argument" 1325 1326 subst_Trm _ _ = TM_Err "subst_Trm: Invalid arguments" 1327 1328 1329 sgn_of_Trm (TM _ _ sg) = SG sg 1330 1331 sgn_of_Trm (TM_Err mesg ) = SG_Err mesg 1332 1333 1334 1335 sgn_of_Dec (DC _ sg) = SG sg 1336 1337 sgn_of_Dec (DC_Err mesg ) = SG_Err mesg 1338 1339 1340 1341 sgn_of_Thm (TH _ sg) = SG sg 1342 1343 sgn_of_Thm (TH_Err mesg ) = SG_Err mesg 1344 1345 1346 1347 1348 is_valid_Thm ( TH _ _ ) = True 1349 1350 is_valid_Thm _ = False 1351 1352 1353 1354 is_valid_Trm ( TM _ _ _ ) = True 1355 1356 is_valid_Trm _ = False 1357 1358 1359 is_valid_Sgn ( SG _ ) = True 1360 1361 is_valid_Sgn _ = False 1362