[opentheory-users] type definitions

[Joe Hurd]

Hi Ramana,

> It occurs to me that it's all right if the stack machine simulating me
> defines a constant, as long as neither I nor it ever refers to that
> constant again.
> Since I won't define the constant, I certainly won't refer to it
> again, and since I'm writing the article for the stack machine, I will
> make sure it doesn't refer to it either.
> Is this reasoning correct?

Here's what I see happening:

1. Emit an OpenTheory defineTypeOp command to define the type (plus
two constants abs and rep).

2. Use the resulting OpenTheory theorems, plus the abs and rep
constants, plus some Boolean theorems, to simulate the proof in
OpenTheory of the canonical HOL4 output:

>> |- ?rep. (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧ ∀x. P x ⇔
>> ∃x'. x = rep x')

3. Now at this point you can proceed, and you'll never need to refer
to the abs and rep constants again.

> The only problem, then, would be that the article would have these
> dummy constants among its exports.

The list of exported constants is precisely the constants appearing in
exported theorems, so these kind of abs and rep constants won't
appear.

> Can I use OpenTheory's "Unwanted" namespace to effectively take them
> out of the exported definitions?

I would rather prefer that you named them ty.abs and ty.rep, where ty
is the name of the type that you're defining. That should avoid any
name clash, and make it clear that these are internal constants for
use in the proof but not for export.

The Unwanted namespace is used as a directive to the opentheory tool
that it should remove these constants and type operators from the
theory, so that they do appear even in the proof. For example, it is
used for removing the HOL Light "NUMERAL" tag that gets wrapped around
numerals.

These abs and rep constants are necessarily used in the proof, so
shouldn't sit in the Unwanted namespace.

Cheers,

Joe