[isabelle-dev] multiplicity and prime numbers

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