Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Manuel Eberl
But is it possible to adapt all lemmas accordingly? I could imagine that some statements use the fact that the support of multiplicity are the prime numbers. Not really. Some facts will still require the primality assumption, e.g. lemma prime_multiplicity_mult_distrib: assumes "is_prime_elem

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Johannes Hölzl
I also would vote for option 3. But is it possible to adapt all lemmas accordingly?  I could imagine that some statements use the fact that the support of multiplicity are the prime numbers.  - Johannes Am Dienstag, den 19.07.2016, 12:09 +0100 schrieb Lawrence Paulson: > This is what I would do 

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Lawrence Paulson
The reason why we put x/0= 0 is because it simplifies the statements of many laws, not because of any admiration of 0. Larry > On 19 Jul 2016, at 11:24, Manuel Eberl <ebe...@in.tum.de> wrote: > > The obvious possibility would be to just let all non-prime numbers have &

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Lawrence Paulson
This is what I would do Larry Paulson > On 19 Jul 2016, at 11:03, Manuel Eberl wrote: > > 3. replace the old multilicity with the new one and adapt all lemmas > accordingly > > Currently, I tend towards the last options. Are there any other opinions on > this?

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Mario Carneiro
FWIW I can attest to your "new" definition being the standard one in Metamath. It also avoids any a priori notion of primality, which allows it to apply in more general circumstances. Mario On Tue, Jul 19, 2016 at 6:24 AM, Manuel Eberl wrote: > As far as I know,

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Manuel Eberl
As far as I know, ‘multiplicity’ in mathematics is only defined for prime factors. That is a luxury that we do not have in HOL, so the question is: How do we extend the definition to the full domain? The obvious possibility would be to just let all non-prime numbers have multiplicity 0. This

Re: [isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Tobias Nipkow
Are you sure that there is no standard definition of this concept in mathematics that we should follow? Tobias On 19/07/2016 12:03, Manuel Eberl wrote: Hallo, as some of you may already know, I am currently in the process of resructing Isabelle's definitions of prime numbers. Before these

[isabelle-dev] multiplicity and prime numbers

2016-07-19 Thread Manuel Eberl
Hallo, as some of you may already know, I am currently in the process of resructing Isabelle's definitions of prime numbers. Before these changes, we had the concept of "multiplicity". This was defined to be the multiplicity of a prime factor in the prime decomposition of a natural number or