neuper@37906: (* use"systest/subp-rooteq.sml";
neuper@37906:    use"subp-rooteq.sml";
neuper@37906:    *)
neuper@37906: val c = [];
neuper@37906: 
neuper@37906: "---------------- miniscript with mini-subpbl -------------";
neuper@37906: "---------------- solve_linear as rootpbl -----------------";
neuper@37906: "---------------- solve_plain_square as rootpbl -----------";
neuper@37906: "---------------- root-eq + subpbl: solve_linear ----------";
neuper@37906: "---------------- root-eq + subpbl: solve_plain_square ----";
neuper@37906: "---------------- root-eq + subpbl: no_met: linear --------";
neuper@37906: "---------------- root-eq + subpbl: no_met: square --------";
neuper@37906: "---------------- no_met in rootpbl -> linear -------------";
neuper@37906: "==========================================================";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- miniscript with mini-subpbl -------------";
neuper@37906: "---------------- miniscript with mini-subpbl -------------";
neuper@37906: "---------------- miniscript with mini-subpbl -------------";
neuper@37906: (*###########################################################
neuper@37906:   ##  12.03 next_tac repariert (gab keine Value zurueck   ###
neuper@37906:   ###########################################################*)
neuper@41970: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","squ-equ-test-subpbl1"]);
neuper@37906: 
neuper@48790: val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
neuper@41970: (writeln o term2str) sc;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*("Specify_Method",Specify_Method ("Test","squ-equ-test-subpbl1"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","squ-equ-test-subpbl1"*)
neuper@37906: (*---vvv--- nxt_ here = loc_ below ------------------vvv-------------------*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = "x + 1 = 2"; val nxt = Rewrite_Set "norm_equation"*)
neuper@37906: (*### solve Apply_Method: is =   ### nxt_solv1 Apply_Method: store is
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37926:  [], NONE,
neuper@37906:  ??.empty, Safe, true)           ########## OK*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = "x + 1 + -1 * 2 = 0"; val nxt = Rewrite_Set "Test_simplify"*)
neuper@37906: (*### locate_gen----------: is=  ### next_tac----------------:E =
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37926:  [], NONE,
neuper@37906:  ??.empty, Safe, true)           ########## OK von loc_ uebernommen
neuper@37906: ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37981:  [R,L,R,L,L,R,R], SOME e_e,
neuper@37906:  x + 1 + -1 * 2 = 0, Safe, true) ########## OK*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: 
neuper@38058: (*val f = "-1 + x = 0"; val nxt = Subproblem ("Test",[#,#,#])
neuper@37906:                                 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
neuper@37906: (*### locate_gen-----------: is= ### next_tac-----------------: E=
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37981:  [R,L,R,L,L,R,R], SOME e_e,
neuper@37906:  x + 1 + -1 * 2 = 0, Safe, true) ########## OK von loc_ uebernommen
neuper@37906: ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37981:  [R,L,R,L,R,R], SOME e_e,
neuper@37906:  -1 + x = 0, Safe, false)         ########## OK*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*### locate_gen------------: is= ### next_tac-----------------: E=
neuper@37906: ScrState (["
neuper@37906: (e_, x + 1 = 2)","
neuper@37906: (v_, x)"],
neuper@37981:  [R,L,R,L,R,R], SOME e_e,
neuper@37906:  -1 + x = 0, Safe, false)         ########## OK von loc_ uebernommen
neuper@37906: ### solve, after locate_gen: is=  ### nxt_solv4 Apply_Method: stored is =
neuper@37906: ScrState (["
neuper@37906: (e_, -1 + x = 0)","
neuper@37906: (v_, x)"],
neuper@37981:  [R,R,D,L,R], SOME e_e,
neuper@37906:  Subproblem (Test.thy, [linear, univariate, equation, test]), Safe, true)
neuper@37906:                                   ########## OK*)
neuper@37906:   p;
neuper@48895:   writeln(istate2str (fst (get_istate pt ([3],Frm))));
neuper@55279: (*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
neuper@48790:   val Prog sc = (#scr o get_met) ["Test","solve_linear"];
neuper@37906:   (writeln o term2str) sc;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906:   p;
neuper@48895:   writeln(istate2str (fst (get_istate pt ([3],Res))));
neuper@37906: (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  miniscript with mini-subpbl";
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- solve_linear as rootpbl -----------------";
neuper@37906: "---------------- solve_linear as rootpbl -----------------";
neuper@37906: "---------------- solve_linear as rootpbl -----------------";
neuper@42124: val fmz = ["equality (1+-1*2+x=(0::real))",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@55279:   ("Test",["LINEAR","univariate","equation","test"],
neuper@37906:    ["Test","solve_linear"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
neuper@37906:   val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
neuper@37906:   val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout                   val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout 
neuper@37906:   val nxt = ("End_Proof'",End_Proof') : string * tac*)
neuper@37906: val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  solve_linear as rootpbl";
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- solve_plain_square as rootpbl -----------";
neuper@37906: "---------------- solve_plain_square as rootpbl -----------";
neuper@37906: "---------------- solve_plain_square as rootpbl -----------";
neuper@37906: val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
neuper@37906: 	   "solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["plain_square","univariate","equation","test"],
neuper@37906:    ["Test","solve_plain_square"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val  Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
neuper@37906: if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  solve_plain_square as rootpbl";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- root-eq + subpbl: solve_linear ----------";
neuper@37906: "---------------- root-eq + subpbl: solve_linear ----------";
neuper@37906: "---------------- root-eq + subpbl: solve_linear ----------";
neuper@37906: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","square_equation1"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
neuper@37906: square_equation_left*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"
neuper@37906: Test_simplify*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"
neuper@37906: rearrange_assoc*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"
neuper@37906: isolate_root*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
neuper@37906: Test_simplify*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"-4 + x = 0"
neuper@55279:   val nxt =("Subproblem",Subproblem ("Test",["LINEAR","univariate"...*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*val nxt =("Model_Problem",Model_Problem ["LINEAR","univariate"...*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x = 0 + -1 * -4", nxt Test_simplify*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*"x = 4", nxt Check_Postcond ["LINEAR","univariate","equation","test"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_linear";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- root-eq + subpbl: solve_plain_square ----";
neuper@37906: "---------------- root-eq + subpbl: solve_plain_square ----";
neuper@37906: "---------------- root-eq + subpbl: solve_plain_square ----";
neuper@37906: val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","square_equation2"]);
neuper@48790: val Prog sc = (#scr o get_met) ["Test","square_equation2"];
neuper@37906: (writeln o term2str) sc;
neuper@37906: 
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = 
neuper@37906: 
neuper@37906: me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"9 + -1 * x ^^^ 2 = 0"
neuper@38058:   Subproblem ("Test",["plain_square","univariate","equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*Model_Problem ["plain_square","univariate","equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*Apply_Method ("Test","solve_plain_square")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"x = -3 | x = 3", nxt Or_to_List*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"[x = -3, x = 3]", 
neuper@37906:   nxt Check_Postcond ["plain_square","univariate","equation","test"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
neuper@37906: 
neuper@37906: 
wneuper@59279: writeln (pr_ctree pr_short pt);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@48790: val Prog s = (#scr o get_met) ["Test","square_equation"];
neuper@37906: atomt s;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- root-eq + subpbl: no_met: linear ----";
neuper@37906: "---------------- root-eq + subpbl: no_met: linear ----";
neuper@37906: "---------------- root-eq + subpbl: no_met: linear ----";
neuper@37906: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["squareroot","univariate","equation","test"],
neuper@37906:    ["Test","square_equation"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*"-4 + x = 0", nxt Subproblem ("Test",["univariate","equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*val nxt =("Model_Problem",Model_Problem ["LINEAR","univar...*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@55279: (*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR","univariate","equ*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*Apply_Method ("Test","norm_univar_equation")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: if p = ([13],Res) then ()
neuper@38031: else error ("subp-rooteq.sml: new.behav. in  \
neuper@37906: 		 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- root-eq + subpbl: no_met: square ----";
neuper@37906: "---------------- root-eq + subpbl: no_met: square ----";
neuper@37906: "---------------- root-eq + subpbl: no_met: square ----";
neuper@37906: val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["squareroot","univariate","equation","test"],
neuper@37906:    ["Test","square_equation"]);
neuper@48790:  val Prog sc = (#scr o get_met) ["Test","square_equation"];
neuper@37906:  (writeln o term2str) sc;
neuper@37906: 
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*Subproblem ("Test",["univariate","equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*Model_Problem ["plain_square","univariate","equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
neuper@37906: if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: no_met: square";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- no_met in rootpbl -> linear --------------";
neuper@37906: "---------------- no_met in rootpbl -> linear --------------";
neuper@37906: "---------------- no_met in rootpbl -> linear --------------";
neuper@37906: val fmz = ["equality (1+2*x+3=4*x- 6)",
neuper@37906: 	   "solveFor x","solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["univariate","equation","test"],
neuper@37906:    ["no_met"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: (*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","norm_univar_equation"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@38058: (*val nxt = ("Subproblem",Subproblem ("Test",["univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@55279: (*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@55279: (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equatio*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
neuper@37906: val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = 
neuper@37906:     me nxt p c pt;
neuper@37906: if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
neuper@38031: else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
neuper@37906: 
neuper@37906: 
neuper@37906: refine fmz ["univariate","equation","test"];
neuper@37906: match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);
neuper@37906: