add-hypo-cp

(in-package "SMT")

(include-book "std/util/bstar" :dir :system)

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "hint-please")

(include-book "hint-interface")

(include-book "computed-hints")

(defsection add-hypo-cp
  :parents (verified)
  :short "Verified clause-processor for adding user hypotheses"
  (defevaluator ev-add-hypo
    ev-lst-add-hypo
    ((not x) (if x
        y
        z)
      (hint-please hint)))
  (def-join-thms ev-add-hypo)
  (define add-hypo-subgoals
    ((hinted-hypos hint-pair-listp) (g pseudo-termp))
    :returns (mv (list-of-h-thm pseudo-term-list-listp)
      (list-of-not-hs pseudo-term-listp))
    :measure (len hinted-hypos)
    (b* ((hinted-hypos (hint-pair-list-fix hinted-hypos)) (g (pseudo-term-fix g))
        ((unless (consp hinted-hypos)) (mv nil nil))
        ((cons first-hinted-h rest-hinted-hs) hinted-hypos)
        (h (hint-pair->thm first-hinted-h))
        (h-hint (hint-pair->hints first-hinted-h))
        (merged-in-theory (treat-in-theory-hint '(hint-please) h-hint))
        (first-h-thm `((hint-please ',SMT::MERGED-IN-THEORY) ,SMT::H ,SMT::G))
        (first-not-h-clause `(not ,SMT::H))
        ((mv rest-h-thms rest-not-h-clauses) (add-hypo-subgoals rest-hinted-hs g)))
      (mv (cons first-h-thm rest-h-thms)
        (cons first-not-h-clause rest-not-h-clauses)))
    ///
    (defthm add-hypo-subgoals-correctness
      (implies (and (pseudo-termp g)
          (alistp b)
          (hint-pair-listp hinted-hypos)
          (ev-add-hypo (disjoin (mv-nth 1
                (add-hypo-subgoals hinted-hypos g)))
            b)
          (ev-add-hypo (conjoin-clauses (mv-nth 0
                (add-hypo-subgoals hinted-hypos g)))
            b))
        (ev-add-hypo g b))
      :hints (("Goal" :induct (add-hypo-subgoals hinted-hypos g)))))
  (local (defthm crock0
      (implies (and (pseudo-term-listp x)
          (pseudo-term-listp cl))
        (pseudo-term-listp (append x (list (disjoin cl)))))))
  (local (defthm crock1
      (implies (pseudo-term-listp x)
        (pseudo-term-listp (append x '('nil))))))
  (define add-hypo-cp
    ((cl pseudo-term-listp) (smtlink-hint t))
    :returns (subgoal-lst pseudo-term-list-listp)
    (b* (((unless (pseudo-term-listp cl)) nil) ((unless (smtlink-hint-p smtlink-hint)) (list cl))
        ((smtlink-hint h) smtlink-hint)
        (hinted-hypos h.hypotheses)
        (next-cp (cdr (assoc-equal 'add-hypo *smt-architecture*)))
        ((if (null next-cp)) (list cl))
        (the-hint `(:clause-processor (,SMT::NEXT-CP clause ',SMT::SMTLINK-HINT)))
        (g (disjoin cl))
        ((mv aux-hypo-clauses list-of-not-hs) (add-hypo-subgoals hinted-hypos g))
        (cl0 `((hint-please ',SMT::THE-HINT) ,@SMT::LIST-OF-NOT-HS
            ,SMT::G)))
      `(,SMT::CL0 ,@SMT::AUX-HYPO-CLAUSES)))
  (local (in-theory (enable add-hypo-cp)))
  (defthm correctness-of-add-hypos
    (implies (and (pseudo-term-listp cl)
        (alistp b)
        (ev-add-hypo (conjoin-clauses (add-hypo-cp cl smtlink-hint))
          b))
      (ev-add-hypo (disjoin cl) b))
    :hints (("Goal" :in-theory (disable add-hypo-subgoals-correctness)
       :use ((:instance add-hypo-subgoals-correctness
          (g (disjoin cl))
          (hinted-hypos (smtlink-hint->hypotheses smtlink-hint))
          (b b)))))
    :rule-classes :clause-processor))