; The M0 Utility Lemmas
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;==============================================================
; This file is a certified book containing some simple lemmas
; used to make it easier to do proofs about m0 programs.

; Instructions

; To certify this book, you must first have certified your local
; copy of m0.lisp.  Then, copy this book to the same directory on 
; which your certified copy of m0.lisp resides and on which you
; have write permission, fire up ACL2 while connected to that 
; directory and then execute the following two events.
#|
(include-book "m0")

(certify-book "m0-utilities" 1)
|#
; After certification, the book may be used in an ACL2 session or
; in other books, by writing the form

; (include-book "m0-utilities")

; using the full path name as necessary.

; End of Instructions
;----------------------------------------------------------------
; Every ACL2 book must begin with an in-package form.

(in-package "M0")

; Some Simple Utility Lemmas

; The standard arithmetic lemmas are brought in here.

(include-book 
 "/home/acl2/acl2-2.7/acl2-sources/books/arithmetic/top")

; Now make stacks and states behave like abstract data types.

(defthm stacks
  (and (equal (top (push x s)) x)
       (equal (pop (push x s)) s)))

(in-theory (disable push top pop))

(defthm states
  (and (equal (pc      (make-state pc locals stack program)) pc)
       (equal (locals  (make-state pc locals stack program)) locals)
       (equal (stack   (make-state pc locals stack program)) stack)
       (equal (program (make-state pc locals stack program)) program)))

(in-theory (disable make-state pc locals stack program))

; The next block of lemmas force ACL2 to expand certain functions
; in certain common situations, augmenting its heuristics 
; controlling expansion.

(defthm step-opener
  (implies (consp (next-inst s))
           (equal (step s) (do-inst (next-inst s) s))))

(in-theory (disable step))

(defthm run-opener
  (and (equal (run s 0) s)
       (implies (and (integerp n)
		     (> n 0))
		(equal (run s n)
		       (run (step s)(+ -1 n))))))

(defthm run-sum
  (implies (and (integerp i)
		(>= i 0)
		(integerp j)
		(>= j 0))
	   (equal (run s (+ i j))
		  (run (run s i) j))))

(in-theory (disable run))