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