• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Verified

Add-hypo-cp

Verified clause-processor for adding user hypotheses

Definitions and Theorems

Theorem: ev-add-hypo-constraint-0

(defthm ev-add-hypo-constraint-0
 (implies
   (and (consp acl2::x)
        (syntaxp (not (equal acl2::a ''nil)))
        (not (equal (car acl2::x) 'quote)))
   (equal
        (ev-add-hypo acl2::x acl2::a)
        (ev-add-hypo (cons (car acl2::x)
                           (kwote-lst (ev-lst-add-hypo (cdr acl2::x)
                                                       acl2::a)))
                     nil))))

Theorem: ev-add-hypo-constraint-1

(defthm ev-add-hypo-constraint-1
  (implies (symbolp acl2::x)
           (equal (ev-add-hypo acl2::x acl2::a)
                  (and acl2::x
                       (cdr (assoc-equal acl2::x acl2::a))))))

Theorem: ev-add-hypo-constraint-2

(defthm ev-add-hypo-constraint-2
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'quote))
           (equal (ev-add-hypo acl2::x acl2::a)
                  (cadr acl2::x))))

Theorem: ev-add-hypo-constraint-3

(defthm ev-add-hypo-constraint-3
  (implies
       (and (consp acl2::x)
            (consp (car acl2::x)))
       (equal (ev-add-hypo acl2::x acl2::a)
              (ev-add-hypo (caddr (car acl2::x))
                           (pairlis$ (cadr (car acl2::x))
                                     (ev-lst-add-hypo (cdr acl2::x)
                                                      acl2::a))))))

Theorem: ev-add-hypo-constraint-4

(defthm ev-add-hypo-constraint-4
  (implies (not (consp acl2::x-lst))
           (equal (ev-lst-add-hypo acl2::x-lst acl2::a)
                  nil)))

Theorem: ev-add-hypo-constraint-5

(defthm ev-add-hypo-constraint-5
  (implies (consp acl2::x-lst)
           (equal (ev-lst-add-hypo acl2::x-lst acl2::a)
                  (cons (ev-add-hypo (car acl2::x-lst) acl2::a)
                        (ev-lst-add-hypo (cdr acl2::x-lst)
                                         acl2::a)))))

Theorem: ev-add-hypo-constraint-6

(defthm ev-add-hypo-constraint-6
  (implies (and (not (consp acl2::x))
                (not (symbolp acl2::x)))
           (equal (ev-add-hypo acl2::x acl2::a)
                  nil)))

Theorem: ev-add-hypo-constraint-7

(defthm ev-add-hypo-constraint-7
  (implies (and (consp acl2::x)
                (not (consp (car acl2::x)))
                (not (symbolp (car acl2::x))))
           (equal (ev-add-hypo acl2::x acl2::a)
                  nil)))

Theorem: ev-add-hypo-constraint-8

(defthm ev-add-hypo-constraint-8
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'not))
           (equal (ev-add-hypo acl2::x acl2::a)
                  (not (ev-add-hypo (cadr acl2::x) acl2::a)))))

Theorem: ev-add-hypo-constraint-9

(defthm ev-add-hypo-constraint-9
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'if))
           (equal (ev-add-hypo acl2::x acl2::a)
                  (if (ev-add-hypo (cadr acl2::x) acl2::a)
                      (ev-add-hypo (caddr acl2::x) acl2::a)
                    (ev-add-hypo (cadddr acl2::x)
                                 acl2::a)))))

Theorem: ev-add-hypo-constraint-10

(defthm ev-add-hypo-constraint-10
  (implies
       (and (consp acl2::x)
            (equal (car acl2::x) 'hint-please))
       (equal (ev-add-hypo acl2::x acl2::a)
              (hint-please (ev-add-hypo (cadr acl2::x) acl2::a)))))

Theorem: ev-add-hypo-disjoin-cons

(defthm ev-add-hypo-disjoin-cons
  (iff (ev-add-hypo (disjoin (cons acl2::x acl2::y))
                    acl2::a)
       (or (ev-add-hypo acl2::x acl2::a)
           (ev-add-hypo (disjoin acl2::y)
                        acl2::a))))

Theorem: ev-add-hypo-disjoin-when-consp

(defthm ev-add-hypo-disjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-add-hypo (disjoin acl2::x) acl2::a)
                (or (ev-add-hypo (car acl2::x) acl2::a)
                    (ev-add-hypo (disjoin (cdr acl2::x))
                                 acl2::a)))))

Theorem: ev-add-hypo-disjoin-atom

(defthm ev-add-hypo-disjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-add-hypo (disjoin acl2::x) acl2::a)
                  nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-add-hypo-disjoin-append

(defthm ev-add-hypo-disjoin-append
  (iff (ev-add-hypo (disjoin (append acl2::x acl2::y))
                    acl2::a)
       (or (ev-add-hypo (disjoin acl2::x) acl2::a)
           (ev-add-hypo (disjoin acl2::y)
                        acl2::a))))

Theorem: ev-add-hypo-conjoin-cons

