Next: Library Documentation Up: New features in LEGO Version 1.3 Previous: Theorems and Configure Theorems

LEGO Version 1.3: UTac

Lego is written in ML. We provide two binaries, lego and legoML. The latter gives you a toplevel of ML in which lego is executed as a function. The command Drop returns you to the ML toplevel. There, you can define any ML function you like e.g., a fancy decision procedure, and execute it to ease some tedious aspects in your proof development. Of course, this function may interrogate the current goals and use known assumptions. Notice, that you have been able to do this with all previous versions of Lego as well! However, with the current release, we provide a mechanism to register simple user-defined tactics so that they can be conveniently executed at the Lego level. While at the ML level, you may register any tactic f:unit->unit via Tactics.add_tactic "TacticId" f After returning to the Lego level via lego(), you can execute the new tactic by invoking UTac TacticId In constructing such a tactic f, you will have to synthesis all arguments from the current proof state. Notice that the function Namespace.getCurrentGoals : unit -> question list gives you access to the current goals wheras interrogation of the context is possible through Namespace.search id (Namespace.getNamespace()) : binding See the source file "src/lib_nat_plus_thms.sml"> for an example on how one might define and integrate a tactic for replacing all occurrences of the form (a+b)+c in the current goal by a+(b+c).

LEGO Team

Last modified: Tue Jun 23 16:46:32 BST 1998