[isabelle-dev] NEWS: Primes

[Tobias Nipkow]

Naming: can't we drop "is_"?

Tobias

On 27/07/2016 10:46, Manuel Eberl wrote:
> *** HOL ***
>
> * Number_Theory: algebraic foundation for primes: Introduction of
> predicates "is_prime", "irreducible", a "prime_factorization"
> function, the "factorial_ring" typeclass with instance proofs for
> nat, int, poly.
>
> * Probability: Code generation and QuickCheck for Probability Mass
> Functions.
>
>
>
> As for the former: There are now three new algebraic predicates:
>
> - "irreducible", i.e. irreducible elements in a ring (cannot be decomposed into
> two non-unit factors)
> - "is_prime_elem", i.e. p is a prime element if for all x,y where p divides x *
> y, it also divides x or y
> - "is_prime" if p is a prime element and it is normalised
>
> For instance, the integer "-3" is a prime element, but not a prime. This
> corresponds nicely to the concept of a "prime number" on the integers. W.r.t.
> the old definitions.
>
> The "is_prime" predicate is necessary because normalisation is necessary for
> some things, such as a unique prime factorisation.
>
> The old "prime" constant is now a mere abbreviation for "is_prime" and can
> perhaps be discontinued in the next version. This is not necessarily the final
> naming scheme; I am open to better suggestions.
>
>
> As a side note, there is a lot of material in this that subsumes material in
> some AFP entries, most notably the "Algebraic Numbers" group by Thiemann et al.
>
>
> Cheers,
>
> Manuel
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160727/fa4849a2/attachment.bin>