[opentheory-users] type definitions

[Ramana Kumar]

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?

The only problem, then, would be that the article would have these
dummy constants among its exports.
Can I use OpenTheory's "Unwanted" namespace to effectively take them
out of the exported definitions?

On Sat, Jan 15, 2011 at 9:44 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Is there a good reason for the defineTypeOp command to define new
> constants as well as the new type operator?
>
> It's causing me a bit of trouble when trying to write an article
> writer for HOL4, because HOL4's type definition mechanism doesn't
> introduce new constants as well. Those constants can be defined after
> the type is defined (both by HOL4 and by other stack machine
> commands), although that might require Hilbert choice to be present...
> actually, if it does require select maybe that's a good reason to do
> it your way, since the stack machine currently doesn't depend on any
> constants existing (except =).
>
> The HOL4 way of doing a type definition is given a theorem |- P t, to
> assert |- ?rep. (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧ ∀x. P x ⇔
> ∃x'. x = rep x')... so it depends on exists and forall as well. I am
> starting to see the reasons for the inconvenient defineTypeOp... were
> they deliberate decisions to avoid those constants?
>
> Anyway it seems like to write a HOL4 article writer, one would just
> need to define some dummy constants every time some HOL4 code wants to
> define a type operator without providing the names for abs and rep (in
> order to be able to accurately log a defineTypeOp command); later if
> they decide to define an abs and reps then there will just be two
> pairs of constants around doing the same job.
>