*To*: Tobias Nipkow <nipkow at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] No Code Equation for LIMSEQ*From*: Dave Thayer <dathayer at microsoft.com>*Date*: Thu, 10 Nov 2011 20:23:05 +0000*Accept-language*: en-US*In-reply-to*: <4EBB7869.4030900@in.tum.de>*References*: <717F714B587F944C88837A99AA4D008149DD634A@TK5EX14MBXC111.redmond.corp.microsoft.com> <4EBB7869.4030900@in.tum.de>*Thread-index*: AcyfNozxs7xbT8r0ReC7WbM2iBlcPwAhAsSAAArozuA=*Thread-topic*: [isabelle] No Code Equation for LIMSEQ

We are trying to create hypothetical explanations couched in HOL terms for a set of orbital observations and create an executable piece of code that determines how well the observations act as a model for our theory. Therefore creating a function that accepts real values as floats is quite acceptable. David -----Original Message----- From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Tobias Nipkow Sent: Wednesday, November 09, 2011 11:08 PM To: cl-isabelle-users at lists.cam.ac.uk Subject: Re: [isabelle] No Code Equation for LIMSEQ You are trying to generate code for real numbers and functions defined by limits. Such definitions are not executable. You have two choices: you can generate code that utilizes machine floats, or you can generate code that realizes arbitrary precision interval arithmetic. The former is a quick hack, the latter is sound but more work. Depending on what you want, we can tell you how to do it. Tobias Am 10/11/2011 00:23, schrieb Dave Thayer: > For technical reasons I am restricted at the moment to using > Isabelle2009 I am trying to use code generation to generate code for trigonometric functions and other functions that utilize the real datatype. > > I have the following code that is attempting to exercise this ability. > > definition test_pi :: "real" where "test_pi = pi" > definition test_sin :: "real => real" where "test_sin x = sin x" > definition test_cos :: "real => real" where "test_cos x = cos x" > definition test_tan :: "real => real" where "test_tan x = tan x" > definition test_arcsin :: "real => real" where "test_arcsin x = arcsin x" > definition test_arccos :: "real => real" where "test_arccos x = arccos x" > definition test_arctan :: "real => real" where "test_arctan x = arctan x" > definition test_trig :: "real => real => real => real" where "test_trig x y a = cos (arctan (y / x) + sin a - pi/4)" > > export_code > test_pi test_sin test_cos test_tan > test_arcsin test_arccos test_arctan > test_trig > in OCaml > module_name "TestCodeGen" > file "TestCodeGen3.ml" > > I am getting the following error message ### No code equation for > LIMSEQ, The > > Does anybody know where the code equations for LIMSEQ are defined? > I have looked through the HOL/Library but found nothing so far. > > Thank you for your time, > David Thayer

**Follow-Ups**:**Re: [isabelle] No Code Equation for LIMSEQ***From:*Johannes Hölzl

**Re: [isabelle] No Code Equation for LIMSEQ***From:*Johannes Hölzl

**References**:**[isabelle] No Code Equation for LIMSEQ***From:*Dave Thayer

**Re: [isabelle] No Code Equation for LIMSEQ***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Previous by Thread: Re: [isabelle] recursive functions
- Next by Thread: Re: [isabelle] No Code Equation for LIMSEQ
- Cl-isabelle-users November 2011 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