1.1 --- a/src/Tools/isac/IsacKnowledge/PolyMinus.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,114 +0,0 @@
     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 -