*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code equations for "power"*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Mon, 11 Jan 2016 08:23:31 +0000*Accept-language*: de-DE, de-AT, en-US*In-reply-to*: <568FE115.4040500@inf.ethz.ch>*References*: <568FCF40.30901@in.tum.de> <568FE115.4040500@inf.ethz.ch>*Thread-index*: AQHRSigZ+pqFkQJQkUWoQpigf9LEdZ7xuwuAgAQyloA=*Thread-topic*: [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Ã

**References**:**[isabelle] Code equations for "power"***From:*Manuel Eberl

**Re: [isabelle] Code equations for "power"***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle2016-RC0 - AFP and Library available for testing
- Next by Date: [isabelle] lift_bnf Subscript exception
- Previous by Thread: Re: [isabelle] Code equations for "power"
- Next by Thread: Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list