convert-normalized-term-to-pairs

other

(in-package "ACL2")

other

(tau-status :system nil)

normalizedpfunction

(defun normalizedp
  (term)
  (cond ((variablep term) t)
    ((fquotep term) t)
    ((eq (ffn-symb term) 'if) (and (or (symbolp (fargn term 1))
          (and (not (fquotep (fargn term 1)))
            (not (eq (ffn-symb (fargn term 1)) 'if))))
        (normalizedp (fargn term 2))
        (normalizedp (fargn term 3))))
    (t t)))

cntp-m-pairfunction

(defun cntp-m-pair
  (pair)
  (fcons-term* 'if (conjoin (car pair)) (cdr pair) *t*))

cntp-mfunction

(defun cntp-m
  (pairs)
  (cond ((endp pairs) *t*)
    (t (fcons-term* 'if
        (cntp-m-pair (car pairs))
        (cntp-m (cdr pairs))
        *nil*))))

other

(defevaluator cntp-evl
  cntp-evl-lst
  ((if x
     y
     z) (not x)
    (equal x y)))

local

(local (defun rev
    (x)
    (if (endp x)
      nil
      (append (rev (cdr x)) (list (car x))))))

local

(local (defthm revappend-is-append-rev
    (equal (revappend x y) (append (rev x) y))))

local

(local (defthm cntp-evl-conjoin-append
    (iff (cntp-evl (conjoin (append x y)) alist)
      (and (cntp-evl (conjoin x) alist)
        (cntp-evl (conjoin y) alist)))))

local

(local (defthm cntp-evl-conjoin-rev
    (iff (cntp-evl (conjoin (rev x)) alist)
      (cntp-evl (conjoin x) alist))))

convert-normalized-term-to-pairsfunction

(defun convert-normalized-term-to-pairs
  (rhyps term ans)
  (cond ((variablep term) (cons (cons (revappend rhyps nil) term) ans))
    ((fquotep term) (if (equal term *nil*)
        (cond ((consp rhyps) (cons (cons (revappend (cdr rhyps) nil)
                (dumb-negate-lit (car rhyps)))
              ans))
          (t (cons (cons nil *nil*) ans)))
        ans))
    ((eq (ffn-symb term) 'if) (cond ((equal (fargn term 3) *nil*) (convert-normalized-term-to-pairs rhyps
            (fargn term 2)
            (cons (cons (revappend rhyps nil) (fargn term 1)) ans)))
        ((equal (fargn term 2) *nil*) (convert-normalized-term-to-pairs rhyps
            (fargn term 3)
            (cons (cons (revappend rhyps nil)
                (dumb-negate-lit (fargn term 1)))
              ans)))
        (t (convert-normalized-term-to-pairs (cons (fargn term 1) rhyps)
            (fargn term 2)
            (convert-normalized-term-to-pairs (cons (dumb-negate-lit (fargn term 1)) rhyps)
              (fargn term 3)
              ans)))))
    (t (cons (cons (revappend rhyps nil) term) ans))))

local

(local (defthm cntp-evl-conjoin-cons
    (iff (cntp-evl (conjoin (cons x y)) alist)
      (and (cntp-evl x alist) (cntp-evl (conjoin y) alist)))))

local

(local (defthm cntp-evl-of-dumb-negate-lit
    (implies (pseudo-termp x)
      (iff (cntp-evl (dumb-negate-lit x) alist)
        (not (cntp-evl x alist))))))

local

(local (defthm pseudo-termp-of-dumb-negate-lit
    (implies (pseudo-termp x)
      (pseudo-termp (dumb-negate-lit x)))))

local

(local (in-theory (disable conjoin
      true-listp
      dumb-negate-lit
      rev
      default-car
      default-cdr
      (:t cntp-m)
      length
      len)))

convert-normalized-term-to-pairs-correcttheorem

(defthm convert-normalized-term-to-pairs-correct
  (implies (and (pseudo-termp term)
      (normalizedp term)
      (pseudo-term-listp rhyps))
    (iff (cntp-evl (cntp-m (convert-normalized-term-to-pairs rhyps term ans))
        alist)
      (and (cntp-evl (fcons-term* 'if (conjoin rhyps) term *t*) alist)
        (cntp-evl (cntp-m ans) alist))))
  :hints (("Goal" :induct (convert-normalized-term-to-pairs rhyps term ans)
     :expand ((pseudo-termp term) (normalizedp term)))))