[opentheory-users] the Unwanted namespace

[Ramana Kumar]

> [I'm not entirely sure what's going on in your second example, but the
> theorem (|- Unwanted.id = \x. F) on the stack is perhaps cause for
> concern.]

I was deliberately trying to expose a possible unsoundness in the
system, hence the scary-looking theorem. But now I see the only
semantic effects implemented for Unwanted.id are less susceptible than
I thought.

> This proof post-processing is extremely simple and ad-hoc right now,
> and as you can see it can only handle one very special kind of
> pattern. I'd be interested in discussing ways to expand its scope, or
> alternatively perhaps there are ways to recast your proofs into the
> existing pattern.
>

Since my proofs are currently generated directly from existing HOL4
script files, I don't see how I could recast them into this pattern in
any way easier than it would be to just pre-process all theorems by
rewriting with the definitions of these unwanted constants before
logging. But I'd still rather have the opentheory tool do all that
processing... So let's have the discussion about ways to expand its
scope.

I eventually came to the conclusion that appTerm and appThm are the
only commands that would ever need to change, because they are the
only way a term of the form (Unwanted.id t) can enter the virtual
machine's state.

Perhaps opentheory should automatically just do an explicit proof
after absThm (|- Unwanted.id = f) (|- x = y) of (|- x = f y), for all
x y and f, using an assumption (|- Unwanted.id x = x). Also, you would
need to prevent the name Unwanted.id from being used by defineConst.