/usr/share/acl2-7.2dfsg/books/misc/transfinite.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 | (in-package "ACL2")
;; Transfinite induction (a.k.a. ordinal induction) in ACL2.
;; See http://www.mtnmath.com/whatrh/node52.html for a discussion of ordinal induction.
;; Thanks to Matt Kaufmann and Pete Manolios for enlightening discussions.
;; The proof below was sketched out by Matt; I basically just typed it
;; up. --Eric Smith
;; Should this be added to the ordinals books?
(defun o-fix (x)
(if (o-p x)
x
0))
(encapsulate
(((transfinite-induction-predicate *) => *))
(local (defun transfinite-induction-predicate (x) (declare (ignore x)) t))
;;We don't need a base case [e.g., one asserting
;;(transfinite-induction-predicate 0)], since it would be subsumed by
;;pred-when-pred-for-smaller below.
;; It's gross that this is in the encapsulate, but I need it to express the constraint:
(defun-sk pred-for-all-ordinals-smaller-than (alpha)
(forall (x) (implies (and (o-p x)
(o< x alpha))
(transfinite-induction-predicate x))))
;; The constraint on pred:
(defthm pred-when-pred-for-smaller
(implies (and (o-p alpha)
(pred-for-all-ordinals-smaller-than alpha))
(transfinite-induction-predicate alpha))))
;; This function suggests the induction scheme. The clever idea of recurring
;; on the witness of the defun-sk is due to Matt Kaufmann. It turns out that
;; we can show the witness is smaller than x if we're not in the base case.
(local
(defun transfinite-induction-scheme (x)
(declare (xargs :measure (o-fix x)))
(if (or (not (o-p x))
(transfinite-induction-predicate x) ;putting this in the base case seems clever
)
x
(transfinite-induction-scheme (pred-for-all-ordinals-smaller-than-witness x)))))
;; The main theorem:
(defthm pred-for-all-ordinals
(implies (o-p y)
(transfinite-induction-predicate y))
:hints (("Goal" :induct (transfinite-induction-scheme y))))
;; Now try it out...
(local
(encapsulate
()
(defun foo (x) (declare (ignore x)) t)
;;We'll keep foo shut off to keep the proof from being trivial.
(in-theory (disable foo (:type-prescription foo) (:executable-counterpart foo)))
(defun-sk foo-for-all-ordinals-smaller-than (alpha)
(forall (x) (implies (and (o-p x)
(o< x alpha))
(foo x))))
(defthm foo-when-foo-for-smaller
(implies (and (o-p alpha)
(foo-for-all-ordinals-smaller-than alpha))
(foo alpha))
:hints (("Goal" :in-theory (enable foo)))) ;this is the only place where we open up foo
;; Is sure would be nice if the defun-sk would just phrase
;; foo-for-all-ordinals-smaller-than-necc this way... The way it currently
;; gets phrased is with the hypothesis as an implies, and it fails to fire
;; due to free variables.
(defthm foo-for-all-ordinals-smaller-than-necc-better
(implies (and (o-p x)
(o< x alpha)
(not (foo x)))
(not (foo-for-all-ordinals-smaller-than alpha)))
:hints (("Goal" :in-theory (disable FOO-FOR-ALL-ORDINALS-SMALLER-THAN-NECC)
:use (:instance FOO-FOR-ALL-ORDINALS-SMALLER-THAN-NECC))))
;; Yep, it works!
(defthm foo-for-all-ordinals
(implies (o-p y)
(foo y))
:hints (("Goal" :do-not '(generalize eliminate-destructors)
:use (:instance (:functional-instance pred-for-all-ordinals
(transfinite-induction-predicate foo)
(pred-for-all-ordinals-smaller-than-witness foo-for-all-ordinals-smaller-than-witness)
(pred-for-all-ordinals-smaller-than foo-for-all-ordinals-smaller-than)
)))))))
|