;;; multiset.lisp
;;; - Useful lemmas about multisets
;;; - Multiset extension of a well-founded relation is a well-founded relation.  
;;; Created: 10-6-99 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 "multiset" 1)
|#

(in-package "MUL")


(ACL2::set-verify-guards-eagerness 2)

;;; *****************************************************
;;; PART I: DEFINITIONS AND USEFUL LEMMAS ABOUT MULTISETS
;;; *****************************************************

;;; ============================================================================
;;; 1. Multisets (unordered lists).
;;; ============================================================================


;;; ----------------------------------------------------------------------------
;;; 1.1 equal-set and properties.
;;; ----------------------------------------------------------------------------

(defun equal-set (x y)
  (declare (xargs :guard
		  (if (acl2::eqlable-listp y)
		      (true-listp x)
		      (if (acl2::eqlable-listp x)
			  (true-listp y)
			  nil))))
  (and (subsetp x y) (subsetp y x)))

(local
 (defthm subsetp-cons
   (implies (subsetp l m)
	    (subsetp l (cons x m)))))

(local  
 (defthm subsetp-reflexive
   (subsetp l l)))

(local
 (defthm subsetp-transitive
   (implies (and (subsetp l m)
		 (subsetp m n))
	    (subsetp l n))))

(acl2::defequiv equal-set)

(acl2::defcong equal-set equal (consp l) 1)

;;; ----------------------------------------------------------------------------
;;; 1.2 remove-one and properties.
;;; ----------------------------------------------------------------------------

(defun remove-one (x l)
  (cond ((atom l) l)
	((equal x (car l)) (cdr l))
	(t (cons (car l) (remove-one x (cdr l))))))

(defthm remove-one-true-listp
  (implies (true-listp l)
	   (true-listp (remove-one x l))))

(local
 (defthm member-remove-one
   (implies (and (member x l) (not (equal x y)))
	    (member x (remove-one y l)))))

(local
 (defthm remove-one-conmute
   (equal (remove-one x (remove-one y l))
	  (remove-one y (remove-one x l)))))

(local
 (defthm remove-one-member
   (implies (not (member x l))
	    (not (member x (remove-one y l))))))

(local
 (defthm remove-one-subsetp
   (subsetp (remove-one x l) l)))

;;; ----------------------------------------------------------------------------
;;; 1.3 Multiset difference and properties.
;;; ----------------------------------------------------------------------------

(defun multiset-diff (m n)
  (if (atom n)
      m
      (multiset-diff (remove-one (car n) m) (cdr n))))

(defthm multiset-diff-true-listp
  (implies (and (true-listp m)
		(true-listp n))
	   (true-listp (multiset-diff m n))))

(local
 (defthm multiset-diff-member
   (implies (and (member x n) (not (member x m)))
	    (member x (multiset-diff n m)))))

(local
 (defthm multiset-diff-removing-the-same-element
   (implies (and (member x n) (member x m))
	    (equal (multiset-diff (remove-one x m)
				  (remove-one x n))
		   (multiset-diff m n)))))

(local
 (defthm multiset-diff-nil
   (not (consp (multiset-diff nil l)))))

(local
 (defthm subsetp-multiset-diff
   (subsetp (multiset-diff n m) n)))

(defthm multiset-diff-remove-one-not-consp
  (not (consp (multiset-diff (remove-one x l) l)))
  :hints (("Goal" :induct (acl2::len l))))

(defthm list-multiset-diff-1
  (implies (not (member x l))
	   (equal (multiset-diff (list x) l)
		  (list x))))

(defthm list-multiset-diff-2
  (implies (not (member x l))
	   (equal (multiset-diff l (list x))
		  l)))

(defthm multiset-diff-append-1
  (equal (multiset-diff (append m1 m2)
			(append m1 m3))
	 (multiset-diff m2 m3)))

;;; REMARK: An analogue property is not true for (multiset-diff (append
;;; m1 m2) (append m3 m2)) (take for example '(3 2 1 3) and '(1
;;; 3)). Nevertheless, we prove below that (multiset-diff (append m1 m2)
;;; (append m3 m2)) is exactly the same set (although not the same list
;;; in general) as (multiset-diff m1 m3). This rewrite rule will be used
;;; together with two congruence rules relating forall-exists-rel-bigger
;;; and equal-se (see 2.3 in this file). Furthermore, using functional
;;; instantiation, these two congruence rules are generated for every
;;; particular relation "rel" by defmul (see defmul.lisp).



