← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/nnf.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/ivy/ivy-v2/ivy-sources/nnf.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; Negation normal form (NNF): definition, syntactic correctness
 
4
;; theorem, soundness theorem, and some preservation-of-property theorems.
 
5
 
 
6
(include-book "stage")
 
7
 
 
8
(defmacro car-and (f)    (list 'equal (list 'car f) ''and))
 
9
(defmacro car-or (f)     (list 'equal (list 'car f) ''or))
 
10
(defmacro car-imp (f)    (list 'equal (list 'car f) ''imp))
 
11
(defmacro car-iff (f)    (list 'equal (list 'car f) ''iff))
 
12
(defmacro car-all (f)    (list 'equal (list 'car f) ''all))
 
13
(defmacro car-exists (f) (list 'equal (list 'car f) ''exists))
 
14
 
 
15
;;==================================================================
 
16
;; Function nnf converts a formula to negation normal form.
 
17
;; That is, in terms of and/or/not, where all nots are up against
 
18
;; simple formulas.  ('true and 'false are not simplified away.)
 
19
         
 
20
(defun nnf (f)
 
21
  (declare (xargs :guard (wff f)))
 
22
  (cond
 
23
   ((wfbinary f)
 
24
    (cond ((car-and f) (list 'and (nnf (a1 f)) (nnf (a2 f))))
 
25
          ((car-or  f) (list 'or  (nnf (a1 f)) (nnf (a2 f))))
 
26
          ((car-imp f) (list 'or  (nnf (list 'not (a1 f))) (nnf (a2 f))))
 
27
          ((car-iff f) (list 'and 
 
28
                             (list 'or (nnf (list 'not (a1 f))) (nnf (a2 f)))
 
29
                             (list 'or (nnf (a1 f)) (nnf (list 'not (a2 f))))))
 
30
          (t f)))  ; should not happen if (wff f)
 
31
 
 
32
   ((wfquant f)
 
33
    (cond ((car-all    f) (list 'all    (a1 f) (nnf (a2 f))))
 
34
          ((car-exists f) (list 'exists (a1 f) (nnf (a2 f))))
 
35
          (t f)))  ; should not happen if (wff f)
 
36
 
 
37
   ((wfnot f)
 
38
    (cond ((wfbinary (a1 f))
 
39
           (cond ((car-and (a1 f)) (list 'or
 
40
                                         (nnf (list 'not (a1 (a1 f))))
 
41
                                         (nnf (list 'not (a2 (a1 f))))))
 
42
                 ((car-or (a1 f))  (list 'and 
 
43
                                         (nnf (list 'not (a1 (a1 f))))
 
44
                                         (nnf (list 'not (a2 (a1 f))))))
 
45
                 ((car-imp (a1 f)) (list 'and 
 
46
                                         (nnf (a1 (a1 f)))
 
47
                                         (nnf (list 'not (a2 (a1 f))))))
 
48
                 ((car-iff (a1 f)) (list 'and 
 
49
                                         (list 'or 
 
50
                                               (nnf (a1 (a1 f)))
 
51
                                               (nnf (a2 (a1 f))))
 
52
                                         (list 'or 
 
53
                                               (nnf (list 'not (a1 (a1 f))))
 
54
                                               (nnf (list 'not (a2 (a1 f)))))))
 
55
                 (t f)))  ; should not happen if (wff f)
 
56
          ((wfquant (a1 f))
 
57
           (cond ((car-all (a1 f))
 
58
                  (list 'exists (a1 (a1 f)) (nnf (list 'not (a2 (a1 f))))))
 
59
                 ((car-exists (a1 f))
 
60
                  (list 'all (a1 (a1 f)) (nnf (list 'not (a2 (a1 f))))))
 
61
                 (t f)))  ; should not happen if (wff f)
 
62
 
 
63
          ((wfnot (a1 f)) (nnf (a1 (a1 f))))
 
64
          (t f)))
 
65
   (t f)))
 
66
 
 
67
;; Prove that nnf preserves well-formedness.
 
68
 
 
69
(defthm nnf-wff
 
70
  (implies (wff f)
 
71
           (wff (nnf f))))
 
72
 
 
73
;; Prove that nnf applied to a wff gives negation normal form.
 
74
 
 
75
(defthm nnf-nnfp
 
76
  (implies (wff x)
 
77
           (nnfp (nnf x))))
 
78
 
 
79
(defthm subst-nnf-commute
 
80
  (equal (subst-free (nnf f) x tm)
 
81
         (nnf (subst-free f x tm))))
 
82
 
 
83
;;---------------------------------
 
84
;; Prove that nnf is sound.  The proof seems to be easier with xeval.
 
85
 
 
86
(defthm nnf-xsound-for-not
 
87
  (equal (xeval (nnf (list 'not f)) dom i)
 
88
         (xeval (list 'not (nnf f)) dom i))
 
89
  :hints (("Goal"
 
90
           :induct (xeval-i f dom i))))
 
91
 
 
92
(defthm nnf-xsound
 
93
  (equal (xeval (nnf f) dom i)
 
94
         (xeval f dom i))
 
95
  :hints (("Goal"
 
96
           :induct (xeval-i f dom i))))
 
97
 
 
98
(defthm nnf-fsound
 
99
  (equal (feval (nnf f) i)
 
100
         (feval f i))
 
101
  :hints (("Goal"
 
102
           :in-theory (enable xeval-feval))))
 
103
 
 
104
;;---------------------------------
 
105
;; Prove that nnf preserves the set of free variables.
 
106
 
 
107
(defthm nnf-preserves-free-vars
 
108
  (equal (free-vars (nnf f)) (free-vars f)))
 
109