(* 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