~/Dropbox/talks/key-workshop-july-2015/demos$ acl2-7.1
Welcome to Clozure Common Lisp Version 1.11-dev-r16378M-trunk  (DarwinX8664)!

 ACL2 Version 7.1 built May 6, 2015  18:48:38.
 Copyright (C) 2015, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).

 Includes support for hash cons, memoization, and applicative hash
 tables.

 See the documentation topic note-7-1 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

Customizing with "/Users/kaufmann/acl2-customization.lsp".

ACL2 Version 7.1.  Level 1.  Cbd "/Users/kaufmann/".
System books directory "/Users/kaufmann/acl2/v7-1/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !><state>
ACL2 !>Bye.

ACL2 Version 7.1.  Level 1.  Cbd 
"/Users/kaufmann/Dropbox/talks/key-workshop-july-2015/demos/".
System books directory "/Users/kaufmann/acl2/v7-1/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(+ 3 4) ; 3+4 in Lisp syntax (prefix notation)
7
ACL2 !>(defun f (x) ; define f(x) = x+10
	 (+ x 10))

Since F is non-recursive, its admission is trivial.
We observe that the type of F is described by the theorem
(ACL2-NUMBERP (F X)).  We used primitive type reasoning.

Summary
Form:  ( DEFUN F ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 F
ACL2 !>(f 3) ; f(3)
13
ACL2 !>(* (f 0) (f 1)) ; f(0) * f(1)
110
ACL2 !>(thm ; trivial theorem: f(x) = 10+x
	(equal (f x)
	       (+ 10 x)))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION F)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  9

Proof succeeded.
ACL2 !>(thm
	;; trivially proved by execution: f(0)*f(1) = 110
	(equal (* (f 0) (f 1))
	       110))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART F))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  7

Proof succeeded.
ACL2 !>(defun fact (n) ; factorial
	 (if (posp n) ; n is a positive integer
	     (* n (fact (- n 1)))
	   1))

For the admission of FACT we will use the relation O<
(which is known to be well-founded on the domain recognized
by O-P) and the measure (ACL2-COUNT N).  The non-trivial
part of the measure conjecture is

Goal
(IMPLIES (POSP N)
         (O< (ACL2-COUNT (+ -1 N))
             (ACL2-COUNT N))).
Goal'

Q.E.D.

That completes the proof of the measure theorem for
FACT.  Thus, we admit this function under the principle
of definition.  We observe that the type of FACT is
described by the theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))).
We used the :compound-recognizer rule POSP-COMPOUND-RECOGNIZER
and primitive type reasoning.

Summary
Form:  ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  24
 FACT
ACL2 !>(thm  ; trivial theorem, proved by execution
	(equal (fact 100)
	       93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART FACT))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  4

Proof succeeded.
ACL2 !>(integer-length (fact 10000)) ; number of bits in answer
118459
ACL2 !>(defun fib (n) ; much more expensive than factorial!
	 (declare (type (integer 0 *) n))
	 (if (posp n)
	     (if (equal n 1)
		 1
	       (+ (fib (- n 1))
		  (fib (- n 2))))
	   1))

For the admission of FIB we will use the relation O<
(which is known to be well-founded on the domain recognized
by O-P) and the measure (ACL2-COUNT N).  The non-trivial
part of the measure conjecture is

Goal
(AND (IMPLIES (AND (POSP N) (NOT (EQUAL N 1)))
              (O< (ACL2-COUNT (+ -2 N))
                  (ACL2-COUNT N)))
     (IMPLIES (AND (POSP N) (NOT (EQUAL N 1)))
              (O< (ACL2-COUNT (+ -1 N))
                  (ACL2-COUNT N)))).
Subgoal 2

Splitter note (see :DOC splitter) for Subgoal 2 (2 subgoals).
  if-intro: ((:DEFINITION ACL2-COUNT)
             (:DEFINITION INTEGER-ABS)
             (:DEFINITION O<))

Subgoal 2.2
Subgoal 2.1
Subgoal 1

Q.E.D.

That completes the proof of the measure theorem for
FIB.  Thus, we admit this function under the principle
of definition.  We observe that the type of FIB is described
by the theorem (AND (INTEGERP (FIB N)) (< 0 (FIB N))).
We used primitive type reasoning.

Computing the guard conjecture for FIB....

The non-trivial part of the guard conjecture for FIB,
given the :compound-recognizer rule POSP-COMPOUND-RECOGNIZER,
primitive type reasoning and the :type-prescription
rule FIB, is

Goal
(IMPLIES (AND (<= 0 N)
              (INTEGERP N)
              (POSP N)
              (NOT (EQUAL N 1)))
         (<= 0 (+ -2 N))).

Q.E.D.

That completes the proof of the guard theorem for FIB.
FIB is compliant with Common Lisp.

Summary
Form:  ( DEFUN FIB ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION ACL2-COUNT)
        (:DEFINITION INTEGER-ABS)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION POSP)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:TYPE-PRESCRIPTION FIB))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION ACL2-COUNT)
             (:DEFINITION INTEGER-ABS)
             (:DEFINITION O<))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  310
 FIB
ACL2 !>(time$ (fib 30))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 0.02 seconds realtime, 0.02 seconds runtime
; (16 bytes allocated).
1346269
ACL2 !>(time$ (fib 40)) ; exponential time behavior!
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 1.77 seconds realtime, 1.77 seconds runtime
; (16 bytes allocated).
165580141
ACL2 !>(memoize 'fib)


ACL2 !>>(TABLE
             MEMOIZE-TABLE
             (DEREF-MACRO-NAME 'FIB
                               (MACRO-ALIASES WORLD))
             (LIST* (CONS :CONDITION-FN T)
                    (CONS :INLINE T)
                    (CONS :COMMUTATIVE NIL)
                    (CONS :FORGET NIL)
                    (CONS :MEMO-TABLE-INIT-SIZE (OR NIL *MHT-DEFAULT-SIZE*))
                    (CONS :AOKP 'NIL)
                    (CONS :STATS :DEFAULT)
                    (AND (NOT (EQ ':DEFAULT :DEFAULT))
                         (LIST (CONS :IDEAL-OKP ':DEFAULT)))))

Summary
Form:  ( TABLE MEMOIZE-TABLE ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MEMOIZE-TABLE


ACL2 !>>(VALUE-TRIPLE (DEREF-MACRO-NAME 'FIB
                                        (MACRO-ALIASES (W STATE))))
FIB

Summary
Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FIB
ACL2 !>(time$ (fib 40)) ; virtually instantaneous!
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 0.00 seconds realtime, 0.00 seconds runtime
; (1,744 bytes allocated).
165580141
ACL2 !>(quit)

~/Dropbox/talks/key-workshop-july-2015/demos$