blob: 5b03b9cec4b85c196b4ed5f08080d2cb7a3020c7 (
plain)
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
(in-package "ACL2")
;; Negation normal form (NNF): definition, syntactic correctness
;; theorem, soundness theorem, and some preservation-of-property theorems.
(include-book "stage")
(defmacro car-and (f) (list 'equal (list 'car f) ''and))
(defmacro car-or (f) (list 'equal (list 'car f) ''or))
(defmacro car-imp (f) (list 'equal (list 'car f) ''imp))
(defmacro car-iff (f) (list 'equal (list 'car f) ''iff))
(defmacro car-all (f) (list 'equal (list 'car f) ''all))
(defmacro car-exists (f) (list 'equal (list 'car f) ''exists))
;;==================================================================
;; Function nnf converts a formula to negation normal form.
;; That is, in terms of and/or/not, where all nots are up against
;; simple formulas. ('true and 'false are not simplified away.)
(defun nnf (f)
(declare (xargs :guard (wff f)))
(cond
((wfbinary f)
(cond ((car-and f) (list 'and (nnf (a1 f)) (nnf (a2 f))))
((car-or f) (list 'or (nnf (a1 f)) (nnf (a2 f))))
((car-imp f) (list 'or (nnf (list 'not (a1 f))) (nnf (a2 f))))
((car-iff f) (list 'and
(list 'or (nnf (list 'not (a1 f))) (nnf (a2 f)))
(list 'or (nnf (a1 f)) (nnf (list 'not (a2 f))))))
(t f))) ; should not happen if (wff f)
((wfquant f)
(cond ((car-all f) (list 'all (a1 f) (nnf (a2 f))))
((car-exists f) (list 'exists (a1 f) (nnf (a2 f))))
(t f))) ; should not happen if (wff f)
((wfnot f)
(cond ((wfbinary (a1 f))
(cond ((car-and (a1 f)) (list 'or
(nnf (list 'not (a1 (a1 f))))
(nnf (list 'not (a2 (a1 f))))))
((car-or (a1 f)) (list 'and
(nnf (list 'not (a1 (a1 f))))
(nnf (list 'not (a2 (a1 f))))))
((car-imp (a1 f)) (list 'and
(nnf (a1 (a1 f)))
(nnf (list 'not (a2 (a1 f))))))
((car-iff (a1 f)) (list 'and
(list 'or
(nnf (a1 (a1 f)))
(nnf (a2 (a1 f))))
(list 'or
(nnf (list 'not (a1 (a1 f))))
(nnf (list 'not (a2 (a1 f)))))))
(t f))) ; should not happen if (wff f)
((wfquant (a1 f))
(cond ((car-all (a1 f))
(list 'exists (a1 (a1 f)) (nnf (list 'not (a2 (a1 f))))))
((car-exists (a1 f))
(list 'all (a1 (a1 f)) (nnf (list 'not (a2 (a1 f))))))
(t f))) ; should not happen if (wff f)
((wfnot (a1 f)) (nnf (a1 (a1 f))))
(t f)))
(t f)))
;; Prove that nnf preserves well-formedness.
(defthm nnf-wff
(implies (wff f)
(wff (nnf f))))
;; Prove that nnf applied to a wff gives negation normal form.
(defthm nnf-nnfp
(implies (wff x)
(nnfp (nnf x))))
(defthm subst-nnf-commute
(equal (subst-free (nnf f) x tm)
(nnf (subst-free f x tm))))
;;---------------------------------
;; Prove that nnf is sound. The proof seems to be easier with xeval.
(defthm nnf-xsound-for-not
(equal (xeval (nnf (list 'not f)) dom i)
(xeval (list 'not (nnf f)) dom i))
:hints (("Goal"
:induct (xeval-i f dom i))))
(defthm nnf-xsound
(equal (xeval (nnf f) dom i)
(xeval f dom i))
:hints (("Goal"
:induct (xeval-i f dom i))))
(defthm nnf-fsound
(equal (feval (nnf f) i)
(feval f i))
:hints (("Goal"
:in-theory (enable xeval-feval))))
;;---------------------------------
;; Prove that nnf preserves the set of free variables.
(defthm nnf-preserves-free-vars
(equal (free-vars (nnf f)) (free-vars f)))
|
