New Implementation of Mark2

Facilities of the old implementation which are not present in the new but which are seldom if ever used at present are user-defined precedence and the "functional programming" features (these features have since been added, but are still not often used).. A major aim of the reimplementation is the installation of a more efficient system for keeping track of different kinds of dependencies, which, it is hoped, will allow reaxiomatization, redefinition, and theorem export facilities to be made usable in practice (this has now been put into practice for forget and theorem export)

The files for the new version are mirrored in my home directory at the University of Idaho: the source is "design", the executable is "Watson", and all the .wat files below are found there, and the corresponding saved theory files (with extension .sav.wat) have been built there. I plan to rebuild these each time I upgrade the executable significantly. The new version is functionally similar but not identical to the current implementation. There follows a list detailing points of difference:

• dependencies: The prover displays dependencies in a Mark2 term format as a list. The last element of the list will be 0, which I use by convention as a list terminator. Dependencies of 0 signal no dependencies on axioms at all. The new version only records dependencies on axioms which have actually been applied; embedded theorems in tactics do not induce dependencies, so many tactics which have extensive dependencies under the old version have none under this version (but applying the tactic does induce dependencies as expected). The restriction on the "reprove" command that it not add dependencies has been removed.
• more dependencies: The prover now records definition dependencies and "theorem text dependencies". A theorem acquires a theorem text dependency on another theorem when it calls the other theorem as a tactic, for example. These dependencies can be viewed by using a new command "showalldeps" which takes the name of a theorem as a parameter; normally the prover will only display axiomatic dependencies. It does now remove superfluous dependencies on definitions, a feature which I had to remove from the old prover because it caused serious performance problems.
• strict prefix operators: Although the overloading of infixes as prefixes with "invisible" left subterms is still supported, the prover now allows (and takes as the default) the declaration of strict prefix operators, which have no right subterm.
• case expressions: Case expressions no longer have an immediate right subterm; you can look at the apparent right subterm, but you can't do anything to it.
• structural tactics: Since a term like ?x^+?y does not match a strict prefix expression or a case expression, structural tactics like LEFT, RIGHT and EVERYWHERE need to be implemented with cases. RIGHT doesn't work at all anymore on case expressions; new tactics LEFT_CASE and RIGHT_CASE are provided to apply theorems to the left and right subterms of the "virtual" right subterm of a case expression. This is already implemented in the script structural2.mk2 below.
• more on case expressions: Hypotheses of the forms true = ?p and ?p (where ?p is not an equation) are now indistinguishable to the prover, and the tactic interpreter will convert any hypothesis of the form true=?p to ?p. This has the further effect that case expressions with the hypotheses true=true and true=false are automatically collapsed in the same way that case expressions with hypotheses true and false were already.
• new variables: When the new prover introduces new variables, it does not necessarily apply the same index to them (this is just as likely to be caused by rewrites of commonly used tactics). Also, this prover is less likely to present a new variable as a function applied to a bound variable.
• special navigation commands: The commands upto,downtoleft, downtoright, and the dlls family do not have precisely the same behavior. I have yet to find a script where this made a difference. One advantage is that the upto command can now be repeated; it does not check the term where you are.
• alternative rule infixes: Alternative theorem applications are now represented in a different way. The effect of the altruleintro and altrevruleintro commands is intended to be the same, but the appearance of the resulting embedded theorem will be different. on-success rule infixes: These infixes (*>, <*) have the order of their arguments reversed. I don't think that any users other than myself have used these, but they are found in structural and typestuff scripts. The change of order was made to bring them into analogy with the new alternative infixes.
• synthetic abstraction: Synthetic abstraction is no longer supported. Operators (prefixes or infixes) beginning with a colon are now free to be used like any other operator.
• error messages: Error messages are generally more informative.
• saved theory files: These have the extension .sav.wat and are entirely different in format from the saved theory files of the old version. These saved theory files are actually scripts. The load and save facilities are a little slower than the old prover's load and save. Save files now include additional information, such as what scripts have been run!
• views and theorem export: The July 1 version supports theorem export. Use commands declareview x (creates a view named x which translates predeclared objects to themselves), addtoview x y z (causes view x to translate y to z) to construct a view. Generally, setting up a correspondence between axioms will do the trick (the prover matches axioms to extend views as needed); an exception exists for operator variables, which do need to be associated with operator variables in the target theory by the view. The command "exportthm view target suffix thm" will, if run in the source theory where theorem thm lives, translate thm and all the theorems it depends on (if it is a tactic, for example) using the view "view", and prove these in the remote theory "target" (which needs to exist on the desktop); the argument "suffix" is used to generate new theorem names where needed to avoid name collisions. Views are not saved, but the view and exportthm commands are supported in scripts. The exportthm command is still rather unstable and may do odd things. It is, however, reasonably fast!

Here are the Watson scripts. Be aware that Watson and the last release of Mark2 are not perfectly compatible; scripts to be run with the last release of Mark2 are found below.

Here is the new Watson page Here is the old Mark2 page.