next up previous contents
Next: The Desktop Environment Up: The Theory Environment Previous: Theorems

Reaxiomatization and Redefinition

Theorems are stored with dependency information, a list of the names of axioms and definitions on which they depend. The dependency structure of a theory can be completely restructured.

The makeanaxiom command can force a theorem to become an axiom; the proveanaxiom command allows one to eliminate an axiom by exhibiting a proof of it from other axioms, with appropriate global dependency modifications. These tools can be used to support the use of lemmas before they are proved.

The defineprimitive command will convert a theorem into a definition of a primitive constant or operator if it has the right form. The redefineconstant or redefineinfix command will replace one definition of a constant or operator (resp.) by another, with appropriate dependency modifications. The undefine operator converts a definition to an axiom.

The elimination of unneeded dependencies on definitions (due to the defined object not being mentioned) should be handled automatically by the proof commands; this is the operational difference between a definition and an axiom. At the moment, however, performance problems with the function which removes unwanted dependencies on definitions make it necessary to remove all automatic applications; the user may apply the temporary reallyremovedefdeps command to effect such reductions of dependencies manually.

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