neuper@37871: (* use"../systest/scriptnew.sml";
neuper@37871:    use"systest/scriptnew.sml";
neuper@37871:    use"scriptnew.sml";
neuper@37871:    *)
neuper@37871: 
neuper@37871: (*contents*)
neuper@37871: " --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
neuper@37871: " --- test  9.5.02 Testeq: While Try Repeat @@ ------------------ ";
neuper@37871: " --- test 11.5.02 Testeq: let e_ =... in [e_] ------------------ ";
neuper@37871: " _________________ me + nxt_step from script ___________________ ";
neuper@37871: " _________________ me + sqrt-equ-test: 1.norm_equation  ________ ";
neuper@37871: " _________________ equation with x =(-12)/5, but L ={} ------- ";
neuper@37871: "------------------ script with Map, Subst (biquadr.equ.)---------";
neuper@37871: (*contents*)
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
neuper@37871: "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
neuper@37871: "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
neuper@37871: store_pbt
neuper@37871:  (prep_pbt Test.thy "pbl_testss" [] e_pblID
neuper@37871:  (["tests"],
neuper@37871:   []:(string * string list) list,
neuper@37871:   e_rls, None, []));
neuper@37871: store_pbt
neuper@37871:  (prep_pbt Test.thy "pbl_testss_term" [] e_pblID
neuper@37871:  (["met_testterm","tests"],
neuper@37871:   [("#Given" ,["realTestGiven g_"]),
neuper@37871:    ("#Find"  ,["realTestFind f_"])
neuper@37871:   ],
neuper@37871:   e_rls, None, []));
neuper@37871: store_met
neuper@37871:  (prep_met Test.thy "met_test_simp" [] e_metID
neuper@37871:  (*test for simplification*)
neuper@37871:  (["Test","met_testterm"]:metID,
neuper@37871:   [("#Given" ,["realTestGiven g_"]),
neuper@37871:    ("#Find"  ,["realTestFind f_"])
neuper@37871:    ],
neuper@37871:    {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
neuper@37871:     crls=tval_rls, nrls=e_rls(*,
neuper@37871:     asm_rls=[],asm_thm=[]*)},
neuper@37871:  "Script Testterm (g_::real) =   \
neuper@37871:  \Repeat\
neuper@37871:  \  ((Repeat (Rewrite rmult_1 False)) Or\
neuper@37871:  \   (Repeat (Rewrite rmult_0 False)) Or\
neuper@37871:  \   (Repeat (Rewrite radd_0 False))) g_"
neuper@37871:  ));
neuper@37871: val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
neuper@37871: val (dI',pI',mI') = ("Test.thy",["met_testterm","tests"],
neuper@37871: 		     ["Test","met_testterm"]);
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met_testterm"))*)
neuper@37871: (*----script 111 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"(#0 + #0) * (#1 * (#1 * a))"  nxt= Rewrite ("rmult_1",*)
neuper@37871: (*----script 222 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"(#0 + #0) * (#1 * a)"         nxt= Rewrite ("rmult_1",*)
neuper@37871: (*----script 333 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"(#0 + #0) * a"                nxt= Rewrite ("radd_0",*)
neuper@37871: (*----script 444 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"#0 * a"*)
neuper@37871: (*----script 555 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"#0"*)
neuper@37871: if p=([4],Res) then ()
neuper@37871: else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
neuper@37871: (*----script 666 ------------------------------------------------*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*"#0"*)
neuper@37871: if nxt=("End_Proof'",End_Proof') then ()
neuper@37871: else raise error "new behaviour in 30.4.02 Testterm: End_Proof";
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
neuper@37871: "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
neuper@37871: "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
neuper@37871: store_pbt
neuper@37871:  (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
neuper@37871:  (["met_testeq","tests"],
neuper@37871:   [("#Given" ,["boolTestGiven e_"]),
neuper@37871:    ("#Find"  ,["boolTestFind v_i_"])
neuper@37871:   ],
neuper@37871:   e_rls, None, []));
neuper@37871: 
neuper@37871: store_met
neuper@37871:  (prep_met Test.thy "met_test_eq1" [] e_metID
neuper@37871:  (["Test","testeq1"]:metID,
neuper@37871:    [("#Given",["boolTestGiven e_"]),
neuper@37871:    ("#Where" ,[]), 
neuper@37871:    ("#Find"  ,["boolTestFind v_i_"]) 
neuper@37871:    ],
neuper@37871:    {rew_ord'="tless_true",rls'=tval_rls,
neuper@37871:     srls=append_rls "testeq1_srls" e_rls 
neuper@37871: 		    [Calc ("Test.contains'_root", eval_contains_root"")],
neuper@37871:     prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
neuper@37871: 		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
neuper@37871:  "Script Testeq (e_::bool) =                                        \
neuper@37871:    \(While (contains_root e_) Do                                     \
neuper@37871:    \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \
neuper@37871:    \  (Try (Repeat (Rewrite square_equation_left True))) @@ \
neuper@37871:    \  (Try (Repeat (Rewrite radd_0 False)))))\
neuper@37871:    \ e_"
neuper@37871:  ));
neuper@37871: 
neuper@37871: val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",
neuper@37871: 	   "boolTestFind v_i_"];
neuper@37871: val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
neuper@37871: 		     ["Test","testeq1"]);
neuper@37871: val Script sc = (#scr o get_met) ["Test","testeq1"];
neuper@37871: atomt sc;
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))
neuper@37871: val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*** No such constant: "Test.contains'_root"  *)
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso
neuper@37871:    nxt=("End_Proof'",End_Proof') then ()
neuper@37871: else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
neuper@37871: " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
neuper@37871: " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
neuper@37871: store_met
neuper@37871:  (prep_met Test.thy "met_test_let" [] e_metID
neuper@37871:  (["Test","testlet"]:metID,
neuper@37871:    [("#Given",["boolTestGiven e_"]),
neuper@37871:    ("#Where" ,[]), 
neuper@37871:    ("#Find"  ,["boolTestFind v_i_"]) 
neuper@37871:    ],
neuper@37871:    {rew_ord'="tless_true",rls'=tval_rls,
neuper@37871:     srls=append_rls "testlet_srls" e_rls 
neuper@37871: 		    [Calc ("Test.contains'_root",eval_contains_root"")],
neuper@37871:     prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
neuper@37871: 		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
neuper@37871:    "Script Testeq2 (e_::bool) =                                        \
neuper@37871:    \(let e_ =\
neuper@37871:    \  ((While (contains_root e_) Do                                     \
neuper@37871:    \   (Rewrite square_equation_left True))\
neuper@37871:    \   e_)\
neuper@37871:    \in [e_::bool])"
neuper@37871:    ));
neuper@37871: val Script sc = (#scr o get_met) ["Test","testlet"];
neuper@37871: writeln(term2str sc);
neuper@37871: val fmz = ["boolTestGiven (sqrt a = 0)",
neuper@37871: 	   "boolTestFind v_i_"];
neuper@37871: val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
neuper@37871: 		     ["Test","testlet"]);
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
neuper@37871: if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso
neuper@37871:    nxt=("End_Proof'",End_Proof') then ()
neuper@37871: else raise error "different behaviour in test 11.5.02 Testeq: let e_ =... in [e_]";
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: " _________________ me + nxt_step from script _________________ ";
neuper@37871: " _________________ me + nxt_step from script _________________ ";
neuper@37871: " _________________ me + nxt_step from script _________________ ";
neuper@37871: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37871: 	   "solveFor x","solutions L"];
neuper@37871: val (dI',pI',mI') =
neuper@37871:   ("Test.thy",["sqroot-test","univariate","equation","test"],
neuper@37871:    ["Test","sqrt-equ-test"]);
neuper@37871: val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
neuper@37871: writeln(term2str sc);
neuper@37871: 
neuper@37871: "--- s1 ---";
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: "--- s2 ---";
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: (* val nxt =
neuper@37871:   ("Add_Given",
neuper@37871:    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s3 ---";
neuper@37871: (* val nxt = ("Add_Given",Add_Given "solveFor x");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s4 ---";
neuper@37871: (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
neuper@37871: "--- s5 ---";
neuper@37871: (* val nxt = ("Add_Find",Add_Find "solutions L");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s6 ---";
neuper@37871: (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s7 ---";
neuper@37871: (* val nxt =
neuper@37871:   ("Specify_Problem",
neuper@37871:    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s8 ---";
neuper@37871: (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s9 ---";
neuper@37871: (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 1 ---";
neuper@37871: (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 2 ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 3 ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 4 ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 5 ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 6 ---";
neuper@37871: (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 7 ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 8<> ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 9<> ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 10<> ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 11<> ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 12<> ---.";
neuper@37871: (* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 13<> ---";
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- 14<> ---";
neuper@37871: (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
neuper@37871: then raise error "scriptnew.sml 1: me + tacs from script: new behaviour" 
neuper@37871: else ();
neuper@37871: "--- 15<> ---";
neuper@37871: (* val nxt = ("End_Proof'",End_Proof');*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: 
neuper@37871: writeln (pr_ptree pr_short pt);
neuper@37871: writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
neuper@37871: "\n=============================================================");
neuper@37871: (*get_obj g_asm pt [];
neuper@37871: val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: 
neuper@37871: " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";
neuper@37871: " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";
neuper@37871: " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";
neuper@37871: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37871: 	   "solveFor x","errorBound (eps=0)",
neuper@37871: 	   "solutions L"];
neuper@37871: val (dI',pI',mI') =
neuper@37871:   ("Test.thy",["sqroot-test","univariate","equation","test"],
neuper@37871:    ["Test","sqrt-equ-test"]);
neuper@37871:  val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
neuper@37871:  (writeln o term2str) sc;
neuper@37871: "--- s1 ---";
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: "--- s2 ---";
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: (* val nxt = ("Add_Given",
neuper@37871:    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s3 ---";
neuper@37871: (* val nxt = ("Add_Given",Add_Given "solveFor x");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s4 ---";
neuper@37871: (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
neuper@37871: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
neuper@37871: "--- s5 ---";
neuper@37871: (* val nxt = ("Add_Find",Add_Find "solutions L");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s6 ---";
neuper@37871: (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s7 ---";
neuper@37871: (* val nxt = ("Specify_Problem",
neuper@37871:    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s8 ---";
neuper@37871: (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- s9 ---";
neuper@37871: (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)
neuper@37871: "--- !!! x1 --- 1.norm_equation";
neuper@37871: (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- !!! x2 --- 1.norm_equation";
neuper@37871: (*meNEW: "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2" -- NICHT norm_equation!!*)
neuper@37871: (*meOLD: "sqrt (9 + 4 * x) + -1 * (sqrt x + sqrt (5 + x)) = 0"*)
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: (*"-1 * sqrt x + (-1 * sqrt (5 + x) + sqrt (9 + 4 * x)) = 0"*)
neuper@37871: (*(me nxt p [1] pt) handle e => print_exn_G e;*)
neuper@37871: "--- !!! x3 --- 1.norm_equation";
neuper@37871: (*val nxt = ("Empty_Tac",Empty_Tac) ### helpless*)
neuper@37871: (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- !!! x4 --- 1.norm_equation";
neuper@37871: (*"-1 * sqrt x + -1 * sqrt (5 + x) + sqrt (9 + 4 * x) = 0"*)
neuper@37871: (*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: "--- !!! x5 --- 1.norm_equation";
neuper@37871: (*"sqrt (9 + 4 * x) = 0 + -1 * (-1 * sqrt x + -1 * sqrt (5 + x))"*)
neuper@37871: (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: 
neuper@37871: (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:
neuper@37871: if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))
neuper@37871: then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test";
neuper@37871: #################################################*)
neuper@37871: 
neuper@37871: (* use"../tests/scriptnew.sml";
neuper@37871:    *)
neuper@37871: 
neuper@37871: " _________________ equation with x =(-12)/5, but L ={} ------- ";
neuper@37871: 
neuper@37871: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
neuper@37871: 	   "solveFor x","errorBound (eps=0)",
neuper@37871: 	   "solutions L"];
neuper@37871: val (dI',pI',mI') =
neuper@37871:   ("Test.thy",["sqroot-test","univariate","equation","test"],
neuper@37871:    ["Test","square_equation"]);
neuper@37871: 
neuper@37871: (*val p = e_pos'; val c = []; 
neuper@37871: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37871: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37871: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Apply_Method",Apply_Method ["Test","square_equation"])*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = "square_equation_left",
neuper@37871:       "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)
neuper@37871: get_assumptions_ pt p;
neuper@37871: (*it = [] : string list;*)
neuper@37871: trace_rewrite:=true;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: trace_rewrite:=false;
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: if asms = [(str2term "0 <= 9 + 4 * x",[1]),
neuper@37871: 	   (str2term "0 <= x",[1]),
neuper@37871: 	   (str2term "0 <= -3 + x",[1])] then ()
neuper@37871: else raise error "scriptnew.sml diff.behav. in sqrt assumptions 1";
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = Rewrite ("square_equation_left",     *)
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: if asms = [(str2term "0 <= 9 + 4 * x",[1]),
neuper@37871: 	   (str2term "0 <= x",[1]),
neuper@37871: 	   (str2term "0 <= -3 + x",[1]),
neuper@37871: 	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),
neuper@37871: 	   (str2term "0 <= 6 + x",[6])] then ()
neuper@37871: else raise error "scriptnew.sml diff.behav. in sqrt assumptions 2";
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Apply_Method",Apply_Method ["Test","solve_linear"])*)
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt =
neuper@37871:   ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: if asms = [] then ()
neuper@37871: else raise error "scriptnew.sml diff.behav. in sqrt assumptions 3";
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
neuper@37871: 
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: if asms = [(str2term "0 <= 9 + 4 * x",[1]),
neuper@37871: 	   (str2term "0 <= x",[1]),
neuper@37871: 	   (str2term "0 <= -3 + x",[1]),
neuper@37871: 	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),
neuper@37871: 	   (str2term "0 <= 6 + x",[6])] then ()
neuper@37871: else raise 
neuper@37871:     error "scriptnew.sml: diff.behav. at Check_elementwise [x = -12 / 5]";
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: (*val nxt = Check_Postcond ["sqroot-test","univariate","equation","test"])*)
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),
neuper@37871:    ("0 <= x ^^^ 2 + -3 * x",[6]),("0 <= 6 + x",[6]),
neuper@37871:    ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",
neuper@37871:     [13])];
neuper@37871: 
neuper@37871: 
neuper@37871: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37871: val Form' (FormKF (_,_,_,_,ff)) = f;
neuper@37871: if ff="[x = -12 / 5]"
neuper@37871: then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")
neuper@37871: else raise error "diff.behav. in scriptnew.sml; root-eq: L = []";
neuper@37871: 
neuper@37871: val asms = get_assumptions_ pt p;
neuper@37871: if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),
neuper@37871: 	   (str2term "0 <= -12 / 5", []),
neuper@37871: 	   (str2term "0 <= -3 + -12 / 5", []),
neuper@37871: 	   (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []),
neuper@37871: 	   (str2term "0 <= 6 + -12 / 5", [])] then ()
neuper@37871: else raise error "scriptnew.sml diff.behav. in sqrt assumptions 4";
neuper@37871: 
neuper@37871: 
neuper@37871: "------------------ script with Map, Subst (biquadr.equ.)---------";
neuper@37871: "------------------ script with Map, Subst (biquadr.equ.)---------";
neuper@37871: "------------------ script with Map, Subst (biquadr.equ.)---------";
neuper@37871: 
neuper@37871: 
neuper@37871: (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
neuper@37871: val scr = Script (((inst_abs thy) o term_of o the o (parse thy))
neuper@37871:     "Script Biquadrat_poly (e_::bool) (v_::real) =                       \
neuper@37871:     \(let e_ = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_;        \ 
neuper@37871:     \     L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met])   \
neuper@37871:     \             [bool_ e_, real_ v_0_]);                               \ 
neuper@37871:     \     L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@                  \
neuper@37871:     \                  ((Rewrite real_root_positive False) Or            \
neuper@37871:     \                   (Rewrite real_root_negative False)) @@           \
neuper@37871:     \                  OrToList) L_0_                                    \ 
neuper@37871:     \ in (flat ....))"
neuper@37871: );
neuper@37871: 
neuper@37871: *)
neuper@37871: