		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-theorem

Process an element of the theorems input.

Signature
(casesplit-process-theorem thm pos old$ ctx state) → (mv erp hyp-new state)
Arguments: thm — An element of theorems.; pos — Position of thm in theorems, 1-based.
Guard (posp pos).; old$ — Guard (symbolp old$).
Returns: hyp-new — A tuple (hyp new) satisfying (typed-tuplep pseudo-termp pseudo-termp hyp-new).

If successful, return the terms hypk and newk described in the documentation (assuming that thm is thmk), in translated form.

Definitions and Theorems

Function: casesplit-process-theorem

(defun casesplit-process-theorem (thm pos old$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (posp pos) (symbolp old$))))
 (let ((__function__ 'casesplit-process-theorem))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (description (msg "The ~n0 element of the third input"
                      (list pos)))
    ((unless (theorem-namep thm wrld))
     (er-soft+
         ctx t nil
         "~@0 must be the name of a theorem, but it is ~x1 instead."
         description thm))
    (formula (thm-formula+ thm wrld))
    (description
     (msg
      "The formula ~x0 of the theorem ~x1 ~
                          specified as ~@2"
      formula
      thm (msg-downcase-first description)))
    ((when (or (variablep formula)
               (fquotep formula)
               (flambda-applicationp formula)
               (not (member-eq (ffn-symb formula)
                               '(implies equal)))))
     (er-soft+ ctx t nil
               "~@0 must be an implication or an equality."
               description))
    (formula (if (eq (ffn-symb formula) 'equal)
                 (cons 'implies
                       (cons ''t (cons formula 'nil)))
               formula))
    (hyp (fargn formula 1))
    (concl (fargn formula 2))
    (description (msg "The conclusion ~x0 of ~@1"
                      concl (msg-downcase-first description)))
    ((when (or (variablep concl)
               (fquotep concl)
               (flambda-applicationp concl)
               (not (eq (ffn-symb concl) 'equal))))
     (er-soft+ ctx t nil
               "~@0 must be an equality." description))
    (left-side (fargn concl 1))
    (description (msg "The left-hand side ~x0 of ~@1"
                      left-side
                      (msg-downcase-first description)))
    (formals (formals+ old$ wrld))
    ((unless (equal left-side (cons old$ formals)))
     (er-soft+
      ctx t nil
      "~@0 must be ~
                   a call of ~x1 on its formal parameters ~x2."
      description old$ formals))
    (new (fargn concl 2)))
   (value (list hyp new)))))