Email Gateway (Mar 12 2024 at 12:28): Email Gateway (Mar 12 2024 at 12:28):From: arithalghomework@sina.com
Dear Isabelle User Mailing List,
I'm going to submit my formalization of prime number theorem with remainder into an AFP entry. Here is my code: https://github.com/mmew-2022/Isabelle_Prime_Number_Theorem. I removed most of custom notations from my first version. What additional changes should I make to fulfill the requirement of an AFP entry? I've read the guideline of https://www.isa-afp.org/submission/, and the Isabelle linter reported some warnings about some rule_tac proofs and too long proof lines. Is this important?
Thanks,
Shuhao Song
Email Gateway (Mar 13 2024 at 11:32):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Shuhao,
I took a look at your proofs. On the whole, they look good. With regard to rule_tac, we specifically object to references to automatically-generated names e.g. xa, xb, but you don't seem to be doing this. I also noticed that where you are using rule_tac, often sledgehammer yielded up a nice simple proof.
In one place I noticed compound methods in a proof:
by (safe, rule zeta_bound_params.zeta_bound_param_axioms)
(use assms in auto)
This sort of thing should be rewritten if possible. Typically what helps is to explicitly prove the hardest subgoals produced by the compound method (if they are not too long to write out).
So please do look at the output of the Linter, and where the problem is easy to fix, please just fix it. It's okay to leave a few of the warnings. If we don't accept your submission the first time, I'm pretty confident it will be accepted soon.
Larry Paulson
Email Gateway (Apr 21 2024 at 09:09):From: arithalghomework@sina.com
I'm Shuhao, I have made some changes in my proof of prime number theorem with remainder. Today I will submit it as an AFP entry.I
will use my academic e-mail (znssong_meow@sina.com) instead of this
e-mail address for submission. Indeed, I want to use
znssong_meow@sina.com to send the previous e-mail to the mailing list,
but I misoperated on my phone and used this mail address. The contract
author will be Bowen Yao, a teacher in Beijing University of Chemical
Technology.
I removed most use of rule_tac, and splitted
complex proof steps. Now the linter only complains at too short names
of definition in locale, for example:```definition B where "B x \<equiv> 5 / 4 * ln x" for x :: realdefinition f where "f x s \<equiv> x powr s / s * logderiv zeta s" for x :: real and s :: complex
this style is common in mathematics (instead of software verification,
in there you usually use names with its actually meaning); In
mathematics you usually don't write `Bound`, only write `B` for name.
If
more changes are needed, please tell me. I'd also want to know whether this submitting will be in AFP 2024 release, as it will be forked
at this Sunday.
[PNT_with_Remainder.thy](/user_uploads/14278/GmSug9AFtHnrcFhagcsFFCUV/PNT_with_Remainder.thy)
From: Manuel Eberl <manuel@pruvisto.org>
Hello,
the AFP fork does not really matter much for you. Until the release of
the next Isabelle version, you can still submit your entry for AFP 2023
for Isabelle 2023 and it will be ported to afp-devel and Isabelle 2024
by us.
In any event, your submission will appear on the AFP website and shortly
thereafter in afp-devel. If you submit before the release of AFP 2024 it
will be part of AFP 2023; otherwise it has to work with Isabelle-2024
and will be part of AFP 2024. But there is little difference in the end
result.
Manuel
Last updated: Apr 29 2024 at 04:18 UTC