(* testexamples for Poly, polynomials

   author: Matthias Goldgruber 2003

   (c) due to copyright terms

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

use"poly.sml";

****************************************************************.*)

(******************************************************************

  WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'

	   'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'

*******************************************************************)

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

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

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

"-------- build Script Expand_binoms -----------------------------";

"-------- investigate new uniary minus ---------------------------";

"-------- Bsple aus Schalk I -------------------------------------";

"-------- Script 'simplification for_polynomials' ----------------";

"-------- check pbl  'polynomial simplification' -----------------";

"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";

"-------- norm_Poly NOT COMPLETE ---------------------------------";

"-------- ord_make_polynomial ------------------------------------";

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

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

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

"-------- build Script Expand_binoms -----------------------------";

"-------- build Script Expand_binoms -----------------------------";

"-------- build Script Expand_binoms -----------------------------";

val scr_expand_binoms =

"Script Expand_binoms t_t =" ^

"(Repeat                       " ^

"((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^

" (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^

" (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^

" (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^

" (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^

" (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^

" (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^

" (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^

" (Try (Repeat (Rewrite add_0_left      False))) @@ " ^

" (Try (Repeat (Calculate PLUS  ))) @@ " ^

" (Try (Repeat (Calculate TIMES ))) @@ " ^

" (Try (Repeat (Calculate POWER))) @@ " ^

" (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^

" (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^

" (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^

" (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^

" (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^

" (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^

" (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^

" (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^ 

" (Try (Repeat (Calculate PLUS  ))) @@ " ^

" (Try (Repeat (Calculate TIMES ))) @@ " ^

" (Try (Repeat (Calculate POWER)))) " ^  

" t_t)";

val scr_expand_binoms =

"Script Expand_binoms t_t = t_t";

val ---------------------------------------------- = "11111";

parse thy scr_expand_binoms;

val ---------------------------------------------- = "22222";

(*----------------------------------------------

"-------- investigate new uniary minus ---------------------------";

"-------- investigate new uniary minus ---------------------------";

"-------- investigate new uniary minus ---------------------------";

val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)

atomty t;

(*** -------------

*** Const ( Trueprop, bool => prop)

*** . Const ( op =, [real, real] => bool)

*** . . Const ( op -, [real, real] => real)

*** . . . Const ( 0, real)

*** . . . Var ((x, 0), real)

*** . . Const ( uminus, real => real)

*** . . . Var ((x, 0), real)              *)

val t = (term_of o the o (parse thy)) "-1";

atomty t;

(*** -------------

*** Free ( -1, real)                      *)

val t = (term_of o the o (parse thy)) "- 1";

atomty t;

(*** -------------

*** Const ( uminus, real => real)

*** . Free ( 1, real)                     *)

val t = (term_of o the o (parse thy)) "-x"; (*1-x  syntyx error !!!*)

atomty t;

(**** -------------

*** Free ( -x, real)*)

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

atomty t;

(**** -------------

*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)

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

atomty t;

(**** -------------

*** Free ( -x, real)*)

"-------- Bsple aus Schalk I -------------------------------------";

"-------- Bsple aus Schalk I -------------------------------------";

"-------- Bsple aus Schalk I -------------------------------------";

(*SPB Schalk I p.63 No.267b*)

val t = str2term

 	    "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";

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

if (term2str t) = 

"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 1";

(*SPB Schalk I p.63 No.275b*)

 val t = str2term

 	     "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";

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

 term2str t;

if (term2str t) = 

"3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \

\4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 2";

(*SPB Schalk I p.63 No.279b*)

 val t = str2term

 	     "(x-a)*(x-b)*(x-c)*(x-d)";

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

 term2str t;

(* Richtig! *)

if (term2str t) = 

"a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 3";

(*SPB Schalk I p.63 No.291*)

 val t = str2term

 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";

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

 term2str t;

if (term2str t) = 

"50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 4";

(*SPB Schalk I p.64 No.295c*)

 val t = str2term

 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";

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

 term2str t;

