Improve TAILREC transformation.

Ensure that the target function is not the domain (if the domain is a function)
and is not called by the domain (if the domain is a lambda expression). This
seems reasonable since the purpose of the transformation is generally to replace
the old function with the new one, but this decision could be revisited if there
is a good example.

books/kestrel/apt/package.lsp

@@ -53,6 +53,7 @@
                         ensure-list-subset$
                         ensure-named-formulas
                         ensure-symbol$
+                        ensure-symbol-different$
                         ensure-symbol-list$
                         ensure-symbol-new-event-name$
                         ensure-term$

books/kestrel/apt/tailrec-reference.lisp

@@ -251,6 +251,7 @@
        If the generated functions are guard-verified
        (which is determined by the @(':verify-guards') input; see below),
        then the @(':domain') function must be guard-verified as well.
+       The @(':domain') function must be distinct from @('old').
        </li>
 
        <li>
@@ -270,6 +271,7 @@
        must only call guard-verified functions,
        except possibly in the @(':logic') subterms of @(tsee mbe)s
        and via @(tsee ec-call).
+       The lambda expression must not include any calls to @('old').
        </li>
 
      </ul>

books/kestrel/apt/tailrec-tests.lisp

@@ -304,7 +304,13 @@
   (must-succeed*
    (defun p (a) (declare (xargs :verify-guards nil)) (natp a))
    (must-fail (tailrec f :domain p))
-   (must-fail (tailrec f :domain (lambda (a) (or (p a) (natp a)))))))
+   (must-fail (tailrec f :domain (lambda (a) (or (p a) (natp a))))))
+
+  ;; same as OLD:
+  (must-fail (tailrec f :domain f))
+
+  ;; calls OLD:
+  (must-fail (tailrec f :domain (lambda (a) (equal (f a) 3)))))
 
  ;; successful applications:
  (must-succeed*

books/kestrel/apt/tailrec.lisp

@@ -360,7 +360,16 @@
                           and the target function ~x0 is guard-verified, ~@1"
                          old-fn-name (msg-downcase-first description))
                     t nil)
-                 (value nil))))
+                 (value nil)))
+       ((er &) (if (symbolp fn/lambda)
+                   (ensure-symbol-different$ fn/lambda
+                                             old-fn-name
+                                             (msg "the target function ~x0"
+                                                  old-fn-name)
+                                             description t nil)
+                 (ensure-term-does-not-call$ (lambda-body fn/lambda)
+                                             old-fn-name
+                                             description t nil))))
     (value fn/lambda)))
 
 (define tailrec-check-new-name