[isabelle-dev] NEWS: Primes

[Manuel Eberl]

Yes, that might be a good idea.

On 27/07/16 11:24, Tobias Nipkow wrote:
> 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
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>