[Isarmathlib-devel] Re: IsarMathLib: two small remarks

[Marnix Klooster]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Slawomir,

You wrote:

> Marnix,
>> First, the list archives don't seem to be available.
>>
> 
> I think the archives are created when the the first
> message is posted to the list. That hasn't happened
> yet.

Ah, that explains it :-)  Let me Cc: this to the list then, to be the
first... :-)

>> Anyway, my
>> alternative definition is
>>
>>     (p == q == r) /\ !(p /\ q /\ r)
> 
> Neat. It's a pity I didn't know that before.

Well, it seems that a number of these things are not well known.
Another example is the associativity of == (equivalence), and the fact
that 'xor' is really the same as =/= (p =/= q means !(p == q)), and that
== and =/= are also mutually associative (so that e.g. p =/= q =/= p ==
q is both meaningful and true).

>> I'm more of a tools guy
> 
> I am working on importing Metamath theorems into
> Isabelle/ZF. The next IsarMathLib release will contain
> some tools (written in Haskell) to automate this.
> Perhaps you will find something enjoyable to
> contribute then?

Perhaps I already have :-)  Did you know about Hmm?  Haskell source code
and darcs repository are at http://www.solcon.nl/mklooster/repos/hmm/.
HmmImpl.hs (through its wrapper Hmm.hs) has functions to read a Metamath
database .mm file, and to verify its proofs.  Its GPL2+-licensed.
README file is at http://www.solcon.nl/mklooster/repos/hmm/README (not
visible in the directory listing now due to a problem at my ISP).

So I'll be glad to help you with Hmm, and work on any necessary patches,
and on thinking about how to do conversions like this.  But note that I
don't have Isabelle/Isar experience, and I don't think I will have the
time to learn in the near future.

Please also note that Raph Levien (address@hidden), the author of
Ghilbert (http://ghilbert.org) has a working Metamath->Ghilbert
conversion, which of course involves turning Metamath statements into
expression trees, and parsing Metamath proofs.  So he (and/or the
Ghilbert source code and darcs repository at
http://ghilbert.org/repo/ghilbert/) might be able to help with specific
issues.

> Thank you for your feedback

You're welcome.

Groetjes,
 <><
Marnix

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.5 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFFLdFpjn9v+6JsL6sRAgwkAJ9tU90qnkZdu+t8HB1xd3Q9k4ATcgCg6ifp
6sAIMtL7PR83GMTMHqgQRSo=
=tEBX
-----END PGP SIGNATURE-----