← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2003/hendrix/support/mtrans.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/hendrix/support/mtrans.lisp
 
1
;;;;; Matrix transpose
 
2
;;;;; Contains definition of matrix transpose and basis properties.
 
3
;;;;; Includes relations with mzero, madd, mid, mmult, and mentry.
 
4
(in-package "ACL2")
 
5
 
 
6
(include-book "mdefthms")
 
7
 
 
8
(defun mtrans (m)
 
9
  (declare (xargs :guard (matrixp m)
 
10
                  :verify-guards nil))
 
11
  (if (m-emptyp m)
 
12
      (m-empty)
 
13
    (col-cons (row-car m) (mtrans (row-cdr m)))))
 
14
 
 
15
(defthm m-emptyp-mtrans
 
16
  (equal (m-emptyp (mtrans m))
 
17
         (m-emptyp m)))
 
18
 
 
19
(defthm row-count-mtrans
 
20
  (implies (matrixp m)
 
21
           (equal (row-count (mtrans m))
 
22
                  (col-count m))))
 
23
 
 
24
(defthm matrixp-mtrans
 
25
  (implies (matrixp m)
 
26
           (matrixp (mtrans m))))
 
27
 
 
28
(local 
 
29
 (defun col-cdr-recurse (m)
 
30
   (if (m-emptyp m)
 
31
       0
 
32
     (col-cdr-recurse (col-cdr m)))))
 
33
 
 
34
(defthm col-count-mtrans
 
35
  (implies (matrixp m)
 
36
           (equal (col-count (mtrans m))
 
37
                  (row-count m)))
 
38
  :hints (("Subgoal *1/3"
 
39
           :use (:instance col-count-def
 
40
                           (m (col-cons (row-car m)
 
41
                                        (mtrans (row-cdr m))))))))
 
42
 
 
43
(verify-guards mtrans)
 
44
 
 
45
(defthm mtrans-by-col-def
 
46
  (implies (matrixp m)
 
47
           (equal (mtrans m)
 
48
                  (if (m-emptyp m)
 
49
                      (m-empty)
 
50
                    (row-cons (col-car m)
 
51
                              (mtrans (col-cdr m))))))
 
52
  :hints (("Goal" :induct (mtrans m)))
 
53
  :rule-classes :definition)
 
54
 
 
55
(defthm mtrans-mtrans
 
56
  (implies (matrixp m)
 
57
           (equal (mtrans (mtrans m))
 
58
                  m)))
 
59
 
 
60
(include-book "mzero")
 
61
 
 
62
(defthm mtrans-zero
 
63
  (equal (mtrans (mzero r c))
 
64
         (mzero c r)))
 
65
 
 
66
(include-book "madd")
 
67
 
 
68
(defthm distr+mtrans
 
69
  (implies (and (matrixp m)
 
70
                (matrixp n))
 
71
           (equal (mtrans (m+ m n))
 
72
                  (m+ (mtrans m) (mtrans n))))
 
73
  :hints (("Goal" :induct (m+ m n))))
 
74
 
 
75
(include-book "mid")
 
76
 
 
77
(defthm mtrans-id
 
78
  (equal (mtrans (mid n))
 
79
         (mid n)))
 
80
 
 
81
(include-book "mscal")
 
82
 
 
83
(defthm sm*-trans
 
84
  (implies (matrixp m)
 
85
           (equal (mtrans (sm* s m))
 
86
                  (sm* s (mtrans m)))))
 
87
 
 
88
(include-book "mmult")
 
89
 
 
90
(defthm col*-mtrans
 
91
  (implies (row*-guard l m)
 
92
           (equal (col* l (mtrans m))
 
93
                  (row* l m))))
 
94
 
 
95
(defthm row*-mtrans
 
96
  (implies (col*-guard l m)
 
97
           (equal (row* l (mtrans m))
 
98
                  (col* l m))))
 
99
 
 
100
(defthm mtrans-m*
 
101
  (implies (m*-guard m n)
 
102
           (equal (mtrans (m* m n))
 
103
                  (m* (mtrans n) (mtrans m))))
 
104
  :hints (("Goal" :induct (m* m n))))
 
105
 
 
106
(include-book "mentry")
 
107
 
 
108
(defthm row-trans
 
109
  (implies (matrixp m)
 
110
           (equal (row i (mtrans m))
 
111
                  (col i m))))
 
112
 
 
113
(defthm col-trans
 
114
  (implies (matrixp m)
 
115
           (equal (col i (mtrans m))
 
116
                  (row i m)))
 
117
; :With directive added 3/14/06 by Matt Kaufmann for after v2-9-4.
 
118
  :hints (("Goal" :expand (:with mtrans (mtrans m)))))
 
119
 
 
120
(defthm entry-trans
 
121
  (implies (matrixp m)
 
122
           (equal (mentry r c (mtrans m))
 
123
                  (mentry c r m)))
 
124
  :hints (("Subgoal *1/2.4'" :use (:instance row-by-col-def (i c)))))