On 19/07/16 10:17, Lars Hupel wrote:
>>> How can I extract this information from within Isabelle/Scala? How would
>>> this information be presented?
>>
>> It is emitted into the session log file. Build.parse_log may serve as an
>> example how to access it.
>
> Is there no structured way of accessi
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
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
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.
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?
_
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
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 m
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 cha
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
>> How can I extract this information from within Isabelle/Scala? How would
>> this information be presented?
>
> It is emitted into the session log file. Build.parse_log may serve as an
> example how to access it.
Is there no structured way of accessing this information? At least it's
Scala but
10 matches
Mail list logo
