next up previous contents
Next: Places where bugs are Up: The Desktop Environment Previous: Theory Management

Views and Theorem Export

A view is an interpretation of a subset of a source theory in a target theory, implemented as a set of translations of names of constants and operators. Views reside in the source theory; they are saved in theory files.

Views are constructed using the declareview command, which creates a trivial view with the predeclared constants and operators interpreted as themselves. They can be edited using the viewasin, viewasselfin, and dropfromview commands.

Views are used to export theorems from the theory in which they reside (the source theory) to another theory (the target theory). The target theory needs to be saved on the desktop. The theorem export functions exportthmlist and exportthm, given a view, information about default prefixes to add to automatically generated names of constants and operators, a single theorem or list of theorems to be exported, and a target theory, will retrieve the target theory from the desktop, automatically check the validity of the view and extend it if necessary (the view must at lest include interpretations of all axioms and definitions on which the exported theorems depend, and often does not need to include more than this; the rest can usually be deduced), and generate analogous theorems in the target theory, guaranteed to be valid theorems of the target theory. The facility will automatically avoid name conflicts by adding additional prefixes to automatically generated names. If a tactic is exported, it will automatically determine what other theorems need to be exported and translate them as well; complex mutually recursive systems of tactics can be exported reliably. A reason to extend views beyond the minimal level of axioms and definitions is to avoid the copying of frequently used theorems found in many theories.

The theorem export commands can be finicky about defined notions in the source theory; these need to match defined notions in the target theory with analogous definitions. The redefinition facilities might be useful in avoiding problems with this.

The theorem export commands do not export module structure; they will export modules but they are unpacked completely.


next up previous contents
Next: Places where bugs are Up: The Desktop Environment Previous: Theory Management

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997