1 (* title: Knowledge/polyminus.sml
4 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 "----------- fun identifier --------------------------------------------------------------------";
11 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
12 "----------- fun ist_monom ---------------------------------------------------------------------";
13 "----------- fun eval_ist_monom -------------------------";
14 "----------- watch order_add_mult ----------------------";
15 "----------- build predicate for +- ordering ------------";
16 "----------- build fasse_zusammen -----------------------";
17 "----------- build verschoenere -------------------------";
18 "----------- met simplification for_polynomials with_minu";
19 "----------- me simplification.for_polynomials.with_minus";
20 "----------- pbl polynom vereinfachen p.33 --------------";
21 "----------- met probe fuer_polynom ---------------------";
22 "----------- pbl polynom probe --------------------------";
23 "----------- pbl klammer polynom vereinfachen p.34 ------";
24 "----------- try fun applyTactics -----------------------";
25 "----------- pbl binom polynom vereinfachen p.39 --------";
26 "----------- pbl binom polynom vereinfachen: cube -------";
27 "----------- Refine.refine Vereinfache -------------------------";
28 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
29 "--------------------------------------------------------";
30 "--------------------------------------------------------";
31 "--------------------------------------------------------";
33 val thy = @{theory "PolyMinus"};
35 "----------- fun identifier --------------------------------------------------------------------";
36 "----------- fun identifier --------------------------------------------------------------------";
37 "----------- fun identifier --------------------------------------------------------------------";
38 (*+*)identifier (TermC.str2term "12 ::real") = "|||||||||||||";
39 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
40 if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
41 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
43 if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
44 if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
46 (*+*)identifier (TermC.str2term "a \<up> 2 ::real") = "|||||||||||||";(*TOODOO <-- START HERE*)
47 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
48 if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
49 if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
50 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
51 if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b";
53 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
54 if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6";
55 if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
58 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
59 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
60 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
63 "123" < "a"; (*unused due to ---vvv*)
64 "12" < "3"; (*true !!!*)
66 " a kleiner b ==> (b + a) = (a + b)";
68 TermC.str2term "222 * aaa";
70 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
71 (*TOODOO eval_kleiner *)
72 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
73 SOME ("123 kleiner 32 = False", _) => ()
74 | _ => error "polyminus.sml: 12 kleiner 9 = False";
75 case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
76 SOME ("a kleiner b = True", _) => ()
77 | _ => error "polyminus.sml: a kleiner b = True";
78 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
79 SOME ("10 * g kleiner f = False", _) => ()
80 | _ => error "polyminus.sml: 10 * g kleiner f = False";
81 case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
82 SOME ("a \<up> 2 kleiner b = True", _) => ()
83 | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
84 case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
85 SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
86 | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
87 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
88 SOME ("a * b kleiner c = True", _) => ()
89 | _ => error "polyminus.sml: a * b kleiner b = True";
90 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
91 SOME ("3 * a * b kleiner c = True", _) => ()
92 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
95 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
96 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
97 eval_kleiner "aaa" "bbb" t "ccc";
98 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
99 ("aaa", "bbb", t, "ccc");
100 (*if*) TermC.is_num b (*else*);
102 (*if*) identifier a < identifier b (*else*);
103 "~~~~~ fun identifier , args:"; val (t) = (a);
105 Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
106 (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
107 | _ => error "eval_kleiner CHANGED"; (*isa*)
108 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
111 "----------- fun ist_monom ---------------------------------------------------------------------";
112 "----------- fun ist_monom ---------------------------------------------------------------------";
113 "----------- fun ist_monom ---------------------------------------------------------------------";
114 val t = TermC.str2term "0 ::real";
115 if ist_monom t then () else error "ist_monom 1";
117 val t = TermC.str2term "a";
118 if ist_monom t then () else error "ist_monom 2";
120 val t = TermC.str2term "2 * a";
121 if ist_monom t then () else error "ist_monom 3";
123 val t = TermC.str2term "2 * a * b";
124 if ist_monom t then () else error "ist_monom 4";
126 val t = TermC.str2term "a * b";
127 if ist_monom t then () else error "ist_monom 5";
129 (*not covered before NEW numerals*)
130 val t = TermC.str2term "2 * a \<up> 2 * b";
131 if ist_monom t then () else error "ist_monom 6";
133 (*not covered before NEW numerals*)
134 val t = TermC.str2term "a \<up> 2 * b \<up> 3";
135 if ist_monom t then () else error "ist_monom 7";
137 val t = TermC.str2term "a \<up> 2 * 4 * b \<up> 3 * 5";
138 if ist_monom t then () else error "ist_monom 8";
141 "----------- fun eval_ist_monom ----------------------------------";
142 "----------- fun eval_ist_monom ----------------------------------";
143 "----------- fun eval_ist_monom ----------------------------------";
144 case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
145 SOME ("12 ist_monom = True", _) => ()
146 | _ => error "polyminus.sml: 12 ist_monom = True";
148 case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of
149 SOME ("a ist_monom = True", _) => ()
150 | _ => error "polyminus.sml: a ist_monom = True";
152 case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of
153 SOME ("3 * a ist_monom = True", _) => ()
154 | _ => error "polyminus.sml: 3 * a ist_monom = True";
156 case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of
157 SOME ("a \<up> 2 ist_monom = True", _) => ()
158 | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
160 case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of
161 SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
162 | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
164 case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
165 SOME ("a * b ist_monom = True", _) => ()
166 | _ => error "polyminus.sml: a*b ist_monom = True";
168 case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of
169 SOME ("3 * a * b ist_monom = True", _) => ()
170 | _ => error "polyminus.sml: 3*a*b ist_monom = True";
173 "----------- watch order_add_mult -------------------------------";
174 "----------- watch order_add_mult -------------------------------";
175 "----------- watch order_add_mult -------------------------------";
176 "----- with these simple variables it works...";
177 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
178 Rewrite.trace_on:=false; (*true false*)
179 val t = TermC.str2term "((a + d) + c) + b";
180 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
181 if UnparseC.term t = "a + (b + (c + d))" then ()
182 else error "polyminus.sml 1 watch order_add_mult";
183 Rewrite.trace_on:=false; (*true false*)
185 "----- the same stepwise...";
186 val od = ord_make_polynomial true (@{theory "Poly"});
187 val t = TermC.str2term "((a + d) + c) + b";
189 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
191 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
193 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
195 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
197 if UnparseC.term t = "a + (b + (c + d))" then ()
198 else error "polyminus.sml 2 watch order_add_mult";
200 "----- if parentheses are right, left_commute is (almost) sufficient...";
201 val t = TermC.str2term "a + (d + (c + b))";
203 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
205 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
207 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
210 "----- but we do not want the parentheses at right; thus: cond.rew.";
211 "WN0712707 complicated monomials do not yet work ...";
212 val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
213 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
214 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
215 else error "polyminus.sml: order_add_mult changed";
217 "----- here we see rew_sub going into subterm with ord.rew....";
218 val od = ord_make_polynomial false (@{theory "Poly"});
219 val t = TermC.str2term "b + a + c + d";
220 val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
221 val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
222 (*@@@ rew_sub gosub: t = d + (b + a + c)
223 @@@ rew_sub begin: t = b + a + c*)
226 "----------- build predicate for +- ordering ---------------------";
227 "----------- build predicate for +- ordering ---------------------";
228 "----------- build predicate for +- ordering ---------------------";
231 "123" < "a"; (*unused due to ---vvv*)
232 "12" < "3"; (*true !!!*)
234 " a kleiner b ==> (b + a) = (a + b)";
235 TermC.str2term "aaa";
236 TermC.str2term "222 * aaa";
238 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
239 SOME ("123 kleiner 32 = False", _) => ()
240 | _ => error "polyminus.sml: 12 kleiner 9 = False";
242 case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
243 SOME ("a kleiner b = True", _) => ()
244 | _ => error "polyminus.sml: a kleiner b = True";
246 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
247 SOME ("10 * g kleiner f = False", _) => ()
248 | _ => error "polyminus.sml: 10 * g kleiner f = False";
250 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
251 (*TOODOO eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 \<longrightarrow> False*)
252 case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
253 SOME ("a \<up> 2 kleiner b = True", _) => ()
254 | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
256 case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
257 SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
258 | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
259 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
261 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
262 SOME ("a * b kleiner c = True", _) => ()
263 | _ => error "polyminus.sml: a * b kleiner b = True";
265 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
266 SOME ("3 * a * b kleiner c = True", _) => ()
267 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
269 "======= compare tausche_plus with real_num_collect";
272 val erls = erls_ordne_alphabetisch;
273 val t = TermC.str2term "b + a";
274 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
275 if UnparseC.term t = "a + b" then ()
276 else error "polyminus.sml: ordne_alphabetisch1 b + a";
278 val erls = Atools_erls;
279 val t = TermC.str2term "2*a + 3*a";
280 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
282 "======= test rewrite_, rewrite_set_";
283 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
284 val erls = erls_ordne_alphabetisch;
285 val t = TermC.str2term "b + a";
286 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
287 if UnparseC.term t = "a + b" then ()
288 else error "polyminus.sml: ordne_alphabetisch a + b";
290 val t = TermC.str2term "2*b + a";
291 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
292 if UnparseC.term t = "a + 2 * b" then ()
293 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
295 val t = TermC.str2term "a + c + b";
296 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
297 if UnparseC.term t = "a + b + c" then ()
298 else error "polyminus.sml: ordne_alphabetisch a + b + c";
300 "======= rewrite goes into subterms";
301 val t = TermC.str2term "a + c + b + d ::real";
302 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
303 if UnparseC.term t = "a + b + c + d" then ()
304 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
306 val t = TermC.str2term "a + c + d + b";
307 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
308 if UnparseC.term t = "a + b + c + d" then ()
309 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
311 "======= here we see rew_sub going into subterm with cond.rew....";
312 val t = TermC.str2term "b + a + c + d";
313 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
314 if UnparseC.term t = "a + b + c + d" then ()
315 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
317 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
318 "======= compile rls for the most complicated terms";
319 val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
320 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
321 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
322 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
323 then () else error "polyminus.sml: ordne_alphabetisch finished";
324 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
327 "----------- build fasse_zusammen --------------------------------";
328 "----------- build fasse_zusammen --------------------------------";
329 "----------- build fasse_zusammen --------------------------------";
330 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
331 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
332 if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
333 else error "polyminus.sml: fasse_zusammen finished";
335 "----------- build verschoenere ----------------------------------";
336 "----------- build verschoenere ----------------------------------";
337 "----------- build verschoenere ----------------------------------";
338 val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g";
339 val SOME (t,_) = rewrite_set_ thy false verschoenere t;
340 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
341 else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
343 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
344 Rewrite.trace_on:=false; (*true false*)
346 "----------- met simplification for_polynomials with_minus -------";
347 "----------- met simplification for_polynomials with_minus -------";
348 "----------- met simplification for_polynomials with_minus -------";
350 "Program SimplifyScript (t_t::real) = \
351 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
352 \ (Try (Rewrite_Set fasse_zusammen False)) #> \
353 \ (Try (Rewrite_Set verschoenere False))) t_t)"
354 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
357 "----------- me simplification.for_polynomials.with_minus";
358 "----------- me simplification.for_polynomials.with_minus";
359 "----------- me simplification.for_polynomials.with_minus";
361 val (p,_,f,nxt,_,pt) =
363 [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
365 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
366 ["simplification", "for_polynomials", "with_minus"]))];
367 val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 val (p,_,f,nxt,_,pt) = me nxt p c pt;
370 val (p,_,f,nxt,_,pt) = me nxt p c pt;
371 val (p,_,f,nxt,_,pt) = me nxt p c pt;
372 val (p,_,f,nxt,_,pt) = me nxt p c pt;
374 val (p,_,f,nxt,_,pt) = me nxt p c pt;
375 f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; (*isa == isa2*)
376 val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
377 val Check_Postcond ["plus_minus", "polynom", "vereinfachen"] = nxt;
379 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
380 val (*TOODOO*) Rewrite_Set "ordne_alphabetisch" = nxt;
381 f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; (*isa2*)
382 val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
383 f2str f = "3 + - 2 * e + 2 * f + 2 * g"; (*isa2*)
384 val (p,_,f,nxt,_,pt) = me nxt p c pt;
385 f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
386 val (p,_,f,nxt,_,pt) = me nxt p c pt;
387 f2str f = "3 - 2 * e + 2 * f + 2 * g"; (*isa2*)
388 if f2str f = "3 - 2 * e + 2 * f + 2 * g" (*isa2*)
389 then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
390 else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
392 "----------- pbl polynom vereinfachen p.33 -----------------------";
393 "----------- pbl polynom vereinfachen p.33 -----------------------";
394 "----------- pbl polynom vereinfachen p.33 -----------------------";
395 "----------- 140 c ---";
397 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
399 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
400 ["simplification", "for_polynomials", "with_minus"]))];
402 autoCalculate 1 CompleteCalc;
403 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
404 if p = ([], Res) andalso
405 UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
406 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
410 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
412 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
413 ["simplification", "for_polynomials", "with_minus"]))];
415 autoCalculate 1 CompleteCalc;
416 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
417 if p = ([], Res) andalso
418 UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
419 then () else error "polyminus.sml: Vereinfache 140 d)";
420 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
424 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
426 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
427 ["simplification", "for_polynomials", "with_minus"]))];
429 autoCalculate 1 CompleteCalc;
430 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
431 if p = ([], Res) andalso
432 UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
433 then () else error "polyminus.sml: Vereinfache 139 c)";
437 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
439 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
440 ["simplification", "for_polynomials", "with_minus"]))];
442 autoCalculate 1 CompleteCalc;
443 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
444 if p = ([], Res) andalso
445 UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v"
446 then () else error "polyminus.sml: Vereinfache 139 b)";
450 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
452 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
453 ["simplification", "for_polynomials", "with_minus"]))];
455 autoCalculate 1 CompleteCalc;
456 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
457 if p = ([], Res) andalso
458 UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v"
459 then () else error "polyminus.sml: Vereinfache 138 a)";
461 "----------- met probe fuer_polynom ------------------------------";
462 "----------- met probe fuer_polynom ------------------------------";
463 "----------- met probe fuer_polynom ------------------------------";
465 "Program ProbeScript (e_e::bool) (w_s::bool list) =\
466 \ (let e_e = Take e_e; \
467 \ e_e = Substitute w_s e_e \
468 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
469 \ (Try (Repeat (Calculate ''PLUS''))) #> \
470 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
471 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
474 "----------- pbl polynom probe -----------------------------------";
475 "----------- pbl polynom probe -----------------------------------";
476 "----------- pbl polynom probe -----------------------------------";
478 CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
479 \3 - 2 * e + 2 * f + 2 * (g::int))",
480 "mitWert [e = (1::int), f = (2::int), g = (3::int)]",
482 ("PolyMinus",["polynom", "probe"],
483 ["probe", "fuer_polynom"]))];
485 autoCalculate 1 CompleteCalc;
486 (* autoCalculate 1 CompleteCalcHead;
487 autoCalculate 1 (Steps 1);
488 autoCalculate 1 (Steps 1);
489 val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
490 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
491 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
492 val ((pt,p),_) = get_calc 1;
493 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
494 then () else error "polyminus.sml: Probe 11 = 11";
495 Test_Tool.show_pt pt;
497 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
498 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
499 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
500 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
502 CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
504 ("PolyMinus",["klammer", "polynom", "vereinfachen"],
505 ["simplification", "for_polynomials", "with_parentheses"]))];
507 autoCalculate 1 CompleteCalc;
508 val ((pt,p),_) = get_calc 1;
509 if p = ([], Res) andalso
510 UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
511 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
512 Test_Tool.show_pt pt;
513 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
515 "======= probe p.34 -----";
517 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))",
518 "mitWert [u = (2::int)]",
520 ("PolyMinus",["polynom", "probe"],
521 ["probe", "fuer_polynom"]))];
523 autoCalculate 1 CompleteCalc;
524 val ((pt,p),_) = get_calc 1;
525 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
526 then () else error "polyminus.sml: Probe 29 = 29";
527 Test_Tool.show_pt pt;
529 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
530 "----------- try fun applyTactics --------------------------------";
531 "----------- try fun applyTactics --------------------------------";
532 "----------- try fun applyTactics --------------------------------";
534 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
536 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
537 ["simplification", "for_polynomials", "with_minus"]))];
539 autoCalculate 1 CompleteCalcHead;
540 autoCalculate 1 (Steps 1);
541 autoCalculate 1 (Steps 1);
542 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
544 fetchApplicableTactics 1 0 p;
545 val appltacs = specific_from_prog pt p;
546 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
547 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
549 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
550 val erls = erls_ordne_alphabetisch;
551 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
553 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
554 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
556 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
558 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
560 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
562 rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
563 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
564 Rewrite.trace_on := false; (*true false*)
567 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
568 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
570 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
571 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
573 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
574 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
576 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
577 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
580 (*<CALCMESSAGE> failure </CALCMESSAGE>
581 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
582 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
585 autoCalculate 1 CompleteCalc;
586 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
587 (*independent from failure above: met_simp_poly_minus not confluent:
588 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
589 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
590 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
591 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
594 "#############################################################################";
596 CalcTree [(["Term (- (8 * g) + 10 * g + h)",
598 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
599 ["simplification", "for_polynomials", "with_minus"]))];
601 autoCalculate 1 CompleteCalc;
602 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
603 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
604 then () else error "polyminus.sml: addiere_vor_minus";
607 "#############################################################################";
609 CalcTree [(["Term (- (8 * g) + 10 * g + f)",
611 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
612 ["simplification", "for_polynomials", "with_minus"]))];
614 autoCalculate 1 CompleteCalc;
615 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
616 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
617 then () else error "polyminus.sml: tausche_vor_plus";
619 "----------- pbl binom polynom vereinfachen p.39 -----------------";
620 "----------- pbl binom polynom vereinfachen p.39 -----------------";
621 "----------- pbl binom polynom vereinfachen p.39 -----------------";
623 val rls = klammern_ausmultiplizieren;
624 val t = TermC.str2term "(3 * a + 2) * (4 * a - 1::real)";
625 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
626 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
627 val rls = discard_parentheses;
628 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
629 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
630 val rls = ordne_monome;
631 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
632 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
634 val t = TermC.str2term "3 * a * 4 * a";
635 val rls = ordne_monome;
636 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
638 val rls = klammern_aufloesen;
639 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
640 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";
641 val rls = ordne_alphabetisch;
642 (*TODO: make is_monom more general, a*a=a^2, ...*)
643 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
644 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
646 val rls = fasse_zusammen;
647 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
648 val rls = verschoenere;
649 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
654 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
656 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
657 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
659 autoCalculate 1 CompleteCalc;
660 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
662 UnparseC.term (get_obj g_res pt (fst p)) = "8 * a + 3 * a * 4 * a - 3 * a * 1 - 2";
663 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
664 if p = ([], Res) andalso
665 UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
666 "- 2 + 5 * a + 12 * a \<up> 2"
667 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
668 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
670 "----------- pbl binom polynom vereinfachen: cube ----------------";
671 "----------- pbl binom polynom vereinfachen: cube ----------------";
672 "----------- pbl binom polynom vereinfachen: cube ----------------";
674 CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],
675 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
676 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
678 autoCalculate 1 CompleteCalc;
679 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
680 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
681 then () else error "pbl binom polynom vereinfachen: cube";
683 "----------- Refine.refine Vereinfache ----------------------------------";
684 "----------- Refine.refine Vereinfache ----------------------------------";
685 "----------- Refine.refine Vereinfache ----------------------------------";
686 val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
687 (*default_print_depth 11;*)
688 val matches = Refine.refine fmz ["vereinfachen"];
689 (*default_print_depth 3;*)
691 "----- go into details, if it seems not to work -----";
692 "--- does the predicate evaluate correctly ?";
693 val t = TermC.str2term
694 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
695 val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy;
697 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
698 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
699 | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A";
701 "--- does the respective prls rewrite ?";
702 val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
703 [Eval ("Poly.is_polyexp", eval_is_polyexp ""),
704 Eval ("Prog_Expr.matchsub", eval_matchsub ""),
705 Thm ("or_true",@{thm or_true}),
706 (*"(?a | True) = True"*)
707 Thm ("or_false",@{thm or_false}),
708 (*"(?a | False) = ?a"*)
709 Thm ("not_true", @{thm not_true}),
710 (*"(~ True) = False"*)
711 Thm ("not_false", @{thm not_false})
712 (*"(~ False) = True"*)];
713 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
714 val SOME (t', _) = rewrite_set_ thy false prls t;
715 Rewrite.trace_on := false; (*true false*)
717 "--- does the respective prls rewrite the whole predicate ?";
718 val t = TermC.str2term
719 "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
720 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
721 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
722 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
723 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
724 val SOME (t', _) = rewrite_set_ thy false prls t;
725 Rewrite.trace_on := false; (*true false*)
726 if UnparseC.term t' = "False" then ()
727 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
729 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
730 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
731 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
732 (*see test/../termC.sml for details*)
733 val t = TermC.parse_patt thy "t_t is_polyexp";
734 val t = TermC.parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^
735 " matchsub (?a + (?b - ?c)) t_t | " ^
736 " matchsub (?a - (?b + ?c)) t_t | " ^
737 " matchsub (?a + (?b - ?c)) t_t )");
738 (*show_types := true;
739 if UnparseC.term t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
740 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
741 show_types := false;*)
743 "\<not> (matchsub (?a + (?b + ?c)) t_t \<or>\n " ^
744 "matchsub (?a + (?b - ?c)) t_t \<or>\n " ^
745 "matchsub (?a - (?b + ?c)) t_t \<or> " ^
746 "matchsub (?a + (?b - ?c)) t_t)"
747 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";