Re: [isabelle] Rational numbers in Isabelle/ML



That should be quite possible, and I expect the proofs to be very easy, if not completely automatic.

Manuel


On 03/04/16 14:01, Makarius wrote:
On Sun, 3 Apr 2016, Manuel Eberl wrote:

* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are
     these actually correct?
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.

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 Echelon_Form.


    Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.