		Search-engine friendly clone of the ACL2 documentation.

Semantics

Lifting

Lifting from deeply to shallowly embedded semantics.

The shallowly embedded semantics of PFCSes includes an ACL2 function sesem-definition to turn a deeply embedded PFCS definition into a shallowly embedded PFCS definition. The two must and can be related formally: the satisfaction of the deeply embedded definition is equivalent to the satisfaction of the shallowly embedded one.

Here we explicate this formal relation, via ACL2 code that maps a deeply embedded PFCS definition not only to a shallowly embedded version of it, but also to a theorem that relates the two. This is a form of lifting: a deeply embedded definition is lifted to a shallowly embedded one. The latter is easier to reason about, and anything proved about it can be extended to the deeply embedded definition by using the lifting theorem generated here.

Subtopics

Lift-thm: Generate the theorem connecting deeply and shallowly embedded semantics.
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-thm-def-hyps: Hypotheses about certain relations having the expected definitions.
Lift-thm-asgfree-pairs: Calculate a list of pairs for constructing a witness assignment to quantified variables.
Lift-thm-free-inst: Calculate an instantiation of free variables.
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-fn: Lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.
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: Macro to lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.
Lift-thm-asgfree-pairs-aux
Lift-thm-called-lift-thms: List of lifting theorems for a set of relations.
Lift-table: Table of information about lifted PFCSes.