[opentheory-users] Status of derived syntax

[Joe Leslie-Hurd]

Hi Rob,

The derived syntax in OpenTheory is rather ad-hoc: I just hard-coded some
common mathematical syntax such as numerals, pairs and sets which is
triggered by specific names in the OpenTheory namespace.

When exporting HOL Light theories to the OpenTheory library, one of the
more involved things I had to do is remove as many HOL Light-specific tags
as possible. So for example, the NUMERAL tag is easily removed, and
OpenTheory numerals are instead recognized by sequences of bit0 and bit1
functions terminated by natural number zero.

The OpenTheory version of GSPEC is called fromPredicate, and you can see
the standard library renamings in the OpenTheory fork of HOL Light in the
file

opentheory/stdlib/stdlib.int

This is how sets are recognized for printing purposes (assuming that the
term argument to fromPredicate has the right shape).

Finally, I'm rather pleased by my scheme for recognizing let expressions,
although it sounds like it might be causing you problems displaying your
theory. Lets are simply terms that can be beta-reduced, so

(\v. t[v]) x

is printed as

let v = x in t[v]

No need for any special term tags, and in all the theories I have so far
encountered there are no subterms in theorems that can be beta-reduced (and
thus accidentally print as let).

Hope that helps,

Joe




On Fri, Nov 22, 2013 at 8:08 AM, Rob Arthan <rda at lemma-one.com> wrote:

> What is the status of things like let-terms and set comprehensions in the
> Gilith Open Theory Repo. I can't see the definitions of the magic constants
> that are used to represent these things (LET and GSPEC in HOL Light and
> HOL4)? A peculiar sequence of complicated assumptions involving let builds
> up in the HTML listings.
>
> Regards,
>
> Rob.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131122/ef921505/attachment.html>