← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2003/kaufmann/support/rtl/results/model-eq.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/2003/kaufmann/support/rtl/results/model-eq.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(local (defun %%sub1-induction (n)
 
4
              (if (zp n)
 
5
                  n (%%sub1-induction (1- n)))))
 
6
 
 
7
(local (defun %%and-tree-fn (args len)
 
8
              (declare (xargs :mode :program))
 
9
              (if (< len 20)
 
10
                  (cons 'and args)
 
11
                  (let* ((len2 (floor len 2)))
 
12
                        (list 'and
 
13
                              (%%and-tree-fn (take len2 args) len2)
 
14
                              (%%and-tree-fn (nthcdr len2 args)
 
15
                                             (- len len2)))))))
 
16
 
 
17
(local (defmacro %%and-tree (&rest args)
 
18
                 (%%and-tree-fn args (length args))))
 
19
 
 
20
(local (include-book "bvecp-raw"))
 
21
 
 
22
(local (include-book "rtl/rel4/lib/top"
 
23
                     :dir :system))
 
24
 
 
25
(local (include-book "rtl/rel4/lib/simplify-model-helpers"
 
26
                     :dir :system))
 
27
 
 
28
(include-book "model-raw")
 
29
 
 
30
(include-book "model")
 
31
 
 
32
(local (table user-defined-functions-table
 
33
              nil nil :clear))
 
34
 
 
35
(local (disable-forcing))
 
36
 
 
37
(local (deftheory theory-0 (theory 'minimal-theory)))
 
38
 
 
39
(local (defmacro %%p0-equalities nil
 
40
                 '(%%and-tree (equal (out1$ n $path)
 
41
                                     (foo$raw::out1$ n $path))
 
42
                              (equal (out2$ n $path)
 
43
                                     (foo$raw::out2$ n $path)))))
 
44
 
 
45
(local (defun %%p0-aux (n $path)
 
46
              (declare (xargs :normalize nil))
 
47
              (%%p0-equalities)))
 
48
 
 
49
(local (defun-sk %%p0 (n)
 
50
                 (forall ($path) (%%p0-aux n $path))))
 
51
 
 
52
(local (defthm %%p0-implies-%%p0-aux
 
53
               (implies (%%p0 n) (%%p0-aux n $path))))
 
54
 
 
55
(local (encapsulate
 
56
            nil
 
57
            (local (defthm %%p0-property-lemma
 
58
                           (implies (%%p0-aux n $path)
 
59
                                    (%%p0-equalities))
 
60
                           :rule-classes nil
 
61
                           :instructions ((:dv 1)
 
62
                                          (:expand nil)
 
63
                                          :top
 
64
                                          (:generalize ((%%p0-equalities) eqs))
 
65
                                          :s)))
 
66
            (defthm %%p0-property
 
67
                    (implies (%%p0 n) (%%p0-equalities))
 
68
                    :instructions ((:use %%p0-property-lemma)
 
69
                                   (:generalize ((%%p0-equalities) eqs))
 
70
                                   :prove))))
 
71
 
 
72
(local
 
73
     (deftheory %%p0-implies-f-is-%f-theory
 
74
                (union-theories (set-difference-theories (current-theory :here)
 
75
                                                         (current-theory '%%p0))
 
76
                                (theory 'minimal-theory))))
 
77
 
 
78
(local
 
79
     (encapsulate
 
80
          nil
 
81
          (local (in-theory (disable %%p0-property)))
 
82
          (local (defthm out2$-is-out2$-base
 
83
                         (implies (zp n)
 
84
                                  (equal (out2$ n $path)
 
85
                                         (foo$raw::out2$ n $path)))
 
86
                         :hints (("Goal" :expand ((out2$ n $path)
 
87
                                                  (foo$raw::out2$ n $path))))))
 
88
          (local (defthm out1$-is-out1$-base
 
89
                         (implies (zp n)
 
90
                                  (equal (out1$ n $path)
 
91
                                         (foo$raw::out1$ n $path)))
 
92
                         :hints (("Goal" :expand ((out1$ n $path)
 
93
                                                  (foo$raw::out1$ n $path))))))
 
94
          (defthm %%p0-base (implies (zp n) (%%p0 n))
 
95
                  :instructions (:promote :x-dumb (:s :normalize nil)))))
 
96
 
 
97
(local
 
98
     (encapsulate
 
99
          nil
 
100
          (local (in-theory (disable %%p0 %%p0-base)))
 
101
          (local (deflabel %%induction-start))
 
102
          (local (defthm out2$-is-out2$-induction_step
 
103
                         (implies (and (not (zp n)) (%%p0 (1- n)))
 
104
                                  (equal (out2$ n $path)
 
105
                                         (foo$raw::out2$ n $path)))
 
106
                         :instructions (:promote (:dv 1)
 
107
                                                 :x-dumb
 
108
                                                 :nx :x-dumb
 
109
                                                 :top (:s :normalize nil
 
110
                                                          :backchain-limit 1000
 
111
                                                          :expand :lambdas
 
112
                                                          :repeat 4))))
 
113
          (local (defthm out1$-is-out1$-induction_step
 
114
                         (implies (and (not (zp n)) (%%p0 (1- n)))
 
115
                                  (equal (out1$ n $path)
 
116
                                         (foo$raw::out1$ n $path)))
 
117
                         :instructions (:promote (:dv 1)
 
118
                                                 :x-dumb
 
119
                                                 :nx :x-dumb
 
120
                                                 :top (:s :normalize nil
 
121
                                                          :backchain-limit 1000
 
122
                                                          :expand :lambdas
 
123
                                                          :repeat 4))))
 
124
          (defthm %%p0-induction_step
 
125
                  (implies (and (not (zp n)) (%%p0 (1- n)))
 
126
                           (%%p0 n))
 
127
                  :instructions (:promote :x-dumb (:s :normalize nil)))))
 
128
 
 
129
(local
 
130
 (defthm
 
131
  %%p0-holds (%%p0 n)
 
132
  :hints
 
133
  (("Goal" :induct (%%sub1-induction n)
 
134
           :do-not '(preprocess)
 
135
           :in-theory (union-theories '(%%p0-base %%p0-induction_step
 
136
                                                  (:induction %%sub1-induction))
 
137
                                      (theory 'minimal-theory))))))
 
138
 
 
139
(ENCAPSULATE
 
140
 (
 
141
 )
 
142
 
 
143
 (local (in-theory (union-theories '(%%p0-holds)
 
144
                                   (theory '%%p0-implies-f-is-%f-theory))))
 
145
 
 
146
 (defthm out2$-is-out2$
 
147
         (equal (out2$ n $path)
 
148
                (foo$raw::out2$ n $path))
 
149
         :hints (("Goal" :do-not '(preprocess))))
 
150
 
 
151
 (defthm out1$-is-out1$
 
152
         (equal (out1$ n $path)
 
153
                (foo$raw::out1$ n $path))
 
154
         :hints (("Goal" :do-not '(preprocess))))
 
155
 
 
156
)
 
157
 
 
158
(deftheory %-removal-theory
 
159
           (union-theories '(out1$-is-out1$ out2$-is-out2$)
 
160
                           (theory 'minimal-theory)))
 
161