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