(* tests on systems of equations over the reals

   author: Walther Neuper 050905

   (c) due to copyright terms

use"../smltest/IsacKnowledge/system.sml";

*)

val thy = EqSystem.thy;

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- normalize system ------------------------------------";

"----------- me --------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"----------- normalize system ------------------------------------";

"----------- normalize system ------------------------------------";

"----------- normalize system ------------------------------------";

val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\

		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";

val SOME (t,_) = rewrite_set_ thy false norm_Poly t;

if term2str t = 

"[0 = -1 * q_0 * (0 / 2) + c_2, 0 = L * c + -1 * q_0 * (L ^^^ 2 / 2) + c_2]"

then () else error "system.sml, diff.behav. in norm_Poly";

val t = str2term "[0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\

		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";

val SOME (t,_) = rewrite_set_ thy false norm_Rational t;

if term2str t = 

"[0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"

then () else error "system.sml, diff.behav. in norm_Rational";

val t = str2term "nth_ 1 [0 = c*0 + -1*q_0*(0^^^2 / 2) + c_2,\

		 \ 0 = c*L + -1*q_0*(L^^^2 / 2) + c_2]";

val SOME (t,_) = rewrite_set_ thy false list_rls t;

if term2str t = "0 = c * 0 + -1 * q_0 * (0 ^^^ 2 / 2) + c_2"

then () else error "system.sml, list_rls";

"----------- me --------------------------------------------------";

"----------- me --------------------------------------------------";

"----------- me --------------------------------------------------";

val fmz = ["equalities [0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2, 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2]",

	   "solveForVars [c, c_2]", "solution ss___"];

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

  ("Biegelinie",["normalize","2x2","linear","system"],

   ["EqSystem","normalize","2x2"]);

val p = e_pos'; val c = [];

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

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

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

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

case nxt of (_, Specify_Theory "Biegelinie") => ()

	  | _ => error "system.sml diff.behav.in me --1";

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

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

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

case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()

	  | _ => error "system.sml diff.behav.in me --2";

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

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

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

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

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

case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2", 

					       "linear", "system"])) => ()

	  | _ => error "system.sml diff.behav.in me --3";

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

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

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

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

case nxt of (_, Specify_Theory "Biegelinie") => ()

	  | _ => error "system.sml diff.behav.in me --1";

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

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

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

case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()

	  | _ => error "system.sml diff.behav.in me --2";

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

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

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

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

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

(*---

WN060421 stopped as soon as exp_IsacCore_Equ_Sys_Lin_No-1.xml worked ...

if f2str f = "" then ()

else error  "system.sml diff.behav.in me --99";

case nxt of ("End_Proof'", End_Proof') => ()

	  | _ => error  "system.sml diff.behav.in me --99";

print_depth 11;nxt;print_depth 3;

---*)

(*

use"../smltest/IsacKnowledge/system.sml";

*)