defarbrec-template

other

(in-package "ACL2")

other

(defstub a (*) => *)

other

(defstub b (*) => *)

other

(defstub c (* *) => *)

other

(defstub d (*) => *)

ffunction

(defun f
  (x)
  (declare (xargs :mode :program))
  (if (a x)
    (b x)
    (c x (f (d x)))))

d*function

(defund d*
  (k x)
  (declare (xargs :measure (acl2-count k)
      :hints (("Goal" :in-theory nil))))
  (if (zp k)
    x
    (d* (1- k) (d x))))

d*-lemmatheorem

(defthm d*-lemma
  (implies (and (a (d* k x)) (not (natp k))) (a (d* 0 x)))
  :hints (("Goal" :in-theory '(d* natp zp)))
  :rule-classes nil)

ttfunction

(defun-sk tt (x) (exists k (a (d* k x))))

in-theory

(in-theory (disable tt tt-suff))

nufunction

(defund nu
  (x k)
  (declare (xargs :measure (nfix (- (tt-witness x) (nfix k)))
      :hints (("Goal" :in-theory '(o-p o-finp o< nfix natp)))))
  (let ((k (nfix k)))
    (if (or (a (d* k x)) (>= k (nfix (tt-witness x))))
      k
      (nu x (1+ k)))))

mufunction

(defund mu (x) (nu x 0))

nu-natptheorem

(defthmd nu-natp
  (natp (nu x k))
  :hints (("Goal" :in-theory '((:type-prescription nu) (:compound-recognizer natp-compound-recognizer)))))

mu-natptheorem

(defthmd mu-natp
  (natp (mu x))
  :hints (("Goal" :in-theory '(mu nu-natp))))

nu-endtheorem

(defthmd nu-end
  (implies (and (tt x) (natp k) (<= k (nfix (tt-witness x))))
    (a (d* (nu x k) x)))
  :hints (("Goal" :in-theory '(nu tt natp nfix) :induct (nu x k)) '(:use (:instance d*-lemma (k (tt-witness x))))))

mu-endtheorem

(defthmd mu-end
  (implies (tt x) (a (d* (mu x) x)))
  :hints (("Goal" :in-theory '(mu nu-end natp nfix))))

nu-mintheorem

(defthmd nu-min
  (implies (and (natp l) (natp k) (>= l k) (a (d* l x)))
    (>= l (nu x k)))
  :hints (("Goal" :in-theory '(nu natp nfix) :induct (nu x k))))

mu-mintheorem

(defthmd mu-min
  (implies (and (natp l) (a (d* l x))) (>= l (mu x)))
  :hints (("Goal" :in-theory '(mu nu-min natp))))

f^function

(defun f^
  (x)
  (declare (xargs :measure (mu x)
      :hints (("Goal" :in-theory '(o-p o-finp natp o< zp d*)
         :use (mu-natp (:instance mu-natp (x (d x)))
           mu-end
           (:instance mu-min (l (1- (mu x))) (x (d x))))))))
  (if (tt x)
    (if (a x)
      (b x)
      (c x (f^ (d x))))
    :nonterminating))