← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/trivial/sawada-model/trivia.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/2000/manolios/pipeline/trivial/sawada-model/trivia.lisp
 
1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2
; Trivia.lisp
 
3
; Copyright reserved by SRC
 
4
; Author  Jun Sawada, University of Texas at Austin
 
5
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;'
 
6
(in-package "ACL2")
 
7
 
 
8
;; Jared: changing this to an include of an identical book
 
9
(include-book "workshops/1999/pipeline/trivia" :dir :system)
 
10
 
 
11
;; (include-book "../../../../../../data-structures/array1")
 
12
;; (include-book "../../../../../../arithmetic/top")
 
13
 
 
14
;; (deflabel begin-trivia)
 
15
 
 
16
;; (defmacro quoted-constant-p (x)
 
17
;;   `(and (consp ,x) (equal (car ,x) 'quote)))
 
18
 
 
19
;; (defthm append-nil
 
20
;;     (implies (true-listp x)
 
21
;;            (equal (append x nil) x))
 
22
;;   :hints (("Goal" :in-theory (enable binary-append))))
 
23
 
 
24
;; (defun natural-induction (i)
 
25
;;     (if (zp i) t
 
26
;;      (natural-induction (1- i))))
 
27
 
 
28
;; ;; in data-structures/list-defthms
 
29
;; ;; (defthm car-nthcdr
 
30
;; ;;     (equal (car (nthcdr idx lst)) (nth idx lst)))
 
31
 
 
32
;; (defthm cdr-nthcdr
 
33
;;     (implies (and (integerp idx) (<= 0 idx))
 
34
;;           (equal (cdr (nthcdr idx lst)) (nthcdr (+ 1 idx) lst))))
 
35
 
 
36
 
 
37
;; (in-theory (disable length))
 
38
 
 
39
;; (in-theory (disable array1p compress1 default dimensions header
 
40
;;                  aref1 aset1 maximum-length))
 
41
 
 
42
;; (defthm array1p-module-type
 
43
;;   (implies
 
44
;;    (array1p name l)
 
45
;;    (and (symbolp name)
 
46
;;      (alistp l)
 
47
;;      (consp (header name l))
 
48
;;      (consp (dimensions name l))
 
49
;;      (true-listp (dimensions name l))
 
50
;;      (integerp (car (dimensions name l)))
 
51
;;      (<= 0 (car (dimensions name l)))
 
52
;;      (integerp (maximum-length name l))
 
53
;;      (<= 0 (maximum-length name l))))
 
54
;;   :hints (("Goal" :in-theory (enable array1p header default dimensions
 
55
;;                                   maximum-length)))
 
56
;;   :rule-classes
 
57
;;   ((:type-prescription :corollary 
 
58
;;               (implies
 
59
;;                (array1p name l)
 
60
;;                (and (consp (header name l)))))
 
61
;;    (:type-prescription :corollary 
 
62
;;               (implies
 
63
;;                (array1p name l)
 
64
;;                (and (consp (dimensions name l))
 
65
;;                     (true-listp (dimensions name l)))))
 
66
;;    (:type-prescription :corollary 
 
67
;;               (implies
 
68
;;                (array1p name l)
 
69
;;                (and (integerp (car (dimensions name l)))
 
70
;;                     (<= 0 (car (dimensions name l))))))
 
71
;;    (:type-prescription :corollary 
 
72
;;               (implies
 
73
;;                (array1p name l)
 
74
;;                (and (integerp (maximum-length name l))
 
75
;;                     (<= 0 (maximum-length name l)))))))
 
76
 
 
77
 
 
78
;; (local
 
79
;; (defthm compress11-empty-array
 
80
;;     (implies (and (integerp n) (>= n 0))
 
81
;;           (equal (compress11 name (list (cons :header info)) n dim default)
 
82
;;                  nil))
 
83
;;   :hints (("Goal" :In-theory (enable compress11)))))
 
84
 
 
85
 
 
86
;; (defthm compress1-empty-array
 
87
;;      (equal (compress1 tag (list (cons :header x)))
 
88
;;          (list (cons :header x)))
 
89
;;    :hints (("Goal" :in-theory (enable compress1 compress11
 
90
;;                                    header default))))
 
91
 
 
92
;; (defthm array1p-cons-with-dimensions
 
93
;;     (implies (and (array1p tag array)
 
94
;;                (integerp index)
 
95
;;                (>= index 0)
 
96
;;                (> (car (dimensions tag array)) index))
 
97
;;           (array1p tag (cons (cons index val) array)))
 
98
;;   :hints (("goal" :in-theory (enable dimensions header))))
 
99