*To*: Brian Huffman <huffman.brian.c at gmail.com>*Subject*: Re: [isabelle] Computing divisors*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sat, 19 Oct 2013 01:14:45 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAMXsiayw8go2TMrNAMbpFm5EXzKdL=-a8Fn9JbZz3qerXyv9g@mail.gmail.com>*References*: <5261A6A0.3040604@in.tum.de> <CAAMXsiayw8go2TMrNAMbpFm5EXzKdL=-a8Fn9JbZz3qerXyv9g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

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

**References**:**[isabelle] Computing divisors***From:*Manuel Eberl

**Re: [isabelle] Computing divisors***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Computing divisors
- Next by Date: Re: [isabelle] Computing divisors
- Previous by Thread: Re: [isabelle] Computing divisors
- Next by Thread: Re: [isabelle] Computing divisors
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list