theory Lorenz_Experiments
imports Lorenz_Approximation
begin

text {*  [0.783524,0.788492][2.148113,2.153095][27.00] *}
definition "R121_61 = aform_of_ivl
  (FloatR 7057356788871681 -53, FloatR 4825901986503079 -51, 27)
  (FloatR 7102104554769234 -53, FloatR 4837120453174859 -51, 27)"

va lue "poincare_distance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R121_61]"


text {*  [0.783524,0.788492][2.148113,2.153095][27.00] *}
definition "R121_62 = aform_of_ivl
  (FloatR 7057356788871681 -53, FloatR 4837120453174859 -51, 27)
  (FloatR 7102104554769234 -53, FloatR 4848338919846639 -51, 27)"

value [code] "poincare_di stance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R121_62] (0, 0, 1) (107/2/2)"

text {* [0.778556,0.783524][2.133167,2.138149][27.00] *}
definition "R121_48 = aform_of_ivl
  (FloatR 7012609022974128 -53, FloatR 4803465053159519 -51, 27)
  (FloatR 7057356788871681 -53, FloatR 4814683519831299 -51, 27)"

value [code] "poi ncare_distance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R121_48] (0, 0, 1) (107/2/2)"

text {* [0.753720,0.758687][2.073385,2.078367][27.00] *}
definition "R121_1 = aform_of_ivl
  (FloatR 6788906222283380 -53, FloatR 4668847956697788 -51, 27)
  (FloatR 6833644980981679 -53, FloatR 4680066423369568 -51, 27)"

value [code] "poincare_dist ance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R121_1] (0, 0, 1) (107/2/2)"

text {* [0.919512,0.979231][2.106930,2.226795][27.00] *}
definition "R124 = aform_of_ivl
  (FloatR 235 -8, FloatR 539 -8, 27)
  (FloatR 251 -8, FloatR 571 -8, 27)"

value [code] "poincare_d istance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R124] (0, 0, 1) (107/2/2)"

text {* R1: (-4.407000, -0.980000) - (-4.377150, -0.854989) *}
definition "R1 = aform_of_ivl
  (FloatR -1127 -8, FloatR -251 -8, 27::real)
  (FloatR -1120 -8, FloatR -216 -8, 27)"

value [code] "poincare_d istance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R1] (0, 0, 1) (107/2/2)"
(*
value [code] "poincares2_iter (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [(aform_of_ivl (FloatR -1127 -8, FloatR -251 -8, 27::real) (FloatR -1120 -8, FloatR -216 -8, 27), ((0,0,1), 10))]"
*)

text {*
  R1R: part of the return
  R1R: (4.765, 2.86) - (4.775, 2,81) *}
definition "R1R = aform_of_ivl
  (FloatR 5364913056105103 -50, FloatR 6327557476455547 -51, 27::real)
  (FloatR 5376172055173530 -50, FloatR 6440147467139809 -51, 27)"

value [code] "poincare_dist ance_d_print (uncurry_options lorenz) (uncurry_options lorenz_d) lorenz_optns
  [R1R] (0, 0, 1) (107/2/2)"


definition "lorenz_poincare_d = lorenz.poincare_distance_d_print lorenz_optns"

subsection {* leftmost rect, easy *}


value [code] "case lorenz.euler_step lorenz_optns R1 1 of Some (a, CX, X) \<Rightarrow>
  let
    _ = print_aform R1;
    _ = print_aform CX;
    _ = print_aform X
  in ()"
definition "test1 (x::unit) = lorenz_poincare_d [R1]"








export_code test1 in SML module_name T file "lorenz_test.ML"
ML {*
  PolyML.profiling 1;
  use  "/Users/immler/work/afp/afp-nfm/thys/Ordinary_Differential_Equations/Ex/lorenz_test.ML";
*}
ML {*
  PolyML.exception_trace (T. test1);
*}

subsection {* close to Gamma on the right*}

text {* [0.919512,0.979231][2.106930,2.226795][27.00] *}
definition "R124 = aform_of_ivl
  (FloatR 235 -8, FloatR 539 -8, 27)
  (FloatR 251 -8, FloatR 571 -8, 27)"

value [code] "lorenz 53 (FloatR 1 -8) R124"






definition "test2 (x::unit) = lorenz_poincare_d [R124]"

export_code test2 in SML module_name T file "lorenz_test.ML"
ML {*
  PolyML.profiling 0;
  use  "/User s/immler/work/afp/afp-nfm/thys/Ordinary_Differential_Equations/Ex/lorenz_test.ML";
*}
ML {*
  PolyML.exception _trace (T.test2);
*}


subsection {* Manual sections for local Poincare maps*}

definition "lorenz_poincare = lorenz.poincare_series
    \<lparr>
    precision = 30,
    tolerance = FloatR 1 -9,
    stepsize  = FloatR 1 -9,
    min_stepsize  = FloatR 1 -12,
    iterations = 40,
    halve_stepsizes = 10,
    widening_mod = 40,
    max_tdev_thres = FloatR 1 -7,
    presplit_summary_tolerance = FloatR 1 1,
    collect_mod = 12000000,
    collect_granularity = FloatR 1 -7,
    printing_fun = print_results 1,
    result_fun = ivls_result 20 40
  \<rparr>"

subsection {* leftmost rect *}

definition "R1' = aform_of_ivl
  (FloatR -1127 -8, FloatR -251 -8, 27)
  (FloatR -1126 -8, FloatR -250 -8, 27)"

definition "test2 (x::unit) = lorenz_poincare [R1']
  [((0, 0, 1), 103/2/2),
  ((1, 0, 0), -173/2/2/2/2/2),
  ((0, 0, -1), -103/2/2),
  ((0, 0, -1), -27),
  ((0, 0, -1), -57/2),
  ((-1, 0, 0), 23/2/2),
  ((-1, 0, 0), 21/2/2),
  ((0, 0, 1), 27)]"

export_code test2 in SML module_name T file "lorenz_test.ML"
ML {*
  PolyML.profiling 1;
  use "/Users/immler/work/afp/afp-nfm/thys/Ordinary_Differential_Equations/Ex/lorenz_test.ML";
*}
ML {*
  PolyML.exception_trace (T.test2);
*}


definition "test2 (x::unit) = lorenz_poincare [R124]
  [((0, 0, 1), 18),
   ((0, 0, 1), 29/2),
   ((0, 0, 1), 10),
   ((-1, 0, 0), -5/2),
   ((-1, 0, 0), -6),
   ((0, 0, -1), -14),
   ((0, 0, -1), -20),
   ((0, 0, -1), -25),
   ((0, 0, -1), -30),
   ((0, 0, -1), -35),
   ((0, 0, -1), -40),
   ((0, 0, -1), -43),
   ((1, 0, 0), 9),
   ((0, 0, 1), 41),
   ((0, 0, 1), 34),
   ((0, 0, 1), 27)]"

export_code test2 in SML module_name T file "lorenz_test.ML"
ML {*
  PolyML.profiling 1;
  use "/Users/immler/work/afp/afp-nfm/thys/Ordinary_Differential_Equations/Ex/lorenz_test.ML";
*}

ML {*
  PolyML.excep tion_trace (T.test2);
*}

definition "R344 = aform_of_ivl
  (FloatR 193 -8, FloatR 531 -8, 27)
  (FloatR 194 -8, FloatR 532 -8, 27)"

end
