1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Thu Jan 17 16:27:03 2008 +0100
1.3 @@ -0,0 +1,114 @@
1.4 +(* attempts to perserve binary minus as wanted by Austrian teachers
1.5 + WN071207
1.6 + (c) due to copyright terms
1.7 +remove_thy"PolyMinus";
1.8 +use_thy_only"IsacKnowledge/PolyMinus";
1.9 +use_thy"IsacKnowledge/Isac";
1.10 +*)
1.11 +
1.12 +PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational +
1.13 +
1.14 +consts
1.15 +
1.16 + (*predicates for conditions in rewriting*)
1.17 + kleiner :: "['a, 'a] => bool" ("_ kleiner _")
1.18 + ist'_monom :: "'a => bool" ("_ ist'_monom")
1.19 +
1.20 + (*the CAS-command*)
1.21 + Probe :: "[bool, bool list] => bool"
1.22 + (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
1.23 +
1.24 + (*descriptions for the pbl and met*)
1.25 + Pruefe :: bool => una
1.26 + mitWert :: bool list => tobooll
1.27 + Geprueft :: bool => una
1.28 +
1.29 + (*Script-name*)
1.30 + ProbeScript :: "[bool, bool list, bool] \
1.31 + \=> bool"
1.32 + ("((Script ProbeScript (_ _ =))// (_))" 9)
1.33 +
1.34 +rules
1.35 +
1.36 + null_minus "0 - a = -a"
1.37 + vor_minus_mal "- a * b = (-a) * b"
1.38 +
1.39 + (*commute with invariant (a.b).c -association*)
1.40 + tausche_plus "[| b ist_monom; a kleiner b |] ==> \
1.41 + \(b + a) = (a + b)"
1.42 + tausche_minus "[| b ist_monom; a kleiner b |] ==> \
1.43 + \(b - a) = (-a + b)"
1.44 + tausche_vor_plus "[| b ist_monom; a kleiner b |] ==> \
1.45 + \(- b + a) = (a - b)"
1.46 + tausche_vor_minus "[| b ist_monom; a kleiner b |] ==> \
1.47 + \(- b - a) = (-a - b)"
1.48 + tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
1.49 + tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
1.50 + tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
1.51 + tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
1.52 +
1.53 + (*commute with invariant (a.b).c -association*)
1.54 + tausche_mal "[| b is_atom; a kleiner b |] ==> \
1.55 + \(b * a) = (a * b)"
1.56 + tausche_vor_mal "[| b is_atom; a kleiner b |] ==> \
1.57 + \(-b * a) = (-a * b)"
1.58 + tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \
1.59 + \(x * c * b) = (x * b * c)"
1.60 + x_quadrat "(x * a) * a = x * a ^^^ 2"
1.61 +
1.62 +
1.63 + subtrahiere "[| l is_const; m is_const |] ==> \
1.64 + \m * v - l * v = (m - l) * v"
1.65 + subtrahiere_von_1 "[| l is_const |] ==> \
1.66 + \v - l * v = (1 - l) * v"
1.67 + subtrahiere_1 "[| l is_const; m is_const |] ==> \
1.68 + \m * v - v = (m - 1) * v"
1.69 +
1.70 + subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==> \
1.71 + \(x + m * v) - l * v = x + (m - l) * v"
1.72 + subtrahiere_x_plus1_minus "[| l is_const |] ==> \
1.73 + \(x + v) - l * v = x + (1 - l) * v"
1.74 + subtrahiere_x_plus_minus1 "[| m is_const |] ==> \
1.75 + \(x + m * v) - v = x + (m - 1) * v"
1.76 +
1.77 + subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==> \
1.78 + \(x - m * v) + l * v = x + (-m + l) * v"
1.79 + subtrahiere_x_minus1_plus "[| l is_const |] ==> \
1.80 + \(x - v) + l * v = x + (-1 + l) * v"
1.81 + subtrahiere_x_minus_plus1 "[| m is_const |] ==> \
1.82 + \(x - m * v) + v = x + (-m + 1) * v"
1.83 +
1.84 + subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==> \
1.85 + \(x - m * v) - l * v = x + (-m - l) * v"
1.86 + subtrahiere_x_minus1_minus"[| l is_const |] ==> \
1.87 + \(x - v) - l * v = x + (-1 - l) * v"
1.88 + subtrahiere_x_minus_minus1"[| m is_const |] ==> \
1.89 + \(x - m * v) - v = x + (-m - 1) * v"
1.90 +
1.91 +
1.92 + addiere_vor_minus "[| l is_const; m is_const |] ==> \
1.93 + \- (l * v) + m * v = (-l + m) * v"
1.94 + addiere_eins_vor_minus "[| m is_const |] ==> \
1.95 + \- v + m * v = (-1 + m) * v"
1.96 + subtrahiere_vor_minus "[| l is_const; m is_const |] ==> \
1.97 + \- (l * v) - m * v = (-l - m) * v"
1.98 + subtrahiere_eins_vor_minus"[| m is_const |] ==> \
1.99 + \- v - m * v = (-1 - m) * v"
1.100 +
1.101 + vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
1.102 + vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
1.103 + vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
1.104 + vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
1.105 +
1.106 + (*klammer_plus_plus = (real_add_assoc RS sym)*)
1.107 + klammer_plus_minus "a + (b - c) = (a + b) - c"
1.108 + klammer_minus_plus "a - (b + c) = (a - b) - c"
1.109 + klammer_minus_minus "a - (b - c) = (a - b) + c"
1.110 +
1.111 + klammer_mult_minus "a * (b - c) = a * b - a * c"
1.112 + klammer_minus_mult "(b - c) * a = b * a - c * a"
1.113 +
1.114 +
1.115 +
1.116 +end
1.117 +