1 (* use_thy"IsacKnowledge/Test"; |
|
2 *) |
|
3 |
|
4 Test = Atools + Rational + Root + Poly + |
|
5 |
|
6 consts |
|
7 |
|
8 (*"cancel":: [real, real] => real (infixl "'/'/'/" 70) ...divide 2002*) |
|
9 |
|
10 Expand'_binomtest |
|
11 :: "['y, \ |
|
12 \ 'y] => 'y" |
|
13 ("((Script Expand'_binomtest (_ =))// \ |
|
14 \ (_))" 9) |
|
15 |
|
16 Solve'_univar'_err |
|
17 :: "[bool,real,bool, \ |
|
18 \ bool list] => bool list" |
|
19 ("((Script Solve'_univar'_err (_ _ _ =))// \ |
|
20 \ (_))" 9) |
|
21 |
|
22 Solve'_linear |
|
23 :: "[bool,real, \ |
|
24 \ bool list] => bool list" |
|
25 ("((Script Solve'_linear (_ _ =))// \ |
|
26 \ (_))" 9) |
|
27 |
|
28 (*17.9.02 aus SqRoot.thy------------------------------vvv---*) |
|
29 |
|
30 "is'_root'_free" :: 'a => bool ("is'_root'_free _" 10) |
|
31 "contains'_root" :: 'a => bool ("contains'_root _" 10) |
|
32 |
|
33 Solve'_root'_equation |
|
34 :: "[bool,real, \ |
|
35 \ bool list] => bool list" |
|
36 ("((Script Solve'_root'_equation (_ _ =))// \ |
|
37 \ (_))" 9) |
|
38 |
|
39 Solve'_plain'_square |
|
40 :: "[bool,real, \ |
|
41 \ bool list] => bool list" |
|
42 ("((Script Solve'_plain'_square (_ _ =))// \ |
|
43 \ (_))" 9) |
|
44 |
|
45 Norm'_univar'_equation |
|
46 :: "[bool,real, \ |
|
47 \ bool] => bool" |
|
48 ("((Script Norm'_univar'_equation (_ _ =))// \ |
|
49 \ (_))" 9) |
|
50 |
|
51 STest'_simplify |
|
52 :: "['z, \ |
|
53 \ 'z] => 'z" |
|
54 ("((Script STest'_simplify (_ =))// \ |
|
55 \ (_))" 9) |
|
56 |
|
57 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
|
58 |
|
59 rules (*stated as axioms, todo: prove as theorems*) |
|
60 |
|
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" |
|
65 rcollect_right |
|
66 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" |
|
67 rcollect_one_left |
|
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" |
|
73 |
|
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" |
|
77 |
|
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" |
|
81 |
|
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" |
|
86 |
|
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)" |
|
93 |
|
94 radd_real_const_eq |
|
95 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" |
|
96 radd_real_const |
|
97 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))" |
|
98 |
|
99 (*for AC-operators*) |
|
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)" |
|
106 |
|
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)" |
|
111 |
|
112 rnorm_equation_add |
|
113 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" |
|
114 |
|
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 ...*) |
|
118 root_add_ge0 |
|
119 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" |
|
120 root_ge0_1 |
|
121 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" |
|
122 root_ge0_2 |
|
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" |
|
124 |
|
125 |
|
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" |
|
130 |
|
131 |
|
132 (*for root-equations*) |
|
133 square_equation_left |
|
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:*) |
|
138 square_equation |
|
139 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" |
|
140 |
|
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)" |
|
144 |
|
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)" |
|
149 |
|
150 square_equality |
|
151 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" |
|
152 square_equality_0 |
|
153 "(x^^^2 = 0) = (x = 0)" |
|
154 |
|
155 (*isolate root on the LEFT hand side of the equation |
|
156 otherwise shuffling from left to right would not terminate*) |
|
157 |
|
158 rroot_to_lhs |
|
159 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" |
|
160 rroot_to_lhs_mult |
|
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)" |
|
164 |
|
165 |
|
166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
|
167 |
|
168 |
|
169 end |
|