Re: [isabelle] Computing divisors



At the end of the day, I want to write a proof method in Isabelle, so I
would imagine a simproc would do just fine. (albeit a definition would
probably be easier to use)

I had not thought of this kind of approach, so thank you for that
suggestion. As for the primality test, I do remember seeing an
implementation of Eratosthenes' sieve somewhere in HOL/Number_Theory.

Well, I shall look into it, thank you.


On 19/10/13 01:00, Brian Huffman wrote:
> 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.