1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,50 @@
1.4 +(*. (c) by Richard Lang, 2003 .*)
1.5 +(* theory collecting all knowledge for LinearEquations
1.6 + created by: rlang
1.7 + date: 02.10
1.8 + changed by: rlang
1.9 + last change by: rlang
1.10 + date: 02.10.20
1.11 +*)
1.12 +
1.13 +(*
1.14 + use"knowledge/LinEq.ML";
1.15 + use"LinEq.ML";
1.16 +
1.17 + use"ROOT.ML";
1.18 + cd"knowledge";
1.19 +
1.20 +*)
1.21 +
1.22 +LinEq = Poly + Equation +
1.23 +
1.24 +(*-------------------- consts------------------------------------------------*)
1.25 +consts
1.26 + Solve'_lineq'_equation
1.27 + :: "[bool,real, \
1.28 + \ bool list] => bool list"
1.29 + ("((Script Solve'_lineq'_equation (_ _ =))// \
1.30 + \ (_))" 9)
1.31 +
1.32 +(*-------------------- rules -------------------------------------------------*)
1.33 +rules
1.34 +(*-- normalize --*)
1.35 + (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
1.36 + all_left
1.37 + "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
1.38 + makex1_x
1.39 + "a^^^1 = a"
1.40 + real_assoc_1
1.41 + "a+(b+c) = a+b+c"
1.42 + real_assoc_2
1.43 + "a*(b*c) = a*b*c"
1.44 +
1.45 +(*-- solve --*)
1.46 + lin_isolate_add1
1.47 + "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
1.48 + lin_isolate_add2
1.49 + "(a + bdv = 0) = ( bdv = (-1)*a)"
1.50 + lin_isolate_div
1.51 + "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
1.52 +end
1.53 +