Filtering...

just-expand

books/clause-processors/just-expand

Included Books

unify-subst meta-extract-user bstar ev-theoremp use-by-hint butlast
other
(in-package "ACL2")
include-book
(include-book "unify-subst")
include-book
(include-book "meta-extract-user")
include-book
(include-book "std/util/bstar" :dir :system)
include-book
(include-book "ev-theoremp")
include-book
(include-book "use-by-hint")
include-book
(include-book "std/lists/butlast" :dir :system)
in-theory
(in-theory (disable butlast))
expand-mefunction
(defund expand-me (x) (declare (xargs :guard t)) x)
in-theory
(in-theory (disable (expand-me) (:t expand-me)))
expand-me-withfunction
(defund expand-me-with
  (rule x)
  (declare (xargs :guard t)
    (ignore rule))
  x)
in-theory
(in-theory (disable (expand-me-with) (:t expand-me-with)))
other
(defevaluator expev
  expev-lst
  ((if a
     b
     c) (equal a b)
    (not a)
    (use-by-hint a)
    (cons a b)
    (binary-+ a b)
    (typespec-check ts x)
    (iff a b)
    (implies a b)
    (expand-me x)
    (expand-me-with rule x))
  :namedp t)
other
(def-ev-theoremp expev)
other
(def-meta-extract expev expev-lst)
other
(def-unify expev expev-alist)
local
(local (in-theory (disable w)))
local
(local (defthm expev-alist-of-pairlis$
    (equal (expev-alist (pairlis$ x y) a)
      (pairlis$ x (expev-lst y a)))))
