;;; defmul.lisp
;;; Definition of macros DEFMUL and DEFMUL-COMPONENTS, needed to define
;;; well-founded multiset relations induced by well-founded
;;; relations. It needs book "multiset.lisp"
;;; Last Revision: 19-09-00
;;;============================================================================
;;; To certify this book:
#|
(in-package "ACL2")
(defpkg "MUL" (union-eq *acl2-exports*
(union-eq
*common-lisp-symbols-from-main-lisp-package*
'(remove-one multiset-diff))))
(certify-book "defmul" 1)
|#
;;; To use in your books, simply include it with (include-book "defmul")
(in-package "ACL2")
(include-book "multiset")
(set-verify-guards-eagerness 2)
;;; ****************************************************
;;; DEFINITION OF THE DEFMUL AND DEFMUL-COMPONENTS MACRO
;;; ****************************************************
;;; Given "rel" a well-founded relation on a set A, we generate
;;; the events needed to extend this relation on the set of finite
;;; multisets over A.
;;; ============================================================================
;;; 1. Definition defmul-components
;;; ============================================================================
;;; First: Given "rel" a well-founded relation on a set A, we need to know the
;;; components needed to extend this relation on the set of finite multisets
;;; over A:
;;; - "rel": The well-founded relation defined on A.
;;; - "mp": The meaure property defining the set A.
;;; - "fn": The embedding justifying well-foundedness of "rel".
;;; - "theorem": The theorem name with rule class
;;; "well-founded-relation" associated with "rel".
;;; - "varx", "vary": The variables used in the "theorem".
(defun search-well-founded-relation-theorem (world theorem)
(declare (xargs :mode :program))
(getprop theorem 'theorem
'(error theorem-not-found)
'current-acl2-world
world))
(defun destructure-aux-well-founded-relation-rule (term)
(declare (xargs :mode :program))
(case-match term
(('IF ('IMPLIES (mp x) ('E0-ORDINALP (fn x)))
('IMPLIES ('IF (mp x)
('IF (mp y) (rel x y) ''NIL)
''NIL)
('E0-ORD-< (fn x) (fn y)))
''NIL)
(mv mp fn rel x y))
(('IF ('E0-ORDINALP (fn x))
('IMPLIES (rel x y)
('E0-ORD-< (fn x) (fn y)))
''NIL)
(mv t fn rel x y))
(& (mv nil nil nil nil nil))))
(defun components-of-well-founded-relation-rule-fn (rel world)
(declare (xargs :mode :program))
(if (eq rel 'e0-ord-<)
(list rel nil 'e0-ordinalp 'e0-ord-<-fn nil nil)
(let ((name
(cadddr (assoc-eq rel
(global-val
'well-founded-relation-alist world)))))
(mv-let (nmp nfn nrel nx ny)
(destructure-aux-well-founded-relation-rule
(search-well-founded-relation-theorem world name))
(list nrel name nmp nfn nx ny)))))
(defun this-symbol-list-is-not-new (symbol-list world)
(declare (xargs :mode :program))
(if (endp symbol-list)
nil
(if (new-namep (car symbol-list) world)
(this-symbol-list-is-not-new (cdr symbol-list) world)
(cons (car symbol-list)
(this-symbol-list-is-not-new (cdr symbol-list) world)))))
(defun packn-in-pkg (lst pkg-witness)
(declare (xargs :mode :program))
(intern-in-package-of-symbol (coerce (packn1 lst) 'string) pkg-witness))
(defun defmul-symbols-not-new (list prefix world)
(declare (xargs :mode :program))
(let ((n-rel (car list))
(theorem (cadr list))
(n-mp (caddr list))
(n-fn (cadddr list)))
(let ((rel-bigg
(packn-in-pkg (append prefix
(list "EXISTS-" n-rel "-BIGGER"))
n-rel))
(for-exis
(packn-in-pkg (append prefix
(list "FORALL-EXISTS-" n-rel "-BIGGER"))
n-rel))
(m-rel
(packn-in-pkg (append prefix (list "MUL-" n-rel))
n-rel))
(map-fn
(packn-in-pkg (append prefix (list "MAP-" n-fn "-E0-ORD"))
n-fn))
(new-mp
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp))
(new-mp-multiset-diff
(packn-in-pkg
(append prefix (list n-mp "-TRUE-LISTP-MULTISET-DIFF"))
n-mp))
(cong-name1
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-1"))
n-rel))
(cong-name2
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-2"))
n-rel))
(n-rewr
(packn-in-pkg (append prefix (list theorem "-REWRITE"))
n-rel))
(mult-th
(packn-in-pkg
(append prefix
(list "MULTISET-EXTENSION-OF-" n-rel "-WELL-FOUNDED"))
n-rel)))
(this-symbol-list-is-not-new
(list rel-bigg for-exis m-rel map-fn new-mp
new-mp-multiset-diff cong-name1 cong-name2 n-rewr mult-th)
world))))
(defmacro defmul-components (rel &key prefix)
`(let ((n-rel
(car (assoc-eq (quote ,rel)
(global-val
'well-founded-relation-alist (w state))))))
(if (eq n-rel nil)
(er soft 'defmul-components
"The symbol ~x0 is not a well-founded relation. ~
See :DOC well-founded-relation."
(quote ,rel))
(let ((list (defmul-symbols-not-new
(components-of-well-founded-relation-rule-fn
(quote ,rel) (w state))
(if (quote ,prefix) (list (quote ,prefix) "-") nil)
(w state))))
(if list
(if (quote ,prefix)
(mv-let
(val state)
(fmx "~%WARNING: The ~#0~[symbol~/symbols~] ~*1 ~
~#0~[is~/are~] defined yet. Perhaps you must ~
use the :PREFIX option with a value different from ~
~x2. ~%~%~
The list of components is: ~%"
(if (= (length list) 1) 0 1)
(list "Empty list" "~x*" "~x* and " "~x*, " list)
(quote ,prefix))
(declare (ignore val))
(mv nil (components-of-well-founded-relation-rule-fn
(quote ,rel) (w state)) state))
(mv-let
(val state)
(fmx "~%WARNING: The ~#0~[symbol~/symbols~] ~*1 ~
~#0~[is~/are~] defined yet. Perhaps you must ~
use the :PREFIX option. ~%~%~
The list of components is: ~%"
(if (= (length list) 1) 0 1)
(list "Empty list" "~x*" "~x* and " "~x*, " list))
(declare (ignore val))
(mv nil (components-of-well-founded-relation-rule-fn
(quote ,rel) (w state)) state)))
(mv-let
(val state)
(fmx "~%The list of components is: ~%")
(declare (ignore val))
(mv nil (components-of-well-founded-relation-rule-fn
(quote ,rel) (w state)) state)))))))
;;; ============================================================================
;;; 2. Definition defmul
;;; ============================================================================
;;; Given "n-rel" a well-founded relation on a set A, and given the
;;; components needed to extend this relation to the set of finite multisets
;;; over A:
;;; - "n-rel": The well-founded relation defined on A.
;;; - "n-mp": The measure property defining the set A.
;;; - "n-fn": The embedding justifying the well-foundedness of "rel".
;;; - "theorem": The theorem name with rule class
;;; "well-founded-relation" associated with "rel".
;;; - "varx", "vary": The variables used in the "theorem".
;;; We build:
;;; - "EXISTS-n-rel-BIGGER": Needed for "MUL-n-rel".
;;; - "FORALL-EXISTS-n-rel-BIGGER": Needed for "MUL-n-rel".
;;; - "MUL-n-rel": Well-founded relation on finite multisets over A.
;;; - "MAP-n-fn-E0-ORD": The embedding justifying the well-foundedness of
;;; "MUL-n-rel".
;;; - "n-mp-TRUE-LISTP": The measure property defining the finite
;;; multisets over A.
;;; - "theorem-REWRITE": Well-founded relation theorem associated with
;;; "n-rel", but now as a rewriting rule.
;;; - "n-mp-TRUE-LISTP-MULTISET-DIFF": Needed for the guards verification of
;;; "MUL-n-rel".
;;; - "MULTISET-EXTENSION-OF-n-rel-WELL-FOUNDED": Well-founded relation
;;; theorem associated with "MUL-n-rel".
;;; - "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-n-rel-BIGGER-1" and
;;; "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-n-rel-BIGGER-2": Some useful
;;; congruences.
;;; We have to distinguish three cases: The two general forms recognized as
;;; well-founded relations (the first with an explicit property "mp" and the
;;; second with this property equal to "t"). The third case is for the
;;; "e0-ord-<" relation (the primitive well-founded relation over
;;; "e0-ordinalp").
(defun defmul-events-rel (prefix v-g n-rel n-mp)
(declare (xargs :mode :program))
(let ((rel-bigg
(packn-in-pkg (append prefix (list "EXISTS-" n-rel "-BIGGER"))
n-rel))
(for-exis
(packn-in-pkg (append prefix (list "FORALL-EXISTS-" n-rel "-BIGGER"))
n-rel))
(m-rel
(packn-in-pkg (append prefix (list "MUL-" n-rel))
n-rel))
(new-mp
(if (eq n-mp t)
'TRUE-LISTP
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp)))
)
(list
`(defun ,rel-bigg (x l) ; exists-rel-bigger
(declare (xargs :guard ,(if (eq n-mp t)
`(,new-mp l)
`(and (,n-mp x) (,new-mp l)))
:guard-hints
(("Goal" :hands-off ,(if (eq n-mp t)
`(,n-rel)
`(,n-rel ,n-mp))))
:verify-guards ,v-g))
(cond ((atom l) nil)
((,n-rel x (car l)) t)
(t (,rel-bigg x (cdr l)))))
`(defun ,for-exis (l m) ; forall-exists-rel-bigger
(declare (xargs :guard (and (,new-mp l)
(,new-mp m))
:guard-hints
(("Goal" :hands-off ,(if (eq n-mp t)
`()
`(,n-mp))))
:verify-guards ,v-g))
(if (atom l)
t
(and (,rel-bigg (car l) m)
(,for-exis (cdr l) m))))
`(defun ,m-rel (n m) ; mul-rel
(declare (xargs :guard (and (,new-mp n)
(,new-mp m))
:verify-guards nil))
(let ((m-n (multiset-diff m n))
(n-m (multiset-diff n m)))
(and (consp m-n) (,for-exis n-m m-n))))
)))
(defun defmul-events-fn (prefix v-g n-fn n-mp)
(declare (xargs :mode :program))
(let ((map-fn
(packn-in-pkg (append prefix (list "MAP-" n-fn "-E0-ORD"))
n-fn))
(new-mp
(if (eq n-mp t)
'TRUE-LISTP
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp)))
)
(list
`(defun ,map-fn (l) ; map-fn-e0-ord
(declare (xargs :guard (,new-mp l)
:guard-hints
(("Goal" :hands-off ,(if (eq n-mp t)
`()
`(,n-mp))))
:verify-guards ,v-g))
(if (consp l)
(MUL::insert-e0-ord-<
(MUL::add1-if-integer
,(if (eq n-fn 'e0-ord-<-fn)
'(car l)
(list n-fn '(car l))))
(,map-fn (cdr l)))
0))
)))
(defun defmul-events-mp (prefix v-g n-mp)
(declare (xargs :mode :program))
(let ((new-mp
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp))
)
(list
`(defun ,new-mp (l) ; mp-true-listp
(declare (xargs :verify-guards ,v-g))
(if (atom l)
(equal l nil)
(and (,n-mp (car l))
(,new-mp (cdr l)))))
)))
(defun defmul-events-theorems-t (prefix rule-classes
theorem n-fn n-rel varx vary)
(declare (xargs :mode :program))
(let ((rel-bigg
(packn-in-pkg (append prefix (list "EXISTS-" n-rel "-BIGGER"))
n-rel))
(for-exis
(packn-in-pkg (append prefix (list "FORALL-EXISTS-" n-rel "-BIGGER"))
n-rel))
(m-rel
(packn-in-pkg (append prefix (list "MUL-" n-rel))
n-rel))
(map-fn
(packn-in-pkg (append prefix (list "MAP-" n-fn "-E0-ORD"))
n-fn))
(n-rewr
(packn-in-pkg (append prefix (list theorem "-REWRITE"))
n-rel))
(cong-name1
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-1"))
n-rel))
(cong-name2
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-2"))
n-rel))
(mult-th
(packn-in-pkg
(append prefix (list "MULTISET-EXTENSION-OF-" n-rel "-WELL-FOUNDED"))
n-rel))
)
(list
`(local (defthm ,n-rewr
(and (e0-ordinalp (,n-fn ,varx))
(implies (,n-rel ,varx ,vary)
(e0-ord-< (,n-fn ,varx) (,n-fn ,vary))))
:rule-classes :rewrite
:hints (("Goal" :use ,theorem))))
`(defthm ,mult-th
(and (implies (true-listp x) (e0-ordinalp (,map-fn x)))
(implies (and (true-listp x)
(true-listp y)
(,m-rel x y))
(e0-ord-< (,map-fn x) (,map-fn y))))
:rule-classes ,(extend-rule-classes :WELL-FOUNDED-RELATION
rule-classes)
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::multiset-extension-of-rel-well-founded
(MUL::x x) (MUL::y y))
(MUL::mp-true-listp true-listp)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)
(MUL::mul-rel ,m-rel)
(MUL::map-fn-e0-ord ,map-fn)
(MUL::rel ,n-rel)
(MUL::mp (lambda (x) t))
(MUL::fn ,n-fn)))
:hands-off (,n-fn ,n-rel))))
`(defcong MUL::equal-set iff (,for-exis l m) 1
:event-name ,cong-name1
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-1
(MUL::l l) (MUL::m m))
(MUL::fn ,n-fn)
(MUL::mp (lambda (x) t))
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)))
:hands-off (,n-fn ,n-rel))))
`(defcong MUL::equal-set iff (,for-exis l m) 2
:event-name ,cong-name2
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-2
(MUL::l l) (MUL::m m))
(MUL::fn ,n-fn)
(MUL::mp (lambda (x) t))
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)))
:hands-off (,n-fn ,n-rel))))
)))
(defun defmul-events-theorems-mp (prefix rule-classes
theorem n-mp n-fn n-rel varx vary)
(declare (xargs :mode :program))
(let ((rel-bigg
(packn-in-pkg (append prefix (list "EXISTS-" n-rel "-BIGGER"))
n-rel))
(for-exis
(packn-in-pkg (append prefix (list "FORALL-EXISTS-" n-rel "-BIGGER"))
n-rel))
(m-rel
(packn-in-pkg (append prefix (list "MUL-" n-rel))
n-rel))
(map-fn
(packn-in-pkg (append prefix (list "MAP-" n-fn "-E0-ORD"))
n-fn))
(new-mp
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp))
(n-rewr
(packn-in-pkg (append prefix (list theorem "-REWRITE"))
n-rel))
(new-mp-multiset-diff
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP-MULTISET-DIFF"))
n-mp))
(cong-name1
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-1"))
n-rel))
(cong-name2
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-2"))
n-rel))
(mult-th
(packn-in-pkg
(append prefix (list "MULTISET-EXTENSION-OF-" n-rel "-WELL-FOUNDED"))
n-rel))
)
(list
`(local (defthm ,n-rewr
(and (implies (,n-mp ,varx) (e0-ordinalp (,n-fn ,varx)))
(implies (and (,n-mp ,varx)
(,n-mp ,vary)
(,n-rel ,varx ,vary))
(e0-ord-< (,n-fn ,varx) (,n-fn ,vary))))
:rule-classes :rewrite
:hints (("Goal" :use ,theorem))))
`(defthm ,new-mp-multiset-diff
(implies (,new-mp m)
(,new-mp (multiset-diff m n)))
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::mp-true-listp-multiset-diff
(MUL::m m) (MUL::n n))
(MUL::mp-true-listp ,new-mp)
(MUL::mp ,n-mp)
(MUL::fn ,n-fn)
(MUL::rel ,n-rel)))
:hands-off (,n-mp ,n-fn ,n-rel))))
`(defthm ,mult-th
(and (implies (,new-mp x) (e0-ordinalp (,map-fn x)))
(implies (and (,new-mp x)
(,new-mp y)
(,m-rel x y))
(e0-ord-< (,map-fn x) (,map-fn y))))
:rule-classes ,(extend-rule-classes :WELL-FOUNDED-RELATION
rule-classes)
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::multiset-extension-of-rel-well-founded
(MUL::x x) (MUL::y y))
(MUL::mp-true-listp ,new-mp)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)
(MUL::mul-rel ,m-rel)
(MUL::map-fn-e0-ord ,map-fn)
(MUL::rel ,n-rel)
(MUL::mp ,n-mp)
(MUL::fn ,n-fn)))
:hands-off (,n-mp ,n-fn ,n-rel))))
`(defcong MUL::equal-set iff (,for-exis l m) 1
:event-name ,cong-name1
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-1
(MUL::l l) (MUL::m m))
(MUL::fn ,n-fn)
(MUL::mp ,n-mp)
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)))
:hands-off (,n-mp ,n-fn ,n-rel))))
`(defcong MUL::equal-set iff (,for-exis l m) 2
:event-name ,cong-name2
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-2
(MUL::l l) (MUL::m m))
(MUL::fn ,n-fn)
(MUL::mp ,n-mp)
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)))
:hands-off (,n-mp ,n-fn ,n-rel))))
)))
(defun defmul-events-theorems-ord (prefix rule-classes
n-mp n-fn n-rel)
(declare (xargs :mode :program))
(let ((rel-bigg
(packn-in-pkg (append prefix (list "EXISTS-" n-rel "-BIGGER"))
n-rel))
(for-exis
(packn-in-pkg (append prefix (list "FORALL-EXISTS-" n-rel "-BIGGER"))
n-rel))
(m-rel
(packn-in-pkg (append prefix (list "MUL-" n-rel))
n-rel))
(map-fn
(packn-in-pkg (append prefix (list "MAP-" n-fn "-E0-ORD"))
n-fn))
(new-mp
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP"))
n-mp))
(new-mp-multiset-diff
(packn-in-pkg (append prefix (list n-mp "-TRUE-LISTP-MULTISET-DIFF"))
n-mp))
(cong-name1
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-1"))
n-rel))
(cong-name2
(packn-in-pkg
(append prefix (list "EQUAL-SET-IMPLIES-IFF-FORALL-EXISTS-"
n-rel "-BIGGER-2"))
n-rel))
(mult-th
(packn-in-pkg
(append prefix (list "MULTISET-EXTENSION-OF-" n-rel "-WELL-FOUNDED"))
n-rel))
)
(list
`(defthm ,new-mp-multiset-diff
(implies (,new-mp m)
(,new-mp (multiset-diff m n)))
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::mp-true-listp-multiset-diff
(MUL::m m) (MUL::n n))
(MUL::mp-true-listp ,new-mp)
(MUL::mp ,n-mp)
(MUL::fn (lambda (x) x))
(MUL::rel ,n-rel)))
:hands-off (,n-mp ,n-rel))))
`(defthm ,mult-th
(and (implies (,new-mp x) (e0-ordinalp (,map-fn x)))
(implies (and (,new-mp x)
(,new-mp y)
(,m-rel x y))
(e0-ord-< (,map-fn x) (,map-fn y))))
:rule-classes ,(extend-rule-classes :WELL-FOUNDED-RELATION
rule-classes)
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::multiset-extension-of-rel-well-founded
(MUL::x x) (MUL::y y))
(MUL::mp-true-listp ,new-mp)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis)
(MUL::mul-rel ,m-rel)
(MUL::map-fn-e0-ord ,map-fn)
(MUL::rel ,n-rel)
(MUL::mp ,n-mp)
(MUL::fn (lambda (x) x)))))))
`(defcong MUL::equal-set iff (,for-exis l m) 1
:event-name ,cong-name1
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-1
(MUL::l l) (MUL::m m))
(MUL::fn (lambda (x) x))
(MUL::mp ,n-mp)
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis))))))
`(defcong MUL::equal-set iff (,for-exis l m) 2
:event-name ,cong-name2
:hints (("Goal"
:use ((:functional-instance
(:instance
MUL::equal-set-implies-iff-forall-exists-rel-bigger-2
(MUL::l l) (MUL::m m))
(MUL::fn (lambda (x) x))
(MUL::mp ,n-mp)
(MUL::rel ,n-rel)
(MUL::exists-rel-bigger ,rel-bigg)
(MUL::forall-exists-rel-bigger ,for-exis))))))
)))
(defun defmul-events (list prefix verify-guards rule-classes)
(declare (xargs :mode :program))
(let ((n-rel (car list))
(m-rel (packn-in-pkg (append prefix (list "MUL-" (car list)))
(car list)))
(theorem (cadr list))
(n-mp (caddr list))
(n-fn (cadddr list))
(varx (car (cddddr list)))
(vary (cadr (cddddr list)))
(l-prefix (if prefix (list prefix "-") nil)))
(append
(if (eq n-mp t)
nil
(defmul-events-mp l-prefix verify-guards n-mp))
(defmul-events-rel l-prefix verify-guards n-rel n-mp)
(defmul-events-fn l-prefix verify-guards n-fn n-mp)
(cond ((eq n-mp t)
(defmul-events-theorems-t l-prefix rule-classes
theorem n-fn n-rel varx vary))
((eq n-mp 'e0-ordinalp)
(defmul-events-theorems-ord l-prefix rule-classes
n-mp n-fn n-rel))
(t
(defmul-events-theorems-mp l-prefix rule-classes
theorem n-mp n-fn n-rel varx vary)))
(if (eq verify-guards t)
(list `(verify-guards ,m-rel))
nil))))
(defmacro defmul (list &key prefix
(verify-guards 'nil)
(rule-classes '(:WELL-FOUNDED-RELATION)))
`(encapsulate
()
,@(defmul-events list prefix verify-guards rule-classes)))
;;; ============================================================================
;;; 3. Documentation
;;; ============================================================================
(defdoc defmul
":Doc-section defmul
extends a well-founded relation to multisets.~/~/
How to use: To extend a well-founded relation to multisets we need
know:
- : The well-founded relation defined on A.
- : The theorem with rule class \"well-founded-relation\"
associated with .
- : The measure property defining the set A.
- : The embedding justifying the well-foundedness of .
- , : The variables used in the .
and eval the \"defmul\" macro with the list of these components:
(defmul ( ))
The main non-local events generated by this macro call are:
- the definitions needed for the multiset relation induced by :
functions exists--bigger, forall-exists--bigger and
mul-.
- the definition of the multiset measure property, -true-listp.
- the definition of mp--e0-ord, the embedding function from
multisets to ordinals.
- the well-foundedness theorem for mul-, named
multiset-extension-of--well-founded.
To see the complete list of generated events use :trans1 on a defmul call.
We expect defmul to work without assistance from the user. After the
above call to defmul, the function mul- is defined as a
well-founded relation on multisets of elements satisfying the property
, induced by the well-founded relation . From
this moment on, mul- can be used in the admissibility test
for recursive functions to show that the recursion terminates.
This macro has three optionals arguments:
:prefix : With this argument we can use as a prefix for
the names of the events builded.
:rule-classes : With this argument we can propose as
additional rule-classes for the well-founded relation theorem
associated with the multiset extension. The default value is
:well-founded-relation.
:verify-guards : The value of must be T or NIL. With this
argument we can decide when the guards of the functions builded must be
verified on definition time.
To know the list of names that we need to supply to a \"defmul\" call, we
have developed a tool to look up the Acl2 \"world\" and print that list:
(defmul-components )
This is only an informative tool, not a event. This macro looks up the Acl2
\"world\", and informs if some symbols (those that the \"defmul\" macro
builds) have been already defined. As the \"defmul\" macro, has one
optional argument to propose a prefix:
:prefix : With this argument we can use as a prefix for
the names of the events builded.
An example:
(encapsulate
((my-mp (v) booleanp)
(my-rel (v w) booleanp)
(my-fn (v) e0-ordinalp))
(local (defun my-mp (v) (declare (ignore v)) nil))
(local (defun my-rel (v w) (declare (ignore v w)) nil))
(local (defun my-fn (v) (declare (ignore v)) 1))
(defthm my-rel-well-founded-relation
(and (implies (my-mp v) (e0-ordinalp (my-fn v)))
(implies (and (my-mp v)
(my-mp w)
(my-rel v w))
(e0-ord-< (my-fn v) (my-fn w))))
:rule-classes :well-founded-relation)
(defun map-my-fn-e0-ord (l)
l))
; (defmul-components my-rel)
; => WARNING: The symbol MAP-MY-FN-E0-ORD is defined yet. Perhaps you must
; use the :PREFIX option.
;
; The list of components is:
; (MY-REL MY-REL-WELL-FOUNDED-RELATION MY-MP MY-FN V W)
;
; (defmul-components my-rel :prefix new)
; => The list of components is:
; (MY-REL MY-REL-WELL-FOUNDED-RELATION MY-MP MY-FN V W)
(defmul (MY-REL MY-REL-WELL-FOUNDED-RELATION MY-MP MY-FN V W)
:prefix new :rule-classes :rewrite)
~/")