Theory Boustrophedon_Transform_Impl_Test
section ‹Code generation tests›
theory Boustrophedon_Transform_Impl_Test
imports
Boustrophedon_Transform_Impl
Euler_Numbers
"HOL-Library.Code_Lazy"
"HOL-Library.Code_Target_Numeral"
begin
text ‹
We now test all the various functions we have implemented.
›
value "zigzag_number 100"
value "zigzag_numbers 100"
value "secant_number 100"
value "secant_numbers 100"
value "tangent_number 100"
value "tangent_numbers 100"
value "euler_number 100"
value "entringer_number 100 32"
value "Bernpolys 20 :: real poly list"
value "Bernpoly 10 :: real poly"
value "Bernpoly 51 :: real poly"
value "bernpoly 10 (1/2) :: real"
value "Euler_polys 20 :: rat poly list"
value "Euler_poly 10 :: rat poly"
value "Euler_poly 51 :: rat poly"
value "euler_poly 51 (3/2) :: real"
code_lazy_type stream
text ‹
As an example of the Boustrophedon transform, the following is the transform of the sequence
$1, 0, 0, 0, \ldots$ with the exponential generating function $1$.
The transformed sequence is the zigzag numbers, with the exponential generating
function $\sec x + \tan x$.
›
value "stake 20 (seidel_triangle_rows (1 ## sconst (0::int)))"
value "stake 20 (boustrophedon_stream (1 ## sconst (0::int)))"
text ‹
The following is another example from the paper by Millar et al: the
Boustrophedon transform of the sequence $1, 1, 1, \ldots$ with the exponential
generating function $e^x$.
The exponential generating function of the transformed sequence is
$e^x (\sec x + \tan x)$.
›
value "stake 20 (seidel_triangle_rows (sconst (1::int)))"
value "stake 20 (boustrophedon_stream (sconst (1::int)))"
end