[opentheory-users] new_specification

[Joe Leslie-Hurd]

Hi Rob,

One of the design goals of OpenTheory is to have very precisely defined
> standards, to maximize compatibility between tools that implement them, and
> even though I can see the conceptual unity of your proposed "spec" command
> it doesn't give precise enough instructions as to what the reader should do
> for my taste.
>
> I thought it was precise. The reader must introduce the new types and
> constants and make the sequence become axioms. The only
> implementation-defined aspect is that it can use the justification to do
> this theory extension conservatively if it knows how. However, ...
>

I think this point has become moot, but I wanted to add one thing: I can
imagine article readers that are not connected to a theorem prover (e.g., a
compiler reading a HOL definition of a program and then compiling it to
native code). So I would really like the file format to be as brain-dead as
possible, to encourage these applications.

> Instead I have sketched out the spec for a draft "defineConstList" command
>
>
> http://www.gilith.com/research/opentheory/article.html#defineConstListCommand
>
>
> ... I can't complain! The above is what I (and, I guess, Ramana) had in mind
> originally. However, that still leaves me with the problem of the other
> thread, which amounts to the fact that I do not see a practical way of
> implementing a reader that can make use of the Gilith OpenTheory Repo. I
> will expand on that in the other thread.
>

I can see your point about integrating the base package into a theorem
prover, and I confess I have not done enough eating of my own dogfood in
this regard. It's been on my TODO list for a long time to take a fresh
version of HOL Light and implement an OpenTheory reader so that a user can
type something like

import-theories ["base", "natural-prime"];;

and it would read in these theories and give them a context where the
exported symbols have been defined and the theorems have been proved,
grafting as naturally as possible onto the existing HOL Light theories.
Then whatever theorems the user proves can be exported with theory meta-data

required: base
required: natural-prime

and the dependencies checked when the dependencies evolve. But I simply
haven't got around to it...

I am happy with the derived rules. By a fortunate coincidence, you have put
> the parameters to trans and proveHyp on the stack in the same order as I do
> in my writer.
>

Excellent.


> For proveHyp (and deductAntisym) it might be helpful to say explicitly
> that the rules do not fail if the formula phi is not present in Delta.
>

Thanks, that's a good suggestion. I've added the documentation to both
commands.

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140318/a30602c5/attachment.html>