export_rewrites

BasicProvers.export_rewrites : string list -> unit

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

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 collection of all the theorems specified in calls to export_rewrites can be obtained as a value of type simpLib.ssfrag using the thy_ssfrag function.

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.

See also

bossLib.augment_srw_ss, bossLib.srw_ss, bossLib.SRW_TAC, BasicProvers.thy_ssfrag