equal
deleted
inserted
replaced
1 (*.c) by Richard Lang, 2003 .*) |
|
2 (* collecting all knowledge for Root and Rational Equations |
|
3 created by: rlang |
|
4 date: 02.10 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.04 |
|
8 *) |
|
9 |
|
10 (* use"knowledge/RootRatEq.ML"; |
|
11 use"RootRatEq.ML"; |
|
12 |
|
13 use"ROOT.ML"; |
|
14 cd"knowledge"; |
|
15 |
|
16 remove_thy"RootRatEq"; |
|
17 use_thy"Isac"; |
|
18 *) |
|
19 |
|
20 RootRatEq = RootEq + RatEq + RootRat + |
|
21 |
|
22 (*-------------------- consts-----------------------------------------------*) |
|
23 consts |
|
24 |
|
25 is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*) |
|
26 |
|
27 (*---------scripts--------------------------*) |
|
28 Elim'_rootrat'_equation |
|
29 :: "[bool,real, \ |
|
30 \ bool list] => bool list" |
|
31 ("((Script Elim'_rootrat'_equation (_ _ =))// \ |
|
32 \ (_))" 9) |
|
33 (*-------------------- rules------------------------------------------------*) |
|
34 rules |
|
35 |
|
36 (* eliminate ratRootTerm *) |
|
37 rootrat_equation_left_1 |
|
38 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" |
|
39 rootrat_equation_left_2 |
|
40 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" |
|
41 rootrat_equation_right_2 |
|
42 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" |
|
43 rootrat_equation_right_1 |
|
44 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))" |
|
45 |
|
46 |
|
47 |
|
48 end |
|