← 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/alls.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/alls.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This book is mostly about universal closures.  The theorem
 
4
;; prover operates on clauses (which contain free variables and
 
5
;; no quantifiers, and free variables are understood as being
 
6
;; universally quantified), and when proving soundness of various
 
7
;; things, we have to frequently add and remove universal quantifiers
 
8
;; to the top of a formula.
 
9
;;
 
10
;; Some of this applies to existential quantifiers as well.
 
11
 
 
12
(include-book "variables")
 
13
(include-book "../../../../../ordinals/e0-ordinal")
 
14
(set-well-founded-relation e0-ord-<)
 
15
 
 
16
;;------------------------------------------
 
17
;; Function alls (vars f) tacks on a list of variables as universally
 
18
;; quantified variables.
 
19
 
 
20
(defun alls (vars f)
 
21
  (declare (xargs :guard (and (var-list vars) (wff f))))
 
22
  (if (atom vars)
 
23
      f
 
24
      (list 'all (car vars) (alls (cdr vars) f))))
 
25
 
 
26
(defthm alls-vars-f-wff
 
27
  (implies (and (var-list vars)
 
28
                (wff f))
 
29
           (wff (alls vars f))))
 
30
 
 
31
(defthm subst-alls-commute
 
32
  (implies (and (not (member-equal x vars))
 
33
                (var-list vars))
 
34
           (equal (subst-free (alls vars f) x e)
 
35
                  (alls vars (subst-free f x e)))))
 
36
 
 
37
(defthm remove-vars-alls
 
38
  (implies (and (domain-term e)
 
39
                (var-list a)
 
40
                (not (member-equal x a))
 
41
                (not (remove-equal x (free-vars (alls a f)))))
 
42
           (not (free-vars (alls a (subst-free f x e)))))
 
43
  :hints (("Goal"
 
44
           :use ((:instance vars-alls-free (f (alls a f)))))))
 
45
 
 
46
(defthm alls-preserves-closedness
 
47
  (implies (not (free-vars f))
 
48
           (not (free-vars (alls v f))))
 
49
  :hints (("Goal"
 
50
           :do-not generalize)))
 
51
 
 
52
(defthm alls-all
 
53
  (implies (and (consp vars)
 
54
                (var-list vars))
 
55
           (wfall (alls vars f))))
 
56
 
 
57
(defthm alls-quant
 
58
  (implies (and (consp vars)
 
59
                (var-list vars))
 
60
           (wfquant (alls vars f))))
 
61
 
 
62
(defun remove-leading-alls (f)
 
63
  (declare (xargs :guard (wff f)))
 
64
  (if (wfall f)
 
65
      (remove-leading-alls (a2 f))
 
66
      f))
 
67
 
 
68
(defthm remove-leading-alls-preserves-wff
 
69
  (implies (wff f)
 
70
           (wff (remove-leading-alls f))))
 
71
 
 
72
(defun leading-alls (f)
 
73
  (declare (xargs :guard (wff f)))
 
74
  (if (wfall f)
 
75
      (cons (a1 f) (leading-alls (a2 f)))
 
76
      nil))
 
77
 
 
78
(defthm lead-alls-var-list
 
79
  (var-list (leading-alls f)))
 
80
 
 
81
(defthm alls-lead-remove-f-is-f
 
82
  (equal (alls (leading-alls f) (remove-leading-alls f)) f))
 
83
 
 
84
(defun remove-leading-quants (f)
 
85
  (declare (xargs :guard (wff f)))
 
86
  (if (wfquant f)
 
87
      (remove-leading-quants (a2 f))
 
88
      f))
 
89
 
 
90
(defun leading-quants (f)
 
91
  (declare (xargs :guard (wff f)))
 
92
  (if (wfquant f)
 
93
      (cons (a1 f) (leading-quants (a2 f)))
 
94
      nil))
 
95
 
 
96
;;--------------------
 
97
 
 
98
(defthm leading-all-is-quantified-var
 
99
  (implies (not (member-equal x (quantified-vars f)))
 
100
           (not (member-equal x (leading-alls f)))))
 
101
 
 
102
(defthm setp-qvars-leading-alls
 
103
  (implies (setp (quantified-vars f))
 
104
           (setp (leading-alls f))))
 
105
 
 
106
(defthm varset-qvars-leading-alls
 
107
  (implies (var-set (quantified-vars f))
 
108
           (var-set (leading-alls f))))
 
109
 
 
110
;;------------
 
111
;; Prove that the universal closure of a formula is closed.
 
112
;; First prove thw two key properties, then do a resolution
 
113
;; step to get the result in terms of member-equal, then
 
114
;; get it in the desired form.
 
115
 
 
116
(defthm alls-eliminates-free-vars
 
117
  (implies (member-equal x vars)
 
118
           (not (member-equal x (free-vars (alls vars f))))))
 
119
 
 
120
(defthm alls-doesnt-introduce-free-vars
 
121
  (implies (not (member-equal x (free-vars f)))
 
122
           (not (member-equal x (free-vars (alls vars f))))))
 
123
 
 
124
(defthm universal-closure-is-closed-almost-in-final-form
 
125
  (not (member-equal x (free-vars (alls (free-vars f) f))))
 
126
  :hints (("Goal"
 
127
           :use ((:instance alls-eliminates-free-vars
 
128
                            (x x) (f f) (vars (free-vars f)))
 
129
                 (:instance alls-doesnt-introduce-free-vars
 
130
                            (x x) (f f) (vars (free-vars f))))
 
131
           )))
 
132
 
 
133
(defmacro universal-closure (f)
 
134
  (list 'alls (list 'free-vars f) f))
 
135
 
 
136
(defthm universal-closure-is-closed
 
137
  (not (free-vars (universal-closure f)))
 
138
  :hints (("Goal"
 
139
           :use ((:instance consp-has-member-equal
 
140
                            (x (free-vars (alls (free-vars f) f))))))))
 
141
 
 
142
;;-------------------------------------
 
143
;; Eval inductions on variables.  These functions give useful induction
 
144
;; schemes for proving soundness theorems about universal closures,
 
145
;; in particular about formulas (alls vars f), with evaluation function xeval.
 
146
;; Think of the two arguments "vars f" as "(alls vars f)".
 
147
 
 
148
(defun var-induct (vars f dom i)
 
149
  (declare (xargs :measure (cons (+ 1 (acl2-count vars)) (acl2-count dom))
 
150
                  :guard (and (var-list vars) (wff f)
 
151
                              (domain-term-list (fringe dom)))))
 
152
  (if (atom vars)
 
153
      nil
 
154
      (if (atom dom)
 
155
          (var-induct (cdr vars) (subst-free f (car vars) dom) (domain i) i)
 
156
          (cons (var-induct vars f (car dom) i)
 
157
                (var-induct vars f (cdr dom) i)))))
 
158
 
 
159
;; This induction scheme goes through two formulas together.
 
160
 
 
161
(defun var-induct-2 (vars f g dom i)
 
162
  (declare (xargs :measure (cons (+ 1 (acl2-count vars)) (acl2-count dom))
 
163
                  :guard (and (var-list vars) (wff f) (wff g)
 
164
                              (domain-term-list (fringe dom)))))
 
165
  (if (atom vars)
 
166
      nil
 
167
      (if (atom dom)
 
168
          (var-induct-2 (cdr vars)
 
169
                        (subst-free f (car vars) dom)
 
170
                        (subst-free g (car vars) dom)
 
171
                        (domain i) i)
 
172
          (cons (var-induct-2 vars f g (car dom) i)
 
173
                (var-induct-2 vars f g (cdr dom) i)))))
 
174
 
 
175
;-------------------------
 
176
 
 
177
(defthm not-free-feval-same
 
178
  (implies (and (variable-term x)
 
179
                (not (member-equal x (free-vars f))))
 
180
           (equal (feval-d (list 'all x f) dom i)
 
181
                  (feval f i)))
 
182
  :hints (("Goal"
 
183
           :induct (dom-i dom))
 
184
          ("Subgoal *1/1"
 
185
           :in-theory (enable not-free-not-change-2))))
 
186
 
 
187
(defthm feval-alls-true
 
188
  (implies (var-list vars)
 
189
           (feval (alls vars 'true) i)))
 
190
 
 
191
(defthm feval-alls-false
 
192
  (implies (var-list vars)
 
193
           (not (feval (alls vars 'false) i))))