← 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/mentry.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/mentry.lisp
 
1
;;;;; Provides indexed access to rows, columns and entries in a matrix.
 
2
(in-package "ACL2")
 
3
 
 
4
;;; If (nfix i) is greater then the length of a list, then the nth equals nil.
 
5
(defthm nth-over
 
6
  (implies (<= (len l) (nfix i))
 
7
           (equal (nth i l) nil)))
 
8
 
 
9
(include-book "mdefthms")
 
10
 
 
11
(defmacro row-guard (i m)
 
12
  `(and (matrixp ,m)
 
13
        (integerp ,i)
 
14
        (<= 0 ,i)
 
15
        (< ,i (row-count ,m))))
 
16
 
 
17
;;; Returns row at index i in matrix m.
 
18
(defun row (i m)
 
19
  (declare (xargs :guard (row-guard i m)))
 
20
  (cond ((m-emptyp m) nil)
 
21
        ((zp i) (row-car m))
 
22
        (t (row (1- i) (row-cdr m)))))
 
23
 
 
24
;;; Provide an alterate definition of row that uses col-cdr instead of row-cdr.
 
25
(defthm row-by-col-def
 
26
  (implies (matrixp m)
 
27
           (equal (row i m)
 
28
                  (if (or (m-emptyp m)
 
29
                          (>= (nfix i) (row-count m)))
 
30
                      nil
 
31
                    (cons (nth i (col-car m))
 
32
                          (row i (col-cdr m))))))
 
33
  :hints (("Goal" :induct (row i m)))
 
34
  :rule-classes :definition)
 
35
 
 
36
(defthm mvectorp-row
 
37
  (implies (matrixp m)
 
38
           (mvectorp (row i m)))
 
39
  :rule-classes (:rewrite :type-prescription))
 
40
 
 
41
(defthm len-row
 
42
  (implies (matrixp m)
 
43
           (equal (len (row i m))
 
44
                  (if (< (nfix i) (row-count m))
 
45
                      (col-count m)
 
46
                    0)))
 
47
  :hints (("Goal" :induct (row i m))))
 
48
 
 
49
(defthm consp-row
 
50
  (implies (matrixp m)
 
51
           (equal (consp (row i m))
 
52
                  (< (nfix i) (row-count m))))
 
53
  :hints (("Subgoal *1/6"
 
54
           :cases ((< (1- i) (row-count (row-cdr m)))))))
 
55
 
 
56
(defmacro col-guard (i m)
 
57
  `(and (matrixp ,m)
 
58
        (integerp ,i)
 
59
        (<= 0 ,i)
 
60
        (< ,i (col-count ,m))))
 
61
 
 
62
(defun col (i m)
 
63
  (declare (xargs :guard (col-guard i m)))
 
64
  (cond ((m-emptyp m) nil)
 
65
        ((zp i) (col-car m))
 
66
        (t (col (1- i) (col-cdr m)))))
 
67
 
 
68
(defthm col-by-row-def
 
69
  (implies (matrixp m)
 
70
           (equal (col i m)
 
71
                  (if (or (m-emptyp m)
 
72
                          (>= (nfix i) (col-count m)))
 
73
                      nil
 
74
                    (cons (nth i (row-car m))
 
75
                          (col i (row-cdr m))))))
 
76
  :hints (("Goal" :induct (col i m)))
 
77
  :rule-classes :definition)
 
78
 
 
79
(defthm mvectorp-col
 
80
  (implies (matrixp m)
 
81
           (mvectorp (col i m)))
 
82
  :rule-classes (:rewrite :type-prescription))
 
83
 
 
84
(defthm len-col
 
85
  (implies (matrixp m)
 
86
           (equal (len (col i m))
 
87
                  (if (< (nfix i) (col-count m))
 
88
                      (row-count m)
 
89
                    0))))
 
90
 
 
91
(defthm consp-col
 
92
  (implies (matrixp m)
 
93
           (equal (consp (col i m))
 
94
                  (< (nfix i) (col-count m))))
 
95
  :hints (("Subgoal *1/6"
 
96
           :cases ((< (1- i) (col-count (col-cdr m)))))))
 
97
 
 
98
(defmacro mentry-guard (r c m)
 
99
  `(and (matrixp ,m)
 
100
        (integerp ,r)
 
101
        (<= 0 ,r)
 
102
        (< ,r (row-count ,m))
 
103
        (integerp ,c)
 
104
        (<= 0 ,c)
 
105
        (< ,c (col-count ,m))))
 
106
 
 
107
;;; Return the entry at the specified row and column
 
108
(defun mentry (r c m)
 
109
  (declare (xargs :guard (mentry-guard r c m)))
 
110
  (nth c (row r m)))
 
111
 
 
112
;;; Provide an alterate equivalent definition of mentry.
 
113
(defthmd mentry-by-col
 
114
  (implies (matrixp m)
 
115
           (equal (mentry r c m)
 
116
                  (nth r (col c m))))
 
117
  :rule-classes :definition)
 
118