(encapsulate
 ()

 (local
  (defun my-occur (x l)
    (cond ((atom l) 0)
	  ((equal x (car l)) (1+ (my-occur x (cdr l))))
	  (t (my-occur x (cdr l))))))
 
 (local
  (defthm my-occur-append
    (equal (my-occur x (append l m))
	   (+ (my-occur x l) (my-occur x m)))))
 
 (local
  (defthm my-occur-remove-one
    (equal (my-occur x (remove-one y l))
	   (if (and (equal x y) (member x l))
	       (1- (my-occur x l))
	       (my-occur x l)))))
 
 (local
  (defthm subsetp-multiset-diff-member
    (implies (not (member x l))
	     (not (member x (multiset-diff l m))))))

 (local
  (defthm multiset-diff-my-occur
    (iff (member x (multiset-diff l m))
	 (> (my-occur x l) (my-occur x m)))))
 
 (local
  (defthm multiset-diff-append-2-lemma
    (iff (member x (multiset-diff (append m1 m2)
				  (append m3 m2)))
	 (member x (multiset-diff m1 m3)))))
 
 (local
  (defun not-subsetp-witness (m1 m2)
    (declare (xargs :verify-guards nil))
    (if (atom m1)
	nil
	(if (member (car m1) m2)
	    (not-subsetp-witness (cdr m1) m2)
	    (car m1)))))

 (local
  (defthm not-subsetp-witness-lemma 
    (equal (subsetp m1 m2)
	   (implies (member (not-subsetp-witness m1 m2) m1)
		    (member (not-subsetp-witness m1 m2) m2)))))

 (defthm multiset-diff-append-2
   (equal-set (multiset-diff (append m1 m2)
			     (append m3 m2))
	      (multiset-diff m1 m3))))

;;; ----------------------------------------------------------------------------
;;; 1.4 A useful meta rule about "multiset-diff"
;;; ----------------------------------------------------------------------------

;;; This rule rewrites expressions of the form:

;;; (multiset-diff (list* x1 ... xm l)
;;; 	           (list* y1 ... yk l))

;;; to the equivalent (w.r.t. equal-set):

;;; (multiset-diff (list x1 ... xm)
;;;    	           (list y1 ... yk))



