1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
|
(in-package "PROOF-CHECKER-ARRAY")
(include-book "literal")
(include-book "unique")
;; ===================================================================
;; ============================= CLAUSE ==============================
(defun clausep (clause)
(declare (xargs :guard t))
(and (literal-listp clause)
(unique-literalsp clause)
(no-conflicting-literalsp clause)))
(defthm clausep-true-listp
(implies (clausep clause)
(true-listp clause)))
(defthm clausep-member
(implies (and (clausep clause)
(member e clause))
(literalp e)))
(defthm clausep-cdr
(implies (and (clausep clause)
(consp clause))
(clausep (cdr clause))))
;; ===================================================================
;; ============================= FORMULA =============================
(defun formulap (formula)
(declare (xargs :guard t))
(if (atom formula)
(null formula)
(and (clausep (car formula))
(formulap (cdr formula)))))
(defthm formulap-true-listp
(implies (formulap formula)
(true-listp formula)))
(defthm formulap-member
(implies (and (formulap formula)
(member e formula))
(clausep e)))
(defthm formulap-cdr
(implies (and (formulap formula)
(consp formula))
(formulap (cdr formula))))
(defthm formulap-implies-clausep-car
(implies (and (formulap formula)
(consp formula))
(clausep (car formula))))
;; ===================================================================
;; ========================= FLATTEN-FORMULA =========================
(defun flatten-formula (formula)
(declare (xargs :guard (formulap formula)))
(if (atom formula)
nil
(append (car formula)
(flatten-formula (cdr formula)))))
(defthm literal-listp-flatten-formula
(implies (formulap formula)
(literal-listp (flatten-formula formula))))
|