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.

- 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.