diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/EqSystem.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,72 @@
+(* equational systems, minimal -- for use in Biegelinie
+   author: Walther Neuper
+   050826,
+   (c) due to copyright terms
+
+remove_thy"EqSystem";
+use_thy"Knowledge/EqSystem";
+
+use_thy_only"Knowledge/EqSystem";
+
+remove_thy"Typefix";
+use_thy"Knowledge/Isac";
+*)
+
+EqSystem = Rational + Root +
+
+consts
+
+  occur'_exactly'_in :: 
+   "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _")
+
+  (*descriptions in the related problems*)
+  solveForVars       :: real list => toreall
+  solution           :: bool list => toreall
+
+  (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
+  solveSystem        :: "[bool list, real list] => bool list"
+
+  (*Script-names*)
+  SolveSystemScript  :: "[bool list, real list,     bool list] \
+						\=> bool list"
+                  ("((Script SolveSystemScript (_ _ =))// (_))" 9)
+
+rules 
+(*stated as axioms, todo: prove as theorems
+  'bdv' is a constant handled on the meta-level 
+   specifically as a 'bound variable'            *)
+
+  commute_0_equality  "(0 = a) = (a = 0)"
+
+  (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
+    [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
+  separate_bdvs_add   
+    "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
+		      			   \ ==> (a + b = c) = (b = c + -1*a)"
+  separate_bdvs0
+    "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0)  |]\
+		      			   \ ==> (a = b) = (a + -1*b = 0)"
+  separate_bdvs_add1  
+    "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\
+		      			   \ ==> (a = b + c) = (a + -1*c = b)"
+  separate_bdvs_add2
+    "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]\
+		      			   \ ==> (a + b = c) = (b = -1*a + c)"
+
+
+
+  separate_bdvs_mult  
+    "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
+		      			   \  ==>(a * b = c) = (b = c / a)"
+
+  (*requires rew_ord for termination, eg. ord_simplify_Integral;
+    works for lists of any length, interestingly !?!*)
+  order_system_NxN     "[a,b] = [b,a]"
+
+(*
+remove_thy"EqSystem";
+use_thy_only"Knowledge/EqSystem";
+use_thy"Knowledge/EqSystem";
+use"Knowledge/EqSystem.ML";
+  *)
+end
\ No newline at end of file