if (term2str t) = 

"169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\

\ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 5";

(*SPB Schalk I p.64 No.299a*)

 val t = str2term

 "(x - y)*(x + y)";

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

 term2str t;

if (term2str t) = 

"x ^^^ 2 + -1 * y ^^^ 2"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 6";

(*SPB Schalk I p.64 No.300c*)

 val t = str2term

 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";

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

 term2str t;

if (term2str t) = 

"-1 + 9 * x ^^^ 4 * y ^^^ 2"

then ()

else raise error "poly.sml: diff.behav. in make_polynomial 7";

(*SPB Schalk I p.64 No.302*)

val t = str2term

 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";

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

if term2str t = "0" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 8";

(* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)

(*SPB Schalk I p.64 No.306a*)

val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";

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

if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()

else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \

		 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";

(*WN071729 when reducing "rls reduce_012_" for Schaerding,

the above resulted in the term below ... but reduces from then correctly*)

val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";

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

if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 9b";

(*SPB Schalk I p.64 No.296a*)

val t = str2term "(x - a)^^^3";

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

if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"

then () else raise error "poly.sml: diff.behav. in make_polynomial 10";

(*SPB Schalk I p.64 No.296c*)

val t = str2term "(-3*x - 4*y)^^^3";

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

if (term2str t) = 

"-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"

then () else raise error "poly.sml: diff.behav. in make_polynomial 11";

(*SPB Schalk I p.62 No.242c*)

val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";

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

if (term2str t) = "1" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 12";

(*SPB Schalk I p.60 No.209a*)

val t = str2term "a^^^(7-x) * a^^^x";

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

if term2str t = "a ^^^ 7" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 13";

(*SPB Schalk I p.60 No.209d*)

val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";

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

if term2str t = "d ^^^ 3" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 14";

(*---------------------------------------------------------------------*)

(*------------------ Bsple bei denen es Probleme gibt------------------*)

(*---------------------------------------------------------------------*)

(*Schalk I p.64 No.303*)

val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";

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

if term2str t = "1280 * b ^^^ 4" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 14b";

(* Richtig - aber Binomische Formel wurde nicht verwendet! *)

(*--------------------------------------------------------------------*)

(*----------------------- Eigene Beispiele ---------------------------*)

(*--------------------------------------------------------------------*)

(*SPO*)

val t = str2term "a^^^2*a^^^(-2)";

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

if term2str t = "1" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 15";

(*SPO*)

val t = str2term "a + a + a";

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

if term2str t = "3 * a" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 16";

(*SPO*)

val t = str2term "a + b + b + b";

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

if term2str t = "a + 3 * b" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 17";

(*SPO*)

val t = str2term "a^^^2*b*b^^^(-1)";

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

if term2str t = "a ^^^ 2" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 18";

(*SPO*)

val t = str2term "a^^^2*a^^^(-2)";

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

if (term2str t) = "1" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 19";

(*SPO*)

val t = str2term "b + a - b";

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

if (term2str t) = "a" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 20";

(*SPO*)

val t = str2term "b * a * a";

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

if term2str t = "a ^^^ 2 * b" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 21";

(*SPO*)

val t = str2term "(a^^^2)^^^3";

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

if term2str t = "a ^^^ 6" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 22";

(*SPO*)

val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";

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

if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 23";

(*SPO*)

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

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

if (term2str t) = "a ^^^ 4" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 24";

(*SPO*)

val t = str2term "a * b * b^^^(-1) + a";

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

if (term2str t) = "2 * a" then ()

else raise error "poly.sml: diff.behav. in make_polynomial 25";

(*SPO*)

val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";

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

if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"

then () else raise error "poly.sml: diff.behav. in make_polynomial 26";

(*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)

(*SPO*)

val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";

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

 term2str t;

if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"

 then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)

val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";

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

 term2str t;

if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"

 then () else raise error "poly.sml: diff.behav. in make_polynomial 28";

"-------- Script 'simplification for_polynomials' ----------------";

