; Big note: ACL2 progress depends on the user community, especially,
; documentation.  Please let me know when you come across inadequate or missing
; documentation.

; Note: I'm to give an invited talk at Empirically Successful Computerized
; Reasoning (ESCoR), Seattle, August 21 (ACL2 workshop is August 15-16).  This
; talk is kind of related to that.  Please feel free to provide suggestions for
; what to say in that talk!

; During this talk, I should point out what I'm doing in emacs.  Feel free to
; stop me and ask what I just did!

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; References
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Documentation:
; + Note availability online, with HTML, and with emacs info.  PS (and PDF)
;   version possible.
; + See :DOC ACL2-TUTORIAL and/or its potentially useful sub-topics such as
;   INTRODUCTION, TIPS and TIDBITS.

; Interaction with the Boyer-Moore Theorem Prover:  A Tutorial Study Using the
; Arithmetic-Geometric Mean Theorem (with Paolo Pecchiari).  {\em Journal of
; Automated Reasoning} 16, no. 1-2 (1996) 181-222.

; See http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/,
; especially "How to Prove Theorems Formally", which has lots of hints and
; exercises.

; {\em Computer-Aided Reasoning: An Approach} (with P. Manolios and J Moore).
; Kluwer Academic Publishers, June, 2000.  Available in paperback (much
; cheaper!) from ACL2 web site.

; The list acl2-help@lists.cc.utexas.edu can be helpful.  There are archives
; available by following the "Useful Addresses" link on the ACL2 home page; or
; go directly to
; http://www.cs.utexas.edu/users/moore/acl2/admin/forms/archive.html.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Demo of proof-trees and proof-checker.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defpkg "HANOI"
    (set-difference-equal
     (union-eq *acl2-exports*
               *common-lisp-symbols-from-main-lisp-package*)
     '(PUSH POP GET)))

(rebuild "/projects/acl2/devel/books/misc/hanoi.lisp" t)

; Using a string that names a package is equivalent to an in-package:
"HANOI" ; or, (in-package "HANOI")

:ubt! h-lemma ; let's try proving h-lemma....

:start-proof-tree

; meta-x start-proof-tree

(defmacro proof-term ()
  '(implies (and (natp n)
                 (true-listp s)
                 (equal (len s) 3)
                 (perm (list a b c) '(0 1 2))
                 (big-tops a b c n s))
            (equal (play (h a b c n)
                         (put (app (tower n) (get a s))
                              a
                              s))
                   (put (app (tower n) (get c s)) c s))))

(defmacro do-proof ()
  `(defthm h-lemma
     (proof-term)
     :rule-classes nil
     :hints (("Goal" :induct (induction-hint a b c n s)))))

(do-proof)

:u

(in-theory (disable get-put))

(do-proof)

; control-c control-c

; control-z c
; control-z c
; control-z c

:pe get-put

:pl (GET B (PUT (CONS N (GET A S)) A S))

(include-book "misc/find-lemmas" :dir :system)

(acl2::find-lemmas (get put))

(verify (proof-term))

p

(induct (induction-hint a b c n s))

th

cg

th

prove

goals

th

split

(quiet prove)

(quiet (repeat prove))

goals

(contradict 2)

p

; Second-to-last line of goal is a get-put term, so try control-t d:

; (dv 1 2 3 1 2 0)

; p

; sr

; [Discuss what would happen if get-put were enabled but had hyps.

comm

(undo 2)

(in-theory (enable get-put))

bash

(quiet (repeat bash))

prove

(quiet (repeat prove))

goals

(exit h-lemma nil)

n

(in-theory (enable get-put))

(acl2::set-saved-output t t)

(do-proof)

:pso!

(acl2::set-saved-output nil :normal)

:set-print-clause-ids t

:u

(set-inhibit-output-lst '(prove))

; See :doc set-inhibit-output-lst, or see books/Makefile-generic for an
; example.

(do-proof)

; meta-x stop-proof-tree

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Emacs stuff
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; See emacs/emacs-acl2.el or follow Hyper-Card link on ACL2 home page (thanks,
; David R.).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Distributed books
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Get help in your proof effort by looking in books/README.html (e.g.,
; ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-9/acl2-sources/books/README.html).

; Sometimes overlooked may be books/misc/README.  Particularly useful may be:

; computed-hint.lisp -- examples of computed hints
; defpun.lisp -- define partial functions
; dft.lisp    -- write proofs in a sort of familiar style using dft macro
; expander.lisp     --   symbolic expansion utilities for ACL2
; dump-events.lisp  --   file-dumping utility for ACL2
; file-io.lisp
; find-lemmas.lisp -- utility for finding relevant lemmas
; priorities.lisp -- priority-based rewriting
; records.lisp   --  canonical key-value record structures
; simplify-defuns.lisp -- simplify definitions in a file and prove equivalence
; symbol-btree.lisp -- log time access on a key
; total-order.lisp -- total order for ACL2

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Break-rewrite
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Start up fresh ACL2.

; From :doc free-variables-examples-rewrite:

(encapsulate
 ((p1 (u x) t)
  (bad (x) t)
  (p2 (x y z) t)
  (bar (x y) t)
  (foo (x y) t)
  (poo (x y) t)
  (prop (u) t))

 (local (defun p1 (u x) (declare (ignore u x)) nil))
 (local (defun bad (x) (declare (ignore x)) nil))
 (local (defun p2 (x y z) (declare (ignore x y z)) nil))
 (local (defun bar (x y) (declare (ignore x y)) nil))
 (local (defun foo (x y) (declare (ignore x y)) nil))
 (local (defun poo (x y) (declare (ignore x y)) nil))
 (local (defun prop (u) (declare (ignore u)) t))

 (defthm foo-poo
   (implies (syntaxp (equal y 'y3))
            (equal (foo x y)
                   (poo x y))))

 (defthm lemma-1
   (implies (and (p1 u x)
                 (bad x)
                 (p2 x y z)
                 (bar x y)
                 (equal x x) ; admittedly silly!
                 (foo x y))
            (prop u))
   :rule-classes ((:rewrite :match-free :all))))

(thm (implies (and (p1 u0 x1)
                   (bad x1)
                   (bad x3)
                   (bar x3 y1)
                   (bar x3 y3)
                   (p1 u0 x2)
                   (p1 u0 x3)
                   (p2 x3 y1 z1)
                   (p2 x3 y3 z1))
              (prop u0)))

:brr t ; see :doc break-rewrite

:monitor (:rewrite lemma-1) t

(thm (implies (and (p1 u0 x1)
                   (bad x1)
                   (bad x3)
                   (bar x3 y1)
                   (bar x3 y3)
                   (p1 u0 x2)
                   (p1 u0 x3)
                   (p2 x3 y1 z1)
                   (p2 x3 y3 z1))
              (prop u0)))

:target
:eval
:failure-reason
(set-brr-term-evisc-tuple '(nil 2 2 nil))
:failure-reason
(set-brr-term-evisc-tuple '(nil 2 2 nil))
(set-free-vars-display-limit 4)
#.

; See :DOC free-variables and see :DOC set-brr-term-evisc-tuple.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Other notes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Tags: meta-x visit-acl2-tags-table, meta-x tags-apropos, meta-., meta-,.

; Note trace$ and note open-trace-file and close-trace-file.

; Note accumulated-persistence.

; Note set-inhibit-output-lst.

; Note :doc pstack.