Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] One more lemma to add to Isabelle/ZF

Email Gateway (Aug 18 2022 at 16:33):

From: Slawomir Kolodynski <skokodyn@yahoo.com>
Victor,
You may want to direct your questions and proposals to the IsarMathLib mailing list (http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel ) instead of the Isabelle mailing list. Very few Isabelle users are interested in Isabelle/ZF.
If you decide to contribute to IsarMathLib, please read the style guide at http://www.nongnu.org/isarmathlib/IsarMathLib/CONTRIBUTING.html first.
Note that Isabelle and IsarMathLib are separate projects and you shouldn't expect that your contributions to IsarMathLib will be automatically included in Isabelle distribution.

Regards,
Slawomir

Email Gateway (Aug 18 2022 at 16:45):

From: Victor Porton <porton@narod.ru>
I suggest one more lemma to add to Isabelle/ZF:

lemma comp_fun2: "[| g: A->B1; f: B0->C; B1<=B0 |] ==> (f O g) : A->C"
proof -
assume "g: A->B1" "f: B0->C" "B1<=B0"
with g: A->B1 have "g: A->B0" by auto (rule fun_weaken_type)
from g: A->B0 f: B0->C show "(f O g) : A->C" by (rule comp_fun)
qed

\--
Victor Porton - http://portonvictor.org

Email Gateway (Aug 18 2022 at 16:46):

From: Alexander Krauss <krauss@in.tum.de>
Victor Porton wrote:

I suggest one more lemma to add to Isabelle/ZF:

Dear Victor,

when I said "contributions are welcome", this was not an
invitation to spam this list with spontaneous proposals of trivial
lemmas, some of which you haven't even proved! Please stop doing
this, as it is just a waste of everybody's time!

Instead, my suggestion is this:

1. Learn the basics of Isabelle using the available documentation. Since
   ZF has less documentation than HOL, it may be helpful to work through
   the Isabelle/HOL tutorial first. Many things described there also apply
   to ZF. Typically, getting sufficiently comfortable with the system to do
   actual work takes a few months.

2. When you have mastered the basics, start working on some
   formalization that you are interested in.

3. When you have proved something non-trivial, you can consider
   submitting your formalization to the AFP (http://afp.sf.net).
   Submissions will be reviewed by the editors and added to the AFP if
   considered relevant. If in this process, it is discovered that some
   lemmas should rather go directly into ZF, rather than the AFP, this will
   be taken care of by the Isabelle developers.

Alex

Last updated: Apr 20 2024 at 01:05 UTC