• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
        • Proof-support
        • Semantics
        • Lifting
          • Lift-thm
          • Lift-var-name-list
          • Lift-thm-constr-satp-specialized-lemma
          • Lift-thm-definition-satp-specialized-lemma
          • Lift-thm-constr-to-def-satp-specialized-lemmas
          • Lift-info
          • Lift-var-name
          • Lift-thm-def-hyps
          • Lift-definition
          • Lift-expression
          • Lift-thm-asgfree-pairs
          • Lift
            • Lift-thm-free-inst
            • Lift-fn
            • Lift-thm-type-prescriptions-for-called-preds
            • Lift-rel-name
            • Lift-constraint
            • Lift-thm-omap-keys-lemma-instances
            • Lift-rules
            • Lift-table-add
            • Lift-gen-fep-terms
            • Lift-expression-list
            • Lift-constraint-list
            • Lift-var-name-set-to-list
            • Lift-thm-asgfree-pairs-aux
            • Current-package+
            • Lift-thm-called-lift-thms
            • Lift-table
          • R1cs-subset
          • Indexed-names
          • Well-formedness
          • Abstract-syntax
          • Concrete-syntax
          • R1cs-bridge
          • Parser-interface
        • Wp-gen
        • Dimacs-reader
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Riscv
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Lifting

    Lift

    Macro to lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.

    The required argument must be a ground form that evaluates to a PFCS definition. The form is evaluated and the resulting definition is processed.

    The pred keyword argument, if present, must be a symbol to use as the name of the predicate the constitutes the generated shallowly embedded PFCS definition. If omitted, the default is nil, which means that the predicate name is determined according to the same mapping as for PFCS variables. This input is quoted (not evaluated) for processing.

    The prime keyword argument, if present, must be a symbol to use as the prime that parameterizes the PFCS semantics. It is p by default. This is quoted (not evaluated) for processing.

    Macro: lift

    (defmacro lift (def &key pred (prime 'p))
     (cons 'make-event
           (cons (cons 'lift-fn
                       (cons def
                             (cons (cons 'quote (cons pred 'nil))
                                   (cons (cons 'quote (cons prime 'nil))
                                         '(state)))))
                 'nil)))