*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Computing divisors*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Fri, 18 Oct 2013 16:00:35 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5261A6A0.3040604@in.tum.de>*References*: <5261A6A0.3040604@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] Computing divisors***From:*Manuel Eberl

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

- Previous by Date: [isabelle] Computing divisors
- Next by Date: Re: [isabelle] Computing divisors
- Previous by Thread: [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