definj

(in-package "ACL2")

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

(define definj-lookup
  ((name symbolp) (wrld plist-worldp))
  :returns (info? "A @(tsee maybe-defmapping-infop).")
  :verify-guards nil
  :short "Return the information for the @(tsee definj) specified by name,
          or @('nil') if there is no @(tsee definj) with that name."
  :long (topstring-p "This is a wrapper of @(tsee defmapping-lookup)
    that makes sure that the @($\alpha$) conversion is an injection
    (and also that the left inverse @($\beta$) conversion is a surjection),
    i.e. that it has the @(':beta-of-alpha') theorem.
    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)))
    info))

(defsection definj-macro-definition
  :short "Definition of the @(tsee definj) macro."
  :long (topstring (p "We call @(tsee defmapping-fn),
     passing @('t') as @(':alpha-of-beta-thm')
     and @('nil') as @(':beta-of-alpha-thm').
     Furthermore, we set the context to reference @(tsee definj).")
    (@def "definj"))
  (defmacro definj
    (&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
        nil
        ',GUARD-THMS
        ',UNCONDITIONAL
        ',THM-NAMES
        ',THM-ENABLE
        ',HINTS
        ',PRINT
        ',SHOW-ONLY
        ',CALL
        (cons 'definj ',NAME)
        state)
      :suppress-errors ,(NOT PRINT))))