wneuper/isa: test/Tools/isac/OLDTESTS/scriptnew.sml@255c853ea2f0

     1 (* use"../systest/scriptnew.sml";

     2    use"systest/scriptnew.sml";

     3    use"scriptnew.sml";

     4    *)

     6 (*contents*)

     7 " --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

     8 " --- test  9.5.02 Testeq: While Try Repeat @@ ------------------ ";

     9 " --- test 11.5.02 Testeq: let e_e =... in [e_] ------------------ ";

    10 " _________________ me + nxt_step from script ___________________ ";

    11 " _________________ me + sqrt-equ-test: 1.norm_equation  ________ ";

    12 " _________________ equation with x =(-12)/5, but L ={} ------- ";

    13 "------------------ script with Map, Subst (biquadr.equ.)---------";

    14 (*contents*)

    19 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    20 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    21 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    22 KEStore_Elems.add_pbts

    23   [prep_pbt Test.thy "pbl_testss" [] e_pblID

    24       (["tests"], []:(string * string list) list, e_rls, NONE, []),

    25     prep_pbt Test.thy "pbl_testss_term" [] e_pblID

    26       (["met_testterm","tests"],

    27         [("#Given" ,["realTestGiven g_"]),

    28           ("#Find"  ,["realTestFind f_"])],

    29         e_rls, NONE, [])]

    30   thy;

    32 store_met

    33  (prep_met Test.thy "met_test_simp" [] e_metID

    34  (*test for simplification*)

    35  (["Test","met_testterm"]:metID,

    36   [("#Given" ,["realTestGiven g_"]),

    37    ("#Find"  ,["realTestFind f_"])

    38    ],

    39    {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    40     crls=tval_rls, errpats = [], nrls=e_rls(*,

    41     asm_rls=[],asm_thm=[]*)},

    42  "Script Testterm (g_::real) =   \

    43  \Repeat\

    44  \  ((Repeat (Rewrite rmult_1 False)) Or\

    45  \   (Repeat (Rewrite rmult_0 False)) Or\

    46  \   (Repeat (Rewrite radd_0 False))) g_"

    47  ));

    48 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];

    49 val (dI',pI',mI') = ("Test",["met_testterm","tests"],

    50 		     ["Test","met_testterm"]);

    51 (*val p = e_pos'; val c = [];

    52 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

    53 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)

    54 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    57 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    58 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    61 (*val nxt = ("Apply_Method",Apply_Method ("Test","met_testterm"))*)

    62 (*----script 111 ------------------------------------------------*)

    63 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    64 (*"(#0 + #0) * (#1 * (#1 * a))"  nxt= Rewrite ("rmult_1",*)

    65 (*----script 222 ------------------------------------------------*)

    66 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    67 (*"(#0 + #0) * (#1 * a)"         nxt= Rewrite ("rmult_1",*)

    68 (*----script 333 ------------------------------------------------*)

    69 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    70 (*"(#0 + #0) * a"                nxt= Rewrite ("radd_0",*)

    71 (*----script 444 ------------------------------------------------*)

    72 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    73 (*"#0 * a"*)

    74 (*----script 555 ------------------------------------------------*)

    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    76 (*"#0"*)

    77 if p=([4],Res) then ()

    78 else error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));

    79 (*----script 666 ------------------------------------------------*)

    80 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    81 (*"#0"*)

    82 if nxt=("End_Proof'",End_Proof') then ()

    83 else error "new behaviour in 30.4.02 Testterm: End_Proof";

    89 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    90 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    91 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    92 KEStore_Elems.add_pbts

    93   [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID

    94       (["met_testeq","tests"],

    95         [("#Given" ,["boolTestGiven e_e"]),

    96           ("#Find"  ,["boolTestFind v_i_"])],

    97         e_rls, NONE, [])]

    98   thy;

   100 store_met

   101  (prep_met Test.thy "met_test_eq1" [] e_metID

   102  (["Test","testeq1"]:metID,

   103    [("#Given",["boolTestGiven e_e"]),

   104    ("#Where" ,[]),

   105    ("#Find"  ,["boolTestFind v_i_"])

   106    ],

   107    {rew_ord'="tless_true",rls'=tval_rls,

   108     srls=append_rls "testeq1_srls" e_rls

   109 		    [Calc ("Test.contains'_root", eval_contains_root"")],

   110     prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls

   111 		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},

   112  "Script Testeq (e_e::bool) =                                        \

   113    \(While (contains_root e_e) Do                                     \

   114    \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \

   115    \  (Try (Repeat (Rewrite square_equation_left True))) @@ \

   116    \  (Try (Repeat (Rewrite radd_0 False)))))\

   117    \ e_e"

   118  ));

   120 val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",

   121 	   "boolTestFind v_i_"];

   122 val (dI',pI',mI') = ("Test",["met_testeq","tests"],

   123 		     ["Test","testeq1"]);

   124 val Prog sc = (#scr o get_met) ["Test","testeq1"];

   125 atomt sc;

   126 (*val p = e_pos'; val c = [];

   127 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   128 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)

   129 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   130 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   131 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   132 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   133 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   134 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   135 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   136 (*val nxt = ("Apply_Method",Apply_Method ("Test","testeq1")) *)

   137 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   138 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   139 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   140 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))

   141 val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)

   142 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   144 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   145 (*** No such constant: "Test.contains'_root"  *)

   147 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   148 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso

   149    nxt=("End_Proof'",End_Proof') then ()

   150 else error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";

   155 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

   156 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

   157 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

   158 store_met

   159  (prep_met Test.thy "met_test_let" [] e_metID

   160  (["Test","testlet"]:metID,

   161    [("#Given",["boolTestGiven e_e"]),

   162    ("#Where" ,[]),

   163    ("#Find"  ,["boolTestFind v_i_"])

   164    ],

   165    {rew_ord'="tless_true",rls'=tval_rls,

   166     srls=append_rls "testlet_srls" e_rls

   167 		    [Calc ("Test.contains'_root",eval_contains_root"")],

   168     prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls

   169 		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},

   170    "Script Testeq2 (e_e::bool) =                                        \

   171    \(let e_e =\

   172    \  ((While (contains_root e_e) Do                                     \

   173    \   (Rewrite square_equation_left True))\

   174    \   e_e)\

   175    \in [e_::bool])"

   176    ));

   177 val Prog sc = (#scr o get_met) ["Test","testlet"];

   178 writeln(term2str sc);

   179 val fmz = ["boolTestGiven (sqrt a = 0)",

   180 	   "boolTestFind v_i_"];

   181 val (dI',pI',mI') = ("Test",["met_testeq","tests"],

   182 		     ["Test","testlet"]);

   183 (*val p = e_pos'; val c = [];

   184 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   185 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)

   186 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   187 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   188 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   189 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   190 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   191 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   192 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   193 (*val nxt = ("Apply_Method",Apply_Method ("Test","testlet"))*)

   194 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   195 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   196 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;

   197 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso

   198    nxt=("End_Proof'",End_Proof') then ()

   199 else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";

   204 " _________________ me + nxt_step from script _________________ ";

   205 " _________________ me + nxt_step from script _________________ ";

   206 " _________________ me + nxt_step from script _________________ ";

   207 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   208 	   "solveFor x","solutions L"];

   209 val (dI',pI',mI') =

   210   ("Test",["sqroot-test","univariate","equation","test"],

   211    ["Test","sqrt-equ-test"]);

   212 val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];

   213 writeln(term2str sc);

   215 "--- s1 ---";

   216 (*val p = e_pos'; val c = [];

   217 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   218 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

   219 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   220 "--- s2 ---";

   221 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   222 (* val nxt =

   223   ("Add_Given",

   224    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

   225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   226 "--- s3 ---";

   227 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)

   228 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   229 "--- s4 ---";

   230 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

   231 "--- s5 ---";

   232 (* val nxt = ("Add_Find",Add_Find "solutions L");*)

   233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   234 "--- s6 ---";

   235 (* val nxt = ("Specify_Theory",Specify_Theory "Test");*)

   236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   237 "--- s7 ---";

   238 (* val nxt =

   239   ("Specify_Problem",

   240    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

   241 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   242 "--- s8 ---";

   243 (* val nxt = ("Specify_Method",Specify_Method ("Test","sqrt-equ-test"));*)

   244 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   245 "--- s9 ---";

   246 (* val nxt = ("Apply_Method",Apply_Method ("Test","sqrt-equ-test"));*)

   247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   248 "--- 1 ---";

   249 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

   250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   251 "--- 2 ---";

   252 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   254 "--- 3 ---";

   255 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

   256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   257 "--- 4 ---";

   258 (* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)

   259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   260 "--- 5 ---";

   261 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   262 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   263 "--- 6 ---";

   264 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

   265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   266 "--- 7 ---";

   267 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   268 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   269 "--- 8<> ---";

   270 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

   271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   272 "--- 9<> ---";

   273 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   275 "--- 10<> ---";

   276 (* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)

   277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   278 "--- 11<> ---";

   279 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   281 "--- 12<> ---.";

   282 (* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)

   283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   284 "--- 13<> ---";

   285 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   286 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   287 "--- 14<> ---";

   288 (* nxt = ("Check_Postcond",Check_Postcond ("Test","sqrt-equ-test"));*)

   289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   290 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))

   291 then error "scriptnew.sml 1: me + tacs from script: new behaviour"

   292 else ();

   293 "--- 15<> ---";

   294 (* val nxt = ("End_Proof'",End_Proof');*)

   295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   297 writeln (pr_ctree pr_short pt);

   298 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^

   299 "\n=============================================================");

   300 (*get_obj g_asm pt [];

   301 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)

   307 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   308 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   309 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   310 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   311 	   "solveFor x","errorBound (eps=0)",

   312 	   "solutions L"];

   313 val (dI',pI',mI') =

   314   ("Test",["sqroot-test","univariate","equation","test"],

   315    ["Test","sqrt-equ-test"]);

   316  val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];

   317  (writeln o term2str) sc;

   318 "--- s1 ---";

   319 (*val p = e_pos'; val c = [];

   320 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   321 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

   322 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   323 "--- s2 ---";

   324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   325 (* val nxt = ("Add_Given",

   326    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

   327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   328 "--- s3 ---";

   329 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)

   330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   331 "--- s4 ---";

   332 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

   333 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)

   334 "--- s5 ---";

   335 (* val nxt = ("Add_Find",Add_Find "solutions L");*)

   336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   337 "--- s6 ---";

   338 (* val nxt = ("Specify_Theory",Specify_Theory "Test");*)

   339 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   340 "--- s7 ---";

   341 (* val nxt = ("Specify_Problem",

   342    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

   343 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   344 "--- s8 ---";

   345 (* val nxt = ("Specify_Method",Specify_Method ("Test","sqrt-equ-test"));*)

   346 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   347 "--- s9 ---";

   348 (* val nxt = ("Apply_Method",Apply_Method ("Test","sqrt-equ-test"));*)

   349 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   350 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)

   351 "--- !!! x1 --- 1.norm_equation";

   352 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");

   353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   354 "--- !!! x2 --- 1.norm_equation";

   355 (*meNEW: "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2" -- NICHT norm_equation!!*)

   356 (*meOLD: "sqrt (9 + 4 * x) + -1 * (sqrt x + sqrt (5 + x)) = 0"*)

   357 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   358 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   359 (*"-1 * sqrt x + (-1 * sqrt (5 + x) + sqrt (9 + 4 * x)) = 0"*)

   360 (*(me nxt p [1] pt) handle e => print_exn_G e;*)

   361 "--- !!! x3 --- 1.norm_equation";

   362 (*val nxt = ("Empty_Tac",Empty_Tac) ### helpless*)

   363 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

   364 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   365 "--- !!! x4 --- 1.norm_equation";

   366 (*"-1 * sqrt x + -1 * sqrt (5 + x) + sqrt (9 + 4 * x) = 0"*)

   367 (*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)

   368 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   369 "--- !!! x5 --- 1.norm_equation";

   370 (*"sqrt (9 + 4 * x) = 0 + -1 * (-1 * sqrt x + -1 * sqrt (5 + x))"*)

   371 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   372 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   374 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:

   375 if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))

   376 then() else error "new behaviour in test-example 1.norm sqrt-equ-test";

   377 #################################################*)

   379 (* use"../tests/scriptnew.sml";

   380    *)

   382 " _________________ equation with x =(-12)/5, but L ={} ------- ";

   384 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",

   385 	   "solveFor x","errorBound (eps=0)",

   386 	   "solutions L"];

   387 val (dI',pI',mI') =

   388   ("Test",["sqroot-test","univariate","equation","test"],

   389    ["Test","square_equation"]);

   391 (*val p = e_pos'; val c = [];

   392 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   393 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

   394 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   396 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   397 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   398 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   399 (*val nxt = ("Apply_Method",Apply_Method ["Test","square_equation"])*)

   400 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   401 (*val nxt = "square_equation_left",

   402       "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)

   403 get_assumptions_ pt p;

   404 (*it = [] : string list;*)

   405 trace_rewrite:=true;

   406 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   407 trace_rewrite:=false;

   408 val asms = get_assumptions_ pt p;

   409 if asms = [(str2term "0 <= 9 + 4 * x",[1]),

   410 	   (str2term "0 <= x",[1]),

   411 	   (str2term "0 <= -3 + x",[1])] then ()

   412 else error "scriptnew.sml diff.behav. in sqrt assumptions 1";

   414 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   415 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   416 (*val nxt = Rewrite ("square_equation_left",     *)

   417 val asms = get_assumptions_ pt p;

   418 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];

   419 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   420 val asms = get_assumptions_ pt p;

   421 if asms = [(str2term "0 <= 9 + 4 * x",[1]),

   422 	   (str2term "0 <= x",[1]),

   423 	   (str2term "0 <= -3 + x",[1]),

   424 	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),

   425 	   (str2term "0 <= 6 + x",[6])] then ()

   426 else error "scriptnew.sml diff.behav. in sqrt assumptions 2";

   428 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   429 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   430 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   431 (*val nxt = Subproblem ("Test",["LINEAR","univariate","equation","test"*)

   432 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   433 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   434 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   435 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   436 (*val nxt = ("Apply_Method",Apply_Method ["Test","solve_linear"])*)

   437 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   438 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   439 (*val nxt =

   440   ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equation","test"])*)

   441 val asms = get_assumptions_ pt p;

   442 if asms = [] then ()

   443 else error "scriptnew.sml diff.behav. in sqrt assumptions 3";

   444 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   445 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

   447 val asms = get_assumptions_ pt p;

   448 if asms = [(str2term "0 <= 9 + 4 * x",[1]),

   449 	   (str2term "0 <= x",[1]),

   450 	   (str2term "0 <= -3 + x",[1]),

   451 	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),

   452 	   (str2term "0 <= 6 + x",[6])] then ()

   453 else raise

   454     error "scriptnew.sml: diff.behav. at Check_elementwise [x = -12 / 5]";

   456 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   457 (*val nxt = Check_Postcond ["sqroot-test","univariate","equation","test"])*)

   458 val asms = get_assumptions_ pt p;

   459 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),

   460    ("0 <= x ^^^ 2 + -3 * x",[6]),("0 <= 6 + x",[6]),

   461    ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",

   462     [13])];

   465 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   466 val Form' (FormKF (_,_,_,_,ff)) = f;

   467 if ff="[x = -12 / 5]"

   468 then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")

   469 else error "diff.behav. in scriptnew.sml; root-eq: L = []";

   471 val asms = get_assumptions_ pt p;

   472 if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),

   473 	   (str2term "0 <= -12 / 5", []),

   474 	   (str2term "0 <= -3 + -12 / 5", []),

   475 	   (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []),

   476 	   (str2term "0 <= 6 + -12 / 5", [])] then ()

   477 else error "scriptnew.sml diff.behav. in sqrt assumptions 4";

   480 "------------------ script with Map, Subst (biquadr.equ.)---------";

   481 "------------------ script with Map, Subst (biquadr.equ.)---------";

   482 "------------------ script with Map, Subst (biquadr.equ.)---------";

   485 (*GoOn.5.03. script with Map, Subst (biquadr.equ.)

   486 val scr = Prog (((inst_abs thy) o Thm.term_of o the o (parse thy))

   487     "Script Biquadrat_poly (e_e::bool) (v_::real) =                       \

   488     \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_;        \

   489     \     L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met])   \

   490     \             [BOOL e_e, REAL v_0_]);                               \

   491     \     L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@                  \

   492     \                  ((Rewrite real_root_positive False) Or            \

   493     \                   (Rewrite real_root_negative False)) @@           \

   494     \                  OrToList) L_0_                                    \

   495     \ in (flat ....))"

   496 );

   498 *)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59188	c477d0f79ab9
child 59395	862eb17f9e16
permissions	-rw-r--r--