[opentheory-users] definition of "new" constants? / processing of packages

[Günter Rote]

On 10.08.2015 10:33, Günter Rote wrote:
> Thanks. I'll go with this in the implementation. (maybe issue a warning)
> Although it is somewhat baroque.
> Two constant terms are considered equal if
>  (a) they were both generated by constTerm commands and
>      have the same name and type
>  (b) they were both generated by defineConst commands
>      with the same name and definition (including type)
> 
and (c) they are the abs or rep constants that were
defined in the same defineTypeOp statement.

> 
> I am beginning to wonder how different constants with the same name
> will survive the interface between several article files in
> a safe and sound way.

Dear Joe!
I gave it a try, and I found that it is forbidden to use
two constants with different definitions and the same name
in exported theorems (using thm) and perhaps also assumptions (using axiom):
This makes perfect sense for a sound proof checker,
but it should be part of the specification.

====================
>opentheory info two-const-conflict.art

FATAL ERROR: opentheory failed:
different constants named "C"
====================

When opentheory processes a theory, does it read all theory article files
on which it depends?
Or is there a way that it just needs to read the theorems from
other packages that it uses?

(In trying to understand how the interface between theories works,
I have looked at
http://www.gilith.com/research/opentheory/theory.html
and the paper
"Composable Packages for Higher Order Logic Theories", which is outdated
in this respect.
(Incidentally, your version of the Schröder–Bernstein theorem
might require the axiom of choice, see
https://en.wikipedia.org/wiki/Schr%C3%B6der%E2%80%93Bernstein_theorem

Here are some questions:
What is the checksum entry?
I can somehow guess what the entry
  show: "Data.Bool"
in the .thm file means, but it is not completely clear.
In particular, what happens when there are several "show: " lines?

Is there a way to eventually look at the theorems that are proved
in detail in an unambiguous format with all type information? (other than the html
format with mouse-over?)

Best regards :
-- 
G"unter Rote               (Germany=49)30-838-75150 (office)
Freie Universit"at Berlin                    -75103 (secretary)
Institut f"ur Informatik       FAX (49)30-838-75192
Takustrase 9, D-14195 Berlin, GERMANY


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5311 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150813/c6eaed29/attachment.bin>