neuper@37906: (* attempts to perserve binary minus as wanted by Austrian teachers
neuper@37906:    WN071207
neuper@37906:    (c) due to copyright terms
neuper@37906: remove_thy"PolyMinus";
neuper@37947: use_thy_only"Knowledge/PolyMinus";
neuper@37947: use_thy"Knowledge/Isac";
neuper@37906: *)
neuper@37906: 
neuper@37906: PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational + 
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*predicates for conditions in rewriting*)
neuper@37906:   kleiner     :: "['a, 'a] => bool" 	("_ kleiner _") 
neuper@37906:   ist'_monom  :: "'a => bool"		("_ ist'_monom")
neuper@37906: 
neuper@37906:   (*the CAS-command*)
neuper@37906:   Probe       :: "[bool, bool list] => bool"  
neuper@37906: 	(*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
neuper@37906: 
neuper@37906:   (*descriptions for the pbl and met*)
neuper@37906:   Pruefe      :: bool => una
neuper@37906:   mitWert     :: bool list => tobooll
neuper@37906:   Geprueft    :: bool => una
neuper@37906: 
neuper@37906:   (*Script-name*)
neuper@37906:   ProbeScript :: "[bool, bool list,       bool] \
neuper@37906: 				      \=> bool"
neuper@37906:                   ("((Script ProbeScript (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37906: rules
neuper@37906: 
neuper@37906:   null_minus            "0 - a = -a"
neuper@37906:   vor_minus_mal         "- a * b = (-a) * b"
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37906:   tausche_plus		"[| b ist_monom; a kleiner b  |] ==> \
neuper@37906: 			\(b + a) = (a + b)"
neuper@37906:   tausche_minus		"[| b ist_monom; a kleiner b  |] ==> \
neuper@37906: 			\(b - a) = (-a + b)"
neuper@37906:   tausche_vor_plus	"[| b ist_monom; a kleiner b  |] ==> \
neuper@37906: 			\(- b + a) = (a - b)"
neuper@37906:   tausche_vor_minus	"[| b ist_monom; a kleiner b  |] ==> \
neuper@37906: 			\(- b - a) = (-a - b)"
neuper@37906:   tausche_plus_plus	"b kleiner c ==> (a + c + b) = (a + b + c)"
neuper@37906:   tausche_plus_minus	"b kleiner c ==> (a + c - b) = (a - b + c)"
neuper@37906:   tausche_minus_plus	"b kleiner c ==> (a - c + b) = (a + b - c)"
neuper@37906:   tausche_minus_minus	"b kleiner c ==> (a - c - b) = (a - b - c)"
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37906:   tausche_mal		"[| b is_atom; a kleiner b  |] ==> \
neuper@37906: 			\(b * a) = (a * b)"
neuper@37906:   tausche_vor_mal	"[| b is_atom; a kleiner b  |] ==> \
neuper@37906: 			\(-b * a) = (-a * b)"
neuper@37906:   tausche_mal_mal	"[| c is_atom; b kleiner c  |] ==> \
neuper@37906: 			\(x * c * b) = (x * b * c)"
neuper@37906:   x_quadrat             "(x * a) * a = x * a ^^^ 2"
neuper@37906: 
neuper@37906: 
neuper@37906:   subtrahiere               "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \m * v - l * v = (m - l) * v"
neuper@37906:   subtrahiere_von_1         "[| l is_const |] ==>  \
neuper@37906: 			    \v - l * v = (1 - l) * v"
neuper@37906:   subtrahiere_1             "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \m * v - v = (m - 1) * v"
neuper@37906: 
neuper@37906:   subtrahiere_x_plus_minus  "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \(x + m * v) - l * v = x + (m - l) * v"
neuper@37906:   subtrahiere_x_plus1_minus "[| l is_const |] ==>  \
neuper@37906: 			    \(x + v) - l * v = x + (1 - l) * v"
neuper@37906:   subtrahiere_x_plus_minus1 "[| m is_const |] ==>  \
neuper@37906: 			    \(x + m * v) - v = x + (m - 1) * v"
neuper@37906: 
neuper@37906:   subtrahiere_x_minus_plus  "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \(x - m * v) + l * v = x + (-m + l) * v"
neuper@37906:   subtrahiere_x_minus1_plus "[| l is_const |] ==>  \
neuper@37906: 			    \(x - v) + l * v = x + (-1 + l) * v"
neuper@37906:   subtrahiere_x_minus_plus1 "[| m is_const |] ==>  \
neuper@37906: 			    \(x - m * v) + v = x + (-m + 1) * v"
neuper@37906: 
neuper@37906:   subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \(x - m * v) - l * v = x + (-m - l) * v"
neuper@37906:   subtrahiere_x_minus1_minus"[| l is_const |] ==>  \
neuper@37906: 			    \(x - v) - l * v = x + (-1 - l) * v"
neuper@37906:   subtrahiere_x_minus_minus1"[| m is_const |] ==>  \
neuper@37906: 			    \(x - m * v) - v = x + (-m - 1) * v"
neuper@37906: 
neuper@37906: 
neuper@37906:   addiere_vor_minus         "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \- (l * v) +  m * v = (-l + m) * v"
neuper@37906:   addiere_eins_vor_minus    "[| m is_const |] ==>  \
neuper@37906: 			    \-  v +  m * v = (-1 + m) * v"
neuper@37906:   subtrahiere_vor_minus     "[| l is_const; m is_const |] ==>  \
neuper@37906: 			    \- (l * v) -  m * v = (-l - m) * v"
neuper@37906:   subtrahiere_eins_vor_minus"[| m is_const |] ==>  \
neuper@37906: 			    \-  v -  m * v = (-1 - m) * v"
neuper@37906: 
neuper@37906:   vorzeichen_minus_weg1  "l kleiner 0 ==> a + l * b = a - -1*l * b"
neuper@37906:   vorzeichen_minus_weg2  "l kleiner 0 ==> a - l * b = a + -1*l * b"
neuper@37906:   vorzeichen_minus_weg3  "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
neuper@37906:   vorzeichen_minus_weg4  "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
neuper@37906: 
neuper@37906:   (*klammer_plus_plus = (real_add_assoc RS sym)*)
neuper@37906:   klammer_plus_minus     "a + (b - c) = (a + b) - c"
neuper@37906:   klammer_minus_plus     "a - (b + c) = (a - b) - c"
neuper@37906:   klammer_minus_minus    "a - (b - c) = (a - b) + c"
neuper@37906: 
neuper@37906:   klammer_mult_minus      "a * (b - c) = a * b - a * c"
neuper@37906:   klammer_minus_mult      "(b - c) * a = b * a - c * a"
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: end
neuper@37906: