neuper@37947
|
1 |
(* use_thy"Knowledge/Test";
|
neuper@37906
|
2 |
*)
|
neuper@37906
|
3 |
|
neuper@37906
|
4 |
Test = Atools + Rational + Root + Poly +
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
consts
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
(*"cancel":: [real, real] => real (infixl "'/'/'/" 70) ...divide 2002*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
Expand'_binomtest
|
neuper@37906
|
11 |
:: "['y, \
|
neuper@37906
|
12 |
\ 'y] => 'y"
|
neuper@37906
|
13 |
("((Script Expand'_binomtest (_ =))// \
|
neuper@37906
|
14 |
\ (_))" 9)
|
neuper@37906
|
15 |
|
neuper@37906
|
16 |
Solve'_univar'_err
|
neuper@37906
|
17 |
:: "[bool,real,bool, \
|
neuper@37906
|
18 |
\ bool list] => bool list"
|
neuper@37906
|
19 |
("((Script Solve'_univar'_err (_ _ _ =))// \
|
neuper@37906
|
20 |
\ (_))" 9)
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
Solve'_linear
|
neuper@37906
|
23 |
:: "[bool,real, \
|
neuper@37906
|
24 |
\ bool list] => bool list"
|
neuper@37906
|
25 |
("((Script Solve'_linear (_ _ =))// \
|
neuper@37906
|
26 |
\ (_))" 9)
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
|
neuper@37906
|
29 |
|
neuper@37906
|
30 |
"is'_root'_free" :: 'a => bool ("is'_root'_free _" 10)
|
neuper@37906
|
31 |
"contains'_root" :: 'a => bool ("contains'_root _" 10)
|
neuper@37906
|
32 |
|
neuper@37906
|
33 |
Solve'_root'_equation
|
neuper@37906
|
34 |
:: "[bool,real, \
|
neuper@37906
|
35 |
\ bool list] => bool list"
|
neuper@37906
|
36 |
("((Script Solve'_root'_equation (_ _ =))// \
|
neuper@37906
|
37 |
\ (_))" 9)
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
Solve'_plain'_square
|
neuper@37906
|
40 |
:: "[bool,real, \
|
neuper@37906
|
41 |
\ bool list] => bool list"
|
neuper@37906
|
42 |
("((Script Solve'_plain'_square (_ _ =))// \
|
neuper@37906
|
43 |
\ (_))" 9)
|
neuper@37906
|
44 |
|
neuper@37906
|
45 |
Norm'_univar'_equation
|
neuper@37906
|
46 |
:: "[bool,real, \
|
neuper@37906
|
47 |
\ bool] => bool"
|
neuper@37906
|
48 |
("((Script Norm'_univar'_equation (_ _ =))// \
|
neuper@37906
|
49 |
\ (_))" 9)
|
neuper@37906
|
50 |
|
neuper@37906
|
51 |
STest'_simplify
|
neuper@37906
|
52 |
:: "['z, \
|
neuper@37906
|
53 |
\ 'z] => 'z"
|
neuper@37906
|
54 |
("((Script STest'_simplify (_ =))// \
|
neuper@37906
|
55 |
\ (_))" 9)
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
(*17.9.02 aus SqRoot.thy------------------------------^^^---*)
|
neuper@37906
|
58 |
|
neuper@37906
|
59 |
rules (*stated as axioms, todo: prove as theorems*)
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n"
|
neuper@37906
|
62 |
rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n"
|
neuper@37906
|
63 |
rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k"
|
neuper@37906
|
64 |
rdistr_div_right "((k::real) + l) / n = k / n + l / n"
|
neuper@37906
|
65 |
rcollect_right
|
neuper@37906
|
66 |
"[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
|
neuper@37906
|
67 |
rcollect_one_left
|
neuper@37906
|
68 |
"m is_const ==> (n::real) + m * n = (1 + m) * n"
|
neuper@37906
|
69 |
rcollect_one_left_assoc
|
neuper@37906
|
70 |
"m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
|
neuper@37906
|
71 |
rcollect_one_left_assoc_p
|
neuper@37906
|
72 |
"m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
|
neuper@37906
|
73 |
|
neuper@37906
|
74 |
rtwo_of_the_same "a + a = 2 * a"
|
neuper@37906
|
75 |
rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a"
|
neuper@37906
|
76 |
rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
rcancel_den "not(a=0) ==> a * (b / a) = b"
|
neuper@37906
|
79 |
rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
|
neuper@37906
|
80 |
rshift_nominator "(a::real) * b / c = a / c * b"
|
neuper@37906
|
81 |
|
neuper@37906
|
82 |
exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
|
neuper@37906
|
83 |
rsqare "(a::real) * a = a ^^^ 2"
|
neuper@37906
|
84 |
power_1 "(a::real) ^^^ 1 = a"
|
neuper@37906
|
85 |
rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
|
neuper@37906
|
86 |
|
neuper@37906
|
87 |
rmult_1 "1 * k = (k::real)"
|
neuper@37906
|
88 |
rmult_1_right "k * 1 = (k::real)"
|
neuper@37906
|
89 |
rmult_0 "0 * k = (0::real)"
|
neuper@37906
|
90 |
rmult_0_right "k * 0 = (0::real)"
|
neuper@37906
|
91 |
radd_0 "0 + k = (k::real)"
|
neuper@37906
|
92 |
radd_0_right "k + 0 = (k::real)"
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
radd_real_const_eq
|
neuper@37906
|
95 |
"[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
|
neuper@37906
|
96 |
radd_real_const
|
neuper@37906
|
97 |
"[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
(*for AC-operators*)
|
neuper@37906
|
100 |
radd_commute "(m::real) + (n::real) = n + m"
|
neuper@37906
|
101 |
radd_left_commute "(x::real) + (y + z) = y + (x + z)"
|
neuper@37906
|
102 |
radd_assoc "(m::real) + n + k = m + (n + k)"
|
neuper@37906
|
103 |
rmult_commute "(m::real) * n = n * m"
|
neuper@37906
|
104 |
rmult_left_commute "(x::real) * (y * z) = y * (x * z)"
|
neuper@37906
|
105 |
rmult_assoc "(m::real) * n * k = m * (n * k)"
|
neuper@37906
|
106 |
|
neuper@37906
|
107 |
(*for equations: 'bdv' is a meta-constant*)
|
neuper@37906
|
108 |
risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
|
neuper@37906
|
109 |
risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
|
neuper@37906
|
110 |
risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)"
|
neuper@37906
|
111 |
|
neuper@37906
|
112 |
rnorm_equation_add
|
neuper@37906
|
113 |
"~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
|
neuper@37906
|
114 |
|
neuper@37906
|
115 |
(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
|
neuper@37906
|
116 |
root_ge0 "0 <= a ==> 0 <= sqrt a"
|
neuper@37906
|
117 |
(*should be dropped with better simplification in eval_rls ...*)
|
neuper@37906
|
118 |
root_add_ge0
|
neuper@37906
|
119 |
"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
|
neuper@37906
|
120 |
root_ge0_1
|
neuper@37906
|
121 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
|
neuper@37906
|
122 |
root_ge0_2
|
neuper@37906
|
123 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
|
neuper@37906
|
124 |
|
neuper@37906
|
125 |
|
neuper@37906
|
126 |
rroot_square_inv "(sqrt a)^^^ 2 = a"
|
neuper@37906
|
127 |
rroot_times_root "sqrt a * sqrt b = sqrt(a*b)"
|
neuper@37906
|
128 |
rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
|
neuper@37906
|
129 |
rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
|
neuper@37906
|
130 |
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
(*for root-equations*)
|
neuper@37906
|
133 |
square_equation_left
|
neuper@37906
|
134 |
"[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
|
neuper@37906
|
135 |
square_equation_right
|
neuper@37906
|
136 |
"[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
|
neuper@37906
|
137 |
(*causes frequently non-termination:*)
|
neuper@37906
|
138 |
square_equation
|
neuper@37906
|
139 |
"[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
|
neuper@37906
|
142 |
risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
|
neuper@37906
|
143 |
risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)"
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
(*for polynomial equations of degree 2; linear case in RatArith*)
|
neuper@37906
|
146 |
mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
|
neuper@37906
|
147 |
constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
|
neuper@37906
|
148 |
constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
square_equality
|
neuper@37906
|
151 |
"0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
|
neuper@37906
|
152 |
square_equality_0
|
neuper@37906
|
153 |
"(x^^^2 = 0) = (x = 0)"
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
(*isolate root on the LEFT hand side of the equation
|
neuper@37906
|
156 |
otherwise shuffling from left to right would not terminate*)
|
neuper@37906
|
157 |
|
neuper@37906
|
158 |
rroot_to_lhs
|
neuper@37906
|
159 |
"is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
|
neuper@37906
|
160 |
rroot_to_lhs_mult
|
neuper@37906
|
161 |
"is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
|
neuper@37906
|
162 |
rroot_to_lhs_add_mult
|
neuper@37906
|
163 |
"is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
|
neuper@37906
|
164 |
|
neuper@37906
|
165 |
|
neuper@37906
|
166 |
(*17.9.02 aus SqRoot.thy------------------------------^^^---*)
|
neuper@37906
|
167 |
|
neuper@37906
|
168 |
|
neuper@37906
|
169 |
end
|