[isabelle-dev] NEWS: Primes

[Manuel Eberl]

*** 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