(* tests on rewrite orders

    author Matthias Goldgruber 2003

    WN0509 do not use this file anymore, since orders require thy:

    do tests in the smltest/IsacKnowledge/file.sml 

    where file.ML defines the respective order !

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

*)

  (*MK die ersten Tests*)

  val substa = [(e_term, (term_of o the o (parse thy)) "a")];

  val substb = [(e_term, (term_of o the o (parse thy)) "b")];

  val substx = [(e_term, (term_of o the o (parse thy)) "x")];

  val x1 = (term_of o the o (parse thy)) "a + b + x";

  val x2 = (term_of o the o (parse thy)) "a + x + b";

  val x3 = (term_of o the o (parse thy)) "a + x + b";

  val x4 = (term_of o the o (parse thy)) "x + a + b";

if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #1";

if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #2";

if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #3";

  val aa = (term_of o the o (parse thy)) "-1 * a * x";

  val bb = (term_of o the o (parse thy)) "x^^^3";

  ord_make_polynomial_in true thy substx (aa, bb);

  true; (* => LESS *) 

  val aa = (term_of o the o (parse thy)) "-1 * a * x";

  val bb = (term_of o the o (parse thy)) "x^^^3";

  ord_make_polynomial_in true thy substa (aa, bb);

  false; (* => GREATER *)

  (*und nach dem Re-engineering der Termorders in den 'rulesets' 

    kannst Du die 'gr"osste' Variable frei w"ahlen: *)

  val bdv= (term_of o the o (parse thy)) "bdv";

  val x  = (term_of o the o (parse thy)) "x";

  val a  = (term_of o the o (parse thy)) "a";

  val b  = (term_of o the o (parse thy)) "b";

  val SOME (t',_) = 

      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;

if term2str t' = "b + x + a" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #11";

  val NONE = 

      rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;

  term2str t';

  "a + x + b";

  val SOME (t',_) = 

      rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;

if term2str t' = "a + b + x" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #13";

  val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";

  val ppp  = (term_of o the o (parse thy)) ppp';

  val SOME (t',_) = 

      rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;

(*MG 2003...

  term2str t';

  "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)

if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #14";

  val SOME (t',_) = 

      rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';

(*MG 2003...

  "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)

if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #15";

  val ttt' = "(3*x + 5)/18";

  val ttt = (term_of o the o (parse thy)) ttt';

  val SOME (uuu,_) = 

      rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;

if term2str uuu = "(5 + 3 * x) / 18" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #16";

  val SOME (uuu,_) = 

      rewrite_set_ thy false make_polynomial ttt;

if term2str uuu = "(5 + 3 * x) / 18" then ()

else error "termorder.sml diff.behav ord_make_polynomial_in #16";

(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML

  (*Aufgabe zum Einstieg in die Arbeit...*)

  val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";

  (*ein 'ruleset' aus Poly.ML wird angewandt...*)

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

  term2str t;

  "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";

  val SOME (t,_) = 

      rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;

  term2str t;

  "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";

(* bei Verwendung von "size_of-term" nach MG :*)

(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0"  !!! *)

  (*wir holen 'a' wieder aus der Klammerung heraus...*)

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

  term2str t;

   "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";

(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)

  val SOME (t,_) =

      rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;

  term2str t;

  "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; 

  (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben

  "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)

  (*das rewriting l"asst sich beobachten mit

  trace_rewrite:=true;

  *)

"------15.11.02 --------------------------";

  val t = (term_of o the o (parse thy)) "1 + a * x + b * x";

  val bdv = (term_of o the o (parse thy)) "bdv";

  val a = (term_of o the o (parse thy)) "a";

 trace_rewrite:=true;

 (* Anwenden einer Regelmenge aus Termorder.ML: *)

 val SOME (t,_) =

     rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

 term2str t;

 val SOME (t,_) =

     rewrite_set_ thy false discard_parentheses t;

 term2str t;

"1 + b * x + x * a";

 val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";

 val SOME (t,_) =

     rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

 term2str t;

 val SOME (t,_) =

     rewrite_set_ thy false discard_parentheses t;

 term2str t;

"1 + (x + b * x) * a + a ^^^ 2";

 val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";

 val SOME (t,_) =

     rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

 term2str t;

 val SOME (t,_) =

     rewrite_set_ thy false discard_parentheses t;

 term2str t;

"1 + b * a + (7 + x) * a ^^^ 2";

(* MG2003

 Atools.thy       grundlegende Algebra

 Poly.thy         Polynome

 Rational.thy     Br"uche

 Root.thy         Wurzeln

 RootRat.thy      Wurzen + Br"uche

 Termorder.thy    BITTE NUR HIERHER SCHREIBEN (...WN03)

 cd"knowledge";

 remove_thy"Termorder";

 use_thy"Isac";

 get_thm Termorder.thy "bdv_n_collect";

 get_thm Isac.thy "bdv_n_collect";

*)

 val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";

 val SOME (t,_) =

     rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

 term2str t;

 val SOME (t,_) =

     rewrite_set_ thy false discard_parentheses t;

 term2str t;

"(7 + x) * a ^^^ 2";

 val t = (term_of o the o (parse Termorder.thy)) "Pi";

 val t = (term_of o the o (parseold thy)) "7";

----------------------------------------------------------------------*)