(* 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";

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