other
(defsection expand-this-term
  (defund expand-this-term
    (x explicit-rule w)
    "returns (mv successp x1)"
    (declare (xargs :guard (and (pseudo-termp x)
          (symbolp explicit-rule)
          (plist-worldp w))))
    (b* (((when (or (variablep x) (fquotep x))) x) (fn (ffn-symb x))
        ((when (flambdap fn)) (b* ((formals (lambda-formals fn)) (body (lambda-body fn))
              (args (fargs x)))
            (substitute-into-term body (pairlis$ formals args))))
        (rule (or explicit-rule fn))
        (formula (meta-extract-formula-w rule w))
        ((unless (pseudo-termp formula)) x)
        ((mv ok lhs rhs) (case-match formula
            (('equal lhs rhs) (mv t lhs rhs))
            (& (mv nil nil nil))))
        ((unless ok) x)
        ((mv match-ok subst) (simple-one-way-unify lhs x nil))
        ((unless match-ok) x))
      (substitute-into-term rhs subst)))
  (local (in-theory (enable expand-this-term)))
  (defthm expand-this-term-correct
    (implies (and (expev-meta-extract-global-facts)
        (equal w (w state))
        (pseudo-termp x))
      (equal (expev (expand-this-term x explicit-rule w) a)
        (expev x a)))
    :hints (("goal" :use ((:instance expev-meta-extract-formula
          (name (or explicit-rule (car x)))
          (st state)
          (a (expev-alist (mv-nth 1
                (simple-one-way-unify (cadr (meta-extract-formula (or explicit-rule (car x)) state))
                  x
                  nil))
              a))))
       :in-theory (disable expev-meta-extract-formula))))
  (defthm expand-this-term-pseudo-termp
    (implies (pseudo-termp x)
      (pseudo-termp (expand-this-term x explicit-rule w)))))
other
(defsection expand-if-marked
  (defund expand-if-marked
    (fn args w)
    (declare (xargs :guard (and (symbolp fn)
          (not (eq fn 'quote))
          (pseudo-term-listp args)
          (plist-worldp w))))
    (b* (((when (eq fn 'expand-me)) (b* ((term (first args))) (expand-this-term term nil w))) ((when (and (eq fn 'expand-me-with) (quotep (first args)))) (b* ((rule (unquote (first args))) (term (second args))
              ((unless (or (symbol-listp rule) (symbolp rule))) term)
              (rule (if (consp rule)
                  (second rule)
                  rule)))
            (expand-this-term term rule w))))
      (cons fn args)))
  (local (in-theory (enable expand-if-marked expand-me expand-me-with)))
  (defthm expand-if-marked-correct
    (implies (and (expev-meta-extract-global-facts)
        (equal w (w state))
        (symbolp fn)
        (pseudo-term-listp args))
      (equal (expev (expand-if-marked fn args w) a)
        (expev (cons fn args) a))))
  (defthm expand-if-marked-pseudo-termp
    (implies (and (symbolp fn)
        (not (eq fn 'quote))
        (pseudo-term-listp args))
      (pseudo-termp (expand-if-marked fn args w))))
  (defun expand-if-marked-meta
    (x mfc state)
    (declare (xargs :stobjs state :guard (pseudo-termp x))
      (ignorable mfc))
    (b* (((when (variablep x)) x) (fn (ffn-symb x))
        ((when (eq fn 'quote)) x)
        ((when (consp fn)) x)
        (args (fargs x)))
      (expand-if-marked fn args (w state))))
  (defthmd expand-marked-meta
    (implies (and (pseudo-termp x) (expev-meta-extract-global-facts))
      (equal (expev x a)
        (expev (expand-if-marked-meta x mfc state) a)))
    :rule-classes ((:meta :trigger-fns (expand-me expand-me-with)))))
other
(defsection term/alist-ind
  (mutual-recursion (defun expev-term/alist-ind
      (x al)
      (b* (((when (variablep x)) al) (fn (ffn-symb x))
          ((when (eq fn 'quote)) al)
          (?args (expev-termlist/alist-ind (fargs x) al))
          ((when (consp fn)) (expev-term/alist-ind (lambda-body fn)
              (pairlis$ (lambda-formals fn) (expev-lst (fargs x) al)))))
        al))
    (defun expev-termlist/alist-ind
      (x al)
      (if (atom x)
        nil
        (cons (expev-term/alist-ind (car x) al)
          (expev-termlist/alist-ind (cdr x) al)))))
  (make-flag expev-term/alist-flag
    expev-term/alist-ind
    :flag-mapping ((expev-term/alist-ind term) (expev-termlist/alist-ind list))))
other
(defsection expand-marked-term
  (mutual-recursion (defun expand-marked-term
      (x w)
      (declare (xargs :guard (and (pseudo-termp x) (plist-worldp w))
          :verify-guards nil))
      (b* (((when (variablep x)) x) (fn (ffn-symb x))
          ((when (eq fn 'quote)) x)
          (args (expand-marked-list (fargs x) w))
          ((when (flambdap fn)) `((lambda ,(LAMBDA-FORMALS FN)
               ,(EXPAND-MARKED-TERM (LAMBDA-BODY FN) W)) . ,ARGS)))
        (expand-if-marked fn args w)))
    (defun expand-marked-list
      (x w)
      (declare (xargs :guard (and (pseudo-term-listp x) (plist-worldp w))))
      (if (atom x)
        nil
        (cons (expand-marked-term (car x) w)
          (expand-marked-list (cdr x) w)))))
  (in-theory (disable expand-marked-term expand-marked-list))
  (defthm len-of-expand-marked-list
    (equal (len (expand-marked-list x w)) (len x))
    :hints (("Goal" :in-theory (enable expand-marked-list))))
  (defthm-expev-term/alist-flag (defthm expand-marked-term-pseudo-termp
      (implies (pseudo-termp x)
        (pseudo-termp (expand-marked-term x w)))
      :hints ('(:expand ((expand-marked-term x w))))
      :flag term)
    (defthm expand-marked-list-pseudo-term-listp
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (expand-marked-list x w)))
      :hints ('(:expand ((expand-marked-list x w) (expand-marked-list nil w))))
      :flag list))
  (local (defthm pseudo-termp-car-when-pseudo-term-listp
      (implies (pseudo-term-listp x) (pseudo-termp (car x)))))
  (verify-guards expand-marked-term)
  (defthm-expev-term/alist-flag (defthm expand-marked-term-correct
      (implies (and (expev-meta-extract-global-facts)
          (equal w (w state))
          (pseudo-termp x))
        (equal (expev (expand-marked-term x w) al) (expev x al)))
      :hints ('(:expand ((expand-marked-term x w))
         :in-theory (enable expev-of-fncall-args)))
      :flag term)
    (defthm expand-marked-list-correct
      (implies (and (expev-meta-extract-global-facts)
          (equal w (w state))
          (pseudo-term-listp x))
        (equal (expev-lst (expand-marked-list x w) al)
          (expev-lst x al)))
      :hints ('(:expand ((expand-marked-list x w) (expand-marked-list nil w))))
      :flag list)))
other
(defsection remove-expand-mes
  (mutual-recursion (defun remove-expand-mes
      (x)
      (declare (xargs :guard (and (pseudo-termp x)) :verify-guards nil))
      (b* (((when (variablep x)) x) (fn (ffn-symb x))
          ((when (eq fn 'quote)) x)
          (args (remove-expand-mes-list (fargs x)))
          ((when (flambdap fn)) `((lambda ,(LAMBDA-FORMALS FN)
               ,(REMOVE-EXPAND-MES (LAMBDA-BODY FN))) . ,ARGS))
          ((when (and (eq fn 'expand-me) (equal (len args) 1))) (car args))
          ((when (and (eq fn 'expand-me-with) (equal (len args) 2))) (cadr args)))
        (cons fn args)))
    (defun remove-expand-mes-list
      (x)
      (declare (xargs :guard (and (pseudo-term-listp x))))
      (if (atom x)
        nil
        (cons (remove-expand-mes (car x))
          (remove-expand-mes-list (cdr x))))))
  (in-theory (disable remove-expand-mes remove-expand-mes-list))
  (defthm len-of-remove-expand-mes-list
    (equal (len (remove-expand-mes-list x)) (len x))
    :hints (("Goal" :in-theory (enable remove-expand-mes-list))))
  (defthm-expev-term/alist-flag (defthm remove-expand-mes-pseudo-termp
      (implies (pseudo-termp x)
        (pseudo-termp (remove-expand-mes x)))
      :hints ('(:expand ((remove-expand-mes x))))
      :flag term)
    (defthm remove-expand-mes-list-pseudo-term-listp
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (remove-expand-mes-list x)))
      :hints ('(:expand ((remove-expand-mes-list x) (remove-expand-mes-list nil))))
      :flag list))
  (local (defthm pseudo-termp-car-when-pseudo-term-listp
      (implies (pseudo-term-listp x) (pseudo-termp (car x)))))
  (verify-guards remove-expand-mes)
  (defthm-expev-term/alist-flag (defthm remove-expand-mes-correct
      (implies (pseudo-termp x)
        (equal (expev (remove-expand-mes x) al) (expev x al)))
      :hints ('(:expand ((remove-expand-mes x))
         :in-theory (enable expev-of-fncall-args expand-me expand-me-with)))
      :flag term)
    (defthm remove-expand-mes-list-correct
      (implies (pseudo-term-listp x)
        (equal (expev-lst (remove-expand-mes-list x) al)
          (expev-lst x al)))
      :hints ('(:expand ((remove-expand-mes-list x) (remove-expand-mes-list nil))))
      :flag list)))
other
(defsection just-expand-cp-parse-hints
  (defun just-expand-cp-finish-hint
    (rule vars term w)
    (declare (xargs :mode :program))
    (b* (((when (atom term)) (er hard?
           'just-expand-cp
           "atom in term position in hints: ~x0~%"
           term)) ((mv erp trans-term) (translate-cmp term
            t
            nil
            nil
            'just-expand-cp
            w
            (default-state-vars nil)))
        ((when erp) (er hard?
            'just-expand-cp
            "translate failed: ~@0~%"
            trans-term))
        (trans-term-vars (simple-term-vars trans-term))
        (nonfree-vars (set-difference-eq trans-term-vars vars))
        ((when (not (or (symbolp rule) (symbol-listp rule)))) (er hard? 'just-expand-cp "invalid rule: ~x0~%" rule))
        (rule (if (consp rule)
            (cadr rule)
            rule)))
      (cons trans-term
        `((rule . ,RULE) (subst . ,(PAIRLIS$ NONFREE-VARS NONFREE-VARS))))))
  (defun just-expand-cp-parse-hint
    (hint w)
    (declare (xargs :mode :program))
    (case-match hint
      ((':with rule (':free vars term)) (just-expand-cp-finish-hint rule vars term w))
      ((':free vars (':with rule term)) (just-expand-cp-finish-hint rule vars term w))
      ((':free vars term) (just-expand-cp-finish-hint nil vars term w))
      ((':with rule term) (just-expand-cp-finish-hint rule nil term w))
      (& (just-expand-cp-finish-hint nil nil hint w))))
  (defun just-expand-cp-parse-hints
    (hints w)
    (declare (xargs :mode :program))
    (if (atom hints)
      nil
      (cons (just-expand-cp-parse-hint (car hints) w)
        (just-expand-cp-parse-hints (cdr hints) w)))))
other
(defsection just-exp-hints-okp
  (defund just-exp-hint-alist-okp
    (alist)
    (declare (xargs :guard t))
    (and (alistp alist)
      (symbolp (cdr (assoc 'rule alist)))
      (alistp (cdr (assoc 'subst alist)))))
  (defund just-exp-hints-okp
    (hints)
    (declare (xargs :guard t))
    (or (atom hints)
      (and (consp (car hints))
        (pseudo-termp (caar hints))
        (just-exp-hint-alist-okp (cdar hints))
        (just-exp-hints-okp (cdr hints))))))
other
(defsection mark-expansion
  (local (in-theory (enable just-exp-hint-alist-okp)))
  (defund mark-expansion
    (term pattern alist)
    (declare (xargs :guard (and (pseudo-termp term)
          (pseudo-termp pattern)
          (just-exp-hint-alist-okp alist))))
    (b* ((subst (cdr (assoc 'subst alist))) ((mv pat-ok &) (simple-one-way-unify pattern term subst))
        ((unless pat-ok) term)
        (rule (cdr (assoc 'rule alist))))
      (if rule
        `(expand-me-with ',RULE ,TERM)
        `(expand-me ,TERM))))
  (local (in-theory (enable mark-expansion expand-me expand-me-with)))
  (defthm mark-expansion-correct
    (implies (and (pseudo-termp term)
        (pseudo-termp pattern)
        (just-exp-hint-alist-okp alist))
      (equal (expev (mark-expansion term pattern alist) a)
        (expev term a)))
    :hints (("goal" :do-not-induct t)))
  (defthm pseudo-termp-mark-expansion
    (implies (pseudo-termp term)
      (pseudo-termp (mark-expansion term pattern alist)))))
other
(defsection mark-expansions
  (local (in-theory (enable just-exp-hints-okp)))
  (defund mark-expansions
    (term hints)
    (declare (xargs :guard (and (pseudo-termp term) (just-exp-hints-okp hints))))
    (if (atom hints)
      term
      (mark-expansions (mark-expansion term (caar hints) (cdar hints))
        (cdr hints))))
  (local (in-theory (enable mark-expansions)))
  (defthm mark-expansions-correct
    (implies (and (just-exp-hints-okp hints) (pseudo-termp term))
      (equal (expev (mark-expansions term hints) a)
        (expev term a))))
  (defthm pseudo-termp-mark-expansions
    (implies (pseudo-termp term)
      (pseudo-termp (mark-expansions term hints)))))
other
(defsection mark-expands-with-hints
  (mutual-recursion (defun mark-expands-with-hints
      (x hints lambdasp)
      (declare (xargs :guard (and (pseudo-termp x) (just-exp-hints-okp hints))
          :verify-guards nil))
      (b* (((when (variablep x)) x) (fn (ffn-symb x))
          ((when (eq fn 'quote)) x)
          (args (mark-expands-with-hints-list (fargs x) hints lambdasp))
          ((when (and lambdasp (flambdap fn))) `((lambda ,(LAMBDA-FORMALS FN)
               ,(MARK-EXPANDS-WITH-HINTS (LAMBDA-BODY FN) HINTS LAMBDASP)) . ,ARGS)))
        (mark-expansions (cons fn args) hints)))
    (defun mark-expands-with-hints-list
      (x hints lambdasp)
      (declare (xargs :guard (and (pseudo-term-listp x) (just-exp-hints-okp hints))))
      (if (atom x)
        nil
        (cons (mark-expands-with-hints (car x) hints lambdasp)
          (mark-expands-with-hints-list (cdr x) hints lambdasp)))))
  (in-theory (disable mark-expands-with-hints
      mark-expands-with-hints-list))
  (defthm len-of-mark-expands-with-hints-list
    (equal (len (mark-expands-with-hints-list x hints lambdasp))
      (len x))
    :hints (("Goal" :in-theory (enable mark-expands-with-hints-list))))
  (defthm-expev-term/alist-flag (defthm mark-expands-with-hints-pseudo-termp
      (implies (pseudo-termp x)
        (pseudo-termp (mark-expands-with-hints x hints lambdasp)))
      :hints ('(:expand ((mark-expands-with-hints x hints lambdasp))))
      :flag term)
    (defthm mark-expands-with-hints-list-pseudo-term-listp
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (mark-expands-with-hints-list x hints lambdasp)))
      :hints ('(:expand ((mark-expands-with-hints-list x hints lambdasp) (mark-expands-with-hints-list nil hints lambdasp))))
      :flag list))
  (verify-guards mark-expands-with-hints
    :hints (("goal" :expand ((:free (a b) (pseudo-termp (cons a b)))))))
  (defthm-expev-term/alist-flag (defthm mark-expands-with-hints-correct
      (implies (and (just-exp-hints-okp hints) (pseudo-termp x))
        (equal (expev (mark-expands-with-hints x hints lambdasp) al)
          (expev x al)))
      :hints ('(:expand ((mark-expands-with-hints x hints lambdasp))
         :in-theory (enable expev-of-fncall-args)))
      :flag term)
    (defthm mark-expands-with-hints-list-correct
      (implies (and (just-exp-hints-okp hints) (pseudo-term-listp x))
        (equal (expev-lst (mark-expands-with-hints-list x hints lambdasp)
            al)
          (expev-lst x al)))
      :hints ('(:expand ((mark-expands-with-hints-list x hints lambdasp) (mark-expands-with-hints-list nil hints lambdasp))))
      :flag list)))
other
(defsection apply-expansion
  (local (in-theory (enable just-exp-hint-alist-okp)))
  (defund apply-expansion
    (term pattern alist w)
    (declare (xargs :guard (and (pseudo-termp term)
          (pseudo-termp pattern)
          (just-exp-hint-alist-okp alist)
          (plist-worldp w))))
    (b* ((subst (cdr (assoc 'subst alist))) ((mv pat-ok &) (simple-one-way-unify pattern term subst))
        ((unless pat-ok) term)
        (rule (cdr (assoc 'rule alist))))
      (expand-this-term term rule w)))
  (local (in-theory (enable apply-expansion)))
  (defthm apply-expansion-correct
    (implies (and (expev-meta-extract-global-facts)
        (equal w (w state))
        (pseudo-termp term)
        (pseudo-termp pattern)
        (just-exp-hint-alist-okp alist))
      (equal (expev (apply-expansion term pattern alist w) a)
        (expev term a)))
    :hints (("goal" :do-not-induct t)))
  (defthm pseudo-termp-apply-expansion
    (implies (pseudo-termp term)
      (pseudo-termp (apply-expansion term pattern alist w)))))
other
(defsection apply-expansions
  (local (in-theory (enable just-exp-hints-okp)))
  (defund apply-expansions
    (term hints w)
    (declare (xargs :guard (and (pseudo-termp term)
          (just-exp-hints-okp hints)
          (plist-worldp w))))
    (if (atom hints)
      term
      (apply-expansions (apply-expansion term (caar hints) (cdar hints) w)
        (cdr hints)
        w)))
  (local (in-theory (enable apply-expansions)))
  (defthm apply-expansions-correct
    (implies (and (expev-meta-extract-global-facts)
        (equal w (w state))
        (just-exp-hints-okp hints)
        (pseudo-termp term))
      (equal (expev (apply-expansions term hints w) a)
        (expev term a))))
  (defthm pseudo-termp-apply-expansions
    (implies (pseudo-termp term)
      (pseudo-termp (apply-expansions term hints w)))))
other
(defsection expand-with-hints
  (mutual-recursion (defun expand-with-hints
      (x hints lambdasp w)
      (declare (xargs :guard (and (pseudo-termp x)
            (plist-worldp w)
            (just-exp-hints-okp hints))
          :verify-guards nil))
      (b* (((when (variablep x)) x) (fn (ffn-symb x))
          ((when (eq fn 'quote)) x)
          (args (expand-with-hints-list (fargs x) hints lambdasp w))
          ((when (and lambdasp (flambdap fn))) `((lambda ,(LAMBDA-FORMALS FN)
               ,(EXPAND-WITH-HINTS (LAMBDA-BODY FN) HINTS LAMBDASP W)) . ,ARGS)))
        (apply-expansions (cons fn args) hints w)))
    (defun expand-with-hints-list
      (x hints lambdasp w)
      (declare (xargs :guard (and (pseudo-term-listp x)
            (just-exp-hints-okp hints)
            (plist-worldp w))))
      (if (atom x)
        nil
        (cons (expand-with-hints (car x) hints lambdasp w)
          (expand-with-hints-list (cdr x) hints lambdasp w)))))
  (in-theory (disable expand-with-hints expand-with-hints-list))
  (defthm len-of-expand-with-hints-list
    (equal (len (expand-with-hints-list x hints lambdasp w))
      (len x))
    :hints (("Goal" :in-theory (enable expand-with-hints-list))))
  (defthm-expev-term/alist-flag (defthm expand-with-hints-pseudo-termp
      (implies (pseudo-termp x)
        (pseudo-termp (expand-with-hints x hints lambdasp w)))
      :hints ('(:expand ((expand-with-hints x hints lambdasp w))))
      :flag term)
    (defthm expand-with-hints-list-pseudo-term-listp
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (expand-with-hints-list x hints lambdasp w)))
      :hints ('(:expand ((expand-with-hints-list x hints lambdasp w) (expand-with-hints-list nil hints lambdasp w))))
      :flag list))
  (verify-guards expand-with-hints
    :hints (("goal" :expand ((:free (a b) (pseudo-termp (cons a b)))))))
  (defthm-expev-term/alist-flag (defthm expand-with-hints-correct
      (implies (and (expev-meta-extract-global-facts)
          (equal w (w state))
          (just-exp-hints-okp hints)
          (pseudo-termp x))
        (equal (expev (expand-with-hints x hints lambdasp w) al)
          (expev x al)))
      :hints ('(:expand ((expand-with-hints x hints lambdasp w))
         :in-theory (enable expev-of-fncall-args)))
      :flag term)
    (defthm expand-with-hints-list-correct
      (implies (and (expev-meta-extract-global-facts)
          (equal w (w state))
          (just-exp-hints-okp hints)
          (pseudo-term-listp x))
        (equal (expev-lst (expand-with-hints-list x hints lambdasp w) al)
          (expev-lst x al)))
      :hints ('(:expand ((expand-with-hints-list x hints lambdasp w) (expand-with-hints-list nil hints lambdasp w))))
      :flag list)))
local
(local (defsection butlast/last/append
    (defthm expev-of-disjoin
      (iff (expev (disjoin x) a) (or-list (expev-lst x a)))
      :hints (("Goal" :in-theory (enable or-list len) :induct (len x))))
    (defthm expev-lst-of-append
      (equal (expev-lst (append x y) a)
        (append (expev-lst x a) (expev-lst y a))))
    (defthm len-of-expev-lst
      (equal (len (expev-lst x a)) (len x)))
    (defthm expev-lst-of-butlast
      (equal (expev-lst (butlast clause n) a)
        (butlast (expev-lst clause a) n))
      :hints (("goal" :induct (butlast clause n)) '(:cases ((consp clause)))))
    (defthm expev-lst-of-last
      (equal (expev-lst (last x) a) (last (expev-lst x a)))
      :hints (("goal" :induct (last x)
         :expand ((last x) (:free (b) (last (cons (expev (car x) a) b))))
         :in-theory (disable (:d last))) '(:cases ((consp x)))))
    (defthm append-butlast-last
      (equal (append (butlast x 1) (last x)) x))
    (defthm pseudo-term-listp-of-last
      (implies (pseudo-term-listp x) (pseudo-term-listp (last x))))
    (defthm pseudo-term-listp-of-butlast
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (butlast x n))))
    (defthm not-or-list-of-butlast-if-not-or-list
      (implies (not (or-list x)) (not (or-list (butlast x n)))))
    (defthm pseudo-term-listp-append
      (implies (and (pseudo-term-listp x) (pseudo-term-listp y))
        (pseudo-term-listp (append x y))))))
other
(defsection just-expand-cp
  (local (defthm true-listp-butlast (true-listp (butlast lst n))))
  (defund just-expand-cp
    (clause hints state)
    (declare (xargs :guard (pseudo-term-listp clause) :stobjs state))
    (b* (((unless (and (true-listp hints) (just-exp-hints-okp (caddr hints)))) (mv "bad hints" nil)) ((list last-only lambdasp hints) hints)
        (clause (if last-only
            (append (butlast clause 1)
              (expand-with-hints-list (last clause)
                hints
                lambdasp
                (w state)))
            (expand-with-hints-list clause hints lambdasp (w state)))))
      (mv nil (list clause))))
  (local (in-theory (enable just-expand-cp)))
  (local (in-theory (disable butlast-redefinition or-list last)))
  (defthm just-expand-cp-correct
    (implies (and (expev-meta-extract-global-facts)
        (pseudo-term-listp clause)
        (alistp a)
        (expev-theoremp (conjoin-clauses (clauses-result (just-expand-cp clause hints state)))))
      (expev (disjoin clause) a))
    :hints (("goal" :do-not-induct t
       :use ((:instance expev-falsify
          (x (disjoin (car (mv-nth 1 (just-expand-cp clause hints state)))))))))
    :rule-classes :clause-processor))
other
(defsection expand-marked-cp
  (local (defthm true-listp-butlast (true-listp (butlast lst n))))
  (defund expand-marked-cp
    (clause hints state)
    (declare (xargs :guard (pseudo-term-listp clause) :stobjs state))
    (b* (((unless (true-listp hints)) (mv "bad hints" nil)) ((list last-only) hints)
        (clause (if last-only
            (append (remove-expand-mes-list (butlast clause 1))
              (expand-marked-list (last clause) (w state)))
            (expand-marked-list clause (w state)))))
      (mv nil (list clause))))
  (local (in-theory (enable expand-marked-cp)))
  (local (in-theory (disable butlast-redefinition or-list last)))
  (defthm expand-marked-cp-correct
    (implies (and (expev-meta-extract-global-facts)
        (pseudo-term-listp clause)
        (alistp a)
        (expev-theoremp (conjoin-clauses (clauses-result (expand-marked-cp clause hints state)))))
      (expev (disjoin clause) a))
    :hints (("goal" :do-not-induct t
       :use ((:instance expev-falsify
          (x (disjoin (car (mv-nth 1 (expand-marked-cp clause hints state)))))))))
    :rule-classes :clause-processor))
other
(defsection remove-expand-marks-cp
  (local (defthm true-listp-butlast (true-listp (butlast lst n))))
  (defund remove-expand-marks-cp
    (clause hints)
    (declare (xargs :guard (pseudo-term-listp clause)))
    (b* (((unless (true-listp hints)) (mv "bad hints" nil)) ((list butlast-only) hints)
        (clause (if butlast-only
            (append (remove-expand-mes-list (butlast clause 1))
              (last clause))
            (remove-expand-mes-list clause))))
      (mv nil (list clause))))
  (local (in-theory (enable remove-expand-marks-cp)))
  (local (in-theory (disable butlast-redefinition or-list last)))
  (defthm remove-expand-marks-cp-correct
    (implies (and (expev-meta-extract-global-facts)
        (pseudo-term-listp clause)
        (alistp a)
        (expev-theoremp (conjoin-clauses (clauses-result (remove-expand-marks-cp clause hints)))))
      (expev (disjoin clause) a))
    :hints (("goal" :do-not-induct t
       :use ((:instance expev-falsify
          (x (disjoin (car (mv-nth 1 (remove-expand-marks-cp clause hints)))))))))
    :rule-classes :clause-processor))
other
(defsection mark-expands-cp
  (defund mark-expands-cp
    (clause hints)
    (declare (xargs :guard (pseudo-term-listp clause)))
    (b* (((unless (and (true-listp hints) (just-exp-hints-okp (caddr hints)))) (mv "bad hints" nil)) ((list last-only lambdasp hints) hints)
        (new-clause (if last-only
            (append (butlast clause 1)
              (mark-expands-with-hints-list (last clause) hints lambdasp))
            (mark-expands-with-hints-list clause hints lambdasp))))
      (mv nil (list new-clause))))
  (local (in-theory (enable mark-expands-cp)))
  (local (in-theory (disable butlast-redefinition or-list last)))
  (defthm mark-expands-cp-correct
    (implies (and (pseudo-term-listp clause)
        (alistp a)
        (expev-theoremp (conjoin-clauses (clauses-result (mark-expands-cp clause hints)))))
      (expev (disjoin clause) a))
    :hints (("goal" :do-not-induct t
       :use ((:instance expev-falsify
          (x (disjoin (car (mv-nth 1 (mark-expands-cp clause hints)))))))))
    :rule-classes :clause-processor))
just-expandmacro
(defmacro just-expand
  (expand-lst &key lambdasp mark-only last-only)
  `(let* ((hints (just-expand-cp-parse-hints ',EXPAND-LST (w state))) (cproc ,(IF MARK-ONLY
     ``(MARK-EXPANDS-CP CLAUSE '(,',LAST-ONLY ,',LAMBDASP ,HINTS))
     ``(JUST-EXPAND-CP CLAUSE '(,',LAST-ONLY ,',LAMBDASP ,HINTS) STATE))))
    `(:computed-hint-replacement ((use-by-computed-hint clause))
      :clause-processor ,CPROC)))
expand-markedmacro
(defmacro expand-marked
  (&key last-only)
  ``(:computed-hint-replacement ((use-by-computed-hint clause))
    :clause-processor (expand-marked-cp clause (list ,',LAST-ONLY) state)))
remove-expand-marksmacro
(defmacro remove-expand-marks
  (&key butlast-only)
  ``(:computed-hint-replacement ((use-by-computed-hint clause))
    :clause-processor (remove-expand-marks-cp clause (list ,',BUTLAST-ONLY))))
local
(local (encapsulate nil
    (value-triple 1)
    (local (defthm foo
        (implies (consp x) (equal (len x) (+ 1 (len (cdr x)))))
        :hints (("goal" :do-not '(simplify preprocess eliminate-destructors)
           :in-theory (disable len)) (let ((res (just-expand ((len x)))))
            (progn$ (cw "hint: ~x0~%" res) res))
          '(:do-not nil))
        :rule-classes nil))))
local
(local (encapsulate nil
    (value-triple 2)
    (local (defthm foo
        (implies (consp x) (equal (len x) (+ 1 (len (cdr x)))))
        :hints (("goal" :do-not '(simplify preprocess eliminate-destructors)
           :in-theory (disable len)) (let ((res (just-expand ((len x)) :mark-only t)))
            (progn$ (cw "hint: ~x0~%" res) res))
          '(:do-not nil)
          (and stable-under-simplificationp
            '(:in-theory (e/d (expand-marked-meta) (len)))))
        :rule-classes nil))))
local
(local (encapsulate nil
    (value-triple 3)
    (local (defthm foo
        (implies (consp x)
          (let ((x (list x x)))
            (equal (len x) (+ 1 (len (cdr x))))))
        :hints (("goal" :do-not '(simplify preprocess eliminate-destructors)
           :in-theory (disable len)) (just-expand ((len x)) :lambdasp t)
          '(:do-not nil))))))
local
(local (encapsulate nil
    (value-triple 4)
    (local (defthm foo
        (implies (consp x) (equal (len x) (+ 1 (len (cdr x)))))
        :hints (("goal" :do-not '(simplify preprocess eliminate-destructors)
           :in-theory (disable len)) (let ((res (just-expand ((len x)) :mark-only t)))
            (progn$ (cw "hint: ~x0~%" res) res))
          '(:do-not nil)
          (and stable-under-simplificationp (expand-marked)))
        :rule-classes nil))))
other
(defsection clause-to-term
  (verify-termination dumb-negate-lit)
  (defun dumb-negate-lit-list
    (lst)
    (declare (xargs :guard (pseudo-term-listp lst)))
    (cond ((endp lst) nil)
      (t (cons (dumb-negate-lit (car lst))
          (dumb-negate-lit-list (cdr lst))))))
  (local (defthm dumb-negate-lit-correct
      (implies (pseudo-termp x)
        (iff (expev (dumb-negate-lit x) a) (not (expev x a))))))
  (local (in-theory (disable dumb-negate-lit)))
  (local (defthm dumb-negate-lit-list-conjoin-correct
      (implies (pseudo-term-listp x)
        (iff (expev (conjoin (dumb-negate-lit-list x)) a)
          (not (expev (disjoin x) a))))))
  (local (in-theory (disable dumb-negate-lit-list)))
  (defund clause-to-term
    (clause)
    (declare (xargs :guard (pseudo-term-listp clause)))
    (let* ((hyp-term (conjoin (dumb-negate-lit-list (butlast clause 1)))) (concl-term (car (last clause)))
        (thm-term (if (equal hyp-term ''t)
            concl-term
            `(implies ,HYP-TERM ,CONCL-TERM))))
      (list (list thm-term))))
  (local (in-theory (enable clause-to-term)))
  (local (defthm expev-car-last
      (implies (expev (car (last clause)) a)
        (or-list (expev-lst clause a)))
      :hints (("goal" :induct (len clause)
         :in-theory (disable last)
         :expand ((last clause))))))
  (defthm clause-to-term-correct
    (implies (and (pseudo-term-listp clause)
        (alistp a)
        (expev (conjoin-clauses (clause-to-term clause)) a))
      (expev (disjoin clause) a))
    :rule-classes :clause-processor))
just-induct-and-expandmacro
(defmacro just-induct-and-expand
  (term &key expand-others lambdasp)
  `(if (equal (car id) '(0))
    (b* ((hints (just-expand-cp-parse-hints (cons ',TERM ',EXPAND-OTHERS)
           (w state))) (cproc `(mark-expands-cp clause '(nil ,',LAMBDASP ,HINTS))))
      `(:computed-hint-replacement ((and (equal (car id) '(0))
           '(:clause-processor clause-to-term)) (and (equal (car id) '(0)) '(:induct ,',TERM)))
        :clause-processor ,CPROC))
    (and (equal (car id) '(0 1)) (expand-marked :last-only t))))
just-induct/expand-default-hintfunction
(defun just-induct/expand-default-hint
  (fnname id wait-til-stablep world)
  (declare (xargs :mode :program))
  (and (eql (len (recursivep fnname t world)) 1)
    (eql 0 (access clause-id id :forcing-round))
    (let* ((pool-lst (access clause-id id :pool-lst)) (formals (fgetprop fnname 'formals nil world)))
      (cond ((not pool-lst) `(:induct (,FNNAME . ,FORMALS)
            :in-theory (disable (:d ,FNNAME))))
        ((equal pool-lst '(1)) (let ((expand-hints (just-expand-cp-parse-hints `((:free ,FORMALS (,FNNAME . ,FORMALS)))
                 world)))
            `(:computed-hint-replacement ((and (or (not ',WAIT-TIL-STABLEP) stable-under-simplificationp)
                 (expand-marked)))
              :clause-processor (mark-expands-cp clause '(t t ,EXPAND-HINTS)))))))))
just-expand-mrec-expandersfunction
(defun just-expand-mrec-expanders
  (fns world)
  (declare (xargs :mode :program))
  (if (atom fns)
    nil
    (let ((formals (fgetprop (car fns) 'formals nil world)))
      (cons `(:free ,FORMALS (,(CAR FNS) . ,FORMALS))
        (just-expand-mrec-expanders (cdr fns) world)))))
just-expand-mrec-default-hintfunction
(defun just-expand-mrec-default-hint
  (fnname id wait-til-stablep world)
  (declare (xargs :mode :program))
  (and (eql 0 (access clause-id id :forcing-round))
    (equal '(1) (access clause-id id :pool-lst))
    (let* ((fns (recursivep fnname t world)) (expand-hints (just-expand-cp-parse-hints (just-expand-mrec-expanders fns world)
            world)))
      `(:computed-hint-replacement ((and (or (not ',WAIT-TIL-STABLEP) stable-under-simplificationp)
           (expand-marked)))
        :in-theory (disable . ,FNS)
        :clause-processor (mark-expands-cp clause '(t t ,EXPAND-HINTS))))))
all-fns-in-cliquesfunction
(defun all-fns-in-cliques
  (fnnames world)
  (declare (xargs :mode :program))
  (if (atom fnnames)
    nil
    (append (recursivep (car fnnames) t world)
      (all-fns-in-cliques (cdr fnnames) world))))
just-expand-mrec-multi-hintfunction
(defun just-expand-mrec-multi-hint
  (fnnames id wait-til-stablep world)
  (declare (xargs :mode :program))
  (and (eql 0 (access clause-id id :forcing-round))
    (equal '(1) (access clause-id id :pool-lst))
    (let* ((fns (all-fns-in-cliques fnnames world)) (expand-hints (just-expand-cp-parse-hints (just-expand-mrec-expanders fns world)
            world)))
      `(:computed-hint-replacement ((and (or (not ',WAIT-TIL-STABLEP) stable-under-simplificationp)
           (expand-marked)))
        :in-theory (disable . ,FNS)
        :clause-processor (mark-expands-cp clause '(t t ,EXPAND-HINTS))))))
local
(local (progn (defun ind
      (x y z)
      (declare (xargs :measure (acl2-count x)))
      (if (atom x)
        (list z y)
        (if (eq y nil)
          (cons x z)
          (ind (cdr x) (nthcdr z y) z))))
    (encapsulate nil
      (value-triple 'just-induct-test)
      (local (in-theory (disable (:definition ind))))
      (local (defthm true-listp-ind
          (implies (true-listp z) (true-listp (ind x y z)))
          :hints ((just-induct-and-expand (ind x y z))))))
    (encapsulate nil
      (value-triple 'just-induct-mark-only-test)
      (local (defthm true-listp-ind
          (implies (true-listp z) (true-listp (ind x y z)))
          :hints ((just-induct-and-expand (ind x y z))))))))