walther@59627: (* Title:  Knowledge/polyeq-1.sml
walther@59627:            testexamples for PolyEq, poynomial equations and equational systems
walther@59627:    Author: Richard Lang 2003  
walther@59627:    (c) due to copyright terms
walther@59627: WN030609: some expls dont work due to unfinished handling of 'expanded terms';
walther@59627:           others marked with TODO have to be checked, too.
walther@59627: *)
walther@59627: 
walther@59627: "-----------------------------------------------------------------";
walther@59627: "table of contents -----------------------------------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
walther@59627: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
walther@59627: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
walther@59627: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
walther@59627: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
walther@59627: "----------- rls make_polynomial_in ------------------------------";
walther@59627: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
walther@59627: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: "-----------------------------------------------------------------";
walther@59627: 
walther@59627: 
walther@59627: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
walther@59627: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
walther@59627: "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
walther@59627:  val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
walther@59627:  	    "solveFor x","solutions L"];
walther@59627:  val (dI',pI',mI') =
walther@59627:      ("PolyEq",["degree_2","expanded","univariate","equation"],
walther@59627:       ["PolyEq","complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
walther@59627: (*WN.2.5.03 TODO FIXME Matthias ?
walther@59627:  case f of 
walther@59627:      Form' 
walther@59627: 	 (FormKF 
walther@59627: 	      (~1,EdUndef,0,Nundef,
walther@59627: 	       "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]")) 
walther@59627: 	 => ()
walther@59627:    | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
walther@59627:  this will be simplified [x = a, x = b] to by Factor.ML*)
walther@59627: 
walther@59627: 
walther@59627: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
walther@59627: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
walther@59627: "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
walther@59627:  val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
walther@59627:  	    "solveFor x","solutions L"];
walther@59627:  val (dI',pI',mI') =
walther@59627:      ("PolyEq",["degree_2","expanded","univariate","equation"],
walther@59627:       ["PolyEq","complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
walther@59627: (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
walther@59627:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
walther@59627: *)
walther@59627: 
walther@59627: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
walther@59627: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
walther@59627: "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
walther@59627: val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
walther@59627:  	    "solveFor x","solutions L"];
walther@59627: val (dI',pI',mI') =
walther@59627:      ("PolyEq",["degree_2","expanded","univariate","equation"],
walther@59627:       ["PolyEq","complete_square"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59627: (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
walther@59627:  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
walther@59627: *)
walther@59627: if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
walther@59627: else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
walther@59627: 
walther@59627: 
walther@59627: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
walther@59627: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
walther@59627: "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
walther@59627: (*EP-17 Schalk_I_p86_n5*)
walther@59627: val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
walther@59627: (* refine fmz ["univariate","equation"];
walther@59627: *)
walther@59627: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (* val nxt =
walther@59627:   ("Model_Problem",
walther@59627:    Model_Problem ["normalise","polynomial","univariate","equation"])
walther@59627:   : string * tac*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (* val nxt =
walther@59627:   ("Subproblem",
walther@59627:    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
walther@59627:   : string * tac *)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (*val nxt =
walther@59627:   ("Model_Problem",
walther@59627:    Model_Problem ["degree_1","polynomial","univariate","equation"])
walther@59627:   : string * tac *)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: case f of FormKF "[x = 2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
walther@59627: 
walther@59627: 
walther@59627: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
walther@59627: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
walther@59627: "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
walther@59627: (*is in rlang.sml, too*)
walther@59627: val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
walther@59627: 	   "solveFor x","solutions L"];
walther@59627: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (* val nxt =
walther@59627:   ("Model_Problem",
walther@59627:    Model_Problem ["normalise","polynomial","univariate","equation"])
walther@59627:   : string * tac *)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (* val nxt =
walther@59627:   ("Subproblem",
walther@59627:    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
walther@59627:   : string * tac*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: (*val nxt =
walther@59627:   ("Model_Problem",
walther@59627:    Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
walther@59627:   : string * tac*)
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: case f of FormKF "[x = 2 / 15, x = 1]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
walther@59627: 
walther@59627: 
walther@59627: "    -4 + x^^^2 =0     ";
walther@59627: "    -4 + x^^^2 =0     ";
walther@59627: "    -4 + x^^^2 =0     ";
walther@59627: val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
walther@59627: (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
walther@59627: (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
walther@59627: val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
walther@59627: (*val p = e_pos'; 
walther@59627: val c = []; 
walther@59627: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
walther@59627: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
walther@59627: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@59627: 
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59627: case f of FormKF "[x = 2, x = -2]" => ()
walther@59627: 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
walther@59627: 
walther@59627: "----------- rls make_polynomial_in ------------------------------";
walther@59627: "----------- rls make_polynomial_in ------------------------------";
walther@59627: "----------- rls make_polynomial_in ------------------------------";
walther@59627: (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
walther@59627: (*WN.19.3.03 ---v-*)
walther@59627: (*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
walther@59627: val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
walther@59627: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
walther@59868: if UnparseC.term t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
walther@59627: else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
walther@59627: "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
walther@59627: (*WN.19.3.03 ---^-*)
walther@59627: 
walther@59627: (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
walther@59627: val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
walther@59627: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
walther@59868: if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()
walther@59627: else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
walther@59627: 
walther@59627: (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
walther@59627: val t = str2term 
walther@59627: "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";
walther@59627: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
walther@59868: if UnparseC.term t' =
walther@59627: "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"
walther@59627: then ()
walther@59627: else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
walther@59627: "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";
walther@59627: 
walther@59627: val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
walther@59868: if UnparseC.term t' = 
walther@59627: "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"
walther@59627: then ()
walther@59627: else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
walther@59627: "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";
walther@59627: 
walther@59627: (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
walther@59627: val t = str2term 
walther@59627: "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
walther@59627: val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
walther@59627: (* the invisible parentheses are as expected *)
walther@59627: 
walther@59627: val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
walther@59901: Rewrite.trace_on:=(*true*)false;
walther@59627: rewrite_set_ thy false expand_binoms t;
walther@59901: Rewrite.trace_on:=false;
walther@59627: 
walther@59627: 
walther@59627: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
walther@59627: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
walther@59627: "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
walther@59627: reset_states ();
walther@59627: CalcTree
walther@59627: [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], 
walther@59627:   ("PolyEq",["univariate","equation"],["no_met"]))];
walther@59627: Iterator 1;
walther@59627: moveActiveRoot 1;
walther@59627: 
walther@59627: autoCalculate 1 CompleteCalc;
walther@59627: val ((pt,p),_) = get_calc 1; show_pt pt;
walther@59627: interSteps 1 ([1],Res)
walther@59627: (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
walther@59627: 
walther@59627: 
walther@59627: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
walther@59627: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
walther@59627: "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
walther@59627: val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
walther@59627: val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
walther@59627: val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
walther@59627: (* steps in rls d2_polyeq_bdv_only_simplify:*)
walther@59627: 
walther@59627: (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
walther@59868: t |> UnparseC.term; t |> atomty;
walther@59871: val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
walther@59868: thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
walther@59868: val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
walther@59627: 
walther@59627: (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) 
walther@59627:                                                                         --> x = 0 | -6 + 5 * x = 0*)
walther@59868: t' |> UnparseC.term; t' |> atomty;
walther@59871: val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
walther@59868: thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
walther@59868: val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
walther@59627: (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
walther@59627:    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
walther@59627: *)
walther@59868: if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
walther@59627: else error "rls d2_polyeq_bdv_only_simplify broken";