1 (* questionable attempts to perserve binary minus as wanted by teachers
3 (c) due to copyright terms
5 use_thy"IsacKnowledge/PolyMinus";
7 use_thy"IsacKnowledge/Isac";
8 use"IsacKnowledge/PolyMinus.ML";
11 (** interface isabelle -- isac **)
12 theory' := overwritel (!theory', [("PolyMinus.thy",PolyMinus.thy)]);
14 (** eval functions **)
16 (* get the identifier from a monomial of the form num | var | num*var;
17 attention: num is Free("123",_) *)
18 fun identifier (Free (id,_)) = id
19 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
20 if is_numeral num then id
22 | identifier _ = "|||||||||||||"(*the "largest" string*);
24 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
25 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
26 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
27 if is_num a andalso is_num b then
28 if int_of_Free a < int_of_Free b then
29 Some ((term2str p) ^ " = True",
30 Trueprop $ (mk_equality (p, HOLogic.true_const)))
31 else Some ((term2str p) ^ " = False",
32 Trueprop $ (mk_equality (p, HOLogic.false_const)))
34 if identifier a < identifier b then
35 Some ((term2str p) ^ " = True",
36 Trueprop $ (mk_equality (p, HOLogic.true_const)))
37 else Some ((term2str p) ^ " = False",
38 Trueprop $ (mk_equality (p, HOLogic.false_const)))
39 | eval_kleiner _ _ _ _ = None;
40 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
43 if int_of_Free a < int_of_Free b then
44 Some ((term2str p) ^ " = True",
45 Trueprop $ (mk_equality (p, HOLogic.true_const)))
46 else Some ((term2str p) ^ " = False",
47 Trueprop $ (mk_equality (p, HOLogic.false_const)))
48 else (* -1 * -2 kleiner 0 *)
49 Some ((term2str p) ^ " = False",
50 Trueprop $ (mk_equality (p, HOLogic.false_const)))
52 if identifier a < identifier b then
53 Some ((term2str p) ^ " = True",
54 Trueprop $ (mk_equality (p, HOLogic.true_const)))
55 else Some ((term2str p) ^ " = False",
56 Trueprop $ (mk_equality (p, HOLogic.false_const)))
57 | eval_kleiner _ _ _ _ = None;
59 fun ist_monom (Free (id,_)) = true
60 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
61 if is_numeral num then true else false
62 | ist_monom _ = false;
64 (* is this a univariate monomial ? *)
65 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
66 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
68 Some ((term2str p) ^ " = True",
69 Trueprop $ (mk_equality (p, HOLogic.true_const)))
70 else Some ((term2str p) ^ " = False",
71 Trueprop $ (mk_equality (p, HOLogic.false_const)))
72 | eval_ist_monom _ _ _ _ = None;
79 val erls_ordne_alphabetisch =
80 append_rls "erls_ordne_alphabetisch" e_rls
81 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
82 Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
85 val ordne_alphabetisch =
86 Rls{id = "ordne_alphabetisch", preconds = [],
87 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
88 erls = erls_ordne_alphabetisch,
89 rules = [Thm ("tausche_plus",num_str tausche_plus),
90 (*"b kleiner a ==> (b + a) = (a + b)"*)
91 Thm ("tausche_minus",num_str tausche_minus),
92 (*"b kleiner a ==> (b - a) = (-a + b)"*)
93 Thm ("tausche_vor_plus",num_str tausche_vor_plus),
94 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
95 Thm ("tausche_vor_minus",num_str tausche_vor_minus),
96 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
97 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
98 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
99 Thm ("tausche_plus_minus",num_str tausche_plus_minus),
100 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
101 Thm ("tausche_minus_plus",num_str tausche_minus_plus),
102 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
103 Thm ("tausche_minus_minus",num_str tausche_minus_minus)
104 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
105 ], scr = EmptyScr}:rls;
108 Rls{id = "fasse_zusammen", preconds = [],
109 rew_ord = ("dummy_ord", dummy_ord),
110 erls = append_rls "erls_fasse_zusammen" e_rls
111 [Calc ("Atools.is'_const",eval_const "#is_const_")],
112 srls = Erls, calc = [],
114 [Thm ("real_num_collect",num_str real_num_collect),
115 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
116 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
117 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
118 Thm ("real_one_collect",num_str real_one_collect),
119 (*"m is_const ==> n + m * n = (1 + m) * n"*)
120 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
121 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
124 Thm ("subtrahiere",num_str subtrahiere),
125 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
126 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
127 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
128 Thm ("subtrahiere_1",num_str subtrahiere_1),
129 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
131 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
132 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
133 Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
134 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
135 Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
136 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
138 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
139 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
140 Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
141 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
142 Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
143 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
145 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
146 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
147 Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
148 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
149 Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
150 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
152 Calc ("op +", eval_binop "#add_"),
153 Calc ("op -", eval_binop "#subtr_"),
155 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
156 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
157 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
158 (*"(k + z1) + z1 = k + 2 * z1"*)
159 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
160 (*"z1 + z1 = 2 * z1"*)
162 Thm ("addiere_vor_minus",num_str addiere_vor_minus),
163 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
164 Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
165 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
166 Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
167 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
168 Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
169 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
171 ], scr = EmptyScr}:rls;
174 Rls{id = "verschoenere", preconds = [],
175 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
176 erls = append_rls "erls_verschoenere" e_rls
177 [Calc ("PolyMinus.kleiner", eval_kleiner "")],
178 rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
179 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
180 Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
181 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
182 Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
183 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
184 Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
185 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
187 Calc ("op *", eval_binop "#mult_"),
189 Thm ("real_mult_0",num_str real_mult_0),
191 Thm ("real_mult_1",num_str real_mult_1),
193 Thm ("real_add_zero_left",num_str real_add_zero_left),
195 Thm ("null_minus",num_str null_minus),
197 Thm ("vor_minus_mal",num_str vor_minus_mal)
198 (*"- a * b = (-a) * b"*)
200 (*Thm ("",num_str ),*)
202 ], scr = EmptyScr}:rls (*end verschoenere*);
204 val klammern_aufloesen =
205 Rls{id = "klammern_aufloesen", preconds = [],
206 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
207 rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
208 (*"a + (b + c) = (a + b) + c"*)
209 Thm ("klammer_plus_minus",num_str klammer_plus_minus),
210 (*"a + (b - c) = (a + b) - c"*)
211 Thm ("klammer_minus_plus",num_str klammer_minus_plus),
212 (*"a - (b + c) = (a - b) - c"*)
213 Thm ("klammer_minus_minus",num_str klammer_minus_minus)
214 (*"a - (b - c) = (a - b) + c"*)
215 ], scr = EmptyScr}:rls;
217 val klammern_ausmultiplizieren =
218 Rls{id = "klammern_ausmultiplizieren", preconds = [],
219 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
220 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
221 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
222 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
223 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
225 Thm ("klammer_mult_minus",num_str klammer_mult_minus),
226 (*"a * (b - c) = a * b - a * c"*)
227 Thm ("klammer_minus_mult",num_str klammer_minus_mult)
228 (*"(b - c) * a = b * a - c * a"*)
232 ], scr = EmptyScr}:rls;
235 Rls{id = "ordne_monome", preconds = [],
236 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
237 erls = append_rls "erls_ordne_monome" e_rls
238 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
239 Calc ("Atools.is'_atom", eval_is_atom "")
241 rules = [Thm ("tausche_mal",num_str tausche_mal),
242 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
243 Thm ("tausche_vor_mal",num_str tausche_vor_mal),
244 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
245 Thm ("tausche_mal_mal",num_str tausche_mal_mal),
246 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
247 Thm ("x_quadrat",num_str x_quadrat)
248 (*"(x * a) * a = x * a ^^^ 2"*)
252 ], scr = EmptyScr}:rls;
256 append_rls "rls_p_33" e_rls
257 [Rls_ ordne_alphabetisch,
262 append_rls "rls_p_34" e_rls
263 [Rls_ klammern_aufloesen,
264 Rls_ ordne_alphabetisch,
269 append_rls "rechnen" e_rls
270 [Calc ("op *", eval_binop "#mult_"),
271 Calc ("op +", eval_binop "#add_"),
272 Calc ("op -", eval_binop "#subtr_")
276 overwritelthy thy (!ruleset',
277 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
278 ("fasse_zusammen", prep_rls fasse_zusammen),
279 ("verschoenere", prep_rls verschoenere),
280 ("ordne_monome", prep_rls ordne_monome),
281 ("klammern_aufloesen", prep_rls klammern_aufloesen),
282 ("klammern_ausmultiplizieren",
283 prep_rls klammern_ausmultiplizieren)
289 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
290 (["polynom","vereinfachen"],
291 [], Erls, None, []));
294 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
295 (["plus_minus","polynom","vereinfachen"],
296 [("#Given" ,["term t_"]),
297 ("#Where" ,["t_ is_polyexp",
298 "Not (matchsub (?a + (?b + ?c)) t_ | \
299 \ matchsub (?a + (?b - ?c)) t_ | \
300 \ matchsub (?a - (?b + ?c)) t_ | \
301 \ matchsub (?a + (?b - ?c)) t_ )"]),
302 ("#Find" ,["normalform n_"])
304 append_rls "prls_pbl_vereinf_poly" e_rls
305 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
306 Calc ("Tools.matchsub", eval_matchsub ""),
307 Thm ("and_true",and_true),
308 (*"(?a & True) = ?a"*)
309 Thm ("and_false",and_false),
310 (*"(?a & False) = False"*)
311 Thm ("not_true",num_str not_true),
312 (*"(~ True) = False"*)
313 Thm ("not_false",num_str not_false)
314 (*"(~ False) = True"*)],
315 Some "Vereinfache t_",
316 [["simplification","for_polynomials","with_minus"]]));
319 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
320 (["klammer","polynom","vereinfachen"],
321 [("#Given" ,["term t_"]),
322 ("#Where" ,["t_ is_polyexp"]),
323 ("#Find" ,["normalform n_"])
325 append_rls "e_rls" e_rls [(*for preds in where_*)
326 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
327 Some "Vereinfache t_",
328 [["simplification","for_polynomials","with_parentheses"]]));
331 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
332 (["binom_klammer","polynom","vereinfachen"],
333 [("#Given" ,["term t_"]),
334 ("#Where" ,["t_ is_polyexp"]),
335 ("#Find" ,["normalform n_"])
337 append_rls "e_rls" e_rls [(*for preds in where_*)
338 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
339 Some "Vereinfache t_",
340 [["simplification","for_polynomials","with_parentheses_mult"]]));
343 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
345 [], Erls, None, []));
348 (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
349 (["polynom","probe"],
350 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
351 ("#Where" ,["e_ is_polyexp"]),
352 ("#Find" ,["Geprueft p_"])
354 append_rls "prls_pbl_probe_poly"
355 e_rls [(*for preds in where_*)
356 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
358 [["probe","fuer_polynom"]]));
361 (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
363 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
364 ("#Where" ,["e_ is_ratpolyexp"]),
365 ("#Find" ,["Geprueft p_"])
367 append_rls "prls_pbl_probe_bruch"
368 e_rls [(*for preds in where_*)
369 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
371 [["probe","fuer_bruch"]]));
377 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
378 (["simplification","for_polynomials","with_minus"],
379 [("#Given" ,["term t_"]),
380 ("#Where" ,["t_ is_polyexp",
381 "Not (matchsub (?a + (?b + ?c)) t_ | \
382 \ matchsub (?a + (?b - ?c)) t_ | \
383 \ matchsub (?a - (?b + ?c)) t_ | \
384 \ matchsub (?a + (?b - ?c)) t_ )"]),
385 ("#Find" ,["normalform n_"])
387 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
388 prls = append_rls "prls_met_simp_poly_minus" e_rls
389 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
390 Calc ("Tools.matchsub", eval_matchsub ""),
391 Thm ("and_true",and_true),
392 (*"(?a & True) = ?a"*)
393 Thm ("and_false",and_false),
394 (*"(?a & False) = False"*)
395 Thm ("not_true",num_str not_true),
396 (*"(~ True) = False"*)
397 Thm ("not_false",num_str not_false)
398 (*"(~ False) = True"*)],
399 crls = e_rls, nrls = rls_p_33},
400 "Script SimplifyScript (t_::real) = \
401 \ ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
402 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
403 \ (Try (Rewrite_Set verschoenere False)))) t_)"
407 (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
408 (["simplification","for_polynomials","with_parentheses"],
409 [("#Given" ,["term t_"]),
410 ("#Where" ,["t_ is_polyexp"]),
411 ("#Find" ,["normalform n_"])
413 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
414 prls = append_rls "simplification_for_polynomials_prls" e_rls
415 [(*for preds in where_*)
416 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
417 crls = e_rls, nrls = rls_p_34},
418 "Script SimplifyScript (t_::real) = \
419 \ ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ \
420 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
421 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
422 \ (Try (Rewrite_Set verschoenere False)))) t_)"
426 (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
427 (["simplification","for_polynomials","with_parentheses_mult"],
428 [("#Given" ,["term t_"]),
429 ("#Where" ,["t_ is_polyexp"]),
430 ("#Find" ,["normalform n_"])
432 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
433 prls = append_rls "simplification_for_polynomials_prls" e_rls
434 [(*for preds in where_*)
435 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
436 crls = e_rls, nrls = rls_p_34},
437 "Script SimplifyScript (t_::real) = \
438 \ ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
439 \ (Try (Rewrite_Set discard_parentheses False)) @@ \
440 \ (Try (Rewrite_Set ordne_monome False)) @@ \
441 \ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
442 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
443 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
444 \ (Try (Rewrite_Set verschoenere False)))) t_)"
448 (prep_met PolyMinus.thy "met_probe" [] e_metID
451 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
452 prls = Erls, crls = e_rls, nrls = Erls},
456 (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
457 (["probe","fuer_polynom"],
458 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
459 ("#Where" ,["e_ is_polyexp"]),
460 ("#Find" ,["Geprueft p_"])
462 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
463 prls = append_rls "prls_met_probe_bruch"
464 e_rls [(*for preds in where_*)
465 Calc ("Rational.is'_ratpolyexp",
466 eval_is_ratpolyexp "")],
467 crls = e_rls, nrls = rechnen},
468 "Script ProbeScript (e_::bool) (ws_::bool list) = \
469 \ (let e_ = Take e_; \
470 \ e_ = Substitute ws_ e_ \
471 \ in (Repeat((Try (Repeat (Calculate times))) @@ \
472 \ (Try (Repeat (Calculate plus ))) @@ \
473 \ (Try (Repeat (Calculate minus))))) e_)"
477 (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
478 (["probe","fuer_bruch"],
479 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
480 ("#Where" ,["e_ is_ratpolyexp"]),
481 ("#Find" ,["Geprueft p_"])
483 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
484 prls = append_rls "prls_met_probe_bruch"
485 e_rls [(*for preds in where_*)
486 Calc ("Rational.is'_ratpolyexp",
487 eval_is_ratpolyexp "")],
488 crls = e_rls, nrls = Erls},