1.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 15:53:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 16:56:22 2010 +0200
1.3 @@ -60,108 +60,108 @@
1.4
1.5 axioms (*TODO: prove as theorems*)
1.6
1.7 - radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n"
1.8 - rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n"
1.9 - rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k"
1.10 - rdistr_div_right "((k::real) + l) / n = k / n + l / n"
1.11 - rcollect_right
1.12 + radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n"
1.13 + rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n"
1.14 + rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k"
1.15 + rdistr_div_right: "((k::real) + l) / n = k / n + l / n"
1.16 + rcollect_right:
1.17 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
1.18 - rcollect_one_left
1.19 + rcollect_one_left:
1.20 "m is_const ==> (n::real) + m * n = (1 + m) * n"
1.21 - rcollect_one_left_assoc
1.22 + rcollect_one_left_assoc:
1.23 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
1.24 - rcollect_one_left_assoc_p
1.25 + rcollect_one_left_assoc_p:
1.26 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
1.27
1.28 - rtwo_of_the_same "a + a = 2 * a"
1.29 - rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a"
1.30 - rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"
1.31 + rtwo_of_the_same: "a + a = 2 * a"
1.32 + rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a"
1.33 + rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x"
1.34
1.35 - rcancel_den "not(a=0) ==> a * (b / a) = b"
1.36 - rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
1.37 - rshift_nominator "(a::real) * b / c = a / c * b"
1.38 + rcancel_den: "not(a=0) ==> a * (b / a) = b"
1.39 + rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
1.40 + rshift_nominator: "(a::real) * b / c = a / c * b"
1.41
1.42 - exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
1.43 - rsqare "(a::real) * a = a ^^^ 2"
1.44 - power_1 "(a::real) ^^^ 1 = a"
1.45 - rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
1.46 + exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
1.47 + rsqare: "(a::real) * a = a ^^^ 2"
1.48 + power_1: "(a::real) ^^^ 1 = a"
1.49 + rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
1.50
1.51 - rmult_1 "1 * k = (k::real)"
1.52 - rmult_1_right "k * 1 = (k::real)"
1.53 - rmult_0 "0 * k = (0::real)"
1.54 - rmult_0_right "k * 0 = (0::real)"
1.55 - radd_0 "0 + k = (k::real)"
1.56 - radd_0_right "k + 0 = (k::real)"
1.57 + rmult_1: "1 * k = (k::real)"
1.58 + rmult_1_right: "k * 1 = (k::real)"
1.59 + rmult_0: "0 * k = (0::real)"
1.60 + rmult_0_right: "k * 0 = (0::real)"
1.61 + radd_0: "0 + k = (k::real)"
1.62 + radd_0_right: "k + 0 = (k::real)"
1.63
1.64 - radd_real_const_eq
1.65 + radd_real_const_eq:
1.66 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
1.67 - radd_real_const
1.68 + radd_real_const:
1.69 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
1.70
1.71 (*for AC-operators*)
1.72 - radd_commute "(m::real) + (n::real) = n + m"
1.73 - radd_left_commute "(x::real) + (y + z) = y + (x + z)"
1.74 - radd_assoc "(m::real) + n + k = m + (n + k)"
1.75 - rmult_commute "(m::real) * n = n * m"
1.76 - rmult_left_commute "(x::real) * (y * z) = y * (x * z)"
1.77 - rmult_assoc "(m::real) * n * k = m * (n * k)"
1.78 + radd_commute: "(m::real) + (n::real) = n + m"
1.79 + radd_left_commute: "(x::real) + (y + z) = y + (x + z)"
1.80 + radd_assoc: "(m::real) + n + k = m + (n + k)"
1.81 + rmult_commute: "(m::real) * n = n * m"
1.82 + rmult_left_commute: "(x::real) * (y * z) = y * (x * z)"
1.83 + rmult_assoc: "(m::real) * n * k = m * (n * k)"
1.84
1.85 (*for equations: 'bdv' is a meta-constant*)
1.86 - risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
1.87 - risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
1.88 - risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)"
1.89 + risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
1.90 + risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
1.91 + risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)"
1.92
1.93 - rnorm_equation_add
1.94 + rnorm_equation_add:
1.95 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
1.96
1.97 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
1.98 - root_ge0 "0 <= a ==> 0 <= sqrt a"
1.99 + root_ge0: "0 <= a ==> 0 <= sqrt a"
1.100 (*should be dropped with better simplification in eval_rls ...*)
1.101 - root_add_ge0
1.102 + root_add_ge0:
1.103 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
1.104 - root_ge0_1
1.105 + root_ge0_1:
1.106 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
1.107 - root_ge0_2
1.108 + root_ge0_2:
1.109 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
1.110
1.111
1.112 - rroot_square_inv "(sqrt a)^^^ 2 = a"
1.113 - rroot_times_root "sqrt a * sqrt b = sqrt(a*b)"
1.114 - rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
1.115 - rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
1.116 + rroot_square_inv: "(sqrt a)^^^ 2 = a"
1.117 + rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)"
1.118 + rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
1.119 + rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
1.120
1.121
1.122 (*for root-equations*)
1.123 - square_equation_left
1.124 + square_equation_left:
1.125 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
1.126 - square_equation_right
1.127 + square_equation_right:
1.128 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
1.129 (*causes frequently non-termination:*)
1.130 - square_equation
1.131 + square_equation:
1.132 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
1.133
1.134 - risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
1.135 - risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
1.136 - risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)"
1.137 + risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
1.138 + risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
1.139 + risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)"
1.140
1.141 (*for polynomial equations of degree 2; linear case in RatArith*)
1.142 - mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
1.143 - constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
1.144 - constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
1.145 + mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
1.146 + constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
1.147 + constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
1.148
1.149 - square_equality
1.150 + square_equality:
1.151 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
1.152 - square_equality_0
1.153 + square_equality_0:
1.154 "(x^^^2 = 0) = (x = 0)"
1.155
1.156 (*isolate root on the LEFT hand side of the equation
1.157 otherwise shuffling from left to right would not terminate*)
1.158
1.159 - rroot_to_lhs
1.160 + rroot_to_lhs:
1.161 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
1.162 - rroot_to_lhs_mult
1.163 + rroot_to_lhs_mult:
1.164 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
1.165 - rroot_to_lhs_add_mult
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 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
1.169