← 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/simple-check.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/simple-check.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This book is a little add-on to Ivy.  I imagine there will
 
4
;; times when we wish to simply check a proof object, without
 
5
;; using Ivy's preprocessing.  For example, if a prover
 
6
;; can build proof objects, but it is inconvenient to use
 
7
;; Ivy's preprocessing.
 
8
;;
 
9
;; Function (bcheck proof) below checks if its input is a proof
 
10
;; object, fixes the substitutions (just like refute-n-check),
 
11
;; and checks it.  Ths soundness theorems says that if the
 
12
;; input steps are true, then all the steps are true.
 
13
;;
 
14
;; Bcheck is similar to the checker of our 1994 Nqthm project.
 
15
;; (But we didn't have any soundness proofs back then.)
 
16
 
 
17
(include-book "derive")
 
18
 
 
19
;; Here is the checker function.  Compare it to refute-n-check
 
20
;; in book "derive".
 
21
 
 
22
(defun bcheck (prf)
 
23
  (declare (xargs :guard t))
 
24
  (if (not (wfproof prf))
 
25
      nil
 
26
    (let ((fixed-prf (fix-substs-in-prf
 
27
                      prf
 
28
                      (free-vars (extract-all-steps prf)))))
 
29
      (check-proof nil fixed-prf))))
 
30
 
 
31
;; Question to us: why weren't the following two lemmas needed
 
32
;; for soundness of refute-n-check?
 
33
 
 
34
(defthm extract-all-fixed
 
35
  (equal (extract-all-steps (fix-substs-in-prf prf vars))
 
36
         (extract-all-steps prf)))
 
37
 
 
38
(defthm extract-input-fixed
 
39
  (equal (extract-input-steps (fix-substs-in-prf prf vars))
 
40
         (extract-input-steps prf)))
 
41
 
 
42
;; Luckily, we can use theorem check-proof-xsound which we
 
43
;; used for soundness of refute-n-check.
 
44
 
 
45
(defthm bcheck-xsound
 
46
  (implies
 
47
   (and (bcheck prf)
 
48
        (xeval (universal-closure (extract-input-steps prf)) (domain i) i))
 
49
   (xeval (universal-closure (extract-all-steps prf)) (domain i) i))
 
50
  :hints (("Goal"
 
51
           :do-not-induct t
 
52
           :use ((:instance check-proof-xsound
 
53
                            (prf (fix-substs-in-prf
 
54
                                  prf
 
55
                                  (free-vars (extract-all-steps prf))
 
56
                                  )))))))
 
57
 
 
58
;; Now state it in terms of the official evaluation function feval.
 
59
 
 
60
(defthm bcheck-fsound
 
61
  (implies (and (bcheck prf)
 
62
                (feval (universal-closure (extract-input-steps prf)) i))
 
63
           (feval (universal-closure (extract-all-steps prf)) i))
 
64
  :hints (("Goal"
 
65
           :in-theory (enable xeval-feval)
 
66
           :do-not-induct t)))
 
67