"-------- Script 'simplification for_polynomials' ----------------";

"-------- Script 'simplification for_polynomials' ----------------";

val str = 

"Script SimplifyScript (t_::real) =                \

\  ((Rewrite_Set norm_Poly False) t_)";

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty sc;

"-------- check pbl  'polynomial simplification' -----------------";

"-------- check pbl  'polynomial simplification' -----------------";

"-------- check pbl  'polynomial simplification' -----------------";

val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \

	   \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",

	   "normalform N"];

(*0*)

case refine fmz ["polynomial","simplification"]of

    [Matches (["polynomial", "simplification"], _)] => ()

  | _ => raise error "poly.sml diff.behav. in check pbl, refine";

(*...if there is an error, then ...*)

(*1*)

print_depth 7;

val pbt = get_pbt ["polynomial","simplification"];

print_depth 3;

(*if there is ...

> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;

... then trace_rewrite:*)

(*2*)

trace_rewrite:=true; 

match_pbl fmz pbt;

trace_rewrite:=false;

(*... if there is no rewrite, then there is something wrong with prls*)

(*3*)

print_depth 7;

val prls = (#prls o get_pbt) ["polynomial","simplification"];

print_depth 3;

val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \

		 \- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";

trace_rewrite:=true; 

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

trace_rewrite:=false;

if t' = HOLogic.true_const then () 

else raise error "poly.sml: diff.behav. in check pbl 'polynomial..";

(*... if this works, but (*1*) does still NOT work, check types:*)

(*4*)

show_types:=true;

(*

> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;

val wh = [False "(t_::real => real) (is_polyexp::real)"]

......................^^^^^^^^^^^^...............^^^^*)

val Matches' _ = match_pbl fmz pbt;

show_types:=false;

"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";

"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";

"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";

val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \

	   \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",

	   "normalform N"];

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

  ("Poly",["polynomial","simplification"],

   ["simplification","for_polynomials"]);

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;

(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

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; 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;

if f2str f = 

"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"

then () else raise error "poly.sml diff.behav. in me Schalk I p.63 No.267b";

"-------- interSteps for Schalk 299a -----------------------------";

"-------- interSteps for Schalk 299a -----------------------------";

"-------- interSteps for Schalk 299a -----------------------------";

states:=[];

CalcTree

[(["TERM ((x - y)*(x + y))", "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["simplification","for_polynomials"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; show_pt pt;

interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);

val ((pt,p),_) = get_calc 1; show_pt pt;

if existpt' ([1,1], Frm) pt then ()

else raise error "poly.sml: interSteps doesnt work again 1";

interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);

val ((pt,p),_) = get_calc 1; show_pt pt;

if existpt' ([1,1,1], Frm) pt then ()

else raise error "poly.sml: interSteps doesnt work again 2";

"-------- norm_Poly NOT COMPLETE ---------------------------------";

"-------- norm_Poly NOT COMPLETE ---------------------------------";

"-------- norm_Poly NOT COMPLETE ---------------------------------";

trace_rewrite:=true;

val SOME (f',_) = rewrite_set_ thy false norm_Poly 

(str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);

trace_rewrite:=false;

term2str f';

"-------- ord_make_polynomial ------------------------------------";

"-------- ord_make_polynomial ------------------------------------";

"-------- ord_make_polynomial ------------------------------------";

val t1 = str2term "2 * b + (3 * a + 3 * b)";

val t2 = str2term "3 * a + 3 * b + 2 * b";

if ord_make_polynomial true Poly.thy [] (t1, t2) then ()

else raise error "poly.sml: diff.behav. in ord_make_polynomial";

(*WN071202: ^^^ why then is there no rewriting ...*)

val term = str2term "2*b + (3*a + 3*b)";

val NONE = rewrite_set_ Isac.thy false order_add_mult term;

(*or why is there no rewriting this way...*)

val t1 = str2term "2 * b + (3 * a + 3 * b)";

val t2 = str2term "3 * a + (2 * b + 3 * b)";

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