1 (* use_thy"IsacKnowledge/Test";
4 Test = Atools + Rational + Root + Poly +
8 (*"cancel":: [real, real] => real (infixl "'/'/'/" 70) ...divide 2002*)
13 ("((Script Expand'_binomtest (_ =))// \
17 :: "[bool,real,bool, \
18 \ bool list] => bool list"
19 ("((Script Solve'_univar'_err (_ _ _ =))// \
24 \ bool list] => bool list"
25 ("((Script Solve'_linear (_ _ =))// \
28 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
30 "is'_root'_free" :: 'a => bool ("is'_root'_free _" 10)
31 "contains'_root" :: 'a => bool ("contains'_root _" 10)
35 \ bool list] => bool list"
36 ("((Script Solve'_root'_equation (_ _ =))// \
41 \ bool list] => bool list"
42 ("((Script Solve'_plain'_square (_ _ =))// \
45 Norm'_univar'_equation
48 ("((Script Norm'_univar'_equation (_ _ =))// \
54 ("((Script STest'_simplify (_ =))// \
57 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
59 rules (*stated as axioms, todo: prove as theorems*)
61 radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n"
62 rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n"
63 rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k"
64 rdistr_div_right "((k::real) + l) / n = k / n + l / n"
66 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
68 "m is_const ==> (n::real) + m * n = (1 + m) * n"
69 rcollect_one_left_assoc
70 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
71 rcollect_one_left_assoc_p
72 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
74 rtwo_of_the_same "a + a = 2 * a"
75 rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a"
76 rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"
78 rcancel_den "not(a=0) ==> a * (b / a) = b"
79 rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
80 rshift_nominator "(a::real) * b / c = a / c * b"
82 exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
83 rsqare "(a::real) * a = a ^^^ 2"
84 power_1 "(a::real) ^^^ 1 = a"
85 rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
87 rmult_1 "1 * k = (k::real)"
88 rmult_1_right "k * 1 = (k::real)"
89 rmult_0 "0 * k = (0::real)"
90 rmult_0_right "k * 0 = (0::real)"
91 radd_0 "0 + k = (k::real)"
92 radd_0_right "k + 0 = (k::real)"
95 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
97 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
100 radd_commute "(m::real) + (n::real) = n + m"
101 radd_left_commute "(x::real) + (y + z) = y + (x + z)"
102 radd_assoc "(m::real) + n + k = m + (n + k)"
103 rmult_commute "(m::real) * n = n * m"
104 rmult_left_commute "(x::real) * (y * z) = y * (x * z)"
105 rmult_assoc "(m::real) * n * k = m * (n * k)"
107 (*for equations: 'bdv' is a meta-constant*)
108 risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
109 risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
110 risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)"
113 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
115 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
116 root_ge0 "0 <= a ==> 0 <= sqrt a"
117 (*should be dropped with better simplification in eval_rls ...*)
119 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
121 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
126 rroot_square_inv "(sqrt a)^^^ 2 = a"
127 rroot_times_root "sqrt a * sqrt b = sqrt(a*b)"
128 rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
129 rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
132 (*for root-equations*)
134 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
135 square_equation_right
136 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
137 (*causes frequently non-termination:*)
139 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
141 risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
142 risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
143 risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)"
145 (*for polynomial equations of degree 2; linear case in RatArith*)
146 mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
147 constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
148 constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
151 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
153 "(x^^^2 = 0) = (x = 0)"
155 (*isolate root on the LEFT hand side of the equation
156 otherwise shuffling from left to right would not terminate*)
159 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
161 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
162 rroot_to_lhs_add_mult
163 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)