[opentheory-users] the Unwanted namespace

[Ramana Kumar]

On Wed, Dec 7, 2011 at 8:46 AM, Michael Norrish
<Michael.Norrish at nicta.com.au> wrote:
> On 7/12/11 6:47 PM, Ramana Kumar wrote:
>> On Dec 6, 2011 11:02 PM, "Michael Norrish" <Michael.Norrish at nicta.com.au
>> <mailto:Michael.Norrish at nicta.com.au>> wrote:
>>>
>>> I think the mistake here is mapping the Abbrev constant to Unwanted.
>>  I'd say it was probably worth preserving.
>>
>> Why? What does it mean outside of HOL4?
>
> Nothing particularly.  But I want to use opentheory as a storage
> mechanism for HOL4 theories, and so the technology needs to be faithful
> to what is in the HOL4 theories.

I think opentheory would need to be augmented with something before it
was really appropriate for storing faithful copies of prover-specific
theories. There's no mechanism for storing syntax information (e.g.
precedence, associativity) or overloads, automatic rewrites, any
additional (non-logical) functionality (like a library associated with
a theory), or even names for theorems. And I think it's correct to map
things like Abbrev and NUMERAL to Unwanted.id, so when you read back
the theory, the numbers are missing their tags, for example (that
might be fixed by a smarter reader).

It would be worth thinking about how to do all that with opentheory.
I wouldn't want to compromise the goal of storing prover-independent
theories without a good reason, though...

> But I admit I may have misunderstood
> the issue here.  In particular, I'd be surprised if Abbrev actually
> appears in any theory's exports except for the definition and that
> forall-rewrite.

I don't think it appears in any of the exports... I guess it must have
been used somewhere in a proof and then, since it couldn't be removed
from the rewrite, ended up having to be defined (and appearing in an
axiom).

>
> Michael
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>