Re: [isabelle] Rational numbers in Isabelle/ML
On Sun, 3 Apr 2016, Manuel Eberl wrote:
There is a ~ missing in MyRat.inv. That code should definitely receive a
thorough review before it goes anywhere. Rat.inv looks fine to me.
* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are
these actually correct?
How about a formally specified and verified implementation? It should be
mostly trivial with all the algebraic tools in Isabelle/HOL.
However, I would imagine that the exported could would be quite ugly.
I did not mean to use exported code, but just to make a demo theory with
all the definitions and maybe some simple proofs (e.g. in HOL/ex). The
idea is just to make certain intentions and invariants explicit, notably
the sign of certain parts.
A related question is about sign in lcm/gcd: in structure Integer,
PolyML.IntInf, and the HOL definitions. There is also a connection of
PolyML.IntInf operations with the code generator in AFP Gauss_Jordan and
This archive was generated by a fusion of
Pipermail (Mailman edition) and