[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Hi Rob,

Many thanks for that. I have now defined a set fold operation like the one
> in the repo and I can import the whole base package conservatively without
> any devious tricks in one go using the article file that your perl magic
> generates.
>

That is excellent news.

I have just one outstanding concern: there are no theorems in the sum
> package and only one in the real package (and the only operators it uses
> are <= and sup. There don't seem to be any uses of real or sum in the other
> packages in the repo, so I haven't really been able to test that I have got
> the mappings right for these packages. Any suggestions would be welcome.
>

Hmm... do you have any suggestions for theorems about sum types that I
could prove in a sum-thm package to help here? Does ProofPower contain any
such theorems?

I am trying with some success to load the other packages in the repo. In
> each case, I constructed an article for each package XYZ in the 35 package
> other than those included in the base package with the command:
>
>    opentheory info --article -o XYZ.art XYZ.
>

That looks like a good thing to do, although you might also want to know
the theories that XYZ depends on, either by looking at the requires:
meta-data in XYZ.thy or by using the command

opentheory info --requires XYZ

This will tell you the intended load-order of theories.

The package modular seems to expect a constant called
> Number.Modular.modulus to be defined, but nothing defines it, so modular
> won't load. The package word seems to expect a constant called
> "Data.Word.width" but nothing defines it. byte will load, but the word10,
> word12 and word16 packages won't, apparently because they are trying to
> redefine a constant called Number.Modular.equivalent.
>

modular is an example of a parameterized theory, which expects its
parameter symbols to be bound to symbols having the required properties.
For each parameterized theory I have uploaded a witness theory that shows
that these parameters can be satisfied, where the parameter symbols are
defined in the witness theory. For example:

$ opentheory install modular-witness
installed package modular-witness-1.3
$ opentheory info --theory modular-witness
3 external type operators: -> bool natural
9 external constants: = ! /\ ==> ~ F T suc zero
8 satisfied assumptions: hidden
1 defined constant: modulus
1 theorem:
  |- ~(modulus = 0)

The parameter symbols show up as defined symbols in the witness theory
(i.e., the constant modulus), and the required properties show up as
theorems (i.e., modulus is non-zero).

word is another parameterized theory that instantiates modular, as can be
seen in its theory source file:

http://opentheory.gilith.com/opentheory/packages/word-def-1.64/word-def.thy

The concrete word theories (e.g., byte, word16, etc) then instantiate the
word theory with different word sizes, for example:

http://opentheory.gilith.com/opentheory/packages/byte-def-1.73/byte-def.thy
http://opentheory.gilith.com/opentheory/packages/word16-def-1.73/word16-def.thy

The upshot is that you'll be able to read in these concrete theories just
fine, but trying to read multiple of them will fail because they will
define internal symbols carried over from modular and word (e.g.,
Number.Modular.equivalent) with the same name but different definitions.
I'm not sure what to do about this, but let me continue this in the other
thread about multiple definitions.

Cheers,

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