Re: [isabelle] Code equations for "power"



Dear Manuel,


>> Lastly, I was wondering whether there was something like "divmod" in Isabelle, i.e. an
>> operation that returns both the quotient and the remainder, since most languages have a
>> corresponding operation that is more efficient than computing the two separately.
> There are various specialised divmod constants in HOL, e.g., divmod_integer, semiring_numeral_div_class.divmod and Divides.divmod_nat, but no systematic, algebraic treatment.

If you care about efficiency, you might also have a look at improved code equations for divmod, e.g., under

http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Improved_Code_Equations.html

for Isabelle 2015

and under 

http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Divmod_Int.html

for Isabelle 2016-RC0.

Best,
RenÃ


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