equal
deleted
inserted
replaced
1 (*.(c) by Richard Lang, 2003 .*) |
|
2 (* theory collecting all knowledge for RationalEquations |
|
3 created by: rlang |
|
4 date: 02.08.12 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.28 |
|
8 *) |
|
9 |
|
10 (* |
|
11 RL.020812 |
|
12 use_thy"knowledge/RatEq"; |
|
13 use_thy"RatEq"; |
|
14 use_thy_only"RatEq"; |
|
15 |
|
16 remove_thy"RatEq"; |
|
17 use_thy"Isac"; |
|
18 |
|
19 use"ROOT.ML"; |
|
20 cd"knowledge"; |
|
21 *) |
|
22 RatEq = Rational + |
|
23 |
|
24 (*-------------------- consts------------------------------------------------*) |
|
25 consts |
|
26 |
|
27 is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _") |
|
28 |
|
29 (*----------------------scripts-----------------------*) |
|
30 Solve'_rat'_equation |
|
31 :: "[bool,real, \ |
|
32 \ bool list] => bool list" |
|
33 ("((Script Solve'_rat'_equation (_ _ =))// \ |
|
34 \ (_))" 9) |
|
35 |
|
36 (*-------------------- rules------------------------------------------------*) |
|
37 rules |
|
38 (* FIXME also in Poly.thy def. --> FIXED*) |
|
39 (*real_diff_minus |
|
40 "a - b = a + (-1) * b"*) |
|
41 real_rat_mult_1 |
|
42 "a*(b/c) = (a*b)/c" |
|
43 real_rat_mult_2 |
|
44 "(a/b)*(c/d) = (a*c)/(b*d)" |
|
45 real_rat_mult_3 |
|
46 "(a/b)*c = (a*c)/b" |
|
47 real_rat_pow |
|
48 "(a/b)^^^2 = a^^^2/b^^^2" |
|
49 |
|
50 rat_double_rat_1 |
|
51 "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" |
|
52 rat_double_rat_2 |
|
53 "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))" |
|
54 rat_double_rat_3 |
|
55 "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" |
|
56 |
|
57 |
|
58 (* equation to same denominator *) |
|
59 rat_mult_denominator_both |
|
60 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" |
|
61 rat_mult_denominator_left |
|
62 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" |
|
63 rat_mult_denominator_right |
|
64 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)" |
|
65 |
|
66 |
|
67 end |
|