Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Manuel Eberl

One remark on the diff:

+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy

This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.


Ah indeed. Jaime probably didn't know about the naming convention and I 
must have missed it. I will take care of it at once.


Manuel

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


Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Manuel Eberl
True, but even though I am hardly an expert in number theory, I would 
imagine that a solid foundation in analysis (especially complex 
analysis) is very helpful, if not indispensable, in the development of 
advanced number theory. (the most obvious example is the 
complex-analytic proof of PNT and the Riemann ζ function)


So I think if anyone wants to work on this in the future, I think we 
have a lot of nice building blocks available.


Cheers,

Manuel


On 18/10/16 13:27, Lawrence Paulson wrote:

That is great news!

It’s a pity that our coverage of number theory is minuscule compared 
with what we have for analysis. I blame John Harrison :-)


Larry

On 18 Oct 2016, at 12:11, Manuel Eberl > wrote:


I am glad to announce that as of261d42f0bfac, Old_Number_Theory is 
finally history.


A lot of the proofs are still quite messy and don't take advantage of 
the new features we now have in Number_Theory (such as a uniform 
concept of ‘primes’ and ‘prime factorisations’ for both nat and int), 
but I do not think the work necessary to achieve that is worth it.


The vast majority of the porting work was done by a student of ours, 
Jaime Mendizabal Roche, so big thanks to him. He even extended the 
‘two squares’ AFP entry a bit, showing the converse direction as well.



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


Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Florian Haftmann
Hi Manuel,

> I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
> finally history.

these are good news indeed.

One remark on the diff:

+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy

This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.

There is another pre-existing CaMlCaSe theory, MiscAlgebra; but from the
description of the theory itself this should go suitable HOL-Algebra
theories anyway.

> A lot of the proofs are still quite messy and don't take advantage of
> the new features we now have in Number_Theory (such as a uniform concept
> of ‘primes’ and ‘prime factorisations’ for both nat and int), but I do
> not think the work necessary to achieve that is worth it.

Messy proofs can be amended in case of need.  Messy definitions are more
critical since they may infect further theories, but all that seems to
have disappeared in the transition.

> The vast majority of the porting work was done by a student of ours,
> Jaime Mendizabal Roche, so big thanks to him. He even extended the ‘two
> squares’ AFP entry a bit, showing the converse direction as well.

Thanks a lot also!

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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


Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Lawrence Paulson
That is great news!

It’s a pity that our coverage of number theory is minuscule compared with what 
we have for analysis. I blame John Harrison :-)

Larry

> On 18 Oct 2016, at 12:11, Manuel Eberl  wrote:
> 
> I am glad to announce that as of 261d42f0bfac, Old_Number_Theory is finally 
> history.
> 
> A lot of the proofs are still quite messy and don't take advantage of the new 
> features we now have in Number_Theory (such as a uniform concept of ‘primes’ 
> and ‘prime factorisations’ for both nat and int), but I do not think the work 
> necessary to achieve that is worth it.
> 
> The vast majority of the porting work was done by a student of ours, Jaime 
> Mendizabal Roche, so big thanks to him. He even extended the ‘two squares’ 
> AFP entry a bit, showing the converse direction as well.
> 
> 
> 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