1 (* questionable attempts to perserve binary minus as wanted by teachers
3 (c) due to copyright terms
5 use_thy"Knowledge/PolyMinus";
7 use_thy"Knowledge/Isac";
8 use"Knowledge/PolyMinus.ML";
11 (** interface isabelle -- isac **)
12 theory' := overwritel (!theory', [("PolyMinus.thy",PolyMinus.thy)]);
14 (** eval functions **)
16 (*. get the identifier from specific monomials; see fun ist_monom .*)
19 let val s::ss = explode str
20 in implode ((chr (ord s + 1))::ss) end;
21 fun identifier (Free (id,_)) = id (* 2, a *)
22 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
24 | identifier (Const ("op *", _) $ (* 3*a*b *)
26 Free (num, _) $ Free _) $ Free (id, _)) =
27 if is_numeral num then id
29 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
30 if is_numeral base then "|||||||||||||" (* a^2 *)
31 else (*increase*) base
32 | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
33 (Const ("Atools.pow", _) $
34 Free (base, _) $ Free (exp, _))) =
35 if is_numeral num andalso not (is_numeral base) then (*increase*) base
37 | identifier _ = "|||||||||||||"(*the "largest" string*);
39 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
40 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
41 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
43 if is_num a then (*123 kleiner 32 = True !!!*)
44 if int_of_Free a < int_of_Free b then
45 SOME ((term2str p) ^ " = True",
46 Trueprop $ (mk_equality (p, HOLogic.true_const)))
47 else SOME ((term2str p) ^ " = False",
48 Trueprop $ (mk_equality (p, HOLogic.false_const)))
49 else (* -1 * -2 kleiner 0 *)
50 SOME ((term2str p) ^ " = False",
51 Trueprop $ (mk_equality (p, HOLogic.false_const)))
53 if identifier a < identifier b then
54 SOME ((term2str p) ^ " = True",
55 Trueprop $ (mk_equality (p, HOLogic.true_const)))
56 else SOME ((term2str p) ^ " = False",
57 Trueprop $ (mk_equality (p, HOLogic.false_const)))
58 | eval_kleiner _ _ _ _ = NONE;
60 fun ist_monom (Free (id,_)) = true
61 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
62 if is_numeral num then true else false
63 | ist_monom _ = false;
64 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
65 fun ist_monom (Free (id,_)) = true (* 2, a *)
66 | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
67 if is_numeral id then false else true
68 | ist_monom (Const ("op *", _) $ (* 3*a*b *)
70 Free (num, _) $ Free _) $ Free (id, _)) =
71 if is_numeral num andalso not (is_numeral id) then true else false
72 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
74 | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
75 (Const ("Atools.pow", _) $
76 Free (base, _) $ Free (exp, _))) =
77 if is_numeral num then true else false
78 | ist_monom _ = false;
80 (* is this a univariate monomial ? *)
81 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
82 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
84 SOME ((term2str p) ^ " = True",
85 Trueprop $ (mk_equality (p, HOLogic.true_const)))
86 else SOME ((term2str p) ^ " = False",
87 Trueprop $ (mk_equality (p, HOLogic.false_const)))
88 | eval_ist_monom _ _ _ _ = NONE;
95 val erls_ordne_alphabetisch =
96 append_rls "erls_ordne_alphabetisch" e_rls
97 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
98 Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
101 val ordne_alphabetisch =
102 Rls{id = "ordne_alphabetisch", preconds = [],
103 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
104 erls = erls_ordne_alphabetisch,
105 rules = [Thm ("tausche_plus",num_str tausche_plus),
106 (*"b kleiner a ==> (b + a) = (a + b)"*)
107 Thm ("tausche_minus",num_str tausche_minus),
108 (*"b kleiner a ==> (b - a) = (-a + b)"*)
109 Thm ("tausche_vor_plus",num_str tausche_vor_plus),
110 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
111 Thm ("tausche_vor_minus",num_str tausche_vor_minus),
112 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
113 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
114 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
115 Thm ("tausche_plus_minus",num_str tausche_plus_minus),
116 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
117 Thm ("tausche_minus_plus",num_str tausche_minus_plus),
118 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
119 Thm ("tausche_minus_minus",num_str tausche_minus_minus)
120 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
121 ], scr = EmptyScr}:rls;
124 Rls{id = "fasse_zusammen", preconds = [],
125 rew_ord = ("dummy_ord", dummy_ord),
126 erls = append_rls "erls_fasse_zusammen" e_rls
127 [Calc ("Atools.is'_const",eval_const "#is_const_")],
128 srls = Erls, calc = [],
130 [Thm ("real_num_collect",num_str real_num_collect),
131 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
132 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
133 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
134 Thm ("real_one_collect",num_str real_one_collect),
135 (*"m is_const ==> n + m * n = (1 + m) * n"*)
136 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
137 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
140 Thm ("subtrahiere",num_str subtrahiere),
141 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
142 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
143 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
144 Thm ("subtrahiere_1",num_str subtrahiere_1),
145 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
147 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
148 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
149 Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
150 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
151 Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
152 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
154 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
155 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
156 Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
157 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
158 Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
159 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
161 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
162 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
163 Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
164 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
165 Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
166 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
168 Calc ("op +", eval_binop "#add_"),
169 Calc ("op -", eval_binop "#subtr_"),
171 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
172 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
173 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
174 (*"(k + z1) + z1 = k + 2 * z1"*)
175 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
176 (*"z1 + z1 = 2 * z1"*)
178 Thm ("addiere_vor_minus",num_str addiere_vor_minus),
179 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
180 Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
181 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
182 Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
183 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
184 Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
185 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
187 ], scr = EmptyScr}:rls;
190 Rls{id = "verschoenere", preconds = [],
191 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
192 erls = append_rls "erls_verschoenere" e_rls
193 [Calc ("PolyMinus.kleiner", eval_kleiner "")],
194 rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
195 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
196 Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
197 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
198 Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
199 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
200 Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
201 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
203 Calc ("op *", eval_binop "#mult_"),
205 Thm ("real_mult_0",num_str real_mult_0),
207 Thm ("real_mult_1",num_str real_mult_1),
209 Thm ("real_add_zero_left",num_str real_add_zero_left),
211 Thm ("null_minus",num_str null_minus),
213 Thm ("vor_minus_mal",num_str vor_minus_mal)
214 (*"- a * b = (-a) * b"*)
216 (*Thm ("",num_str ),*)
218 ], scr = EmptyScr}:rls (*end verschoenere*);
220 val klammern_aufloesen =
221 Rls{id = "klammern_aufloesen", preconds = [],
222 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
223 rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
224 (*"a + (b + c) = (a + b) + c"*)
225 Thm ("klammer_plus_minus",num_str klammer_plus_minus),
226 (*"a + (b - c) = (a + b) - c"*)
227 Thm ("klammer_minus_plus",num_str klammer_minus_plus),
228 (*"a - (b + c) = (a - b) - c"*)
229 Thm ("klammer_minus_minus",num_str klammer_minus_minus)
230 (*"a - (b - c) = (a - b) + c"*)
231 ], scr = EmptyScr}:rls;
233 val klammern_ausmultiplizieren =
234 Rls{id = "klammern_ausmultiplizieren", preconds = [],
235 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
236 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
237 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
238 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
239 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
241 Thm ("klammer_mult_minus",num_str klammer_mult_minus),
242 (*"a * (b - c) = a * b - a * c"*)
243 Thm ("klammer_minus_mult",num_str klammer_minus_mult)
244 (*"(b - c) * a = b * a - c * a"*)
248 ], scr = EmptyScr}:rls;
251 Rls{id = "ordne_monome", preconds = [],
252 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
253 erls = append_rls "erls_ordne_monome" e_rls
254 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
255 Calc ("Atools.is'_atom", eval_is_atom "")
257 rules = [Thm ("tausche_mal",num_str tausche_mal),
258 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
259 Thm ("tausche_vor_mal",num_str tausche_vor_mal),
260 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
261 Thm ("tausche_mal_mal",num_str tausche_mal_mal),
262 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
263 Thm ("x_quadrat",num_str x_quadrat)
264 (*"(x * a) * a = x * a ^^^ 2"*)
268 ], scr = EmptyScr}:rls;
272 append_rls "rls_p_33" e_rls
273 [Rls_ ordne_alphabetisch,
278 append_rls "rls_p_34" e_rls
279 [Rls_ klammern_aufloesen,
280 Rls_ ordne_alphabetisch,
285 append_rls "rechnen" e_rls
286 [Calc ("op *", eval_binop "#mult_"),
287 Calc ("op +", eval_binop "#add_"),
288 Calc ("op -", eval_binop "#subtr_")
292 overwritelthy thy (!ruleset',
293 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
294 ("fasse_zusammen", prep_rls fasse_zusammen),
295 ("verschoenere", prep_rls verschoenere),
296 ("ordne_monome", prep_rls ordne_monome),
297 ("klammern_aufloesen", prep_rls klammern_aufloesen),
298 ("klammern_ausmultiplizieren",
299 prep_rls klammern_ausmultiplizieren)
305 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
306 (["polynom","vereinfachen"],
307 [], Erls, NONE, []));
310 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
311 (["plus_minus","polynom","vereinfachen"],
312 [("#Given" ,["term t_"]),
313 ("#Where" ,["t_ is_polyexp",
314 "Not (matchsub (?a + (?b + ?c)) t_ | \
315 \ matchsub (?a + (?b - ?c)) t_ | \
316 \ matchsub (?a - (?b + ?c)) t_ | \
317 \ matchsub (?a + (?b - ?c)) t_ )",
318 "Not (matchsub (?a * (?b + ?c)) t_ | \
319 \ matchsub (?a * (?b - ?c)) t_ | \
320 \ matchsub ((?b + ?c) * ?a) t_ | \
321 \ matchsub ((?b - ?c) * ?a) t_ )"]),
322 ("#Find" ,["normalform n_"])
324 append_rls "prls_pbl_vereinf_poly" e_rls
325 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
326 Calc ("Tools.matchsub", eval_matchsub ""),
327 Thm ("or_true",or_true),
328 (*"(?a | True) = True"*)
329 Thm ("or_false",or_false),
330 (*"(?a | False) = ?a"*)
331 Thm ("not_true",num_str not_true),
332 (*"(~ True) = False"*)
333 Thm ("not_false",num_str not_false)
334 (*"(~ False) = True"*)],
335 SOME "Vereinfache t_",
336 [["simplification","for_polynomials","with_minus"]]));
339 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
340 (["klammer","polynom","vereinfachen"],
341 [("#Given" ,["term t_"]),
342 ("#Where" ,["t_ is_polyexp",
343 "Not (matchsub (?a * (?b + ?c)) t_ | \
344 \ matchsub (?a * (?b - ?c)) t_ | \
345 \ matchsub ((?b + ?c) * ?a) t_ | \
346 \ matchsub ((?b - ?c) * ?a) t_ )"]),
347 ("#Find" ,["normalform n_"])
349 append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
350 Calc ("Tools.matchsub", eval_matchsub ""),
351 Thm ("or_true",or_true),
352 (*"(?a | True) = True"*)
353 Thm ("or_false",or_false),
354 (*"(?a | False) = ?a"*)
355 Thm ("not_true",num_str not_true),
356 (*"(~ True) = False"*)
357 Thm ("not_false",num_str not_false)
358 (*"(~ False) = True"*)],
359 SOME "Vereinfache t_",
360 [["simplification","for_polynomials","with_parentheses"]]));
363 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
364 (["binom_klammer","polynom","vereinfachen"],
365 [("#Given" ,["term t_"]),
366 ("#Where" ,["t_ is_polyexp"]),
367 ("#Find" ,["normalform n_"])
369 append_rls "e_rls" e_rls [(*for preds in where_*)
370 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
371 SOME "Vereinfache t_",
372 [["simplification","for_polynomials","with_parentheses_mult"]]));
375 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
377 [], Erls, NONE, []));
380 (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
381 (["polynom","probe"],
382 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
383 ("#Where" ,["e_ is_polyexp"]),
384 ("#Find" ,["Geprueft p_"])
386 append_rls "prls_pbl_probe_poly"
387 e_rls [(*for preds in where_*)
388 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
390 [["probe","fuer_polynom"]]));
393 (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
395 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
396 ("#Where" ,["e_ is_ratpolyexp"]),
397 ("#Find" ,["Geprueft p_"])
399 append_rls "prls_pbl_probe_bruch"
400 e_rls [(*for preds in where_*)
401 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
403 [["probe","fuer_bruch"]]));
409 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
410 (["simplification","for_polynomials","with_minus"],
411 [("#Given" ,["term t_"]),
412 ("#Where" ,["t_ is_polyexp",
413 "Not (matchsub (?a + (?b + ?c)) t_ | \
414 \ matchsub (?a + (?b - ?c)) t_ | \
415 \ matchsub (?a - (?b + ?c)) t_ | \
416 \ matchsub (?a + (?b - ?c)) t_ )"]),
417 ("#Find" ,["normalform n_"])
419 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
420 prls = append_rls "prls_met_simp_poly_minus" e_rls
421 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
422 Calc ("Tools.matchsub", eval_matchsub ""),
423 Thm ("and_true",and_true),
424 (*"(?a & True) = ?a"*)
425 Thm ("and_false",and_false),
426 (*"(?a & False) = False"*)
427 Thm ("not_true",num_str not_true),
428 (*"(~ True) = False"*)
429 Thm ("not_false",num_str not_false)
430 (*"(~ False) = True"*)],
431 crls = e_rls, nrls = rls_p_33},
432 "Script SimplifyScript (t_::real) = \
433 \ ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
434 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
435 \ (Try (Rewrite_Set verschoenere False)))) t_)"
439 (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
440 (["simplification","for_polynomials","with_parentheses"],
441 [("#Given" ,["term t_"]),
442 ("#Where" ,["t_ is_polyexp"]),
443 ("#Find" ,["normalform n_"])
445 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
446 prls = append_rls "simplification_for_polynomials_prls" e_rls
447 [(*for preds in where_*)
448 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
449 crls = e_rls, nrls = rls_p_34},
450 "Script SimplifyScript (t_::real) = \
451 \ ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ \
452 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
453 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
454 \ (Try (Rewrite_Set verschoenere False)))) t_)"
458 (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
459 (["simplification","for_polynomials","with_parentheses_mult"],
460 [("#Given" ,["term t_"]),
461 ("#Where" ,["t_ is_polyexp"]),
462 ("#Find" ,["normalform n_"])
464 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
465 prls = append_rls "simplification_for_polynomials_prls" e_rls
466 [(*for preds in where_*)
467 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
468 crls = e_rls, nrls = rls_p_34},
469 "Script SimplifyScript (t_::real) = \
470 \ ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
471 \ (Try (Rewrite_Set discard_parentheses False)) @@ \
472 \ (Try (Rewrite_Set ordne_monome False)) @@ \
473 \ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
474 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
475 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
476 \ (Try (Rewrite_Set verschoenere False)))) t_)"
480 (prep_met PolyMinus.thy "met_probe" [] e_metID
483 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
484 prls = Erls, crls = e_rls, nrls = Erls},
488 (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
489 (["probe","fuer_polynom"],
490 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
491 ("#Where" ,["e_ is_polyexp"]),
492 ("#Find" ,["Geprueft p_"])
494 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
495 prls = append_rls "prls_met_probe_bruch"
496 e_rls [(*for preds in where_*)
497 Calc ("Rational.is'_ratpolyexp",
498 eval_is_ratpolyexp "")],
499 crls = e_rls, nrls = rechnen},
500 "Script ProbeScript (e_::bool) (ws_::bool list) = \
501 \ (let e_ = Take e_; \
502 \ e_ = Substitute ws_ e_ \
503 \ in (Repeat((Try (Repeat (Calculate times))) @@ \
504 \ (Try (Repeat (Calculate plus ))) @@ \
505 \ (Try (Repeat (Calculate minus))))) e_)"
509 (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
510 (["probe","fuer_bruch"],
511 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
512 ("#Where" ,["e_ is_ratpolyexp"]),
513 ("#Find" ,["Geprueft p_"])
515 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
516 prls = append_rls "prls_met_probe_bruch"
517 e_rls [(*for preds in where_*)
518 Calc ("Rational.is'_ratpolyexp",
519 eval_is_ratpolyexp "")],
520 crls = e_rls, nrls = Erls},