1 (* attempts to perserve binary minus as wanted by Austrian teachers
3 (c) due to copyright terms
5 use_thy_only"Knowledge/PolyMinus";
6 use_thy"Knowledge/Isac";
9 PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational +
13 (*predicates for conditions in rewriting*)
14 kleiner :: "['a, 'a] => bool" ("_ kleiner _")
15 ist'_monom :: "'a => bool" ("_ ist'_monom")
18 Probe :: "[bool, bool list] => bool"
19 (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
21 (*descriptions for the pbl and met*)
23 mitWert :: bool list => tobooll
24 Geprueft :: bool => una
27 ProbeScript :: "[bool, bool list, bool] \
29 ("((Script ProbeScript (_ _ =))// (_))" 9)
33 null_minus "0 - a = -a"
34 vor_minus_mal "- a * b = (-a) * b"
36 (*commute with invariant (a.b).c -association*)
37 tausche_plus "[| b ist_monom; a kleiner b |] ==> \
39 tausche_minus "[| b ist_monom; a kleiner b |] ==> \
41 tausche_vor_plus "[| b ist_monom; a kleiner 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)"
50 (*commute with invariant (a.b).c -association*)
51 tausche_mal "[| b is_atom; a kleiner b |] ==> \
53 tausche_vor_mal "[| b is_atom; a kleiner 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"
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"
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"
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"
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"
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"
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"
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"
108 klammer_mult_minus "a * (b - c) = a * b - a * c"
109 klammer_minus_mult "(b - c) * a = b * a - c * a"