Re: [Isarmathlib-devel] Direct product

[Slawomir Kolodynski]

I have uploaded DirectProduct_ZF to
http://formalmath.tiddlyspot.com/#DirectProduct_ZF.
I have made a couple of changes - see the attached
file. Here are my comments:

"constdefs" and "prems" are obsolete in Isabelle 2007.
I replaced them with "definition" and "assms".

There is no need to label definitions. Theorems with
names ending with "_def" corresponding to definitions
are created automatically by Isabelle.

I used to define functions in IsarMathLib as sets of
the form 

{<x,y> \<in> X\<times>Y. y = E(x)}

where E is the expression (a meta-function) that
defines the function. Later on I switched to

{<x,E(x)>.  x\<in>X}

The second way is shorter and I think easier to
understand. I modified the definition of DirectProduct
to use this style and replaced func1_1_L11A with
ZF_fun_from_total and func1_1_L11B with
ZF_fun_from_tot_val.

I replaced all "<" and ">" characters in the ordered
pair notation with "\<langle> and "\<rangle>". This
looks better in the Isabelle generated proof documents
and my tool for converting IsarMathLib theories to
TiddlyWiki markup can not handle the "<x,y>" notation
(and it would be quite difficult to add this feature).

It is better to use LaTeX in the comments rather than
@{text "..."}. LaTeX looks better and we want formally
verified mathematics to look a bit different. The only
exception is when we want to refer to a theorem name
or we really want the symbol to look like in the
formalized part for some reason.

That was an excellent first contribution and I hope
there will be more.

> It took incredibly long time to get this done

There is a value in figuring things by yourself, but
there is also a value in discussing the difficulties.
Asking question on the mailing list saves effort and
builds the knowledge base that makes things easier for
other people. I encourage you to ask questions on the
mailing list, I will do my best to help.

Slawek




http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

DirectProduct_ZF.thy
Description: 2148494091-DirectProduct_ZF.thy