Re: [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.


-----Original Message-----
From: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] On Behalf Of Tobias Nipkow
Sent: Wednesday, November 09, 2011 11:08 PM
To: cl-isabelle-users at
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.


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 ""
> I am getting the following error message ### No code equation for 
> 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

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