1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*.(c) by Richard Lang, 2003 .*)
     1.5 +(* theory collecting all knowledge for RationalEquations
     1.6 +   created by: rlang 
     1.7 +         date: 02.08.12
     1.8 +   changed by: rlang
     1.9 +   last change by: rlang
    1.10 +             date: 02.11.28
    1.11 +*)
    1.12 +
    1.13 +(*
    1.14 +   RL.020812
    1.15 +   use_thy"knowledge/RatEq";
    1.16 +   use_thy"RatEq";
    1.17 +   use_thy_only"RatEq";
    1.18 +
    1.19 +   remove_thy"RatEq";
    1.20 +   use_thy"Isac";
    1.21 +
    1.22 +   use"ROOT.ML";
    1.23 +   cd"knowledge";
    1.24 + *)
    1.25 +RatEq = Rational +
    1.26 +
    1.27 +(*-------------------- consts------------------------------------------------*)
    1.28 +consts
    1.29 +
    1.30 +  is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
    1.31 +
    1.32 +  (*----------------------scripts-----------------------*)
    1.33 +  Solve'_rat'_equation
    1.34 +             :: "[bool,real, \
    1.35 +		  \ bool list] => bool list"
    1.36 +               ("((Script Solve'_rat'_equation (_ _ =))// \
    1.37 +                 \ (_))" 9)
    1.38 +
    1.39 +(*-------------------- rules------------------------------------------------*)
    1.40 +rules 
    1.41 +   (* FIXME also in Poly.thy def. --> FIXED*)
    1.42 +   (*real_diff_minus            
    1.43 +   "a - b = a + (-1) * b"*)
    1.44 +   real_rat_mult_1
    1.45 +   "a*(b/c) = (a*b)/c"
    1.46 +   real_rat_mult_2
    1.47 +   "(a/b)*(c/d) = (a*c)/(b*d)"
    1.48 +   real_rat_mult_3
    1.49 +   "(a/b)*c = (a*c)/b"
    1.50 +   real_rat_pow
    1.51 +   "(a/b)^^^2 = a^^^2/b^^^2"
    1.52 +
    1.53 +   rat_double_rat_1
    1.54 +   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
    1.55 +   rat_double_rat_2
    1.56 +   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"
    1.57 +   rat_double_rat_3
    1.58 +   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
    1.59 +
    1.60 +
    1.61 +  (* equation to same denominator *)
    1.62 +  rat_mult_denominator_both
    1.63 +   "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
    1.64 +  rat_mult_denominator_left
    1.65 +   "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
    1.66 +  rat_mult_denominator_right
    1.67 +   "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
    1.68 +
    1.69 +
    1.70 +end