← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/make-event/defspec.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/make-event/defspec.lisp
437
437
       (defthm f-is-identity (equal (f x) x))))
438
438
 
439
439
    (table spec-table 'i 10)))))
 
440
 
 
441
; Added by Matt K.  This example responds to an observation from Bob Boyer,
 
442
; that it would be nice for there to be a general method of specifying notions
 
443
; like "bijection" to avoid errors in an ad hoc attempt to specify that a
 
444
; particular function is a bijection.  I don't claim that this example is a
 
445
; anything like a complete solution to that problem -- in particular, it
 
446
; specifies bijection only for a function mapping pairs from a given domain --
 
447
; but I hope it suggests how one might develop a library of such "higher-order"
 
448
; specifications.
 
449
(local (progn
 
450
 
 
451
; Specify that a function bij2: dom2 x dom2 -> ran2 is a bijection.
 
452
 
 
453
(defspec bijection2
 
454
  (((bij2 * *) => *)
 
455
   ((inv1 *) => *)
 
456
   ((inv2 *) => *)
 
457
   ((dom2 *) => *)
 
458
   ((ran2 *) => *))
 
459
  (local (defun bij2 (x y) (cons x y)))
 
460
  (local (defun inv1 (x) (car x)))
 
461
  (local (defun inv2 (x) (cdr x)))
 
462
  (local (defun dom2 (x) (declare (ignore x)) t))
 
463
  (local (defun ran2 (x) (consp x)))
 
464
  (defthm ran2-bij2
 
465
    (implies (and (dom2 x1)
 
466
                  (dom2 x2))
 
467
             (ran2 (bij2 x1 x2))))
 
468
  (defthm dom2-inv1
 
469
    (implies (ran2 x)
 
470
             (dom2 (inv1 x))))
 
471
  (defthm dom2-inv2
 
472
    (implies (ran2 x)
 
473
             (dom2 (inv2 x))))
 
474
  (defthm bij2-is-injective
 
475
    (implies (and (dom2 x1)
 
476
                  (dom2 x2)
 
477
                  (dom2 y1)
 
478
                  (dom2 y2)
 
479
                  (equal (bij2 x1 x2)
 
480
                         (bij2 y1 y2)))
 
481
             (and (equal x1 y1)
 
482
                  (equal x2 y2)))
 
483
    :rule-classes nil)
 
484
  (defthm bij2-is-surjective
 
485
    (implies (ran2 x)
 
486
             (equal (bij2 (inv1 x) (inv2 x))
 
487
                    x))))
 
488
 
 
489
; Include Harsh's revised book.
 
490
 
 
491
(include-book "system/cantor-pairing-bijective" :dir :system)
 
492
 
 
493
; Separate out three key lemmas.
 
494
 
 
495
(defthm lemma1
 
496
  (implies (and (natp x1)
 
497
                (natp x2)
 
498
                (natp y1)
 
499
                (natp y2)
 
500
                (equal (cantor-pairing x1 x2)
 
501
                       (cantor-pairing y1 y2)))
 
502
           (equal x1 y1))
 
503
  :hints (("Goal"
 
504
           :use ((:instance cantor-pairing-one-one
 
505
                            (a1 x1) (b1 x2) (a2 y1) (b2 y2)))))
 
506
  :rule-classes nil)
 
507
 
 
508
(defthm lemma2
 
509
  (implies (and (natp x1)
 
510
                (natp x2)
 
511
                (natp y1)
 
512
                (natp y2)
 
513
                (equal (cantor-pairing x1 x2)
 
514
                       (cantor-pairing y1 y2)))
 
515
           (equal x2 y2))
 
516
  :hints (("Goal"
 
517
           :use ((:instance cantor-pairing-one-one
 
518
                            (a1 x1) (b1 x2) (a2 y1) (b2 y2)))))
 
519
  :rule-classes nil)
 
520
 
 
521
(defthm lemma3
 
522
  (implies (natp x)
 
523
           (equal (cantor-pairing (car (cantor-pairing-inverse x))
 
524
                                  (cadr (cantor-pairing-inverse x)))
 
525
                  x))
 
526
  :hints (("Goal"
 
527
           :use ((:instance cantor-pairing-onto
 
528
                            (n x)))))
 
529
  :rule-classes nil)
 
530
 
 
531
; Prove that cantor-pairing is a bijection.
 
532
 
 
533
(definstance bijection2 cantor-pairing-is-bijection
 
534
  :functional-substitution
 
535
  ((bij2 cantor-pairing)
 
536
   (inv1 (lambda (x) (car (cantor-pairing-inverse x))))
 
537
   (inv2 (lambda (x) (cadr (cantor-pairing-inverse x))))
 
538
   (dom2 natp)
 
539
   (ran2 natp))
 
540
  :hints (("Goal" :use (lemma1 lemma2 lemma3))))
 
541
 
 
542
; Finally, just for fun, show what was actually proved above.  I would like to
 
543
; use (set-enforce-redundancy t) here.  But unfortunately, one cannot use
 
544
; set-enforce-redundancy in a local context.
 
545
 
 
546
(defthm cantor-pairing-is-bijection
 
547
  (and (implies (and (natp x1) (natp x2))
 
548
                (natp (cantor-pairing x1 x2)))
 
549
       (implies (natp x)
 
550
                (natp (car (cantor-pairing-inverse x))))
 
551
       (implies (natp x)
 
552
                (natp (cadr (cantor-pairing-inverse x))))
 
553
       (implies (and (natp x1)
 
554
                     (natp x2)
 
555
                     (natp y1)
 
556
                     (natp y2)
 
557
                     (equal (cantor-pairing x1 x2)
 
558
                            (cantor-pairing y1 y2)))
 
559
                (and (equal x1 y1) (equal x2 y2)))
 
560
       (implies (natp x)
 
561
                (equal (cantor-pairing (car (cantor-pairing-inverse x))
 
562
                                       (cadr (cantor-pairing-inverse x)))
 
563
                       x)))
 
564
  :rule-classes nil)
 
565
 
 
566
))