transfinite - ACL2 Book

other

(in-package "ACL2")

o-fixfunction

(defun o-fix
  (x)
  (if (o-p x)
    x
    0))

pred-when-pred-for-smallerencapsulate

(encapsulate (((transfinite-induction-predicate *) => *))
  (local (defun transfinite-induction-predicate
      (x)
      (declare (ignore x))
      t))
  (defun-sk pred-for-all-ordinals-smaller-than
    (alpha)
    (forall (x)
      (implies (and (o-p x) (o< x alpha))
        (transfinite-induction-predicate x))))
  (defthm pred-when-pred-for-smaller
    (implies (and (o-p alpha) (pred-for-all-ordinals-smaller-than alpha))
      (transfinite-induction-predicate alpha))))

local

(local (defun transfinite-induction-scheme
    (x)
    (declare (xargs :measure (o-fix x)))
    (if (or (not (o-p x)) (transfinite-induction-predicate x))
      x
      (transfinite-induction-scheme (pred-for-all-ordinals-smaller-than-witness x)))))

pred-for-all-ordinalstheorem

(defthm pred-for-all-ordinals
  (implies (o-p y) (transfinite-induction-predicate y))
  :hints (("Goal" :induct (transfinite-induction-scheme y))))

local

(local (encapsulate nil
    (defun foo (x) (declare (ignore x)) t)
    (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))))
    (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))))
    (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))))))))