1 (* attempts to perserve binary minus as wanted by Austrian teachers
3 (c) due to copyright terms
6 theory PolyMinus imports (*Poly// due to "is_ratpolyexp" in...*) Rational begin
10 (*predicates for conditions in rewriting*)
11 kleiner :: "['a, 'a] => bool" ("_ kleiner _")
12 ist'_monom :: "'a => bool" ("_ ist'_monom")
15 Probe :: "[bool, bool list] => bool"
16 (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
18 (*descriptions for the pbl and met*)
19 Pruefe :: "bool => una"
20 mitWert :: "bool list => tobooll"
21 Geprueft :: "bool => una"
24 ProbeScript :: "[bool, bool list, bool]
26 ("((Script ProbeScript (_ _ =))// (_))" 9)
30 null_minus "0 - a = -a"
31 vor_minus_mal "- a * b = (-a) * b"
33 (*commute with invariant (a.b).c -association*)
34 tausche_plus "[| b ist_monom; a kleiner b |] ==>
36 tausche_minus "[| b ist_monom; a kleiner b |] ==>
38 tausche_vor_plus "[| b ist_monom; a kleiner b |] ==>
40 tausche_vor_minus "[| b ist_monom; a kleiner b |] ==>
42 tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
43 tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
44 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
45 tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
47 (*commute with invariant (a.b).c -association*)
48 tausche_mal "[| b is_atom; a kleiner b |] ==>
50 tausche_vor_mal "[| b is_atom; a kleiner b |] ==>
52 tausche_mal_mal "[| c is_atom; b kleiner c |] ==>
53 (x * c * b) = (x * b * c)"
54 x_quadrat "(x * a) * a = x * a ^^^ 2"
57 subtrahiere "[| l is_const; m is_const |] ==>
58 m * v - l * v = (m - l) * v"
59 subtrahiere_von_1 "[| l is_const |] ==>
60 v - l * v = (1 - l) * v"
61 subtrahiere_1 "[| l is_const; m is_const |] ==>
62 m * v - v = (m - 1) * v"
64 subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==>
65 (x + m * v) - l * v = x + (m - l) * v"
66 subtrahiere_x_plus1_minus "[| l is_const |] ==>
67 (x + v) - l * v = x + (1 - l) * v"
68 subtrahiere_x_plus_minus1 "[| m is_const |] ==>
69 (x + m * v) - v = x + (m - 1) * v"
71 subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==>
72 (x - m * v) + l * v = x + (-m + l) * v"
73 subtrahiere_x_minus1_plus "[| l is_const |] ==>
74 (x - v) + l * v = x + (-1 + l) * v"
75 subtrahiere_x_minus_plus1 "[| m is_const |] ==>
76 (x - m * v) + v = x + (-m + 1) * v"
78 subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==>
79 (x - m * v) - l * v = x + (-m - l) * v"
80 subtrahiere_x_minus1_minus"[| l is_const |] ==>
81 (x - v) - l * v = x + (-1 - l) * v"
82 subtrahiere_x_minus_minus1"[| m is_const |] ==>
83 (x - m * v) - v = x + (-m - 1) * v"
86 addiere_vor_minus "[| l is_const; m is_const |] ==>
87 - (l * v) + m * v = (-l + m) * v"
88 addiere_eins_vor_minus "[| m is_const |] ==>
89 - v + m * v = (-1 + m) * v"
90 subtrahiere_vor_minus "[| l is_const; m is_const |] ==>
91 - (l * v) - m * v = (-l - m) * v"
92 subtrahiere_eins_vor_minus"[| m is_const |] ==>
93 - v - m * v = (-1 - m) * v"
95 vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
96 vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
97 vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
98 vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
100 (*klammer_plus_plus = (real_add_assoc RS sym)*)
101 klammer_plus_minus "a + (b - c) = (a + b) - c"
102 klammer_minus_plus "a - (b + c) = (a - b) - c"
103 klammer_minus_minus "a - (b - c) = (a - b) + c"
105 klammer_mult_minus "a * (b - c) = a * b - a * c"
106 klammer_minus_mult "(b - c) * a = b * a - c * a"
109 (** eval functions **)
111 (*. get the identifier from specific monomials; see fun ist_monom .*)
114 let val s::ss = explode str
115 in implode ((chr (ord s + 1))::ss) end;
116 fun identifier (Free (id,_)) = id (* 2, a *)
117 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
119 | identifier (Const ("op *", _) $ (* 3*a*b *)
121 Free (num, _) $ Free _) $ Free (id, _)) =
122 if is_numeral num then id
124 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
125 if is_numeral base then "|||||||||||||" (* a^2 *)
126 else (*increase*) base
127 | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
128 (Const ("Atools.pow", _) $
129 Free (base, _) $ Free (exp, _))) =
130 if is_numeral num andalso not (is_numeral base) then (*increase*) base
132 | identifier _ = "|||||||||||||"(*the "largest" string*);
134 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
135 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
136 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
138 if is_num a then (*123 kleiner 32 = True !!!*)
139 if int_of_Free a < int_of_Free b then
140 SOME ((term2str p) ^ " = True",
141 Trueprop $ (mk_equality (p, HOLogic.true_const)))
142 else SOME ((term2str p) ^ " = False",
143 Trueprop $ (mk_equality (p, HOLogic.false_const)))
144 else (* -1 * -2 kleiner 0 *)
145 SOME ((term2str p) ^ " = False",
146 Trueprop $ (mk_equality (p, HOLogic.false_const)))
148 if identifier a < identifier b then
149 SOME ((term2str p) ^ " = True",
150 Trueprop $ (mk_equality (p, HOLogic.true_const)))
151 else SOME ((term2str p) ^ " = False",
152 Trueprop $ (mk_equality (p, HOLogic.false_const)))
153 | eval_kleiner _ _ _ _ = NONE;
155 fun ist_monom (Free (id,_)) = true
156 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
157 if is_numeral num then true else false
158 | ist_monom _ = false;
159 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
160 fun ist_monom (Free (id,_)) = true (* 2, a *)
161 | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
162 if is_numeral id then false else true
163 | ist_monom (Const ("op *", _) $ (* 3*a*b *)
165 Free (num, _) $ Free _) $ Free (id, _)) =
166 if is_numeral num andalso not (is_numeral id) then true else false
167 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
169 | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
170 (Const ("Atools.pow", _) $
171 Free (base, _) $ Free (exp, _))) =
172 if is_numeral num then true else false
173 | ist_monom _ = false;
175 (* is this a univariate monomial ? *)
176 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
177 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
179 SOME ((term2str p) ^ " = True",
180 Trueprop $ (mk_equality (p, HOLogic.true_const)))
181 else SOME ((term2str p) ^ " = False",
182 Trueprop $ (mk_equality (p, HOLogic.false_const)))
183 | eval_ist_monom _ _ _ _ = NONE;
186 (** rewrite order **)
190 val erls_ordne_alphabetisch =
191 append_rls "erls_ordne_alphabetisch" e_rls
192 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
193 Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
196 val ordne_alphabetisch =
197 Rls{id = "ordne_alphabetisch", preconds = [],
198 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
199 erls = erls_ordne_alphabetisch,
200 rules = [Thm ("tausche_plus",num_str tausche_plus),
201 (*"b kleiner a ==> (b + a) = (a + b)"*)
202 Thm ("tausche_minus",num_str tausche_minus),
203 (*"b kleiner a ==> (b - a) = (-a + b)"*)
204 Thm ("tausche_vor_plus",num_str tausche_vor_plus),
205 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
206 Thm ("tausche_vor_minus",num_str tausche_vor_minus),
207 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
208 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
209 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
210 Thm ("tausche_plus_minus",num_str tausche_plus_minus),
211 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
212 Thm ("tausche_minus_plus",num_str tausche_minus_plus),
213 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
214 Thm ("tausche_minus_minus",num_str tausche_minus_minus)
215 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
216 ], scr = EmptyScr}:rls;
219 Rls{id = "fasse_zusammen", preconds = [],
220 rew_ord = ("dummy_ord", dummy_ord),
221 erls = append_rls "erls_fasse_zusammen" e_rls
222 [Calc ("Atools.is'_const",eval_const "#is_const_")],
223 srls = Erls, calc = [],
225 [Thm ("real_num_collect",num_str real_num_collect),
226 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
227 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
228 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
229 Thm ("real_one_collect",num_str real_one_collect),
230 (*"m is_const ==> n + m * n = (1 + m) * n"*)
231 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
232 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
235 Thm ("subtrahiere",num_str subtrahiere),
236 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
237 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
238 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
239 Thm ("subtrahiere_1",num_str subtrahiere_1),
240 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
242 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
243 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
244 Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
245 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
246 Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
247 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
249 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
250 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
251 Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
252 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
253 Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
254 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
256 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
257 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
258 Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
259 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
260 Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
261 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
263 Calc ("op +", eval_binop "#add_"),
264 Calc ("op -", eval_binop "#subtr_"),
266 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
267 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
268 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
269 (*"(k + z1) + z1 = k + 2 * z1"*)
270 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
271 (*"z1 + z1 = 2 * z1"*)
273 Thm ("addiere_vor_minus",num_str addiere_vor_minus),
274 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
275 Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
276 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
277 Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
278 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
279 Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
280 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
282 ], scr = EmptyScr}:rls;
285 Rls{id = "verschoenere", preconds = [],
286 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
287 erls = append_rls "erls_verschoenere" e_rls
288 [Calc ("PolyMinus.kleiner", eval_kleiner "")],
289 rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
290 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
291 Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
292 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
293 Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
294 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
295 Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
296 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
298 Calc ("op *", eval_binop "#mult_"),
300 Thm ("real_mult_0",num_str real_mult_0),
302 Thm ("real_mult_1",num_str real_mult_1),
304 Thm ("real_add_zero_left",num_str real_add_zero_left),
306 Thm ("null_minus",num_str null_minus),
308 Thm ("vor_minus_mal",num_str vor_minus_mal)
309 (*"- a * b = (-a) * b"*)
311 (*Thm ("",num_str ),*)
313 ], scr = EmptyScr}:rls (*end verschoenere*);
315 val klammern_aufloesen =
316 Rls{id = "klammern_aufloesen", preconds = [],
317 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
318 rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
319 (*"a + (b + c) = (a + b) + c"*)
320 Thm ("klammer_plus_minus",num_str klammer_plus_minus),
321 (*"a + (b - c) = (a + b) - c"*)
322 Thm ("klammer_minus_plus",num_str klammer_minus_plus),
323 (*"a - (b + c) = (a - b) - c"*)
324 Thm ("klammer_minus_minus",num_str klammer_minus_minus)
325 (*"a - (b - c) = (a - b) + c"*)
326 ], scr = EmptyScr}:rls;
328 val klammern_ausmultiplizieren =
329 Rls{id = "klammern_ausmultiplizieren", preconds = [],
330 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
331 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
332 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
333 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
334 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
336 Thm ("klammer_mult_minus",num_str klammer_mult_minus),
337 (*"a * (b - c) = a * b - a * c"*)
338 Thm ("klammer_minus_mult",num_str klammer_minus_mult)
339 (*"(b - c) * a = b * a - c * a"*)
343 ], scr = EmptyScr}:rls;
346 Rls{id = "ordne_monome", preconds = [],
347 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
348 erls = append_rls "erls_ordne_monome" e_rls
349 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
350 Calc ("Atools.is'_atom", eval_is_atom "")
352 rules = [Thm ("tausche_mal",num_str tausche_mal),
353 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
354 Thm ("tausche_vor_mal",num_str tausche_vor_mal),
355 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
356 Thm ("tausche_mal_mal",num_str tausche_mal_mal),
357 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
358 Thm ("x_quadrat",num_str x_quadrat)
359 (*"(x * a) * a = x * a ^^^ 2"*)
363 ], scr = EmptyScr}:rls;
367 append_rls "rls_p_33" e_rls
368 [Rls_ ordne_alphabetisch,
373 append_rls "rls_p_34" e_rls
374 [Rls_ klammern_aufloesen,
375 Rls_ ordne_alphabetisch,
380 append_rls "rechnen" e_rls
381 [Calc ("op *", eval_binop "#mult_"),
382 Calc ("op +", eval_binop "#add_"),
383 Calc ("op -", eval_binop "#subtr_")
387 overwritelthy thy (!ruleset',
388 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
389 ("fasse_zusammen", prep_rls fasse_zusammen),
390 ("verschoenere", prep_rls verschoenere),
391 ("ordne_monome", prep_rls ordne_monome),
392 ("klammern_aufloesen", prep_rls klammern_aufloesen),
393 ("klammern_ausmultiplizieren",
394 prep_rls klammern_ausmultiplizieren)
400 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
401 (["polynom","vereinfachen"],
402 [], Erls, NONE, []));
405 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
406 (["plus_minus","polynom","vereinfachen"],
407 [("#Given" ,["term t_"]),
408 ("#Where" ,["t_ is_polyexp",
409 "Not (matchsub (?a + (?b + ?c)) t_ | " ^
410 " matchsub (?a + (?b - ?c)) t_ | " ^
411 " matchsub (?a - (?b + ?c)) t_ | " ^
412 " matchsub (?a + (?b - ?c)) t_ )",
413 "Not (matchsub (?a * (?b + ?c)) t_ | " ^
414 " matchsub (?a * (?b - ?c)) t_ | " ^
415 " matchsub ((?b + ?c) * ?a) t_ | " ^
416 " matchsub ((?b - ?c) * ?a) t_ )"]),
417 ("#Find" ,["normalform n_"])
419 append_rls "prls_pbl_vereinf_poly" e_rls
420 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
421 Calc ("Tools.matchsub", eval_matchsub ""),
422 Thm ("or_true",or_true),
423 (*"(?a | True) = True"*)
424 Thm ("or_false",or_false),
425 (*"(?a | False) = ?a"*)
426 Thm ("not_true",num_str not_true),
427 (*"(~ True) = False"*)
428 Thm ("not_false",num_str not_false)
429 (*"(~ False) = True"*)],
430 SOME "Vereinfache t_",
431 [["simplification","for_polynomials","with_minus"]]));
434 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
435 (["klammer","polynom","vereinfachen"],
436 [("#Given" ,["term t_"]),
437 ("#Where" ,["t_ is_polyexp",
438 "Not (matchsub (?a * (?b + ?c)) t_ | " ^
439 " matchsub (?a * (?b - ?c)) t_ | " ^
440 " matchsub ((?b + ?c) * ?a) t_ | " ^
441 " matchsub ((?b - ?c) * ?a) t_ )"]),
442 ("#Find" ,["normalform n_"])
444 append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
445 Calc ("Tools.matchsub", eval_matchsub ""),
446 Thm ("or_true",or_true),
447 (*"(?a | True) = True"*)
448 Thm ("or_false",or_false),
449 (*"(?a | False) = ?a"*)
450 Thm ("not_true",num_str not_true),
451 (*"(~ True) = False"*)
452 Thm ("not_false",num_str not_false)
453 (*"(~ False) = True"*)],
454 SOME "Vereinfache t_",
455 [["simplification","for_polynomials","with_parentheses"]]));
458 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
459 (["binom_klammer","polynom","vereinfachen"],
460 [("#Given" ,["term t_"]),
461 ("#Where" ,["t_ is_polyexp"]),
462 ("#Find" ,["normalform n_"])
464 append_rls "e_rls" e_rls [(*for preds in where_*)
465 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
466 SOME "Vereinfache t_",
467 [["simplification","for_polynomials","with_parentheses_mult"]]));
470 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
472 [], Erls, NONE, []));
475 (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
476 (["polynom","probe"],
477 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
478 ("#Where" ,["e_ is_polyexp"]),
479 ("#Find" ,["Geprueft p_"])
481 append_rls "prls_pbl_probe_poly"
482 e_rls [(*for preds in where_*)
483 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
485 [["probe","fuer_polynom"]]));
488 (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
490 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
491 ("#Where" ,["e_ is_ratpolyexp"]),
492 ("#Find" ,["Geprueft p_"])
494 append_rls "prls_pbl_probe_bruch"
495 e_rls [(*for preds in where_*)
496 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
498 [["probe","fuer_bruch"]]));
504 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
505 (["simplification","for_polynomials","with_minus"],
506 [("#Given" ,["term t_"]),
507 ("#Where" ,["t_ is_polyexp",
508 "Not (matchsub (?a + (?b + ?c)) t_ | " ^
509 " matchsub (?a + (?b - ?c)) t_ | " ^
510 " matchsub (?a - (?b + ?c)) t_ | " ^
511 " matchsub (?a + (?b - ?c)) t_ )"]),
512 ("#Find" ,["normalform n_"])
514 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
515 prls = append_rls "prls_met_simp_poly_minus" e_rls
516 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
517 Calc ("Tools.matchsub", eval_matchsub ""),
518 Thm ("and_true",and_true),
519 (*"(?a & True) = ?a"*)
520 Thm ("and_false",and_false),
521 (*"(?a & False) = False"*)
522 Thm ("not_true",num_str not_true),
523 (*"(~ True) = False"*)
524 Thm ("not_false",num_str not_false)
525 (*"(~ False) = True"*)],
526 crls = e_rls, nrls = rls_p_33},
527 "Script SimplifyScript (t_::real) = " ^
528 " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
529 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
530 " (Try (Rewrite_Set verschoenere False)))) t_)"
534 (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
535 (["simplification","for_polynomials","with_parentheses"],
536 [("#Given" ,["term t_"]),
537 ("#Where" ,["t_ is_polyexp"]),
538 ("#Find" ,["normalform n_"])
540 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
541 prls = append_rls "simplification_for_polynomials_prls" e_rls
542 [(*for preds in where_*)
543 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
544 crls = e_rls, nrls = rls_p_34},
545 "Script SimplifyScript (t_::real) = " ^
546 " ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
547 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
548 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
549 " (Try (Rewrite_Set verschoenere False)))) t_)"
553 (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
554 (["simplification","for_polynomials","with_parentheses_mult"],
555 [("#Given" ,["term t_"]),
556 ("#Where" ,["t_ is_polyexp"]),
557 ("#Find" ,["normalform n_"])
559 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
560 prls = append_rls "simplification_for_polynomials_prls" e_rls
561 [(*for preds in where_*)
562 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
563 crls = e_rls, nrls = rls_p_34},
564 "Script SimplifyScript (t_::real) = " ^
565 " ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
566 " (Try (Rewrite_Set discard_parentheses False)) @@ " ^
567 " (Try (Rewrite_Set ordne_monome False)) @@ " ^
568 " (Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
569 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
570 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
571 " (Try (Rewrite_Set verschoenere False)))) t_)"
575 (prep_met PolyMinus.thy "met_probe" [] e_metID
578 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
579 prls = Erls, crls = e_rls, nrls = Erls},
583 (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
584 (["probe","fuer_polynom"],
585 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
586 ("#Where" ,["e_ is_polyexp"]),
587 ("#Find" ,["Geprueft p_"])
589 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
590 prls = append_rls "prls_met_probe_bruch"
591 e_rls [(*for preds in where_*)
592 Calc ("Rational.is'_ratpolyexp",
593 eval_is_ratpolyexp "")],
594 crls = e_rls, nrls = rechnen},
595 "Script ProbeScript (e_::bool) (ws_::bool list) = " ^
596 " (let e_ = Take e_; " ^
597 " e_ = Substitute ws_ e_ " ^
598 " in (Repeat((Try (Repeat (Calculate times))) @@ " ^
599 " (Try (Repeat (Calculate plus ))) @@ " ^
600 " (Try (Repeat (Calculate minus))))) e_)"
604 (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
605 (["probe","fuer_bruch"],
606 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
607 ("#Where" ,["e_ is_ratpolyexp"]),
608 ("#Find" ,["Geprueft p_"])
610 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
611 prls = append_rls "prls_met_probe_bruch"
612 e_rls [(*for preds in where_*)
613 Calc ("Rational.is'_ratpolyexp",
614 eval_is_ratpolyexp "")],
615 crls = e_rls, nrls = Erls},