		Search-engine friendly clone of the ACL2 documentation.

Pfcs

Lifting

Lifting of PFCSes.

The semantics informally described in semantics can be also formalized in a shallowly embedded way, by defining ACL2 functions that turn (abstract syntax of) expressions and constraints into ACL2 terms and functions that express the semantics. This amounts to lifting deeply embedded PFCSes into a shallowly embedded representation of them.

Here we define these ACL2 functions. We also provide an event macro to turn a deeply embedded PFCS definition to a shallowly embedded version of it, also generating a theorem that relates the two. The theorem says that the satisfaction of the deeply embedded definition is equivalent to the satisfaction of the shallowly embedded one.

Subtopics

Lift-thm: Generate the theorem connecting deeply and shallowly embedded semantics.
Lift-var-name-list: Lift a list of PFCS variable names to a list of ACL2 symbols.
Lift-thm-constr-satp-specialized-lemma: Generate a local lemma to apply constraint-satp-of-relation or constraint-satp-of-relation-when-nofreevars to a specific relation constraint.
Lift-thm-definition-satp-specialized-lemma: Generate a local lemma to apply the definition of definition-satp to a specific definition.
Lift-thm-constr-to-def-satp-specialized-lemmas: Generate local lemmas to apply constraint-satp-to-definition-satp to specific relations.
Lift-info: Fixtype of information about lifted PFCSes.
Lift-var-name: Lift a PFCS variable name to an ACL2 symbol.
Lift-thm-def-hyps: Hypotheses about certain relations having the expected definitions.
Lift-definition: Shallowly embedded semantics of a definition.
Lift-expression: Shallowly embedded semantics of expressions.
Lift-thm-asgfree-pairs: Calculate a list of pairs for constructing a witness assignment to quantified variables.
Lift: Macro to lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.
Lift-thm-free-inst: Calculate an instantiation of free variables.
Lift-fn: Lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.
Lift-thm-type-prescriptions-for-called-preds: List of type prescription rules for the shallowly embedded predicates for the relations called by the definition being lifted.
Lift-rel-name: Lift a PFCS relation name to an ACL2 symbol.
Lift-constraint: Shallowly embedded semantics of a constraint.
Lift-thm-omap-keys-lemma-instances: Calculate lemmas instances for the lifting theorem.
Lift-rules: Some rules used by the lifter.
Lift-table-add: Event to update the table of lifted PFCSes.
Lift-gen-fep-terms: Generate a list of terms (fep x1 p), ..., (fep xn p) from a list of variables x1, ..., xn.
Lift-expression-list: Shallowly embedded semantics of lists of expressions.
Lift-constraint-list: Shallowly embedded semantics of a list of constraints.
Lift-var-name-set-to-list: Lift a set of PFCS variable names to a list of ACL2 symbols.
Lift-thm-asgfree-pairs-aux
Current-package+: Logic-friendly wrapper of the built-in current-package.
Lift-thm-called-lift-thms: List of lifting theorems for a set of relations.
Lift-table: Table of information about lifted PFCSes.