diff options
Diffstat (limited to 'books/workshops/2002/cowles-flat')
17 files changed, 3316 insertions, 0 deletions
diff --git a/books/workshops/2002/cowles-flat/flat-slides.pdf.gz b/books/workshops/2002/cowles-flat/flat-slides.pdf.gz Binary files differnew file mode 100644 index 0000000..2493219 --- /dev/null +++ b/books/workshops/2002/cowles-flat/flat-slides.pdf.gz diff --git a/books/workshops/2002/cowles-flat/parial-a1a.pdf.gz b/books/workshops/2002/cowles-flat/parial-a1a.pdf.gz Binary files differnew file mode 100644 index 0000000..994051b --- /dev/null +++ b/books/workshops/2002/cowles-flat/parial-a1a.pdf.gz diff --git a/books/workshops/2002/cowles-flat/parial-a1a.ps.gz b/books/workshops/2002/cowles-flat/parial-a1a.ps.gz Binary files differnew file mode 100644 index 0000000..00c0728 --- /dev/null +++ b/books/workshops/2002/cowles-flat/parial-a1a.ps.gz diff --git a/books/workshops/2002/cowles-flat/support/flat-ackermann.acl2 b/books/workshops/2002/cowles-flat/support/flat-ackermann.acl2 new file mode 100644 index 0000000..569f9e4 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-ackermann.acl2 @@ -0,0 +1,6 @@ +(in-package "ACL2") +(defpkg "FLAT" + (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) +(certify-book "flat-ackermann" ? t) diff --git a/books/workshops/2002/cowles-flat/support/flat-ackermann.lisp b/books/workshops/2002/cowles-flat/support/flat-ackermann.lisp new file mode 100644 index 0000000..e56036d --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-ackermann.lisp @@ -0,0 +1,465 @@ +; Introduction of a function satisfying a slightly altered version +; of the Ackermann recursive equation. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; Original Peter version of the Ackermann recursive equation: + +; (equal (f x1 x2) +; (if (equal x1 0) +; (+ x2 1) +; (if (equal x2 0) +; (f (- x1 1) 1) +; (f (- x1 1)(f x1 (- x2 1)))))) + +; Construction based on flat domains in ACL2. + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Modified 28 December 2001. +; Last modified 2 March 2002. + +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-ackermann" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") + +#| We want a function that satisfies the original Peter version of + the Ackermann recursive equation: +(equal (f x1 x2) + (if (equal x1 0) + (+ x2 1) + (if (equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1)))))) +|# + +(defun + <def= (x y) + (or (eq x 'undef$) + (equal x y))) + +(defmacro + sq-if (test then else) + "Sequential version of IF." + `(if (eq ,test 'undef$) + 'undef$ + (if ,test ,then ,else))) + +(defmacro + lt-st-equal (x y) + "Left-strict version of equal." + `(if (eq ,x 'undef$) + 'undef$ + (equal ,x ,y))) + +(defmacro + lt-st-+ (x y) + "Left-strict version of (binary) +." + `(if (eq ,x 'undef$) + 'undef$ + (+ ,x ,y))) + +#| Our heuristics say it should be possible to get this: +(equal (f x1 x2) + (if (equal x1 0) + (+ x2 1) + (sq-if (lt-st-equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1)))))) +|# +#| Our heuristics are too primitive: + In fact we can get define a function f that satisfies: +(equal (f x1 x2) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1)))))) + + Recall that we wanted a function that satisfies the original + Peter version of the Ackermann recursive equation: +(equal (f x1 x2) + (if (equal x1 0) + (+ x2 1) + (if (equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1)))))) + + ACL2 can then prove the following, which is close to what we + had hoped for: + +(implies (not (equal x2 'undef$)) + (equal (f x1 x2) + (if (equal x1 0) + (+ x2 1) + (if (equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1))))))) +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +#| Preliminary test for suitability of definition: +(defun + f21-chain (i x1 x2) + (if (zp i) + 'undef$ + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f21-chain (- i 1)(- x1 1) 1) + (f21-chain (- i 1)(- x1 1) + (f21-chain (- i 1) x1 + (- x2 1))))))) + +(thm + (<def= (f21-chain i x1 x2) + (f21-chain (+ 1 i) x1 x2))) +|# +#| Unary version of what we want: +(equal f1 (x) + (let ((x1 (car x)) + (x2 (cadr x))) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f1 (list (- x1 1) 1)) + (f1 (list (- x1 1) + (f1 (list x1 (- x2 1))))))))) + +Heuristics suggest that second list should be right strict. +|# + +(defmacro + rt-st-list (x y) + "Right-strict version of (binary) list." + `(if (eq ,y 'undef$) + 'undef$ + (list ,x ,y))) + +(defun + f1-chain (i x) + (if (zp i) + 'undef$ + (if (eq x 'undef$) ;; Ensure f1 is strict and + 'undef$ ;; thus a monotonic function. + (let ((x1 (car x)) + (x2 (cadr x))) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f1-chain (- i 1) + (list (- x1 1) 1)) + (f1-chain + (- i 1) + (rt-st-list (- x1 1) + (f1-chain (- i 1) + (list + x1 + (- x2 1)))) + ))))))) + +(defthm + base-of-f1-chain=undef$ + (implies (zp i) + (equal (f1-chain i x) + 'undef$))) + +(defthm + f1-chain-is-<def=-chain + (implies (and (integerp i) + (>= i 0)) + (<def= (f1-chain i x) + (f1-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of f1-chain: + +(defchoose + lub-f1-chain-i i (x) + (not (equal (f1-chain i x) + 'undef$))) + +(defthm + lub-f1-chain-i-rewrite + (implies (equal (f1-chain (lub-f1-chain-i x) x) + 'undef$) + (equal (f1-chain i x) 'undef$)) + :hints (("Goal" + :use lub-f1-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-f1-chain-nat-i (x) + (nfix (lub-f1-chain-i x))) + +(in-theory (disable (:executable-counterpart + lub-f1-chain-nat-i))) + +;; Define the least upper bound of f-chain: + +(defun + lub-f1-chain (x) + (f1-chain (lub-f1-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-f1-chain))) + +(defthm + lub-f1-chain-is-upper-bound + (<def= (f1-chain i x) + (lub-f1-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($bottom$-based-chain f1-chain) + (lub-$bottom$-based-chain lub-f1-chain) + (lub-$bottom$-based-chain-nat-i lub-f1-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f1-chain-i))) + ("Subgoal 2" ; changed after v4-3 from "Subgoal 3", for tau system + :use f1-chain-is-<def=-chain))) + +(defthm + f1-chain-is-<def=-chain-f + (implies (and (>= i (lub-f1-chain-nat-i x)) + (integerp i)) + (equal (lub-f1-chain x) + (f1-chain i x))) + :hints (("Goal" + :by + (:functional-instance + $bottom$-based-chain-is-$<=$-chain-f + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($bottom$-based-chain f1-chain) + (lub-$bottom$-based-chain lub-f1-chain) + (lub-$bottom$-based-chain-nat-i lub-f1-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f1-chain-i))))) + +(defun + f1 (x) + (lub-f1-chain x)) + +(in-theory (disable (:executable-counterpart f1))) + +(defthm + f1-is-strict + (equal (f1 'undef$) 'undef$)) + +(defun + g1-chain (i x) + (f1-chain (+ 1 i) x)) + +(defun + ub-g1-chain (x) + (if (eq x 'undef$) + 'undef$ + (let ((x1 (car x)) + (x2 (cadr x))) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f1 (list (- x1 1) 1)) + (f1 (rt-st-list (- x1 1) + (f1 (list x1 (- x2 1)))) + )))))) + +(defthm + g1-chain-<def=-ub-g1-chain + (implies (and (integerp i) + (>= i 0)) + (<def= (g1-chain i x) + (ub-g1-chain x))) +; fcd/Satriani v3.7 Moore - used to be Subgoal 8 + :hints (("Subgoal 2" + :in-theory (disable lub-f1-chain-is-upper-bound) + :use (:instance + lub-f1-chain-is-upper-bound + (x (list (- (car x) 1) 1)))) +; fcd/Satriani v3.7 Moore - used to be Subgoal 3 + ("Subgoal 6" + :in-theory (disable lub-f1-chain-is-upper-bound) + :use ((:instance + lub-f1-chain-is-upper-bound + (x (list (car x)(- (cadr x) 1)))) + (:instance + lub-f1-chain-is-upper-bound + (x (list (- (car x) 1) + (f1-chain i (list (car x) + (- (cadr x) 1))))) + ))))) + +(defun + Skolem-f1 (x) + (max (lub-f1-chain-nat-i (list (- (car x) 1) 1)) + (max (lub-f1-chain-nat-i (list (car x)(- (cadr x) 1))) + (lub-f1-chain-nat-i (rt-st-list (- (car x) 1) + (f1 (list + (car x) + (- (cadr x) 1))) + ))))) + +(defthm + ub-g1-chain-=-g1-chain-Skolem-f1 + (equal (ub-g1-chain x) + (g1-chain (Skolem-f1 x) x)) + :hints (("Goal" + :use ((:instance + f1-chain-is-<def=-chain-f + (x (list (- (car x) 1) 1)) + (i (Skolem-f1 x))) + (:instance + f1-chain-is-<def=-chain-f + (x (list (car x)(- (cadr x) 1))) + (i (Skolem-f1 x))) + (:instance + f1-chain-is-<def=-chain-f + (x (rt-st-list (- (car x) 1) + (f1 (list + (car x) + (- (cadr x) 1))))) + (i (Skolem-f1 x))))))) + +(defthm + lub-f1-chain=ub-g1-chain + (equal (lub-f1-chain x)(ub-g1-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($chain$ f1-chain) + (lub-$chain$ lub-f1-chain) + (lub-$chain$-i lub-f1-chain-i) + (lub-$chain$-nat-i lub-f1-chain-nat-i) + ($f$ Skolem-f1) + (shifted-$chain$ g1-chain) + (ub-shifted-$chain$ ub-g1-chain))) + ("Subgoal 4" ; changed after v4-3 from "Subgoal 5", for tau system + :use g1-chain-<def=-ub-g1-chain) + ("Subgoal 3" ; changed after v4-3 from "Subgoal 4", for tau system + :use f1-chain-is-<def=-chain) + )) + +(defthm + f1-def + (equal (f1 x) + (if (eq x 'undef$) + 'undef$ + (let ((x1 (car x)) + (x2 (cadr x))) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f1 (list (- x1 1) 1)) + (f1 (rt-st-list (- x1 1) + (f1 (list x1 + (- x2 1)) + )) + )))))) + :hints (("Goal" + :in-theory (disable ;;lub-f1-chain + ub-g1-chain-=-g1-chain-Skolem-f1) + :use lub-f1-chain=ub-g1-chain))) + +(defun + f (x1 x2) + (f1 (list x1 x2))) + +(defthm + f-def + (equal (f x1 x2) + (if (equal x1 0) + (lt-st-+ x2 1) + (sq-if (lt-st-equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1)))))) + :hints (("Goal" + :use (:instance + f1-def + (x (list x1 x2)))))) + +; Recall the original Peter version of the Ackermann recursive +; equation: + +; (equal (f x1 x2) +; (if (equal x1 0) +; (+ x2 1) +; (if (equal x2 0) +; (f (- x1 1) 1) +; (f (- x1 1)(f x1 (- x2 1)))))) + +(in-theory (disable f f-def)) + +(defthm + Peter-version-f-def + (implies (not (equal x2 'undef$)) + (equal (f x1 x2) + (if (equal x1 0) + (+ x2 1) + (if (equal x2 0) + (f (- x1 1) 1) + (f (- x1 1)(f x1 (- x2 1))))))) + :hints (("Goal" + :use f-def))) diff --git a/books/workshops/2002/cowles-flat/support/flat-nested.acl2 b/books/workshops/2002/cowles-flat/support/flat-nested.acl2 new file mode 100644 index 0000000..d0d9495 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-nested.acl2 @@ -0,0 +1,5 @@ +(in-package "ACL2") +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) +(certify-book "flat-nested" ? t) diff --git a/books/workshops/2002/cowles-flat/support/flat-nested.lisp b/books/workshops/2002/cowles-flat/support/flat-nested.lisp new file mode 100644 index 0000000..419d6cb --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-nested.lisp @@ -0,0 +1,269 @@ +; Introduction of an arbitrary nested-recursive function. +; Construction based on flat domains in ACL2. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 20 December 2001. +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-nested" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") +#| +A construction based on flat domains in ACL2, as introduced in +flat.lisp, of a function f that satisfies the equation, for +strict functions (test x), in the following theorem, + +(defthm generic-nested-recursive-f + (equal (f x) + (sq-if (test x) (base x) (f (f (st x)))))). +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proceed with the construction: + +(defmacro + sq-if (test then else) + "Sequential version of IF." + `(if (equal ,test ($bottom$)) + ($bottom$) + (if ,test ,then ,else))) + +(encapsulate + (((test *) => *)) + + (local + (defun + test (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + test-is-strict + (equal (test ($bottom$))($bottom$))) + ) ;; end encapsulate + +(defstub + base (*) => *) + +(defstub + st (*) => *) + +(defun + f-chain (i x) + (if (zp i) + ($bottom$) + (sq-if (test x) + (base x) + (f-chain (- i 1)(f-chain (- i 1)(st x)))))) + +(defthm + base-of-f-chain=$bottom$ + (implies (zp i) + (equal (f-chain i x) + ($bottom$)))) + +(defthm + f-chain-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (f-chain i x) + (f-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of f-chain: + +(defchoose + lub-f-chain-i i (x) + (not (equal (f-chain i x) + ($bottom$)))) + +(defthm + lub-f-chain-i-rewrite + (implies (equal (f-chain (lub-f-chain-i x) x) + ($bottom$)) + (equal (f-chain i x) ($bottom$))) + :hints (("Goal" + :use lub-f-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-f-chain-nat-i (x) + (nfix (lub-f-chain-i x))) + +;; Define the least upper bound of f-chain: + +(defun + lub-f-chain (x) + (f-chain (lub-f-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-f-chain))) + +(defthm + lub-f-chain-is-upper-bound + ($<=$ (f-chain i x) + (lub-f-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))) + ("Subgoal 2" + :use f-chain-is-$<=$-chain))) + +(defthm + f-chain-is-$<=$-chain-f + (implies (and (>= i (lub-f-chain-nat-i x)) + (integerp i)) + (equal (lub-f-chain x) + (f-chain i x))) + :hints (("Goal" + :by + (:functional-instance + $bottom$-based-chain-is-$<=$-chain-f + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))))) + +(defun + f (x) + (lub-f-chain x)) + +(defun + g-chain (i x) + (f-chain (+ 1 i) x)) + +(defun + ub-g-chain (x) + (sq-if (test x) + (base x) + (f (f (st x))))) + +(defthm + g-chain-$<=$-ub-g-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (g-chain i x) + (ub-g-chain x))) + :hints (("Subgoal 2" + :in-theory (disable lub-f-chain-is-upper-bound) + :use ((:instance + lub-f-chain-is-upper-bound + (x (st x))) + (:instance + lub-f-chain-is-upper-bound + (x (f (st x)))))))) + +(defun + Skolem-f (x) + (max (lub-f-chain-nat-i (st x)) + (lub-f-chain-nat-i (f (st x))))) + +(defthm + ub-g-chain-=-g-chain-Skolem-f + (equal (ub-g-chain x) + (g-chain (Skolem-f x) x)) + :hints (("Goal" + :use ((:instance + f-chain-is-$<=$-chain-f + (x (st x)) + (i (Skolem-f x))) + (:instance + f-chain-is-$<=$-chain-f + (x (f (st x))) + (i (Skolem-f x))))))) + +(defthm + lub-f-chain=ub-g-chain + (equal (lub-f-chain x)(ub-g-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($chain$ f-chain) + (lub-$chain$ lub-f-chain) + (lub-$chain$-i lub-f-chain-i) + (lub-$chain$-nat-i lub-f-chain-nat-i) + ($f$ Skolem-f) + (shifted-$chain$ g-chain) + (ub-shifted-$chain$ ub-g-chain))) + ("Subgoal 5" + :use g-chain-$<=$-ub-g-chain) + ("Subgoal 4" + :use f-chain-is-$<=$-chain) + )) + +(defthm + generic-nested-recursive-f + (equal (f x) + (sq-if (test x) + (base x) + (f (f (st x))))) + :hints (("Goal" + :in-theory (disable lub-f-chain + ub-g-chain-=-g-chain-Skolem-f) + :use lub-f-chain=ub-g-chain))) diff --git a/books/workshops/2002/cowles-flat/support/flat-primitive.acl2 b/books/workshops/2002/cowles-flat/support/flat-primitive.acl2 new file mode 100644 index 0000000..91ba578 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-primitive.acl2 @@ -0,0 +1,6 @@ +(in-package "ACL2") +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + +(certify-book "flat-primitive" ? t) diff --git a/books/workshops/2002/cowles-flat/support/flat-primitive.lisp b/books/workshops/2002/cowles-flat/support/flat-primitive.lisp new file mode 100644 index 0000000..381ba2c --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-primitive.lisp @@ -0,0 +1,252 @@ +; Introduction of an arbitrary primitive-recursive function. +; Construction based on flat domains in ACL2. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 20 December 2001. +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-primitive" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") +#| +A construction based on flat domains in ACL2, as introduced in +flat.lisp, of a function f that satisfies the equation, for +functions h that are monotonic in their second argument, in the +following theorem, + +(defthm generic-primitive-recursive-f + (equal (f x) + (if (test x) (base x) (h x (f (st x)))))). + +The book primitive.lisp gives an alternative (and simpler) +construction of such a primitive-recursive f. +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proceed with the construction: + +(defstub + test (*) => *) + +(defstub + base (*) => *) + +(defstub + st (*) => *) + +(encapsulate + (((h * *) => *)) + + (local + (defun + h (x y) + (declare (ignore x y)) + ($bottom$))) + + (defthm + h-is-monotonic-2 + (implies ($<=$ y1 y2) + ($<=$ (h x y1)(h x y2)))) + ) ;; end encapsulate + +(defthm + h-is-monotonic-2-a + (implies (and (syntaxp (not (equal y '($bottom$)))) + (not (equal (h x ($bottom$)) ($bottom$)))) + (equal (h x y)(h x ($bottom$)))) + :hints (("Goal" + :in-theory (disable h-is-monotonic-2) + :use (:instance + h-is-monotonic-2 + (y1 ($bottom$)) + (y2 y))))) + +(defun + f-chain (i x) + (if (zp i) + ($bottom$) + (if (test x) + (base x) + (h x (f-chain (- i 1)(st x)))))) + +(defthm + base-of-f-chain=$bottom$ + (implies (zp i) + (equal (f-chain i x) + ($bottom$)))) + +(defthm + f-chain-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (f-chain i x) + (f-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of f-chain: + +(defchoose + lub-f-chain-i i (x) + (not (equal (f-chain i x) + ($bottom$)))) + +(defthm + lub-f-chain-i-rewrite + (implies (equal (f-chain (lub-f-chain-i x) x) + ($bottom$)) + (equal (f-chain i x) ($bottom$))) + :hints (("Goal" + :use lub-f-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-f-chain-nat-i (x) + (nfix (lub-f-chain-i x))) + +;; Define the least upper bound of f-chain: + +(defun + lub-f-chain (x) + (f-chain (lub-f-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-f-chain))) + +(defthm + lub-f-chain-is-upper-bound + ($<=$ (f-chain i x) + (lub-f-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))) + ("Subgoal 2" + :use f-chain-is-$<=$-chain))) + +(defun + f (x) + (lub-f-chain x)) + +(defun + g-chain (i x) + (f-chain (+ 1 i) x)) + +(defun + ub-g-chain (x) + (if (test x) + (base x) + (h x (f (st x))))) + +(defthm + g-chain-$<=$-ub-g-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (g-chain i x) + (ub-g-chain x))) + :hints (("Subgoal 2" + :in-theory (disable lub-f-chain-is-upper-bound) + :use (:instance + lub-f-chain-is-upper-bound + (x (st x)))))) + +(defun + Skolem-f (x) + (lub-f-chain-nat-i (st x))) + +(defthm + ub-g-chain-=-g-chain-Skolem-f + (equal (ub-g-chain x) + (g-chain (Skolem-f x) x))) + +(defthm + lub-f-chain=ub-g-chain + (equal (lub-f-chain x)(ub-g-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($chain$ f-chain) + (lub-$chain$ lub-f-chain) + (lub-$chain$-i lub-f-chain-i) + (lub-$chain$-nat-i lub-f-chain-nat-i) + ($f$ Skolem-f) + (shifted-$chain$ g-chain) + (ub-shifted-$chain$ ub-g-chain))) + ("Subgoal 5" + :use g-chain-$<=$-ub-g-chain) + ("Subgoal 4" + :use f-chain-is-$<=$-chain) + )) + +(defthm + generic-primitive-recursive-f + (equal (f x) + (if (test x) + (base x) + (h x (f (st x))))) + :hints (("Goal" + :use lub-f-chain=ub-g-chain))) diff --git a/books/workshops/2002/cowles-flat/support/flat-reverse.acl2 b/books/workshops/2002/cowles-flat/support/flat-reverse.acl2 new file mode 100644 index 0000000..50a9e56 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-reverse.acl2 @@ -0,0 +1,5 @@ +(in-package "ACL2") +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) +(certify-book "flat-reverse" ? t)
\ No newline at end of file diff --git a/books/workshops/2002/cowles-flat/support/flat-reverse.lisp b/books/workshops/2002/cowles-flat/support/flat-reverse.lisp new file mode 100644 index 0000000..e49dbe7 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-reverse.lisp @@ -0,0 +1,414 @@ +; Introduction of a function satisfying a slightly altered version +; of the Ashcroft recursive equation for reverse. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; Original Ashcroft recursive equation for reverse: + +; (equal (f x) +; (if (equal x nil) +; x +; (if (equal (cdr x) nil) +; x +; (let* ((a (car x)) +; (b (f (cdr x))) +; (c (car b)) +; (y (f (cdr b)))) +; (cons c (f (cons a y))))))) + +; Construction based on flat domains in ACL2. + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 28 December 2001. + +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-reverse" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") + +#| We want a function that satisfies Ashcroft's recursive + equation for reverse: + +(equal (f x) + (if (equal x nil) + x + (if (equal (cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (car b)) + (y (f (cdr b)))) + (cons c (f (cons a y))))))) +|# + + +#|| + +[Jared]: fool make_cert_help into allowing more memory for this book. + +(set-max-mem (* 6 (expt 2 30))) + +||# + +(defun + <def= (x y) + (or (eq x 'undef$) + (equal x y))) + +(defmacro + sq-if (test then else) + "Sequential version of IF." + `(if (eq ,test 'undef$) + 'undef$ + (if ,test ,then ,else))) + +(defmacro + lt-st-equal (x y) + "Left-strict version of equal." + `(if (eq ,x 'undef$) + 'undef$ + (equal ,x ,y))) + +(defmacro + st-car (x) + "Strict version of car." + `(if (eq ,x 'undef$) + 'undef$ + (car ,x))) + +(defmacro + st-cdr (x) + "Strict version of cdr." + `(if (eq ,x 'undef$) + 'undef$ + (cdr ,x))) + +(defmacro + rt-st-cons (x y) + "Right-strict version of cons." + `(if (eq ,y 'undef$) + 'undef$ + (cons ,x ,y))) + +(defmacro + st-cons (x y) + "Strict version of cons." + `(cond ((eq ,x 'undef$) 'undef$) + ((eq ,y 'undef$) 'undef$) + (t (cons ,x ,y)))) + +#| Our heuristics say it should be possible to get this: + +(equal (f x) + (if (equal x nil) + x + (sq-if (lt-st-equal (st-cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (st-car b)) + (y (f (st-cdr b)))) + (st-cons c (f (rt-st-cons a y))))))) +|# + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +(defun + f-chain (i x) + (if (zp i) + 'undef$ + (if (equal x nil) + x + (sq-if (lt-st-equal (st-cdr x) nil) + x + (let* ((a (car x)) + (b (f-chain (- i 1)(cdr x))) + (c (st-car b)) + (y (f-chain (- i 1)(st-cdr b)))) + (st-cons c (f-chain (- i 1) + (rt-st-cons a y)))))) + )) + +(defthm + base-of-f-chain=undef$ + (implies (zp i) + (equal (f-chain i x) + 'undef$))) + +(defthm + f-chain-is-<def=-chain + (implies (and (integerp i) + (>= i 0)) + (<def= (f-chain i x) + (f-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of f-chain: + +(defchoose + lub-f-chain-i i (x) + (not (equal (f-chain i x) + 'undef$))) + +(defthm + lub-f-chain-i-rewrite + (implies (equal (f-chain (lub-f-chain-i x) x) + 'undef$) + (equal (f-chain i x) 'undef$)) + :hints (("Goal" + :use lub-f-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-f-chain-nat-i (x) + (nfix (lub-f-chain-i x))) + +(in-theory (disable (:executable-counterpart + lub-f-chain-nat-i))) + +;; Define the least upper bound of f-chain: + +(defun + lub-f-chain (x) + (f-chain (lub-f-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-f-chain))) + +(defthm + lub-f-chain-is-upper-bound + (<def= (f-chain i x) + (lub-f-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))) + + ("Subgoal 2" ; changed after v4-3 from "Subgoal 3", for tau system + :use f-chain-is-<def=-chain))) + +(defthm + f-chain-is-<def=-chain-f + (implies (and (>= i (lub-f-chain-nat-i x)) + (integerp i)) + (equal (lub-f-chain x) + (f-chain i x))) + :hints (("Goal" + :by + (:functional-instance + $bottom$-based-chain-is-$<=$-chain-f + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))))) + +(defun + f (x) + (lub-f-chain x)) + +(in-theory (disable (:executable-counterpart f))) + +(defun + g-chain (i x) + (f-chain (+ 1 i) x)) + +(defun + ub-g-chain (x) + (if (equal x nil) + x + (sq-if (lt-st-equal (st-cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (st-car b)) + (y (f (st-cdr b)))) + (st-cons c (f (rt-st-cons a y))))))) + +(defthm + g-chain-<def=-ub-g-chain + (implies (and (integerp i) + (>= i 0)) + (<def= (g-chain i x) + (ub-g-chain x))) + :hints (("Subgoal 2" + :in-theory (disable lub-f-chain-is-upper-bound) + :use ((:instance + lub-f-chain-is-upper-bound + (x (rt-st-cons (car x) + (f (st-cdr (f (cdr x))))))) + (:instance + lub-f-chain-is-upper-bound + (x (st-cdr (f (cdr x))))) + (:instance + lub-f-chain-is-upper-bound + (x (cdr x))))))) + +(defun + Skolem-f (x) + (max (lub-f-chain-nat-i (cdr x)) + (max (lub-f-chain-nat-i (st-cdr (f (cdr x)))) + (lub-f-chain-nat-i (rt-st-cons + (car x) + (f (st-cdr (f (cdr x))))))))) + +(defthm + ub-g-chain-=-g-chain-Skolem-f + (equal (ub-g-chain x) + (g-chain (Skolem-f x) x)) + :hints (("Goal" + :use ((:instance + f-chain-is-<def=-chain-f + (x (cdr x)) + (i (Skolem-f x))) + (:instance + f-chain-is-<def=-chain-f + (x (st-cdr (f (cdr x)))) + (i (Skolem-f x))) + (:instance + f-chain-is-<def=-chain-f + (x (rt-st-cons + (car x) + (f (st-cdr (f (cdr x)))))) + (i (Skolem-f x))))))) + +(defthm + lub-f-chain=ub-g-chain + (equal (lub-f-chain x)(ub-g-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($<=$ <def=) + ($bottom$ (lambda () 'undef$)) + ($chain$ f-chain) + (lub-$chain$ lub-f-chain) + (lub-$chain$-i lub-f-chain-i) + (lub-$chain$-nat-i lub-f-chain-nat-i) + ($f$ Skolem-f) + (shifted-$chain$ g-chain) + (ub-shifted-$chain$ ub-g-chain))) + ("Subgoal 4" ; changed after v4-3 from "Subgoal 5", for tau system + :use g-chain-<def=-ub-g-chain) + ("Subgoal 3" ; changed after v4-3 from "Subgoal 4", for tau system + :use f-chain-is-<def=-chain) + )) + +(defthm + f-def + (equal (f x) + (if (equal x nil) + x + (sq-if (lt-st-equal (st-cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (st-car b)) + (y (f (st-cdr b)))) + (st-cons c (f (rt-st-cons a y))))))) + :hints (("Goal" + :in-theory (disable ub-g-chain-=-g-chain-Skolem-f) + :use lub-f-chain=ub-g-chain))) + +#| Recall the original Ashcroft version of a recursive equation + for reverse: + +(equal (f x) + (if (equal x nil) + x + (if (equal (cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (car b)) + (y (f (cdr b)))) + (cons c (f (cons a y))))))) +|# + +(in-theory (disable f f-def)) + +(defthm + f=Ashcroft-def + (implies (and (true-listp x) + (true-listp (f (cdr x))) + (not (equal (car (f (cdr x))) 'undef$)) + (not (equal (f (cdr (f (cdr x)))) 'undef$)) + (not (equal (f (cons (car x)(f (cdr (f (cdr x)))))) + 'undef$))) + (equal (f x) + (if (equal x nil) + x + (if (equal (cdr x) nil) + x + (let* ((a (car x)) + (b (f (cdr x))) + (c (car b)) + (y (f (cdr b)))) + (cons c (f (cons a y)))))))) + :hints (("Goal" + :use f-def))) diff --git a/books/workshops/2002/cowles-flat/support/flat-tail.acl2 b/books/workshops/2002/cowles-flat/support/flat-tail.acl2 new file mode 100644 index 0000000..5aa6492 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-tail.acl2 @@ -0,0 +1,7 @@ +(in-package "ACL2") + +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + +(certify-book "flat-tail" ? t) diff --git a/books/workshops/2002/cowles-flat/support/flat-tail.lisp b/books/workshops/2002/cowles-flat/support/flat-tail.lisp new file mode 100644 index 0000000..0ae2f5d --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-tail.lisp @@ -0,0 +1,224 @@ +; Introduction of an arbitrary tail-recursive function. +; Construction based on flat domains in ACL2. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 20 December 2001. +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-tail" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") +#| +A construction based on flat domains in ACL2, as introduced in +flat.lisp, of a function f that satisfies the equation in the +following theorem, + +(defthm generic-tail-recursive-f + (equal (f x) + (if (test x) (base x) (f (st x))))). + +As reported in defpun.lisp, Pete & J give an alternative (and +simpler) construction of such a tail-recursive f. +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proceed with the construction: + +(defstub + test (*) => *) + +(defstub + base (*) => *) + +(defstub + st (*) => *) + +(defun + f-chain (i x) + (if (zp i) + ($bottom$) + (if (test x) + (base x) + (f-chain (- i 1)(st x))))) + +(defthm + base-of-f-chain=$bottom$ + (implies (zp i) + (equal (f-chain i x) + ($bottom$)))) + +(defthm + f-chain-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (f-chain i x) + (f-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of f-chain: + +(defchoose + lub-f-chain-i i (x) + (not (equal (f-chain i x) + ($bottom$)))) + +(defthm + lub-f-chain-i-rewrite + (implies (equal (f-chain (lub-f-chain-i x) x) + ($bottom$)) + (equal (f-chain i x) ($bottom$))) + :hints (("Goal" + :use lub-f-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-f-chain-nat-i (x) + (nfix (lub-f-chain-i x))) + +;; Define the least upper bound of f-chain: + +(defun + lub-f-chain (x) + (f-chain (lub-f-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-f-chain))) + +(defthm + lub-f-chain-is-upper-bound + ($<=$ (f-chain i x) + (lub-f-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($bottom$-based-chain f-chain) + (lub-$bottom$-based-chain lub-f-chain) + (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i) + (lub-$bottom$-based-chain-i lub-f-chain-i))) + ("Subgoal 2" + :use f-chain-is-$<=$-chain))) + +(defun + f (x) + (lub-f-chain x)) + +(defun + g-chain (i x) + (f-chain (+ 1 i) x)) + +(defun + ub-g-chain (x) + (if (test x) + (base x) + (f (st x)))) + +(defthm + g-chain-$<=$-ub-g-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (g-chain i x) + (ub-g-chain x))) + :hints (("Subgoal 2" + :in-theory (disable lub-f-chain-is-upper-bound) + :use (:instance + lub-f-chain-is-upper-bound + (x (st x)))))) + +(defun + Skolem-f (x) + (lub-f-chain-nat-i (st x))) + +(defthm + ub-g-chain-=-g-chain-Skolem-f + (equal (ub-g-chain x) + (g-chain (Skolem-f x) x))) + +(defthm + lub-f-chain=ub-g-chain + (equal (lub-f-chain x)(ub-g-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($chain$ f-chain) + (lub-$chain$ lub-f-chain) + (lub-$chain$-i lub-f-chain-i) + (lub-$chain$-nat-i lub-f-chain-nat-i) + ($f$ Skolem-f) + (shifted-$chain$ g-chain) + (ub-shifted-$chain$ ub-g-chain))) + ("Subgoal 5" + :use g-chain-$<=$-ub-g-chain) + ("Subgoal 4" + :use f-chain-is-$<=$-chain) + )) + +(defthm + generic-tail-recursive-f + (equal (f x) + (if (test x) + (base x) + (f (st x)))) + :hints (("Goal" + :use lub-f-chain=ub-g-chain))) diff --git a/books/workshops/2002/cowles-flat/support/flat-z.acl2 b/books/workshops/2002/cowles-flat/support/flat-z.acl2 new file mode 100644 index 0000000..ba556e5 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-z.acl2 @@ -0,0 +1,8 @@ +(in-package "ACL2") + +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + +(certify-book "flat-z" ? t) + diff --git a/books/workshops/2002/cowles-flat/support/flat-z.lisp b/books/workshops/2002/cowles-flat/support/flat-z.lisp new file mode 100644 index 0000000..be21c72 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat-z.lisp @@ -0,0 +1,261 @@ +; Introduction of the partial function Z defined by +; (Z x) <== (if (equal x 0) +; 0 +; (* (Z (- x 1))(Z (+ x 1)))). +; Construction based on flat domains in ACL2. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 28 December 2001. +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat-z" 1 nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +(include-book "flat") +#| +A construction based on flat domains in ACL2, as introduced in +flat.lisp, of a function Z that satisfies the equation, + + (equal (Z x) + (if (equal x 0) + 0 + (* (Z (- x 1))(Z (+ x 1)))). +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proceed with the construction: + +;; Zero plays the part of ($bottom$) + +(defun + $0<=$ (x y) + (or (equal x 0) + (equal x y))) + +(defun + Z-chain (i x) + (if (zp i) + 0 + (if (equal x 0) + 0 + (* (Z-chain (- i 1)(- x 1)) + (Z-chain (- i 1)(+ x 1)))))) + +(defthm + base-of-Z-chain=0 + (implies (zp i) + (equal (Z-chain i x) + 0))) + +(defthm + Z-chain-is-$0<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($0<=$ (Z-chain i x) + (Z-chain (+ 1 i) x)))) + +;; Choose an ``index'' for definition of lub of Z-chain: + +(defchoose + lub-Z-chain-i i (x) + (not (equal (Z-chain i x) + 0))) + +(defthm + lub-Z-chain-i-rewrite + (implies (equal (Z-chain (lub-Z-chain-i x) x) + 0) + (equal (Z-chain i x) 0)) + :hints (("Goal" + :use lub-Z-chain-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-Z-chain-nat-i (x) + (nfix (lub-Z-chain-i x))) + +;; Define the least upper bound of f-chain: + +(defun + lub-Z-chain (x) + (Z-chain (lub-Z-chain-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-Z-chain))) + +(defthm + lub-Z-chain-is-upper-bound + ($0<=$ (Z-chain i x) + (lub-Z-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($bottom$ (lambda () 0)) + ($<=$ $0<=$) + ($bottom$-based-chain Z-chain) + (lub-$bottom$-based-chain lub-Z-chain) + (lub-$bottom$-based-chain-nat-i lub-Z-chain-nat-i) + (lub-$bottom$-based-chain-i lub-Z-chain-i))) + ("Subgoal 2" + :use Z-chain-is-$0<=$-chain))) + +(defthm + Z-chain-is-$0<=$-chain-f + (implies (and (>= i (lub-Z-chain-nat-i x)) + (integerp i)) + (equal (lub-Z-chain x) + (Z-chain i x))) + :hints (("Goal" + :by + (:functional-instance + $bottom$-based-chain-is-$<=$-chain-f + ($bottom$ (lambda () 0)) + ($<=$ $0<=$) + ($bottom$-based-chain Z-chain) + (lub-$bottom$-based-chain lub-Z-chain) + (lub-$bottom$-based-chain-nat-i lub-Z-chain-nat-i) + (lub-$bottom$-based-chain-i lub-Z-chain-i))))) + +(defun + Z (x) + (lub-Z-chain x)) + +(defun + g-chain (i x) + (Z-chain (+ 1 i) x)) + +(defun + ub-g-chain (x) + (if (equal x 0) + 0 + (* (Z (- x 1)) + (Z (+ x 1))))) + +(defthm + g-chain-$0<=$-ub-g-chain + (implies (and (integerp i) + (>= i 0)) + ($0<=$ (g-chain i x) + (ub-g-chain x))) + :hints (("Subgoal 2" + :in-theory (disable lub-Z-chain-is-upper-bound) + :use ((:instance + lub-Z-chain-is-upper-bound + (x (- x 1))) + (:instance + lub-Z-chain-is-upper-bound + (x (+ x 1))))))) + +(defun + Skolem-Z (x) + (max (lub-Z-chain-nat-i (- x 1)) + (lub-Z-chain-nat-i (+ x 1)))) + +(defthm + ub-g-chain-=-g-chain-Skolem-Z + (equal (ub-g-chain x) + (g-chain (Skolem-Z x) x)) + :hints (("Goal" + :use ((:instance + Z-chain-is-$0<=$-chain-f + (x (- x 1)) + (i (Skolem-Z x))) + (:instance + Z-chain-is-$0<=$-chain-f + (x (+ x 1)) + (i (Skolem-Z x))))))) + +(defthm + lub-Z-chain=ub-g-chain + (equal (lub-Z-chain x)(ub-g-chain x)) + :rule-classes nil + :hints (("Goal" + :by + (:functional-instance + lub-$chain$=ub-shifted-$chain$ + ($bottom$ (lambda () 0)) + ($<=$ $0<=$) + ($chain$ Z-chain) + (lub-$chain$ lub-Z-chain) + (lub-$chain$-i lub-Z-chain-i) + (lub-$chain$-nat-i lub-Z-chain-nat-i) + ($f$ Skolem-Z) + (shifted-$chain$ g-chain) + (ub-shifted-$chain$ ub-g-chain))) + ("Subgoal 5" + :use g-chain-$0<=$-ub-g-chain) + ("Subgoal 4" + :use Z-chain-is-$0<=$-chain) + )) + +(defthm + Z-axiom + (equal (Z x) + (if (equal x 0) + 0 + (* (Z (- x 1)) + (Z (+ x 1))))) + :hints (("Goal" + :in-theory (disable lub-Z-chain + ub-g-chain-=-g-chain-Skolem-Z) + :use lub-Z-chain=ub-g-chain))) diff --git a/books/workshops/2002/cowles-flat/support/flat.acl2 b/books/workshops/2002/cowles-flat/support/flat.acl2 new file mode 100644 index 0000000..0c5aaa0 --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat.acl2 @@ -0,0 +1,7 @@ +(in-package "ACL2") + +(defpkg "FLAT" + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + +(certify-book "flat" ? t) diff --git a/books/workshops/2002/cowles-flat/support/flat.lisp b/books/workshops/2002/cowles-flat/support/flat.lisp new file mode 100644 index 0000000..70fa15e --- /dev/null +++ b/books/workshops/2002/cowles-flat/support/flat.lisp @@ -0,0 +1,1387 @@ +; The ACL2 FLat Domain Book. +; Copyright (C) 2001 John R. Cowles, University of Wyoming + +; This book 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 book 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 book; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: +; John Cowles +; Department of Computer Science +; University of Wyoming +; Laramie, WY 82071-3682 U.S.A. + +; Fall 2001. +; Last modified 20 December 2001. +#| + To certify (originally in ACL2 Version 2.6): + (defpkg + "FLAT" (union-eq + *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + + (certify-book "flat" + 1 + nil ; compile-flg + :defaxioms-okp nil + :skip-proofs-okp nil) +|# +(in-package "FLAT") +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Add some basic arithmetic facts: + +(local + (defthm + commutativity-2-of-+ + (equal (+ x y z) + (+ y x z)))) + +(local + (defthm + associate-constants-left-+ + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep y))) + (equal (+ x (+ y z)) + (+ (+ x y) z))))) + +(local + (defthm + minus-inverse-+-a + (implies (acl2-numberp y) + (equal (+ (- x) x y) + y)))) + +(local + (defthm + minus-inverse-+-b + (implies (acl2-numberp y) + (equal (+ x (- x) y) + y)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Formalize a flat domain: + +;; Impose a partial order on ACL2 data: +;; Specify a least element, ($bottom$), in this +;; partial order. Thus ($bottom$) is strictly +;; less than any other ACL2 datum. +;; No other data items are related by this strict +;; partial order. Hence, the name ``flat'' comes +;; from the standard graph of this order: + +;; ACL2 flat data: o o .... o o +;; \ | | / +;; \ | | / +;; ($bottom$) + +;; Items (represented by nodes) related by this +;; strict partial order are connected by edges. +;; In what follows, the reflexive closure, of this +;; strict partial order, is denoted by $<=$. +;; ACL2 is used to verify that $<=$ is a reflexive +;; partial order: +(defstub + $bottom$ () => *) + +(defun + $<=$ (x y) + (or (equal x ($bottom$)) + (equal x y))) + +;; $<=$ is a reflexive partial order on the ACL2 +;; universe: +#| +(thm ;; Reflexive + ($<=$ x x)) + +(thm ;; Antisymmetric + (implies (and ($<=$ x y) + ($<=$ y x)) + (equal x y))) + +(thm ;; Transitive + (implies (and ($<=$ x y) + ($<=$ y z)) + ($<=$ x z))) +|# +;; For each positive integer, n, the partial order +;; $<=$ is extended elementwise to functions with +;; n arguments, x_1,...,x_n: +;; For functions $f$ and $g$, +;; ($<=$ $f$ $g$) iff (for all x_1,...,x_n) +;; ($<=$ ($f$ x_1 ... x_n) +;; ($g$ x_1 ... x_n)). +;; +;; Extended this way, $<=$ is a reflexive partial +;; order on functions, with n arguments, with a +;; least element, $bottom-n$. $Bottom-n$ is the +;; constant function, with n arguments, that always +;; returns the constant ($bottom$). +;; ACL2 is used to verify the above claims about +;; about n-ary functions for n = 1. +#| +(defstub + $f$ (*) => *) + +(thm ;; Reflexive + ($<=$ ($f$ x)($f$ x))) + +(defun + $bottom-1$ (x) + (declare (ignore x)) + ($bottom$)) + +(thm ;; Least unary function. + ($<=$ ($bottom-1$ x) + ($f$ x))) +:ubt :x-1 +(encapsulate + ;; Antisymmetric: + ;; For functions $f$ and $g$, + ;; (implies (and ($<=$ $f$ $g$) + ;; ($<=$ $g$ $f$)) + ;; (equal $f$ $g$))) + ((($f$ *) => *) + (($g$ *) => *)) + + (local + (defun + $f$ (x) + (declare (ignore x)) + ($bottom$))) + + (local + (defun + $g$ (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + $f$-$<=$-$g$ + ($<=$ ($f$ x)($g$ x)) + :rule-classes nil) + + (defthm + $g$-$<=$-$f$ + ($<=$ ($g$ x)($f$ x)) + :rule-classes nil) + ) ;; end encapsulate + +(thm ;; Antisymmetric: + (equal ($f$ x)($g$ x)) + :hints (("Goal" + :use ($f$-$<=$-$g$ + $g$-$<=$-$f$)))) +:ubt :x +(encapsulate + ;; Transitive: + ;; For functions $f$, $g$, and $h$, + ;; (implies (and ($<=$ $f$ $g$) + ;; ($<=$ $g$ $h$)) + ;; (equal $f$ $h$))) + ((($f$ *) => *) + (($g$ *) => *) + (($h$ *) => *)) + + (local + (defun + $f$ (x) + (declare (ignore x)) + ($bottom$))) + + (local + (defun + $g$ (x) + (declare (ignore x)) + ($bottom$))) + + (local + (defun + $h$ (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + $f$-$<=$-$g$ + ($<=$ ($f$ x)($g$ x)) + :rule-classes nil) + + (defthm + $g$-$<=$-$h$ + ($<=$ ($g$ x)($h$ x)) + :rule-classes nil) + ) ;; end encapsulate + +(thm ;; Transitive: + ($<=$ ($f$ x)($h$ x)) + :hints (("Goal" + :use ($f$-$<=$-$g$ + $g$-$<=$-$h$)))) +:ubt :x +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize functions $f$1 and $f$2 such that ($<=$ $f$1 $f$2). +;; Prove some theorems about $f$1 $f$2. + +(encapsulate + ((($f$1 *) => *) + (($f$2 *) => *)) + + (local + (defun + $f$1 (x) + (declare (ignore x)) + ($bottom$))) + + (local + (defun + $f$2 (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + $f$1-$<=$-$f$2 + ($<=$ ($f$1 x)($f$2 x)) + :rule-classes nil) + ) ;; end encapsulate + +(defthm + $f$1-$<=$-$f$2-a + (implies (equal ($f$2 x) ($bottom$)) + (equal ($f$1 x) ($bottom$))) + :hints (("Goal" + :use $f$1-$<=$-$f$2))) + +(defthm + $f$1-$<=$-$f$2-b + (implies (not (equal ($f$1 x) ($bottom$))) + (equal ($f$2 x)($f$1 x))) + :hints (("Goal" + :use $f$1-$<=$-$f$2))) + +(defthm + $f$1-$<=$-$f$2-c + (implies (and (equal ($f$1 x) y) + (not (equal y ($bottom$)))) + (equal ($f$2 x)($f$1 x)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize various situations involving unary +;; functions indexed by nonnegative integers: +;; f_0, f_1, ..., f_i, ... . +;; Indexed functions are formalized in ACL2 by +;; treating the index as an argument to the +;; function. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize a $<=$ upper-bound of an indexed set +;; of functions: + +(encapsulate + (((f$1 * *) => *) + ((ub-f$1 *) => *)) + + (local + (defun + f$1 (i x) + (declare (ignore i x)) + ($bottom$))) + + (local + (defun + ub-f$1 (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + f$1-$<=$-ub-f$1 + ($<=$ (f$1 i x)(ub-f$1 x)) + :rule-classes nil) + ) ;; end encapsulate + +(defthm + f$1-$<=$-ub-f$1-a + (implies (equal (ub-f$1 x)($bottom$)) + (equal (f$1 i x)($bottom$))) + :hints (("Goal" + :use f$1-$<=$-ub-f$1))) + +(defthm + f$1-$<=$-ub-f$1-b + (implies (not (equal (f$1 i x)($bottom$))) + (equal (ub-f$1 x)(f$1 i x))) + :hints (("Goal" + :use f$1-$<=$-ub-f$1))) + +(defthm + f$1-$<=$-ub-f$1-c + (implies (and (equal (f$1 i x) y) + (not (equal y ($bottom$)))) + (equal (ub-f$1 x)(f$1 i x)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize a $<=$-chain of functions with +;; ($bottom$) base: + +(encapsulate + ((($bottom$-based-chain * *) => *)) + + (local + (defun + $bottom$-based-chain (i x) + (declare (ignore i x)) + ($bottom$))) + + (defthm + base-of-$bottom$-based-chain=$bottom$ + (implies (zp i) + (equal ($bottom$-based-chain i x) + ($bottom$)))) + + (defthm + $bottom$-based-chain-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ ($bottom$-based-chain i x) + ($bottom$-based-chain (+ 1 i) + x)))) + ) ;; end encapsulate + +(defthm + $bottom$-based-chain-i>0 + (implies (not (equal ($bottom$-based-chain i x) + ($bottom$))) + (> i 0)) + :rule-classes (:forward-chaining + :rewrite)) + +(defun + induct-nat (x) + (if (zp x) + t + (induct-nat (- x 1)))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-a + (implies (and (integerp j) + (>= j 0)) + ($<=$ ($bottom$-based-chain i x) + ($bottom$-based-chain (+ i j) x))) + :hints (("Goal" + :induct (induct-nat j)) + ("Subgoal *1/2" + :use (:instance + $bottom$-based-chain-is-$<=$-chain + (i (+ -1 i j)))))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-b + (implies (and (equal ($bottom$-based-chain + (+ i j) + x) + ($bottom$)) + (integerp j) + (>= j 0)) + (equal ($bottom$-based-chain i x) + ($bottom$))) + :hints (("Goal" + :use + $bottom$-based-chain-is-$<=$-chain-a))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-c + (implies (and (integerp j) + (>= j 0) + (not (equal + ($bottom$-based-chain i x) + ($bottom$)))) + (equal ($bottom$-based-chain (+ i j) x) + ($bottom$-based-chain i x))) + :hints (("Goal" + :in-theory + (disable + $bottom$-based-chain-is-$<=$-chain-a) + :use + $bottom$-based-chain-is-$<=$-chain-a))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-d + (implies (and (not (equal + ($bottom$-based-chain i x) + ($bottom$))) + (integerp i) + (integerp j) + (>= j i)) + (equal ($bottom$-based-chain i x) + ($bottom$-based-chain j x))) + :rule-classes nil + :hints (("Goal" + :in-theory + (disable + $bottom$-based-chain-is-$<=$-chain-c) + :use + (:instance + $bottom$-based-chain-is-$<=$-chain-c + (j (- j i)))))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-e + (implies (and (not (equal + ($bottom$-based-chain i x) + ($bottom$))) + (not (equal + ($bottom$-based-chain j x) + ($bottom$)))) + (equal ($bottom$-based-chain i x) + ($bottom$-based-chain j x))) + :rule-classes nil + :hints (("Goal" + :use + ($bottom$-based-chain-is-$<=$-chain-d + (:instance + $bottom$-based-chain-is-$<=$-chain-d + (i j) + (j i)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Choose an ``index'' for definition of lub of +;; $bottom$-based-chain: + +(defchoose + lub-$bottom$-based-chain-i i (x) + (not (equal ($bottom$-based-chain i x) + ($bottom$)))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-$bottom$-based-chain-nat-i (x) + (nfix (lub-$bottom$-based-chain-i x))) + +(defthm + lub-$bottom$-based-chain-nat-i-rewrite + (implies (equal + ($bottom$-based-chain + (lub-$bottom$-based-chain-nat-i x) + x) + ($bottom$)) + (equal + ($bottom$-based-chain i x)($bottom$))) + :hints (("Goal" + :use lub-$bottom$-based-chain-i))) + +(in-theory (disable + lub-$bottom$-based-chain-nat-i + (:executable-counterpart + lub-$bottom$-based-chain-nat-i))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Define the least upper bound of +;; $bottom$-based-chain: + +(defun + lub-$bottom$-based-chain (x) + ($bottom$-based-chain + (lub-$bottom$-based-chain-nat-i x) + x)) + +(in-theory (disable (:executable-counterpart + lub-$bottom$-based-chain))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; lub-$bottom$-based-chain is upper bound of +;; $bottom$-based-chain: + +(defthm + lub-$bottom$-based-chain-is-upper-bound + ($<=$ ($bottom$-based-chain i x) + (lub-$bottom$-based-chain x)) + :hints (("Goal" + :use + (:instance + $bottom$-based-chain-is-$<=$-chain-e + (j (lub-$bottom$-based-chain-nat-i x)) + )))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Show lub-$bottom$-based-chain is LEAST upper bound +;; of $bottom$-based-chain: + +;; Axiomatize an upper bound of +;; $bottom$-based-chain: + +(encapsulate + (((ub-$bottom$-based-chain *) => *)) + + (local + (defun + ub-$bottom$-based-chain (x) + (lub-$bottom$-based-chain x))) + + (defthm + ub-$bottom$-based-chain-is-upper-bound + ($<=$ ($bottom$-based-chain i x) + (ub-$bottom$-based-chain x))) + ) ;; end encapsulate + +(defthm + lub-$bottom$-based-chain-is-LEAST-upper-bound + ($<=$ (lub-$bottom$-based-chain x) + (ub-$bottom$-based-chain x)) + :hints (("Goal" + :in-theory + (disable + ub-$bottom$-based-chain-is-upper-bound) + :use + (:instance + ub-$bottom$-based-chain-is-upper-bound + (i (lub-$bottom$-based-chain-nat-i x)) + )))) + +(defthm + $bottom$-based-chain-is-$<=$-chain-f + (implies (and + (>= i + (lub-$bottom$-based-chain-nat-i x)) + (integerp i)) + (equal + (lub-$bottom$-based-chain x) + ($bottom$-based-chain i x))) + :hints (("Goal" + :use + (:instance + $bottom$-based-chain-is-$<=$-chain-d + (i (lub-$bottom$-based-chain-nat-i x)) + (j i))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize a $<=$-chain of functions (possibly +;; without $bottom$ base): + +(encapsulate + (((chain$ * *) => *)) + + (local + (defun + chain$ (i x) + (declare (ignore i x)) + ($bottom$))) + + (defthm + chain$-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (chain$ i x) + (chain$ (+ 1 i) x)))) + ) ;; end encapsulate + +;; Extend chain$ by adding an $bottom$ base: + +(defun + chain$+$bottom$-base (i x) + (if (zp i) + ($bottom$) + (chain$ (- i 1) x))) + +;; Choose an ``index'' for definition of lub of +;; chain$: + +(defchoose + lub-chain$-i i (x) + (not (equal (chain$+$bottom$-base i x) + ($bottom$)))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-chain$-nat-i (x) + (nfix (lub-chain$-i x))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Define the least upper bound of chain$: + +(defun + lub-chain$ (x) + (chain$+$bottom$-base (lub-chain$-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-chain$))) + +;; lub-chain$ is upper bound of chain$+$bottom$-base: + +(defthm + lub-chain$-is-upper-bound-chain$+$bottom$-base + ($<=$ (chain$+$bottom$-base i x)(lub-chain$ x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-upper-bound + ($bottom$-based-chain + chain$+$bottom$-base) + (lub-$bottom$-based-chain lub-chain$) + (lub-$bottom$-based-chain-nat-i + lub-chain$-nat-i) + (lub-$bottom$-based-chain-i + lub-chain$-i))) + ("Subgoal 3" + :use lub-chain$-i) + ("Subgoal 2" + :use (:instance + chain$-is-$<=$-chain + (i (- i 1)))))) + +;; lub-chain$ is upper bound of chain$: + +(defthm + lub-chain$-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (chain$ i x)(lub-chain$ x))) + :hints + (("Goal" + :in-theory + (disable + lub-chain$-is-upper-bound-chain$+$bottom$-base) + :use + (:instance + lub-chain$-is-upper-bound-chain$+$bottom$-base + (i (+ i 1)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Show lub-chain$ is LEAST upper bound of chain$: + +;; Axiomatize an upper bound of chain$: + +(encapsulate + (((ub-chain$ *) => *)) + + (local + (defun + ub-chain$ (x) + (lub-chain$ x))) + + (defthm + ub-chain$-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (chain$ i x)(ub-chain$ x))) + :hints (("Goal" + :in-theory + (disable $<=$ lub-chain$)))) + ) ;; end encapsulate + +(defthm + lub-chain$-is-LEAST-upper-bound + ($<=$ (lub-chain$ x)(ub-chain$ x)) + :hints (("Goal" + :in-theory + (disable ub-chain$-is-upper-bound) + :use (:instance + ub-chain$-is-upper-bound + (i (- (lub-chain$-nat-i x) 1)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ($Bottom$-based-chain (+ i 1) x) is a chain with +;; same lub as ($bottom$-based-chain i x): + +(encapsulate + (((shifted$-chain * *) => *)) + + (local + (defun + shifted$-chain (i x) + ($bottom$-based-chain (+ i 1) x))) + + (defthm + shifted$-chain-rewrite + (implies (and (integerp i) + (>= i 0)) + (equal (shifted$-chain i x) + ($bottom$-based-chain (+ 1 i) + x)))) + ) ;; end encapsulate + +(defthm + shifted$-chain-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted$-chain i x) + (shifted$-chain (+ 1 i) x))) + :hints (("Goal" + :use + (:instance + $bottom$-based-chain-is-$<=$-chain + (i (+ i 1)))))) + +;; Extend shifted$-chain by adding an $bottom$ base: + +(defun + shifted$-chain+$bottom$-base (i x) + (if (zp i) + ($bottom$) + (shifted$-chain (- i 1) x))) + +;; Choose an ``index'' for definition of lub of +;; shifted$-chain: + +(defchoose + lub-shifted$-chain-i i (x) + (not (equal (shifted$-chain+$bottom$-base i x) + ($bottom$)))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-shifted$-chain-nat-i (x) + (nfix (lub-shifted$-chain-i x))) + +;; Define the least upper bound of shifted-chain: + +(defun + lub-shifted$-chain (x) + (shifted$-chain+$bottom$-base + (lub-shifted$-chain-nat-i x) + x)) + +(in-theory (disable (:executable-counterpart + lub-shifted$-chain))) + +(defthm + lub-shifted$-chain-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted$-chain i x) + (lub-shifted$-chain x))) + :hints (("Goal" + :by (:functional-instance + lub-chain$-is-upper-bound + (chain$ shifted$-chain) + (chain$+$bottom$-base + shifted$-chain+$bottom$-base) + (lub-chain$ lub-shifted$-chain) + (lub-chain$-nat-i + lub-shifted$-chain-nat-i) + (lub-chain$-i + lub-shifted$-chain-i))) + ("Subgoal 3" + :use lub-shifted$-chain-i) + ("Subgoal 1" + :use (:instance + $bottom$-based-chain-is-$<=$-chain + (i (+ i 1)))))) + +(defthm + lub-shifted$-chain-is-upper-bound-of-$bottom$-based-chain-lemma + (implies (and (integerp i) + (> i 0)) + ($<=$ ($bottom$-based-chain i x) + (lub-shifted$-chain x))) + :hints (("Goal" + :use (:instance + lub-shifted$-chain-is-upper-bound + (i (- i 1)))))) + +(defthm + $<=$-$bottom$ + ($<=$ ($bottom$) x)) + +(defthm + lub-shifted$-chain-is-upper-bound-of-$bottom$-based-chain + ($<=$ ($bottom$-based-chain i x) + (lub-shifted$-chain x)) + :hints (("Goal" + :in-theory + (disable $<=$ lub-shifted$-chain) + :cases ((zp i))))) + +(defthm + lub-$bottom$-based-chain-is-upper-bound-of-shifted$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted$-chain i x) + (lub-$bottom$-based-chain x))) + :hints (("Goal" + :in-theory + (disable $<=$ + lub-$bottom$-based-chain)))) + +(defthm + lub-$bottom$-based-chain-$<=$-lub-shifted$-chain + ($<=$ (lub-$bottom$-based-chain x) + (lub-shifted$-chain x)) + :hints (("Goal" + :by + (:functional-instance + lub-$bottom$-based-chain-is-LEAST-upper-bound + (ub-$bottom$-based-chain + lub-shifted$-chain))))) + +(defthm + lub-shifted$-chain-$<=$-lub-$bottom$-based-chain + ($<=$ (lub-shifted$-chain x) + (lub-$bottom$-based-chain x)) + :hints (("Goal" + :in-theory + (disable $<=$ + lub-$bottom$-based-chain) + :by (:functional-instance + lub-chain$-is-LEAST-upper-bound + (ub-chain$ + lub-$bottom$-based-chain) + (chain$ shifted$-chain) + (chain$+$bottom$-base + shifted$-chain+$bottom$-base) + (lub-chain$ lub-shifted$-chain) + (lub-chain$-nat-i + lub-shifted$-chain-nat-i) + (lub-chain$-i + lub-shifted$-chain-i))) + ("Subgoal 2" + :use lub-shifted$-chain-i))) + +(defthm + lub-shifted$-chain-=-lub-$bottom$-based-chain + (equal (lub-shifted$-chain x) + (lub-$bottom$-based-chain x)) + :hints (("Goal" + :in-theory + (disable lub-shifted$-chain + lub-$bottom$-based-chain) + :use (:instance + (:theorem + (implies (and ($<=$ x y) + ($<=$ y x)) + (equal x y))) + (x (lub-$bottom$-based-chain x)) + (y (lub-shifted$-chain x)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize a function ($f$ x) and a $<=$-chain, +;; ($chain$ i x), of functions with $bottom$ base +;; such that the shifted version of the chain, +;; (shifted-$chain$ i x), has an upper bound, +;; (ub-shifted-$chain$ x), with the property that +;; for all x, (equal (ub-shifted-$chain$ x) +;; (shifted-$chain$ ($f$ x) x)): + +(encapsulate + ((($chain$ * *) => *) + (($f$ *) => *) + ((shifted-$chain$ * *) => *) + ((ub-shifted-$chain$ *) => *)) + + (local + (defun + $chain$ (i x) + (declare (ignore i x)) + ($bottom$))) + + (defthm + base-of-$chain$=$bottom$ + (implies (zp i) + (equal ($chain$ i x) + ($bottom$)))) + + (defthm + $chain$-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ ($chain$ i x) + ($chain$ (+ 1 i) x)))) + + (local + (defun + shifted-$chain$ (i x) + ($chain$ (+ 1 i) x))) + + (defthm + shifted-$chain$=$chain$ + (implies (and (integerp i) + (>= i 0)) + (equal (shifted-$chain$ i x) + ($chain$ (+ 1 i) x)))) + + (local + (defun + ub-shifted-$chain$ (x) + (declare (ignore x)) + ($bottom$))) + + (defthm + shifted-$chain$-$<=$-ub-shifted-$chain$ + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted-$chain$ i x) + (ub-shifted-$chain$ x)))) + + (local + (defun + $f$ (x) + (declare (ignore x)) + 0)) + + (defthm + nat-$f$ + (and (integerp ($f$ x)) + (>= ($f$ x) 0)) + :rule-classes :type-prescription) + + (defthm + ub-shifted-$chain$-=-shifted-$chain$-$f$ + (equal (ub-shifted-$chain$ x) + (shifted-$chain$ ($f$ x) x))) + ) ;; end encapsulate + +(defthm + shifted-$chain$-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted-$chain$ i x) + (shifted-$chain$ (+ 1 i) x))) + :hints (("Goal" + :use (:instance + $chain$-is-$<=$-chain + (i (+ 1 i)))))) + +;; Choose an ``index'' for definition of lub of +;; $chain$: + +(defchoose + lub-$chain$-i i (x) + (not (equal ($chain$ i x) + ($bottom$)))) + +(defthm + lub-$chain$-i-rewrite + (implies (equal ($chain$ (lub-$chain$-i x) x) + ($bottom$)) + (equal ($chain$ i x) ($bottom$))) + :hints (("Goal" + :use lub-$chain$-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-$chain$-nat-i (x) + (nfix (lub-$chain$-i x))) + +;; Define the least upper bound of $chain$: + +(defun + lub-$chain$ (x) + ($chain$ (lub-$chain$-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-$chain$))) + +;; Extend shifted-$chain$ by adding an $bottom$ base: + +(defun + shifted-$chain$+$bottom$-base (i x) + (if (zp i) + ($bottom$) + (shifted-$chain$ (- i 1) x))) + +(defthm + shifted-$chain$+$bottom$-base-rewrite + (and (implies (zp i) + (equal + (shifted-$chain$+$bottom$-base i + x) + ($bottom$))) + (implies (not (zp i)) + (equal + (shifted-$chain$+$bottom$-base i + x) + (shifted-$chain$ (- i 1) x))))) + +;; Choose an ``index'' for definition of lub of +;; shifted-$chain$: + +(defchoose + lub-shifted-$chain$-i i (x) + (not (equal (shifted-$chain$+$bottom$-base i x) + ($bottom$)))) + +(defthm + lub-shifted-$chain$-i-rewrite + (implies (equal (shifted-$chain$+$bottom$-base + (lub-shifted-$chain$-i x) x) + ($bottom$)) + (equal (shifted-$chain$+$bottom$-base i + x) + ($bottom$))) + :hints (("Goal" + :use lub-shifted-$chain$-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-shifted-$chain$-nat-i (x) + (nfix (lub-shifted-$chain$-i x))) + +;; Define the least upper bound of shifted-$chain$: + +(defun + lub-shifted-$chain$ (x) + (shifted-$chain$+$bottom$-base + (lub-shifted-$chain$-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-shifted-$chain$))) + +(defthm + lub-shifted-$chain$-=-lub-$chain$ + (equal (lub-shifted-$chain$ x)(lub-$chain$ x)) + :rule-classes nil + :hints (("Goal" + :in-theory + (disable $<=$ + shifted-$chain$+$bottom$-base) + :by + (:functional-instance + lub-shifted$-chain-=-lub-$bottom$-based-chain + (lub-shifted$-chain + lub-shifted-$chain$) + (lub-$bottom$-based-chain lub-$chain$) + ($bottom$-based-chain $chain$) + (lub-$bottom$-based-chain-i + lub-$chain$-i) + (lub-$bottom$-based-chain-nat-i + lub-$chain$-nat-i) + (shifted$-chain shifted-$chain$) + (shifted$-chain+$bottom$-base + shifted-$chain$+$bottom$-base) + (lub-shifted$-chain-i + lub-shifted-$chain$-i) + (lub-shifted$-chain-nat-i + lub-shifted-$chain$-nat-i))))) + +(defthm + lub-shifted-$chain$-$<=$-ub-shifted-$chain$ + ($<=$ (lub-shifted-$chain$ x) + (ub-shifted-$chain$ x)) + :hints (("Goal" + :in-theory + (disable + $<=$ shifted-$chain$=$chain$ + shifted-$chain$+$bottom$-base + ub-shifted-$chain$-=-shifted-$chain$-$f$) + :by (:functional-instance + lub-chain$-is-LEAST-upper-bound + (ub-chain$ ub-shifted-$chain$) + (chain$ shifted-$chain$) + (chain$+$bottom$-base + shifted-$chain$+$bottom$-base) + (lub-chain$ lub-shifted-$chain$) + (lub-chain$-nat-i + lub-shifted-$chain$-nat-i) + (lub-chain$-i + lub-shifted-$chain$-i))))) + +(defthm + lub-shifted-$chain$-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (shifted-$chain$ i x) + (lub-shifted-$chain$ x))) + :hints (("Goal" + :in-theory + (disable shifted-$chain$+$bottom$-base) + :by (:functional-instance + lub-shifted$-chain-is-upper-bound + (shifted$-chain shifted-$chain$) + (shifted$-chain+$bottom$-base + shifted-$chain$+$bottom$-base) + (lub-shifted$-chain + lub-shifted-$chain$) + (lub-shifted$-chain-i + lub-shifted-$chain$-i) + (lub-shifted$-chain-nat-i + lub-shifted-$chain$-nat-i) + ($bottom$-based-chain $chain$))))) + +(defthm + ub-shifted-$chain$-$<=$-lub-shifted-$chain$ + ($<=$ (ub-shifted-$chain$ x) + (lub-shifted-$chain$ x)) + :hints (("Goal" + :in-theory + (disable $<=$ shifted-$chain$=$chain$ + lub-shifted-$chain$)))) + +(defthm + ub-shifted-$chain$=lub-shifted-$chain$ + (equal (ub-shifted-$chain$ x) + (lub-shifted-$chain$ x)) + :rule-classes nil + :hints (("Goal" + :in-theory (disable lub-shifted-$chain$) + :use (:instance + (:theorem + (implies (and ($<=$ x y) + ($<=$ y x)) + (equal x y))) + (x (ub-shifted-$chain$ x)) + (y (lub-shifted-$chain$ x)))))) + +(defthm + lub-$chain$=ub-shifted-$chain$ + (equal (lub-$chain$ x)(ub-shifted-$chain$ x)) + :rule-classes nil + :hints (("Goal" + :in-theory (disable lub-$chain$ + lub-shifted-$chain$) + :use + (ub-shifted-$chain$=lub-shifted-$chain$ + lub-shifted-$chain$-=-lub-$chain$)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; An unary function f is said to be monotonic (with +;; respect to $<=$) just in case for all x and y, +;; ($<=$ x y) implies ($<=$ (f x)(f y)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Axiomatize a $<=$-chain of monotonic functions: + +(encapsulate + (((mono-chain$ * *) => *)) + + (local + (defun + mono-chain$ (i x) + (declare (ignore i x)) + ($bottom$))) + + (defthm + mono-chain$-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (mono-chain$ i x) + (mono-chain$ (+ 1 i) x)))) + + (defthm + mono-chain$-is-chain-of-monotonic-functions + (implies ($<=$ x y) + ($<=$ (mono-chain$ i x) + (mono-chain$ i y)))) + ) ;; end encapsulate + +;; Monotonic unary functions either preserve +;; ($bottom$) or are constant. Functions that +;; preserve ($bottom$) are called strict. + +(defthm + mono-chain$-is-chain-of-monotonic-functions-a + (or (equal (mono-chain$ i ($bottom$))($bottom$)) + (equal (mono-chain$ i x) + (mono-chain$ i ($bottom$)))) + :rule-classes nil + :hints + (("Goal" + :in-theory + (disable + mono-chain$-is-chain-of-monotonic-functions) + :use + (:instance + mono-chain$-is-chain-of-monotonic-functions + (x ($bottom$)) + (y x))))) + +;; Extend mono-chain$ by adding an $bottom$ base: + +(defun + mono-chain$+$bottom$-base (i x) + (if (zp i) + ($bottom$) + (mono-chain$ (- i 1) x))) + +;; Choose an ``index'' for definition of lub of +;; mono-chain$: + +(defchoose + lub-mono-chain$-i i (x) + (not (equal (mono-chain$+$bottom$-base i x) + ($bottom$)))) + +(defthm + lub-mono-chain$-i-rewrite + (implies (equal (mono-chain$+$bottom$-base + (lub-mono-chain$-i x) + x) + ($bottom$)) + (equal (mono-chain$+$bottom$-base i x) + ($bottom$))) + :hints (("Goal" + :use lub-mono-chain$-i))) + +;; Make sure the chosen index is a nonneg. integer: + +(defun + lub-mono-chain$-nat-i (x) + (nfix (lub-mono-chain$-i x))) + +;; Define the least upper bound of mono-chain$: + +(defun + lub-mono-chain$ (x) + (mono-chain$+$bottom$-base + (lub-mono-chain$-nat-i x) x)) + +(in-theory (disable (:executable-counterpart + lub-mono-chain$))) + +;; lub-mono-chain$ is upper bound of mono-chain$: + +(defthm + lub-mono-chain$-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (mono-chain$ i x) + (lub-mono-chain$ x))) + :hints + (("Goal" + :in-theory (disable $<=$) + :by (:functional-instance + lub-chain$-is-upper-bound + (chain$ mono-chain$) + (lub-chain$ lub-mono-chain$) + (chain$+$bottom$-base + mono-chain$+$bottom$-base) + (lub-chain$-i lub-mono-chain$-i) + (lub-chain$-nat-i lub-mono-chain$-nat-i))) + ("Subgoal 3" + :in-theory (disable mono-chain$+$bottom$-base) + ))) + +;; Show lub-mono-chain$ is LEAST upper bound of +;; mono-chain$: + +;; Axiomatize an upper bound of mono-chain$: + +(encapsulate + (((ub-mono-chain$ *) => *)) + + (local + (defun + ub-mono-chain$ (x) + (lub-mono-chain$ x))) + + (defthm + ub-mono-chain$-is-upper-bound + (implies (and (integerp i) + (>= i 0)) + ($<=$ (mono-chain$ i x) + (ub-mono-chain$ x))) + :hints (("Goal" + :in-theory + (disable $<=$ lub-mono-chain$)))) + ) ;; end encapsulate + +(defthm + lub-mono-chain$-is-LEAST-upper-bound + ($<=$ (lub-mono-chain$ x)(ub-mono-chain$ x)) + :hints + (("Goal" + :in-theory (disable $<=$) + :by (:functional-instance + lub-chain$-is-LEAST-upper-bound + (chain$ mono-chain$) + (lub-chain$ lub-mono-chain$) + (ub-chain$ ub-mono-chain$) + (chain$+$bottom$-base + mono-chain$+$bottom$-base) + (lub-chain$-i lub-mono-chain$-i) + (lub-chain$-nat-i lub-mono-chain$-nat-i))) + ("Subgoal 2" + :in-theory (disable mono-chain$+$bottom$-base) + ))) + +(defthm + mono-chain$+$bottom$-base-is-$<=$-chain + (implies (and (integerp i) + (>= i 0)) + ($<=$ (mono-chain$+$bottom$-base i x) + (mono-chain$+$bottom$-base (+ 1 i) + x))) + :hints (("Goal" + :in-theory (disable $<=$) + :use (:instance + mono-chain$-is-$<=$-chain + (i (+ -1 i)))))) + +(defthm + mono-chain$+$bottom$-base=$bottom$ + (implies (zp i) + (equal (mono-chain$+$bottom$-base i x) + ($bottom$)))) + +(defthm + mono-chain$+$bottom$-base-is-$<=$-chain-e + (implies (and (not (equal + (mono-chain$+$bottom$-base i + x) + ($bottom$))) + (not (equal + (mono-chain$+$bottom$-base j + x) + ($bottom$)))) + (equal (mono-chain$+$bottom$-base i x) + (mono-chain$+$bottom$-base j x))) + :rule-classes nil + :hints (("Goal" + :in-theory (disable + $<=$ + mono-chain$+$bottom$-base) + :by + (:functional-instance + $bottom$-based-chain-is-$<=$-chain-e + ($bottom$-based-chain + mono-chain$+$bottom$-base))))) + +(defthm + mono-chain$+$bottom$-base-is-chain-of-monotonic-fns + (or (equal (mono-chain$+$bottom$-base i ($bottom$)) + ($bottom$)) + (equal (mono-chain$+$bottom$-base i x) + (mono-chain$+$bottom$-base i + ($bottom$)))) + :rule-classes nil + :hints + (("Goal" + :use + (:instance + mono-chain$-is-chain-of-monotonic-functions-a + (i (+ -1 i)))))) + +;; lub-mono-chain$ is a monotonic function: + +(defthm + lub-mono-chain$-is-monotonic + (implies ($<=$ x y) + ($<=$ (lub-mono-chain$ x) + (lub-mono-chain$ y))) + :hints + (("Goal" + :in-theory + (disable mono-chain$+$bottom$-base) + :use + ((:instance + mono-chain$+$bottom$-base-is-chain-of-monotonic-fns + (i (lub-mono-chain$-nat-i ($bottom$))) + (x y)) + (:instance + mono-chain$+$bottom$-base-is-$<=$-chain-e + (i (lub-mono-chain$-nat-i ($bottom$))) + (j (lub-mono-chain$-nat-i y)) + (x y)))))) |