Re: [isabelle-dev] multiplicity and prime numbers

[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 p" "x ≠ 0" "y ≠ 0"
  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"


Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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 
> 
> 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?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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  wrote:
> 
> The obvious possibility would be to just let all non-prime numbers have 
> multiplicity 0.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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, ‘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 makes a few things look nicer (e.g. the prime factors
> are then precisely the numbers with non-zero multiplicity). However, it
> also means that the multiplicity of "X - 1" in "X² - 1" is 1, whereas the
> multiplicity of "1 - X" is 0, which I find a bit odd.
>
> A more general possibility is that which I chose, i.e. the biggest n such
> that p^n divides x. This is well-defined as long as x is non-zero and p is
> not a unit. I would argue that having a more general notion like this is
> nicer.
>
>
> Cheers,
>
> Manuel
>
>
>
> On 19/07/16 12:18, Tobias Nipkow wrote:
>
>> 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 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 an integer. The
>>> multiplicity of a non-prime was defined to be 0.
>>>
>>> I have now created an alternative definition of "multiplicity" which
>>> is simply
>>> defined as "the highest power that is still a divisor" (as long as
>>> this is
>>> well-defined); e.g. the multiplicity of -4 in 64 would be 3.
>>>
>>> I see three possibilities:
>>> 1. redefine my "new", more general multiplicity to the "old" multiplicity
>>> 2. keep both notions of multiplicity around with different names
>>> 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?
>>>
>>>
>>> Cheers,
>>>
>>> Manuel
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>>
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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 makes a few things look nicer (e.g. the prime 
factors are then precisely the numbers with non-zero multiplicity). 
However, it also means that the multiplicity of "X - 1" in "X² - 1" is 
1, whereas the multiplicity of "1 - X" is 0, which I find a bit odd.


A more general possibility is that which I chose, i.e. the biggest n 
such that p^n divides x. This is well-defined as long as x is non-zero 
and p is not a unit. I would argue that having a more general notion 
like this is nicer.



Cheers,

Manuel


On 19/07/16 12:18, Tobias Nipkow wrote:

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 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 an integer. The
multiplicity of a non-prime was defined to be 0.

I have now created an alternative definition of "multiplicity" which
is simply
defined as "the highest power that is still a divisor" (as long as
this is
well-defined); e.g. the multiplicity of -4 in 64 would be 3.

I see three possibilities:
1. redefine my "new", more general multiplicity to the "old" multiplicity
2. keep both notions of multiplicity around with different names
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?


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[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 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 an integer. The
multiplicity of a non-prime was defined to be 0.

I have now created an alternative definition of "multiplicity" which is simply
defined as "the highest power that is still a divisor" (as long as this is
well-defined); e.g. the multiplicity of -4 in 64 would be 3.

I see three possibilities:
1. redefine my "new", more general multiplicity to the "old" multiplicity
2. keep both notions of multiplicity around with different names
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?


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev