(* Title:  Knowledge/polyeq- 1.sml

           testexamples for PolyEq, poynomial equations and equational systems

   Author: Richard Lang 2003  

   (c) due to copyright terms

WN030609: some expls dont work due to unfinished handling of 'expanded terms';

          others marked with TODO have to be checked, too.

*)

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

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

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

"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";

"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

"----------- rls make_polynomial_in ------------------------------";

"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

"----------- rls d2_polyeq_bdv_only_simplify ---------------------";

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

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

"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

 val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",

 	    "solveFor x", "solutions L"];

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

     ("PolyEq",["degree_2", "expanded", "univariate", "equation"],

      ["PolyEq", "complete_square"]);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(*WN.2.5.03 TODO FIXME Matthias ?

 case f of 

     Form' 

	 (Test_Out.FormKF 

	      (~1,EdUndef,0,Nundef,

	       "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]")) 

	 => ()

   | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";

 this will be simplified [x = a, x = b] to by Factor.ML*)

"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

 val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)

 	    "solveFor x", "solutions L"];

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

     ("PolyEq",["degree_2", "expanded", "univariate", "equation"],

      ["PolyEq", "complete_square"]);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]"

 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()

	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";

*)

"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)

 	    "solveFor x", "solutions L"];

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

     ("PolyEq",["degree_2", "expanded", "univariate", "equation"],

      ["PolyEq", "complete_square"]);

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

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

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

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

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

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

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

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

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

(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"

 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()

	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";

*)

if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()

else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";

"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";

"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";

"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";

(*EP- 17 Schalk_I_p86_n5*)

val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"];

(* Refine.refine fmz ["univariate", "equation"];

*)

val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);

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

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt =

  ("Model_Problem",

   Model_Problem ["normalise", "polynomial", "univariate", "equation"])

  : string * tac*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt =

  ("Subproblem",

   Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))

  : string * tac *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt =

  ("Model_Problem",

   Model_Problem ["degree_1", "polynomial", "univariate", "equation"])

  : string * tac *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

case f of Test_Out.FormKF "[x = 2]" => ()

	 | _ => error "polyeq.sml: diff.behav. in [x = 2]";

"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

(*is in rlang.sml, too*)

val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",

	   "solveFor x", "solutions L"];

val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);

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

(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt =

  ("Model_Problem",

   Model_Problem ["normalise", "polynomial", "univariate", "equation"])

  : string * tac *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt =

  ("Subproblem",

   Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))

  : string * tac*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt =

  ("Model_Problem",

   Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])

  : string * tac*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()

	 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";

"    -4 + x \<up> 2 =0     ";

"    -4 + x \<up> 2 =0     ";

"    -4 + x \<up> 2 =0     ";

val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];

(* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)

(*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)

val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);

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

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()

	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";

"----------- rls make_polynomial_in ------------------------------";

"----------- rls make_polynomial_in ------------------------------";

"----------- rls make_polynomial_in ------------------------------";

val thy = @{theory};

(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)

(*WN.19.3.03 ---v-*)

(*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");

val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";

val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()

else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";

"- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";

(*WN.19.3.03 ---^-*)

(*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");

val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";

val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()

else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";

(*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");

val t = TermC.str2term 

"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1 * (x1 * (y2 * (1 / 2))) + - 1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + - 1 * (y3 * (1 / 2 * x2)) = 0";

val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

if UnparseC.term t' =

"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0"

then ()

else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";

"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";

val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;

if UnparseC.term t' = 

"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0"

then ()

else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";

"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) + - 1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - 1 * y3 * (1 / 2)) * x2 = 0";

(*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");

val t = TermC.str2term 

"A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";

val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

(* the invisible parentheses are as expected *)

val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";

Rewrite.trace_on:= false; (*true false*)

rewrite_set_ thy false expand_binoms t;

Rewrite.trace_on:=false; (*true false*)

"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

reset_states ();

CalcTree

[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"], 

  ("PolyEq",["univariate", "equation"],["no_met"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

interSteps 1 ([1],Res)

(*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);

"----------- rls d2_polyeq_bdv_only_simplify ---------------------";

"----------- rls d2_polyeq_bdv_only_simplify ---------------------";

"----------- rls d2_polyeq_bdv_only_simplify ---------------------";

val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";

val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];

val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;

(* steps in rls d2_polyeq_bdv_only_simplify:*)

(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)

t |> UnparseC.term; t |> TermC.atomty;

val thm = @{thm d2_prescind1};

thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;

val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';

(*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 

                                                                        --> x = 0 | -6 + 5 * x = 0*)

t' |> UnparseC.term; t' |> TermC.atomty;

val thm = @{thm d2_reduce_equation1};

thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;

val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';

(* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"

   instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"

*)

if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()

else error "rls d2_polyeq_bdv_only_simplify broken";