(defun initial-cars (l)
  (if (and (consp l)
	   (eq (car l) 'cons)
	   (consp (cdr l))
	   (consp (cddr l))
	   (eq (cdddr l) 'nil))
      (list 'cons (cadr l) (initial-cars (caddr l)))
      ''nil))

(defun last-cdr (l)
  (if (and (consp l)
	   (eq (car l) 'cons)
	   (consp (cdr l))
	   (consp (cddr l))
	   (eq (cdddr l) 'nil))
      (last-cdr (caddr l))
      l))

(defun exclude-last-cdr-multiset-diff (x)
  (if (and (consp x)
	   (eq (car x) 'multiset-diff)
	   (consp (cdr x))
	   (consp (cddr x))
	   (eq (cdddr x) 'nil))
      (list 'multiset-diff
	    (initial-cars (cadr x))
	    (initial-cars (caddr x)))
      x))

(acl2::defevaluator ev-multiset-diff ev-multiset-diff-list
		    ((cons x l)
		     (multiset-diff l1 l2)
		     (equal l1 l2)))

(local
 (defthm ev-multiset-diff-append-initial-cars-last-cdr
   (equal (append (ev-multiset-diff (initial-cars l) a)
		  (ev-multiset-diff (last-cdr l) a))
	  (ev-multiset-diff l a))))

(defun hypothesis-multiset-diff-meta (x)
  (if (and (consp x)
	   (consp (cdr x))
	   (consp (cddr x))
	   (eq (cdddr x) 'nil))
      (list 'equal
	    (last-cdr (cadr x))
	    (last-cdr (caddr x)))
      ''nil))

(defthm multiset-diff-meta
  (implies
   (ev-multiset-diff (hypothesis-multiset-diff-meta x) a)
   (equal-set (ev-multiset-diff x a)
	      (ev-multiset-diff (exclude-last-cdr-multiset-diff x) a)))
  :rule-classes ((:meta :trigger-fns (multiset-diff)))
  :hints (("Goal"
	   :use ((:instance
		  multiset-diff-append-2
		  (m1 (ev-multiset-diff (initial-cars (cadr x)) a))
		  (m2 (ev-multiset-diff (last-cdr (cadr x)) a))
		  (m3 (ev-multiset-diff (initial-cars (caddr x)) a))))
	   :in-theory (disable initial-cars))))




;;; **********************************************
;;; PART II: WELL-FOUNDEDNES OF MULTISET RELATIONS
;;; **********************************************


;;; ============================================================================
;;; 2. Multiset extension of a well-founded relation is a well-founded
;;;    relation. 
;;; ============================================================================

;;; ----------------------------------------------------------------------------
;;; 2.1 A general well-founded relation
;;; ----------------------------------------------------------------------------
 
;;; Definition of a general well-founded relation on a set:
;;; - mp:  the measure property defining the set.
;;; - rel: the well-founded relation defined on elements satisfying mp.  
;;; - fn:  the embedding justifying the well-foundedness of rel.

(encapsulate 
 ((mp (x) booleanp)
  (rel (x y) booleanp)
  (fn (x) e0-ordinalp))

 (local (defun mp (x) (declare (ignore x)) nil))
 (local (defun rel (x y) (declare (ignore x y)) nil))
 (local (defun fn (x) (declare (ignore x)) 1))

 (defthm rel-well-founded-relation-on-mp
   (and (implies (mp x) (e0-ordinalp (fn x)))
	(implies (and (mp x)                      
		      (mp y)
		      (rel x y))
		 (e0-ord-< (fn x) (fn y))))
   :rule-classes :well-founded-relation))

;;; REMARK: For our purpouses, we need another property about "fn", its
;;; values must be greater than 0.  Thus, we define a new measure
;;; function "fn1" equal to "fn" except for integers, where 1 is added.


(defun add1-if-integer (x)
  (if (integerp x) (1+ x) x))

(local
 (defmacro fn1 (x)
   `(add1-if-integer (fn ,x))))

;;; We prove now that fn1 is also an embedding, with the aditional
;;; property that never returns zero

(local
 (defthm e0-ord-<-add1-if-integer
   (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-< x y))
	    (e0-ord-< (add1-if-integer x) (add1-if-integer y)))))
 
(local
 (defthm add1-if-integer-e0-ordinalp-not-equal-0
   (implies (e0-ordinalp x)
	    (not (equal (add1-if-integer x) 0)))))

(local
 (defthm add1-if-integer-e0-ordinalp
   (implies (e0-ordinalp x)
	    (e0-ordinalp (add1-if-integer x)))))

(local (in-theory (disable add1-if-integer)))

(local
 (defthm fn-e0-ordinalp
   (implies (mp x)
	    (e0-ordinalp (fn x)))
   :hints (("Goal" :use rel-well-founded-relation-on-mp))))

;;; Here they are:

(local
 (defthm fn1-e0-ordinalp
   (implies (mp x)
	    (and (e0-ordinalp (fn1 x))
		 (not (equal (fn1 x) 0))))))


(local
 (defthm rel-well-founded-relation-on-mp-rewrite
   (implies (and (mp x)                      
                 (mp y)
                 (rel x y))
	    (e0-ord-< (fn1 x) (fn1 y)))
   :hints (("Goal" :use rel-well-founded-relation-on-mp))))

;;; ----------------------------------------------------------------------------
;;; 2.2 Induced multiset relation
;;; ---------------------------------------------------------------------------- 

;;; Now we define the multiset extension on multisets of elements with
;;; the MP-property.  We need to define: 
;;; - The measure property defining multisets of elements:
;;;   mp-true-listp.  
;;; - The well-founded relation: mul-rel.  
;;; - The embedding justifying well-foundedness: mp-fn-e0-ord.


;;; Measure property

(defun mp-true-listp (l)
  (if (atom l)
      (equal l nil)
      (and (mp (car l)) (mp-true-listp (cdr l)))))

;;; Multiset relation

(defun exists-rel-bigger (x l)
  (cond ((atom l) nil)
	((rel x (car l)) t)
	(t (exists-rel-bigger x (cdr l)))))

(defun forall-exists-rel-bigger (l m)
  (if (atom l)
      t
      (and (exists-rel-bigger (car l) m)
	   (forall-exists-rel-bigger (cdr l) m))))

(defun mul-rel (n m)
  (let ((m-n (multiset-diff m n))
	(n-m (multiset-diff n m)))
    (and (consp m-n) (forall-exists-rel-bigger n-m m-n))))
;;; Embedding

(defun insert-e0-ord-< (x l)
  (cond ((atom l) (cons x l))
	((not (e0-ord-< x (car l)))  (cons x l))
	(t (cons (car l) (insert-e0-ord-< x (cdr l))))))

(defun map-fn-e0-ord (l)
  (if (consp l)
      (insert-e0-ord-< (add1-if-integer (fn (car l)))
		       (map-fn-e0-ord (cdr l)))
      0))

;;; ----------------------------------------------------------------------------
;;; 2.3 An interesting congruence.
;;; ----------------------------------------------------------------------------

;;; These rules are used in conjuction with rewite rules that simplify
;;; multiset differences (w.r.t equal or equal-set)

;;; REMARK: These two congruence rules will be instantiated by every
;;; defmul macro to prove the analogues for every particular rel.


(encapsulate 
 ()

 (local (defthm exists-rel-bigger-subsetp
	  (implies (and
		    (exists-rel-bigger x a)
		    (subsetp a b))
		   (exists-rel-bigger x b))))

 (acl2::defcong equal-set iff (forall-exists-rel-bigger l m) 2))


(encapsulate
 ()

 (local
  (defthm forall-exists-rel-bigger-subsetp
    (implies (and
	      (forall-exists-rel-bigger b l)
	      (subsetp a b))
	     (forall-exists-rel-bigger a l))))
 
 (acl2::defcong equal-set iff (forall-exists-rel-bigger l m) 1))


(in-theory
 (disable
  equal-set-implies-iff-forall-exists-rel-bigger-2
  equal-set-implies-iff-forall-exists-rel-bigger-1))
 

;;; ----------------------------------------------------------------------------
;;; 2.4 Some ad hoc lemmas about ordinals.
;;; ----------------------------------------------------------------------------


(local
 (defthm weak-e0-ord-<-trichotomy
   (implies (e0-ord-< o1 o2)
	    (not (e0-ord-< o2 o1)))))

(local (in-theory (disable weak-e0-ord-<-trichotomy)))

(local
 (defthm e0-ord-<-trichotomy
   (implies (and (e0-ordinalp o1)
		 (e0-ordinalp o2)
		 (not (equal o1 o2))
		 (not (e0-ord-< o1 o2)))
	    (e0-ord-< o2 o1))
   :rule-classes :type-prescription))

(defthm e0-ord-<-irreflexive
  (not (e0-ord-< x x)))

(local (in-theory (disable e0-ord-<-irreflexive)))

(local
 (defthm e0-ord-<-transitive-corollary
   (implies (and (e0-ordinalp o1)
		 (e0-ordinalp o3)
		 (e0-ord-< o3 o2)
		 (not (e0-ord-< o1 o2)))
	    (e0-ord-< o3 o1))
   :rule-classes :type-prescription
   :hints (("Goal" :in-theory (enable e0-ord-<-trichotomy)))))


;;; ----------------------------------------------------------------------------
;;; 2.5 Well-foundedness of mul-rel
;;; ----------------------------------------------------------------------------


;;; Our goal is to prove that mul-rel is a well-founded relation on elements
;;;   satisfying mp-true-listp. We have to prove: 
;;; 1) If (mp-true-listp m), the (map-fn-e0-ord m) is an ordinal.
;;; 2) If l and m are mp-true-listp and (mul-rel n m), then
;;;    (e0-ord-< (map-fn-e0-ord n) (map-fn-e0-ord m))


;;; ············································································
;;; 2.5.1 The measure is an ordinal.
;;; ············································································

(local
 (defthm e0-ordinalp-insert-e0-ord-<
   (implies (and (e0-ordinalp l)
		 (e0-ordinalp o)
		 (not (equal o 0)))
	    (e0-ordinalp (insert-e0-ord-< o l)))
   :hints (("Goal" :in-theory (enable weak-e0-ord-<-trichotomy)))))

(local
 (defthm e0-ordinalp-map-fn-e0-ord
   (implies (mp-true-listp m)
	    (e0-ordinalp (map-fn-e0-ord m)))))


;;; ············································································
;;; 2.5.2 The measure is an embedding
;;; ············································································



;;; SKETCH OF THE PROOF: 
;;; Let N and M such that (mul-rel N M). We have to prove that 
;;;      (e0-ord-< (map-fn-e0-ord N) (map-fn-e0-ord M))
;;;  Suppose (fn x) and (fn y) are the biggest
;;; (w.r.t. e0-ord-<) elements of fn[N] and fn[M], respectively. Since
;;; they are ordinals, three cases are possible:

;;; 1) (fn x) < (fn y). Done.

;;; 2) (fn x) > (fn y). This is not possible: in that case x is in N-M
;;; and by the multiset order definition, exists z in M-N such that (rel
;;; x z) and consequently (fn z) > (fn x) >= (fn y). This is a
;;; contradiction with the fact that (fn y) is the biggest element of
;;; fn[M]. 

;;; 3) (fn x) = (fn y). In that case, x is in M, since otherwise it
;;; would exist z in M-N such that (rel z x) and the same contradiction
;;; as in case 2) appears. So N-{x} and M-{x} are multisets and N-{x}
;;; bigger than M-{x} w.r.t. multiset relation with the property that
;;; the ordinal mesures of these two multisets are respectively the
;;; cdr's of the ordinal measures of N and M. Induction hypothesis can
;;; be applied here.
;;;
;;; We must define an induction scheme to mimic this proof sketch.
;;; This will be done later by induction-multiset
;;; But we previously prove some lemmas...



;;; max-fn1-list (an element in l with maximal (fn1 ..)) and properties.
;;; ······································································

(local
 (defun max-fn1-list (l)
   (cond ((atom l) nil)
	 ((atom (cdr l)) (car l))
	 (t (let ((max-cdr (max-fn1-list (cdr l))))
	      (if (e0-ord-< (fn1 max-cdr) (fn1 (car l)))
		  (car l)
		  max-cdr))))))

(local 
 (defthm max-fn1-list-member
   (implies (consp l)
	    (member (max-fn1-list l) l))))

(local 
 (defthm mp-member-true-listp
   (implies (and (mp-true-listp l)
		 (member x l))
	    (mp x))
   :rule-classes :type-prescription))

(local
 (defthm max-fn1-listp-mp
   (implies (and (consp l) (mp-true-listp l))
	    (mp (max-fn1-list l)))))

(local 
 (defthm max-fn1-list-maximal
   (implies (member x l)
	    (not (e0-ord-< (fn1 (max-fn1-list l)) (fn1 x))))
   :hints (("Goal" :in-theory (enable e0-ord-<-irreflexive)))))




;;; An "alternative definition" of "map-fn-e0-ord".
;;; ···············································

(local
 (encapsulate
  ()

  (local 
   (defthm insert-e0-ord-<-conmute
     (implies (and (e0-ordinalp x) (e0-ordinalp y))
	      (equal (insert-e0-ord-< x (insert-e0-ord-< y l))
		     (insert-e0-ord-< y (insert-e0-ord-< x l))))
     :hints (("Goal" :in-theory (enable 
				 weak-e0-ord-<-trichotomy
				 e0-ord-<-trichotomy
				 e0-ord-<-transitive-corollary)))))

  (local
   (defthm another-definition-of-map-fn-e0-ord-lemma
     (implies (and (mp-true-listp l) (member x l))
	      (equal (map-fn-e0-ord l)
		     (insert-e0-ord-< (fn1 x)
				      (map-fn-e0-ord (remove-one x l)))))
     :rule-classes nil))
  
  (local 
   (defun bigger-than-list (x l)
     (declare (xargs :verify-guards nil))
     (cond ((atom l) t)
	   ((e0-ord-< x (car l)) nil)
	   (t (bigger-than-list x (cdr l))))))

  (local 
   (defthm bigger-than-list-insert
     (implies (and (bigger-than-list x l)
		   (not (e0-ord-< x y)))
	      (bigger-than-list x (insert-e0-ord-< y l)))))

  (local 
   (defthm bigger-than-list-max-fn1-map-fn-e0-ord-subsetp
     (implies (subsetp m l)
	      (bigger-than-list (fn1 (max-fn1-list l))
				(map-fn-e0-ord m)))
     :rule-classes nil))

  (local  
   (defthm bigger-than-list-max-fn1-map-fn-e0-ord-remove-one
     (implies (equal (fn1 x) (fn1 (max-fn1-list l)))
	      (bigger-than-list (fn1 x) (map-fn-e0-ord (remove-one x l))))
     :hints (("Goal" 
	      :use (:instance bigger-than-list-max-fn1-map-fn-e0-ord-subsetp
			      (m (remove-one x l)))))))

  (local
   (defthm bigger-than-list-insert-e0-ord-<-cons
     (implies (bigger-than-list (fn1 x) l)
	      (equal (insert-e0-ord-< (fn1 x) l)
		     (cons (fn1 x) l)))))
  
  (defthm another-definition-of-map-fn-e0-ord
    (implies (and (equal (fn1 x) (fn1 (max-fn1-list l)))
		  (mp-true-listp l)
		  (member x l))
	     (equal (map-fn-e0-ord l)
		    (cons (fn1 x) (map-fn-e0-ord (remove-one x l)))))
    :hints (("Goal" :use another-definition-of-map-fn-e0-ord-lemma))
    :rule-classes ((:definition :controller-alist ((map-fn-e0-ord t)))))))
 
;;; REMARK: 
;;; It's very interesting the use of this definition rule and
;;; the free variables in it, essential for expanding in an adequate
;;; manner for the induction scheme in map-fn-e0-ord-measure. Note that
;;; this rule has "x" as a free variable. We put the first hypotesis
;;; (equal (fn1 x) (fn1 (max-fn1-list l))), and the rule will only be
;;; used (and "x" conveniently instantiated) if such condition is among
;;; the assumptions. Contrary to most of cases, this is pretty good for
;;; our purpouses. (see "Subgoal *1/6" (where it is used) and "Subgoal
;;; *1/4" (where it is not used) of
;;; map-fn-e0-ord-measure, in the expansion of (map-fn-e0-ord m))

;;; Once we used the following commented rule, but with that rule
;;; definition of map-fn-e0-ord is expanded. This is convenient for
;;; Subgoal *1/6 but not for Subgoal *1/4 where we need
;;;  (map-fn-e0-ord m) to be expanded to the expression :
;;;  (cons (max-fn-list l) (map-fn-e0-ord (remove-one (max-fn-list l) m)))
;;;  and not to the expression:
;;;  (cons (max-fn-list l) (map-fn-e0-ord (remove-one (max-fn-list m) m)))
;;;  Such expression would be obtained if the following rewrite rule
;;;  were used:
;;; (defthm another-definition-of-map-fn-e0-ord-rewrite-rule 
;;;   (implies (and (mp-true-listp l) (consp l)) 
;;;     (equal (map-fn-e0-ord l) 
;;; 	   (cons (fn1 (max-fn1-list l)) 
;;; 		 (map-fn-e0-ord 
;;; 		  (remove-one (max-fn1-list l) l)))))
;;;   :hints (("Goal" 
;;; 	   :use ((:instance 
;;; 		  another-definition-of-map-fn-e0-ord
;;; 		  (x (max-fn1-list l)))))))

;;; Solution: The rule another-definition-of-map-fn-e0-ord-rewrite-rules
;;; (see below) rewrites car and cdr of map-fn-e0-ord and the criteria
;;; of expanding definitions, when applied to e0-ord-<, determines that
;;; those rules are applied in (map-fn-e0-ord l) and NOT in
;;; (map-fn-e0-ord m). In this case, the role of the free variables is
;;; essential.


(local
 (defthm another-definition-of-map-fn-e0-ord-rewrite-rules
   (implies (and (mp-true-listp l)
		 (consp l))
	    (and (equal (car (map-fn-e0-ord l)) (fn1 (max-fn1-list l)))
		 (equal (cdr (map-fn-e0-ord l))
			(map-fn-e0-ord (remove-one (max-fn1-list l) l)))))
   :hints (("Goal" :use (:instance
			 another-definition-of-map-fn-e0-ord
			 (x (max-fn1-list l)))))))

;;; Expansion of the definition of (map-fn-e0-ord l) and (map-fn-e0-ord
;;; m) is always tried. The above rules help the system to satisfy the
;;; criteria for function expansion in the cases where it is really
;;; needed.  (see "Subgoal *1/6" or "Subgoal *1/4" of
;;; map-fn-e0-ord-measure)



;;; Needed for forall-exists-rel-bigger-max-fn1-list
;;; ················································

;;; We prove forall-exists-rel-bigger-max-fn1-list-lemma, establishing
;;; that if (mul-rel n m), and x is in n and not in m, then (fn1 x) is
;;; strictly smaller than (fn1 (max-fn1-list m)). This property will be
;;; used to show forall-exists-rel-bigger-max-fn1-list, essential for
;;; handling cases *1/7 and *1/6 of our map-fn-e0-ord-measure. And also
;;; is used to show
;;; forall-exists-rel-bigger-max-fn1-list-lemma-corollary, for handling
;;; case *1/5

(local
 (defthm member-fn1-ordinal
   (implies (and (member x l) (mp-true-listp l))
	    (e0-ordinalp (fn1 x)))))

(local 
 (defthm mp-true-listp-remove-one
   (implies (mp-true-listp l)
	    (mp-true-listp (remove-one x l)))))


(defthm mp-true-listp-multiset-diff
  (implies (mp-true-listp m)
	   (mp-true-listp (multiset-diff m n))))

(local
 (encapsulate
  ()

  (local
   (defun exists-rel-bigger-witness (x l)
     (declare (xargs :verify-guards nil))
     (cond ((atom l) nil)
	   ((rel x (car l)) (car l))
	   (t (exists-rel-bigger-witness x (cdr l))))))

  (local 
   (defthm exists-rel-bigger-witness-main-property-lemma
     (implies (and (mp-true-listp l) (exists-rel-bigger x l))
	      (mp (exists-rel-bigger-witness x l)))))

  (local
   (defthm exists-rel-bigger-witness-main-property
     (implies (exists-rel-bigger x l)
	      (rel x (exists-rel-bigger-witness x l)))))
  
  (local
   (defthm forall-exists-rel-bigger-lemma
     (implies (and
	       (forall-exists-rel-bigger l1 l2)
	       (member x l1)
	       (mp-true-listp l1)
	       (mp-true-listp l2))
	      (e0-ord-< (fn1 x) (fn1 (exists-rel-bigger-witness x l2))))))
  
  (local
   (defthm member-multiset-diff-exists-rel-bigger-witness-lemma
     (implies (and
	       (forall-exists-rel-bigger l1 l2)
	       (member x l1)
	       (subsetp l2 l3))
	      (member (exists-rel-bigger-witness x l2) l3))))
  
  (local 
   (defthm member-multiset-diff-exists-rel-bigger-witness
     (implies (and
	       (member x n)
	       (not (member x m))
	       (forall-exists-rel-bigger (multiset-diff n m)
					 (multiset-diff m n)))
	      (member (exists-rel-bigger-witness x (multiset-diff m n)) m))))
  
  (defthm forall-exists-rel-bigger-max-fn1-list-lemma
    (implies (and
	      (consp m)
	      (mp-true-listp n)
	      (mp-true-listp m)
	      (member x n)
	      (not (member x m))
	      (forall-exists-rel-bigger (multiset-diff n m)
					(multiset-diff m n)))
	     (e0-ord-< (fn1 x) (fn1 (max-fn1-list m))))
    :hints (("Goal" :use ((:instance
			   e0-ord-<-transitive-corollary
			   (o3 (fn1 x))
			   (o2 (fn1
				(exists-rel-bigger-witness
				 x
				 (multiset-diff m n))))
			   (o1 (fn1 (max-fn1-list m))))))))))




;;; Previous lemmas to map-fn-e0-ord-measure, handling every subgoal
;;; ································································

;;; Needed for "Subgoal *1/8":

(local
 (defthm max-fn1-e0-ordinalp
   (implies (and (consp l) (mp-true-listp l))
	    (e0-ordinalp (fn1 (max-fn1-list l))))))

(local 
 (defthm max-fn1-e0-ord-trichotomy-<
   (implies (and
	     (mp-true-listp n) (mp-true-listp m) (consp n) (consp m)
	     (not (equal (fn1 (max-fn1-list n))
			 (fn1 (max-fn1-list m))))
	     (not (e0-ord-< (fn1 (max-fn1-list n))
			    (fn1 (max-fn1-list m)))))
	    (e0-ord-< (fn1 (max-fn1-list m))
		      (fn1 (max-fn1-list n))))
   :hints (("Goal" 
	    :use (:instance e0-ord-<-trichotomy
			    (o1 (add1-if-integer (fn (max-fn1-list n))))
			    (o2 (add1-if-integer (fn (max-fn1-list m)))))))))

;;; Needed for "Subgoal *1/7":
;;; - another-definition-of-map-fn-e0-ord-rewrite-rules 
;;; - max-fn1-e0-ord-trichotomy-< and

(local
 (defthm forall-exists-rel-bigger-max-fn1-list
   (implies (and (consp n)
		 (consp m)
		 (mp-true-listp n)
		 (mp-true-listp m)
		 (forall-exists-rel-bigger (multiset-diff n m)
					   (multiset-diff m n)))
	    (not (e0-ord-< (fn1 (max-fn1-list m)) (fn1 (max-fn1-list n)))))
   :hints (("Goal" 
	    :use (:instance forall-exists-rel-bigger-max-fn1-list-lemma
			    (x (max-fn1-list n)))
	    :in-theory (enable weak-e0-ord-<-trichotomy)))))


;;; Needed for "Subgoal *1/6":
;;; - another-definition-of-map-fn-e0-ord-rewrite-rules and

(local 
 (defthm consp-map-fn1
   (implies (consp l) (consp (map-fn-e0-ord l)))
   :rule-classes :type-prescription))

;;; Needed for "Subgoal *1/5":
 
(local
 (defthm forall-exists-rel-bigger-max-fn1-list-lemma-corollary
   (implies (and (consp n)
		 (consp m)
		 (mp-true-listp n)
		 (mp-true-listp m)
		 (equal (fn1 (max-fn1-list n))
			(fn1 (max-fn1-list m)))
		 (forall-exists-rel-bigger (multiset-diff n m)
					   (multiset-diff m n)))
	    (member (max-fn1-list n) m))
   :hints (("Goal" :use ((:instance forall-exists-rel-bigger-max-fn1-list-lemma
				    (x (max-fn1-list n))))))))

;;; Needed for "Subgoal *1/4": 
;;;   - another-definition-of-map-fn-e0-ord
;;;   - another-definition-of-map-fn-e0-ord-rewrite-rules
;;;   - max-fn1-list-member
;;;   - mp-true-listp-remove-one 
;;;   - multiset-diff-removing-the-same-element and


;;; Needed for "Subgoal *1/3" and "Subgoal *1/2":
;;;   - multiset-diff-nil

;;; Subgoal *1/1 is solved simply expanding definitions


;;; At last: map-fn-e0-ord-measure.
;;; ·······························

(local
 (encapsulate
  ()

  ;;; Induction scheme.

  (local
   (defun induction-multiset (n m)
     (declare (xargs :measure (acl2::len n)
		     :verify-guards nil))
     (cond ((atom n) (if (atom m) 1 2))
	   ((atom m) 3)
	   (t (let* ((max-m (max-fn1-list m))
		     (max-n (max-fn1-list n))
		     (fn1-max-m (fn1 max-m))
		     (fn1-max-n (fn1 max-n)))
		(cond ((equal fn1-max-m fn1-max-n)
		       (if (member max-n m)
			   (induction-multiset
			    (remove-one max-n n)
			    (remove-one max-n m))
			   5))
		      ((e0-ord-< fn1-max-n fn1-max-m) 6)
		      ((e0-ord-< fn1-max-m fn1-max-n) 7)
		      (t 8)))))))
  
  (defthm map-fn-e0-ord-measure
    (implies (and (mp-true-listp n)
		  (mp-true-listp m)
		  (mul-rel n m))
	     (e0-ord-< (map-fn-e0-ord n)
		       (map-fn-e0-ord m)))
    :hints (("Goal" :induct (induction-multiset n m))))))
	    

;;; ######################################################################## 
;;; THE MAIN THEOREM OF THIS BOOK:
;;; The multiset relation induced by a well-founded relation is well-founded
;;; ########################################################################

;;; The main theorem exported by this book:

(defthm multiset-extension-of-rel-well-founded
  (and (implies (mp-true-listp x) (e0-ordinalp (map-fn-e0-ord x)))
       (implies (and (mp-true-listp x)                   
		     (mp-true-listp y)
		     (mul-rel x y))
		(e0-ord-< (map-fn-e0-ord x) (map-fn-e0-ord y))))
  :rule-classes :well-founded-relation)