[opentheory-users] definition of "new" constants? / defineTypeOp rule

[Joe Leslie-Hurd]

[cc'ing opentheory mailing list]

Hi Gunter,

> (It is fine it you want to Cc the mailing list in your replies; I just don't want to
> create too much traffic.

The purpose of the OpenTheory mailing list is to answer people's
questions and discuss OpenTheory topics, so please don't worry about
creating traffic on the list. Also, I prefer to use the mailing list
for OpenTheory emails as a public record of the discussions and so
other people also have the chance to answer questions.

>> I have also added some verbiage at the bottom of the Virtual Machine
>> section describing the constraint that there should not be different
>> symbols with the same name in exported theorems.
>
> 1. "must not reference two different constants that have the same name."
>
> This is stricter than what the opentheory tool currently allows?
> (I prefer it that way.)

It is not intended to be stricter. The set of constants contained in
the exported theorems must have the property that different constants
have different names, which I believe is what the opentheory tool
requires. Have you encountered a situation that violates this but is
permitted by the opentheory tool?

> "The same constraint also holds for the set of assumptions Γ".
> For clarity, I would put it right at the beginning
>
> "Constraint: The set of theorems Δ and assumptions Γ must not ..."
>
> (otherwise it looks as if one constant in  Δ and a different constant in Γ were o.k.

Actually there's nothing wrong with this scenario: it's just some
sloppy programming in the opentheory tool that generated an error in
this case. I've just released a new version of the opentheory tool
that permits this scenario (with a warning) and added a new test case
that demonstrates it:

$ opentheory info test/articles/example12.art
WARNING: 2 different constants named c
1 external type operator: bool
1 external constant: c
1 assumption:
  |- c
1 defined constant: c
1 theorem:
  |- c

> 3. another question: I don't completely see through the definetypeop
> rule.
>
> a) Is the role of Thm(⊦ φ t) only to specify the type of t?

The main purpose is to prove that the predicate \phi is non-empty,
which is a required condition of every higher order logic type.

> b) When I look at the *list* type operator
> in list-def-1.63.art
> it is defined with the type of t being bool.

These files are just the theorem caches for a package, they do not
define symbols properly. They are really only intended for internal
use to optimize theory dependency computations:

http://www.gilith.com/research/opentheory/faq.html#what-are-theorem-files

I recommend simply ignoring these files: they are a great source of confusion.

> c) Is there an example where rep and abs and the theorems are not
> thrown away?

My standard pattern is to define a type, use the abs/rep constants and
bijection theorems to define some other constants and prove some
characteristic theorems about the new type, and then export these
characteristic theorems from the theory. This effectively hides the
primitive abs/rep constants returned from defineTypeOp inside the
theory abstraction.

> d) Where can I find some background information on the
> defineTypeOp rule of the OpenTheory logical kernel?
> (PS. I found some explanation on p. 81 in
> https://who.rocq.inria.fr/Ali.Assaf/research/thesis.pdf

Take a look at the HOL4 "Logic" manual:

http://hol-theorem-prover.org/documentation.html

Section 2.5.4 describes type definition.

Cheers,

Joe