1;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 2;; __ __ __ __ ;; 3;; / \ / \ (__) | | ____ ___ __ ____ ;; 4;; / \/ \ __ | | / _ | \ \ __ / / / _ | ;; 5;; / /\ /\ \ | | | | / / | | \ ' ' / / / | | ;; 6;; / / \__/ \ \ | | | | \ \_| | \ /\ / \ \_| | ;; 7;; /__/ \__\ |__| |__| \____| \/ \/ \____| ;; 8;; ~ ~~ \ ~ ~ ~_~~ ~/~ /~ | ~|~ | ~| ~ /~_ ~|~ ~ ~\ ~\~ ~ ~ ~ |~~ ~ ;; 9;; ~ ~ \~ \~ / ~\~ / ~/ ~ |~ | ~| ~ ~/~/ | |~ ~~/ ~\/ ~~ ~ / / | |~ ~ ;; 10;; ~ ~ ~ \ ~\/ ~ \~ ~/ ~~ ~__| |~ ~ ~ \_~ ~ ~ .__~ ~\ ~\ ~_| ~ ~ ~~ ;; 11;; ~~ ~ ~\ ~ /~ ~ ~ ~ ~ __~ | ~ ~ \~__~| ~/__~ ~\__~ ~~___~| ~ ~ ;; 12;; ~ ~~ ~ \~_/ ~_~/ ~ ~ ~(__~ ~|~_| ~ ~ ~~ ~ ~ ~~ ~ ~ ~~ ~ ~ ;; 13;; ;; 14;; A R e f l e c t i v e P r o o f C h e c k e r ;; 15;; ;; 16;; Copyright (C) 2005-2009 by Jared Davis <jared@cs.utexas.edu> ;; 17;; ;; 18;; This program is free software; you can redistribute it and/or modify it ;; 19;; under the terms of the GNU General Public License as published by the ;; 20;; Free Software Foundation; either version 2 of the License, or (at your ;; 21;; option) any later version. ;; 22;; ;; 23;; This program is distributed in the hope that it will be useful, but ;; 24;; WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABIL- ;; 25;; ITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public ;; 26;; License for more details. ;; 27;; ;; 28;; You should have received a copy of the GNU General Public License along ;; 29;; with this program (see the file COPYING); if not, write to the Free ;; 30;; Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA ;; 31;; 02110-1301, USA. ;; 32;; ;; 33;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 34 35; core.lisp 36; - used by Common Lisp systems and also Jitawa 37; - contains core Milawa definitions 38 39(define 'lookup-safe '(a x) 40 '(if (consp x) 41 (if (equal a (car (car x))) 42 (if (consp (car x)) 43 (car x) 44 (cons (car (car x)) (cdr (car x)))) 45 (lookup-safe a (cdr x))) 46 'nil)) 47 48(define 'define-safe '(ftbl name formals body) 49 ;; Returns FTBL-PRIME or causes an error. 50 '(let* ((this-def (list name formals body)) 51 (prev-def (lookup-safe name ftbl))) 52 (if prev-def 53 (if (equal prev-def this-def) 54 ftbl 55 (error (list 'redefinition-error prev-def this-def))) 56 (let ((unused (define name formals body))) 57 (cons this-def ftbl))))) 58 59(define 'define-safe-list '(ftbl defs) 60 ;; DEFS are 3-tuples of the form: (name formals body) 61 ;; We define all of these functions, in order. 62 ;; We return FTBL-PRIME or causes an error. 63 '(if (consp defs) 64 (let* ((def1 (car defs)) 65 (ftbl (define-safe ftbl (first def1) (second def1) (third def1)))) 66 (define-safe-list ftbl (cdr defs))) 67 ftbl)) 68 69(define 'milawa-init '() 70 '(define-safe-list 71 72; We start with "ill-formed" definitions for any functions we don't want the 73; user to be able to redefine. This list includes (1) all of the primitive 74; Milawa functions like IF, EQUAL, etc., and (2) any built-in system functions 75; that the Lisp relies upon. 76; 77; The point of this is to ensure that any attempt by the user to define any of 78; these functions will fail. No matter what formals and body they try to use, 79; the resulting call of DEFUN-SAFE will insist that (F FORMALS BODY) is in the 80; FTBL, but the actual entry is just (F). 81 82 '(;; Milawa Primitives 83 (if) 84 (equal) 85 (symbolp) 86 (symbol-<) 87 (natp) 88 (<) 89 (+) 90 (-) 91 (consp) 92 (cons) 93 (car) 94 (cdr) 95 96 ;; Extralogical System Functions 97 (error) 98 (print) 99 (define) 100 (defun) 101 (funcall) 102 (lookup-safe) 103 (define-safe) 104 (define-safe-list) 105 (milawa-init) 106 (milawa-main)) 107 108; We now extend the above FTBL wth definitions for all of the functions for our 109; proof-checking system. Note that the act of defining these functions does 110; not "admit" them and add definitional axioms, but instead merely (1) 111; introduces Lisp definitions of these functions and (2) installs FTBL entries 112; for these functions so that the user may not define them in any other way. 113 114 '((not (x) (if x nil t)) 115 116 (rank (x) 117 (if (consp x) 118 (+ 1 119 (+ (rank (car x)) 120 (rank (cdr x)))) 121 0)) 122 123 (ord< (x y) 124 (cond ((not (consp x)) 125 (if (consp y) t (< x y))) 126 ((not (consp y)) 127 nil) 128 ((not (equal (car (car x)) (car (car y)))) 129 (ord< (car (car x)) (car (car y)))) 130 ((not (equal (cdr (car x)) (cdr (car y)))) 131 (< (cdr (car x)) (cdr (car y)))) 132 (t 133 (ord< (cdr x) (cdr y))))) 134 135 (ordp (x) 136 (if (not (consp x)) 137 (natp x) 138 (and (consp (car x)) 139 (ordp (car (car x))) 140 (not (equal (car (car x)) 0)) 141 (< 0 (cdr (car x))) 142 (ordp (cdr x)) 143 (if (consp (cdr x)) 144 (ord< (car (car (cdr x))) (car (car x))) 145 t)))) 146 147 (nfix (x) (if (natp x) x 0)) 148 149 (<= (a b) (not (< b a))) 150 151 (zp (x) (if (natp x) (equal x 0) t)) 152 153 (true-listp (x) 154 (if (consp x) 155 (true-listp (cdr x)) 156 (equal x nil))) 157 158 (list-fix (x) 159 (if (consp x) 160 (cons (car x) (list-fix (cdr x))) 161 nil)) 162 163 (len (x) 164 (if (consp x) 165 (+ 1 (len (cdr x))) 166 0)) 167 168 (memberp (a x) 169 (if (consp x) 170 (or (equal a (car x)) 171 (memberp a (cdr x))) 172 nil)) 173 174 (subsetp (x y) 175 (if (consp x) 176 (and (memberp (car x) y) 177 (subsetp (cdr x) y)) 178 t)) 179 180 (uniquep (x) 181 (if (consp x) 182 (and (not (memberp (car x) (cdr x))) 183 (uniquep (cdr x))) 184 t)) 185 186 (app (x y) 187 (if (consp x) 188 (cons (car x) (app (cdr x) y)) 189 (list-fix y))) 190 191 (rev (x) 192 (if (consp x) 193 (app (rev (cdr x)) (list (car x))) 194 nil)) 195 196 (tuplep (n x) 197 (if (zp n) 198 (equal x nil) 199 (and (consp x) 200 (tuplep (- n 1) (cdr x))))) 201 202 (pair-lists (x y) 203 (if (consp x) 204 (cons (cons (car x) (car y)) 205 (pair-lists (cdr x) (cdr y))) 206 nil)) 207 208 (lookup (a x) 209 (if (consp x) 210 (if (equal a (car (car x))) 211 (if (consp (car x)) 212 (car x) 213 (cons (car (car x)) (cdr (car x)))) 214 (lookup a (cdr x))) 215 nil)) 216 217 ;; THE PROOF CHECKER - TERMS 218 219 (|LOGIC.VARIABLEP| (x) 220 (and (symbolp x) 221 (not (equal x t)) 222 (not (equal x nil)))) 223 224 (|LOGIC.VARIABLE-LISTP| (x) 225 (if (consp x) 226 (and (|LOGIC.VARIABLEP| (car x)) 227 (|LOGIC.VARIABLE-LISTP| (cdr x))) 228 t)) 229 230 (|LOGIC.CONSTANTP| (x) 231 (and (tuplep 2 x) 232 (equal (first x) 'quote))) 233 234 (|LOGIC.CONSTANT-LISTP| (x) 235 (if (consp x) 236 (and (|LOGIC.CONSTANTP| (car x)) 237 (|LOGIC.CONSTANT-LISTP| (cdr x))) 238 t)) 239 240 (|LOGIC.FUNCTION-NAMEP| (x) 241 (and (symbolp x) 242 (not (memberp x '(nil quote pequal* pnot* 243 por* first second third 244 fourth fifth and or list 245 cond let let*))))) 246 247 (|LOGIC.FLAG-TERM-VARS| (flag x acc) 248 (if (equal flag 'term) 249 (cond ((|LOGIC.CONSTANTP| x) acc) 250 ((|LOGIC.VARIABLEP| x) (cons x acc)) 251 ((not (consp x)) acc) 252 (t 253 (|LOGIC.FLAG-TERM-VARS| 'list (cdr x) acc))) 254 (if (consp x) 255 (|LOGIC.FLAG-TERM-VARS| 'term (car x) 256 (|LOGIC.FLAG-TERM-VARS| 'list (cdr x) acc)) 257 acc))) 258 259 (|LOGIC.TERM-VARS| (x) (|LOGIC.FLAG-TERM-VARS| 'term x nil)) 260 261 (|LOGIC.FLAG-TERMP| (flag x) 262 (if (equal flag 'term) 263 (or (|LOGIC.VARIABLEP| x) 264 (|LOGIC.CONSTANTP| x) 265 (and (consp x) 266 (if (|LOGIC.FUNCTION-NAMEP| (car x)) 267 (let ((args (cdr x))) 268 (and (true-listp args) 269 (|LOGIC.FLAG-TERMP| 'list args))) 270 (and (tuplep 3 (car x)) 271 (let ((lambda-symbol (first (car x))) 272 (formals (second (car x))) 273 (body (third (car x))) 274 (actuals (cdr x))) 275 (and (equal lambda-symbol 'lambda) 276 (true-listp formals) 277 (|LOGIC.VARIABLE-LISTP| formals) 278 (uniquep formals) 279 (|LOGIC.FLAG-TERMP| 'term body) 280 (subsetp (|LOGIC.TERM-VARS| body) formals) 281 (equal (len formals) (len actuals)) 282 (true-listp actuals) 283 (|LOGIC.FLAG-TERMP| 'list actuals))))))) 284 (if (consp x) 285 (and (|LOGIC.FLAG-TERMP| 'term (car x)) 286 (|LOGIC.FLAG-TERMP| 'list (cdr x))) 287 t))) 288 289 (|LOGIC.TERMP| (x) (|LOGIC.FLAG-TERMP| 'term x)) 290 291 (|LOGIC.UNQUOTE| (x) (second x)) 292 293 (|LOGIC.UNQUOTE-LIST| (x) 294 (if (consp x) 295 (cons (|LOGIC.UNQUOTE| (car x)) 296 (|LOGIC.UNQUOTE-LIST| (cdr x))) 297 nil)) 298 299 (|LOGIC.FUNCTIONP| (x) (|LOGIC.FUNCTION-NAMEP| (car x))) 300 (|LOGIC.FUNCTION-NAME| (x) (car x)) 301 (|LOGIC.FUNCTION-ARGS| (x) (cdr x)) 302 (|LOGIC.FUNCTION| (name args) (cons name args)) 303 304 (|LOGIC.LAMBDAP| (x) (consp (car x))) 305 (|LOGIC.LAMBDA-FORMALS| (x) (second (car x))) 306 (|LOGIC.LAMBDA-BODY| (x) (third (car x))) 307 (|LOGIC.LAMBDA-ACTUALS| (x) (cdr x)) 308 (|LOGIC.LAMBDA| (xs b ts) (cons (list 'lambda xs b) ts)) 309 310 (|LOGIC.FLAG-TERM-ATBLP| (flag x atbl) 311 (if (equal flag 'term) 312 (cond ((|LOGIC.CONSTANTP| x) t) 313 ((|LOGIC.VARIABLEP| x) t) 314 ((|LOGIC.FUNCTIONP| x) 315 (let ((name (|LOGIC.FUNCTION-NAME| x)) 316 (args (|LOGIC.FUNCTION-ARGS| x))) 317 (and (equal (len args) (cdr (lookup name atbl))) 318 (|LOGIC.FLAG-TERM-ATBLP| 'list args atbl)))) 319 ((|LOGIC.LAMBDAP| x) 320 (let ((body (|LOGIC.LAMBDA-BODY| x)) 321 (actuals (|LOGIC.LAMBDA-ACTUALS| x))) 322 (and (|LOGIC.FLAG-TERM-ATBLP| 'term body atbl) 323 (|LOGIC.FLAG-TERM-ATBLP| 'list actuals atbl)))) 324 (t nil)) 325 (if (consp x) 326 (and (|LOGIC.FLAG-TERM-ATBLP| 'term (car x) atbl) 327 (|LOGIC.FLAG-TERM-ATBLP| 'list (cdr x) atbl)) 328 t))) 329 330 (|LOGIC.TERM-ATBLP| (x atbl) 331 (|LOGIC.FLAG-TERM-ATBLP| 'term x atbl)) 332 333 334 ;; THE PROOF CHECKER - FORMULAS 335 336 (|LOGIC.FORMULAP| (x) 337 (cond ((equal (first x) 'pequal*) 338 (and (tuplep 3 x) 339 (|LOGIC.TERMP| (second x)) 340 (|LOGIC.TERMP| (third x)))) 341 ((equal (first x) 'pnot*) 342 (and (tuplep 2 x) 343 (|LOGIC.FORMULAP| (second x)))) 344 ((equal (first x) 'por*) 345 (and (tuplep 3 x) 346 (|LOGIC.FORMULAP| (second x)) 347 (|LOGIC.FORMULAP| (third x)))) 348 (t nil))) 349 350 (|LOGIC.FORMULA-LISTP| (x) 351 (if (consp x) 352 (and (|LOGIC.FORMULAP| (car x)) 353 (|LOGIC.FORMULA-LISTP| (cdr x))) 354 t)) 355 356 (|LOGIC.FMTYPE| (x) (first x)) 357 358 (|LOGIC.=LHS| (x) (second x)) 359 (|LOGIC.=RHS| (x) (third x)) 360 (|LOGIC.~ARG| (x) (second x)) 361 (|LOGIC.VLHS| (x) (second x)) 362 (|LOGIC.VRHS| (x) (third x)) 363 364 (|LOGIC.PEQUAL| (a b) (list 'pequal* a b)) 365 (|LOGIC.PNOT| (a) (list 'pnot* a)) 366 (|LOGIC.POR| (a b) (list 'por* a b)) 367 368 (|LOGIC.FORMULA-ATBLP| (x atbl) 369 (let ((type (|LOGIC.FMTYPE| x))) 370 (cond ((equal type 'por*) 371 (and (|LOGIC.FORMULA-ATBLP| (|LOGIC.VLHS| x) atbl) 372 (|LOGIC.FORMULA-ATBLP| (|LOGIC.VRHS| x) atbl))) 373 ((equal type 'pnot*) 374 (|LOGIC.FORMULA-ATBLP| (|LOGIC.~ARG| x) atbl)) 375 ((equal type 'pequal*) 376 (and (|LOGIC.TERM-ATBLP| (|LOGIC.=LHS| x) atbl) 377 (|LOGIC.TERM-ATBLP| (|LOGIC.=RHS| x) atbl))) 378 (t nil)))) 379 380 (|LOGIC.DISJOIN-FORMULAS| (x) 381 (if (consp x) 382 (if (consp (cdr x)) 383 (|LOGIC.POR| (car x) (|LOGIC.DISJOIN-FORMULAS| (cdr x))) 384 (car x)) 385 nil)) 386 387 ;; THE PROOF CHECKER - APPEALS 388 389 (|LOGIC.FLAG-APPEALP| (flag x) 390 (if (equal flag 'proof) 391 (and (true-listp x) 392 (<= (len x) 4) 393 (symbolp (first x)) 394 (|LOGIC.FORMULAP| (second x)) 395 (true-listp (third x)) 396 (|LOGIC.FLAG-APPEALP| 'list (third x))) 397 (if (consp x) 398 (and (|LOGIC.FLAG-APPEALP| 'proof (car x)) 399 (|LOGIC.FLAG-APPEALP| 'list (cdr x))) 400 t))) 401 402 (|LOGIC.APPEALP| (x) (|LOGIC.FLAG-APPEALP| 'proof x)) 403 (|LOGIC.APPEAL-LISTP| (x) (|LOGIC.FLAG-APPEALP| 'list x)) 404 405 (|LOGIC.METHOD| (x) (first x)) 406 (|LOGIC.CONCLUSION| (x) (second x)) 407 (|LOGIC.SUBPROOFS| (x) (third x)) 408 (|LOGIC.EXTRAS| (x) (fourth x)) 409 410 (|LOGIC.STRIP-CONCLUSIONS| (x) 411 (if (consp x) 412 (cons (|LOGIC.CONCLUSION| (car x)) 413 (|LOGIC.STRIP-CONCLUSIONS| (cdr x))) 414 nil)) 415 416 ;; THE PROOF CHECKER - STEP CHECKING 417 418 (|LOGIC.AXIOM-OKP| (x axioms atbl) 419 (let ((method (|LOGIC.METHOD| x)) 420 (conclusion (|LOGIC.CONCLUSION| x)) 421 (subproofs (|LOGIC.SUBPROOFS| x)) 422 (extras (|LOGIC.EXTRAS| x))) 423 (and (equal method 'axiom) 424 (equal subproofs nil) 425 (equal extras nil) 426 (memberp conclusion axioms) 427 (|LOGIC.FORMULA-ATBLP| conclusion atbl)))) 428 429 (|LOGIC.THEOREM-OKP| (x thms atbl) 430 (let ((method (|LOGIC.METHOD| x)) 431 (conclusion (|LOGIC.CONCLUSION| x)) 432 (subproofs (|LOGIC.SUBPROOFS| x)) 433 (extras (|LOGIC.EXTRAS| x))) 434 (and (equal method 'theorem) 435 (equal subproofs nil) 436 (equal extras nil) 437 (memberp conclusion thms) 438 (|LOGIC.FORMULA-ATBLP| conclusion atbl)))) 439 440 ;; Basic Rules 441 442 (|LOGIC.ASSOCIATIVITY-OKP| (x) 443 (let ((method (|LOGIC.METHOD| x)) 444 (conclusion (|LOGIC.CONCLUSION| x)) 445 (subproofs (|LOGIC.SUBPROOFS| x)) 446 (extras (|LOGIC.EXTRAS| x))) 447 (and (equal method 'associativity) 448 (equal extras nil) 449 (tuplep 1 subproofs) 450 (let ((sub-or-a-or-b-c (|LOGIC.CONCLUSION| (first subproofs)))) 451 (and (equal (|LOGIC.FMTYPE| conclusion) 'por*) 452 (equal (|LOGIC.FMTYPE| sub-or-a-or-b-c) 'por*) 453 (let ((conc-or-a-b (|LOGIC.VLHS| conclusion)) 454 (conc-c (|LOGIC.VRHS| conclusion)) 455 (sub-a (|LOGIC.VLHS| sub-or-a-or-b-c)) 456 (sub-or-b-c (|LOGIC.VRHS| sub-or-a-or-b-c))) 457 (and (equal (|LOGIC.FMTYPE| conc-or-a-b) 'por*) 458 (equal (|LOGIC.FMTYPE| sub-or-b-c) 'por*) 459 (let ((conc-a (|LOGIC.VLHS| conc-or-a-b)) 460 (conc-b (|LOGIC.VRHS| conc-or-a-b)) 461 (sub-b (|LOGIC.VLHS| sub-or-b-c)) 462 (sub-c (|LOGIC.VRHS| sub-or-b-c))) 463 (and (equal conc-a sub-a) 464 (equal conc-b sub-b) 465 (equal conc-c sub-c)))))))))) 466 467 (|LOGIC.CONTRACTION-OKP| (x) 468 (let ((method (|LOGIC.METHOD| x)) 469 (conclusion (|LOGIC.CONCLUSION| x)) 470 (subproofs (|LOGIC.SUBPROOFS| x)) 471 (extras (|LOGIC.EXTRAS| x))) 472 (and (equal method 'contraction) 473 (equal extras nil) 474 (tuplep 1 subproofs) 475 (let ((or-a-a (|LOGIC.CONCLUSION| (first subproofs)))) 476 (and (equal (|LOGIC.FMTYPE| or-a-a) 'por*) 477 (equal (|LOGIC.VLHS| or-a-a) conclusion) 478 (equal (|LOGIC.VRHS| or-a-a) conclusion)))))) 479 480 (|LOGIC.CUT-OKP| (x) 481 (let ((method (|LOGIC.METHOD| x)) 482 (conclusion (|LOGIC.CONCLUSION| x)) 483 (subproofs (|LOGIC.SUBPROOFS| x)) 484 (extras (|LOGIC.EXTRAS| x))) 485 (and (equal method 'cut) 486 (equal extras nil) 487 (tuplep 2 subproofs) 488 (let ((or-a-b (|LOGIC.CONCLUSION| (first subproofs))) 489 (or-not-a-c (|LOGIC.CONCLUSION| (second subproofs)))) 490 (and (equal (|LOGIC.FMTYPE| or-a-b) 'por*) 491 (equal (|LOGIC.FMTYPE| or-not-a-c) 'por*) 492 (let ((a (|LOGIC.VLHS| or-a-b)) 493 (b (|LOGIC.VRHS| or-a-b)) 494 (not-a (|LOGIC.VLHS| or-not-a-c)) 495 (c (|LOGIC.VRHS| or-not-a-c))) 496 (and (equal (|LOGIC.FMTYPE| not-a) 'pnot*) 497 (equal (|LOGIC.~ARG| not-a) a) 498 (equal (|LOGIC.FMTYPE| conclusion) 'por*) 499 (equal (|LOGIC.VLHS| conclusion) b) 500 (equal (|LOGIC.VRHS| conclusion) c)))))))) 501 502 (|LOGIC.EXPANSION-OKP| (x atbl) 503 (let ((method (|LOGIC.METHOD| x)) 504 (conclusion (|LOGIC.CONCLUSION| x)) 505 (subproofs (|LOGIC.SUBPROOFS| x)) 506 (extras (|LOGIC.EXTRAS| x))) 507 (and (equal method 'expansion) 508 (equal extras nil) 509 (tuplep 1 subproofs) 510 (let ((b (|LOGIC.CONCLUSION| (first subproofs)))) 511 (and (equal (|LOGIC.FMTYPE| conclusion) 'por*) 512 (equal (|LOGIC.VRHS| conclusion) b) 513 (|LOGIC.FORMULA-ATBLP| (|LOGIC.VLHS| conclusion) atbl)))))) 514 515 (|LOGIC.PROPOSITIONAL-SCHEMA-OKP| (x atbl) 516 (let ((method (|LOGIC.METHOD| x)) 517 (conclusion (|LOGIC.CONCLUSION| x)) 518 (subproofs (|LOGIC.SUBPROOFS| x)) 519 (extras (|LOGIC.EXTRAS| x))) 520 (and (equal method 'propositional-schema) 521 (equal subproofs nil) 522 (equal extras nil) 523 (equal (|LOGIC.FMTYPE| conclusion) 'por*) 524 (let ((not-a (|LOGIC.VLHS| conclusion)) 525 (a (|LOGIC.VRHS| conclusion))) 526 (and (equal (|LOGIC.FMTYPE| not-a) 'pnot*) 527 (equal (|LOGIC.~ARG| not-a) a) 528 (|LOGIC.FORMULA-ATBLP| a atbl)))))) 529 530 (|LOGIC.CHECK-FUNCTIONAL-AXIOM| (x ti si) 531 (if (equal (|LOGIC.FMTYPE| x) 'pequal*) 532 (and (|LOGIC.FUNCTIONP| (|LOGIC.=LHS| x)) 533 (|LOGIC.FUNCTIONP| (|LOGIC.=RHS| x)) 534 (equal (|LOGIC.FUNCTION-NAME| (|LOGIC.=LHS| x)) 535 (|LOGIC.FUNCTION-NAME| (|LOGIC.=RHS| x))) 536 (equal (|LOGIC.FUNCTION-ARGS| (|LOGIC.=LHS| x)) (rev ti)) 537 (equal (|LOGIC.FUNCTION-ARGS| (|LOGIC.=RHS| x)) (rev si))) 538 (and (equal (|LOGIC.FMTYPE| x) 'por*) 539 (equal (|LOGIC.FMTYPE| (|LOGIC.VLHS| x)) 'pnot*) 540 (equal (|LOGIC.FMTYPE| (|LOGIC.~ARG| (|LOGIC.VLHS| x))) 'pequal*) 541 (|LOGIC.CHECK-FUNCTIONAL-AXIOM| 542 (|LOGIC.VRHS| x) 543 (cons (|LOGIC.=LHS| (|LOGIC.~ARG| (|LOGIC.VLHS| x))) ti) 544 (cons (|LOGIC.=RHS| (|LOGIC.~ARG| (|LOGIC.VLHS| x))) si))))) 545 546 (|LOGIC.FUNCTIONAL-EQUALITY-OKP| (x atbl) 547 (let ((method (|LOGIC.METHOD| x)) 548 (conclusion (|LOGIC.CONCLUSION| x)) 549 (subproofs (|LOGIC.SUBPROOFS| x)) 550 (extras (|LOGIC.EXTRAS| x))) 551 (and (equal method 'functional-equality) 552 (equal subproofs nil) 553 (equal extras nil) 554 (|LOGIC.CHECK-FUNCTIONAL-AXIOM| conclusion nil nil) 555 (|LOGIC.FORMULA-ATBLP| conclusion atbl)))) 556 557 558 ;; Beta-Reduction, Instantiation 559 560 (|LOGIC.SIGMAP| (x) 561 (if (consp x) 562 (and (consp (car x)) 563 (|LOGIC.VARIABLEP| (car (car x))) 564 (|LOGIC.TERMP| (cdr (car x))) 565 (|LOGIC.SIGMAP| (cdr x))) 566 t)) 567 568 (|LOGIC.SIGMA-LISTP| (x) 569 (if (consp x) 570 (and (|LOGIC.SIGMAP| (car x)) 571 (|LOGIC.SIGMA-LISTP| (cdr x))) 572 t)) 573 574 (|LOGIC.SIGMA-LIST-LISTP| (x) 575 (if (consp x) 576 (and (|LOGIC.SIGMA-LISTP| (car x)) 577 (|LOGIC.SIGMA-LIST-LISTP| (cdr x))) 578 t)) 579 580 (|LOGIC.FLAG-SUBSTITUTE| (flag x sigma) 581 (if (equal flag 'term) 582 (cond ((|LOGIC.VARIABLEP| x) 583 (if (lookup x sigma) 584 (cdr (lookup x sigma)) 585 x)) 586 ((|LOGIC.CONSTANTP| x) 587 x) 588 ((|LOGIC.FUNCTIONP| x) 589 (let ((fn (|LOGIC.FUNCTION-NAME| x)) 590 (args (|LOGIC.FUNCTION-ARGS| x))) 591 (|LOGIC.FUNCTION| fn (|LOGIC.FLAG-SUBSTITUTE| 592 'list args sigma)))) 593 ((|LOGIC.LAMBDAP| x) 594 (let ((formals (|LOGIC.LAMBDA-FORMALS| x)) 595 (body (|LOGIC.LAMBDA-BODY| x)) 596 (actuals (|LOGIC.LAMBDA-ACTUALS| x))) 597 (|LOGIC.LAMBDA| formals body (|LOGIC.FLAG-SUBSTITUTE| 598 'list actuals sigma)))) 599 (t nil)) 600 (if (consp x) 601 (cons (|LOGIC.FLAG-SUBSTITUTE| 'term (car x) sigma) 602 (|LOGIC.FLAG-SUBSTITUTE| 'list (cdr x) sigma)) 603 nil))) 604 605 (|LOGIC.SUBSTITUTE| (x sigma) 606 (|LOGIC.FLAG-SUBSTITUTE| 'term x sigma)) 607 608 (|LOGIC.SUBSTITUTE-LIST| (x sigma) 609 (|LOGIC.FLAG-SUBSTITUTE| 'list x sigma)) 610 611 (|LOGIC.SUBSTITUTE-FORMULA| (formula sigma) 612 (let ((type (|LOGIC.FMTYPE| formula))) 613 (cond ((equal type 'por*) 614 (|LOGIC.POR| 615 (|LOGIC.SUBSTITUTE-FORMULA| (|LOGIC.VLHS| formula) sigma) 616 (|LOGIC.SUBSTITUTE-FORMULA| (|LOGIC.VRHS| formula) sigma))) 617 ((equal type 'pnot*) 618 (|LOGIC.PNOT| 619 (|LOGIC.SUBSTITUTE-FORMULA| (|LOGIC.~ARG| formula) sigma))) 620 ((equal type 'pequal*) 621 (|LOGIC.PEQUAL| 622 (|LOGIC.SUBSTITUTE| (|LOGIC.=LHS| formula) sigma) 623 (|LOGIC.SUBSTITUTE| (|LOGIC.=RHS| formula) sigma))) 624 (t nil)))) 625 626 (|LOGIC.INSTANTIATION-OKP| (x atbl) 627 (let ((method (|LOGIC.METHOD| x)) 628 (conclusion (|LOGIC.CONCLUSION| x)) 629 (subproofs (|LOGIC.SUBPROOFS| x)) 630 (extras (|LOGIC.EXTRAS| x))) 631 (and (equal method 'instantiation) 632 (|LOGIC.SIGMAP| extras) 633 (tuplep 1 subproofs) 634 (equal (|LOGIC.SUBSTITUTE-FORMULA| 635 (|LOGIC.CONCLUSION| (first subproofs)) extras) 636 conclusion) 637 (|LOGIC.FORMULA-ATBLP| conclusion atbl)))) 638 639 (|LOGIC.BETA-REDUCTION-OKP| (x atbl) 640 (let ((method (|LOGIC.METHOD| x)) 641 (conclusion (|LOGIC.CONCLUSION| x)) 642 (subproofs (|LOGIC.SUBPROOFS| x)) 643 (extras (|LOGIC.EXTRAS| x))) 644 (and (equal method 'beta-reduction) 645 (equal subproofs nil) 646 (equal extras nil) 647 (|LOGIC.FORMULA-ATBLP| conclusion atbl) 648 (equal (|LOGIC.FMTYPE| conclusion) 'pequal*) 649 (let ((lhs (|LOGIC.=LHS| conclusion)) 650 (rhs (|LOGIC.=RHS| conclusion))) 651 (and (|LOGIC.LAMBDAP| lhs) 652 (let ((formals (|LOGIC.LAMBDA-FORMALS| lhs)) 653 (body (|LOGIC.LAMBDA-BODY| lhs)) 654 (actuals (|LOGIC.LAMBDA-ACTUALS| lhs))) 655 (equal (|LOGIC.SUBSTITUTE| 656 body (pair-lists formals actuals)) 657 rhs))))))) 658 659 ;; Base Evaluation 660 661 (|LOGIC.INITIAL-ARITY-TABLE| () 662 '((if . 3) 663 (equal . 2) 664 (consp . 1) 665 (cons . 2) 666 (car . 1) 667 (cdr . 1) 668 (symbolp . 1) 669 (symbol-< . 2) 670 (natp . 1) 671 (< . 2) 672 (+ . 2) 673 (- . 2))) 674 675 (|LOGIC.BASE-EVALUABLEP| (x) 676 (and (|LOGIC.FUNCTIONP| x) 677 (let ((fn (|LOGIC.FUNCTION-NAME| x)) 678 (args (|LOGIC.FUNCTION-ARGS| x))) 679 (let ((entry (lookup fn (|LOGIC.INITIAL-ARITY-TABLE|)))) 680 (and entry 681 (|LOGIC.CONSTANT-LISTP| args) 682 (tuplep (cdr entry) args)))))) 683 684 (|LOGIC.BASE-EVALUATOR| (x) 685 (let ((fn (|LOGIC.FUNCTION-NAME| x)) 686 (vals (|LOGIC.UNQUOTE-LIST| (|LOGIC.FUNCTION-ARGS| x)))) 687 (list 'quote 688 (cond ((equal fn 'if) 689 (if (first vals) 690 (second vals) 691 (third vals))) 692 ((equal fn 'equal) 693 (equal (first vals) (second vals))) 694 ((equal fn 'consp) 695 (consp (first vals))) 696 ((equal fn 'cons) 697 (cons (first vals) (second vals))) 698 ((equal fn 'car) 699 (car (first vals))) 700 ((equal fn 'cdr) 701 (cdr (first vals))) 702 ((equal fn 'symbolp) 703 (symbolp (first vals))) 704 ((equal fn 'symbol-<) 705 (symbol-< (first vals) (second vals))) 706 ((equal fn 'natp) 707 (natp (first vals))) 708 ((equal fn '<) 709 (< (first vals) (second vals))) 710 ((equal fn '+) 711 (+ (first vals) (second vals))) 712 ((equal fn '-) 713 (- (first vals) (second vals))))))) 714 715 (|LOGIC.BASE-EVAL-OKP| (x atbl) 716 (let ((method (|LOGIC.METHOD| x)) 717 (conclusion (|LOGIC.CONCLUSION| x)) 718 (subproofs (|LOGIC.SUBPROOFS| x)) 719 (extras (|LOGIC.EXTRAS| x))) 720 (and (equal method 'base-eval) 721 (equal subproofs nil) 722 (equal extras nil) 723 (equal (|LOGIC.FMTYPE| conclusion) 'pequal*) 724 (let ((lhs (|LOGIC.=LHS| conclusion)) 725 (rhs (|LOGIC.=RHS| conclusion))) 726 (and (|LOGIC.BASE-EVALUABLEP| lhs) 727 (equal (|LOGIC.BASE-EVALUATOR| lhs) rhs) 728 (|LOGIC.TERM-ATBLP| lhs atbl)))))) 729 730 731 ;; Induction 732 733 (|LOGIC.MAKE-BASIS-STEP| (f qs) 734 (|LOGIC.DISJOIN-FORMULAS| (cons f qs))) 735 736 (|LOGIC.SUBSTITUTE-EACH-SIGMA-INTO-FORMULA| (f x) 737 (if (consp x) 738 (cons (|LOGIC.SUBSTITUTE-FORMULA| f (car x)) 739 (|LOGIC.SUBSTITUTE-EACH-SIGMA-INTO-FORMULA| f (cdr x))) 740 nil)) 741 742 (|LOGIC.MAKE-INDUCTION-STEP| (f q-i sigmas-i) 743 (|LOGIC.DISJOIN-FORMULAS| 744 (cons f (cons (|LOGIC.PNOT| q-i) 745 (|LOGIC.SUBSTITUTE-EACH-SIGMA-INTO-FORMULA| 746 (|LOGIC.PNOT| f) sigmas-i))))) 747 748 (|LOGIC.MAKE-INDUCTION-STEPS| (f qs all-sigmas) 749 (if (consp qs) 750 (cons (|LOGIC.MAKE-INDUCTION-STEP| f (car qs) (car all-sigmas)) 751 (|LOGIC.MAKE-INDUCTION-STEPS| f (cdr qs) (cdr all-sigmas))) 752 nil)) 753 754 (|LOGIC.MAKE-ORDINAL-STEP| (m) 755 (|LOGIC.PEQUAL| (|LOGIC.FUNCTION| 'ordp (list m)) ''t)) 756 757 (|LOGIC.MAKE-MEASURE-STEP| (m q-i sigma-i-j) 758 (|LOGIC.POR| 759 (|LOGIC.PNOT| q-i) 760 (|LOGIC.PEQUAL| 761 (|LOGIC.FUNCTION| 'ord< (list (|LOGIC.SUBSTITUTE| m sigma-i-j) m)) 762 ''t))) 763 764 (|LOGIC.MAKE-MEASURE-STEPS| (m q-i sigmas-i) 765 (if (consp sigmas-i) 766 (cons (|LOGIC.MAKE-MEASURE-STEP| m q-i (car sigmas-i)) 767 (|LOGIC.MAKE-MEASURE-STEPS| m q-i (cdr sigmas-i))) 768 nil)) 769 770 (|LOGIC.MAKE-ALL-MEASURE-STEPS| (m qs all-sigmas) 771 (if (consp all-sigmas) 772 (app (|LOGIC.MAKE-MEASURE-STEPS| m (car qs) (car all-sigmas)) 773 (|LOGIC.MAKE-ALL-MEASURE-STEPS| m (cdr qs) (cdr all-sigmas))) 774 nil)) 775 776 (|LOGIC.INDUCTION-OKP| (x) 777 (let ((method (|LOGIC.METHOD| x)) 778 (conclusion (|LOGIC.CONCLUSION| x)) 779 (subproofs (|LOGIC.SUBPROOFS| x)) 780 (extras (|LOGIC.EXTRAS| x))) 781 (and 782 (equal method 'induction) 783 (tuplep 3 extras) 784 (let ((m (first extras)) 785 (qs (second extras)) 786 (all-sigmas (third extras)) 787 (subconcs (|LOGIC.STRIP-CONCLUSIONS| subproofs))) 788 (and (|LOGIC.TERMP| m) 789 (|LOGIC.FORMULA-LISTP| qs) 790 (|LOGIC.SIGMA-LIST-LISTP| all-sigmas) 791 (equal (len qs) (len all-sigmas)) 792 (memberp (|LOGIC.MAKE-BASIS-STEP| conclusion qs) subconcs) 793 (subsetp (|LOGIC.MAKE-INDUCTION-STEPS| conclusion qs all-sigmas) 794 subconcs) 795 (memberp (|LOGIC.MAKE-ORDINAL-STEP| m) subconcs) 796 (subsetp (|LOGIC.MAKE-ALL-MEASURE-STEPS| m qs all-sigmas) 797 subconcs)))))) 798 799 800 ;; Proof Checking 801 802 (|LOGIC.APPEAL-STEP-OKP| (x axioms thms atbl) 803 (let ((how (|LOGIC.METHOD| x))) 804 (cond ((equal how 'axiom) 805 (|LOGIC.AXIOM-OKP| x axioms atbl)) 806 ((equal how 'theorem) 807 (|LOGIC.THEOREM-OKP| x thms atbl)) 808 ((equal how 'propositional-schema) 809 (|LOGIC.PROPOSITIONAL-SCHEMA-OKP| x atbl)) 810 ((equal how 'functional-equality) 811 (|LOGIC.FUNCTIONAL-EQUALITY-OKP| x atbl)) 812 ((equal how 'beta-reduction) 813 (|LOGIC.BETA-REDUCTION-OKP| x atbl)) 814 ((equal how 'expansion) 815 (|LOGIC.EXPANSION-OKP| x atbl)) 816 ((equal how 'contraction) 817 (|LOGIC.CONTRACTION-OKP| x)) 818 ((equal how 'associativity) 819 (|LOGIC.ASSOCIATIVITY-OKP| x)) 820 ((equal how 'cut) 821 (|LOGIC.CUT-OKP| x)) 822 ((equal how 'instantiation) 823 (|LOGIC.INSTANTIATION-OKP| x atbl)) 824 ((equal how 'induction) 825 (|LOGIC.INDUCTION-OKP| x)) 826 ((equal how 'base-eval) 827 (|LOGIC.BASE-EVAL-OKP| x atbl)) 828 (t nil)))) 829 830 (|LOGIC.FLAG-PROOFP| (flag x axioms thms atbl) 831 (if (equal flag 'proof) 832 (and (|LOGIC.APPEAL-STEP-OKP| x axioms thms atbl) 833 (|LOGIC.FLAG-PROOFP| 'list (|LOGIC.SUBPROOFS| x) axioms thms atbl)) 834 (if (consp x) 835 (and (|LOGIC.FLAG-PROOFP| 'proof (car x) axioms thms atbl) 836 (|LOGIC.FLAG-PROOFP| 'list (cdr x) axioms thms atbl)) 837 t))) 838 839 (|LOGIC.PROOFP| (x axioms thms atbl) 840 (|LOGIC.FLAG-PROOFP| 'proof x axioms thms atbl)) 841 842 (|LOGIC.PROVABLE-WITNESS| 843 (x axioms thms atbl) 844 (error '(|LOGIC.PROVABLE-WITNESS| 845 proof 846 (x axioms thms atbl) 847 (and (|LOGIC.APPEALP| proof) 848 (|LOGIC.PROOFP| proof axioms thms atbl) 849 (equal (|LOGIC.CONCLUSION| proof) x))))) 850 851 (|LOGIC.PROVABLEP| (x axioms thms atbl) 852 (let ((proof (|LOGIC.PROVABLE-WITNESS| x axioms thms atbl))) 853 (and (|LOGIC.APPEALP| proof) 854 (|LOGIC.PROOFP| proof axioms thms atbl) 855 (equal (|LOGIC.CONCLUSION| proof) x)))) 856 857 ;; SUPPORTING ABBREVIATIONS 858 859 (remove-all (a x) 860 (if (consp x) 861 (if (equal a (car x)) 862 (remove-all a (cdr x)) 863 (cons (car x) (remove-all a (cdr x)))) 864 nil)) 865 866 (remove-duplicates (x) 867 (if (consp x) 868 (if (memberp (car x) (cdr x)) 869 (remove-duplicates (cdr x)) 870 (cons (car x) (remove-duplicates (cdr x)))) 871 nil)) 872 873 (difference (x y) 874 (if (consp x) 875 (if (memberp (car x) y) 876 (difference (cdr x) y) 877 (cons (car x) 878 (difference (cdr x) y))) 879 nil)) 880 881 (strip-firsts (x) 882 (if (consp x) 883 (cons (first (car x)) 884 (strip-firsts (cdr x))) 885 nil)) 886 887 (strip-seconds (x) 888 (if (consp x) 889 (cons (second (car x)) 890 (strip-seconds (cdr x))) 891 nil)) 892 893 (tuple-listp (n x) 894 (if (consp x) 895 (and (tuplep n (car x)) 896 (tuple-listp n (cdr x))) 897 t)) 898 899 (sort-symbols-insert 900 (a x) 901 (if (consp x) 902 (if (symbol-< a (car x)) 903 (cons a x) 904 (cons (car x) 905 (sort-symbols-insert a (cdr x)))) 906 (list a))) 907 908 (sort-symbols 909 (x) 910 (if (consp x) 911 (sort-symbols-insert (car x) 912 (sort-symbols (cdr x))) 913 nil)) 914 915 (|LOGIC.TRANSLATE-AND-TERM| (args) 916 (if (consp args) 917 (if (consp (cdr args)) 918 (|LOGIC.FUNCTION| 919 'if 920 (list (first args) 921 (|LOGIC.TRANSLATE-AND-TERM| (cdr args)) 922 ''nil)) 923 (first args)) 924 ''t)) 925 926 (|LOGIC.TRANSLATE-LET-TERM| (vars terms body) 927 (let* ((body-vars (remove-duplicates (|LOGIC.TERM-VARS| body))) 928 (id-vars (sort-symbols (difference body-vars vars))) 929 (formals (app id-vars vars)) 930 (actuals (app id-vars terms))) 931 (|LOGIC.LAMBDA| formals body actuals))) 932 933 (|LOGIC.TRANSLATE-OR-TERM| (args) 934 (if (consp args) 935 (if (consp (cdr args)) 936 (let* ((else-term (|LOGIC.TRANSLATE-OR-TERM| (cdr args))) 937 (cheap-p (or (|LOGIC.VARIABLEP| (car args)) 938 (|LOGIC.CONSTANTP| (car args))))) 939 (if (or cheap-p 940 (memberp 'special-var-for-or 941 (|LOGIC.TERM-VARS| else-term))) 942 (|LOGIC.FUNCTION| 'if (list (car args) (car args) else-term)) 943 (|LOGIC.TRANSLATE-LET-TERM| 944 (list 'special-var-for-or) 945 (list (car args)) 946 (|LOGIC.FUNCTION| 'if (list 'special-var-for-or 947 'special-var-for-or 948 else-term))))) 949 (first args)) 950 ''nil)) 951 952 (|LOGIC.TRANSLATE-LIST-TERM| (args) 953 (if (consp args) 954 (|LOGIC.FUNCTION| 955 'cons 956 (list (car args) 957 (|LOGIC.TRANSLATE-LIST-TERM| (cdr args)))) 958 ''nil)) 959 960 (|LOGIC.TRANSLATE-COND-TERM| (tests thens) 961 (if (consp tests) 962 (let ((test1 (car tests)) 963 (then1 (car thens))) 964 (|LOGIC.FUNCTION| 965 'if 966 (list test1 967 then1 968 (|LOGIC.TRANSLATE-COND-TERM| (cdr tests) 969 (cdr thens))))) 970 ''nil)) 971 972 (|LOGIC.TRANSLATE-LET*-TERM| (vars terms body) 973 (if (consp vars) 974 (|LOGIC.TRANSLATE-LET-TERM| 975 (list (car vars)) 976 (list (car terms)) 977 (|LOGIC.TRANSLATE-LET*-TERM| (cdr vars) (cdr terms) body)) 978 body)) 979 980 (|LOGIC.FLAG-TRANSLATE| (flag x) 981 (if (equal flag 'term) 982 (cond ((natp x) 983 (list 'quote x)) 984 ((symbolp x) 985 (if (or (equal x nil) 986 (equal x t)) 987 (list 'quote x) 988 x)) 989 ((symbolp (car x)) 990 (let ((fn (car x))) 991 (cond ((equal fn 'quote) 992 (if (tuplep 2 x) 993 x 994 nil)) 995 ((memberp fn '(first second third fourth fifth)) 996 (and (tuplep 2 x) 997 (let ((arg (|LOGIC.FLAG-TRANSLATE| 'term (second x)))) 998 (and arg 999 (let* ((|1CDR| (|LOGIC.FUNCTION| 'cdr (list arg))) 1000 (|2CDR| (|LOGIC.FUNCTION| 'cdr (list |1CDR|))) 1001 (|3CDR| (|LOGIC.FUNCTION| 'cdr (list |2CDR|))) 1002 (|4CDR| (|LOGIC.FUNCTION| 'cdr (list |3CDR|)))) 1003 (|LOGIC.FUNCTION| 1004 'car 1005 (list (cond ((equal fn 'first) arg) 1006 ((equal fn 'second) |1CDR|) 1007 ((equal fn 'third) |2CDR|) 1008 ((equal fn 'fourth) |3CDR|) 1009 (t |4CDR|))))))))) 1010 ((memberp fn '(and or list)) 1011 (and (true-listp (cdr x)) 1012 (let ((arguments+ (|LOGIC.FLAG-TRANSLATE| 'list (cdr x)))) 1013 (and (car arguments+) 1014 (cond ((equal fn 'and) 1015 (|LOGIC.TRANSLATE-AND-TERM| (cdr arguments+))) 1016 ((equal fn 'or) 1017 (|LOGIC.TRANSLATE-OR-TERM| (cdr arguments+))) 1018 (t 1019 (|LOGIC.TRANSLATE-LIST-TERM| (cdr arguments+)))))))) 1020 ((equal fn 'cond) 1021 (and (true-listp (cdr x)) 1022 (tuple-listp 2 (cdr x)) 1023 (let* ((tests (strip-firsts (cdr x))) 1024 (thens (strip-seconds (cdr x))) 1025 (tests+ (|LOGIC.FLAG-TRANSLATE| 'list tests)) 1026 (thens+ (|LOGIC.FLAG-TRANSLATE| 'list thens))) 1027 (and (car tests+) 1028 (car thens+) 1029 (|LOGIC.TRANSLATE-COND-TERM| (cdr tests+) 1030 (cdr thens+)))))) 1031 ((memberp fn '(let let*)) 1032 (and (tuplep 3 x) 1033 (let ((pairs (second x)) 1034 (body (|LOGIC.FLAG-TRANSLATE| 'term (third x)))) 1035 (and body 1036 (true-listp pairs) 1037 (tuple-listp 2 pairs) 1038 (let* ((vars (strip-firsts pairs)) 1039 (terms (strip-seconds pairs)) 1040 (terms+ (|LOGIC.FLAG-TRANSLATE| 'list terms))) 1041 (and (car terms+) 1042 (|LOGIC.VARIABLE-LISTP| vars) 1043 (cond ((equal fn 'let) 1044 (and (uniquep vars) 1045 (|LOGIC.TRANSLATE-LET-TERM| vars 1046 (cdr terms+) 1047 body))) 1048 (t 1049 (|LOGIC.TRANSLATE-LET*-TERM| vars 1050 (cdr terms+) 1051 body))))))))) 1052 ((|LOGIC.FUNCTION-NAMEP| fn) 1053 (and (true-listp (cdr x)) 1054 (let ((arguments+ (|LOGIC.FLAG-TRANSLATE| 'list (cdr x)))) 1055 (and (car arguments+) 1056 (|LOGIC.FUNCTION| fn (cdr arguments+)))))) 1057 (t 1058 nil)))) 1059 ((and (tuplep 3 (car x)) 1060 (true-listp (cdr x))) 1061 (let* ((lambda-symbol (first (car x))) 1062 (vars (second (car x))) 1063 (body (third (car x))) 1064 (new-body (|LOGIC.FLAG-TRANSLATE| 'term body)) 1065 (actuals+ (|LOGIC.FLAG-TRANSLATE| 'list (cdr x)))) 1066 (and (equal lambda-symbol 'lambda) 1067 (true-listp vars) 1068 (|LOGIC.VARIABLE-LISTP| vars) 1069 (uniquep vars) 1070 new-body 1071 (subsetp (|LOGIC.TERM-VARS| new-body) vars) 1072 (car actuals+) 1073 (equal (len vars) (len (cdr actuals+))) 1074 (|LOGIC.LAMBDA| vars new-body (cdr actuals+))))) 1075 (t 1076 nil)) 1077 (if (consp x) 1078 (let ((first (|LOGIC.FLAG-TRANSLATE| 'term (car x))) 1079 (rest (|LOGIC.FLAG-TRANSLATE| 'list (cdr x)))) 1080 (if (and first (car rest)) 1081 (cons t (cons first (cdr rest))) 1082 (cons nil nil))) 1083 (cons t nil)))) 1084 1085 (|LOGIC.TRANSLATE| (x) (|LOGIC.FLAG-TRANSLATE| 'term x)) 1086 1087 1088 ;; TERMINATION OBLIGATIONS 1089 1090 (cons-onto-ranges 1091 (a x) 1092 (if (consp x) 1093 (cons (cons (car (car x)) 1094 (cons a (cdr (car x)))) 1095 (cons-onto-ranges a (cdr x))) 1096 nil)) 1097 1098 (|LOGIC.SUBSTITUTE-CALLMAP| 1099 (x sigma) 1100 (if (consp x) 1101 (let ((actuals (car (car x))) 1102 (rulers (cdr (car x)))) 1103 (cons (cons (|LOGIC.SUBSTITUTE-LIST| actuals sigma) 1104 (|LOGIC.SUBSTITUTE-LIST| rulers sigma)) 1105 (|LOGIC.SUBSTITUTE-CALLMAP| (cdr x) sigma))) 1106 nil)) 1107 1108 (|LOGIC.FLAG-CALLMAP| 1109 (flag f x) 1110 (if (equal flag 'term) 1111 (cond ((|LOGIC.CONSTANTP| x) 1112 nil) 1113 ((|LOGIC.VARIABLEP| x) 1114 nil) 1115 ((|LOGIC.FUNCTIONP| x) 1116 (let ((name (|LOGIC.FUNCTION-NAME| x)) 1117 (args (|LOGIC.FUNCTION-ARGS| x))) 1118 (cond ((and (equal name 'if) 1119 (equal (len args) 3)) 1120 (let ((test-calls 1121 (|LOGIC.FLAG-CALLMAP| 'term f (first args))) 1122 (true-calls 1123 (cons-onto-ranges 1124 (first args) 1125 (|LOGIC.FLAG-CALLMAP| 'term f (second args)))) 1126 (else-calls 1127 (cons-onto-ranges 1128 (|LOGIC.FUNCTION| 'not (list (first args))) 1129 (|LOGIC.FLAG-CALLMAP| 'term f (third args))))) 1130 (app test-calls (app true-calls else-calls)))) 1131 ((equal name f) 1132 (let ((this-call (cons args nil)) 1133 (child-calls (|LOGIC.FLAG-CALLMAP| 'list f args))) 1134 (cons this-call child-calls))) 1135 (t 1136 (|LOGIC.FLAG-CALLMAP| 'list f args))))) 1137 ((|LOGIC.LAMBDAP| x) 1138 (let ((formals (|LOGIC.LAMBDA-FORMALS| x)) 1139 (body (|LOGIC.LAMBDA-BODY| x)) 1140 (actuals (|LOGIC.LAMBDA-ACTUALS| x))) 1141 (let ((actuals-calls (|LOGIC.FLAG-CALLMAP| 'list f actuals)) 1142 (body-calls (|LOGIC.FLAG-CALLMAP| 'term f body)) 1143 (sigma (pair-lists formals actuals))) 1144 (app actuals-calls 1145 (|LOGIC.SUBSTITUTE-CALLMAP| body-calls sigma)))))) 1146 (if (consp x) 1147 (app (|LOGIC.FLAG-CALLMAP| 'term f (car x)) 1148 (|LOGIC.FLAG-CALLMAP| 'list f (cdr x))) 1149 nil))) 1150 1151 (|LOGIC.CALLMAP| (f x) 1152 (|LOGIC.FLAG-CALLMAP| 'term f x)) 1153 1154 (repeat (a n) 1155 (if (zp n) 1156 nil 1157 (cons a (repeat a (- n 1))))) 1158 1159 (|LOGIC.PEQUAL-LIST| (x y) 1160 (if (and (consp x) 1161 (consp y)) 1162 (cons (|LOGIC.PEQUAL| (car x) (car y)) 1163 (|LOGIC.PEQUAL-LIST| (cdr x) (cdr y))) 1164 nil)) 1165 1166 (|LOGIC.PROGRESS-OBLIGATION| (measure formals actuals rulers) 1167 (let* ((sigma (pair-lists formals actuals)) 1168 (|M/SIGMA| (|LOGIC.SUBSTITUTE| measure sigma)) 1169 (ord-term (|LOGIC.FUNCTION| 'ord< (list |M/SIGMA| measure)))) 1170 (|LOGIC.DISJOIN-FORMULAS| 1171 (cons (|LOGIC.PEQUAL| ord-term ''t) 1172 (|LOGIC.PEQUAL-LIST| rulers (repeat ''nil (len rulers))))))) 1173 1174 (|LOGIC.PROGRESS-OBLIGATIONS| 1175 (measure formals callmap) 1176 (if (consp callmap) 1177 (let* ((entry (car callmap)) 1178 (actuals (car entry)) 1179 (rulers (cdr entry))) 1180 (cons (|LOGIC.PROGRESS-OBLIGATION| measure formals actuals rulers) 1181 (|LOGIC.PROGRESS-OBLIGATIONS| measure formals (cdr callmap)))) 1182 nil)) 1183 1184 (|LOGIC.TERMINATION-OBLIGATIONS| 1185 (name formals body measure) 1186 (let ((callmap (|LOGIC.CALLMAP| name body))) 1187 (if callmap 1188 (cons (|LOGIC.PEQUAL| (|LOGIC.FUNCTION| 'ordp (list measure)) ''t) 1189 (|LOGIC.PROGRESS-OBLIGATIONS| measure formals callmap)) 1190 nil))) 1191 1192 1193 (|CORE.INITIAL-ATBL| () 1194 (app '((not . 1) 1195 (rank . 1) 1196 (ordp . 1) 1197 (ord< . 2)) 1198 (|LOGIC.INITIAL-ARITY-TABLE|))) 1199 1200 (|CORE.INITIAL-AXIOMS| () 1201 (app '( ;; reflexivity 1202 (pequal* x x) 1203 1204 ;; equality 1205 (por* (pnot* (pequal* x1 y1)) 1206 (por* (pnot* (pequal* x2 y2)) 1207 (por* (pnot* (pequal* x1 x2)) 1208 (pequal* y1 y2)))) 1209 1210 ;; t-not-nil 1211 (pnot* (pequal* 't 'nil)) 1212 1213 ;; equal-when-same 1214 (por* (pnot* (pequal* x y)) 1215 (pequal* (equal x y) 't)) 1216 1217 ;; equal-when-diff 1218 (por* (pequal* x y) 1219 (pequal* (equal x y) 'nil)) 1220 1221 ;; if-when-nil 1222 (por* (pnot* (pequal* x 'nil)) 1223 (pequal* (if x y z) z)) 1224 1225 ;; if-when-not-nil 1226 (por* (pequal* x 'nil) 1227 (pequal* (if x y z) y)) 1228 1229 ;; consp-of-cons 1230 (pequal* (consp (cons x y)) 't) 1231 1232 ;; car-of-cons 1233 (pequal* (car (cons x y)) x) 1234 1235 ;; cdr-of-cons 1236 (pequal* (cdr (cons x y)) y) 1237 1238 ;; consp-nil-or-t 1239 (por* (pequal* (consp x) 'nil) 1240 (pequal* (consp x) 't)) 1241 1242 ;; car-when-not-consp 1243 (por* (pnot* (pequal* (consp x) 'nil)) 1244 (pequal* (car x) 'nil)) 1245 1246 ;; cdr-when-not-consp 1247 (por* (pnot* (pequal* (consp x) 'nil)) 1248 (pequal* (cdr x) 'nil)) 1249 1250 ;; cons-of-car-and-cdr 1251 (por* (pequal* (consp x) 'nil) 1252 (pequal* (cons (car x) (cdr x)) x)) 1253 1254 ;; symbolp-nil-or-t 1255 (por* (pequal* (symbolp x) 'nil) 1256 (pequal* (symbolp x) 't)) 1257 1258 ;; symbol-<-nil-or-t 1259 (por* (pequal* (symbol-< x y) 'nil) 1260 (pequal* (symbol-< x y) 't)) 1261 1262 ;; irreflexivity-of-symbol-< 1263 (pequal* (symbol-< x x) 'nil) 1264 1265 ;; antisymmetry-of-symbol-< 1266 (por* (pequal* (symbol-< x y) 'nil) 1267 (pequal* (symbol-< y x) 'nil)) 1268 1269 ;; transitivity-of-symbol-< 1270 (por* (pequal* (symbol-< x y) 'nil) 1271 (por* (pequal* (symbol-< y z) 'nil) 1272 (pequal* (symbol-< x z) 't))) 1273 1274 ;; trichotomy-of-symbol-< 1275 (por* (pequal* (symbolp x) 'nil) 1276 (por* (pequal* (symbolp y) 'nil) 1277 (por* (pequal* (symbol-< x y) 't) 1278 (por* (pequal* (symbol-< y x) 't) 1279 (pequal* x y))))) 1280 1281 ;; symbol-<-completion-left 1282 (por* (pequal* (symbolp x) 't) 1283 (pequal* (symbol-< x y) 1284 (symbol-< 'nil y))) 1285 1286 ;; symbol-<-completion-right 1287 (por* (pequal* (symbolp y) 't) 1288 (pequal* (symbol-< x y) 1289 (symbol-< x 'nil))) 1290 1291 ;; disjoint-symbols-and-naturals 1292 (por* (pequal* (symbolp x) 'nil) 1293 (pequal* (natp x) 'nil)) 1294 1295 ;; disjoint-symbols-and-conses 1296 (por* (pequal* (symbolp x) 'nil) 1297 (pequal* (consp x) 'nil)) 1298 1299 ;; disjoint-naturals-and-conses 1300 (por* (pequal* (natp x) 'nil) 1301 (pequal* (consp x) 'nil)) 1302 1303 ;; natp-nil-or-t 1304 (por* (pequal* (natp x) 'nil) 1305 (pequal* (natp x) 't)) 1306 1307 ;; natp-of-plus 1308 (pequal* (natp (+ a b)) 't) 1309 1310 ;; commutativity-of-+ 1311 (pequal* (+ a b) (+ b a)) 1312 1313 ;; associativity-of-+ 1314 (pequal* (+ (+ a b) c) 1315 (+ a (+ b c))) 1316 1317 ;; plus-when-not-natp-left 1318 (por* (pequal* (natp a) 't) 1319 (pequal* (+ a b) (+ '0 b))) 1320 1321 ;; plus-of-zero-when-natural 1322 (por* (pequal* (natp a) 'nil) 1323 (pequal* (+ a '0) a)) 1324 1325 ;; <-nil-or-t 1326 (por* (pequal* (< x y) 'nil) 1327 (pequal* (< x y) 't)) 1328 1329 ;; irreflexivity-of-< 1330 (pequal* (< a a) 'nil) 1331 1332 ;; less-of-zero-right 1333 (pequal* (< a '0) 'nil) 1334 1335 ;; less-of-zero-left-when-natp 1336 (por* (pequal* (natp a) 'nil) 1337 (pequal* (< '0 a) 1338 (if (equal a '0) 'nil 't))) 1339 1340 ;; less-completion-left 1341 (por* (pequal* (natp a) 't) 1342 (pequal* (< a b) 1343 (< '0 b))) 1344 1345 ;; less-completion-right 1346 (por* (pequal* (natp b) 't) 1347 (pequal* (< a b) 1348 'nil)) 1349 1350 ;; transitivity-of-< 1351 (por* (pequal* (< a b) 'nil) 1352 (por* (pequal* (< b c) 'nil) 1353 (pequal* (< a c) 't))) 1354 1355 ;; trichotomy-of-<-when-natp 1356 (por* (pequal* (natp a) 'nil) 1357 (por* (pequal* (natp b) 'nil) 1358 (por* (pequal* (< a b) 't) 1359 (por* (pequal* (< b a) 't) 1360 (pequal* a b))))) 1361 1362 ;; one-plus-trick 1363 (por* (pequal* (< a b) 'nil) 1364 (pequal* (< b (+ '1 a)) 'nil)) 1365 1366 ;; natural-less-than-one-is-zero 1367 (por* (pequal* (natp a) 'nil) 1368 (por* (pequal* (< a '1) 'nil) 1369 (pequal* a '0))) 1370 1371 ;; less-than-of-plus-and-plus 1372 (pequal* (< (+ a b) (+ a c)) 1373 (< b c)) 1374 1375 ;; natp-of-minus 1376 (pequal* (natp (- a b)) 't) 1377 1378 ;; minus-when-subtrahend-as-large 1379 (por* (pequal* (< b a) 't) 1380 (pequal* (- a b) '0)) 1381 1382 ;; minus-cancels-summand-right 1383 (pequal* (- (+ a b) b) 1384 (if (natp a) a '0)) 1385 1386 ;; less-of-minus-left 1387 (por* (pequal* (< b a) 'nil) 1388 (pequal* (< (- a b) c) 1389 (< a (+ b c)))) 1390 1391 ;; less-of-minus-right 1392 (pequal* (< a (- b c)) 1393 (< (+ a c) b)) 1394 1395 ;; plus-of-minus-right 1396 (por* (pequal* (< c b) 'nil) 1397 (pequal* (+ a (- b c)) 1398 (- (+ a b) c))) 1399 1400 ;; minus-of-minus-right 1401 (por* (pequal* (< c b) 'nil) 1402 (pequal* (- a (- b c)) 1403 (- (+ a c) b))) 1404 1405 ;; minus-of-minus-left 1406 (pequal* (- (- a b) c) 1407 (- a (+ b c))) 1408 1409 ;; equal-of-minus-property 1410 (por* (pequal* (< b a) 'nil) 1411 (pequal* (equal (- a b) c) 1412 (equal a (+ b c)))) 1413 1414 ;; closed-universe 1415 (por* (pequal* (natp x) 't) 1416 (por* (pequal* (symbolp x) 't) 1417 (pequal* (consp x) 't)))) 1418 1419 (list 1420 ;; definition-of-not 1421 (|LOGIC.PEQUAL| '(not x) 1422 (|LOGIC.TRANSLATE| '(if x nil t))) 1423 1424 ;; definition-of-rank 1425 (|LOGIC.PEQUAL| '(rank x) 1426 (|LOGIC.TRANSLATE| '(if (consp x) 1427 (+ 1 1428 (+ (rank (car x)) 1429 (rank (cdr x)))) 1430 0))) 1431 1432 ;; definition-of-ord< 1433 (|LOGIC.PEQUAL| '(ord< x y) 1434 (|LOGIC.TRANSLATE| '(cond ((not (consp x)) 1435 (if (consp y) 1436 t 1437 (< x y))) 1438 ((not (consp y)) 1439 nil) 1440 ((not (equal (car (car x)) 1441 (car (car y)))) 1442 (ord< (car (car x)) 1443 (car (car y)))) 1444 ((not (equal (cdr (car x)) 1445 (cdr (car y)))) 1446 (< (cdr (car x)) 1447 (cdr (car y)))) 1448 (t 1449 (ord< (cdr x) (cdr y)))))) 1450 1451 ;; definition-of-ordp 1452 (|LOGIC.PEQUAL| '(ordp x) 1453 (|LOGIC.TRANSLATE| '(if (not (consp x)) 1454 (natp x) 1455 (and (consp (car x)) 1456 (ordp (car (car x))) 1457 (not (equal (car (car x)) 0)) 1458 (< 0 (cdr (car x))) 1459 (ordp (cdr x)) 1460 (if (consp (cdr x)) 1461 (ord< (car (car (cdr x))) 1462 (car (car x))) 1463 t)))))))) 1464 1465 (|CORE.STATE| (axioms thms atbl checker ftbl) 1466 (list axioms thms atbl checker ftbl)) 1467 1468 (|CORE.AXIOMS| (x) (first x)) 1469 (|CORE.THMS| (x) (second x)) 1470 (|CORE.ATBL| (x) (third x)) 1471 (|CORE.CHECKER| (x) (fourth x)) 1472 (|CORE.FTBL| (x) (fifth x)) 1473 1474 (|CORE.CHECK-PROOF| 1475 (checker proof axioms thms atbl) 1476 (funcall checker proof axioms thms atbl)) 1477 1478 (|CORE.CHECK-PROOF-LIST| 1479 (checker proofs axioms thms atbl) 1480 (if (consp proofs) 1481 (and (|CORE.CHECK-PROOF| checker (car proofs) axioms thms atbl) 1482 (|CORE.CHECK-PROOF-LIST| checker (cdr proofs) axioms thms atbl)) 1483 t)) 1484 1485 (|LOGIC.SOUNDNESS-CLAIM| 1486 (name) 1487 (|LOGIC.POR| 1488 '(pequal* (|LOGIC.APPEALP| x) 'nil) 1489 (|LOGIC.POR| 1490 (|LOGIC.PEQUAL| (|LOGIC.FUNCTION| name '(x axioms thms atbl)) 1491 ''nil) 1492 '(pnot* (pequal* (|LOGIC.PROVABLEP| (|LOGIC.CONCLUSION| x) 1493 axioms thms atbl) 1494 'nil))))) 1495 1496 (|CORE.ADMIT-SWITCH| 1497 (cmd state) 1498 ;; Returns a new state or calls error. 1499 ;; CMD should be (SWITCH NAME) 1500 (if (or (not (tuplep 2 cmd)) 1501 (not (equal (first cmd) 'switch))) 1502 (error (list 'admit-switch 'invalid-cmd cmd)) 1503 (let ((axioms (|CORE.AXIOMS| state)) 1504 (thms (|CORE.THMS| state)) 1505 (atbl (|CORE.ATBL| state)) 1506 (ftbl (|CORE.FTBL| state)) 1507 (name (second cmd))) 1508 (cond ((not (|LOGIC.FUNCTION-NAMEP| name)) 1509 (error (list 'admit-switch 'invalid-name name))) 1510 ((not (memberp (|LOGIC.SOUNDNESS-CLAIM| name) 1511 (|CORE.THMS| state))) 1512 (error (list 'admit-switch 'not-verified name))) 1513 (t 1514 (|CORE.STATE| axioms thms atbl name ftbl)))))) 1515 1516 (|CORE.ADMIT-THEOREM| 1517 (cmd state) 1518 ;; Returns a new state or calls error. 1519 ;; CMD should be (VERIFY NAME FORMULA PROOF) 1520 (if (or (not (tuplep 4 cmd)) 1521 (not (equal (first cmd) 'verify))) 1522 (error (list 'admit-theorem 'invalid-cmd cmd)) 1523 (let ((axioms (|CORE.AXIOMS| state)) 1524 (thms (|CORE.THMS| state)) 1525 (atbl (|CORE.ATBL| state)) 1526 (checker (|CORE.CHECKER| state)) 1527 (ftbl (|CORE.FTBL| state)) 1528 (name (second cmd)) 1529 (formula (third cmd)) 1530 (proof (fourth cmd))) 1531 (cond 1532 ((not (|LOGIC.FORMULAP| formula)) 1533 (error (list 'admit-theorem 'not-formulap name))) 1534 ((not (|LOGIC.FORMULA-ATBLP| formula atbl)) 1535 (error (list 'admit-theorem 'not-formula-atblp 1536 name formula atbl))) 1537 ((not (|LOGIC.APPEALP| proof)) 1538 (error (list 'admit-theorem 'not-appealp name))) 1539 ((not (equal (|LOGIC.CONCLUSION| proof) formula)) 1540 (error (list 'admit-theorem 'wrong-conclusion name))) 1541 ((not (|CORE.CHECK-PROOF| checker proof axioms thms atbl)) 1542 (error (list 'admit-theorem 'proof-rejected name))) 1543 (t 1544 (if (memberp formula thms) 1545 state 1546 (|CORE.STATE| axioms (cons formula thms) atbl checker ftbl))))))) 1547 1548 (|CORE.ADMIT-DEFUN| 1549 (cmd state) 1550 ;; Returns a new state or calls error. 1551 ;; CMD should be (DEFINE NAME FORMALS BODY MEASURE PROOF-LIST) 1552 (if (or (not (tuplep 6 cmd)) 1553 (not (equal (car cmd) 'define))) 1554 (error (list 'admit-defun 'invalid-cmd cmd)) 1555 (let* ((axioms (|CORE.AXIOMS| state)) 1556 (thms (|CORE.THMS| state)) 1557 (atbl (|CORE.ATBL| state)) 1558 (checker (|CORE.CHECKER| state)) 1559 (ftbl (|CORE.FTBL| state)) 1560 (name (second cmd)) 1561 (formals (third cmd)) 1562 (raw-body (fourth cmd)) 1563 (raw-measure (fifth cmd)) 1564 (proofs (fifth (cdr cmd))) 1565 (body (|LOGIC.TRANSLATE| raw-body)) 1566 (measure (|LOGIC.TRANSLATE| raw-measure)) 1567 (arity (len formals)) 1568 (new-atbl (cons (cons name arity) atbl)) 1569 (obligations (|LOGIC.TERMINATION-OBLIGATIONS| 1570 name formals body measure))) 1571 (cond ((not (|LOGIC.FUNCTION-NAMEP| name)) 1572 (error (list 'admit-defun 'bad-name name))) 1573 ((not (true-listp formals)) 1574 (error (list 'admit-defun 'bad-formals name))) 1575 ((not (|LOGIC.VARIABLE-LISTP| formals)) 1576 (error (list 'admit-defun 'bad-formals name))) 1577 ((not (uniquep formals)) 1578 (error (list 'admit-defun 'duplicated-formals name))) 1579 ((not (|LOGIC.TERMP| body)) 1580 (error (list 'admit-defun 'bad-body name 1581 body raw-body cmd))) 1582 ((not (|LOGIC.TERMP| measure)) 1583 (error (list 'admit-defun 'bad-measure name))) 1584 ((not (subsetp (|LOGIC.TERM-VARS| body) formals)) 1585 (error (list 'admit-defun 'free-vars-in-body name))) 1586 ((not (subsetp (|LOGIC.TERM-VARS| measure) formals)) 1587 (error (list 'admit-defun 'free-vars-in-measure name))) 1588 ((not (|LOGIC.TERM-ATBLP| body new-atbl)) 1589 (error (list 'admit-defun 'bad-arity-in-body name))) 1590 ((not (|LOGIC.TERM-ATBLP| measure new-atbl)) 1591 (error (list 'admit-defun 'bad-arity-in-measure name))) 1592 ((not (|LOGIC.APPEAL-LISTP| proofs)) 1593 (error (list 'admit-defun 'proofs-not-appeals name))) 1594 ((not (equal (|LOGIC.STRIP-CONCLUSIONS| proofs) obligations)) 1595 (error (list 'admit-defun 'proofs-wrong-conclusions name))) 1596 ((not (|CORE.CHECK-PROOF-LIST| checker proofs axioms thms new-atbl)) 1597 (error (list 'admit-defun 'proof-rejected name))) 1598 (t 1599 (let* ((ftbl (define-safe ftbl name formals raw-body)) 1600 (new-axiom (|LOGIC.PEQUAL| (|LOGIC.FUNCTION| name formals) body)) 1601 (atbl (if (lookup name atbl) 1602 atbl 1603 new-atbl)) 1604 (axioms (if (memberp new-axiom axioms) 1605 axioms 1606 (cons new-axiom axioms)))) 1607 (|CORE.STATE| axioms thms atbl checker ftbl))))))) 1608 1609 (|CORE.ADMIT-WITNESS| 1610 (cmd state) 1611 ;; Returns a new state or calls error 1612 ;; CMD should be (SKOLEM NAME BOUND-VAR FREE-VAR BODY) 1613 (if (or (not (tuplep 5 cmd)) 1614 (not (equal (car cmd) 'skolem))) 1615 (error (list 'admit-witness 'invalid-cmd cmd)) 1616 (let* ((axioms (|CORE.AXIOMS| state)) 1617 (thms (|CORE.THMS| state)) 1618 (atbl (|CORE.ATBL| state)) 1619 (checker (|CORE.CHECKER| state)) 1620 (ftbl (|CORE.FTBL| state)) 1621 (name (second cmd)) 1622 (bound-var (third cmd)) 1623 (free-vars (fourth cmd)) 1624 (raw-body (fifth cmd)) 1625 (body (|LOGIC.TRANSLATE| raw-body)) 1626 (all-vars (cons bound-var free-vars))) 1627 (cond 1628 ((not (|LOGIC.FUNCTION-NAMEP| name)) 1629 (error (list 'admit-witness 'bad-name name))) 1630 ((not (true-listp free-vars)) 1631 (error (list 'admit-witness 'bad-formals name))) 1632 ((not (|LOGIC.VARIABLEP| bound-var)) 1633 (error (list 'admit-witness 'bad-bound-var name))) 1634 ((not (|LOGIC.VARIABLE-LISTP| free-vars)) 1635 (error (list 'admit-witness 'bad-free-vars name))) 1636 ((not (uniquep (cons bound-var free-vars))) 1637 (error (list 'admit-witness 'duplicate-free-vars name))) 1638 ((not (|LOGIC.TERMP| body)) 1639 (error (list 'admit-witness 'bad-body name))) 1640 ((not (subsetp (|LOGIC.TERM-VARS| body) all-vars)) 1641 (error (list 'admit-witness 'free-vars-in-body name))) 1642 ((not (|LOGIC.TERM-ATBLP| body atbl)) 1643 (error (list 'admit-witness 'bad-arity-in-body name))) 1644 (t 1645 (let* ((ftbl (define-safe ftbl name free-vars 1646 (list 'error 1647 (list 'quote 1648 (list name bound-var 1649 free-vars raw-body))))) 1650 (atbl (if (lookup name atbl) 1651 atbl 1652 (cons (cons name (len free-vars)) atbl))) 1653 (new-axiom 1654 (|LOGIC.POR| (|LOGIC.PEQUAL| body ''nil) 1655 (|LOGIC.PNOT| 1656 (|LOGIC.PEQUAL| 1657 (|LOGIC.LAMBDA| 1658 all-vars body 1659 (cons (|LOGIC.FUNCTION| name free-vars) 1660 free-vars)) 1661 ''nil)))) 1662 (axioms (if (memberp new-axiom axioms) 1663 axioms 1664 (cons new-axiom axioms)))) 1665 (|CORE.STATE| axioms thms atbl checker ftbl))))))) 1666 1667 (|CORE.EVAL-FUNCTION| (x) 1668 (let* ((fn (|LOGIC.FUNCTION-NAME| x)) 1669 (vals (|LOGIC.UNQUOTE-LIST| (|LOGIC.FUNCTION-ARGS| x))) 1670 (n (len vals)) 1671 (x1 (first vals)) 1672 (x2 (second vals)) 1673 (x3 (third vals)) 1674 (x4 (fourth vals)) 1675 (x5 (fifth vals))) 1676 (list 'quote 1677 (cond ((equal n 0) (funcall fn)) 1678 ((equal n 1) (funcall fn x1)) 1679 ((equal n 2) (funcall fn x1 x2)) 1680 ((equal n 3) (funcall fn x1 x2 x3)) 1681 ((equal n 4) (funcall fn x1 x2 x3 x4)) 1682 ((equal n 5) (funcall fn x1 x2 x3 x4 x5)) 1683 (t (error (list 'core-eval-function 'too-many-parameters))))))) 1684 1685 (|CORE.ADMIT-EVAL| 1686 (cmd state) 1687 ;; Performs evaluation in the runtime 1688 ;; CMD should be (EVAL (fn 'arg1 'arg2 ... 'argN)) 1689 (let* ((axioms (|CORE.AXIOMS| state)) 1690 (thms (|CORE.THMS| state)) 1691 (atbl (|CORE.ATBL| state)) 1692 (checker (|CORE.CHECKER| state)) 1693 (ftbl (|CORE.FTBL| state)) 1694 (lhs (second cmd))) 1695 (cond 1696 ((not (|LOGIC.TERMP| lhs)) 1697 (error (list 'admit-eval 'bad-term-on-lhs lhs))) 1698 ((not (|LOGIC.FUNCTIONP| lhs)) 1699 (error (list 'admit-eval 'not-function-on-lhs lhs))) 1700 ((not (|LOGIC.CONSTANT-LISTP| (|LOGIC.FUNCTION-ARGS| lhs))) 1701 (error (list 'admit-eval 'not-const-list-on-lhs lhs))) 1702 ((not (|LOGIC.TERM-ATBLP| lhs atbl)) 1703 (error (list 'admit-eval 'bad-arity-on-lhs lhs))) 1704 ((lookup (|LOGIC.FUNCTION-NAME| lhs) (|CORE.INITIAL-ATBL|)) 1705 (error (list 'admit-eval 'not-user-defined-function lhs))) 1706 (t 1707 (let* ((rhs (|CORE.EVAL-FUNCTION| lhs)) 1708 (new-thm (|LOGIC.PEQUAL| lhs rhs)) 1709 (thms (cons new-thm thms))) 1710 (|CORE.STATE| axioms thms atbl checker ftbl)))))) 1711 1712 (|CORE.ADMIT-PRINT| 1713 (cmd state) 1714 ;; Prints a theorem and returns original state, or calls error 1715 ;; CMD should be (PRINT FORMULA) 1716 (if (or (not (tuplep 2 cmd)) 1717 (not (equal (car cmd) 'print))) 1718 (error (list 'admit-print 'invalid-cmd cmd)) 1719 (let* ((axioms (|CORE.AXIOMS| state)) 1720 (thms (|CORE.THMS| state)) 1721 (formula (second cmd))) 1722 (cond 1723 ((not (or (memberp formula axioms) 1724 (memberp formula thms))) 1725 (error (list 'admit-print 'no-such-theorem))) 1726 (t (let* ((unused (print (list 'theorem formula)))) 1727 state)))))) 1728 1729 (|CORE.ACCEPT-COMMAND| 1730 (cmd state) 1731 ;; Returns a new state or calls error 1732 (cond ((equal (car cmd) 'verify) (|CORE.ADMIT-THEOREM| cmd state)) 1733 ((equal (car cmd) 'define) (|CORE.ADMIT-DEFUN| cmd state)) 1734 ((equal (car cmd) 'skolem) (|CORE.ADMIT-WITNESS| cmd state)) 1735 ((equal (car cmd) 'switch) (|CORE.ADMIT-SWITCH| cmd state)) 1736 ((equal (car cmd) 'print) (|CORE.ADMIT-PRINT| cmd state)) 1737 ((equal (car cmd) 'eval) (|CORE.ADMIT-EVAL| cmd state)) 1738 (t 1739 (error (list 'accept-cmd 'invalid-command cmd))))) 1740 1741 (|CORE.ACCEPT-COMMANDS| 1742 (cmds event-number state) 1743 ;; Returns a new state or calls error. 1744 (if (consp cmds) 1745 (let* ((unused (print (list event-number 1746 (first (car cmds)) 1747 (second (car cmds))))) 1748 (state (|CORE.ACCEPT-COMMAND| (car cmds) state))) 1749 (|CORE.ACCEPT-COMMANDS| (cdr cmds) 1750 (+ 1 event-number) 1751 state)) 1752 state)) 1753 1754 ))) 1755 1756(define 'milawa-main '(cmds) 1757 '(let* ((ftbl (milawa-init)) 1758 (axioms (|CORE.INITIAL-AXIOMS|)) 1759 (thms 'nil) 1760 (atbl (|CORE.INITIAL-ATBL|)) 1761 (checker '|LOGIC.PROOFP|) 1762 (state (|CORE.STATE| axioms thms atbl checker ftbl))) 1763 (and (|CORE.ACCEPT-COMMANDS| cmds '1 state) 1764 'success))) 1765