cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
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" and
31 vor_minus_mal: "- a * b = (-a) * b" and
33 (*commute with invariant (a.b).c -association*)
34 tausche_plus: "[| b ist_monom; a kleiner b |] ==>
35 (b + a) = (a + b)" and
36 tausche_minus: "[| b ist_monom; a kleiner b |] ==>
37 (b - a) = (-a + b)" and
38 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
39 (- b + a) = (a - b)" and
40 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
41 (- b - a) = (-a - b)" and
42 tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
43 tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
44 tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
45 tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
47 (*commute with invariant (a.b).c -association*)
48 tausche_mal: "[| b is_atom; a kleiner b |] ==>
49 (b * a) = (a * b)" and
50 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
51 (-b * a) = (-a * b)" and
52 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
53 (x * c * b) = (x * b * c)" and
54 x_quadrat: "(x * a) * a = x * a ^^^ 2" and
57 subtrahiere: "[| l is_const; m is_const |] ==>
58 m * v - l * v = (m - l) * v" and
59 subtrahiere_von_1: "[| l is_const |] ==>
60 v - l * v = (1 - l) * v" and
61 subtrahiere_1: "[| l is_const; m is_const |] ==>
62 m * v - v = (m - 1) * v" and
64 subtrahiere_x_plus_minus: "[| l is_const; m is_const |] ==>
65 (x + m * v) - l * v = x + (m - l) * v" and
66 subtrahiere_x_plus1_minus: "[| l is_const |] ==>
67 (x + v) - l * v = x + (1 - l) * v" and
68 subtrahiere_x_plus_minus1: "[| m is_const |] ==>
69 (x + m * v) - v = x + (m - 1) * v" and
71 subtrahiere_x_minus_plus: "[| l is_const; m is_const |] ==>
72 (x - m * v) + l * v = x + (-m + l) * v" and
73 subtrahiere_x_minus1_plus: "[| l is_const |] ==>
74 (x - v) + l * v = x + (-1 + l) * v" and
75 subtrahiere_x_minus_plus1: "[| m is_const |] ==>
76 (x - m * v) + v = x + (-m + 1) * v" and
78 subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>
79 (x - m * v) - l * v = x + (-m - l) * v" and
80 subtrahiere_x_minus1_minus:"[| l is_const |] ==>
81 (x - v) - l * v = x + (-1 - l) * v" and
82 subtrahiere_x_minus_minus1:"[| m is_const |] ==>
83 (x - m * v) - v = x + (-m - 1) * v" and
86 addiere_vor_minus: "[| l is_const; m is_const |] ==>
87 - (l * v) + m * v = (-l + m) * v" and
88 addiere_eins_vor_minus: "[| m is_const |] ==>
89 - v + m * v = (-1 + m) * v" and
90 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==>
91 - (l * v) - m * v = (-l - m) * v" and
92 subtrahiere_eins_vor_minus:"[| m is_const |] ==>
93 - v - m * v = (-1 - m) * v" and
95 vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
96 vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
97 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
98 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
100 (*klammer_plus_plus = (add_assoc RS sym)*)
101 klammer_plus_minus: "a + (b - c) = (a + b) - c" and
102 klammer_minus_plus: "a - (b + c) = (a - b) - c" and
103 klammer_minus_minus: "a - (b - c) = (a - b) + c" and
105 klammer_mult_minus: "a * (b - c) = a * b - a * c" and
106 klammer_minus_mult: "(b - c) * a = b * a - c * a"
111 (** eval functions **)
113 (*. get the identifier from specific monomials; see fun ist_monom .*)
116 let val s::ss = Symbol.explode str
117 in implode ((chr (ord s + 1))::ss) end;
118 fun identifier (Free (id,_)) = id (* 2, a *)
119 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
121 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
122 (Const ("Groups.times_class.times", _) $
123 Free (num, _) $ Free _) $ Free (id, _)) =
124 if is_numeral num then id
126 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
127 if is_numeral base then "|||||||||||||" (* a^2 *)
128 else (*increase*) base
129 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
130 (Const ("Atools.pow", _) $
131 Free (base, _) $ Free (exp, _))) =
132 if is_numeral num andalso not (is_numeral base) then (*increase*) base
134 | identifier _ = "|||||||||||||"(*the "largest" string*);
136 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
137 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
138 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
140 if is_num a then (*123 kleiner 32 = True !!!*)
141 if int_of_Free a < int_of_Free b then
142 SOME ((term2str p) ^ " = True",
143 Trueprop $ (mk_equality (p, @{term True})))
144 else SOME ((term2str p) ^ " = False",
145 Trueprop $ (mk_equality (p, @{term False})))
146 else (* -1 * -2 kleiner 0 *)
147 SOME ((term2str p) ^ " = False",
148 Trueprop $ (mk_equality (p, @{term False})))
150 if identifier a < identifier b then
151 SOME ((term2str p) ^ " = True",
152 Trueprop $ (mk_equality (p, @{term True})))
153 else SOME ((term2str p) ^ " = False",
154 Trueprop $ (mk_equality (p, @{term False})))
155 | eval_kleiner _ _ _ _ = NONE;
157 fun ist_monom (Free (id,_)) = true
158 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
159 if is_numeral num then true else false
160 | ist_monom _ = false;
161 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
162 fun ist_monom (Free (id,_)) = true (* 2, a *)
163 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
164 if is_numeral id then false else true
165 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
166 (Const ("Groups.times_class.times", _) $
167 Free (num, _) $ Free _) $ Free (id, _)) =
168 if is_numeral num andalso not (is_numeral id) then true else false
169 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
171 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
172 (Const ("Atools.pow", _) $
173 Free (base, _) $ Free (exp, _))) =
174 if is_numeral num then true else false
175 | ist_monom _ = false;
177 (* is this a univariate monomial ? *)
178 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
179 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
181 SOME ((term2str p) ^ " = True",
182 Trueprop $ (mk_equality (p, @{term True})))
183 else SOME ((term2str p) ^ " = False",
184 Trueprop $ (mk_equality (p, @{term False})))
185 | eval_ist_monom _ _ _ _ = NONE;
188 (** rewrite order **)
192 val erls_ordne_alphabetisch =
193 append_rls "erls_ordne_alphabetisch" e_rls
194 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
195 Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
198 val ordne_alphabetisch =
199 Rls{id = "ordne_alphabetisch", preconds = [],
200 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [],
201 erls = erls_ordne_alphabetisch,
202 rules = [Thm ("tausche_plus",num_str @{thm tausche_plus}),
203 (*"b kleiner a ==> (b + a) = (a + b)"*)
204 Thm ("tausche_minus",num_str @{thm tausche_minus}),
205 (*"b kleiner a ==> (b - a) = (-a + b)"*)
206 Thm ("tausche_vor_plus",num_str @{thm tausche_vor_plus}),
207 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
208 Thm ("tausche_vor_minus",num_str @{thm tausche_vor_minus}),
209 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
210 Thm ("tausche_plus_plus",num_str @{thm tausche_plus_plus}),
211 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
212 Thm ("tausche_plus_minus",num_str @{thm tausche_plus_minus}),
213 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
214 Thm ("tausche_minus_plus",num_str @{thm tausche_minus_plus}),
215 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
216 Thm ("tausche_minus_minus",num_str @{thm tausche_minus_minus})
217 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
218 ], scr = EmptyScr}:rls;
221 Rls{id = "fasse_zusammen", preconds = [],
222 rew_ord = ("dummy_ord", dummy_ord),
223 erls = append_rls "erls_fasse_zusammen" e_rls
224 [Calc ("Atools.is'_const",eval_const "#is_const_")],
225 srls = Erls, calc = [], errpatts = [],
227 [Thm ("real_num_collect",num_str @{thm real_num_collect}),
228 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
229 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),
230 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
231 Thm ("real_one_collect",num_str @{thm real_one_collect}),
232 (*"m is_const ==> n + m * n = (1 + m) * n"*)
233 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
234 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
237 Thm ("subtrahiere",num_str @{thm subtrahiere}),
238 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
239 Thm ("subtrahiere_von_1",num_str @{thm subtrahiere_von_1}),
240 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
241 Thm ("subtrahiere_1",num_str @{thm subtrahiere_1}),
242 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
244 Thm ("subtrahiere_x_plus_minus",num_str @{thm subtrahiere_x_plus_minus}),
245 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
246 Thm ("subtrahiere_x_plus1_minus",num_str @{thm subtrahiere_x_plus1_minus}),
247 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
248 Thm ("subtrahiere_x_plus_minus1",num_str @{thm subtrahiere_x_plus_minus1}),
249 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
251 Thm ("subtrahiere_x_minus_plus",num_str @{thm subtrahiere_x_minus_plus}),
252 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
253 Thm ("subtrahiere_x_minus1_plus",num_str @{thm subtrahiere_x_minus1_plus}),
254 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
255 Thm ("subtrahiere_x_minus_plus1",num_str @{thm subtrahiere_x_minus_plus1}),
256 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
258 Thm ("subtrahiere_x_minus_minus",num_str @{thm subtrahiere_x_minus_minus}),
259 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
260 Thm ("subtrahiere_x_minus1_minus",num_str @{thm subtrahiere_x_minus1_minus}),
261 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
262 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}),
263 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
265 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
266 Calc ("Groups.minus_class.minus", eval_binop "#subtr_"),
268 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
269 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
270 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),
271 (*"(k + z1) + z1 = k + 2 * z1"*)
272 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym})),
273 (*"z1 + z1 = 2 * z1"*)
275 Thm ("addiere_vor_minus",num_str @{thm addiere_vor_minus}),
276 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
277 Thm ("addiere_eins_vor_minus",num_str @{thm addiere_eins_vor_minus}),
278 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
279 Thm ("subtrahiere_vor_minus",num_str @{thm subtrahiere_vor_minus}),
280 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
281 Thm ("subtrahiere_eins_vor_minus",num_str @{thm subtrahiere_eins_vor_minus})
282 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
284 ], scr = EmptyScr}:rls;
287 Rls{id = "verschoenere", preconds = [],
288 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [],
289 erls = append_rls "erls_verschoenere" e_rls
290 [Calc ("PolyMinus.kleiner", eval_kleiner "")],
291 rules = [Thm ("vorzeichen_minus_weg1",num_str @{thm vorzeichen_minus_weg1}),
292 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
293 Thm ("vorzeichen_minus_weg2",num_str @{thm vorzeichen_minus_weg2}),
294 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
295 Thm ("vorzeichen_minus_weg3",num_str @{thm vorzeichen_minus_weg3}),
296 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
297 Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}),
298 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
300 Calc ("Groups.times_class.times", eval_binop "#mult_"),
302 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
304 Thm ("mult_1_left",num_str @{thm mult_1_left}),
306 Thm ("add_0_left",num_str @{thm add_0_left}),
308 Thm ("null_minus",num_str @{thm null_minus}),
310 Thm ("vor_minus_mal",num_str @{thm vor_minus_mal})
311 (*"- a * b = (-a) * b"*)
313 (*Thm ("",num_str @{}),*)
315 ], scr = EmptyScr}:rls (*end verschoenere*);
317 val klammern_aufloesen =
318 Rls{id = "klammern_aufloesen", preconds = [],
319 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [], erls = Erls,
320 rules = [Thm ("sym_add_assoc",
321 num_str (@{thm add_assoc} RS @{thm sym})),
322 (*"a + (b + c) = (a + b) + c"*)
323 Thm ("klammer_plus_minus",num_str @{thm klammer_plus_minus}),
324 (*"a + (b - c) = (a + b) - c"*)
325 Thm ("klammer_minus_plus",num_str @{thm klammer_minus_plus}),
326 (*"a - (b + c) = (a - b) - c"*)
327 Thm ("klammer_minus_minus",num_str @{thm klammer_minus_minus})
328 (*"a - (b - c) = (a - b) + c"*)
329 ], scr = EmptyScr}:rls;
331 val klammern_ausmultiplizieren =
332 Rls{id = "klammern_ausmultiplizieren", preconds = [],
333 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [], erls = Erls,
334 rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
335 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
336 Thm ("distrib_left",num_str @{thm distrib_left}),
337 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
339 Thm ("klammer_mult_minus",num_str @{thm klammer_mult_minus}),
340 (*"a * (b - c) = a * b - a * c"*)
341 Thm ("klammer_minus_mult",num_str @{thm klammer_minus_mult})
342 (*"(b - c) * a = b * a - c * a"*)
344 (*Thm ("",num_str @{}),
346 ], scr = EmptyScr}:rls;
349 Rls{id = "ordne_monome", preconds = [],
350 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], errpatts = [],
351 erls = append_rls "erls_ordne_monome" e_rls
352 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
353 Calc ("Atools.is'_atom", eval_is_atom "")
355 rules = [Thm ("tausche_mal",num_str @{thm tausche_mal}),
356 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
357 Thm ("tausche_vor_mal",num_str @{thm tausche_vor_mal}),
358 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
359 Thm ("tausche_mal_mal",num_str @{thm tausche_mal_mal}),
360 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
361 Thm ("x_quadrat",num_str @{thm x_quadrat})
362 (*"(x * a) * a = x * a ^^^ 2"*)
364 (*Thm ("",num_str @{}),
366 ], scr = EmptyScr}:rls;
370 append_rls "rls_p_33" e_rls
371 [Rls_ ordne_alphabetisch,
376 append_rls "rls_p_34" e_rls
377 [Rls_ klammern_aufloesen,
378 Rls_ ordne_alphabetisch,
383 append_rls "rechnen" e_rls
384 [Calc ("Groups.times_class.times", eval_binop "#mult_"),
385 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
386 Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
389 setup {* KEStore_Elems.add_rlss
390 [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls ordne_alphabetisch)),
391 ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls fasse_zusammen)),
392 ("verschoenere", (Context.theory_name @{theory}, prep_rls verschoenere)),
393 ("ordne_monome", (Context.theory_name @{theory}, prep_rls ordne_monome)),
394 ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls klammern_aufloesen)),
395 ("klammern_ausmultiplizieren",
396 (Context.theory_name @{theory}, prep_rls klammern_ausmultiplizieren))] *}
402 (prep_pbt thy "pbl_vereinf_poly" [] e_pblID
403 (["polynom","vereinfachen"],
404 [], Erls, NONE, []));
407 (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
408 (["plus_minus","polynom","vereinfachen"],
409 [("#Given" ,["Term t_t"]),
410 ("#Where" ,["t_t is_polyexp",
411 "Not (matchsub (?a + (?b + ?c)) t_t | " ^
412 " matchsub (?a + (?b - ?c)) t_t | " ^
413 " matchsub (?a - (?b + ?c)) t_t | " ^
414 " matchsub (?a + (?b - ?c)) t_t )",
415 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
416 " matchsub (?a * (?b - ?c)) t_t | " ^
417 " matchsub ((?b + ?c) * ?a) t_t | " ^
418 " matchsub ((?b - ?c) * ?a) t_t )"]),
419 ("#Find" ,["normalform n_n"])
421 append_rls "prls_pbl_vereinf_poly" e_rls
422 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
423 Calc ("Tools.matchsub", eval_matchsub ""),
424 Thm ("or_true", num_str @{thm or_true}),
425 (*"(?a | True) = True"*)
426 Thm ("or_false", num_str @{thm or_false}),
427 (*"(?a | False) = ?a"*)
428 Thm ("not_true",num_str @{thm not_true}),
429 (*"(~ True) = False"*)
430 Thm ("not_false",num_str @{thm not_false})
431 (*"(~ False) = True"*)],
432 SOME "Vereinfache t_t",
433 [["simplification","for_polynomials","with_minus"]]));
436 (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
437 (["klammer","polynom","vereinfachen"],
438 [("#Given" ,["Term t_t"]),
439 ("#Where" ,["t_t is_polyexp",
440 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
441 " matchsub (?a * (?b - ?c)) t_t | " ^
442 " matchsub ((?b + ?c) * ?a) t_t | " ^
443 " matchsub ((?b - ?c) * ?a) t_t )"]),
444 ("#Find" ,["normalform n_n"])
446 append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
447 Calc ("Tools.matchsub", eval_matchsub ""),
448 Thm ("or_true", num_str @{thm or_true}),
449 (*"(?a | True) = True"*)
450 Thm ("or_false", num_str @{thm or_false}),
451 (*"(?a | False) = ?a"*)
452 Thm ("not_true",num_str @{thm not_true}),
453 (*"(~ True) = False"*)
454 Thm ("not_false",num_str @{thm not_false})
455 (*"(~ False) = True"*)],
456 SOME "Vereinfache t_t",
457 [["simplification","for_polynomials","with_parentheses"]]));
460 (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
461 (["binom_klammer","polynom","vereinfachen"],
462 [("#Given" ,["Term t_t"]),
463 ("#Where" ,["t_t is_polyexp"]),
464 ("#Find" ,["normalform n_n"])
466 append_rls "e_rls" e_rls [(*for preds in where_*)
467 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
468 SOME "Vereinfache t_t",
469 [["simplification","for_polynomials","with_parentheses_mult"]]));
472 (prep_pbt thy "pbl_probe" [] e_pblID
474 [], Erls, NONE, []));
477 (prep_pbt thy "pbl_probe_poly" [] e_pblID
478 (["polynom","probe"],
479 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
480 ("#Where" ,["e_e is_polyexp"]),
481 ("#Find" ,["Geprueft p_p"])
483 append_rls "prls_pbl_probe_poly"
484 e_rls [(*for preds in where_*)
485 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
486 SOME "Probe e_e w_w",
487 [["probe","fuer_polynom"]]));
490 (prep_pbt thy "pbl_probe_bruch" [] e_pblID
492 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
493 ("#Where" ,["e_e is_ratpolyexp"]),
494 ("#Find" ,["Geprueft p_p"])
496 append_rls "prls_pbl_probe_bruch"
497 e_rls [(*for preds in where_*)
498 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
499 SOME "Probe e_e w_w",
500 [["probe","fuer_bruch"]]));
502 setup {* KEStore_Elems.add_pbts
503 [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
504 (["polynom","vereinfachen"], [], Erls, NONE, [])),
505 (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
506 (["plus_minus","polynom","vereinfachen"],
507 [("#Given", ["Term t_t"]),
508 ("#Where", ["t_t is_polyexp",
509 "Not (matchsub (?a + (?b + ?c)) t_t | " ^
510 " matchsub (?a + (?b - ?c)) t_t | " ^
511 " matchsub (?a - (?b + ?c)) t_t | " ^
512 " matchsub (?a + (?b - ?c)) t_t )",
513 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
514 " matchsub (?a * (?b - ?c)) t_t | " ^
515 " matchsub ((?b + ?c) * ?a) t_t | " ^
516 " matchsub ((?b - ?c) * ?a) t_t )"]),
517 ("#Find", ["normalform n_n"])],
518 append_rls "prls_pbl_vereinf_poly" e_rls
519 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
520 Calc ("Tools.matchsub", eval_matchsub ""),
521 Thm ("or_true", num_str @{thm or_true}),
522 (*"(?a | True) = True"*)
523 Thm ("or_false", num_str @{thm or_false}),
524 (*"(?a | False) = ?a"*)
525 Thm ("not_true",num_str @{thm not_true}),
526 (*"(~ True) = False"*)
527 Thm ("not_false",num_str @{thm not_false})
528 (*"(~ False) = True"*)],
529 SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
530 (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
531 (["klammer","polynom","vereinfachen"],
532 [("#Given" ,["Term t_t"]),
533 ("#Where" ,["t_t is_polyexp",
534 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
535 " matchsub (?a * (?b - ?c)) t_t | " ^
536 " matchsub ((?b + ?c) * ?a) t_t | " ^
537 " matchsub ((?b - ?c) * ?a) t_t )"]),
538 ("#Find" ,["normalform n_n"])],
539 append_rls "prls_pbl_vereinf_poly_klammer" e_rls
540 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
541 Calc ("Tools.matchsub", eval_matchsub ""),
542 Thm ("or_true", num_str @{thm or_true}),
543 (*"(?a | True) = True"*)
544 Thm ("or_false", num_str @{thm or_false}),
545 (*"(?a | False) = ?a"*)
546 Thm ("not_true",num_str @{thm not_true}),
547 (*"(~ True) = False"*)
548 Thm ("not_false",num_str @{thm not_false})
549 (*"(~ False) = True"*)],
550 SOME "Vereinfache t_t",
551 [["simplification","for_polynomials","with_parentheses"]])),
552 (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
553 (["binom_klammer","polynom","vereinfachen"],
554 [("#Given", ["Term t_t"]),
555 ("#Where", ["t_t is_polyexp"]),
556 ("#Find", ["normalform n_n"])],
557 append_rls "e_rls" e_rls [(*for preds in where_*)
558 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
559 SOME "Vereinfache t_t",
560 [["simplification","for_polynomials","with_parentheses_mult"]])),
561 (prep_pbt thy "pbl_probe" [] e_pblID (["probe"], [], Erls, NONE, [])),
562 (prep_pbt thy "pbl_probe_poly" [] e_pblID
563 (["polynom","probe"],
564 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
565 ("#Where", ["e_e is_polyexp"]),
566 ("#Find", ["Geprueft p_p"])],
567 append_rls "prls_pbl_probe_poly" e_rls [(*for preds in where_*)
568 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
569 SOME "Probe e_e w_w",
570 [["probe","fuer_polynom"]])),
571 (prep_pbt thy "pbl_probe_bruch" [] e_pblID
573 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
574 ("#Where" ,["e_e is_ratpolyexp"]),
575 ("#Find" ,["Geprueft p_p"])],
576 append_rls "prls_pbl_probe_bruch" e_rls [(*for preds in where_*)
577 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
578 SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))] *}
585 (prep_met thy "met_simp_poly_minus" [] e_metID
586 (["simplification","for_polynomials","with_minus"],
587 [("#Given" ,["Term t_t"]),
588 ("#Where" ,["t_t is_polyexp",
589 "Not (matchsub (?a + (?b + ?c)) t_t | " ^
590 " matchsub (?a + (?b - ?c)) t_t | " ^
591 " matchsub (?a - (?b + ?c)) t_t | " ^
592 " matchsub (?a + (?b - ?c)) t_t )"]),
593 ("#Find" ,["normalform n_n"])
595 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
596 prls = append_rls "prls_met_simp_poly_minus" e_rls
597 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
598 Calc ("Tools.matchsub", eval_matchsub ""),
599 Thm ("and_true",num_str @{thm and_true}),
600 (*"(?a & True) = ?a"*)
601 Thm ("and_false",num_str @{thm and_false}),
602 (*"(?a & False) = False"*)
603 Thm ("not_true",num_str @{thm not_true}),
604 (*"(~ True) = False"*)
605 Thm ("not_false",num_str @{thm not_false})
606 (*"(~ False) = True"*)],
607 crls = e_rls, errpats = [], nrls = rls_p_33},
608 "Script SimplifyScript (t_t::real) = " ^
609 " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
610 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
611 " (Try (Rewrite_Set verschoenere False)))) t_t)"
615 (prep_met thy "met_simp_poly_parenth" [] e_metID
616 (["simplification","for_polynomials","with_parentheses"],
617 [("#Given" ,["Term t_t"]),
618 ("#Where" ,["t_t is_polyexp"]),
619 ("#Find" ,["normalform n_n"])
621 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
622 prls = append_rls "simplification_for_polynomials_prls" e_rls
623 [(*for preds in where_*)
624 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
625 crls = e_rls, errpats = [], nrls = rls_p_34},
626 "Script SimplifyScript (t_t::real) = " ^
627 " ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
628 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
629 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
630 " (Try (Rewrite_Set verschoenere False)))) t_t)"
634 (prep_met thy "met_simp_poly_parenth_mult" [] e_metID
635 (["simplification","for_polynomials","with_parentheses_mult"],
636 [("#Given" ,["Term t_t"]),
637 ("#Where" ,["t_t is_polyexp"]),
638 ("#Find" ,["normalform n_n"])
640 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
641 prls = append_rls "simplification_for_polynomials_prls" e_rls
642 [(*for preds in where_*)
643 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
644 crls = e_rls, errpats = [], nrls = rls_p_34},
645 "Script SimplifyScript (t_t::real) = " ^
646 " ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
647 " (Try (Rewrite_Set discard_parentheses False)) @@ " ^
648 " (Try (Rewrite_Set ordne_monome False)) @@ " ^
649 " (Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
650 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
651 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
652 " (Try (Rewrite_Set verschoenere False)))) t_t)"
656 (prep_met thy "met_probe" [] e_metID
659 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
660 prls = Erls, crls = e_rls, errpats = [], nrls = Erls},
664 (prep_met thy "met_probe_poly" [] e_metID
665 (["probe","fuer_polynom"],
666 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
667 ("#Where" ,["e_e is_polyexp"]),
668 ("#Find" ,["Geprueft p_p"])
670 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
671 prls = append_rls "prls_met_probe_bruch"
672 e_rls [(*for preds in where_*)
673 Calc ("Rational.is'_ratpolyexp",
674 eval_is_ratpolyexp "")],
675 crls = e_rls, errpats = [], nrls = rechnen},
676 "Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
677 " (let e_e = Take e_e; " ^
678 " e_e = Substitute w_w e_e " ^
679 " in (Repeat((Try (Repeat (Calculate TIMES))) @@ " ^
680 " (Try (Repeat (Calculate PLUS ))) @@ " ^
681 " (Try (Repeat (Calculate MINUS))))) e_e)"
685 (prep_met thy "met_probe_bruch" [] e_metID
686 (["probe","fuer_bruch"],
687 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
688 ("#Where" ,["e_e is_ratpolyexp"]),
689 ("#Find" ,["Geprueft p_p"])
691 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
692 prls = append_rls "prls_met_probe_bruch"
693 e_rls [(*for preds in where_*)
694 Calc ("Rational.is'_ratpolyexp",
695 eval_is_ratpolyexp "")],
696 crls = e_rls, errpats = [], nrls = Erls},