Re: [isabelle-dev] NEWS: powr
On Sun, 12 Apr 2015, Larry Paulson wrote: You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult. Does that mean there will be further changes, to make it fully work in the coming release? It would be nice to see this last-minute change properly stabilized, such that Isabelle does not degrade into continuous non-release repository-snapshot quality, like so many other projects today. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: powr
* Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y = 0 by definition. INCOMPATIBILITY: type constraints may be necessary. But I had to remove support for powr in code generation and the approximation method. If anybody thinks these are priorities for restoration, I guess we only have a few days. The problem with code generation has something to do with types. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: powr
I am not terribly happy about that. I use approximation of powr in my work on Akra–Bazzi and the Master theorem. I take it that a powr b = exp (ln a * b) still holds for positive a. I could probably apply that rewrite rule before applying approximation, but it would of course be nice if I did not have to. The issue is, however, not terribly urgent since my project is still several weeks from being finished, and I only need approximation for a small part that is independent from everything else. Manuel Larry Paulson l...@cam.ac.uk wrote: * Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y = 0 by definition. INCOMPATIBILITY: type constraints may be necessary. But I had to remove support for powr in code generation and the approximation method. If anybody thinks these are priorities for restoration, I guess we only have a few days. The problem with code generation has something to do with types. Larry ___ 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] NEWS: powr
You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult. Larry On 12 Apr 2015, at 12:26, Manuel Eberl ebe...@in.tum.de wrote: I am not terribly happy about that. I use approximation of powr in my work on Akra–Bazzi and the Master theorem. I take it that a powr b = exp (ln a * b) still holds for positive a. I could probably apply that rewrite rule before applying approximation, but it would of course be nice if I did not have to. The issue is, however, not terribly urgent since my project is still several weeks from being finished, and I only need approximation for a small part that is independent from everything else. Manuel Larry Paulson l...@cam.ac.uk wrote: * Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y = 0 by definition. INCOMPATIBILITY: type constraints may be necessary. But I had to remove support for powr in code generation and the approximation method. If anybody thinks these are priorities for restoration, I guess we only have a few days. The problem with code generation has something to do with types. Larry ___ 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] NEWS: powr
Hi Larry, * Complex powers and square roots. The functions ln and powr are now overloaded for types real and complex, and 0 powr y = 0 by definition. INCOMPATIBILITY: type constraints may be necessary. But I had to remove support for powr in code generation and the approximation method. If anybody thinks these are priorities for restoration, I guess we only have a few days. The problem with code generation has something to do with types. from inspecting your diffs hg diff -c b785d6d06430 | grep code hg diff -c 065ecea354d0 | grep code I see that both hardly tinker with code declarations anyway. And previously the definitions of ln and powr have been the same on real as they are now. So, there should hardly have been any working code setup before, and I can confirm that there is no such setup in Isabelle2014. Maybe there has been some particular support in the approximation method, but I do not know the details of that. Hope this helps, Florian Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.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] NEWS: powr
All I know is that HOL-Codegenerator_Test failed because of some (?) type-related ambiguity connected with powr, with no indication of where this instance of powr actually was. Adding [code del] to its definition eliminated the error, God knows why. Larry On 12 Apr 2015, at 20:03, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: from inspecting your diffs hg diff -c b785d6d06430 | grep code hg diff -c 065ecea354d0 | grep code I see that both hardly tinker with code declarations anyway. And previously the definitions of ln and powr have been the same on real as they are now. So, there should hardly have been any working code setup before, and I can confirm that there is no such setup in Isabelle2014. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
