wneuper/isa: test/Tools/isac/OLDTESTS/scriptnew.sml@460c24a6a6ba

     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, []));

    34 store_met

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

    36  (*test for simplification*)

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

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

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

    40    ],

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

    42     crls=tval_rls, nrls=e_rls(*,

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

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

    45  \Repeat\

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

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

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

    49  ));

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

    51 val (dI',pI',mI') = ("Test.thy",["met_testterm","tests"],

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

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

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

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

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

    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 (p,_,f,nxt,_,pt) = me nxt p c pt;

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

    63 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met_testterm"))*)

    64 (*----script 111 ------------------------------------------------*)

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

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

    67 (*----script 222 ------------------------------------------------*)

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

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

    70 (*----script 333 ------------------------------------------------*)

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

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

    73 (*----script 444 ------------------------------------------------*)

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

    75 (*"#0 * a"*)

    76 (*----script 555 ------------------------------------------------*)

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

    78 (*"#0"*)

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

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

    81 (*----script 666 ------------------------------------------------*)

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

    83 (*"#0"*)

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

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

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

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

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

    94 store_pbt

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

    96  (["met_testeq","tests"],

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

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

    99   ],

   100   e_rls, NONE, []));

   102 store_met

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

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

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

   106    ("#Where" ,[]),

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

   108    ],

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

   110     srls=append_rls "testeq1_srls" e_rls

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

   112     prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls

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

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

   115    \(While (contains_root e_e) Do                                     \

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

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

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

   119    \ e_e"

   120  ));

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

   123 	   "boolTestFind v_i_"];

   124 val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],

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

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

   127 atomt sc;

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

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

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

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

   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 (p,_,f,nxt,_,pt) = me nxt p c pt;

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

   138 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   160 store_met

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

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

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

   164    ("#Where" ,[]),

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

   166    ],

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

   168     srls=append_rls "testlet_srls" e_rls

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

   170     prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls

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

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

   173    \(let e_e =\

   174    \  ((While (contains_root e_e) Do                                     \

   175    \   (Rewrite square_equation_left True))\

   176    \   e_e)\

   177    \in [e_::bool])"

   178    ));

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

   180 writeln(term2str sc);

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

   182 	   "boolTestFind v_i_"];

   183 val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],

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

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

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

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

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

   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 (p,_,f,nxt,_,pt) = me nxt p c pt;

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

   195 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)

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

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

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

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

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

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

   206 " _________________ me + nxt_step from script _________________ ";

   207 " _________________ me + nxt_step from script _________________ ";

   208 " _________________ me + nxt_step from script _________________ ";

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

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

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

   212   ("Test.thy",["sqroot-test","univariate","equation","test"],

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

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

   215 writeln(term2str sc);

   217 "--- s1 ---";

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

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

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

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

   222 "--- s2 ---";

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

   224 (* val nxt =

   225   ("Add_Given",

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

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

   228 "--- s3 ---";

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

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

   231 "--- s4 ---";

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

   233 "--- s5 ---";

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

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

   236 "--- s6 ---";

   237 (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)

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

   239 "--- s7 ---";

   240 (* val nxt =

   241   ("Specify_Problem",

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

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

   244 "--- s8 ---";

   245 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

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

   247 "--- s9 ---";

   248 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

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

   250 "--- 1 ---";

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

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

   253 "--- 2 ---";

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

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

   256 "--- 3 ---";

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

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

   259 "--- 4 ---";

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

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

   262 "--- 5 ---";

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

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

   265 "--- 6 ---";

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

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

   268 "--- 7 ---";

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

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

   271 "--- 8<> ---";

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

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

   274 "--- 9<> ---";

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

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

   277 "--- 10<> ---";

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

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

   280 "--- 11<> ---";

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

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

   283 "--- 12<> ---.";

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

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

   286 "--- 13<> ---";

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

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

   289 "--- 14<> ---";

   290 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)

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

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

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

   294 else ();

   295 "--- 15<> ---";

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

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

   299 writeln (pr_ptree pr_short pt);

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

   301 "\n=============================================================");

   302 (*get_obj g_asm pt [];

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

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

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

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

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

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

   314 	   "solutions L"];

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

   316   ("Test.thy",["sqroot-test","univariate","equation","test"],

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

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

   319  (writeln o term2str) sc;

   320 "--- s1 ---";

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

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

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

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

   325 "--- s2 ---";

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

   327 (* val nxt = ("Add_Given",

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

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

   330 "--- s3 ---";

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

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

   333 "--- s4 ---";

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

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

   336 "--- s5 ---";

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

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

   339 "--- s6 ---";

   340 (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)

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

   342 "--- s7 ---";

   343 (* val nxt = ("Specify_Problem",

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

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

   346 "--- s8 ---";

   347 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

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

   349 "--- s9 ---";

   350 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   376 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:

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

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

   379 #################################################*)

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

   382    *)

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

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

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

   388 	   "solutions L"];

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

   390   ("Test.thy",["sqroot-test","univariate","equation","test"],

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

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

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

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

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

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

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

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

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

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

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

   403 (*val nxt = "square_equation_left",

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

   405 get_assumptions_ pt p;

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

   407 trace_rewrite:=true;

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

   409 trace_rewrite:=false;

   410 val asms = get_assumptions_ pt p;

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

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

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

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

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

   419 val asms = get_assumptions_ pt p;

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

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

   422 val asms = get_assumptions_ pt p;

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

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

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

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

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

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

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

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

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

   433 (*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*)

   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 (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

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

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

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

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

   441 (*val nxt =

   442   ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)

   443 val asms = get_assumptions_ pt p;

   444 if asms = [] then ()

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

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

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

   449 val asms = get_assumptions_ pt p;

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

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

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

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

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

   455 else raise

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

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

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

   460 val asms = get_assumptions_ pt p;

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

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

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

   464     [13])];

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

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

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

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

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

   473 val asms = get_assumptions_ pt p;

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

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

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

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

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

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

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

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

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

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

   488 val scr = Script (((inst_abs thy) o term_of o the o (parse thy))

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

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

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

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

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

   494     \                  ((Rewrite real_root_positive False) Or            \

   495     \                   (Rewrite real_root_negative False)) @@           \

   496     \                  OrToList) L_0_                                    \

   497     \ in (flat ....))"

   498 );

   500 *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37984	972a73d7c50b
child 38043	6a36acec95d9
permissions	-rw-r--r--