*** 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
