Lift-iso
Lift an isomorphism to an isomorphism on a structure containing the original isoporphism predicate.
Introduction
lift-iso takes a predicate and one or more isomorphisms where the domain predicates
of the isomorphisms are referenced by the predicate, and lifts them to create an isomorphism
from the predicate to a newly created predicate. It is useful for cases where the predicate
specifies a structure that includes components for which isomorphisms exist. It is also
useful for extending an isomorphism to a subdomain. Examples are in lift-iso-tests.lisp.
lift-iso is used by propagate-iso to lift isomorphisms, and it is more general
as it also lifts theorems and functions involving the lifted isomorphism and new predicate.
General Form
(lift-iso pred isomorphism-name-or-names
fn-iso-specs
&key
:iso-name ; Name of new isomorphism
:iso-pred-name ; Name of new predicate
)isomorphism-name-or-names
A single name or a list of names of isomorphisms defined using defiso.
iso-name
The name to be used for the generated isomorphism. If not provided, lift-iso generates
a name from the provided predicate and the isomorphism names.
iso-pred-name
The name to be used for the generated predicate. If not providd,e lift-iso generates
a name from the provided predicate and the isomorphism names.
