[opentheory-users] new_specification

[Rob Arthan]

Joe,

On 14 Mar 2014, at 21:35, Joe Leslie-Hurd <joe at gilith.com> wrote:

> I have thought about this some more, and I believe I have answered my own questions.
> 
> 1. The proposed definition mechanism is not more expressive than new_definition, because it can be simulated by first defining c_1 = t_1, ..., c_n = t_n, instantiating the given theorem with the substitution [c_1/v_1, ..., c_n/v_n], and then using the definition theorems of the c_i to prove the hypotheses.

It doesn’t claim to be more expressive. What it is designed to offer is abstraction. The OpenTheory kernel has a different way of hiding representation details, but HOL4, HOL Light, ProofPower and the OpenTheory article format don’t have that option.

> So I think the best thing is to keep the OpenTheory defineConst mechanism, and "compile" the proposed definition mechanism using the above scheme.
> 
But that means that the article format can’t express the desired abstraction in a way that can be ported from one system to another. That seems like a major shortfall to me.

My proposal for OpenTheory would be a new command, called “spec” say, which would actually provide the functionality of new_type, new_const, new_axiom, new_specification, gen_new_specification and new_type_definition in their HOL4, ProofPower and HOL Light guises. (Here gen_new_specification is the new principle from HOL Constant Definition Done Right.) “spec" would have four parameters:

(1) a list of type name/arity pairs identifying new types to be introduced;
(2) a list of constant name/type pairs identifying new constants to be introduced (the types in list (1) may appear in the types of these constants);
(3) A list of sequents giving new axioms to be introduced (the types in list (1) and the constants in list (2) may appear in these sequence);
(4) a list of objects, which constitute a “justification” for the new axiom.

(4) would be empty for new_axiom, new_const or new_type. It would give the input theorem for new_specification, gen_new_specification and new_type_definition.

A reader would analyse the parameters to figure out the best way to introduce the types and constants and so derive the required axioms. Recognising the various new_XYZ forms that I listed above and allowing for the differences between systems is easy and the reader can always fall back on a combination of new_type, new_const and new_axiom (or some kind of cheat).

By making parameter (4) a list of objects, the “spec” command is general enough to accommodate any conceivable extension to the definitional mechanisms without changing the article format.

The “spec” also makes the article format support higher levels of abstraction. For example, it would let the Gilith OpenTheory repo describe the types and constants in the base package (and others) in a way that is easy to import. The pair type for example, would be introduced by a spec command that introduces the type constructor “x", the constants “,”, “fst” and “snd” and with the theorems that characterize the type in terms of these constants as the new axioms. The justification could be a string like “primitive” to hint to a reader that it should already have the types and constants. This declarative approach would make the base package a really useful resource (solving the problems discussed in this thread: [opentheory-users] Importing from the Gilith OpenTheory Repo).

> 2. I think my simplification is bogus because defining the c_i in terms of c can fail because of the type variable condition.
> 
That is correct.

Regards,

Rob.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140315/6460e5d2/attachment.html>