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