neuper@37906
|
1 |
(* equational systems, minimal -- for use in Biegelinie
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
050826,
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
remove_thy"EqSystem";
|
neuper@37906
|
7 |
use_thy"IsacKnowledge/EqSystem";
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
use_thy_only"IsacKnowledge/EqSystem";
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
remove_thy"Typefix";
|
neuper@37906
|
12 |
use_thy"IsacKnowledge/Isac";
|
neuper@37906
|
13 |
*)
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
EqSystem = Rational + Root +
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
consts
|
neuper@37906
|
18 |
|
neuper@37906
|
19 |
occur'_exactly'_in ::
|
neuper@37906
|
20 |
"[real list, real list, 'a] => bool" ("_ from'_ _ occur'_exactly'_in _")
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
(*descriptions in the related problems*)
|
neuper@37906
|
23 |
solveForVars :: real list => toreall
|
neuper@37906
|
24 |
solution :: bool list => toreall
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
(*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
|
neuper@37906
|
27 |
solveSystem :: "[bool list, real list] => bool list"
|
neuper@37906
|
28 |
|
neuper@37906
|
29 |
(*Script-names*)
|
neuper@37906
|
30 |
SolveSystemScript :: "[bool list, real list, bool list] \
|
neuper@37906
|
31 |
\=> bool list"
|
neuper@37906
|
32 |
("((Script SolveSystemScript (_ _ =))// (_))" 9)
|
neuper@37906
|
33 |
|
neuper@37906
|
34 |
rules
|
neuper@37906
|
35 |
(*stated as axioms, todo: prove as theorems
|
neuper@37906
|
36 |
'bdv' is a constant handled on the meta-level
|
neuper@37906
|
37 |
specifically as a 'bound variable' *)
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
commute_0_equality "(0 = a) = (a = 0)"
|
neuper@37906
|
40 |
|
neuper@37906
|
41 |
(*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
|
neuper@37906
|
42 |
[bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
|
neuper@37906
|
43 |
separate_bdvs_add
|
neuper@37906
|
44 |
"[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
|
neuper@37906
|
45 |
\ ==> (a + b = c) = (b = c + -1*a)"
|
neuper@37906
|
46 |
separate_bdvs0
|
neuper@37906
|
47 |
"[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]\
|
neuper@37906
|
48 |
\ ==> (a = b) = (a + -1*b = 0)"
|
neuper@37906
|
49 |
separate_bdvs_add1
|
neuper@37906
|
50 |
"[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\
|
neuper@37906
|
51 |
\ ==> (a = b + c) = (a + -1*c = b)"
|
neuper@37906
|
52 |
separate_bdvs_add2
|
neuper@37906
|
53 |
"[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]\
|
neuper@37906
|
54 |
\ ==> (a + b = c) = (b = -1*a + c)"
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
separate_bdvs_mult
|
neuper@37906
|
59 |
"[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
|
neuper@37906
|
60 |
\ ==>(a * b = c) = (b = c / a)"
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
(*requires rew_ord for termination, eg. ord_simplify_Integral;
|
neuper@37906
|
63 |
works for lists of any length, interestingly !?!*)
|
neuper@37906
|
64 |
order_system_NxN "[a,b] = [b,a]"
|
neuper@37906
|
65 |
|
neuper@37906
|
66 |
(*
|
neuper@37906
|
67 |
remove_thy"EqSystem";
|
neuper@37906
|
68 |
use_thy_only"IsacKnowledge/EqSystem";
|
neuper@37906
|
69 |
use_thy"IsacKnowledge/EqSystem";
|
neuper@37906
|
70 |
use"IsacKnowledge/EqSystem.ML";
|
neuper@37906
|
71 |
*)
|
neuper@37906
|
72 |
end |