wneuper/isa: test/Tools/isac/OLDTESTS/scriptnew.sml@73dc85c025ab

     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 store_pbt

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

    24  (["tests"],

    25   []:(string * string list) list,

    26   e_rls, NONE, []));

    27 store_pbt

    28  (prep_pbt Test.thy "pbl_testss_term" [] e_pblID

    29  (["met_testterm","tests"],

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

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

    32   ],

    33   e_rls, NONE, []));

    35 Test_KEStore_Elems.add_pbts

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

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

    38     prep_pbt Test.thy "pbl_testss_term" [] e_pblID

    39       (["met_testterm","tests"],

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

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

    42         e_rls, NONE, [])]

    43   thy;

    45 store_met

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

    47  (*test for simplification*)

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

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

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

    51    ],

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

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

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

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

    56  \Repeat\

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

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

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

    60  ));

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    75 (*----script 111 ------------------------------------------------*)

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

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

    78 (*----script 222 ------------------------------------------------*)

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

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

    81 (*----script 333 ------------------------------------------------*)

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

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

    84 (*----script 444 ------------------------------------------------*)

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

    86 (*"#0 * a"*)

    87 (*----script 555 ------------------------------------------------*)

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

    89 (*"#0"*)

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

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

    92 (*----script 666 ------------------------------------------------*)

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

    94 (*"#0"*)

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

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

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

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

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

   105 store_pbt

   106  (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID

   107  (["met_testeq","tests"],

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

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

   110   ],

   111   e_rls, NONE, []));

   112 Test_KEStore_Elems.add_pbts

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

   114       (["met_testeq","tests"],

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

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

   117         e_rls, NONE, [])]

   118   thy;

   120 store_met

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

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

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

   124    ("#Where" ,[]),

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

   126    ],

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

   128     srls=append_rls "testeq1_srls" e_rls

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

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

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

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

   133    \(While (contains_root e_e) Do                                     \

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

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

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

   137    \ e_e"

   138  ));

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

   141 	   "boolTestFind v_i_"];

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

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

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

   145 atomt sc;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   178 store_met

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

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

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

   182    ("#Where" ,[]),

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

   184    ],

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

   186     srls=append_rls "testlet_srls" e_rls

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

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

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

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

   191    \(let e_e =\

   192    \  ((While (contains_root e_e) Do                                     \

   193    \   (Rewrite square_equation_left True))\

   194    \   e_e)\

   195    \in [e_::bool])"

   196    ));

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

   198 writeln(term2str sc);

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

   200 	   "boolTestFind v_i_"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   224 " _________________ me + nxt_step from script _________________ ";

   225 " _________________ me + nxt_step from script _________________ ";

   226 " _________________ me + nxt_step from script _________________ ";

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

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

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

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

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

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

   233 writeln(term2str sc);

   235 "--- s1 ---";

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

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

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

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

   240 "--- s2 ---";

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

   242 (* val nxt =

   243   ("Add_Given",

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

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

   246 "--- s3 ---";

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

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

   249 "--- s4 ---";

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

   251 "--- s5 ---";

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

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

   254 "--- s6 ---";

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

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

   257 "--- s7 ---";

   258 (* val nxt =

   259   ("Specify_Problem",

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

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

   262 "--- s8 ---";

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

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

   265 "--- s9 ---";

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

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

   268 "--- 1 ---";

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

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

   271 "--- 2 ---";

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

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

   274 "--- 3 ---";

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

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

   277 "--- 4 ---";

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

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

   280 "--- 5 ---";

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

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

   283 "--- 6 ---";

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

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

   286 "--- 7 ---";

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

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

   289 "--- 8<> ---";

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

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

   292 "--- 9<> ---";

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

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

   295 "--- 10<> ---";

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

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

   298 "--- 11<> ---";

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

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

   301 "--- 12<> ---.";

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

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

   304 "--- 13<> ---";

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

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

   307 "--- 14<> ---";

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

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

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

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

   312 else ();

   313 "--- 15<> ---";

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

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

   317 writeln (pr_ptree pr_short pt);

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

   319 "\n=============================================================");

   320 (*get_obj g_asm pt [];

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

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

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

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

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

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

   332 	   "solutions L"];

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

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

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

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

   337  (writeln o term2str) sc;

   338 "--- s1 ---";

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

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

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

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

   343 "--- s2 ---";

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

   345 (* val nxt = ("Add_Given",

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

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

   348 "--- s3 ---";

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

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

   351 "--- s4 ---";

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

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

   354 "--- s5 ---";

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

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

   357 "--- s6 ---";

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

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

   360 "--- s7 ---";

   361 (* val nxt = ("Specify_Problem",

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

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

   364 "--- s8 ---";

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

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

   367 "--- s9 ---";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   394 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:

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

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

   397 #################################################*)

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

   400    *)

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

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

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

   406 	   "solutions L"];

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

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

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

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

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

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

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

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

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

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

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

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

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

   421 (*val nxt = "square_equation_left",

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

   423 get_assumptions_ pt p;

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

   425 trace_rewrite:=true;

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

   427 trace_rewrite:=false;

   428 val asms = get_assumptions_ pt p;

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

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

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

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

   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 = Rewrite ("square_equation_left",     *)

   437 val asms = get_assumptions_ pt p;

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

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

   440 val asms = get_assumptions_ pt p;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   459 (*val nxt =

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

   461 val asms = get_assumptions_ pt p;

   462 if asms = [] then ()

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

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

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

   467 val asms = get_assumptions_ pt p;

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

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

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

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

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

   473 else raise

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

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

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

   478 val asms = get_assumptions_ pt p;

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

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

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

   482     [13])];

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

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

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

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

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

   491 val asms = get_assumptions_ pt p;

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

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

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

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

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

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

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

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

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

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

   506 val scr = Prog (((inst_abs thy) o term_of o the o (parse thy))

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

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

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

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

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

   512     \                  ((Rewrite real_root_positive False) Or            \

   513     \                   (Rewrite real_root_negative False)) @@           \

   514     \                  OrToList) L_0_                                    \

   515     \ in (flat ....))"

   516 );

   518 *)

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55355	e55f16caf498
child 55363	d78bc1342183
permissions	-rw-r--r--