neuper@37906: (* RL 10.02
neuper@37906:  use"../kbtest/rooteq.sml";
neuper@37906:  use"rooteq.sml";
neuper@37906:  testexamples for RootEq, equations with fractions
neuper@37906: 
neuper@37906:  Compiler.Control.Print.printDepth:=10; (*4 default*)
neuper@37906:  Compiler.Control.Print.printDepth:=5; (*4 default*)
neuper@37906: *)
neuper@37906: "----------- rooteq.sml begin--------";
neuper@37906: "--------------(1/sqrt(x)=5)---------------------------------------";
neuper@37906: "--------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))----------------------";
neuper@37906: "--------------(sqrt(x+1)=5)---------------------------------------";
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
neuper@37906: "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
wneuper@59430: "---------------- root-eq + subpbl: solve_linear ----------";
wneuper@59430: "---------------- root-eq + subpbl: solve_plain_square ----";
wneuper@59430: "---------------- root-eq + subpbl: no_met: linear --------";
wneuper@59430: "---------------- root-eq + subpbl: no_met: square --------";
wneuper@59430: "---------------- no_met in rootpbl -> linear -------------";
neuper@41943: "--------------------------------------------------------";
neuper@41943: 
neuper@41943: (*=== inhibit exn ?=============================================================
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>False\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>False\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>False\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60230: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60242: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 - (sqrt(2+x+3) \<up> 3)) is_normSqrtTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>False\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
walther@60242: val t = (Thm.term_of o the o (TermC.parse RootEq.thy)) "(1 + (sqrt(2+x+3) \<up> 3)) is_normSqrtTerm_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
walther@59868: val result = UnparseC.term t_;
wenzelm@60309: if result <>  \<^const_name>\<open>True\<close>  then error "rooteq.sml: new behaviour:" else ();
neuper@37906: 
neuper@37906: 
neuper@37906: 
walther@59997: val result = M_Match.match_pbl ["equality (sqrt(x)=1)", "solveFor x", "solutions L"] 
walther@59997:                 (Problem.from_store ["rootX", "univariate", "equation"]); 
walther@59984: case result of M_Match.Matches' _  => ()  | _ => error "rooteq.sml: new behaviour:";
neuper@37906: 
walther@59997: val result = M_Match.match_pbl ["equality (sqrt(25)=1)", "solveFor x", "solutions L"] 
walther@59997:                 (Problem.from_store ["rootX", "univariate", "equation"]); 
walther@59984: case result of M_Match.NoMatch' _  => ()  | _ => error "rooteq.sml: new behaviour:";
neuper@37906: 
neuper@37906: (*---------rooteq---- 23.8.02 ---------------------*)
neuper@37906: "---------(1/sqrt(x)=5)---------------------";
walther@59997: val fmz = ["equality (1/sqrt(x)=5)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37991: (*"1 / x = 25" -> Subproblem ("RootEq", ["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: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37991: (*"1 = 25 * x" -> Subproblem ("RatEq", ["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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "1 + - 25 * x = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
neuper@37991: (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
neuper@38031: 	 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
walther@59868: if UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
walther@59851: (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..:
Walther@60565:      [(TermC.parse_test @{context}"25 ~= 0",[])] *)
neuper@37906: then writeln "should be True\n\
neuper@37906: 	     \should be True\n\
neuper@37906: 	     \should be True\n"
neuper@38031: else error "rooteq.sml: diff.behav. with 25 ~= 0";
neuper@37906: 
neuper@37906: "---------(sqrt(x+1)=5)---------------------";
walther@59997: val fmz = ["equality (sqrt(x+1)=5)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
neuper@37906: (*val p = e_pos'; 
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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37991: (*-> Subproblem ("RootEq", ["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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 24 + x = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
neuper@37991: (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
neuper@38031: 	 | _ => error "rooteq.sml: diff.behav. [x = 24]";
neuper@37906: 
neuper@37906: "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
walther@59997: val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 184 + 46 * x = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
neuper@38031: 	 | _ => error "rooteq.sml: diff.behav. [x = 4]";
Walther@60565: if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= 12 * sqrt 2 * 4"] 
neuper@37906: then writeln "should be True\nshould be True\nshould be True\n\
neuper@37906: 	     \should be True\nshould be True\nshould be True\n"
neuper@38031: else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
neuper@37906: 
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
walther@59997: val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59997: (*val nxt = Model_Problem ["sq", "rootX", "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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60329: (*"13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60242: (*"144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
neuper@37991: (*-> Subproblem ("PolyEq", ["degree_0", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59844: val asm = Ctree.get_assumptions pt p;
walther@59959: if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
neuper@38031: then () else error "rooteq.sml: diff.behav. in UniversalList 1";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
neuper@37906: val fmz = 
walther@60329:     ["equality (13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
walther@59997:      "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
walther@59997: 		     ["RootEq", "solve_sq_root_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60242: (*"144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"])) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([6,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
walther@59997: val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
walther@59959: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = Specify_Method ["PolyEq", "solve_d0_polyeq_equation"])       *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wenzelm@60309: (*val p = ([6,3,1],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,\<^const_name>\<open>True\<close>))
neuper@37906: val nxt = ("Or_to_List",Or_to_List) : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val p = ([6,3,2],Res)  val f = (~1,EdUndef,3,Nundef,"UniversalList"))
walther@59997: val nxt = Check_Postcond ["degree_0", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList"))
walther@59997: val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
walther@59959: (* val Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, str)) = f;
neuper@37906:    *)
neuper@37906: 
neuper@37906: (*same error as full expl #######*)
neuper@37906: 
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
walther@59997: val fmz = ["equality (sqrt(x) = 1)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
walther@59997: 		     ["RootEq", "solve_sq_root_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq", "solve_sq_root_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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (* val p = ([2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = 1"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Specify_Method",Specify_Method ["PolyEq", "normalise_poly"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60329: (*val p = ([3,2],Res)val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"- 1 + x = 0"))
walther@59997: val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
walther@60329: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 1 + x = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = Specify_Method ["PolyEq", "solve_d1_polyeq_equation"])       *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([3,3,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"x = 1"))
neuper@37906: val nxt = ("Or_to_List",Or_to_List) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([3,3,3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
neuper@37906: val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([3,3,4],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
walther@59997: val nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([3,3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"[x = 1]"))
walther@59997: val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: 
walther@59959: (*val p = ([3],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
neuper@37906: val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
neuper@37906:                                --------------------------------*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([4],Res)  val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
walther@59997: val nxt = Check_Postcond ["sq", "rootX", "univariate", "equation"]) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: if p = ([],Res) andalso f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
neuper@38031: then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
neuper@37906: \                                                            with same error";
walther@59997: val fmz = ["equality (sqrt x = sqrt x)", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
walther@59997: 		     ["RootEq", "solve_sq_root_equation"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq", "solve_sq_root_equation"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([1],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = x"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([2,2],Res) val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
walther@59997: val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
walther@59959: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val p = ([2,3],Pbl)nxt=Specify_Method ["PolyEq", "solve_d0_polyeq_equation"]*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([2,3,2],Res) val f = (Test_Out.FormKF (~1,EdUndef,3,Nundef,"UniversalList"))
walther@59997: val nxt = Check_Postcond ["degree_0", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([2,3],Res) val f = (Test_Out.FormKF (~1,EdUndef,2,Nundef,"UniversalList"))
walther@59997: val nxt =  Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([2],Res)  val f = (Test_Out.FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
neuper@37906: val nxt = Check_elementwise "Assumptions"*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: (*val p = ([3],Res) val f = (Test_Out.FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
walther@59997: val nxt = Check_Postcond ["sq", "rootX", "univariate", "equation"])       *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: if p = ([],Res) andalso f = Form'(Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
neuper@38031: then () else error "new behav. in rooteq.sml: sqrt x = sqrt x";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
walther@59997: val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))", "solveFor x", "solutions L"];
walther@59997: val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*        "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = Model_Problem ["sq", "rootX", "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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60242: (*"2916 + x \<up> 2 + 1296 * x + 143 * x \<up> 2 = 3564 + 1620 * x + 144 * x \<up> 2"))
walther@59997: val nxt = ("Subproblem",Subproblem ("RootEq",["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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59959: if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
neuper@38031: else error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
neuper@37991: (*-> Subproblem ("PolyEq", ["degree_1", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;                                  
walther@60329: case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2]")) => ()
walther@60329: 	 | _ => error "rooteq.sml: diff.behav. [x = - 2]";
neuper@37906: 
neuper@37906: "----------- rooteq.sml end--------";
neuper@37906: 
neuper@37906: 
neuper@41943: ===== inhibit exn ?===========================================================*)
wneuper@59430: 
wneuper@59585: (*===== copied here from OLDTESTS in case there is a Program ===vvv=============================
wneuper@59430: val c = [];
wneuper@59430: 
wneuper@59430: "---------------- root-eq + subpbl: solve_linear ----------";
wneuper@59430: "---------------- root-eq + subpbl: solve_linear ----------";
wneuper@59430: "---------------- root-eq + subpbl: solve_linear ----------";
wneuper@59430: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
walther@59997: 	   "solveFor x", "solutions L"];
wneuper@59430: val (dI',pI',mI') =
walther@59997:   ("Test",["sqroot-test", "univariate", "equation", "test"],
walther@59997:    ["Test", "square_equation1"]);
wneuper@59430: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
wneuper@59430: square_equation_left*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60242: (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2"
wneuper@59430: Test_simplify*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60242: (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))"
wneuper@59430: rearrange_assoc*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60242: (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"
wneuper@59430: isolate_root*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
wneuper@59430: Test_simplify*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"x \<up> 2 + 5 * x + - 1 * (4 + (x \<up> 2 + 4 * x)) = 0"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*"-4 + x = 0"
walther@59997:   val nxt =("Subproblem",Subproblem ("Test",["LINEAR", "univariate"...*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univariate"...*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: 
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equation"])*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"x = 0 + - 1 * -4", nxt Test_simplify*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*"x = 4", nxt Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*"[]", nxt Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
wneuper@59430: if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
wneuper@59430: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_linear";
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: "---------------- root-eq + subpbl: solve_plain_square ----";
wneuper@59430: "---------------- root-eq + subpbl: solve_plain_square ----";
wneuper@59430: "---------------- root-eq + subpbl: solve_plain_square ----";
wneuper@59430: val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
walther@59997: 	   "solveFor x", "solutions L"];
wneuper@59430: val (dI',pI',mI') =
walther@59997:   ("Test",["sqroot-test", "univariate", "equation", "test"],
walther@59997:    ["Test", "square_equation2"]);
Walther@60559: val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation2"];
walther@59868: (writeln o UnparseC.term) sc;
wneuper@59430: 
wneuper@59430: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt = ("Apply_Method",Apply_Method ("Test", "square_equation1"))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = 
wneuper@59430: 
wneuper@59430: me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"9 + - 1 * x \<up> 2 = 0"
walther@59997:   Subproblem ("Test",["plain_square", "univariate", "equation"]))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*Model_Problem ["plain_square", "univariate", "equation"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*Apply_Method ("Test", "solve_plain_square")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"9 + - 1 * x \<up> 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"x \<up> 2 = (0 + - 1 * 9) / - 1", nxt Rewrite_Set "Test_simplify"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60242: (*"x \<up> 2 = 9", nxt Rewrite ("square_equality"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60329: (*"x = sqrt 9 | x = - 1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*"x = -3 | x = 3", nxt Or_to_List*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*"[x = -3, x = 3]", 
walther@59997:   nxt Check_Postcond ["plain_square", "univariate", "equation", "test"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*"[]", nxt Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
wneuper@59430: if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
wneuper@59430: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
wneuper@59430: 
wneuper@59430: 
wneuper@59430: writeln (pr_ctree pr_short pt);
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
Walther@60559: val Prog s = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
wneuper@59430: atomt s;
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: "---------------- root-eq + subpbl: no_met: linear ----";
wneuper@59430: "---------------- root-eq + subpbl: no_met: linear ----";
wneuper@59430: "---------------- root-eq + subpbl: no_met: linear ----";
wneuper@59430: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
walther@59997: 	   "solveFor x", "solutions L"];
wneuper@59430: val (dI',pI',mI') =
walther@59997:   ("Test",["squareroot", "univariate", "equation", "test"],
walther@59997:    ["Test", "square_equation"]);
wneuper@59430: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*"-4 + x = 0", nxt Subproblem ("Test",["univariate", "equation"]))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univar...*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equ*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*Apply_Method ("Test", "norm_univar_equation")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: if p = ([13],Res) then ()
wneuper@59430: else error ("subp-rooteq.sml: new.behav. in  \
wneuper@59430: 		 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
wneuper@59430: if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
wneuper@59430: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: "---------------- root-eq + subpbl: no_met: square ----";
wneuper@59430: "---------------- root-eq + subpbl: no_met: square ----";
wneuper@59430: "---------------- root-eq + subpbl: no_met: square ----";
wneuper@59430: val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
walther@59997: 	   "solveFor x", "solutions L"];
wneuper@59430: val (dI',pI',mI') =
walther@59997:   ("Test",["squareroot", "univariate", "equation", "test"],
walther@59997:    ["Test", "square_equation"]);
Walther@60559:  val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
walther@59868:  (writeln o UnparseC.term) sc;
wneuper@59430: 
wneuper@59430: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt = ("Apply_Method",Apply_Method ("Test", "square_equation1"))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*Subproblem ("Test",["univariate", "equation"]))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*Model_Problem ["plain_square", "univariate", "equation"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot", "univariate", "equ*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59959: val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
wneuper@59430: if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
wneuper@59430: else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: no_met: square";
wneuper@59430: 
wneuper@59430: 
wneuper@59430: 
wneuper@59430: "---------------- no_met in rootpbl -> linear --------------";
wneuper@59430: "---------------- no_met in rootpbl -> linear --------------";
wneuper@59430: "---------------- no_met in rootpbl -> linear --------------";
wneuper@59430: val fmz = ["equality (1+2*x+3=4*x- 6)",
walther@59997: 	   "solveFor x", "solutions L"];
wneuper@59430: val (dI',pI',mI') =
walther@59997:   ("Test",["univariate", "equation", "test"],
wneuper@59430:    ["no_met"]);
wneuper@59430: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59997: (*val nxt = ("Model_Problem",Model_Problem ["normalise", "univariate", "equati*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Apply_Method",Apply_Method ("Test", "norm_univar_equation"*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Subproblem",Subproblem ("Test",["univariate", "equation"])*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Model_Problem",Model_Problem ["LINEAR", "univariate", "equation"]*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "equatio*)
wneuper@59430: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*val nxt = ("Check_Postcond",Check_Postcond ["normalise", "univariate", "equa*)
walther@59959: val (p,_,Form' (Test_Out.FormKF (_,_,_,_,f)),nxt,_,_) = 
wneuper@59430:     me nxt p c pt;
wneuper@59430: if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
wneuper@59430: else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
wneuper@59430: 
wneuper@59430: 
walther@59997: Refine.refine fmz ["univariate", "equation", "test"];
walther@59997: M_Match.match_pbl fmz (Problem.from_store ["polynomial", "univariate", "equation", "test"]);
wneuper@59430: 
walther@60242: ===== copied here from OLDTESTS in case there is a Program === \<up> =============================*)