[opentheory-users] HOL light

[Joe Leslie-Hurd]

Hi Ramana,

[cc'ing the opentheory-users mailing list]

> The proof-logging fork [of HOL Light] has sets as a
> separate type, and the scripts in Model/ haven't been updated yet.

Just a brief note on this design decision, because I know the
convention in HOL implementations is to use the type 'a -> bool for
sets. For the standard theory library I aim to prioritise ease of
importing theories into a theorem prover over ease of exporting, and
as Michael notes it's easy to "bind" 'a set to 'a -> bool when
importing (the other way around would be more difficult).

Also, when thinking about how to design reusable theories I thought
the extra isolation of a new type would make it easier to derive
consequences of sets by theory interpretation (by interpreting a
helpful parametric theory type operator to the "set"), and would
prevent the accidental inclusion of "ill-formed" terms like "{ x | P x
} t" in exported theorems.

> So... someone (probably me) just needs to work through the scripts in Model/
> and get them to compile again...

I'd be happy to provide tech support for a porting effort to do this.
My experience with porting the set theory library in HOL Light is that
most tactic proofs are insensitive to the choice of set
representation.

Cheers,

Joe