(* attempts to perserve binary minus as wanted by Austrian teachers

   WN071207

   (c) due to copyright terms

remove_thy"PolyMinus";

use_thy_only"Knowledge/PolyMinus";

use_thy"Knowledge/Isac";

*)

PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational + 

consts

  (*predicates for conditions in rewriting*)

  kleiner     :: "['a, 'a] => bool" 	("_ kleiner _") 

  ist'_monom  :: "'a => bool"		("_ ist'_monom")

  (*the CAS-command*)

  Probe       :: "[bool, bool list] => bool"  

	(*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)

  (*descriptions for the pbl and met*)

  Pruefe      :: bool => una

  mitWert     :: bool list => tobooll

  Geprueft    :: bool => una

  (*Script-name*)

  ProbeScript :: "[bool, bool list,       bool] \

				      \=> bool"

                  ("((Script ProbeScript (_ _ =))// (_))" 9)

rules

  null_minus            "0 - a = -a"

  vor_minus_mal         "- a * b = (-a) * b"

  (*commute with invariant (a.b).c -association*)

  tausche_plus		"[| b ist_monom; a kleiner b  |] ==> \

			\(b + a) = (a + b)"

  tausche_minus		"[| b ist_monom; a kleiner b  |] ==> \

			\(b - a) = (-a + b)"

  tausche_vor_plus	"[| b ist_monom; a kleiner b  |] ==> \

			\(- b + a) = (a - b)"

  tausche_vor_minus	"[| b ist_monom; a kleiner b  |] ==> \

			\(- b - a) = (-a - b)"

  tausche_plus_plus	"b kleiner c ==> (a + c + b) = (a + b + c)"

  tausche_plus_minus	"b kleiner c ==> (a + c - b) = (a - b + c)"

  tausche_minus_plus	"b kleiner c ==> (a - c + b) = (a + b - c)"

  tausche_minus_minus	"b kleiner c ==> (a - c - b) = (a - b - c)"

  (*commute with invariant (a.b).c -association*)

  tausche_mal		"[| b is_atom; a kleiner b  |] ==> \

			\(b * a) = (a * b)"

  tausche_vor_mal	"[| b is_atom; a kleiner b  |] ==> \

			\(-b * a) = (-a * b)"

  tausche_mal_mal	"[| c is_atom; b kleiner c  |] ==> \

			\(x * c * b) = (x * b * c)"

  x_quadrat             "(x * a) * a = x * a ^^^ 2"

  subtrahiere               "[| l is_const; m is_const |] ==>  \

			    \m * v - l * v = (m - l) * v"

  subtrahiere_von_1         "[| l is_const |] ==>  \

			    \v - l * v = (1 - l) * v"

  subtrahiere_1             "[| l is_const; m is_const |] ==>  \

			    \m * v - v = (m - 1) * v"

  subtrahiere_x_plus_minus  "[| l is_const; m is_const |] ==>  \

			    \(x + m * v) - l * v = x + (m - l) * v"

  subtrahiere_x_plus1_minus "[| l is_const |] ==>  \

			    \(x + v) - l * v = x + (1 - l) * v"

  subtrahiere_x_plus_minus1 "[| m is_const |] ==>  \

			    \(x + m * v) - v = x + (m - 1) * v"

  subtrahiere_x_minus_plus  "[| l is_const; m is_const |] ==>  \

			    \(x - m * v) + l * v = x + (-m + l) * v"

  subtrahiere_x_minus1_plus "[| l is_const |] ==>  \

			    \(x - v) + l * v = x + (-1 + l) * v"

  subtrahiere_x_minus_plus1 "[| m is_const |] ==>  \

			    \(x - m * v) + v = x + (-m + 1) * v"

  subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==>  \

			    \(x - m * v) - l * v = x + (-m - l) * v"

  subtrahiere_x_minus1_minus"[| l is_const |] ==>  \

			    \(x - v) - l * v = x + (-1 - l) * v"

  subtrahiere_x_minus_minus1"[| m is_const |] ==>  \

			    \(x - m * v) - v = x + (-m - 1) * v"

  addiere_vor_minus         "[| l is_const; m is_const |] ==>  \

			    \- (l * v) +  m * v = (-l + m) * v"

  addiere_eins_vor_minus    "[| m is_const |] ==>  \

			    \-  v +  m * v = (-1 + m) * v"

  subtrahiere_vor_minus     "[| l is_const; m is_const |] ==>  \

			    \- (l * v) -  m * v = (-l - m) * v"

  subtrahiere_eins_vor_minus"[| m is_const |] ==>  \

			    \-  v -  m * v = (-1 - m) * v"

  vorzeichen_minus_weg1  "l kleiner 0 ==> a + l * b = a - -1*l * b"

  vorzeichen_minus_weg2  "l kleiner 0 ==> a - l * b = a + -1*l * b"

  vorzeichen_minus_weg3  "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"

  vorzeichen_minus_weg4  "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"

  (*klammer_plus_plus = (real_add_assoc RS sym)*)

  klammer_plus_minus     "a + (b - c) = (a + b) - c"

  klammer_minus_plus     "a - (b + c) = (a - b) - c"

  klammer_minus_minus    "a - (b - c) = (a - b) + c"

  klammer_mult_minus      "a * (b - c) = a * b - a * c"

  klammer_minus_mult      "(b - c) * a = b * a - c * a"

end