		Search-engine friendly clone of the ACL2 documentation.

Propagate-iso

Propagate an isomorphism from a set of isomorphically transformed functions to events that use them.

Introduction

propagate-iso takes one or more isomorphisms and a set of functions and a sequence of events and propagates the isomorphisms from the given set of functions to those events that reference any of these functions either directly or directly. It maintains a substitution from old functions to their new isomorphic functions. For function definitions it creates a new function by applying the substitution to the old body and extends the substitution to map the old function name to the newly created function name. Similarly, it applies the substitution to existing theorems to generate theorems on the new functions. Currently does not handle mutual recursion.

General Form

(propagate-iso isomorphism-name-or-names
               fn-iso-specs
               &key
               :first-event       ; required name of an event
               :last-event        ; required name of an event
               :dont-verify-guards   ; default nil
               :enabled           ; default nil
               :iso-rules         ; default nil
               :osi-rules         ; default nil
               :hints-map         ; default nil
               )

isomorphism-name-or-names

A single name or a list of names of isomorphisms defined using defiso.

fn-iso-specs

A list of functions associated with information about their isomorphics translations and signatures. Each element of the list has the form:
(fn iso-fn fn-->iso-fn--thm iso-fn-->fn--thm arg-sig => result-sig)
where iso-fn is the isomorphic version of fn and fn-->iso-fn--thm is a theorem for rewriting fn to iso-fn, and and iso-fn-->fn--thm is a theorem for rewriting iso-fn to fn. arg-sig gives the signature of the argument list of fn with respect to the isomorphism, i.e. if an argument of fn is of one of the isomorphism types (predicate) then the corresponding element of the signature is that predicate, otherwise it is *. Similarly, if fn returns a single value then it is * or the name of an isomorphism predicate, or if it returns multiple values then it is a list of such values.

:first-event and :last-event

These give the first and last event that propagate-iso considers. Functions definitions and theorems are ignored if they do not reference any of the functions in fn-iso-specs or any of the functions for which propagate-iso has already generated an isomorphic version.

The remaining options are only useful in the cases where the hints generated by propagate-iso are not sufficient to allow any proofs to go through.

:dont-verify-guards

T means do not verify guards of any of the generated events.

:enabled

A list of runes to use in proofs to add to the lists that propagate-iso determines to be appropriate.

:iso-rules

A list of runes to use in proofs for theorems where propagate-iso is using a strategy that transforms old functions into new functions.

:osi-rules

A list of runes to use in proofs for theorems where propagate-iso is using a strategy that transforms new functions into old functions.

propagate-iso ensures that rules in :iso-rules and :osi-rules are not enabled at the same time.

:hints-map

Used to override or augment the hints generated by propagate-iso