← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2003/gamboa-cowles-van-baalen/support/kalman-proof.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/gamboa-cowles-van-baalen/support/kalman-proof.lisp
 
1
; The ACL2 Matrix Algebra Book. Summary of definitions and algebra in matrix.lisp.
 
2
; Copyright (C) 2002 Ruben Gamboa and John R. Cowles, University of Wyoming
 
3
 
 
4
; This book is free software; you can redistribute it and/or modify
 
5
; it under the terms of the GNU General Public License as published by
 
6
; the Free Software Foundation; either version 2 of the License, or
 
7
; (at your option) any later version.
 
8
 
 
9
; This book is distributed in the hope that it will be useful,
 
10
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
; GNU General Public License for more details.
 
13
 
 
14
; You should have received a copy of the GNU General Public License
 
15
; along with this book; if not, write to the Free Software
 
16
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
17
 
 
18
; Written by:
 
19
; Ruben Gamboa and John Cowles
 
20
; Department of Computer Science
 
21
; University of Wyoming
 
22
; Laramie, WY 82071-3682 U.S.A.
 
23
 
 
24
; Summer and Fall 2002.
 
25
;  Last modified 1 November 2002.
 
26
 
 
27
#|
 
28
 To certify in ACL2 Version 2.6
 
29
 
 
30
  (ld ;; Newline to fool dependency scanner
 
31
   "defpkg.lsp")
 
32
  (certify-book "kalman-proof" 1)
 
33
|#
 
34
 
 
35
(in-package "KALMAN")
 
36
 
 
37
(include-book "kalman-defs")
 
