[isabelle] Computing divisors


I wonder if, by any chance, any of you know anything about work having
been done in Isabelle concerning the efficient computation of the set of
divisors of a natural number or an integer. Specifically, I require an
executable and ideally quite efficient function "divisors (n::int) = {d.
d dvd n}", but obviously, the same for natural numbers would be quite
sufficient as well.

I surveyed the Isabelle library but failed to find anything of the sort.
I also thought about resorting to constructing the set of divisors from
a prime factorisation should I fail to find any formalisation of the set
of divisors. Has a fast, executable prime factorisation function been
implemented in Isabelle? So far, all I could find is the uniqueness of
the prime factorisation.

I should probably add that I am, of course, perfectly aware that there
is no known algorithm for integer factorisation in polynomial time,
which, if I am not mistaken, implies that there is also no known
algorithm for computing the divisors of an integer in polynomial time;
by "efficient", I therefore mean, as it were, "not unnecessarily
inefficient". I am not looking for anything overly fancy such as number
field sieves, just something slightly better than trial division with
all integers from 1 to n.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.