1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
;; Copyright (C) 2024 Carl Kwan
;;
;; Some basic theorems about mtrans and symmetric matrices
;;
;; Requires:
(in-package "ACL2")
(include-book "mout")
(encapsulate
nil
(defthm row-car-mtrans
(implies (matrixp A)
(equal (row-car (mtrans A)) (col-car A))))
(defthm col-car-mtrans
(implies (matrixp A)
(equal (col-car (mtrans A)) (row-car A))))
(defthm row-car-col-cdr-mtrans
(implies (and (matrixp A) (not (m-emptyp A)))
(equal (row-car (col-cdr (mtrans A)))
(col-car (row-cdr A)))))
(defthm mtrans-row-car-col-car
(implies (and (matrixp A) (equal (mtrans A) A) (not (m-emptyp A)))
(equal (row-car A) (col-car A)))
:rule-classes :forward-chaining)
(defthm col-cdr-row-cdr-mtrans
(implies (and (matrixp A) (not (m-emptyp A)))
(equal (col-cdr (row-cdr (mtrans A)))
(mtrans (row-cdr (col-cdr A))))))
(defthm row-cdr-col-cdr-mtrans
(implies (and (matrixp A) (not (m-emptyp A)))
(equal (row-cdr (col-cdr (mtrans A)))
(mtrans (row-cdr (col-cdr A))))))
(defthm sym-monotonicity
(implies (and (matrixp A)
(not (m-emptyp (row-cdr (col-cdr A))))
(equal (mtrans A) A))
(equal (mtrans (col-cdr (row-cdr A)))
(col-cdr (row-cdr A))))))
;; end encapsulate
(defthm sym-out-*-self
(implies (mvectorp v) (equal (mtrans (out-* v v)) (out-* v v))))
(defthm sum-of-sym
(implies (and (matrixp A) (matrixp B)
(equal (mtrans A) A)
(equal (mtrans B) B))
(equal (mtrans (m+ A B)) (m+ A B))))
(defthm sm*-of-sym
(implies (and (equal (mtrans A) A) (matrixp A))
(equal (mtrans (sm* c A)) (sm* c A))))
(defthm m--of-sym
(implies (and (equal (mtrans A) A) (matrixp A))
(equal (mtrans (sm* -1 A)) (sm* -1 A))))
(defthm sym-of-syr1-update
(implies (and (mvectorp v)
(matrixp A)
(equal (mtrans A) A)
(equal (len v) (row-count A))
(equal (col-count A) (row-count A)))
(equal (mtrans (m+ A (out-* v v)))
(m+ A (out-* v v)))))
(defthm sym-of-syr1-update-minus
(implies (and (mvectorp v)
(matrixp A)
(equal (mtrans A) A)
(equal (len v) (row-count A))
(equal (col-count A) (row-count A)))
(equal (mtrans (m+ A (sm* -1 (out-* v v))))
(m+ A (sm* -1 (out-* v v))))))
(in-theory (disable sym-out-*-self
sum-of-sym
sm*-of-sym
m--of-sym
sym-of-syr1-update
sym-of-syr1-update-minus))
|
