|
1 (* attempts to perserve binary minus as wanted by Austrian teachers |
|
2 WN071207 |
|
3 (c) due to copyright terms |
|
4 remove_thy"PolyMinus"; |
|
5 use_thy_only"Knowledge/PolyMinus"; |
|
6 use_thy"Knowledge/Isac"; |
|
7 *) |
|
8 |
|
9 PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational + |
|
10 |
|
11 consts |
|
12 |
|
13 (*predicates for conditions in rewriting*) |
|
14 kleiner :: "['a, 'a] => bool" ("_ kleiner _") |
|
15 ist'_monom :: "'a => bool" ("_ ist'_monom") |
|
16 |
|
17 (*the CAS-command*) |
|
18 Probe :: "[bool, bool list] => bool" |
|
19 (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*) |
|
20 |
|
21 (*descriptions for the pbl and met*) |
|
22 Pruefe :: bool => una |
|
23 mitWert :: bool list => tobooll |
|
24 Geprueft :: bool => una |
|
25 |
|
26 (*Script-name*) |
|
27 ProbeScript :: "[bool, bool list, bool] \ |
|
28 \=> bool" |
|
29 ("((Script ProbeScript (_ _ =))// (_))" 9) |
|
30 |
|
31 rules |
|
32 |
|
33 null_minus "0 - a = -a" |
|
34 vor_minus_mal "- a * b = (-a) * b" |
|
35 |
|
36 (*commute with invariant (a.b).c -association*) |
|
37 tausche_plus "[| b ist_monom; a kleiner b |] ==> \ |
|
38 \(b + a) = (a + b)" |
|
39 tausche_minus "[| b ist_monom; a kleiner b |] ==> \ |
|
40 \(b - a) = (-a + b)" |
|
41 tausche_vor_plus "[| b ist_monom; a kleiner b |] ==> \ |
|
42 \(- b + a) = (a - b)" |
|
43 tausche_vor_minus "[| b ist_monom; a kleiner b |] ==> \ |
|
44 \(- b - a) = (-a - b)" |
|
45 tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)" |
|
46 tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)" |
|
47 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)" |
|
48 tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)" |
|
49 |
|
50 (*commute with invariant (a.b).c -association*) |
|
51 tausche_mal "[| b is_atom; a kleiner b |] ==> \ |
|
52 \(b * a) = (a * b)" |
|
53 tausche_vor_mal "[| b is_atom; a kleiner b |] ==> \ |
|
54 \(-b * a) = (-a * b)" |
|
55 tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \ |
|
56 \(x * c * b) = (x * b * c)" |
|
57 x_quadrat "(x * a) * a = x * a ^^^ 2" |
|
58 |
|
59 |
|
60 subtrahiere "[| l is_const; m is_const |] ==> \ |
|
61 \m * v - l * v = (m - l) * v" |
|
62 subtrahiere_von_1 "[| l is_const |] ==> \ |
|
63 \v - l * v = (1 - l) * v" |
|
64 subtrahiere_1 "[| l is_const; m is_const |] ==> \ |
|
65 \m * v - v = (m - 1) * v" |
|
66 |
|
67 subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==> \ |
|
68 \(x + m * v) - l * v = x + (m - l) * v" |
|
69 subtrahiere_x_plus1_minus "[| l is_const |] ==> \ |
|
70 \(x + v) - l * v = x + (1 - l) * v" |
|
71 subtrahiere_x_plus_minus1 "[| m is_const |] ==> \ |
|
72 \(x + m * v) - v = x + (m - 1) * v" |
|
73 |
|
74 subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==> \ |
|
75 \(x - m * v) + l * v = x + (-m + l) * v" |
|
76 subtrahiere_x_minus1_plus "[| l is_const |] ==> \ |
|
77 \(x - v) + l * v = x + (-1 + l) * v" |
|
78 subtrahiere_x_minus_plus1 "[| m is_const |] ==> \ |
|
79 \(x - m * v) + v = x + (-m + 1) * v" |
|
80 |
|
81 subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==> \ |
|
82 \(x - m * v) - l * v = x + (-m - l) * v" |
|
83 subtrahiere_x_minus1_minus"[| l is_const |] ==> \ |
|
84 \(x - v) - l * v = x + (-1 - l) * v" |
|
85 subtrahiere_x_minus_minus1"[| m is_const |] ==> \ |
|
86 \(x - m * v) - v = x + (-m - 1) * v" |
|
87 |
|
88 |
|
89 addiere_vor_minus "[| l is_const; m is_const |] ==> \ |
|
90 \- (l * v) + m * v = (-l + m) * v" |
|
91 addiere_eins_vor_minus "[| m is_const |] ==> \ |
|
92 \- v + m * v = (-1 + m) * v" |
|
93 subtrahiere_vor_minus "[| l is_const; m is_const |] ==> \ |
|
94 \- (l * v) - m * v = (-l - m) * v" |
|
95 subtrahiere_eins_vor_minus"[| m is_const |] ==> \ |
|
96 \- v - m * v = (-1 - m) * v" |
|
97 |
|
98 vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b" |
|
99 vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b" |
|
100 vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" |
|
101 vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" |
|
102 |
|
103 (*klammer_plus_plus = (real_add_assoc RS sym)*) |
|
104 klammer_plus_minus "a + (b - c) = (a + b) - c" |
|
105 klammer_minus_plus "a - (b + c) = (a - b) - c" |
|
106 klammer_minus_minus "a - (b - c) = (a - b) + c" |
|
107 |
|
108 klammer_mult_minus "a * (b - c) = a * b - a * c" |
|
109 klammer_minus_mult "(b - c) * a = b * a - c * a" |
|
110 |
|
111 |
|
112 |
|
113 end |
|
114 |