[isabelle-dev] Isabelle_01-Jun-2016 snapshot
This is just a totally arbitrary snapshot in the middle of the release cycle: http://www4.in.tum.de/~wenzelm/test/Isabelle_01-Jun-2016 It might help to check if Java 8u92 works on all platforms. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
>> Both are ok in my view; ironically, lcm is used more often in >> Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, >> though: >> >> Integer.gcd = PolyML.gcd >> Integer.lcm = abs oo PolyML.lcm > > These two lines are the plan. Is that a good one or a bad one? I tinkered around with (a) fractions.gcd in Python and (b) http://api.mathjs.org/ (a) has mixed signs for gcd (b) has everything normalized Maybe this is evidence that we are rather free in choosing our sign rules, and then normalizing could be a legitimate choice, conceeding that most practical occuring lcm computations concern non-negative denominators. Cheers, Florian > > Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for > rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML > library environment to refer to structure PolyML. > > > BTW, AFP has special code generator setup for PolyML.IntInf.gcd here: > > https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy?at=default=file-view-default#Code_Generation_IArrays_SML.thy-33 > > https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy?at=default=file-view-default#Examples_Echelon_Form_IArrays.thy-44 > > Luckily, this is only gcd and not lcm, so it coincides already. > > > Makarius > > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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] NEWS: Rat in Isabelle/ML
On 01/06/16 21:47, Lawrence Paulson wrote: > Doesn’t Poly/ML include an option to support GCDs (if not rationals) > efficiently? Do you mean PolyML.IntInf.gcd and PolyML.IntInf.lcm? That is already used (da38571dd5bd). These operations normally use GNU MP, but on Mac OS X only the old builtin bigints of Poly/ML. (I still don't know how to compile Poly/ML with libgmp such that the binary becomes self-contained.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rat in Isabelle/ML
On 01/06/16 21:58, Florian Haftmann wrote: > > One could regard the dedicated literal syntax for rationals a little bit > oversophisticated; maybe an infix // for Rat.make would serve better. > Or we could A matter of personal taste, though. There is a delicate point here: our antiquotation infrastructure distinguishes inlined text from compile-time values. @a/b is the latter, so it is always guaranteed to be pre-evaluated, independently of other code inline options of Poly/ML. This is also the reason why I have removed Rat.zero, Rat.one, Rat.two and used @0, @1, @2 everywhere. Makarius 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: Rat in Isabelle/ML
> * Structure Rat for rational numbers is now an integral part of
> Isabelle/ML, with special notation @int/nat or @int for numerals (an
> abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
> printing. Standard operations on type Rat.rat are provided via ad-hoc
> overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
> use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
> superseded by General.Div.
>
>
> This refers to Isabelle/c7de5b311909, which also contains the updated
> documentation.
>
> The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
> the existing syntax very little, see 921a5be54132. Further changesets in
> the vicinity clean up rat.ML is various repects -- it is surprising how
> many details can be missing in such a small module.
>
> I have compared it with the MyRat implementation by Manuel Eberl
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
> as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
> b11e8139b880 (where a comment says that it goes back to John Harrison).
>
>
> Further comments? Anything missing?
Very fine. Indeed rat.ML has been one of my first Isabelle playgrounds,
and I did not have much experience then.
One could regard the dedicated literal syntax for rationals a little bit
oversophisticated; maybe an infix // for Rat.make would serve better.
Or we could A matter of personal taste, though.
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] Proper sign of gcd / lcm on type int
On 01/06/16 21:27, Florian Haftmann wrote: > Note that the mixed signs of PolyML.IntInf.lcm maintain the property > > gcd a b * lcm a b = a * b > > whereas the lcm in GCD.thy obeys > > gcd a b * lcm a b = normalize a * normalize b > > which emphasises the dual nature of the gcd/lcm lattice. > > Both are ok in my view; ironically, lcm is used more often in > Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, > though: > > Integer.gcd = PolyML.gcd > Integer.lcm = abs oo PolyML.lcm These two lines are the plan. Is that a good one or a bad one? Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML library environment to refer to structure PolyML. BTW, AFP has special code generator setup for PolyML.IntInf.gcd here: https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy?at=default=file-view-default#Code_Generation_IArrays_SML.thy-33 https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy?at=default=file-view-default#Examples_Echelon_Form_IArrays.thy-44 Luckily, this is only gcd and not lcm, so it coincides already. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Rat in Isabelle/ML
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.
This refers to Isabelle/c7de5b311909, which also contains the updated
documentation.
The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
the existing syntax very little, see 921a5be54132. Further changesets in
the vicinity clean up rat.ML is various repects -- it is surprising how
many details can be missing in such a small module.
I have compared it with the MyRat implementation by Manuel Eberl
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
b11e8139b880 (where a comment says that it goes back to John Harrison).
Further comments? Anything missing?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jdk-8u92
Isabelle/7e8ef9ac3159 is now on jdk-8u92, which Oracle has release some time ago, when I was not looking. See also http://www.oracle.com/technetwork/java/javase/2col/8u92-bugfixes-2949473.html Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper sign of gcd / lcm on type int
Hi Makarius, > presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to > understand the situation of gcd / lcm for negative arguments. > > We have the following slightly divergent operations: > > * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs") > > * PolyML.IntInf.gcd: always >= 0 > PolyML.IntInf.lcm: mixed signs, according to product of arguments > > * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only > meant to operate on "nat", which happens to be spelled "int" in ML. > > My impression is that the HOL definitions are canonical: several number > theory experts have gone over it over the years. Is this correct? well, I tend to say they are Isabelle/HOLish. You could also legitimately specify polymorphic gcd as gcd :: nat => nat => nat gcd :: int => int => nat gcd :: … but then you cannot use (single-parameter) type classes. Or you could only specify properties on equivalence classes, e.g. gcd a a =[dvd]= a where a =[dvd]= b <--> a dvd b && b dvd a but such properties cannot be used as rewrite rules of the simplifier. > An investigation of the (very few) uses of the above Poly/ML and > Isabelle/ML operations in Isabelle + AFP supports the following working > hypothesis: > > Integer.gcd / lcm should follow the HOL versions, in "normalizing" the > sign, i.e. removing it. (The updated implementation will use > PolyML.IntInf gcd for improved performance.) Note that the mixed signs of PolyML.IntInf.lcm maintain the property gcd a b * lcm a b = a * b whereas the lcm in GCD.thy obeys gcd a b * lcm a b = normalize a * normalize b which emphasises the dual nature of the gcd/lcm lattice. Both are ok in my view; ironically, lcm is used more often in Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial, though: Integer.gcd = PolyML.gcd Integer.lcm = abs oo PolyML.lcm Cheers, Florian > > > Does this sound like a good idea? > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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
