defiso

(in-package "ACL2")

(defxdoc+ defiso-implementation
  :parents (defiso)
  :short "Implementation of @(tsee defiso)."
  :long (topstring (p "We implement @(tsee defiso) as a thin wrapper of @(tsee defmapping).
     We also provide a programmatic interface
     to retrieve isomorphic mappings from the "
      (seetopic "defmapping-table" "@('defmapping') table")
      "."))
  :order-subtopics t
  :default-parent t)

(define defiso-lookup
  ((name symbolp) (wrld plist-worldp))
  :returns (info? "A @(tsee maybe-defmapping-infop).")
  :verify-guards nil
  :short "Return the information for the @(tsee defiso) specified by name,
          or @('nil') if there is no @(tsee defiso) with that name."
  :long (topstring-p "This is a wrapper of @(tsee defmapping-lookup)
    that makes sure that the mapping is an isomorphism,
    i.e. that it has
    both the @(':beta-of-alpha') and @(':alpha-of-beta') theorems.
    It causes an error if that is not the case.")
  (b* ((info (defmapping-lookup name wrld)) ((when (not info)) nil)
      ((when (not (defmapping-info->beta-of-alpha info))) (raise "The mapping ~x0 does not have the :BETA-OF-ALPHA theorem."
          name))
      ((when (not (defmapping-info->alpha-of-beta info))) (raise "The mapping ~x0 does not have the :ALPHA-OF-BETA theorem."
          name)))
    info))

(defsection defiso-macro-definition
  :short "Definition of the @(tsee defiso) macro."
  :long (topstring (p "We call @(tsee defmapping-fn),
     passing @('t') as
     both @(':beta-of-alpha-thm') and @(':alpha-of-beta-thm').
     Furthermore, we set the context to reference @(tsee defiso).")
    (@def "defiso"))
  (defmacro defiso
    (&whole call
      name
      doma
      domb
      alpha
      beta
      &key
      (unconditional 'nil)
      (guard-thms 't)
      (thm-names 'nil)
      (thm-enable 'nil)
      (hints 'nil)
      (print ':result)
      (show-only 'nil))
    `(make-event-terse (defmapping-fn ',NAME
        ',DOMA
        ',DOMB
        ',ALPHA
        ',BETA
        t
        t
        ',GUARD-THMS
        ',UNCONDITIONAL
        ',THM-NAMES
        ',THM-ENABLE
        ',HINTS
        ',PRINT
        ',SHOW-ONLY
        ',CALL
        (cons 'defiso ',NAME)
        state)
      :suppress-errors ,(NOT PRINT))))