equal
deleted
inserted
replaced
1 (*. (c) by Richard Lang, 2003 .*) |
|
2 (* theory collecting all knowledge for LinearEquations |
|
3 created by: rlang |
|
4 date: 02.10 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.10.20 |
|
8 *) |
|
9 |
|
10 (* |
|
11 use"knowledge/LinEq.ML"; |
|
12 use"LinEq.ML"; |
|
13 |
|
14 use"ROOT.ML"; |
|
15 cd"knowledge"; |
|
16 |
|
17 *) |
|
18 |
|
19 LinEq = Poly + Equation + |
|
20 |
|
21 (*-------------------- consts------------------------------------------------*) |
|
22 consts |
|
23 Solve'_lineq'_equation |
|
24 :: "[bool,real, \ |
|
25 \ bool list] => bool list" |
|
26 ("((Script Solve'_lineq'_equation (_ _ =))// \ |
|
27 \ (_))" 9) |
|
28 |
|
29 (*-------------------- rules -------------------------------------------------*) |
|
30 rules |
|
31 (*-- normalize --*) |
|
32 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*) |
|
33 all_left |
|
34 "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" |
|
35 makex1_x |
|
36 "a^^^1 = a" |
|
37 real_assoc_1 |
|
38 "a+(b+c) = a+b+c" |
|
39 real_assoc_2 |
|
40 "a*(b*c) = a*b*c" |
|
41 |
|
42 (*-- solve --*) |
|
43 lin_isolate_add1 |
|
44 "(a + b*bdv = 0) = (b*bdv = (-1)*a)" |
|
45 lin_isolate_add2 |
|
46 "(a + bdv = 0) = ( bdv = (-1)*a)" |
|
47 lin_isolate_div |
|
48 "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)" |
|
49 end |
|
50 |
|