| author | Walther Neuper <neuper@ist.tugraz.at> |
| Wed, 25 Aug 2010 16:20:07 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 37947 | 22235e4dbe5f |
| parent 37906 | src/Tools/isac/IsacKnowledge/LinEq.thy@e2b23ba9df13 |
| child 37950 | 525a28152a67 |
| permissions | -rw-r--r-- |
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 *)
10 (*
11 use"knowledge/LinEq.ML";
12 use"LinEq.ML";
14 use"ROOT.ML";
15 cd"knowledge";
17 *)
19 LinEq = Poly + Equation +
21 (*-------------------- consts------------------------------------------------*)
22 consts
23 Solve'_lineq'_equation
24 :: "[bool,real, \
25 \ bool list] => bool list"
26 ("((Script Solve'_lineq'_equation (_ _ =))// \
27 \ (_))" 9)
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"
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