defmapping-templates

other

(in-package "ACL2")

gen-eqsfunction

(defun gen-eqs
  (lefts rights)
  (cond ((or (atom lefts) (atom rights)) nil)
    (t (cons `(equal ,(CAR LEFTS) ,(CAR RIGHTS))
        (gen-eqs (cdr lefts) (cdr rights))))))

defthm-alpha-imagemacro

(defmacro defthm-alpha-image
  (&key (name 'alpha-image)
    (a1...an '(a))
    (b1...bm '(b))
    (doma 'doma)
    (domb 'domb)
    (alpha 'alpha))
  `(defthm ,NAME
    (implies (,DOMA ,@A1...AN)
      ,(IF (= (LEN B1...BM) 1)
     `(,DOMB (,ALPHA ,@A1...AN))
     `(MV-LET ,B1...BM (,ALPHA ,@A1...AN) (,DOMB ,@B1...BM))))))

defthm-beta-imagemacro

(defmacro defthm-beta-image
  (&key (name 'beta-image)
    (a1...an '(a))
    (b1...bm '(b))
    (doma 'doma)
    (domb 'domb)
    (beta 'beta))
  `(defthm ,NAME
    (implies (,DOMB ,@B1...BM)
      ,(IF (= (LEN A1...AN) 1)
     `(,DOMA (,BETA ,@B1...BM))
     `(MV-LET ,A1...AN (,BETA ,@B1...BM) (,DOMA ,@A1...AN))))))

defthm-beta-of-alphamacro

(defmacro defthm-beta-of-alpha
  (&key (name 'beta-of-alpha)
    (a1...an '(a))
    (b1...bm '(b))
    (doma 'doma)
    (alpha 'alpha)
    (beta 'beta)
    aa1...aan
    unconditional)
  (let ((core (if (= (len a1...an) 1)
         (if (= (len b1...bm) 1)
           `(equal (,BETA (,ALPHA ,(CAR A1...AN))) ,(CAR A1...AN))
           `(mv-let ,B1...BM
             (,ALPHA ,@A1...AN)
             (equal (,BETA ,@B1...BM) ,(CAR A1...AN))))
         (if (= (len b1...bm) 1)
           `(mv-let ,AA1...AAN
             (,BETA (,ALPHA ,@A1...AN))
             (and ,@(GEN-EQS AA1...AAN A1...AN)))
           `(mv-let ,B1...BM
             (,ALPHA ,@A1...AN)
             (mv-let ,AA1...AAN
               (,BETA ,@B1...BM)
               (and ,@(GEN-EQS AA1...AAN A1...AN))))))))
    (if unconditional
      `(defthm ,NAME ,CORE)
      `(defthm ,NAME (implies (,DOMA ,@A1...AN) ,CORE)))))

defthm-alpha-of-betamacro

(defmacro defthm-alpha-of-beta
  (&key (name 'alpha-of-beta)
    (a1...an '(a))
    (b1...bm '(b))
    (domb 'domb)
    (alpha 'alpha)
    (beta 'beta)
    bb1...bbm
    unconditional)
  (let ((core (if (= (len b1...bm) 1)
         (if (= (len a1...an) 1)
           `(equal (,ALPHA (,BETA ,(CAR B1...BM))) ,(CAR B1...BM))
           `(mv-let ,A1...AN
             (,BETA ,@B1...BM)
             (equal (,ALPHA ,@A1...AN) ,(CAR B1...BM))))
         (if (= (len a1...an) 1)
           `(mv-let ,BB1...BBM
             (,ALPHA (,BETA ,@B1...BM))
             (and ,@(GEN-EQS BB1...BBM B1...BM)))
           `(mv-let ,A1...AN
             (,BETA ,@B1...BM)
             (mv-let ,BB1...BBM
               (,ALPHA ,@A1...AN)
               (and ,@(GEN-EQS BB1...BBM B1...BM))))))))
    (if unconditional
      `(defthm ,NAME ,CORE)
      `(defthm ,NAME (implies (,DOMB ,@B1...BM) ,CORE)))))

defthm-alpha-injectivemacro

(defmacro defthm-alpha-injective
  (&key (name 'alpha-injective)
    (a1...an '(a))
    (aa1...aan '(aa))
    (doma 'doma)
    (alpha 'alpha)
    unconditional
    hints)
  (let ((core `(equal (equal (,ALPHA ,@A1...AN) (,ALPHA ,@AA1...AAN))
         ,(IF (= (LEN A1...AN) 1)
     `(EQUAL ,(CAR A1...AN) ,(CAR AA1...AAN))
     `(AND ,@(GEN-EQS A1...AN AA1...AAN))))))
    (if unconditional
      `(defthm ,NAME ,CORE ,@(AND HINTS (LIST :HINTS HINTS)))
      `(defthm ,NAME
        (implies (and (,DOMA ,@A1...AN) (,DOMA ,@AA1...AAN)) ,CORE)
        ,@(AND HINTS (LIST :HINTS HINTS))))))

defthm-beta-injectivemacro

(defmacro defthm-beta-injective
  (&key (name 'beta-injective)
    (b1...bm '(b))
    (bb1...bbm '(bb))
    (domb 'domb)
    (beta 'beta)
    unconditional
    hints)
  (let ((core `(equal (equal (,BETA ,@B1...BM) (,BETA ,@BB1...BBM))
         ,(IF (= (LEN B1...BM) 1)
     `(EQUAL ,(CAR B1...BM) ,(CAR BB1...BBM))
     `(AND ,@(GEN-EQS B1...BM BB1...BBM))))))
    (if unconditional
      `(defthm ,NAME ,CORE ,@(AND HINTS (LIST :HINTS HINTS)))
      `(defthm ,NAME
        (implies (and (,DOMB ,@B1...BM) (,DOMB ,@BB1...BBM)) ,CORE)
        ,@(AND HINTS (LIST :HINTS HINTS))))))

defthm-doma-guardmacro

(defmacro defthm-doma-guard
  (&key (name 'doma-guard) (a1...an '(a)) (g-doma 'g-doma))
  `(defthm ,NAME (,G-DOMA ,@A1...AN)))

defthm-domb-guardmacro

(defmacro defthm-domb-guard
  (&key (name 'domb-guard) (b1...bm '(b)) (g-domb 'g-domb))
  `(defthm ,NAME (,G-DOMB ,@B1...BM)))

defthm-alpha-guardmacro

(defmacro defthm-alpha-guard
  (&key (name 'alpha-guard)
    (a1...an '(a))
    (doma 'doma)
    (g-alpha 'g-alpha))
  `(defthm ,NAME
    (implies (,DOMA ,@A1...AN) (,G-ALPHA ,@A1...AN))))

defthm-beta-guardmacro

(defmacro defthm-beta-guard
  (&key (name 'beta-guard)
    (b1...bm '(b))
    (domb 'domb)
    (g-beta 'g-beta))
  `(defthm ,NAME
    (implies (,DOMB ,@B1...BM) (,G-BETA ,@B1...BM))))

defthm-allmacro

(defmacro defthm-all
  (&key (alpha-image 'alpha-image)
    (beta-image 'beta-image)
    (beta-of-alpha 'beta-of-alpha)
    (alpha-of-beta 'alpha-of-beta)
    (alpha-injective 'alpha-injective)
    (beta-injective 'beta-injective)
    (doma-guard 'doma-guard)
    (domb-guard 'domb-guard)
    (alpha-guard 'alpha-guard)
    (beta-guard 'beta-guard)
    unconditional
    (doma 'doma)
    (domb 'domb)
    (alpha 'alpha)
    (beta 'beta)
    (g-doma 'g-doma)
    (g-domb 'g-domb)
    (g-alpha 'g-alpha)
    (g-beta 'g-beta)
    (a1...an '(a))
    (b1...bm '(b))
    (aa1...aan '(a$))
    (bb1...bbm '(b$)))
  `(progn (defthm-alpha-image :name ,ALPHA-IMAGE
      :a1...an ,A1...AN
      :b1...bm ,B1...BM
      :doma ,DOMA
      :domb ,DOMB
      :alpha ,ALPHA)
    (defthm-beta-image :name ,BETA-IMAGE
      :a1...an ,A1...AN
      :b1...bm ,B1...BM
      :doma ,DOMA
      :domb ,DOMB
      :beta ,BETA)
    ,@(AND BETA-OF-ALPHA
       `((DEFTHM-BETA-OF-ALPHA :NAME ,BETA-OF-ALPHA :A1...AN ,A1...AN :B1...BM
          ,B1...BM :DOMA ,DOMA :ALPHA ,ALPHA :BETA ,BETA :AA1...AAN ,AA1...AAN
          :UNCONDITIONAL ,UNCONDITIONAL)))
    ,@(AND ALPHA-OF-BETA
       `((DEFTHM-ALPHA-OF-BETA :NAME ,ALPHA-OF-BETA :A1...AN ,A1...AN :B1...BM
          ,B1...BM :DOMB ,DOMB :ALPHA ,ALPHA :BETA ,BETA :BB1...BBM ,BB1...BBM
          :UNCONDITIONAL ,UNCONDITIONAL)))
    ,@(AND ALPHA-INJECTIVE
       `((DEFTHM-ALPHA-INJECTIVE :NAME ,ALPHA-INJECTIVE :A1...AN ,A1...AN
          :AA1...AAN ,AA1...AAN :DOMA ,DOMA :ALPHA ,ALPHA :UNCONDITIONAL
          ,UNCONDITIONAL)))
    ,@(AND BETA-INJECTIVE
       `((DEFTHM-BETA-INJECTIVE :NAME ,BETA-INJECTIVE :B1...BM ,B1...BM
          :BB1...BBM ,BB1...BBM :DOMB ,DOMB :BETA ,BETA :UNCONDITIONAL
          ,UNCONDITIONAL)))
    ,@(AND DOMA-GUARD
       `((DEFTHM-DOMA-GUARD :NAME ,DOMA-GUARD :A1...AN ,A1...AN :G-DOMA
          ,G-DOMA)))
    ,@(AND DOMB-GUARD
       `((DEFTHM-DOMB-GUARD :NAME ,DOMB-GUARD :B1...BM ,B1...BM :G-DOMB
          ,G-DOMB)))
    ,@(AND ALPHA-GUARD
       `((DEFTHM-ALPHA-GUARD :NAME ,ALPHA-GUARD :A1...AN ,A1...AN :DOMA ,DOMA
          :G-ALPHA ,G-ALPHA)))
    ,@(AND BETA-GUARD
       `((DEFTHM-BETA-GUARD :NAME ,BETA-GUARD :B1...BM ,B1...BM :DOMB ,DOMB
          :G-BETA ,G-BETA)))))

definputs-guarded-1-1macro

(defmacro definputs-guarded-1-1
  nil
  '(encapsulate (((doma *) => * :formals (a) :guard (g-doma a)) ((domb *) => * :formals (b) :guard (g-domb b))
      ((alpha *) => * :formals (a) :guard (g-alpha a))
      ((beta *) => * :formals (b) :guard (g-beta b))
      ((g-doma *) => *)
      ((g-domb *) => *)
      ((g-alpha *) => *)
      ((g-beta *) => *))
    (local (defun doma (a) (declare (ignore a)) t))
    (local (defun domb (b) (declare (ignore b)) t))
    (local (defun alpha (a) a))
    (local (defun beta (b) b))
    (local (defun g-doma (a) (declare (ignore a)) t))
    (local (defun g-domb (b) (declare (ignore b)) t))
    (local (defun g-alpha (a) (doma a)))
    (local (defun g-beta (b) (domb b)))
    (defthm-alpha-image)
    (defthm-beta-image)
    (defthm-beta-of-alpha)
    (defthm-alpha-of-beta)
    (defthm-beta-of-alpha :name beta-of-alpha-uncond
      :unconditional t)
    (defthm-alpha-of-beta :name alpha-of-beta-uncond
      :unconditional t)
    (defthm-doma-guard)
    (defthm-domb-guard)
    (defthm-alpha-guard)
    (defthm-beta-guard)
    (in-theory (disable alpha-image
        beta-image
        beta-of-alpha
        alpha-of-beta
        beta-of-alpha-uncond
        alpha-of-beta-uncond
        doma-guard
        domb-guard
        alpha-guard
        beta-guard))))

definputs-guarded-2-1macro

(defmacro definputs-guarded-2-1
  nil
  '(encapsulate (((doma * *) => * :formals (a1 a2) :guard (g-doma a1 a2)) ((domb *) => * :formals (b) :guard (g-domb b))
      ((alpha * *) => * :formals (a1 a2) :guard (g-alpha a1 a2))
      ((beta *) => (mv * *) :formals (b) :guard (g-beta b))
      ((g-doma * *) => *)
      ((g-domb *) => *)
      ((g-alpha * *) => *)
      ((g-beta *) => *))
    (local (defun doma (a1 a2) (declare (ignore a1 a2)) t))
    (local (defun domb (b) (consp b)))
    (local (defun alpha (a1 a2) (cons a1 a2)))
    (local (defun beta (b) (mv (car b) (cdr b))))
    (local (defun g-doma (a1 a2) (declare (ignore a1 a2)) t))
    (local (defun g-domb (b) (declare (ignore b)) t))
    (local (defun g-alpha (a1 a2) (doma a1 a2)))
    (local (defun g-beta (b) (domb b)))
    (defthm-alpha-image :a1...an (a1 a2))
    (defthm-beta-image :a1...an (a1 a2))
    (defthm-beta-of-alpha :a1...an (a1 a2) :aa1...aan (aa1 aa2))
    (defthm-alpha-of-beta :a1...an (a1 a2))
    (defthm-doma-guard :a1...an (a1 a2))
    (defthm-domb-guard)
    (defthm-alpha-guard :a1...an (a1 a2))
    (defthm-beta-guard)
    (in-theory (disable alpha-image
        beta-image
        beta-of-alpha
        alpha-of-beta
        doma-guard
        domb-guard
        alpha-guard
        beta-guard))))

definputs-guarded-1-2macro

(defmacro definputs-guarded-1-2
  nil
  '(encapsulate (((doma *) => * :formals (a) :guard (g-doma a)) ((domb * *) => * :formals (b1 b2) :guard (g-domb b1 b2))
      ((alpha *) => (mv * *) :formals (a) :guard (g-alpha a))
      ((beta * *) => * :formals (b1 b2) :guard (g-beta b1 b2))
      ((g-doma *) => *)
      ((g-domb * *) => *)
      ((g-alpha *) => *)
      ((g-beta * *) => *))
    (local (defun doma (a) (consp a)))
    (local (defun domb (b1 b2) (declare (ignore b1 b2)) t))
    (local (defun alpha (a) (mv (car a) (cdr a))))
    (local (defun beta (b1 b2) (cons b1 b2)))
    (local (defun g-doma (a) (declare (ignore a)) t))
    (local (defun g-domb (b1 b2) (declare (ignore b1 b2)) t))
    (local (defun g-alpha (a) (doma a)))
    (local (defun g-beta (b1 b2) (domb b1 b2)))
    (defthm-alpha-image :b1...bm (b1 b2))
    (defthm-beta-image :b1...bm (b1 b2))
    (defthm-beta-of-alpha :b1...bm (b1 b2))
    (defthm-alpha-of-beta :b1...bm (b1 b2) :bb1...bbm (bb1 bb2))
    (defthm-doma-guard)
    (defthm-domb-guard :b1...bm (b1 b2))
    (defthm-alpha-guard)
    (defthm-beta-guard :b1...bm (b1 b2))
    (in-theory (disable alpha-image
        beta-image
        beta-of-alpha
        alpha-of-beta
        doma-guard
        domb-guard
        alpha-guard
        beta-guard))))

definputs-guarded-2-2macro

(defmacro definputs-guarded-2-2
  nil
  '(encapsulate (((doma * *) => * :formals (a1 a2) :guard (g-doma a1 a2)) ((domb * *) => * :formals (b1 b2) :guard (g-domb b1 b2))
      ((alpha * *) =>
        (mv * *)
        :formals (a1 a2)
        :guard (g-alpha a1 a2))
      ((beta * *) =>
        (mv * *)
        :formals (b1 b2)
        :guard (g-beta b1 b2))
      ((g-doma * *) => *)
      ((g-domb * *) => *)
      ((g-alpha * *) => *)
      ((g-beta * *) => *))
    (local (defun doma (a1 a2) (declare (ignore a1 a2)) t))
    (local (defun domb (b1 b2) (declare (ignore b1 b2)) t))
    (local (defun alpha (a1 a2) (mv a1 a2)))
    (local (defun beta (b1 b2) (mv b1 b2)))
    (local (defun g-doma (a1 a2) (declare (ignore a1 a2)) t))
    (local (defun g-domb (b1 b2) (declare (ignore b1 b2)) t))
    (local (defun g-alpha (a1 a2) (doma a1 a2)))
    (local (defun g-beta (b1 b2) (domb b1 b2)))
    (defthm-alpha-image :a1...an (a1 a2) :b1...bm (b1 b2))
    (defthm-beta-image :a1...an (a1 a2) :b1...bm (b1 b2))
    (defthm-beta-of-alpha :a1...an (a1 a2)
      :b1...bm (b1 b2)
      :aa1...aan (aa1 aa2))
    (defthm-alpha-of-beta :a1...an (a1 a2)
      :b1...bm (b1 b2)
      :bb1...bbm (bb1 bb2))
    (defthm-beta-of-alpha :name beta-of-alpha-uncond
      :a1...an (a1 a2)
      :b1...bm (b1 b2)
      :aa1...aan (aa1 aa2)
      :unconditional t)
    (defthm-alpha-of-beta :name alpha-of-beta-uncond
      :a1...an (a1 a2)
      :b1...bm (b1 b2)
      :bb1...bbm (bb1 bb2)
      :unconditional t)
    (defthm-doma-guard :a1...an (a1 a2))
    (defthm-domb-guard :b1...bm (b1 b2))
    (defthm-alpha-guard :a1...an (a1 a2))
    (defthm-beta-guard :b1...bm (b1 b2))
    (in-theory (disable alpha-image
        beta-image
        beta-of-alpha
        alpha-of-beta
        doma-guard
        domb-guard
        alpha-guard
        beta-guard))))

enable-allmacro

(defmacro enable-all
  nil
  `(in-theory (enable alpha-image
      beta-image
      beta-of-alpha
      alpha-of-beta
      doma-guard
      domb-guard
      alpha-guard
      beta-guard)))

enable-all-uncondmacro

(defmacro enable-all-uncond
  nil
  `(in-theory (enable alpha-image
      beta-image
      beta-of-alpha-uncond
      alpha-of-beta-uncond
      doma-guard
      domb-guard
      alpha-guard
      beta-guard)))