(defthm ev-add-hypo-conjoin-cons
  (iff (ev-add-hypo (conjoin (cons acl2::x acl2::y))
                    acl2::a)
       (and (ev-add-hypo acl2::x acl2::a)
            (ev-add-hypo (conjoin acl2::y)
                         acl2::a))))

Theorem: ev-add-hypo-conjoin-when-consp

(defthm ev-add-hypo-conjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-add-hypo (conjoin acl2::x) acl2::a)
                (and (ev-add-hypo (car acl2::x) acl2::a)
                     (ev-add-hypo (conjoin (cdr acl2::x))
                                  acl2::a)))))

Theorem: ev-add-hypo-conjoin-atom

(defthm ev-add-hypo-conjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-add-hypo (conjoin acl2::x) acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-add-hypo-conjoin-append

(defthm ev-add-hypo-conjoin-append
  (iff (ev-add-hypo (conjoin (append acl2::x acl2::y))
                    acl2::a)
       (and (ev-add-hypo (conjoin acl2::x) acl2::a)
            (ev-add-hypo (conjoin acl2::y)
                         acl2::a))))

Theorem: ev-add-hypo-conjoin-clauses-cons

(defthm ev-add-hypo-conjoin-clauses-cons
  (iff (ev-add-hypo (conjoin-clauses (cons acl2::x acl2::y))
                    acl2::a)
       (and (ev-add-hypo (disjoin acl2::x) acl2::a)
            (ev-add-hypo (conjoin-clauses acl2::y)
                         acl2::a))))

Theorem: ev-add-hypo-conjoin-clauses-when-consp

(defthm ev-add-hypo-conjoin-clauses-when-consp
  (implies (consp acl2::x)
           (iff (ev-add-hypo (conjoin-clauses acl2::x)
                             acl2::a)
                (and (ev-add-hypo (disjoin (car acl2::x))
                                  acl2::a)
                     (ev-add-hypo (conjoin-clauses (cdr acl2::x))
                                  acl2::a)))))

Theorem: ev-add-hypo-conjoin-clauses-atom

(defthm ev-add-hypo-conjoin-clauses-atom
  (implies (not (consp acl2::x))
           (equal (ev-add-hypo (conjoin-clauses acl2::x)
                               acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-add-hypo-conjoin-clauses-append

(defthm ev-add-hypo-conjoin-clauses-append
  (iff (ev-add-hypo (conjoin-clauses (append acl2::x acl2::y))
                    acl2::a)
       (and (ev-add-hypo (conjoin-clauses acl2::x)
                         acl2::a)
            (ev-add-hypo (conjoin-clauses acl2::y)
                         acl2::a))))

Function: add-hypo-subgoals

(defun add-hypo-subgoals (hinted-hypos g)
  (declare (xargs :guard (and (hint-pair-listp hinted-hypos)
                              (pseudo-termp g))))
  (let ((acl2::__function__ 'add-hypo-subgoals))
    (declare (ignorable acl2::__function__))
    (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
              (cons (cons 'hint-please
                          (cons (cons 'quote
                                      (cons merged-in-theory 'nil))
                                'nil))
                    (cons h (cons g 'nil))))
         (first-not-h-clause (cons 'not (cons h 'nil)))
         ((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)))))

Theorem: pseudo-term-list-listp-of-add-hypo-subgoals.list-of-h-thm

(defthm pseudo-term-list-listp-of-add-hypo-subgoals.list-of-h-thm
  (b* (((mv ?list-of-h-thm ?list-of-not-hs)
        (add-hypo-subgoals hinted-hypos g)))
    (pseudo-term-list-listp list-of-h-thm))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-add-hypo-subgoals.list-of-not-hs

(defthm pseudo-term-listp-of-add-hypo-subgoals.list-of-not-hs
  (b* (((mv ?list-of-h-thm ?list-of-not-hs)
        (add-hypo-subgoals hinted-hypos g)))
    (pseudo-term-listp list-of-not-hs))
  :rule-classes :rewrite)

Theorem: add-hypo-subgoals-correctness

(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)))

Function: add-hypo-cp

(defun add-hypo-cp (cl smtlink-hint)
 (declare (xargs :guard (pseudo-term-listp cl)))
 (let ((acl2::__function__ 'add-hypo-cp))
  (declare (ignorable acl2::__function__))
  (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
     (cons
      ':clause-processor
      (cons (cons next-cp
                  (cons 'clause
                        (cons (cons 'quote (cons smtlink-hint 'nil))
                              'nil)))
            'nil)))
    (g (disjoin cl))
    ((mv aux-hypo-clauses list-of-not-hs)
     (add-hypo-subgoals hinted-hypos g))
    (cl0 (cons (cons 'hint-please
                     (cons (cons 'quote (cons the-hint 'nil))
                           'nil))
               (append list-of-not-hs (cons g 'nil)))))
   (cons cl0 aux-hypo-clauses))))

Theorem: pseudo-term-list-listp-of-add-hypo-cp

(defthm pseudo-term-list-listp-of-add-hypo-cp
  (b* ((subgoal-lst (add-hypo-cp cl smtlink-hint)))
    (pseudo-term-list-listp subgoal-lst))
  :rule-classes :rewrite)

Theorem: correctness-of-add-hypos

(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))
 :rule-classes :clause-processor)