38
 
 
39
(defmacro enable-disable (enable-list disable-list)
 
40
  (list 'union-theories
 
41
        (cons 'disable disable-list)
 
42
        `(quote ,enable-list)))
 
43
 
 
44
(defstub best-estimate-of-x (*) => *)
 
45
 
 
46
(defun best-prior-estimate-of-x (k)
 
47
  (if (zp k)
 
48
      (xhatmin k)
 
49
    (m-* (phi (1- k)) 
 
50
         (best-estimate-of-x (1- k)))))
 
51
 
 
52
(defun result-form (y Xp k)
 
53
  (m-+ Xp
 
54
       (m-* y
 
55
            (m-- (z k)
 
56
                 (m-* (h k)
 
57
                      Xp)))))
 
58
 
 
59
(defun result-form-derivative (y Xp k)
 
60
  (m-+ (s-* 2 (m-mean (m-* (m-- Xp (x k))
 
61
                           (m-trans (m-- (z k)
 
62
                                         (m-* (h k) Xp))))))
 
63
       (s-* 2 (m-* y
 
64
                   (m-mean (m-* (m-- (z k)
 
65
                                     (m-* (h k) Xp))
 
66
                                (m-trans (m-- (z k)
 
67
                                              (m-* (h k) Xp)))))))))
 
68
  
 
69
(defaxiom best-estimate-of-x-def
 
70
  (implies (and (m-= (best-prior-estimate-of-x k) Xp)
 
71
                (m-= (result-form-derivative y Xp k) (m-zero (n) (m))))
 
72
           (m-= (best-estimate-of-x k)
 
73
                (result-form y Xp k))))
 
74
 
 
75
(skip-proofs
 
76
 (defthm non-singular-gain-component
 
77
   (not (m-singular (m-mean (m-* (m-+ (z k)
 
78
                                 (m-unary-- (m-* (h k) (xhatmin k))))
 
79
                            (m-+ (m-trans (z k))
 
80
                                 (m-unary-- (m-* (m-trans (xhatmin k))
 
81
                                                 (m-trans (h k)))))))))))
 
82
 
 
83
(skip-proofs
 
84
 (defthm non-singular-gain-component-2
 
85
   (not (m-singular (m-+ (r k) (m-* (h k) (m-* (pminus k) (m-trans (h k)))))))))
 
86
 
 
87
(defthm pminus-as-mean-case-0
 
88
  (implies (= k 0)
 
89
           (m-= (pminus k)
 
90
                (m-mean (m-* (m-- (x k) (xhatmin k))
 
91
                             (m-trans (m-- (x k) (xhatmin k)))))))
 
92
  :hints (("Goal"
 
93
           :expand ((pminus k))
 
94
           :in-theory (enable-disable (pminus xhatmin)
 
95
                                      (x ; added by Matt K. for v2-8, 7/31/03
 
96
                                       (pminus) (xhatmin))))))
 
97
 
 
98
(encapsulate
 
99
 ()
 
100
 
 
101
 (local
 
102
  (defthm lemma-1
 
103
    (implies (and (integerp k)
 
104
                  (< 0 k))
 
105
             (equal (m-- (x k) (xhatmin k))
 
106
                    (m-- (m-+ (m-* (phi (1- k)) (x (1- k)))
 
107
                              (ww (1- k)))
 
108
                         (m-* (phi (1- k))
 
109
                              (xhat (1- k))))))
 
110
    :hints (("Goal" :do-not-induct t
 
111
             :in-theory (disable xhat)))
 
112
    :rule-classes nil))
 
113
 
 
114
 (local
 
115
  (defthm lemma-2
 
116
    (implies (and (integerp k)
 
117
                  (< 0 k))
 
118
             (equal (m-- (x k) (xhatmin k))
 
119
                    (m-+ (m-* (phi (1- k))
 
120
                              (m-- (x (1- k))
 
121
                                   (xhat (1- k))))
 
122
                         (ww (1- k)))))
 
123
    :hints (("Goal" :do-not-induct t
 
124
             :use ((:instance lemma-1)
 
125
                   (:instance (:theorem 
 
126
                               (implies (and (m-matrixp (l phi) (c phi) phi)
 
127
                                             (m-matrixp (l x) (c x) x)
 
128
                                             (m-matrixp (l xhat) (c xhat) xhat)
 
129
                                             (m-matrixp (l ww) (c x) ww)
 
130
                                             (equal (c phi) (l x))
 
131
                                             (equal (l phi) (l ww))
 
132
                                             (equal (c x) (c ww))
 
133
                                             (equal (c phi) (l xhat))
 
134
                                             (equal (c x) (c xhat))
 
135
                                             (equal (l x) (l xhat)))
 
136
                                        (equal (m-- (m-+ (m-* phi x)
 
137
                                                         ww)
 
138
                                                    (m-* phi xhat))
 
139
                                               (m-+ (m-* phi (m-- x xhat))
 
140
                                                    ww))))
 
141
                              (phi (phi (1- k)))
 
142
                              (x (x (1- k)))
 
143
                              (ww (ww (1- k)))
 
144
                              (xhat (xhat (1- k))))))
 
145
            ("Subgoal 2'" :in-theory nil))
 
146
    :rule-classes nil))
 
147
 
 
148
 (local 
 
149
  (defthm lemma-3a
 
150
    (implies (and (m-matrixp (l a) (c a) a)
 
151
                  (m-matrixp (l b) (c b) b)
 
152
                  (equal (l a) (l b))
 
153
                  (equal (c a) (c b)))
 
154
             (m-= (m-* (m-+ a b)
 
155
                       (m-trans (m-+ a b)))
 
156
                  (m-+ (m-* a (m-trans a))
 
157
                       (m-+ (m-* a (m-trans b))
 
158
                            (m-+ (m-* b (m-trans a))
 
159
                                 (m-* b (m-trans b)))))))
 
160
    :rule-classes nil))
 
161
 
 
162
 (local
 
163
  (defthm lemma-3b-1
 
164
    (implies (and (m-= (m-* (m-+ (m-* phi (m-+ x (m-unary-- xhat))) ww)
 
165
                            (m-trans (m-+ (m-* phi (m-+ x (m-unary-- xhat))) ww)))
 
166
                       (m-+ (m-* phi 
 
167
                                 (m-* (m-+ x (m-unary-- xhat))
 
168
                                      (m-trans (m-* phi 
 
169
                                                    (m-+ x 
 
170
                                                         (m-unary-- xhat))))))
 
171
                            (m-+ (m-* phi (m-* (m-+ x (m-unary-- xhat))
 
172
                                               (m-trans ww)))
 
173
                                 (m-+ (m-* ww 
 
174
                                           (m-trans (m-* phi 
 
175
                                                         (m-+ x 
 
176
                                                              (m-unary-- xhat)))))
 
177
                                      (m-* ww (m-trans ww))))))
 
178
                  (m-matrixp (l x) (c x) x)
 
179
                  (m-matrixp (l xhat) (c xhat) xhat)
 
180
                  (m-matrixp (l phi) (c phi) phi)
 
181
                  (m-matrixp (l ww) (c ww) ww)
 
182
                  (equal (l phi) (l ww))
 
183
                  (equal (c x) (c ww))
 
184
                  (equal (c phi) (l x))
 
185
                  (equal (c ww) (c xhat))
 
186
                  (equal (l x) (l xhat)))
 
187
             (m-= (m-* (m-+ (m-* phi (m-+ x (m-unary-- xhat))) ww)
 
188
                       (m-trans (m-+ (m-* phi (m-+ x (m-unary-- xhat))) ww)))
 
189
                  (m-+ (m-* phi (m-* (m-+ x (m-unary-- xhat))
 
190
                                     (m-* (m-trans (m-+ x (m-unary-- xhat)))
 
191
                                          (m-trans phi))))
 
192
                   (m-+ (m-* phi (m-* (m-+ x (m-unary-- xhat)) (m-trans ww)))
 
193
                        (m-+ (m-* ww (m-* (m-trans (m-+ x (m-unary-- xhat)))
 
194
                                          (m-trans phi)))
 
195
                             (m-* ww (m-trans ww)))))))
 
196
    :hints (("Goal"
 
197
             :use ((:instance acl2::trans-*
 
198
                              (acl2::p phi)
 
199
                              (acl2::q (m-- x xhat))))
 
200
             :in-theory (disable acl2::trans-*
 
201
                                 acl2::*-+-right
 
202
                                 acl2::*-+-left)))
 
203
    :rule-classes nil))
 
204
 
 
205
 (local
 
206
  (defthm lemma-3b
 
207
    (implies (and (m-matrixp (l x) (c x) x)
 
208
                  (m-matrixp (l xhat) (c xhat) xhat)
 
209
                  (m-matrixp (l phi) (c phi) phi)
 
210
                  (m-matrixp (l ww) (c ww) ww)
 
211
                  (equal (c phi) (l x))
 
212
                  (equal (l phi) (l ww))
 
213
                  (equal (c x) (c ww))
 
214
                  (equal (c phi) (l xhat))
 
215
                  (equal (c x) (c xhat))
 
216
                  (equal (l x) (l xhat)))
 
217
             (m-= (m-* (m-+ (m-* phi (m-- x xhat)) ww)
 
218
                       (m-trans (m-+ (m-* phi (m-- x xhat)) ww)))
 
219
                  (m-+ (m-* (m-* phi (m-- x xhat)) (m-* (m-trans (m-- x xhat))
 
220
                                                        (m-trans phi)))
 
221
                       (m-+ (m-* (m-* phi (m-- x xhat)) (m-trans ww))
 
222
                            (m-+ (m-* ww (m-* (m-trans (m-- x xhat))
 
223
                                              (m-trans phi)))
 
224
                                 (m-* ww (m-trans ww)))))))
 
225
    :hints (("Goal"
 
226
             :use ((:instance lemma-3a
 
227
                              (a (m-* phi (m-- x xhat)))
 
228
                              (b ww))))
 
229
            ("Goal''"
 
230
             :use ((:instance lemma-3b-1))
 
231
             :in-theory (disable acl2::trans-* 
 
232
                                 acl2::*-+-right
 
233
                                 acl2::*-+-left)))
 
234
    :rule-classes nil))
 
235
 
 
236
 (local
 
237
  (defthm lemma-3
 
238
    (m-= (m-* (m-+ (m-* (phi (1- k)) (m-- (x (1- k)) (xhat (1- k))))
 
239
                     (ww (1- k)))
 
240
                (m-trans (m-+ (m-* (phi (1- k))
 
241
                                   (m-- (x (1- k)) (xhat (1- k)))) 
 
242
                              (ww (1- k)))))
 
243
           (m-+ (m-* (m-* (phi (1- k)) 
 
244
                          (m-- (x (1- k)) (xhat (1- k))))
 
245
                     (m-* (m-trans (m-- (x (1- k)) (xhat (1- k))))
 
246
                          (m-trans (phi (1- k)))))
 
247
                (m-+ (m-* (m-* (phi (1- k))
 
248
                               (m-- (x (1- k)) (xhat (1- k))))
 
249
                          (m-trans (ww (1- k))))
 
250
                     (m-+ (m-* (ww (1- k)) 
 
251
                               (m-* (m-trans (m-- (x (1- k)) 
 
252
                                                  (xhat (1- k))))
 
253
                                    (m-trans (phi (1- k)))))
 
254
                          (m-* (ww (1- k)) (m-trans (ww (1- k))))))))
 
255
    :hints (("Goal"
 
256
             :use ((:instance lemma-3b
 
257
                              (phi (phi (1- k)))
 
258
                              (x (x (1- k)))
 
259
                              (ww (ww (1- k)))
 
260
                              (xhat (xhat (1- k)))))))
 
261
    :rule-classes nil))
 
262
 
 
263
 (local
 
264
  (defthm lemma-4a
 
265
    (m-= (M-MEAN
 
266
          (ACL2::M-BINARY-* (PHI (+ -1 K))
 
267
                            (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X (+ -1 K))
 
268
                                                                (ACL2::M-UNARY-- (XHAT (+ -1 K))))
 
269
                                              (ACL2::M-TRANS (WW (+ -1 K))))))
 
270
         (m-zero (n) (n)))
 
271
    :hints (("Goal" :do-not-induct t
 
272
             :use ((:instance mean-*
 
273
                              (p (phi (+ -1 k)))
 
274
                              (q (m-* (m-+ (x (+ -1 k))
 
275
                                           (m-unary-- (xhat (+ -1 k))))
 
276
                                      (m-trans (ww (+ -1 k))))))
 
277
                   (:instance mean-of-x-xhat*wtrans
 
278
                              (k (1- k))))
 
279
             :in-theory (disable xhat z 
 
280
                                 acl2::*-+-right
 
281
                                 mean-of-x-xhat*wtrans)))))
 
282
 
 
283
 (local
 
284
  (defthm lemma-4b
 
285
    (m-= (M-MEAN
 
286
          (ACL2::M-BINARY-* (WW (+ -1 K))
 
287
                            (ACL2::M-BINARY-*
 
288
                             (ACL2::M-BINARY-+ (ACL2::M-TRANS (X (+ -1 K)))
 
289
                                               (ACL2::M-UNARY-- (ACL2::M-TRANS (XHAT (+ -1 K)))))
 
290
                             (ACL2::M-TRANS (PHI (+ -1 K))))))
 
291
           (m-zero (n) (n)))
 
292
    :hints (("Goal" :do-not-induct t
 
293
             :use ((:instance mean-*
 
294
                              (p (m-* (ww (+ -1 k))
 
295
                                      (m-+ (m-trans (x (+ -1 k)))
 
296
                                           (m-unary-- (m-trans (xhat (+ -1 k)))))))
 
297
                              (q (m-trans (phi (+ -1 k)))))
 
298
                   (:instance mean-of-w*trans-of-x-xhat
 
299
                              (k (1- k))))
 
300
             :in-theory (disable xhat z 
 
301
                                 acl2::*-+-right
 
302
                                 mean-of-w*trans-of-x-xhat)))))
 
303
 
 
304
 
 
305
 (local
 
306
  (defthm lemma-4c
 
307
    (m-= (M-MEAN 
 
308
          (ACL2::M-BINARY-* (PHI (+ -1 K))
 
309
                            (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X (+ -1 K))
 
310
                                                                (ACL2::M-UNARY-- (XHAT (+ -1 K))))
 
311
                                              (ACL2::M-BINARY-*
 
312
                                               (ACL2::M-BINARY-+ (ACL2::M-TRANS (X (+ -1 K)))
 
313
                                                                 (ACL2::M-UNARY-- (ACL2::M-TRANS (XHAT (+ -1 K)))))
 
314
                                               (ACL2::M-TRANS (PHI (+ -1 K)))))))
 
315
         (m-* (m-* (phi (1- k))
 
316
                   (m-mean (m-* (m-+ (x (+ -1 k))
 
317
                                     (m-unary-- (xhat (+ -1 k))))
 
318
                                (m-trans (m-+ (x (+ -1 k))
 
319
                                              (m-unary-- (xhat (+ -1 k))))))))
 
320
              (m-trans (phi (1- k)))))
 
321
    :hints (("Goal" :do-not-induct t
 
322
             :use ((:instance mean-*
 
323
                              (p (m-* (phi (1- k))
 
324
                                      (m-* (m-+ (x (+ -1 k))
 
325
                                                (m-unary-- (xhat (+ -1 k))))
 
326
                                           (m-trans (m-+ (x (+ -1 k))
 
327
                                                         (m-unary-- (xhat (+ -1 k))))))))
 
328
                              (q (m-trans (phi (+ -1 k)))))
 
329
                   (:instance mean-*
 
330
                              (p (phi (+ -1 k)))
 
331
                              (q (m-* (m-+ (x (+ -1 k))
 
332
                                           (m-unary-- (xhat (+ -1 k))))
 
333
                                      (m-trans (m-+ (x (+ -1 k))
 
334
                                                    (m-unary-- (xhat (+ -1 k))))))))
 
335
                   (:instance mean-delete
 
336
                              (p (phi (1- k)))))
 
337
             :in-theory (disable xhat z acl2::*-+-right)))))
 
338
 
 
339
 (local 
 
340
  (defthm lemma-4-1
 
341
    (acl2::m-=
 
342
     (m-mean
 
343
      (acl2::m-binary-+
 
344
       (acl2::m-binary-*
 
345
        (phi (+ -1 k))
 
346
        (acl2::m-binary-*
 
347
         (acl2::m-binary-+ (x (+ -1 k))
 
348
                           (acl2::m-unary-- (xhat (+ -1 k))))
 
349
         (acl2::m-binary-*
 
350
          (acl2::m-binary-+ (acl2::m-trans (x (+ -1 k)))
 
351
                            (acl2::m-unary-- (acl2::m-trans (xhat (+ -1 k)))))
 
352
          (acl2::m-trans (phi (+ -1 k))))))
 
353
       (acl2::m-binary-+
 
354
        (acl2::m-binary-*
 
355
         (phi (+ -1 k))
 
356
         (acl2::m-binary-* (acl2::m-binary-+ (x (+ -1 k))
 
357
                                             (acl2::m-unary-- (xhat (+ -1 k))))
 
358
                           (acl2::m-trans (ww (+ -1 k)))))
 
359
        (acl2::m-binary-+
 
360
         (acl2::m-binary-* (ww (+ -1 k))
 
361
                           (acl2::m-trans (ww (+ -1 k))))
 
362
         (acl2::m-binary-*
 
363
          (ww (+ -1 k))
 
364
          (acl2::m-binary-*
 
365
           (acl2::m-binary-+ (acl2::m-trans (x (+ -1 k)))
 
366
                             (acl2::m-unary-- (acl2::m-trans (xhat (+ -1 k)))))
 
367
           (acl2::m-trans (phi (+ -1 k)))))))))
 
368
     (acl2::m-binary-+
 
369
      (q (+ -1 k))
 
370
      (acl2::m-binary-*
 
371
       (phi (+ -1 k))
 
372
       (acl2::m-binary-*
 
373
        (m-mean
 
374
         (acl2::m-binary-*
 
375
          (acl2::m-binary-+ (x (+ -1 k))
 
376
                            (acl2::m-unary-- (xhat (+ -1 k))))
 
377
          (acl2::m-binary-+ (acl2::m-trans (x (+ -1 k)))
 
378
                            (acl2::m-unary-- (acl2::m-trans (xhat (+ -1 k)))))))
 
379
        (acl2::m-trans (phi (+ -1 k)))))))    
 
380
    :hints (("Goal" :in-theory (disable acl2::*-+-right 
 
381
                                        acl2::*---right 
 
382
                                        acl2::*-+-left
 
383
                                        acl2::*---left
 
384
                                        acl2::right-distributivity-of-m-*-over-m-+
 
385
                                        acl2::left-distributivity-of-m-*-over-m-+
 
386
                                        xhat x z xhatmin-recdef gain-recdef)))))
 
387
 
 
388
 (local
 
389
  (defthm lemma-4
 
390
    (m-= (m-mean (m-* (m-+ (m-* (phi (1- k)) (m-- (x (1- k)) (xhat (1- k))))
 
391
                           (ww (1- k)))
 
392
                      (m-trans (m-+ (m-* (phi (1- k))
 
393
                                         (m-- (x (1- k)) (xhat (1- k)))) 
 
394
                                    (ww (1- k))))))
 
395
         (m-+ (m-* (m-* (phi (1- k)) 
 
396
                        (m-mean (m-* (m-- (x (1- k)) (xhat (1- k)))
 
397
                                     (m-trans (m-- (x (1- k)) (xhat (1- k)))))))
 
398
                   (m-trans (phi (1- k))))
 
399
              (q (1- k))))
 
400
    :hints (("Goal"
 
401
             :use ((:instance lemma-3))
 
402
             :in-theory nil)
 
403
            ("Goal'"
 
404
             :use ((:theorem  (m-=
 
405
                               (m-mean
 
406
                                (m-+ (m-* (m-* (phi (+ -1 k))
 
407
                                               (m-- (x (+ -1 k)) (xhat (+ -1 k))))
 
408
                                          (m-* (m-trans (m-- (x (+ -1 k)) (xhat (+ -1 k))))
 
409
                                               (m-trans (phi (+ -1 k)))))
 
410
                                     (m-+ (m-* (m-* (phi (+ -1 k))
 
411
                                                    (m-- (x (+ -1 k)) (xhat (+ -1 k))))
 
412
                                               (m-trans (ww (+ -1 k))))
 
413
                                          (m-+ (m-* (ww (+ -1 k))
 
414
                                                    (m-* (m-trans (m-- (x (+ -1 k)) (xhat (+ -1 k))))
 
415
                                                         (m-trans (phi (+ -1 k)))))
 
416
                                               (m-* (ww (+ -1 k))
 
417
                                                    (m-trans (ww (+ -1 k))))))))
 
418
                               (m-+ (m-* (m-* (phi (+ -1 k))
 
419
                                              (m-mean (m-* (m-- (x (+ -1 k)) (xhat (+ -1 k)))
 
420
                                                           (m-trans (m-- (x (+ -1 k)) (xhat (+ -1 k)))))))
 
421
                                         (m-trans (phi (+ -1 k))))
 
422
                                    (q (+ -1 k))))))
 
423
             :in-theory (disable acl2::*-+-right
 
424
                                 acl2::*---right
 
425
                                 acl2::*-+-left
 
426
                                 acl2::*---left
 
427
                                 acl2::right-distributivity-of-m-*-over-m-+
 
428
                                 acl2::left-distributivity-of-m-*-over-m-+
 
429
                                 acl2::commutativity-2-of-m-+
 
430
                                 xhat 
 
431
                                 x
 
432
                                 z
 
433
                                 xhatmin-recdef
 
434
                                 gain-recdef)))
 
435
    :rule-classes nil))
 
436
 
 
437
 (local
 
438
  (defthm lemma-5
 
439
    (implies (and (integerp k)
 
440
                  (< 0 k))
 
441
             (m-= (m-mean (m-* (m-- (x k) (xhatmin k))
 
442
                               (m-trans (m-- (x k) (xhatmin k)))))
 
443
                  (m-+ (m-* (m-* (phi (1- k)) 
 
444
                                 (m-mean (m-* (m-- (x (1- k)) (xhat (1- k)))
 
445
                                              (m-trans (m-- (x (1- k)) (xhat (1- k)))))))
 
446
                            (m-trans (phi (1- k))))
 
447
                       (q (1- k)))))
 
448
    :hints (("Goal" :do-not-induct t
 
449
             :use ((:instance lemma-2)
 
450
                   (:instance lemma-4))
 
451
             :in-theory (disable x xhat xhatmin-recdef 
 
452
                                 acl2::*-+-right
 
453
                                 acl2::*---right
 
454
                                 acl2::*-+-left
 
455
                                 acl2::*---left
 
456
                                 acl2::right-distributivity-of-m-*-over-m-+
 
457
                                 acl2::left-distributivity-of-m-*-over-m-+
 
458
                                 acl2::commutativity-2-of-m-+)))
 
459
    :rule-classes nil))
 
460
 
 
461
 (defthm pminus-as-mean-almost
 
462
   (implies (and (integerp k)
 
463
                 (< 0 k)
 
464
                 (m-= (pplus (1- k))
 
465
                      (m-mean (m-* (m-- (x (1- k))
 
466
                                        (xhat (1- k)))
 
467
                                   (m-trans (m-- (x (1- k))
 
468
                                                 (xhat (1- k))))))))
 
469
            (m-= (pminus k)
 
470
                 (m-mean (m-* (m-- (x k) (xhatmin k))
 
471
                              (m-trans (m-- (x k) (xhatmin k)))))))
 
472
   :hints (("Goal" :do-not-induct t
 
473
            :use ((:instance lemma-5))
 
474
            :in-theory (disable x xhat xhatmin 
 
475
                                gain-recdef pplus-recdef xhatmin-recdef
 
476
                                acl2::*-+-right
 
477
                                acl2::*---right
 
478
                                acl2::*-+-left
 
479
                                acl2::*---left
 
480
                                acl2::right-distributivity-of-m-*-over-m-+
 
481
                                acl2::left-distributivity-of-m-*-over-m-+
 
482
                                acl2::commutativity-2-of-m-+))))
 
483
 )
 
484
 
 
485
(defthm matrix-*-trans
 
486
  (implies (and (equal m (l x))
 
487
                (equal n (l x))
 
488
                (m-matrixp m n x))
 
489
           (m-matrixp m n (m-* x (m-trans x)))))
 
490
 
 
491
(defthm id-*-x-useful
 
492
   (implies (and (equal (l p) n)
 
493
                 (m-matrixp (l p) (c p) p))
 
494
            (m-= (m-* (m-id n) p) p))
 
495
   :hints (("Goal"
 
496
            :use ((:instance acl2::id-*-x
 
497
                             (acl2::n (l p))
 
498
                             (acl2::n2 (c p))
 
499
                             (acl2::p p)))
 
500
            :in-theory (disable acl2::id-*-x))))
 
501
 
 
502
(defthm x-*-id-useful
 
503
   (implies (and (equal (c p) n)
 
504
                 (m-matrixp (l p) (c p) p))
 
505
            (m-= (m-* p (m-id n)) p))
 
506
   :hints (("Goal"
 
507
            :use ((:instance acl2::x-*-id
 
508
                             (acl2::m (l p))
 
509
                             (acl2::n (c p))
 
510
                             (acl2::p p)))
 
511
            :in-theory (disable acl2::x-*-id))))
 
512
 
 
513
(encapsulate
 
514
 ()
 
515
 
 
516
 (local
 
517
  (defthm lemma-1
 
518
    (m-= (m-- (x k) (xhat k))
 
519
         (m-- (m-* (m-- (m-id (n))
 
520
                        (m-* (gain k) (h k)))
 
521
                   (m-- (x k) (xhatmin k)))
 
522
              (m-* (gain k)
 
523
                   (v k))))
 
524
    :hints (("Goal" :do-not-induct t
 
525
             :use ((:instance acl2::id-*-x
 
526
                              (acl2::p (x k))
 
527
                              (acl2::n (n))
 
528
                              (acl2::n2 1))
 
529
                   (:instance acl2::id-*-x
 
530
                              (acl2::p (xhatmin k))
 
531
                              (acl2::n (n))
 
532
                              (acl2::n2 1)))
 
533
             :in-theory (disable acl2::id-*-x)))
 
534
    :rule-classes nil))
 
535
               
 
536
 
 
537
 (local 
 
538
  (defthm lemma-2a
 
539
    (implies (and (equal (l a) (l b))
 
540
                  (equal (c a) (c b))
 
541
                  (m-matrixp (l b) (c b) b)
 
542
                  (m-matrixp (l a) (c a) a))
 
543
             (m-= (m-* (m-- a b)
 
544
                       (m-trans (m-- a b)))
 
545
                  (m-+ (m-* a (m-trans a))
 
546
                       (m-+ (m-unary-- (m-* a (m-trans b)))
 
547
                            (m-+ (m-unary-- (m-* b (m-trans a)))
 
548
                                 (m-* b (m-trans b)))))))
 
549
    :hints (("Goal"
 
550
             :use ((:instance acl2::unary---unary--
 
551
                              (acl2::p (m-* b (m-trans b)))))
 
552
             :in-theory (disable acl2::unary---unary--)))
 
553
    :rule-classes nil))
 
554
 
 
555
 (local
 
556
  (defthm lemma-2
 
557
    (m-= (m-* (m-- (x k) (xhat k))
 
558
              (m-trans (m-- (x k) (xhat k))))
 
559
         (m-+ (m-* (m-- (m-id (n))
 
560
                        (m-* (gain k) (h k)))
 
561
                   (m-* (m-* (m-- (x k) (xhatmin k))
 
562
                             (m-trans (m-- (x k) (xhatmin k))))
 
563
                        (m-trans (m-- (m-id (n))
 
564
                                      (m-* (gain k) (h k))))))
 
565
              (m-+ (m-unary-- (m-* (m-- (m-id (n))
 
566
                                        (m-* (gain k) (h k)))
 
567
                                   (m-* (m-* (m-- (x k) (xhatmin k))
 
568
                                             (m-trans (v k)))
 
569
                                        (m-trans (gain k)))))
 
570
                   (m-+ (m-unary-- (m-* (gain k) 
 
571
                                        (m-* (m-* (v k)
 
572
                                                  (m-trans (m-- (x k) (xhatmin k))))
 
573
                                             (m-trans (m-- (m-id (n))
 
574
                                                           (m-* (gain k) (h k)))))))
 
575
                        (m-* (gain k)
 
576
                             (m-* (m-* (v k)
 
577
                                       (m-trans (v k)))
 
578
                                  (m-trans (gain k))))))))
 
579
    :hints (("Goal"
 
580
             :use ((:instance lemma-1)
 
581
                   (:instance lemma-2a
 
582
                              (a (m-* (m-- (m-id (n))
 
583
                                           (m-* (gain k) (h k)))
 
584
                                      (m-- (x k) (xhatmin k))))
 
585
                              (b (m-* (gain k)
 
586
                                      (v k)))))
 
587
             :in-theory (disable x xhat xhatmin 
 
588
                                 gain-recdef pplus-recdef xhatmin-recdef
 
589
                                 acl2::*-+-right
 
590
                                 acl2::*-+-left
 
591
                                 acl2::*---right
 
592
                                 acl2::*---left
 
593
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
594
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))
 
595
    :rule-classes nil))
 
596
 
 
597
 
 
598
 (local
 
599
  (defthm lemma-3a1
 
600
    (and (equal (l (m-- (x k) (xhatmin k))) (n))
 
601
         (equal (c (m-- (m-id (n)) (m-* (gain k) (h k)))) (n)))))
 
602
 
 
603
 (local
 
604
  (defthm lemma-3a
 
605
    (m-= (m-mean (ACL2::M-BINARY-*
 
606
                  (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
607
                                    (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
608
                  (ACL2::M-BINARY-*
 
609
                   (ACL2::M-BINARY-+ (X K)
 
610
                                     (ACL2::M-UNARY-- (XHATMIN K)))
 
611
                   (ACL2::M-BINARY-*
 
612
                    (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
613
                                      (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
614
                    (ACL2::M-BINARY-+
 
615
                     (ACL2::M-1 (N))
 
616
                     (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
617
                                                        (ACL2::M-TRANS (GAIN K)))))))))
 
618
         (m-* (m-- (m-id (n))
 
619
                   (m-* (gain k) (h k)))
 
620
              (m-* (m-mean (m-* (m-- (x k) (xhatmin k))
 
621
                                (m-trans (m-- (x k) (xhatmin k)))))
 
622
                   (m-trans (m-- (m-id (n))
 
623
                                 (m-* (gain k) (h k)))))))
 
624
    :hints (("Goal"
 
625
             :use ((:instance mean-*
 
626
                              (p (m-- (m-id (n))
 
627
                                      (m-* (gain k) (h k))))
 
628
                              (q (m-* (m-- (x k) (xhatmin k))
 
629
                                      (m-* (m-trans (m-- (x k) (xhatmin k)))
 
630
                                           (m-trans (m-- (m-id (n))
 
631
                                                         (m-* (gain k) (h k))))))))
 
632
                   (:instance mean-*
 
633
                              (p (m-* (m-- (x k) (xhatmin k))
 
634
                                      (m-trans (m-- (x k) (xhatmin k)))))
 
635
                              (q (m-trans (m-- (m-id (n))
 
636
                                               (m-* (gain k) (h k))))))
 
637
                   (:instance mean-delete
 
638
                              (p (m-id (n))))
 
639
                   (:instance mean-delete
 
640
                              (p (m-* (gain k) (h k)))))
 
641
             :in-theory (disable x xhatmin gain gain-recdef
 
642
                                 acl2::*-+-right
 
643
                                 acl2::*-+-left
 
644
                                 acl2::*---right
 
645
                                 acl2::*---left
 
646
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
647
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
648
                                        ;acl2::trans-* acl2::trans-+ acl2::trans---
 
649
                                 )))))
 
650
 
 
651
 (local
 
652
  (defthm lemma-3b
 
653
    (m-= (m-mean (ACL2::M-UNARY--
 
654
                  (ACL2::M-BINARY-*
 
655
                   (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
656
                                     (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
657
                   (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
658
                                                       (ACL2::M-UNARY-- (XHATMIN K)))
 
659
                                     (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
660
                                                       (ACL2::M-TRANS (GAIN K)))))))
 
661
         (m-zero (n) (n)))
 
662
    :hints (("Goal" :do-not-induct t
 
663
             :use ((:instance mean-*
 
664
                              (p (m-- (m-id (n))
 
665
                                      (m-* (gain k) (h k))))
 
666
                              (q (m-* (m-* (m-- (x k) (xhatmin k))
 
667
                                           (m-trans (v k)))
 
668
                                      (m-trans (gain k)))))
 
669
                   (:instance mean-*
 
670
                              (p (m-* (m-- (x k) (xhatmin k))
 
671
                                      (m-trans (v k))))
 
672
                              (q (m-trans (gain k))))
 
673
                   (:instance mean-of-x-xhatmin*vtrans))
 
674
             :in-theory (disable mean-of-x-xhatmin*vtrans
 
675
                                 mean-+
 
676
                                 acl2::*-+-right
 
677
                                 acl2::*-+-left
 
678
                                 acl2::*---right
 
679
                                 acl2::*---left
 
680
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
681
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
682
                                 )))))
 
683
 
 
684
 (local
 
685
  (defthm lemma-3c
 
686
    (m-=  (M-MEAN
 
687
           (ACL2::M-UNARY--
 
688
            (ACL2::M-BINARY-*
 
689
             (GAIN K)
 
690
             (ACL2::M-BINARY-*
 
691
              (V K)
 
692
              (ACL2::M-BINARY-*
 
693
               (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
694
                                 (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
695
               (ACL2::M-BINARY-+
 
696
                (ACL2::M-1 (N))
 
697
                (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
698
                                                   (ACL2::M-TRANS (GAIN K))))))))))
 
699
 
 
700
 
 
701
          (m-zero (n) (n)))
 
702
    :hints (("Goal" :do-not-induct t
 
703
             :use ((:instance mean-*
 
704
                              (p (gain k))
 
705
                              (q (m-* (m-* (v k)
 
706
                                           (m-trans (m-- (x k) (xhatmin k))))
 
707
                                      (m-trans (m-- (m-id (n))
 
708
                                                    (m-* (gain k) (h k)))))))
 
709
                   (:instance mean-*
 
710
                              (p (m-* (v k)
 
711
                                      (m-trans (m-- (x k) (xhatmin k)))))
 
712
                              (q (m-trans (m-- (m-id (n))
 
713
                                               (m-* (gain k) (h k))))))
 
714
                   (:instance mean-of-v*trans-of-x-xhatmin))
 
715
             :in-theory (disable mean-of-v*trans-of-x-xhatmin
 
716
                                 mean-+
 
717
                                 acl2::*-+-right
 
718
                                 acl2::*-+-left
 
719
                                 acl2::*---right
 
720
                                 acl2::*---left
 
721
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
722
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
723
                                 )))))
 
724
 
 
725
 
 
726
 (local
 
727
  (defthm lemma-3d
 
728
    (equal (m-mean (m-* (gain k)
 
729
                        (m-* (v k)
 
730
                             (m-* (m-trans (v k))
 
731
                                  (m-trans (gain k))))))
 
732
           (m-* (gain k)
 
733
                (m-* (r k)
 
734
                     (m-trans (gain k)))))
 
735
    :hints (("Goal"
 
736
             :use ((:instance mean-*
 
737
                              (p (gain k))
 
738
                              (q (m-* (m-* (v k)
 
739
                                           (m-trans (v k)))
 
740
                                      (m-trans (gain k)))))
 
741
                   (:instance mean-* 
 
742
                              (p (m-* (v k)
 
743
                                      (m-trans (v k))))
 
744
                              (q (m-trans (gain k))))
 
745
                   (:instance mean-delete
 
746
                              (p (gain k))))
 
747
             :in-theory (disable gain gain-recdef)))))
 
748
 
 
749
 
 
750
 
 
751
 
 
752
 (local
 
753
  (defthm lemma-3e
 
754
 
 
755
    (EQUAL
 
756
     (CAR
 
757
      (DIMENSIONS
 
758
       'ACL2::$ARG
 
759
       (ACL2::M-BINARY-*
 
760
        (GAIN K)
 
761
        (ACL2::M-BINARY-* (V K)
 
762
                          (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
763
                                            (ACL2::M-TRANS (GAIN K)))))))
 
764
     (CAR
 
765
      (DIMENSIONS
 
766
       'ACL2::$ARG
 
767
       (ACL2::M-BINARY-+
 
768
        (ACL2::M-UNARY--
 
769
         (ACL2::M-BINARY-*
 
770
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
771
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
772
          (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
773
                                              (ACL2::M-UNARY-- (XHATMIN K)))
 
774
                            (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
775
                                              (ACL2::M-TRANS (GAIN K))))))
 
776
        (ACL2::M-BINARY-+
 
777
         (ACL2::M-UNARY--
 
778
          (ACL2::M-BINARY-*
 
779
           (GAIN K)
 
780
           (ACL2::M-BINARY-*
 
781
            (V K)
 
782
            (ACL2::M-BINARY-*
 
783
             (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
784
                               (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
785
             (ACL2::M-BINARY-+
 
786
              (ACL2::M-1 (N))
 
787
              (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
788
                                                 (ACL2::M-TRANS (GAIN K)))))))))
 
789
         (ACL2::M-BINARY-*
 
790
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
791
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
792
          (ACL2::M-BINARY-*
 
793
           (ACL2::M-BINARY-+ (X K)
 
794
                             (ACL2::M-UNARY-- (XHATMIN K)))
 
795
           (ACL2::M-BINARY-*
 
796
            (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
797
                              (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
798
            (ACL2::M-BINARY-+
 
799
             (ACL2::M-1 (N))
 
800
             (ACL2::M-UNARY--
 
801
              (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
802
                                (ACL2::M-TRANS (GAIN K)))))))))))))
 
803
    :hints (("Goal"
 
804
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
805
                                 acl2::*-+-right
 
806
                                 acl2::*-+-left
 
807
                                 acl2::*---right
 
808
                                 acl2::*---left
 
809
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
810
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
811
 
 
812
 (local
 
813
  (defthm lemma-3f
 
814
 
 
815
    (EQUAL
 
816
     (CADR
 
817
      (DIMENSIONS
 
818
       'ACL2::$ARG
 
819
       (ACL2::M-BINARY-*
 
820
        (GAIN K)
 
821
        (ACL2::M-BINARY-* (V K)
 
822
                          (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
823
                                            (ACL2::M-TRANS (GAIN K)))))))
 
824
     (CADR
 
825
      (DIMENSIONS
 
826
       'ACL2::$ARG
 
827
       (ACL2::M-BINARY-+
 
828
        (ACL2::M-UNARY--
 
829
         (ACL2::M-BINARY-*
 
830
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
831
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
832
          (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
833
                                              (ACL2::M-UNARY-- (XHATMIN K)))
 
834
                            (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
835
                                              (ACL2::M-TRANS (GAIN K))))))
 
836
        (ACL2::M-BINARY-+
 
837
         (ACL2::M-UNARY--
 
838
          (ACL2::M-BINARY-*
 
839
           (GAIN K)
 
840
           (ACL2::M-BINARY-*
 
841
            (V K)
 
842
            (ACL2::M-BINARY-*
 
843
             (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
844
                               (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
845
             (ACL2::M-BINARY-+
 
846
              (ACL2::M-1 (N))
 
847
              (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
848
                                                 (ACL2::M-TRANS (GAIN K)))))))))
 
849
         (ACL2::M-BINARY-*
 
850
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
851
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
852
          (ACL2::M-BINARY-*
 
853
           (ACL2::M-BINARY-+ (X K)
 
854
                             (ACL2::M-UNARY-- (XHATMIN K)))
 
855
           (ACL2::M-BINARY-*
 
856
            (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
857
                              (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
858
            (ACL2::M-BINARY-+
 
859
             (ACL2::M-1 (N))
 
860
             (ACL2::M-UNARY--
 
861
              (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
862
                                (ACL2::M-TRANS (GAIN K)))))))))))))
 
863
    :hints (("Goal"
 
864
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
865
                                 acl2::*-+-right
 
866
                                 acl2::*-+-left
 
867
                                 acl2::*---right
 
868
                                 acl2::*---left
 
869
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
870
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
871
 
 
872
 (local
 
873
  (defthm lemma-3g
 
874
 
 
875
    (EQUAL
 
876
     (CAR
 
877
      (DIMENSIONS
 
878
       'ACL2::$ARG
 
879
       (ACL2::M-UNARY--
 
880
        (ACL2::M-BINARY-*
 
881
         (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
882
                           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
883
         (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
884
                                             (ACL2::M-UNARY-- (XHATMIN K)))
 
885
                           (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
886
                                             (ACL2::M-TRANS (GAIN K))))))))
 
887
     (CAR
 
888
      (DIMENSIONS
 
889
       'ACL2::$ARG
 
890
       (ACL2::M-BINARY-+
 
891
        (ACL2::M-UNARY--
 
892
         (ACL2::M-BINARY-*
 
893
          (GAIN K)
 
894
          (ACL2::M-BINARY-*
 
895
           (V K)
 
896
           (ACL2::M-BINARY-*
 
897
            (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
898
                              (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
899
            (ACL2::M-BINARY-+
 
900
             (ACL2::M-1 (N))
 
901
             (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
902
                                                (ACL2::M-TRANS (GAIN K)))))))))
 
903
        (ACL2::M-BINARY-*
 
904
         (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
905
                           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
906
         (ACL2::M-BINARY-*
 
907
          (ACL2::M-BINARY-+ (X K)
 
908
                            (ACL2::M-UNARY-- (XHATMIN K)))
 
909
          (ACL2::M-BINARY-*
 
910
           (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
911
                             (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
912
           (ACL2::M-BINARY-+
 
913
            (ACL2::M-1 (N))
 
914
            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
915
                                               (ACL2::M-TRANS (GAIN K))))))))))))
 
916
 
 
917
    :hints (("Goal"
 
918
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
919
                                 acl2::*-+-right
 
920
                                 acl2::*-+-left
 
921
                                 acl2::*---right
 
922
                                 acl2::*---left
 
923
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
924
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
925
 
 
926
 (local
 
927
  (defthm lemma-3h
 
928
 
 
929
    (EQUAL
 
930
     (CADR
 
931
      (DIMENSIONS
 
932
       'ACL2::$ARG
 
933
       (ACL2::M-UNARY--
 
934
        (ACL2::M-BINARY-*
 
935
         (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
936
                           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
937
         (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
938
                                             (ACL2::M-UNARY-- (XHATMIN K)))
 
939
                           (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
940
                                             (ACL2::M-TRANS (GAIN K))))))))
 
941
     (CADR
 
942
      (DIMENSIONS
 
943
       'ACL2::$ARG
 
944
       (ACL2::M-BINARY-+
 
945
        (ACL2::M-UNARY--
 
946
         (ACL2::M-BINARY-*
 
947
          (GAIN K)
 
948
          (ACL2::M-BINARY-*
 
949
           (V K)
 
950
           (ACL2::M-BINARY-*
 
951
            (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
952
                              (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
953
            (ACL2::M-BINARY-+
 
954
             (ACL2::M-1 (N))
 
955
             (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
956
                                                (ACL2::M-TRANS (GAIN K)))))))))
 
957
        (ACL2::M-BINARY-*
 
958
         (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
959
                           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
960
         (ACL2::M-BINARY-*
 
961
          (ACL2::M-BINARY-+ (X K)
 
962
                            (ACL2::M-UNARY-- (XHATMIN K)))
 
963
          (ACL2::M-BINARY-*
 
964
           (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
965
                             (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
966
           (ACL2::M-BINARY-+
 
967
            (ACL2::M-1 (N))
 
968
            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
969
                                               (ACL2::M-TRANS (GAIN K))))))))))))
 
970
 
 
971
    :hints (("Goal"
 
972
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
973
                                 acl2::*-+-right
 
974
                                 acl2::*-+-left
 
975
                                 acl2::*---right
 
976
                                 acl2::*---left
 
977
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
978
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
979
 
 
980
 (local
 
981
  (defthm lemma-3i
 
982
 
 
983
    (EQUAL
 
984
     (CAR
 
985
      (DIMENSIONS
 
986
       'ACL2::$ARG
 
987
       (ACL2::M-UNARY--
 
988
        (ACL2::M-BINARY-*
 
989
         (GAIN K)
 
990
         (ACL2::M-BINARY-*
 
991
          (V K)
 
992
          (ACL2::M-BINARY-*
 
993
           (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
994
                             (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
995
           (ACL2::M-BINARY-+
 
996
            (ACL2::M-1 (N))
 
997
            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
998
                                               (ACL2::M-TRANS (GAIN K)))))))))))
 
999
     (CAR
 
1000
      (DIMENSIONS
 
1001
       'ACL2::$ARG
 
1002
       (ACL2::M-BINARY-*
 
1003
        (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1004
                          (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1005
        (ACL2::M-BINARY-*
 
1006
         (ACL2::M-BINARY-+ (X K)
 
1007
                           (ACL2::M-UNARY-- (XHATMIN K)))
 
1008
         (ACL2::M-BINARY-*
 
1009
          (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1010
                            (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
1011
          (ACL2::M-BINARY-+
 
1012
           (ACL2::M-1 (N))
 
1013
           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1014
                                              (ACL2::M-TRANS (GAIN K)))))))))))
 
1015
 
 
1016
    :hints (("Goal"
 
1017
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
1018
                                 acl2::*-+-right
 
1019
                                 acl2::*-+-left
 
1020
                                 acl2::*---right
 
1021
                                 acl2::*---left
 
1022
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1023
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
1024
 
 
1025
 (local
 
1026
  (defthm lemma-3j
 
1027
 
 
1028
    (EQUAL
 
1029
     (CADR
 
1030
      (DIMENSIONS
 
1031
       'ACL2::$ARG
 
1032
       (ACL2::M-UNARY--
 
1033
        (ACL2::M-BINARY-*
 
1034
         (GAIN K)
 
1035
         (ACL2::M-BINARY-*
 
1036
          (V K)
 
1037
          (ACL2::M-BINARY-*
 
1038
           (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1039
                             (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
1040
           (ACL2::M-BINARY-+
 
1041
            (ACL2::M-1 (N))
 
1042
            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1043
                                               (ACL2::M-TRANS (GAIN K)))))))))))
 
1044
     (CADR
 
1045
      (DIMENSIONS
 
1046
       'ACL2::$ARG
 
1047
       (ACL2::M-BINARY-*
 
1048
        (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1049
                          (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1050
        (ACL2::M-BINARY-*
 
1051
         (ACL2::M-BINARY-+ (X K)
 
1052
                           (ACL2::M-UNARY-- (XHATMIN K)))
 
1053
         (ACL2::M-BINARY-*
 
1054
          (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1055
                            (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
1056
          (ACL2::M-BINARY-+
 
1057
           (ACL2::M-1 (N))
 
1058
           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1059
                                              (ACL2::M-TRANS (GAIN K)))))))))))
 
1060
 
 
1061
    :hints (("Goal"
 
1062
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
1063
                                 acl2::*-+-right
 
1064
                                 acl2::*-+-left
 
1065
                                 acl2::*---right
 
1066
                                 acl2::*---left
 
1067
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1068
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
1069
 
 
1070
 
 
1071
 
 
1072
 (local
 
1073
  (defthm lemma-3k
 
1074
 
 
1075
    (ACL2::M-=
 
1076
     (ACL2::M-BINARY-+
 
1077
      (ACL2::M-0 (N) (N))
 
1078
      (ACL2::M-BINARY-+
 
1079
       (ACL2::M-0 (N) (N))
 
1080
       (ACL2::M-BINARY-+
 
1081
        (ACL2::M-BINARY-* (GAIN K)
 
1082
                          (ACL2::M-BINARY-* (R K)
 
1083
                                            (ACL2::M-TRANS (GAIN K))))
 
1084
        (ACL2::M-BINARY-*
 
1085
         (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1086
                           (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1087
         (ACL2::M-BINARY-*
 
1088
          (M-MEAN
 
1089
           (ACL2::M-BINARY-*
 
1090
            (ACL2::M-BINARY-+ (X K)
 
1091
                              (ACL2::M-UNARY-- (XHATMIN K)))
 
1092
            (ACL2::M-TRANS (ACL2::M-BINARY-+ (X K)
 
1093
                                             (ACL2::M-UNARY-- (XHATMIN K))))))
 
1094
          (ACL2::M-TRANS
 
1095
           (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1096
                             (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K)
 
1097
                                                                (H K))))))))))
 
1098
     (ACL2::M-BINARY-+
 
1099
      (ACL2::M-BINARY-* (GAIN K)
 
1100
                        (ACL2::M-BINARY-* (R K)
 
1101
                                          (ACL2::M-TRANS (GAIN K))))
 
1102
      (ACL2::M-BINARY-*
 
1103
       (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1104
                         (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1105
       (ACL2::M-BINARY-*
 
1106
        (M-MEAN
 
1107
         (ACL2::M-BINARY-*
 
1108
          (ACL2::M-BINARY-+ (X K)
 
1109
                            (ACL2::M-UNARY-- (XHATMIN K)))
 
1110
          (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1111
                            (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))))
 
1112
        (ACL2::M-BINARY-+
 
1113
         (ACL2::M-1 (N))
 
1114
         (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1115
                                            (ACL2::M-TRANS (GAIN K)))))))))
 
1116
 
 
1117
    :hints (("Goal"
 
1118
             :in-theory (disable gain gain-recdef x xhat xhatmin
 
1119
                                 acl2::*-+-right
 
1120
                                 acl2::*-+-left
 
1121
                                 acl2::*---right
 
1122
                                 acl2::*---left
 
1123
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1124
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
1125
 
 
1126
 
 
1127
 (local
 
1128
  (DEFTHM
 
1129
    lemma-3l
 
1130
    (ACL2::M-=
 
1131
     (M-MEAN
 
1132
      (ACL2::M-BINARY-+
 
1133
       (ACL2::M-BINARY-*
 
1134
        (GAIN K)
 
1135
        (ACL2::M-BINARY-* (V K)
 
1136
                          (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
1137
                                            (ACL2::M-TRANS (GAIN K)))))
 
1138
       (ACL2::M-BINARY-+
 
1139
        (ACL2::M-UNARY--
 
1140
         (ACL2::M-BINARY-*
 
1141
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1142
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1143
          (ACL2::M-BINARY-* (ACL2::M-BINARY-+ (X K)
 
1144
                                              (ACL2::M-UNARY-- (XHATMIN K)))
 
1145
                            (ACL2::M-BINARY-* (ACL2::M-TRANS (V K))
 
1146
                                              (ACL2::M-TRANS (GAIN K))))))
 
1147
        (ACL2::M-BINARY-+
 
1148
         (ACL2::M-UNARY--
 
1149
          (ACL2::M-BINARY-*
 
1150
           (GAIN K)
 
1151
           (ACL2::M-BINARY-*
 
1152
            (V K)
 
1153
            (ACL2::M-BINARY-*
 
1154
             (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1155
                               (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
1156
             (ACL2::M-BINARY-+
 
1157
              (ACL2::M-1 (N))
 
1158
              (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1159
                                                 (ACL2::M-TRANS (GAIN K)))))))))
 
1160
         (ACL2::M-BINARY-*
 
1161
          (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1162
                            (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1163
          (ACL2::M-BINARY-*
 
1164
           (ACL2::M-BINARY-+ (X K)
 
1165
                             (ACL2::M-UNARY-- (XHATMIN K)))
 
1166
           (ACL2::M-BINARY-*
 
1167
            (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1168
                              (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))
 
1169
            (ACL2::M-BINARY-+
 
1170
             (ACL2::M-1 (N))
 
1171
             (ACL2::M-UNARY--
 
1172
              (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1173
                                (ACL2::M-TRANS (GAIN K))))))))))))
 
1174
     (ACL2::M-BINARY-+
 
1175
      (ACL2::M-BINARY-* (GAIN K)
 
1176
                        (ACL2::M-BINARY-* (R K)
 
1177
                                          (ACL2::M-TRANS (GAIN K))))
 
1178
      (ACL2::M-BINARY-*
 
1179
       (ACL2::M-BINARY-+ (ACL2::M-1 (N))
 
1180
                         (ACL2::M-UNARY-- (ACL2::M-BINARY-* (GAIN K) (H K))))
 
1181
       (ACL2::M-BINARY-*
 
1182
        (M-MEAN
 
1183
         (ACL2::M-BINARY-*
 
1184
          (ACL2::M-BINARY-+ (X K)
 
1185
                            (ACL2::M-UNARY-- (XHATMIN K)))
 
1186
          (ACL2::M-BINARY-+ (ACL2::M-TRANS (X K))
 
1187
                            (ACL2::M-UNARY-- (ACL2::M-TRANS (XHATMIN K))))))
 
1188
        (ACL2::M-BINARY-+
 
1189
         (ACL2::M-1 (N))
 
1190
         (ACL2::M-UNARY-- (ACL2::M-BINARY-* (ACL2::M-TRANS (H K))
 
1191
                                            (ACL2::M-TRANS (GAIN K)))))))))
 
1192
    :INSTRUCTIONS
 
1193
    ((:DV 1)
 
1194
     (:REWRITE MEAN-+)
 
1195
     (:CHANGE-GOAL NIL T)
 
1196
     (:USE LEMMA-3E)
 
1197
     (:USE LEMMA-3F)
 
1198
     (:DV 1)
 
1199
     (:REWRITE LEMMA-3D)
 
1200
     :NX (:REWRITE MEAN-+)
 
1201
     (:CHANGE-GOAL NIL T)
 
1202
     (:USE LEMMA-3G)
 
1203
     (:USE LEMMA-3H)
 
1204
     (:DV 1)
 
1205
     (:REWRITE LEMMA-3B)
 
1206
     :NX (:REWRITE MEAN-+)
 
1207
     (:CHANGE-GOAL NIL T)
 
1208
     (:USE LEMMA-3I)
 
1209
     (:USE LEMMA-3J)
 
1210
     (:DV 1)
 
1211
     (:REWRITE LEMMA-3C)
 
1212
     :NX (:REWRITE LEMMA-3A)
 
1213
     :TOP (:DV 1)
 
1214
     (:REWRITE ACL2::COMMUTATIVITY-2-OF-M-+)
 
1215
     (:DIVE 2) ; changed by Matt K. for v2-9 due to proof-checker DV fix for binops
 
1216
     (:REWRITE ACL2::COMMUTATIVITY-2-OF-M-+)
 
1217
     :TOP (:USE LEMMA-3K))))
 
1218
 
 
1219
 (local
 
1220
  (defthm lemma-3
 
1221
    (m-= (m-mean (m-* (m-- (x k) (xhat k))
 
1222
                      (m-trans (m-- (x k) (xhat k)))))
 
1223
         (m-+ (m-* (m-- (m-id (n))
 
1224
                        (m-* (gain k) (h k)))
 
1225
                   (m-* (m-mean (m-* (m-- (x k) (xhatmin k))
 
1226
                                     (m-trans (m-- (x k) (xhatmin k)))))
 
1227
                        (m-trans (m-- (m-id (n))
 
1228
                                      (m-* (gain k) (h k))))))
 
1229
              (m-* (gain k)
 
1230
                   (m-* (r k)
 
1231
                        (m-trans (gain k))))))
 
1232
    :hints (("Goal"
 
1233
             :use ((:instance lemma-2))
 
1234
             :in-theory (disable x xhat xhatmin 
 
1235
                                 gain-recdef pplus-recdef xhatmin-recdef
 
1236
                                 acl2::*-+-right
 
1237
                                 acl2::*-+-left
 
1238
                                 acl2::*---right
 
1239
                                 acl2::*---left
 
1240
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1241
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1242
                                 ))
 
1243
            ("Goal'4'"
 
1244
             :by (:instance lemma-3l)))
 
1245
    :rule-classes nil))
 
1246
 
 
1247
 (local
 
1248
  (defthm lemma-4
 
1249
    (m-= (m-* (m-- (m-id (n))
 
1250
                   (m-* (gain k) (h k)))
 
1251
              (m-* (pminus k)
 
1252
                   (m-trans (m-- (m-id (n))
 
1253
                                 (m-* (gain k) (h k))))))
 
1254
         (m-+ (pminus k)
 
1255
              (m-+ (m-unary-- (m-* (gain k) (m-* (h k) (pminus k))))
 
1256
                   (m-+ (m-unary-- (m-* (pminus k) 
 
1257
                                        (m-* (m-trans (h k))
 
1258
                                             (m-trans (gain k)))))
 
1259
                        (m-* (gain k)
 
1260
                             (m-* (h k)
 
1261
                                  (m-* (pminus k)
 
1262
                                       (m-* (m-trans (h k))
 
1263
                                            (m-trans (gain k))))))))))
 
1264
    :hints (("Goal" :do-not-induct t
 
1265
             :in-theory (disable gain gain-recdef
 
1266
                                 pminus pminus-recdef)))
 
1267
    :rule-classes nil))
 
1268
                                 
 
1269
 (local
 
1270
  (defthm lemma-5
 
1271
    (m-= (m-+ (m-* (m-- (m-id (n))
 
1272
                        (m-* (gain k) (h k)))
 
1273
                   (m-* (pminus k)
 
1274
                        (m-trans (m-- (m-id (n))
 
1275
                                      (m-* (gain k) (h k))))))
 
1276
              (m-* (gain k)
 
1277
                   (m-* (r k)
 
1278
                        (m-trans (gain k)))))
 
1279
         (m-+ (pminus k)
 
1280
              (m-+ (m-unary-- (m-* (gain k) (m-* (h k) (pminus k))))
 
1281
                   (m-+ (m-unary-- (m-* (pminus k) 
 
1282
                                        (m-* (m-trans (h k))
 
1283
                                             (m-trans (gain k)))))
 
1284
                        (m-+ (m-* (gain k)
 
1285
                                  (m-* (h k)
 
1286
                                       (m-* (pminus k)
 
1287
                                            (m-* (m-trans (h k))
 
1288
                                                 (m-trans (gain k))))))
 
1289
                             (m-* (gain k)
 
1290
                                  (m-* (r k)
 
1291
                                       (m-trans (gain k)))))))))
 
1292
    :hints (("Goal" :do-not-induct t
 
1293
             :use ((:instance lemma-4))
 
1294
             :in-theory (disable gain gain-recdef
 
1295
                                 pminus pminus-recdef)))
 
1296
    :rule-classes nil))
 
1297
 
 
1298
 (local
 
1299
  (defthm lemma-6
 
1300
    (m-= (m-+ (m-* (gain k)
 
1301
                   (m-* (h k)
 
1302
                        (m-* (pminus k)
 
1303
                             (m-* (m-trans (h k))
 
1304
                                  (m-trans (gain k))))))
 
1305
              (m-* (gain k)
 
1306
                   (m-* (r k)
 
1307
                        (m-trans (gain k)))))
 
1308
         (m-* (gain k)
 
1309
              (m-* (m-+ (m-* (h k) (m-* (pminus k) (m-trans (h k))))
 
1310
                        (r k))
 
1311
                   (m-trans (gain k)))))
 
1312
    :hints (("Goal"
 
1313
             :in-theory (disable gain gain-recdef pminus pminus-recdef)))
 
1314
    :rule-classes nil))
 
1315
 
 
1316
 (local
 
1317
  (defthm lemma-7a
 
1318
    (implies (and (not (m-singular x))
 
1319
                  (m-matrixp (l x) (c x) x)
 
1320
                  (m-matrixp (l y) (c y) y)
 
1321
                  (equal (c v) (l w))
 
1322
                  (equal (c w) (l x))
 
1323
                  (equal (c x) (l y)))
 
1324
             (m-= (m-* v
 
1325
                       (m-* w
 
1326
                            (m-* (m-inv x)
 
1327
                                 (m-* x y))))
 
1328
                  (m-* v (m-* w y))))
 
1329
    :hints (("Goal"
 
1330
             :use ((:instance acl2::assoc-*
 
1331
                              (acl2::p (m-inv x))
 
1332
                              (acl2::q x)
 
1333
                              (acl2::r y))
 
1334
                   (:instance acl2::inv-*-x
 
1335
                              (acl2::p x)))
 
1336
             :in-theory (disable acl2::assoc-* 
 
1337
                                 acl2::inv-*-x))
 
1338
            ("Goal'4'"
 
1339
             :in-theory (enable acl2::assoc-*)))))
 
1340
                              
 
1341
 (local
 
1342
  (defthm lemma-7
 
1343
    (implies (and (integerp k) (<= 0 k))
 
1344
             (m-= (m-+ (m-* (gain k)
 
1345
                            (m-* (h k)
 
1346
                                 (m-* (pminus k)
 
1347
                                      (m-* (m-trans (h k))
 
1348
                                           (m-trans (gain k))))))
 
1349
                       (m-* (gain k)
 
1350
                            (m-* (r k)
 
1351
                                 (m-trans (gain k)))))
 
1352
                  (m-* (pminus k)
 
1353
                       (m-* (m-trans (h k)) (m-trans (gain k))))))
 
1354
    :hints (("Goal"
 
1355
             :use ((:instance lemma-6))
 
1356
             :in-theory (disable gain pminus pminus-recdef
 
1357
                                 acl2::assoc-*
 
1358
                                 acl2::comm-+
 
1359
                                 ACL2::*-+-RIGHT
 
1360
                                 ACL2::*---RIGHT
 
1361
                                 ACL2::*-+-left
 
1362
                                 ACL2::*---left
 
1363
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1364
                                 ACL2::left-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1365
                                 acl2::COMMUTATIVITY-2-OF-M-+
 
1366
                                 ))
 
1367
            ("Goal'''"
 
1368
             :use (:theorem 
 
1369
                   (implies (and (integerp k) (<= 0 k))
 
1370
                            (m-= (m-* (gain k)
 
1371
                                      (m-* (m-+ (m-* (h k)
 
1372
                                                     (m-* (pminus k) (m-trans (h k))))
 
1373
                                                (r k))
 
1374
                                           (m-trans (gain k))))
 
1375
                                 (m-* (pminus k)
 
1376
                                      (m-* (m-trans (h k))
 
1377
                                           (m-trans (gain k))))))))
 
1378
            ("Subgoal 1"
 
1379
             :in-theory (disable gain pminus pminus-recdef
 
1380
                                        ;acl2::comm-+
 
1381
                                 ACL2::*-+-RIGHT
 
1382
                                 ACL2::*---RIGHT
 
1383
                                 ACL2::*-+-left
 
1384
                                 ACL2::*---left
 
1385
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1386
                                 ACL2::left-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1387
                                 acl2::COMMUTATIVITY-2-OF-M-+
 
1388
                                 ))
 
1389
            )
 
1390
    :rule-classes nil))
 
1391
 
 
1392
 (local
 
1393
  (defthm lemma-8
 
1394
    (implies (and (integerp k) (<= 0 k))
 
1395
             (m-= (m-+ (m-* (m-- (m-id (n))
 
1396
                                 (m-* (gain k) (h k)))
 
1397
                            (m-* (pminus k)
 
1398
                                 (m-trans (m-- (m-id (n))
 
1399
                                               (m-* (gain k) (h k))))))
 
1400
                       (m-* (gain k)
 
1401
                            (m-* (r k)
 
1402
                                 (m-trans (gain k)))))
 
1403
                  (m-- (pminus k)
 
1404
                       (m-* (gain k) (m-* (h k) (pminus k))))))
 
1405
    :hints (("Goal" :do-not-induct t
 
1406
             :use ((:instance lemma-5)
 
1407
                   (:instance lemma-6)
 
1408
                   (:instance lemma-7))
 
1409
             :in-theory (disable gain gain-recdef
 
1410
                                 pminus pminus-recdef
 
1411
                                 acl2::assoc-*
 
1412
                                 acl2::comm-+
 
1413
                                 ACL2::*-+-RIGHT
 
1414
                                 ACL2::*---RIGHT
 
1415
                                 ACL2::*-+-left
 
1416
                                 ACL2::*---left
 
1417
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1418
                                 ACL2::left-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1419
                                 acl2::COMMUTATIVITY-2-OF-M-+
 
1420
                                 acl2::trans-*
 
1421
                                 acl2::trans-+
 
1422
                                 acl2::trans---))
 
1423
            ("Goal'7'"
 
1424
             :by (:theorem
 
1425
                  (m-= (m-+ (pminus k)
 
1426
                            (m-+ (m-unary-- (m-* (gain k) (m-* (h k) (pminus k))))
 
1427
                                 (m-zero (n) (n))))
 
1428
                       (m-- (pminus k)
 
1429
                            (m-* (gain k)
 
1430
                                 (m-* (h k) (pminus k))))))
 
1431
             :in-theory (disable pminus pminus-recdef gain gain-recdef)))
 
1432
    :rule-classes nil))
 
1433
 
 
1434
 (local
 
1435
  (defthm lemma-9-for-lemma-10
 
1436
    (implies (and (integerp k) (<= 0 k))
 
1437
             (m-= (m-+ (m-* (m-- (m-id (n))
 
1438
                                 (m-* (gain k) (h k)))
 
1439
                            (m-* (pminus k)
 
1440
                                 (m-trans (m-- (m-id (n))
 
1441
                                               (m-* (gain k) (h k))))))
 
1442
                       (m-* (gain k)
 
1443
                            (m-* (r k)
 
1444
                                 (m-trans (gain k)))))
 
1445
                  (m-* (m-- (m-id (n))
 
1446
                            (m-* (gain k) (h k)))
 
1447
                       (pminus k))))
 
1448
    :hints (("Goal" :do-not-induct t
 
1449
             :use ((:instance lemma-8))
 
1450
             :in-theory (disable pminus pminus-recdef gain gain-recdef)))
 
1451
    :rule-classes nil))
 
1452
                 
 
1453
 (local
 
1454
  (defthm lemma-10
 
1455
    (implies (and (integerp k) (<= 0 k))
 
1456
             (m-= (m-+ (m-* (m-- (m-id (n))
 
1457
                                 (m-* (gain k) (h k)))
 
1458
                            (m-* (pminus k)
 
1459
                                 (m-trans (m-- (m-id (n))
 
1460
                                               (m-* (gain k) (h k))))))
 
1461
                       (m-* (gain k)
 
1462
                            (m-* (r k)
 
1463
                                 (m-trans (gain k)))))
 
1464
                  (pplus k)))
 
1465
    :hints (("Goal" :do-not-induct t
 
1466
             :use ((:instance lemma-9-for-lemma-10))
 
1467
             :in-theory (disable pminus pminus-recdef gain gain-recdef)))
 
1468
    :rule-classes nil))
 
1469
 
 
1470
 (local
 
1471
  (defthm pplus-as-mean-case-0
 
1472
    (implies (equal k 0)
 
1473
             (m-= (pplus k)
 
1474
                  (m-mean (m-* (m-- (x k) (xhat k))
 
1475
                               (m-trans (m-- (x k) (xhat k)))))))
 
1476
    :hints (("Goal" :do-not-induct t
 
1477
             :use ((:instance lemma-3)
 
1478
                   (:instance lemma-10)
 
1479
                   (:instance pminus-as-mean-case-0))
 
1480
             :in-theory (disable pminus pminus-recdef gain gain-recdef)))
 
1481
    :rule-classes nil))
 
1482
 
 
1483
 (local
 
1484
  (defthm pplus-as-mean-almost
 
1485
    (implies (and (integerp k)
 
1486
                  (< 0 k)
 
1487
                  (m-= (pplus (1- k))
 
1488
                       (m-mean (m-* (m-- (x (1- k))
 
1489
                                         (xhat (1- k)))
 
1490
                                    (m-trans (m-- (x (1- k))
 
1491
                                                  (xhat (1- k))))))))
 
1492
             (m-= (pplus k)
 
1493
                  (m-mean (m-* (m-- (x k) (xhat k))
 
1494
                               (m-trans (m-- (x k) (xhat k)))))))
 
1495
    :hints (("Goal" :do-not-induct t
 
1496
             :use ((:instance lemma-3)
 
1497
                   (:instance lemma-10)
 
1498
                   (:instance pminus-as-mean-almost))
 
1499
             :in-theory (disable gain gain-recdef
 
1500
                                 pminus pminus-recdef
 
1501
                                 acl2::assoc-*
 
1502
                                 acl2::comm-+
 
1503
                                 ACL2::*-+-RIGHT
 
1504
                                 ACL2::*---RIGHT
 
1505
                                 ACL2::*-+-left
 
1506
                                 ACL2::*---left
 
1507
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1508
                                 ACL2::left-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1509
                                 acl2::COMMUTATIVITY-2-OF-M-+
 
1510
                                 acl2::trans-*
 
1511
                                 acl2::trans-+
 
1512
                                 acl2::trans---)))
 
1513
    :rule-classes nil)) 
 
1514
 
 
1515
 (local
 
1516
  (defun natural-induction (n)
 
1517
    (if (zp n)
 
1518
        0
 
1519
      (1+ (natural-induction (1- n))))))
 
1520
 
 
1521
 (defthm pplus-as-mean
 
1522
   (implies (and (integerp k)
 
1523
                 (<= 0 k))
 
1524
            (m-= (pplus k)
 
1525
                 (m-mean (m-* (m-- (x k) (xhat k))
 
1526
                              (m-trans (m-- (x k) (xhat k)))))))
 
1527
   :hints (("Goal"
 
1528
            :induct (natural-induction k))
 
1529
           ("Subgoal *1/2"
 
1530
            :use ((:instance pplus-as-mean-almost)))
 
1531
           ("Subgoal *1/1"
 
1532
            :use ((:instance pplus-as-mean-case-0)))
 
1533
           ))
 
1534
    
 
1535
 )
 
1536
   
 
1537
(defthm pminus-as-mean
 
1538
  (implies (and (integerp k) (<= 0 k))
 
1539
           (m-= (pminus k)
 
1540
                (m-mean (m-* (m-- (x k) (xhatmin k))
 
1541
                             (m-trans (m-- (x k) (xhatmin k)))))))
 
1542
  :hints (("Goal" :do-not-induct t
 
1543
           :use ((:instance pminus-as-mean-almost)
 
1544
                 (:instance pplus-as-mean (k (1- k))))
 
1545
           :in-theory (disable pminus-as-mean-almost pplus-as-mean
 
1546
                               x xhat xhatmin 
 
1547
                               gain-recdef pplus-recdef xhatmin-recdef
 
1548
                               (pminus) (x) (xhatmin)))))
 
1549
 
 
1550
(encapsulate
 
1551
 ()
 
1552
 
 
1553
 (local
 
1554
  (encapsulate
 
1555
   ()
 
1556
 
 
1557
   (local
 
1558
    (defthm lemma-0-1
 
1559
      (implies (and (m-matrixp (l y) (c y) y)
 
1560
                    (m-matrixp (l z) (c z) z)
 
1561
                    (equal (c x) (l y))
 
1562
                    (equal (c y) (l z)))
 
1563
               (equal (m-* x (m-mean (m-* y z)))
 
1564
                      (m-mean (m-* (m-* x y) z))))
 
1565
      :hints (("Goal"
 
1566
               :use ((:instance mean-*
 
1567
                                (p x)
 
1568
                                (q (m-* y z)))
 
1569
                     (:instance mean-delete
 
1570
                                (p x)))))))
 
1571
 
 
1572
   (local
 
1573
    (defthm lemma-0-2
 
1574
      (implies (and (m-matrixp (l x) (c x) x)
 
1575
                    (m-matrixp (l y) (c y) y)
 
1576
                    (equal (c x) (l y))
 
1577
                    (equal (c y) (l z)))
 
1578
               (equal (m-* (m-mean (m-* x y)) z)
 
1579
                      (m-mean (m-* x (m-* y z)))))
 
1580
      :hints (("Goal"
 
1581
               :use ((:instance mean-*
 
1582
                                (p (m-* x y))
 
1583
                                (q z))
 
1584
                     (:instance mean-delete
 
1585
                                (p z)))))))
 
1586
 
 
1587
   (defthm lemma-0
 
1588
     (implies (and (integerp k) (<= 0 k))
 
1589
              (m-= (m-* (pminus k) (m-trans (h k)))
 
1590
                   (m-mean (m-* (m-- (x k) (xhatmin k))
 
1591
                                (m-trans (m-- (m-* (h k) (x k))
 
1592
                                              (m-* (h k) (xhatmin k))))))))
 
1593
     :hints (("Goal" :do-not-induct t
 
1594
              :use ((:instance pminus-as-mean))
 
1595
              :in-theory (disable pplus-as-mean pminus-as-mean))))
 
1596
 
 
1597
 
 
1598
   (defthm lemma-1
 
1599
     (implies (and (integerp k) (<= 0 k))
 
1600
              (m-= (m-* (h k) (m-* (pminus k) (m-trans (h k))))
 
1601
                   (m-mean (m-* (m-- (m-* (h k) (x k))
 
1602
                                     (m-* (h k) (xhatmin k)))
 
1603
                                (m-trans (m-- (m-* (h k) (x k))
 
1604
                                              (m-* (h k) (xhatmin k)))))))))
 
1605
   ))
 
1606
 
 
1607
 (local
 
1608
  (encapsulate
 
1609
   ()
 
1610
 
 
1611
   (local
 
1612
    (defthm lemma-2-1
 
1613
      (equal (l (m-* (v k) (m-trans (v k))))
 
1614
             (l (m-* (m-- (m-* (h k) (x k))
 
1615
                          (m-* (h k) (xhatmin k)))
 
1616
                     (m-trans (m-- (m-* (h k) (x k))
 
1617
                                   (m-* (h k) (xhatmin k)))))))))
 
1618
 
 
1619
   (local
 
1620
    (defthm lemma-2-2
 
1621
      (equal (c (m-* (v k) (m-trans (v k))))
 
1622
             (c (m-* (m-- (m-* (h k) (x k))
 
1623
                          (m-* (h k) (xhatmin k)))
 
1624
                     (m-trans (m-- (m-* (h k) (x k))
 
1625
                                   (m-* (h k) (xhatmin k)))))))))
 
1626
 
 
1627
   (defthm lemma-2
 
1628
     (implies (and (integerp k) (<= 0 k))
 
1629
              (m-= (m-+ (m-* (h k)
 
1630
                             (m-* (pminus k) (m-trans (h k))))
 
1631
                        (m-mean (m-* (v k) (m-trans (v k)))))
 
1632
                   (m-mean (m-+ (m-* (m-- (m-* (h k) (x k))
 
1633
                                          (m-* (h k) (xhatmin k)))
 
1634
                                     (m-trans (m-- (m-* (h k) (x k))
 
1635
                                                   (m-* (h k) (xhatmin k)))))
 
1636
                                (m-* (v k) (m-trans (v k)))))))
 
1637
     :hints (("Goal" :do-not-induct t
 
1638
              :in-theory '(lemma-1 mean-+ lemma-2-1 lemma-2-2 
 
1639
                                   acl2::m-=-implies-equal-m-+-1))))
 
1640
 
 
1641
   ))
 
1642
 
 
1643
 (local
 
1644
  (defthm lemma-3
 
1645
    (implies (and (integerp k) (<= 0 k))
 
1646
             (m-= (m-+ (m-* (h k)
 
1647
                            (m-* (pminus k)
 
1648
                                 (m-trans (h k))))
 
1649
                       (r k))
 
1650
                  (m-mean (m-+ (m-* (m-- (m-* (h k) (x k))
 
1651
                                         (m-* (h k) (xhatmin k)))
 
1652
                                    (m-trans (m-- (m-* (h k) (x k))
 
1653
                                                  (m-* (h k) (xhatmin k)))))
 
1654
                               (m-* (v k) (m-trans (v k)))))))
 
1655
    :hints (("Goal"
 
1656
             :use ((:instance mean-of-v-vtrans)
 
1657
                   (:instance lemma-2))
 
1658
             :in-theory '(acl2::m-=-implies-equal-m-+-2)))))
 
1659
 
 
1660
 (local
 
1661
  (encapsulate
 
1662
   nil
 
1663
 
 
1664
   (local
 
1665
    (defthm lemma-4-1
 
1666
      (implies (and (m-matrixp (l a) (c a) a)
 
1667
                    (m-matrixp (l b) (c b) b)
 
1668
                    (equal (l a) (l b))
 
1669
                    (equal (c a) (c b)))
 
1670
               (m-= (m-mean (m-* (m-+ a b) (m-trans (m-+ a b))))
 
1671
                    (m-+ (m-mean (m-* a (m-trans a)))
 
1672
                         (m-+ (m-mean (m-* a (m-trans b)))
 
1673
                              (m-+ (m-mean (m-* b (m-trans a)))
 
1674
                                   (m-mean (m-* b (m-trans b))))))))))
 
1675
 
 
1676
   (local
 
1677
    (defthm lemma-4-2
 
1678
      (m-= (m-mean (m-* (m-- (m-* (h k) (x k))
 
1679
                             (m-* (h k) (xhatmin k)))
 
1680
                        (m-trans (v k))))
 
1681
           (m-zero (m) (m)))
 
1682
      :hints (("Goal" :do-not-induct t
 
1683
               :use ((:instance mean-of-x-xhatmin*vtrans)
 
1684
                     (:instance acl2::x-*-zero
 
1685
                                (acl2::p (h k))
 
1686
                                (acl2::m (n))
 
1687
                                (acl2::n (m)))
 
1688
                     (:instance acl2::*-+-right
 
1689
                                (acl2::p (h k))
 
1690
                                (acl2::q (m-* (x k) (m-trans (v k))))
 
1691
                                (acl2::r (m-* (m-unary-- (xhatmin k)) 
 
1692
                                              (m-trans (v k)))))
 
1693
                     (:instance mean-*
 
1694
                                (p (h k))
 
1695
                                (q (m-* (m-- (x k) (xhatmin k))
 
1696
                                        (m-trans (v k)))))
 
1697
                     (:instance mean-delete
 
1698
                                (p (h k))))
 
1699
               :in-theory (disable mean-of-x-xhatmin*vtrans
 
1700
                                   acl2::x-*-zero
 
1701
                                   acl2::*-+-right)))))
 
1702
 
 
1703
   (local
 
1704
    (defthm lemma-4-3
 
1705
      (m-= (m-mean (m-* (v k)
 
1706
                        (m-trans (m-- (m-* (h k) (x k))
 
1707
                                      (m-* (h k) (xhatmin k))))))
 
1708
           (m-zero (m) (m)))
 
1709
      :hints (("Goal" :do-not-induct t
 
1710
               :use ((:instance mean-of-v*trans-of-x-xhatmin)
 
1711
                     (:instance acl2::zero-*-x
 
1712
                                (acl2::p (m-trans (h k)))
 
1713
                                (acl2::m (m))
 
1714
                                (acl2::n (n)))
 
1715
                     (:instance mean-*
 
1716
                                (p (m-* (v k)
 
1717
                                        (m-trans (m-- (x k) (xhatmin k)))))
 
1718
                                (q (m-trans (h k))))
 
1719
                     (:instance mean-delete
 
1720
                                (p (m-trans (h k)))))
 
1721
               :in-theory (disable mean-of-v*trans-of-x-xhatmin
 
1722
                                   acl2::*-+-left
 
1723
                                   acl2::*-+-right
 
1724
                                   acl2::*---left
 
1725
                                   acl2::*---right
 
1726
                                   ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1727
                                   ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1728
                                   acl2::x-*-zero))
 
1729
              ("Goal'7'"
 
1730
               :use ((:theorem 
 
1731
                      (IMPLIES (m-= (m-mean (m-* (v k)
 
1732
                                                 (m-* (m-- (m-trans (x k))
 
1733
                                                           (m-trans (xhatmin k)))
 
1734
                                                      (m-trans (h k)))))
 
1735
                                    (m-* (m-zero (m) (n))
 
1736
                                         (m-trans (h k))))
 
1737
                               (m-= (m-mean (m-* (v k)
 
1738
                                                 (m-- (m-* (m-trans (x k))
 
1739
                                                           (m-trans (h k)))
 
1740
                                                      (m-* (m-trans (xhatmin k))
 
1741
                                                           (m-trans (h k))))))
 
1742
                                    (m-zero (m) (m)))))))
 
1743
              ("Subgoal 1"
 
1744
               :in-theory (enable acl2::*-+-left)))))
 
1745
 
 
1746
   (defthm lemma-4
 
1747
     (m-= (m-mean (m-* (m-+ (m-- (m-* (h k) (x k))
 
1748
                                 (m-* (h k) (xhatmin k)))
 
1749
                            (v k))
 
1750
                       (m-trans (m-+ (m-- (m-* (h k) (x k))
 
1751
                                          (m-* (h k) (xhatmin k)))
 
1752
                                     (v k)))))
 
1753
          (m-mean (m-+ (m-* (m-- (m-* (h k) (x k))
 
1754
                                 (m-* (h k) (xhatmin k)))
 
1755
                            (m-trans (m-- (m-* (h k) (x k))
 
1756
                                          (m-* (h k) (xhatmin k)))))
 
1757
                       (m-* (v k) (m-trans (v k))))))
 
1758
     :hints (("Goal" :do-not-induct t
 
1759
              :use ((:instance lemma-4-1
 
1760
                               (a (m-- (m-* (h k) (x k))
 
1761
                                       (m-* (h k) (xhatmin k))))
 
1762
                               (b (v k))))
 
1763
              :in-theory (disable lemma-4-1
 
1764
                                  xhatmin-recdef
 
1765
                                  mean-of-v-vtrans
 
1766
                                  mean-unary--
 
1767
                                  acl2::trans-*
 
1768
                                  acl2::trans-+
 
1769
                                  acl2::assoc-*
 
1770
                                  acl2::assoc-+
 
1771
                                  acl2::comm-+
 
1772
                                  acl2::*-+-left
 
1773
                                  acl2::*---left
 
1774
                                  ))))
 
1775
   ))
 
1776
 
 
1777
 (local
 
1778
  (encapsulate
 
1779
   ()
 
1780
 
 
1781
   (local
 
1782
    (defthm lemma-5-1
 
1783
      (implies (and (equal (l a) (l b))
 
1784
                    (equal (c a) (c b))
 
1785
                    (equal (l b) (l c))
 
1786
                    (equal (c b) (c c)))
 
1787
               (m-= (m-+ b (m-+ a c))
 
1788
                    (m-+ a (m-+ b c))))
 
1789
      :hints (("Goal"
 
1790
               :use ((:instance acl2::assoc-+
 
1791
                                (acl2::p b)
 
1792
                                (acl2::q a)
 
1793
                                (acl2::r c))
 
1794
                     (:instance acl2::assoc-+
 
1795
                                (acl2::p a)
 
1796
                                (acl2::q b)
 
1797
                                (acl2::r c)))
 
1798
               :in-theory (disable acl2::assoc-+)))))
 
1799
 
 
1800
   (defthm lemma-5
 
1801
     (m-= (m-+ (m-- (m-* (h k) (x k))
 
1802
                    (m-* (h k) (xhatmin k)))
 
1803
               (v k))
 
1804
          (m-- (z k) (m-* (h k) (xhatmin k))))
 
1805
     :hints (("Goal" :do-not-induct t)))
 
1806
   ))
 
1807
 
 
1808
 (local
 
1809
  (defthm lemma-6
 
1810
    (m-= (m-mean (m-* (m-- (z k) (m-* (h k) (xhatmin k)))
 
1811
                      (m-trans (m-- (z k) (m-* (h k) (xhatmin k))))))
 
1812
         (m-mean (m-+ (m-* (m-- (m-* (h k) (x k))
 
1813
                                (m-* (h k) (xhatmin k)))
 
1814
                           (m-trans (m-- (m-* (h k) (x k))
 
1815
                                         (m-* (h k) (xhatmin k)))))
 
1816
                      (m-* (v k) (m-trans (v k))))))
 
1817
    :hints (("Goal" :do-not-induct t
 
1818
             :use ((:instance lemma-4)
 
1819
                   (:instance lemma-5))
 
1820
             :in-theory (disable lemma-4 
 
1821
                                 lemma-5
 
1822
                                 z
 
1823
                                 xhatmin
 
1824
                                 x
 
1825
                                 mean-+
 
1826
                                 acl2::assoc-+
 
1827
                                 acl2::comm-+
 
1828
                                 acl2::commutativity-2-of-m-+
 
1829
                                 acl2::trans-*
 
1830
                                 acl2::trans-+
 
1831
                                 acl2::trans---
 
1832
                                 acl2::*-+-left
 
1833
                                 acl2::*-+-right
 
1834
                                 acl2::*---left
 
1835
                                 acl2::*---right
 
1836
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1837
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
1838
 
 
1839
 (local
 
1840
  (defthm lemma-7
 
1841
    (implies (and (integerp k) (<= 0 k))
 
1842
             (m-= (m-+ (m-* (h k)
 
1843
                            (m-* (pminus k)
 
1844
                                 (m-trans (h k))))
 
1845
                       (r k))
 
1846
                  (m-mean (m-* (m-- (z k) (m-* (h k) (xhatmin k)))
 
1847
                               (m-trans (m-- (z k) (m-* (h k) (xhatmin k))))))))
 
1848
    :hints (("Goal" :do-not-induct t
 
1849
             :use ((:instance lemma-3)
 
1850
                   (:instance lemma-6))
 
1851
             :in-theory (disable lemma-3 
 
1852
                                 lemma-6
 
1853
                                 z
 
1854
                                 xhatmin
 
1855
                                 x
 
1856
                                 mean-+
 
1857
                                 acl2::assoc-+
 
1858
                                 acl2::comm-+
 
1859
                                 acl2::commutativity-2-of-m-+
 
1860
                                 acl2::trans-*
 
1861
                                 acl2::trans-+
 
1862
                                 acl2::trans---
 
1863
                                 acl2::*-+-left
 
1864
                                 acl2::*-+-right
 
1865
                                 acl2::*---left
 
1866
                                 acl2::*---right
 
1867
                                 ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
1868
                                 ACL2::RIGHT-DISTRIBUTIVITY-OF-M-*-OVER-M-+)))))
 
1869
 
 
1870
 (local
 
1871
  (defthm lemma-8
 
1872
    (implies (and (integerp k) (<= 0 k))
 
1873
             (m-= (s-* 2 (m-* (gain k)
 
1874
                              (m-mean (m-* (m-- (z k)
 
1875
                                                (m-* (h k) (xhatmin k)))
 
1876
                                           (m-trans (m-- (z k)
 
1877
                                                         (m-* (h k) (xhatmin k))))))))
 
1878
                  (s-* 2 (m-* (pminus k) (m-trans (h k))))))
 
1879
    :hints (("Goal" :do-not-induct t
 
1880
             :use ((:instance lemma-7)
 
1881
                   (:instance gain-recdef))
 
1882
             :in-theory (disable lemma-0 lemma-1 lemma-3 lemma-7
 
1883
                                 gain-recdef
 
1884
                                 z
 
1885
                                 acl2::*-+-right
 
1886
                                 acl2::*-+-left
 
1887
                                 acl2::*---right
 
1888
                                 acl2::*---left
 
1889
                                 acl2::assoc-+
 
1890
                                 acl2::comm-+
 
1891
                                 acl2::left-distributivity-of-m-*-over-m-+
 
1892
                                 acl2::right-distributivity-of-m-*-over-m-+
 
1893
                                 pminus-as-mean))
 
1894
            ("Goal'5'"
 
1895
             :by (:theorem
 
1896
                  (implies (and (integerp k) (<= 0 k))
 
1897
                           (m-= (s-* 2 (m-* (pminus k)
 
1898
                                            (m-* (m-trans (h k))
 
1899
                                                 (m-* (m-inv (m-+
 
1900
                                                              (m-* (h k)
 
1901
                                                                   (m-* (pminus k)
 
1902
                                                                        (m-trans (h k))))
 
1903
                                                              (r k)))
 
1904
                                                      (m-+
 
1905
                                                       (m-* (h k)
 
1906
                                                            (m-* (pminus k)
 
1907
                                                                 (m-trans (h k))))
 
1908
                                                       (r k))))))
 
1909
                                (s-* 2
 
1910
                                     (m-* (pminus k)
 
1911
                                          (m-trans (h k))))))))
 
1912
            ("Goal'6'"
 
1913
             :use ((:instance acl2::inv-*-x
 
1914
                              (acl2::p (m-+ (r k)
 
1915
                                            (m-* (h k)
 
1916
                                                 (m-* (pminus k)
 
1917
                                                      (m-trans (h k))))))))
 
1918
             :in-theory (disable lemma-0 lemma-1 lemma-3 lemma-7
 
1919
                                 z
 
1920
                                 acl2::inv-*-x
 
1921
                                 acl2::*-+-left
 
1922
                                 acl2::*-+-right
 
1923
                                 acl2::*---left
 
1924
                                 acl2::*---right
 
1925
                                 acl2::assoc-*
 
1926
                                 acl2::assoc-+
 
1927
                                        ;acl2::comm-+
 
1928
                                 acl2::k-*---p
 
1929
                                 acl2::k-*-x-+-y
 
1930
                                 mean-+
 
1931
                                 mean-of-v-vtrans
 
1932
                                 mean-unary--
 
1933
                                 acl2::trans-*
 
1934
                                 acl2::trans-+
 
1935
                                 acl2::unary---+
 
1936
                                 pminus-as-mean)))))
 
1937
 
 
1938
 (local
 
1939
  (defthm lemma-9
 
1940
    (implies (and (integerp k) (<= 0 k))
 
1941
             (m-= (s-* 2 (m-* (gain k)
 
1942
                              (m-mean (m-* (m-- (z k)
 
1943
                                                (m-* (h k) (xhatmin k)))
 
1944
                                           (m-trans (m-- (z k)
 
1945
                                                         (m-* (h k) (xhatmin k))))))))
 
1946
                  (s-* 2 (m-mean (m-* (m-- (x k) (xhatmin k))
 
1947
                                      (m-trans (m-- (m-* (h k) (x k))
 
1948
                                                    (m-* (h k) (xhatmin k)))))))))
 
1949
    :hints (("Goal" :do-not-induct t
 
1950
             :use ((:instance lemma-0)
 
1951
                   (:instance lemma-8))
 
1952
             :in-theory (disable lemma-0 lemma-8
 
1953
                                 gain gain-recdef
 
1954
                                 z
 
1955
                                 xhatmin
 
1956
                                 x
 
1957
                                 )
 
1958
             ))))
 
1959
 
 
1960
 (local
 
1961
  (encapsulate
 
1962
   ()
 
1963
 
 
1964
   (local
 
1965
    (defthm lemma-10-1
 
1966
      (implies (and (equal (l a) (l b))
 
1967
                    (equal (c a) (c b))
 
1968
                    (equal (l b) (l c))
 
1969
                    (equal (c b) (c c)))
 
1970
               (m-= (m-+ b (m-+ a c))
 
1971
                    (m-+ a (m-+ b c))))
 
1972
      :hints (("Goal"
 
1973
               :use ((:instance acl2::assoc-+
 
1974
                                (acl2::p b)
 
1975
                                (acl2::q a)
 
1976
                                (acl2::r c))
 
1977
                     (:instance acl2::assoc-+
 
1978
                                (acl2::p a)
 
1979
                                (acl2::q b)
 
1980
                                (acl2::r c)))
 
1981
               :in-theory (disable acl2::assoc-+)))))
 
1982
 
 
1983
   (local
 
1984
    (defthm lemma-10-2
 
1985
      (equal (m-- (z k) (m-* (h k) (xhatmin k)))
 
1986
             (m-+ (m-* (h k) (m-- (x k) (xhatmin k))) (v k)))
 
1987
      :hints (("Goal" :do-not-induct t))
 
1988
      ))
 
1989
 
 
1990
   (local
 
1991
    (defthm lemma-10-3
 
1992
      (m-= (m-trans (m-- (z k) (m-* (h k) (xhatmin k))))
 
1993
           (m-+ (m-trans (m-- (m-* (h k) (x k)) 
 
1994
                              (m-* (h k) (xhatmin k))))
 
1995
                (m-trans (v k))))
 
1996
      :hints (("Goal" :do-not-induct t))))
 
1997
 
 
1998
   (local
 
1999
    (defthm lemma-10-4
 
2000
      (m-= (m-mean (m-* (m-- (xhatmin k) (x k))
 
2001
                        (m-trans (m-- (z k)
 
2002
                                      (m-* (h k) (xhatmin k))))))
 
2003
           (m-mean (m-* (m-- (xhatmin k) (x k))
 
2004
                        (m-trans (m-- (m-* (h k) (x k)) 
 
2005
                                      (m-* (h k) (xhatmin k)))))))
 
2006
      :hints (("Goal" :do-not-induct t
 
2007
               :in-theory (disable MEAN-UNARY--
 
2008
                                   z
 
2009
                                   mean-+
 
2010
                                   acl2::trans---
 
2011
                                   acl2::trans-+
 
2012
                                   acl2::trans-*
 
2013
                                   lemma-10-1
 
2014
                                   lemma-10-2
 
2015
                                   acl2::*-+-left
 
2016
                                   acl2::*---left
 
2017
                                   acl2::*-+-right
 
2018
                                   acl2::*---right
 
2019
                                   acl2::left-distributivity-of-m-*-over-m-+
 
2020
                                   acl2::right-distributivity-of-m-*-over-m-+
 
2021
                                   acl2::comm-+
 
2022
                                   ))
 
2023
 
 
2024
 
 
2025
              ("Goal'"
 
2026
               :use ((:instance acl2::*-+-right
 
2027
                                (acl2::p (M-- (XHATMIN K) (X K)))
 
2028
                                (acl2::q (M-TRANS (M-- (M-* (H K) (X K))
 
2029
                                                       (M-* (H K) (XHATMIN K)))))
 
2030
                                (acl2::r (M-TRANS (V K)))))
 
2031
               :in-theory (disable z
 
2032
                                   MEAN-UNARY--
 
2033
                                   mean-+
 
2034
                                   acl2::trans---
 
2035
                                   acl2::trans-+
 
2036
                                   acl2::trans-*
 
2037
                                   acl2::*-+-right
 
2038
                                   acl2::*---right
 
2039
                                   acl2::*-+-left
 
2040
                                   acl2::*---left
 
2041
                                   acl2::comm-+
 
2042
                                   acl2::left-distributivity-of-m-*-over-m-+
 
2043
                                   acl2::right-distributivity-of-m-*-over-m-+
 
2044
                                   ))
 
2045
 
 
2046
              ("Goal'5'"
 
2047
               :by (:theorem
 
2048
                    (m-=
 
2049
                     (m-mean (m-+ (m-* (m-+ (xhatmin k) (m-unary-- (x k)))
 
2050
                                       (m-trans (m-+ (m-* (h k) (x k))
 
2051
                                                     (m-unary-- (m-* (h k) (xhatmin k))))))
 
2052
                                  (m-* (m-+ (xhatmin k) (m-unary-- (x k)))
 
2053
                                       (m-trans (v k)))))
 
2054
                     (m-mean (m-* (m-+ (xhatmin k) (m-unary-- (x k)))
 
2055
                                  (m-trans (m-+ (m-* (h k) (x k))
 
2056
                                                (m-unary-- (m-* (h k) (xhatmin k))))))))))
 
2057
              ("Goal'6'"
 
2058
               :use ((:instance mean-of-x-xhatmin*vtrans)
 
2059
                     (:instance mean-unary-- 
 
2060
                                (p (m-* (m-+ (x k)
 
2061
                                             (m-unary-- (xhatmin k)))
 
2062
                                        (m-trans (v k)))))
 
2063
                     (:theorem (m-= (m-unary-- (m-* (m-+ (x k)
 
2064
                                                         (m-unary-- (xhatmin k)))
 
2065
                                                    (m-trans (v k))))
 
2066
                                    (m-* (m-+ (xhatmin k) (m-unary-- (x k)))
 
2067
                                         (m-trans (v k))))))
 
2068
               :in-theory (disable mean-of-x-xhatmin*vtrans
 
2069
                                   mean-unary--))
 
2070
 
 
2071
              ("Subgoal 2"
 
2072
               :use ((:instance M-=-IMPLIES-M-=-M-MEAN-1
 
2073
                                (x (m-* (m-- (xhatmin k) (x k)) 
 
2074
                                        (m-trans (v k))))
 
2075
                                (x-equiv (m-unary-- (m-* (m-- (x k) (xhatmin k))
 
2076
                                                         (m-trans (v k))))))
 
2077
                     )
 
2078
               :in-theory (disable mean-of-x-xhatmin*vtrans
 
2079
                                   mean-unary--
 
2080
                                   lemma-10-1
 
2081
                                   acl2::*-+-left
 
2082
                                   acl2::*-+-right
 
2083
                                   acl2::*---left
 
2084
                                   acl2::*---right
 
2085
                                        ;acl2::comm-+
 
2086
                                   acl2::trans-*
 
2087
                                   acl2::trans-+
 
2088
                                   acl2::trans---
 
2089
                                   acl2::left-distributivity-of-m-*-over-m-+
 
2090
                                   acl2::right-distributivity-of-m-*-over-m-+
 
2091
                                   (:congruence M-=-IMPLIES-M-=-M-MEAN-1)
 
2092
                                   ))
 
2093
              )))
 
2094
 
 
2095
   (local
 
2096
    (defthm lemma-10-5
 
2097
      (implies (and (m-matrixp (l a) (c a) a)
 
2098
                    (m-matrixp (l b) (c b) b)
 
2099
                    (equal (l a) (l b))
 
2100
                    (equal (c a) (c b)))
 
2101
               (m-= (m-- b a)
 
2102
                    (m-unary-- (m-- a b))))))
 
2103
 
 
2104
 
 
2105
   (local
 
2106
    (defthm lemma-10-6
 
2107
      (implies (and (m-matrixp (l a) (c a) a)
 
2108
                    (m-matrixp (l b) (c b) b)
 
2109
                    (m-matrixp (l c) (c c) c)
 
2110
                    (equal (l a) (l b))
 
2111
                    (equal (c a) (c b))
 
2112
                    (equal (c b) (l c)))
 
2113
               (m-= (m-unary-- (m-mean (m-* (m-- a b) c)))
 
2114
                    (m-mean (m-* (m-- b a) c))))
 
2115
      :hints (("Goal" 
 
2116
               :use ((:instance lemma-10-5)
 
2117
                     (:instance M-=-IMPLIES-M-=-M-MEAN-1
 
2118
                                (x (ACL2::M-BINARY-* (ACL2::M-BINARY-+ B (ACL2::M-UNARY-- A))
 
2119
                                                     C))
 
2120
                                (x-equiv (m-* (m-unary-- (m-- a b)) c)))
 
2121
                     )
 
2122
               :in-theory (disable lemma-10-5 acl2::unary---+ acl2::assoc-+
 
2123
                                   m-=-implies-m-=-m-mean-1))
 
2124
              ("Goal'4'"
 
2125
               :by (:theorem 
 
2126
                    (implies
 
2127
                     (and (acl2::matrixp (car (dimensions 'acl2::$arg a))
 
2128
                                         (car (dimensions 'acl2::$arg c))
 
2129
                                         a)
 
2130
                          (acl2::matrixp (car (dimensions 'acl2::$arg a))
 
2131
                                         (car (dimensions 'acl2::$arg c))
 
2132
                                         b)
 
2133
                          (acl2::matrixp (car (dimensions 'acl2::$arg c))
 
2134
                                         (cadr (dimensions 'acl2::$arg c))
 
2135
                                         c))
 
2136
                     (acl2::m-=
 
2137
                      (acl2::m-unary--
 
2138
                       (m-mean (acl2::m-binary-* (acl2::m-binary-+ a (acl2::m-unary-- b))
 
2139
                                                 c)))
 
2140
                      (m-mean (acl2::m-binary-*
 
2141
                               (acl2::m-unary-- (acl2::m-binary-+ a (acl2::m-unary-- b)))
 
2142
                               c)))))
 
2143
               :in-theory (disable lemma-10-5 acl2::unary---+ acl2::assoc-+)))))
 
2144
 
 
2145
   (defthm lemma-10
 
2146
     (m-= (m-mean (m-* (m-- (xhatmin k) (x k))
 
2147
                       (m-trans (m-- (z k)
 
2148
                                     (m-* (h k) (xhatmin k))))))
 
2149
          (m-unary-- (m-mean (m-* (m-- (x k) (xhatmin k))
 
2150
                                  (m-trans (m-- (m-* (h k) (x k))
 
2151
                                                (m-* (h k) (xhatmin k))))))))
 
2152
     :hints (("Goal" :do-not-induct t
 
2153
              :use ((:instance lemma-10-4)
 
2154
                    (:instance lemma-10-6
 
2155
                               (a (xhatmin k))
 
2156
                               (b (x k))
 
2157
                               (c (m-trans (m-- (m-* (h k) (x k))
 
2158
                                                (m-* (h k) (xhatmin k))))))
 
2159
                    )
 
2160
              :in-theory (disable lemma-10-2
 
2161
                                  lemma-10-3
 
2162
                                  lemma-10-4
 
2163
                                  lemma-10-5
 
2164
                                  lemma-10-6
 
2165
                                  z
 
2166
                                  mean-unary--
 
2167
                                  acl2::*---left
 
2168
                                  acl2::*---right
 
2169
                                  acl2::*-+-left
 
2170
                                  acl2::*-+-right
 
2171
                                  acl2::unary---+
 
2172
                                  acl2::trans-*
 
2173
                                  acl2::trans-+
 
2174
                                  acl2::trans---
 
2175
                                  acl2::comm-+
 
2176
                                  acl2::assoc-+
 
2177
                                  ACL2::LEFT-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
2178
                                  ACL2::right-DISTRIBUTIVITY-OF-M-*-OVER-M-+
 
2179
                                  mean-+))))
 
2180
   ))
 
2181
    
 
2182
 (defthm gain-minimizes-error
 
2183
   (implies (and (integerp k) (<= 0 k))
 
2184
            (m-= (result-form-derivative (gain k) (xhatmin k) k)
 
2185
                 (m-zero (n) (m))))
 
2186
   :hints (("Goal" :do-not-induct t
 
2187
            :use ((:instance lemma-9)
 
2188
                  (:instance lemma-10)
 
2189
                  (:instance gain-recdef))
 
2190
            :in-theory (disable lemma-9 
 
2191
                                lemma-10 
 
2192
                                lemma-0
 
2193
                                lemma-1
 
2194
                                lemma-3
 
2195
                                lemma-6
 
2196
                                lemma-7
 
2197
                                lemma-8
 
2198
                                gain-recdef
 
2199
                                xhatmin-recdef
 
2200
                                acl2::assoc-+
 
2201
                                acl2::*-+-left
 
2202
                                acl2::*-+-right
 
2203
                                acl2::*---left
 
2204
                                acl2::*---right
 
2205
                                acl2::assoc-*
 
2206
                                acl2::comm-+
 
2207
                                z
 
2208
                                acl2::trans-*
 
2209
                                acl2::trans-+
 
2210
                                acl2::trans---
 
2211
                                pminus-recdef
 
2212
                                        ;MINUS-AS-PLUS-INVERSE
 
2213
                                ))))
 
2214
 )
 
2215
 
 
2216
(defthm xhatmin=best-prior-almost
 
2217
  (implies (m-= (xhat (1- k))
 
2218
                (best-estimate-of-x (1- k)))
 
2219
           (m-= (xhatmin k)
 
2220
                (best-prior-estimate-of-x k)))
 
2221
  :hints (("Goal" :do-not-induct t
 
2222
           :in-theory (disable xhat z)))
 
2223
  :rule-classes nil)
 
2224
 
 
2225
(local
 
2226
 (defun natural-induction (k)
 
2227
   (if (zp k)
 
2228
       1
 
2229
     (1+ (natural-induction (1- k))))))
 
2230
 
 
2231
(defthm result-form-=-xhat
 
2232
  (equal (result-form (gain k) (xhatmin k) k)
 
2233
         (xhat k)))
 
2234
 
 
2235
(defthm xhat=best-estimate
 
2236
  (implies (and (integerp k)
 
2237
                (<= 0 k))
 
2238
           (m-= (xhat k)
 
2239
                (best-estimate-of-x k)))
 
2240
  :hints (("Goal" 
 
2241
           :induct (natural-induction k))
 
2242
          ("Subgoal *1/2"
 
2243
           :use ((:instance xhatmin=best-prior-almost)
 
2244
                 (:instance best-estimate-of-x-def
 
2245
                            (y (gain k))
 
2246
                            (Xp (xhatmin k)))
 
2247
                 (:instance gain-minimizes-error))
 
2248
           :in-theory (disable xhat))
 
2249
          ("Subgoal *1/1"
 
2250
           :use ((:instance best-estimate-of-x-def
 
2251
                            (y (gain 0))
 
2252
                            (Xp (xhatmin 0))
 
2253
                            (k 0)))
 
2254
           :in-theory (disable gain-recdef
 
2255
                               (best-prior-estimate-of-x)
 
2256
                               (xhatmin)
 
2257
                               (gain)))
 
2258
          )
 
2259
  :rule-classes nil)
 
2260
 
 
2261
(defthm xhatmin=best-prior
 
2262
  (implies (and (integerp k)
 
2263
                (<= 0 k))
 
2264
           (m-= (xhatmin k)
 
2265
                (best-prior-estimate-of-x k)))
 
2266
  :hints (("Goal" :do-not-induct t
 
2267
           :use ((:instance xhatmin=best-prior-almost)
 
2268
                 (:instance xhat=best-estimate (k (1- k))))
 
2269
           :in-theory '(best-prior-estimate-of-x zp)))
 
2270
  :rule-classes nil)
 
2271