Some possible improvements and extensions to SOFT.

SOFT should be extended with the ability to introduce and instantiate
mutually recursive functions,
perhaps via a new

Currently recursive second-order functions
must use `o<` as their well-founded relation.
This could be relaxed, perhaps even to the point of
allowing second-order well-founded relations.

Besides second-order versions of
`defun`,
`defchoose`,
`defun-sk`,
`define2`, and
`define-sk2`,
we could add support for second-order versions of
`defun-nx`, `defpun`, and other function introduction events.
`defun-inst` would generate the same macros for instances.
The macros could be called

Under some conditions, it would make sense for `defun-inst`
to instantiate a partial second-order function
(introduced, say, via a future `defun2` or `defun`),
when the instantiated

`defthm-inst` could also generate instances with the same macros
from second-order theorems introduced via
`defthm`, `defrule`, and other theorem introduction events.

Currently SOFT only supports logic-mode second-order functions. Supporting program-mode functions as well may be useful.

It would be useful to allow the default guards of instances of second-order functions (obtained by instantiating the guards of the second-order functions) to be overridden by stronger guards.

The

See the future work section of the Workshop paper for a more detailed discussion with examples.

Instantiations could be extended to allow function variables to be replaces with lambda expressions, besides named functions.

Intuitively,
if `defun-inst`,
but probably it should be.

See the future work section of the Workshop paper for a more detailed discussion with examples.

The types of function variables are currently limited to

Other than their types, function variables are currently unconstrained.
In some cases, it may be useful to specify some logical constraints,
resulting in a constrained function as in non-trivial `encapsulate`s.
Instantiations will have to respect these additional constraints.

The latter extension would overlap with some existing tools,
such as

Function variables current have guard

Currently, when an instantiation is applied to a term, the table of instances of second-order functions is consulted to find replacements for certain second-order functions, and the application of the instantiation fails if replacements are not found. Thus, all the needed instances must be introduced before applying the instantiation. SOFT could be extended to generate automatically the needed instances of second-order functions.

SOFT could also be extended with a macro `defthm`
and to record the theorem in a new table,
along with information about the involved second-order functions.
`defun-inst` could be extended with
the option to generate instances of the second-order theorems
that involve the second-order function being instantiated.
`defthm-inst`s.

The convention of including function variables in square brackets in the names of second-order functions and theorems, could be exploited to name the automatically generated function and theorem instances.

Currently the default rule classes
of an instance of a second-order theorem are