1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Wed Sep 18 12:15:59 2019 +0200
1.3 @@ -0,0 +1,304 @@
1.4 +(* Title: Knowledge/polyeq-1.sml
1.5 + testexamples for PolyEq, poynomial equations and equational systems
1.6 + Author: Richard Lang 2003
1.7 + (c) due to copyright terms
1.8 +WN030609: some expls dont work due to unfinished handling of 'expanded terms';
1.9 + others marked with TODO have to be checked, too.
1.10 +*)
1.11 +
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.16 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.17 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.18 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.19 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.20 +"----------- rls make_polynomial_in ------------------------------";
1.21 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.22 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.23 +"-----------------------------------------------------------------";
1.24 +"-----------------------------------------------------------------";
1.25 +
1.26 +
1.27 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.28 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.29 +"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.30 + val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
1.31 + "solveFor x","solutions L"];
1.32 + val (dI',pI',mI') =
1.33 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.34 + ["PolyEq","complete_square"]);
1.35 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.53 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.54 +(*WN.2.5.03 TODO FIXME Matthias ?
1.55 + case f of
1.56 + Form'
1.57 + (FormKF
1.58 + (~1,EdUndef,0,Nundef,
1.59 + "[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)]"))
1.60 + => ()
1.61 + | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
1.62 + this will be simplified [x = a, x = b] to by Factor.ML*)
1.63 +
1.64 +
1.65 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.66 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.67 +"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.68 + val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.69 + "solveFor x","solutions L"];
1.70 + val (dI',pI',mI') =
1.71 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.72 + ["PolyEq","complete_square"]);
1.73 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.77 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.78 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.87 +(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1.88 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1.89 + | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.90 +*)
1.91 +
1.92 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.93 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.94 +"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.95 +val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.96 + "solveFor x","solutions L"];
1.97 +val (dI',pI',mI') =
1.98 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.99 + ["PolyEq","complete_square"]);
1.100 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.101 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.102 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.103 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.104 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.106 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.107 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.109 +(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1.110 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1.111 + | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1.112 +*)
1.113 +if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1.114 +else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1.115 +
1.116 +
1.117 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.118 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.119 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.120 +(*EP-17 Schalk_I_p86_n5*)
1.121 +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1.122 +(* refine fmz ["univariate","equation"];
1.123 +*)
1.124 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.125 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.126 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.127 +(* val nxt =
1.128 + ("Model_Problem",
1.129 + Model_Problem ["normalise","polynomial","univariate","equation"])
1.130 + : string * tac*)
1.131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.132 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.133 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.134 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.135 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.136 +(* val nxt =
1.137 + ("Subproblem",
1.138 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.139 + : string * tac *)
1.140 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.141 +(*val nxt =
1.142 + ("Model_Problem",
1.143 + Model_Problem ["degree_1","polynomial","univariate","equation"])
1.144 + : string * tac *)
1.145 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.146 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.147 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.148 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.149 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.150 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.151 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.152 +case f of FormKF "[x = 2]" => ()
1.153 + | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1.154 +
1.155 +
1.156 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.157 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.158 +"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.159 +(*is in rlang.sml, too*)
1.160 +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1.161 + "solveFor x","solutions L"];
1.162 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.163 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.164 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.165 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.166 +(* val nxt =
1.167 + ("Model_Problem",
1.168 + Model_Problem ["normalise","polynomial","univariate","equation"])
1.169 + : string * tac *)
1.170 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.171 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.172 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.173 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.174 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.175 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.176 +(* val nxt =
1.177 + ("Subproblem",
1.178 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.179 + : string * tac*)
1.180 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.181 +(*val nxt =
1.182 + ("Model_Problem",
1.183 + Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
1.184 + : string * tac*)
1.185 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.186 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.187 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.188 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.189 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.190 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.191 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.192 +case f of FormKF "[x = 2 / 15, x = 1]" => ()
1.193 + | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1.194 +
1.195 +
1.196 +" -4 + x^^^2 =0 ";
1.197 +" -4 + x^^^2 =0 ";
1.198 +" -4 + x^^^2 =0 ";
1.199 +val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1.200 +(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1.201 +(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1.202 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.203 +(*val p = e_pos';
1.204 +val c = [];
1.205 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.206 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.207 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.208 +
1.209 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.210 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.211 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.212 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.213 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.214 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.215 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.216 +case f of FormKF "[x = 2, x = -2]" => ()
1.217 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1.218 +
1.219 +"----------- rls make_polynomial_in ------------------------------";
1.220 +"----------- rls make_polynomial_in ------------------------------";
1.221 +"----------- rls make_polynomial_in ------------------------------";
1.222 +(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1.223 +(*WN.19.3.03 ---v-*)
1.224 +(*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
1.225 +val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.226 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.227 +if term2str t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
1.228 +else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
1.229 +"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1.230 +(*WN.19.3.03 ---^-*)
1.231 +
1.232 +(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1.233 +val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.234 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.235 +if term2str t' = "y ^^^ 2 + -2 * x * p = 0" then ()
1.236 +else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
1.237 +
1.238 +(*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
1.239 +val t = str2term
1.240 +"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";
1.241 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.242 +if term2str t' =
1.243 +"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"
1.244 +then ()
1.245 +else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
1.246 +"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";
1.247 +
1.248 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.249 +if term2str t' =
1.250 +"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"
1.251 +then ()
1.252 +else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
1.253 +"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";
1.254 +
1.255 +(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1.256 +val t = str2term
1.257 +"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1.258 +val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.259 +(* the invisible parentheses are as expected *)
1.260 +
1.261 +val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1.262 +trace_rewrite:=(*true*)false;
1.263 +rewrite_set_ thy false expand_binoms t;
1.264 +trace_rewrite:=false;
1.265 +
1.266 +
1.267 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.268 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.269 +"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.270 +reset_states ();
1.271 +CalcTree
1.272 +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1.273 + ("PolyEq",["univariate","equation"],["no_met"]))];
1.274 +Iterator 1;
1.275 +moveActiveRoot 1;
1.276 +
1.277 +autoCalculate 1 CompleteCalc;
1.278 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.279 +interSteps 1 ([1],Res)
1.280 +(*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
1.281 +
1.282 +
1.283 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.284 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.285 +"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.286 +val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
1.287 +val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
1.288 +val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
1.289 +(* steps in rls d2_polyeq_bdv_only_simplify:*)
1.290 +
1.291 +(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
1.292 +t |> term2str; t |> atomty;
1.293 +val thm = num_str @{thm d2_prescind1};
1.294 +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
1.295 +val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
1.296 +
1.297 +(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))
1.298 + --> x = 0 | -6 + 5 * x = 0*)
1.299 +t' |> term2str; t' |> atomty;
1.300 +val thm = num_str @{thm d2_reduce_equation1};
1.301 +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
1.302 +val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t'';
1.303 +(* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.304 + instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
1.305 +*)
1.306 +if term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
1.307 +else error "rls d2_polyeq_bdv_only_simplify broken";