1.1 --- a/src/Tools/isac/IsacKnowledge/EqSystem.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,72 +0,0 @@
     1.4 -(* equational systems, minimal -- for use in Biegelinie
     1.5 -   author: Walther Neuper
     1.6 -   050826,
     1.7 -   (c) due to copyright terms
     1.8 -
     1.9 -remove_thy"EqSystem";
    1.10 -use_thy"IsacKnowledge/EqSystem";
    1.11 -
    1.12 -use_thy_only"IsacKnowledge/EqSystem";
    1.13 -
    1.14 -remove_thy"Typefix";
    1.15 -use_thy"IsacKnowledge/Isac";
    1.16 -*)
    1.17 -
    1.18 -EqSystem = Rational + Root +
    1.19 -
    1.20 -consts
    1.21 -
    1.22 -  occur'_exactly'_in :: 
    1.23 -   "[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _")
    1.24 -
    1.25 -  (*descriptions in the related problems*)
    1.26 -  solveForVars       :: real list => toreall
    1.27 -  solution           :: bool list => toreall
    1.28 -
    1.29 -  (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
    1.30 -  solveSystem        :: "[bool list, real list] => bool list"
    1.31 -
    1.32 -  (*Script-names*)
    1.33 -  SolveSystemScript  :: "[bool list, real list,     bool list] \
    1.34 -						\=> bool list"
    1.35 -                  ("((Script SolveSystemScript (_ _ =))// (_))" 9)
    1.36 -
    1.37 -rules 
    1.38 -(*stated as axioms, todo: prove as theorems
    1.39 -  'bdv' is a constant handled on the meta-level 
    1.40 -   specifically as a 'bound variable'            *)
    1.41 -
    1.42 -  commute_0_equality  "(0 = a) = (a = 0)"
    1.43 -
    1.44 -  (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
    1.45 -    [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
    1.46 -  separate_bdvs_add   
    1.47 -    "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
    1.48 -		      			   \ ==> (a + b = c) = (b = c + -1*a)"
    1.49 -  separate_bdvs0
    1.50 -    "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0)  |]\
    1.51 -		      			   \ ==> (a = b) = (a + -1*b = 0)"
    1.52 -  separate_bdvs_add1  
    1.53 -    "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\
    1.54 -		      			   \ ==> (a = b + c) = (a + -1*c = b)"
    1.55 -  separate_bdvs_add2
    1.56 -    "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]\
    1.57 -		      			   \ ==> (a + b = c) = (b = -1*a + c)"
    1.58 -
    1.59 -
    1.60 -
    1.61 -  separate_bdvs_mult  
    1.62 -    "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
    1.63 -		      			   \  ==>(a * b = c) = (b = c / a)"
    1.64 -
    1.65 -  (*requires rew_ord for termination, eg. ord_simplify_Integral;
    1.66 -    works for lists of any length, interestingly !?!*)
    1.67 -  order_system_NxN     "[a,b] = [b,a]"
    1.68 -
    1.69 -(*
    1.70 -remove_thy"EqSystem";
    1.71 -use_thy_only"IsacKnowledge/EqSystem";
    1.72 -use_thy"IsacKnowledge/EqSystem";
    1.73 -use"IsacKnowledge/EqSystem.ML";
    1.74 -  *)
    1.75 -end
    1.76 \ No newline at end of file