BasicProvers.export

STRUCTURE

SYNOPSIS

Exports theorems so that they merge with the “stateful” rewriter’s simpset.

DESCRIPTION

A call to export_rewrites strlist causes the theorems named by the strings in strlist to be merged into the simpset value maintained behind the function srw_ss(), both in the current session and also when the theory generated by the script file is loaded.

Theorems are named by giving the name of the segment, a full-stop (or period) character, and the name of theorem. If the theorem is in the current segment, the segment can be omitted. Thus, if working in the development of the theory of lists, the following are valid names list.MAP_GENLIST, MAP_GENLIST and arithmetic.LESS_TRANS.

The theory is also augmented with an element in its signature of the form <thyname>_rwts of type simpLib.ssfrag. This value is the collection of all the theorems specified in calls to export_rewrites.

Multiple calls to export_rewrites cumulatively add to the list of theorems being exported.

FAILURE

Fails if any of the strings in the list does not name a theorem in the current context.

COMMENTS

This function is useful for ensuring that the stateful rewriter is augmented as theories are loaded. This in turn means that users of these theories don’t need to learn the names of their “obvious” theorems. Because theorems can not be removed from the stateful rewriter’s underlying simpset, choice of “obvious” theorems needs to be done with care.

SEEALSO

augment_srw_ss, srw_ss, SRW_TAC