Email Gateway (Jul 16 2020 at 01:33): Email Gateway (Jul 16 2020 at 01:33):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear all,
Wondering about the following :
given a specific large number, is there a way to show what the set of
its proper divisors is?
E.g. define:
definition proper_divisor :: "nat ⇒nat ⇒ bool " (infixr "properdiv" 80)
where " n properdiv m ≡(( n ≥ 1) ∧( n< m) ∧ ( n dvd m) ) "
definition properdiv_set: "properdiv_set m ={n. n properdiv m }"
I want to show that :
"properdiv_set 819 = { 1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273 }".
Now, for a small number, e.g. for 9, the following works:
"properdiv_set (Suc(Suc(Suc(Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) =
{1,3}"
by (auto simp: properdiv_set proper_divisor_def less_Suc_eq dvd_def;
presburger)
but I need to have a way of showing what the set of proper divisors for
much larger numbers is.
Any ideas would be much appreciated.
Thank you,
Angeliki
Email Gateway (Jul 16 2020 at 04:45):From: Tobias Nipkow <nipkow@in.tum.de>
If you formulate it more computationally (and more consistenly spaced), you can
use evaluation in ML:
definition proper_divisor :: "int ⇒int ⇒ bool " (infixr "properdiv" 80)
where "n properdiv m = (n ≥ 1 ∧ n< m ∧ n dvd m)"
definition properdiv_set: "properdivs m = filter (λn. n properdiv m) [1..m]"
lemma "properdivs 819 = [1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273]"
by eval
Tobias
smime.p7s
Email Gateway (Jul 17 2020 at 11:11):From: Manuel Eberl <eberlm@in.tum.de>
As far as I know, the fastest known algorithm for large numbers is to
compute a prime factorisation and then just read off the set of
divisors. Let's define the set of (not necessarily proper) divisors.
definition divisors :: "'a :: normalization_semidom ⇒ 'a set" where
"divisors x = {y. normalize y = y ∧ y dvd x}"
I use a more general type so that it also works for int, poly, etc. but
I require that the divisors be normalized to make things nicer. For nat,
it doesn't make a difference.
Then we can prove various nice lemmas like
lemma divisors_prime_power:
fixes p :: "'a :: factorial_semiring"
assumes "prime p"
shows "divisors (p ^ n) = (λi. normalize (p ^ i)) ` {..n}"
lemma divisors_mult_coprime:
fixes a b :: "'a :: semiring_gcd"
assumes "coprime a b"
shows "divisors (a * b) = normalize ` (divisors a * divisors b)"
and finally
lemma divisors_conv_prime_factorization':
fixes x :: "'a :: factorial_semiring_gcd"
assumes "prime_factorization x = P"
assumes "x ≠ 0"
shows "divisors x = normalize (∏p∈set_mset P. (λi. p ^ i)
{..count P p})"
With this, you can easily compute the set of divisors as long as you
factorize beforehand:
lemma "divisors (80389990399 :: nat) =
{1, 101, 199, 10201, 20099, 39601, 2029999, 3999701, 7880599,
403969801,
795940499, 80389990399}"
proof -
have "prime (101 :: nat)" and "prime (199 :: nat)"
by simp_all
hence *: "prime_factorization 80389990399 = {#101, 101, 199, 199,
199::nat#}"
by (intro prime_factorization_eqI_strong) (auto simp del:
prime_nat_numeral_eq)
show ?thesis
by (subst divisors_conv_prime_factorization'[OF *])
(simp_all add: set_times_image atMost_Suc insert_commute)
qed
If you want the proper divisors, just kick out 1 and the number itself
and you're done! Of course, if you have a number with lots of prime
divisors, it will be slow since there are lots of divisors. The builtin
procedure to prove primality is also very slow, but other methods are
available, as you know.
By the way, a student of mine and I developed a simproc to do such
things completely automatically, but I haven't had the time to put it in
the distribution yet. Then, with some simple setup, you could just
evaluate "divisors" by an invocation of "simp" without having to
factorise yourself.
If you use the stuff I attached for anything that will go in the AFP,
please put a "TODO" tag there because I should probably put this stuff
in the distribution at some point and then we can eliminate this
duplication.
Manuel
Divisors.thy
Email Gateway (Jul 20 2020 at 05:38):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
computing the divisors for integers and natural numbers via
prime factorization is also readily available in the AFP:
in thys/Polynomial_Factorization/Prime_Factorization.thy there
are divisors_nat and divisors_int functions.
Best,
René
signature.asc
Email Gateway (Jul 20 2020 at 15:50):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear all,
Many thanks to Manuel, Tobias and René for their great alternative
suggestions.
I think I will opt for making use of René's AFP entry
(as it is the one that is straightforward to use with my development,
which is already quite long-- using the other definitions would require
a complete re-work of all my proofs)
I noticed that computations of divisors of specific numbers using the
above AFP entry are also easily done using "by eval"
Thank you again,
Best,
Angeliki
Last updated: Jul 15 2022 at 23:21 UTC