(* use_thy"Knowledge/Test";

    *) 

 Test = Atools + Rational + Root + Poly + 

 consts

 (*"cancel":: [real, real] => real    (infixl "'/'/'/" 70) ...divide 2002*)

   Expand'_binomtest

              :: "['y, \

 		  \ 'y] => 'y"

                ("((Script Expand'_binomtest (_ =))// \

                  \ (_))" 9)

   Solve'_univar'_err

              :: "[bool,real,bool, \

 		  \ bool list] => bool list"

                ("((Script Solve'_univar'_err (_ _ _ =))// \

                  \ (_))" 9)

   Solve'_linear

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_linear (_ _ =))// \

                  \ (_))" 9)

 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)

   "is'_root'_free" :: 'a => bool           ("is'_root'_free _" 10)

   "contains'_root" :: 'a => bool           ("contains'_root _" 10)

   Solve'_root'_equation 

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_root'_equation (_ _ =))// \

                  \ (_))" 9)

   Solve'_plain'_square 

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_plain'_square (_ _ =))// \

                  \ (_))" 9)

   Norm'_univar'_equation 

              :: "[bool,real, \

 		  \ bool] => bool"

                ("((Script Norm'_univar'_equation (_ _ =))// \

                  \ (_))" 9)

   STest'_simplify

              :: "['z, \

 		  \ 'z] => 'z"

                ("((Script STest'_simplify (_ =))// \

                  \ (_))" 9)

 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)  

 rules (*stated as axioms, todo: prove as theorems*)

   radd_mult_distrib2      "(k::real) * (m + n) = k * m + k * n"

   rdistr_right_assoc      "(k::real) + l * n + m * n = k + (l + m) * n"

   rdistr_right_assoc_p    "l * n + (m * n + (k::real)) = (l + m) * n + k"

   rdistr_div_right        "((k::real) + l) / n = k / n + l / n"

   rcollect_right

           "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"

   rcollect_one_left

           "m is_const ==> (n::real) + m * n = (1 + m) * n"

   rcollect_one_left_assoc

           "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"

   rcollect_one_left_assoc_p

           "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"

   rtwo_of_the_same        "a + a = 2 * a"

   rtwo_of_the_same_assoc  "(x + a) + a = x + 2 * a"

   rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"

   rcancel_den             "not(a=0) ==> a * (b / a) = b"

   rcancel_const           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"

   rshift_nominator        "(a::real) * b / c = a / c * b"

   exp_pow                 "(a ^^^ b) ^^^ c = a ^^^ (b * c)"

   rsqare                  "(a::real) * a = a ^^^ 2"

   power_1                 "(a::real) ^^^ 1 = a"

   rbinom_power_2          "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"

   rmult_1                 "1 * k = (k::real)"

   rmult_1_right           "k * 1 = (k::real)"

   rmult_0                 "0 * k = (0::real)"

   rmult_0_right           "k * 0 = (0::real)"

   radd_0                  "0 + k = (k::real)"

   radd_0_right            "k + 0 = (k::real)"

   radd_real_const_eq

           "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"

   radd_real_const

           "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  

 (*for AC-operators*)

   radd_commute            "(m::real) + (n::real) = n + m"

   radd_left_commute       "(x::real) + (y + z) = y + (x + z)"

   radd_assoc              "(m::real) + n + k = m + (n + k)"

   rmult_commute           "(m::real) * n = n * m"

   rmult_left_commute      "(x::real) * (y * z) = y * (x * z)"

   rmult_assoc             "(m::real) * n * k = m * (n * k)"

 (*for equations: 'bdv' is a meta-constant*)

   risolate_bdv_add       "((k::real) + bdv = m) = (bdv = m + (-1)*k)"

   risolate_bdv_mult_add  "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"

   risolate_bdv_mult      "((n::real) * bdv = m) = (bdv = m / n)"

   rnorm_equation_add

       "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"

 (*17.9.02 aus SqRoot.thy------------------------------vvv---*) 

   root_ge0            "0 <= a ==> 0 <= sqrt a"

   (*should be dropped with better simplification in eval_rls ...*)

   root_add_ge0

 	"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"

   root_ge0_1

 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"

   root_ge0_2

 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"

   rroot_square_inv         "(sqrt a)^^^ 2 = a"

   rroot_times_root         "sqrt a * sqrt b = sqrt(a*b)"

   rroot_times_root_assoc   "(a * sqrt b) * sqrt c = a * sqrt(b*c)"

   rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"

 (*for root-equations*)

   square_equation_left

           "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"

   square_equation_right

           "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"

   (*causes frequently non-termination:*)

   square_equation  

           "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"

   risolate_root_add        "(a+  sqrt c = d) = (  sqrt c = d + (-1)*a)"

   risolate_root_mult       "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"

   risolate_root_div        "(a * sqrt c = d) = (  sqrt c = d / a)"

 (*for polynomial equations of degree 2; linear case in RatArith*)

   mult_square		"(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"

   constant_square       "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"

   constant_mult_square  "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"

   square_equality 

 	     "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"

   square_equality_0

 	     "(x^^^2 = 0) = (x = 0)"

 (*isolate root on the LEFT hand side of the equation

   otherwise shuffling from left to right would not terminate*)  

   rroot_to_lhs

           "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"

   rroot_to_lhs_mult

           "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"

   rroot_to_lhs_add_mult

           "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"

 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)  

 end