1 (* Title: Knowledge/polyeq- 1.sml
2 testexamples for PolyEq, poynomial equations and equational systems
3 Author: Richard Lang 2003
4 (c) due to copyright terms
5 WN030609: some expls dont work due to unfinished handling of 'expanded terms';
6 others marked with TODO have to be checked, too.
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "------ polyeq-2.sml ---------------------------------------------";
13 "------ polyeq-1.sml ---------------------------------------------";
14 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
15 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
16 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
17 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
18 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
19 "----------- rls make_polynomial_in ------------------------------";
20 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
21 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
22 "-----------------------------------------------------------------";
23 "-----------------------------------------------------------------";
26 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
27 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
28 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
29 val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",
30 "solveFor x", "solutions L"];
32 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
33 ["PolyEq", "complete_square"]);
34 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
40 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
42 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
43 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
45 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
46 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
47 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
48 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
49 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
50 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
51 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
52 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
53 (*WN.2.5.03 TODO FIXME Matthias ?
58 "[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)]"))
60 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";
61 this will be simplified [x = a, x = b] to by Factor.ML*)
64 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
65 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
66 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
67 val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
68 "solveFor x", "solutions L"];
70 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
71 ["PolyEq", "complete_square"]);
72 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
73 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
74 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
75 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
76 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
77 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
82 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
83 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
84 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
85 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
86 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]"
87 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
88 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
91 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
92 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
93 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
94 val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
95 "solveFor x", "solutions L"];
97 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
98 ["PolyEq", "complete_square"]);
99 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
107 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
108 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
109 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
110 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
112 if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
113 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
116 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
117 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
118 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
119 (*EP- 17 Schalk_I_p86_n5*)
120 val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"];
121 (* Refine.refine fmz ["univariate", "equation"];
123 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
124 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 Model_Problem ["normalise", "polynomial", "univariate", "equation"])
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
137 Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
142 Model_Problem ["degree_1", "polynomial", "univariate", "equation"])
144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 case f of Test_Out.FormKF "[x = 2]" => ()
152 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
155 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
156 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
157 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
158 (*is in rlang.sml, too*)
159 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",
160 "solveFor x", "solutions L"];
161 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
162 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
163 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*)
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
167 Model_Problem ["normalise", "polynomial", "univariate", "equation"])
169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
173 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
177 Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
182 Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()
192 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
195 " -4 + x \<up> 2 =0 ";
196 " -4 + x \<up> 2 =0 ";
197 " -4 + x \<up> 2 =0 ";
198 val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];
199 (* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)
200 (*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)
201 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
202 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
211 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
212 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
214 "----------- rls make_polynomial_in ------------------------------";
215 "----------- rls make_polynomial_in ------------------------------";
216 "----------- rls make_polynomial_in ------------------------------";
218 val ctxt = @{context};
219 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
221 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
222 val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
223 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
224 if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
225 else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
226 "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
229 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
230 val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";
231 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
232 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
233 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
235 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
236 val t = TermC.str2term
237 "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";
238 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
239 if UnparseC.term t' =
240 "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"
242 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
243 "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";
245 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_ratpoly_in t;
246 if UnparseC.term t' =
247 "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"
249 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
250 "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";
252 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
253 val t = TermC.str2term
254 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
255 val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
256 (* the invisible parentheses are as expected *)
258 val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
259 rewrite_set_ ctxt false expand_binoms t;
262 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
263 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
264 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
267 [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"],
268 ("PolyEq",["univariate", "equation"],["no_met"]))];
272 autoCalculate 1 CompleteCalc;
273 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
274 interSteps 1 ([1],Res)
275 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
278 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
279 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
280 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
281 val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";
282 val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;
284 (* steps in rls d2_polyeq_bdv_only_simplify:*)
286 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
287 t |> UnparseC.term; t |> TermC.atomty;
288 val thm = @{thm d2_prescind1};
289 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
290 val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
292 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
293 --> x = 0 | -6 + 5 * x = 0*)
294 t' |> UnparseC.term; t' |> TermC.atomty;
295 val thm = @{thm d2_reduce_equation1};
296 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
297 val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
298 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
299 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
301 if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
302 else error "rls d2_polyeq_bdv_only_simplify broken";