1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Test.thy	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,170 @@
     1.4 +(* arithmetic on rationals
     1.5 +   WN.22.10.99
     1.6 + *) 
     1.7 +
     1.8 +Test = Atools + Rational + Root + Poly + 
     1.9 + 
    1.10 +consts
    1.11 +
    1.12 +(*"cancel":: [real, real] => real    (infixl "'/'/'/" 70) ...divide 2002*)
    1.13 +
    1.14 +  Expand'_binomtest
    1.15 +             :: "['y, \
    1.16 +		  \ 'y] => 'y"
    1.17 +               ("((Script Expand'_binomtest (_ =))// \
    1.18 +                 \ (_))" 9)
    1.19 +
    1.20 +  Solve'_univar'_err
    1.21 +             :: "[bool,real,bool, \
    1.22 +		  \ bool list] => bool list"
    1.23 +               ("((Script Solve'_univar'_err (_ _ _ =))// \
    1.24 +                 \ (_))" 9)
    1.25 +  
    1.26 +  Solve'_linear
    1.27 +             :: "[bool,real, \
    1.28 +		  \ bool list] => bool list"
    1.29 +               ("((Script Solve'_linear (_ _ =))// \
    1.30 +                 \ (_))" 9)
    1.31 +
    1.32 +(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
    1.33 +
    1.34 +  "is'_root'_free" :: 'a => bool           ("is'_root'_free _" 10)
    1.35 +  "contains'_root" :: 'a => bool           ("contains'_root _" 10)
    1.36 +
    1.37 +  Solve'_root'_equation 
    1.38 +             :: "[bool,real,bool, \
    1.39 +		  \ bool list] => bool list"
    1.40 +               ("((Script Solve'_root'_equation (_ _ _ =))// \
    1.41 +                 \ (_))" 9)
    1.42 +
    1.43 +  Solve'_plain'_square 
    1.44 +             :: "[bool,real, \
    1.45 +		  \ bool list] => bool list"
    1.46 +               ("((Script Solve'_plain'_square (_ _ =))// \
    1.47 +                 \ (_))" 9)
    1.48 +
    1.49 +  Norm'_univar'_equation 
    1.50 +             :: "[bool,real, \
    1.51 +		  \ bool] => bool"
    1.52 +               ("((Script Norm'_univar'_equation (_ _ =))// \
    1.53 +                 \ (_))" 9)
    1.54 +
    1.55 +  STest'_simplify
    1.56 +             :: "[real, \
    1.57 +		  \ real] => real"
    1.58 +               ("((Script STest'_simplify (_ =))// \
    1.59 +                 \ (_))" 9)
    1.60 +
    1.61 +(*17.9.02 aus SqRoot.thy------------------------------^^^---*)  
    1.62 +
    1.63 +rules (*stated as axioms, todo: prove as theorems*)
    1.64 +
    1.65 +  radd_mult_distrib2      "(k::real) * (m + n) = k * m + k * n"
    1.66 +  rdistr_right_assoc      "(k::real) + l * n + m * n = k + (l + m) * n"
    1.67 +  rdistr_right_assoc_p    "l * n + (m * n + (k::real)) = (l + m) * n + k"
    1.68 +  rdistr_div_right        "((k::real) + l) / n = k / n + l / n"
    1.69 +  rcollect_right
    1.70 +          "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
    1.71 +  rcollect_one_left
    1.72 +          "m is_const ==> (n::real) + m * n = (1 + m) * n"
    1.73 +  rcollect_one_left_assoc
    1.74 +          "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
    1.75 +  rcollect_one_left_assoc_p
    1.76 +          "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
    1.77 +
    1.78 +  rtwo_of_the_same        "a + a = 2 * a"
    1.79 +  rtwo_of_the_same_assoc  "(x + a) + a = x + 2 * a"
    1.80 +  rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"
    1.81 +
    1.82 +  rcancel_den             "not(a=0) ==> a * (b / a) = b"
    1.83 +  rcancel_const           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
    1.84 +  rshift_nominator        "(a::real) * b / c = a / c * b"
    1.85 +
    1.86 +  exp_pow                 "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
    1.87 +  rsqare                  "(a::real) * a = a ^^^ 2"
    1.88 +  power_1                 "(a::real) ^^^ 1 = a"
    1.89 +  rbinom_power_2          "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
    1.90 +
    1.91 +  rmult_1                 "1 * k = (k::real)"
    1.92 +  rmult_1_right           "k * 1 = (k::real)"
    1.93 +  rmult_0                 "0 * k = (0::real)"
    1.94 +  rmult_0_right           "k * 0 = (0::real)"
    1.95 +  radd_0                  "0 + k = (k::real)"
    1.96 +  radd_0_right            "k + 0 = (k::real)"
    1.97 +
    1.98 +  radd_real_const_eq
    1.99 +          "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
   1.100 +  radd_real_const
   1.101 +          "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  
   1.102 +  
   1.103 +(*for AC-operators*)
   1.104 +  radd_commute            "(m::real) + (n::real) = n + m"
   1.105 +  radd_left_commute       "(x::real) + (y + z) = y + (x + z)"
   1.106 +  radd_assoc              "(m::real) + n + k = m + (n + k)"
   1.107 +  rmult_commute           "(m::real) * n = n * m"
   1.108 +  rmult_left_commute      "(x::real) * (y * z) = y * (x * z)"
   1.109 +  rmult_assoc             "(m::real) * n * k = m * (n * k)"
   1.110 +
   1.111 +(*for equations: 'bdv' is a meta-constant*)
   1.112 +  risolate_bdv_add       "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
   1.113 +  risolate_bdv_mult_add  "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
   1.114 +  risolate_bdv_mult      "((n::real) * bdv = m) = (bdv = m / n)"
   1.115 +
   1.116 +  rnorm_equation_add
   1.117 +      "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
   1.118 +
   1.119 +(*17.9.02 aus SqRoot.thy------------------------------vvv---*) 
   1.120 +  root_ge0            "0 <= a ==> 0 <= sqrt a"
   1.121 +  (*should be dropped with better simplification in eval_rls ...*)
   1.122 +  root_add_ge0
   1.123 +	"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
   1.124 +  root_ge0_1
   1.125 +	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
   1.126 +  root_ge0_2
   1.127 +	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
   1.128 +
   1.129 +
   1.130 +  rroot_square_inv         "(sqrt a)^^^ 2 = a"
   1.131 +  rroot_times_root         "sqrt a * sqrt b = sqrt(a*b)"
   1.132 +  rroot_times_root_assoc   "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
   1.133 +  rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
   1.134 +
   1.135 +
   1.136 +(*for root-equations*)
   1.137 +  square_equation_left
   1.138 +          "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
   1.139 +  square_equation_right
   1.140 +          "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
   1.141 +  (*causes frequently non-termination:*)
   1.142 +  square_equation  
   1.143 +          "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
   1.144 +  
   1.145 +  risolate_root_add        "(a+  sqrt c = d) = (  sqrt c = d + (-1)*a)"
   1.146 +  risolate_root_mult       "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
   1.147 +  risolate_root_div        "(a * sqrt c = d) = (  sqrt c = d / a)"
   1.148 +
   1.149 +(*for polynomial equations of degree 2; linear case in RatArith*)
   1.150 +  mult_square		"(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
   1.151 +  constant_square       "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
   1.152 +  constant_mult_square  "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
   1.153 +
   1.154 +  square_equality 
   1.155 +	     "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
   1.156 +  square_equality_0
   1.157 +	     "(x^^^2 = 0) = (x = 0)"
   1.158 +
   1.159 +(*isolate root on the LEFT hand side of the equation
   1.160 +  otherwise shuffling from left to right would not terminate*)  
   1.161 +
   1.162 +  rroot_to_lhs
   1.163 +          "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
   1.164 +  rroot_to_lhs_mult
   1.165 +          "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
   1.166 +  rroot_to_lhs_add_mult
   1.167 +          "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
   1.168 +
   1.169 + 
   1.170 +(*17.9.02 aus SqRoot.thy------------------------------^^^---*)  
   1.171 +
   1.172 +
   1.173 +end