Re: [isabelle] Computing divisors



On Fri, Oct 18, 2013 at 2:22 PM, Manuel Eberl <eberlm at in.tum.de> wrote:
> Hallo,
>
> 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.

Do you need an Isabelle definition that works for code generation, or
would it be sufficient to have something that works in Isabelle
proofs, e.g. a simproc that could rewrite "prime_factorization 60" to
"[2,2,3,5]"?

I don't know of any pre-existing solution for factorization, but if a
simproc is all you need, then you might consider doing something like
what we have for div/mod on integer numerals. (See simprocs
binary_int_div and binary_int_mod in src/HOL/Divides.thy.)

If you have a function defined in Isabelle as "f x == THE y. P x y",
then you can use an external oracle or ML function to compute "y" from
"x". Within Isabelle, you then prove "P x y" and use the uniqueness
theorem to derive "f x = y".

If the uniqueness of prime factorizations is already proved, then we
just need a way to prove in Isabelle that a given factorization is
indeed a prime factorization of a given number. I guess the next step
is to find an efficient way to test for primality in Isabelle. :)

- Brian




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