Email Gateway (Aug 22 2022 at 15:25): Email Gateway (Aug 22 2022 at 15:25):From: Manuel Eberl <eberlm@in.tum.de>
I just noticed something peculiar about the Euler totient function in
Isabelle ("phi" in Isabelle-2016; "totient" as of 067210a08a22 in
isabelle-dev): Everyone seems to agree that ϕ(1) = 1, but in Isabelle,
"phi 1 = 0" resp. "totient 1 = 0".
Furthermore, before anyone invests more time into developing that
function, I would like to point out that I have my own version of that
function in an ongoing development on Analytic Number Theory that should
end up in the AFP eventually [1].
I've shown pretty much all the basic properties of the function and a
few not-so-basic ones. My suggestion would be to change the definition
of "totient" in HOL-Number_Theory to "totient 1 = 1" and I will then
merge the more basic facts of my development into HOL-Number_Theory.
(Also, if anyone has any plans/stakes/interests in Analytic Number
Theory in Isabelle, feel free to contact me, because at the moment I'm
not sure how to continue this development, but I don't think it's quite
ready for submission to the AFP yet either)
Manuel
[1]:
https://bitbucket.org/pruvisto/dirichlet/src/df668238de758209997b0371765ed04057b1d8df/Totient.thy
Email Gateway (Aug 22 2022 at 15:25):From: Manuel Eberl <eberlm@in.tum.de>
Apparently, that link I sent does not work for people other than me.
What should work is going to the repository [1] and navigating to the
file "Totient.thy".
Manuel
[1]: https://bitbucket.org/pruvisto/dirichlet
Email Gateway (Aug 22 2022 at 15:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,
that totient function stems from an application / example in
HOL-Number_Theory, which I took the opportunity to separate into a
dedicated theory to achieve more attention prominence. Successfully, I
deem ;-).
I just noticed something peculiar about the Euler totient function in
Isabelle ("phi" in Isabelle-2016; "totient" as of 067210a08a22 in
isabelle-dev): Everyone seems to agree that ϕ(1) = 1, but in Isabelle,
"phi 1 = 0" resp. "totient 1 = 0".
As far as I understand, this is mainly due to the definition (»<«
instead of »<=«). Since that started mainly as an example, I expect
little difficulty to adjust this.
I've shown pretty much all the basic properties of the function and a
few not-so-basic ones. My suggestion would be to change the definition
of "totient" in HOL-Number_Theory to "totient 1 = 1" and I will then
merge the more basic facts of my development into HOL-Number_Theory.
Would be excellent.
Cheers,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC