neuper@37906
|
1 |
(*.(c) by Richard Lang, 2003 .*)
|
neuper@37906
|
2 |
(* theory collecting all knowledge
|
neuper@37906
|
3 |
(predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
|
neuper@37906
|
4 |
for PolynomialEquations.
|
neuper@37906
|
5 |
alternative dependencies see Isac.thy
|
neuper@37906
|
6 |
created by: rlang
|
neuper@37906
|
7 |
date: 02.07
|
neuper@37906
|
8 |
changed by: rlang
|
neuper@37906
|
9 |
last change by: rlang
|
neuper@37906
|
10 |
date: 03.06.03
|
neuper@37906
|
11 |
*)
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
(* remove_thy"PolyEq";
|
neuper@37906
|
14 |
use_thy"IsacKnowledge/Isac";
|
neuper@37906
|
15 |
use_thy"IsacKnowledge/PolyEq";
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
remove_thy"PolyEq";
|
neuper@37906
|
18 |
use_thy"Isac";
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
use"ROOT.ML";
|
neuper@37906
|
21 |
cd"knowledge";
|
neuper@37906
|
22 |
*)
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
PolyEq = LinEq + RootRatEq +
|
neuper@37906
|
25 |
(*-------------------- consts ------------------------------------------------*)
|
neuper@37906
|
26 |
consts
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*---------scripts--------------------------*)
|
neuper@37906
|
29 |
Complete'_square
|
neuper@37906
|
30 |
:: "[bool,real, \
|
neuper@37906
|
31 |
\ bool list] => bool list"
|
neuper@37906
|
32 |
("((Script Complete'_square (_ _ =))// \
|
neuper@37906
|
33 |
\ (_))" 9)
|
neuper@37906
|
34 |
(*----- poly ----- *)
|
neuper@37906
|
35 |
Normalize'_poly
|
neuper@37906
|
36 |
:: "[bool,real, \
|
neuper@37906
|
37 |
\ bool list] => bool list"
|
neuper@37906
|
38 |
("((Script Normalize'_poly (_ _=))// \
|
neuper@37906
|
39 |
\ (_))" 9)
|
neuper@37906
|
40 |
Solve'_d0'_polyeq'_equation
|
neuper@37906
|
41 |
:: "[bool,real, \
|
neuper@37906
|
42 |
\ bool list] => bool list"
|
neuper@37906
|
43 |
("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \
|
neuper@37906
|
44 |
\ (_))" 9)
|
neuper@37906
|
45 |
Solve'_d1'_polyeq'_equation
|
neuper@37906
|
46 |
:: "[bool,real, \
|
neuper@37906
|
47 |
\ bool list] => bool list"
|
neuper@37906
|
48 |
("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \
|
neuper@37906
|
49 |
\ (_))" 9)
|
neuper@37906
|
50 |
Solve'_d2'_polyeq'_equation
|
neuper@37906
|
51 |
:: "[bool,real, \
|
neuper@37906
|
52 |
\ bool list] => bool list"
|
neuper@37906
|
53 |
("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \
|
neuper@37906
|
54 |
\ (_))" 9)
|
neuper@37906
|
55 |
Solve'_d2'_polyeq'_sqonly'_equation
|
neuper@37906
|
56 |
:: "[bool,real, \
|
neuper@37906
|
57 |
\ bool list] => bool list"
|
neuper@37906
|
58 |
("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \
|
neuper@37906
|
59 |
\ (_))" 9)
|
neuper@37906
|
60 |
Solve'_d2'_polyeq'_bdvonly'_equation
|
neuper@37906
|
61 |
:: "[bool,real, \
|
neuper@37906
|
62 |
\ bool list] => bool list"
|
neuper@37906
|
63 |
("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \
|
neuper@37906
|
64 |
\ (_))" 9)
|
neuper@37906
|
65 |
Solve'_d2'_polyeq'_pq'_equation
|
neuper@37906
|
66 |
:: "[bool,real, \
|
neuper@37906
|
67 |
\ bool list] => bool list"
|
neuper@37906
|
68 |
("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \
|
neuper@37906
|
69 |
\ (_))" 9)
|
neuper@37906
|
70 |
Solve'_d2'_polyeq'_abc'_equation
|
neuper@37906
|
71 |
:: "[bool,real, \
|
neuper@37906
|
72 |
\ bool list] => bool list"
|
neuper@37906
|
73 |
("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \
|
neuper@37906
|
74 |
\ (_))" 9)
|
neuper@37906
|
75 |
Solve'_d3'_polyeq'_equation
|
neuper@37906
|
76 |
:: "[bool,real, \
|
neuper@37906
|
77 |
\ bool list] => bool list"
|
neuper@37906
|
78 |
("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \
|
neuper@37906
|
79 |
\ (_))" 9)
|
neuper@37906
|
80 |
Solve'_d4'_polyeq'_equation
|
neuper@37906
|
81 |
:: "[bool,real, \
|
neuper@37906
|
82 |
\ bool list] => bool list"
|
neuper@37906
|
83 |
("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \
|
neuper@37906
|
84 |
\ (_))" 9)
|
neuper@37906
|
85 |
Biquadrat'_poly
|
neuper@37906
|
86 |
:: "[bool,real, \
|
neuper@37906
|
87 |
\ bool list] => bool list"
|
neuper@37906
|
88 |
("((Script Biquadrat'_poly (_ _=))// \
|
neuper@37906
|
89 |
\ (_))" 9)
|
neuper@37906
|
90 |
|
neuper@37906
|
91 |
(*-------------------- rules -------------------------------------------------*)
|
neuper@37906
|
92 |
rules
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
95 |
\ (a/c + b/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
96 |
cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
97 |
\ (a/c - b/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
98 |
cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \
|
neuper@37906
|
99 |
\ (a/c + b/c*bdv - bdv^^^2 = 0)"
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
102 |
\ (a/c + 1/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
103 |
cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
104 |
\ (a/c - 1/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
105 |
cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \
|
neuper@37906
|
106 |
\ (a/c + 1/c*bdv - bdv^^^2 = 0)"
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
109 |
\ ( b/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
110 |
cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \
|
neuper@37906
|
111 |
\ ( b/c*bdv - bdv^^^2 = 0)"
|
neuper@37906
|
112 |
|
neuper@37906
|
113 |
cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \
|
neuper@37906
|
114 |
\ ( 1/c*bdv + bdv^^^2 = 0)"
|
neuper@37906
|
115 |
cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \
|
neuper@37906
|
116 |
\ ( 1/c*bdv - bdv^^^2 = 0)"
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \
|
neuper@37906
|
119 |
\ (a/b + bdv^^^2 = 0)"
|
neuper@37906
|
120 |
cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \
|
neuper@37906
|
121 |
\ (a/b - bdv^^^2 = 0)"
|
neuper@37906
|
122 |
cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \
|
neuper@37906
|
123 |
\ ( bdv^^^2 = 0/b)"
|
neuper@37906
|
124 |
|
neuper@37906
|
125 |
complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \
|
neuper@37906
|
126 |
\(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
|
neuper@37906
|
127 |
complete_square2 "( p*bdv + bdv^^^2 = 0) = \
|
neuper@37906
|
128 |
\( (p/2 + bdv)^^^2 = (p/2)^^^2)"
|
neuper@37906
|
129 |
complete_square3 "( bdv + bdv^^^2 = 0) = \
|
neuper@37906
|
130 |
\( (1/2 + bdv)^^^2 = (1/2)^^^2)"
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \
|
neuper@37906
|
133 |
\(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
|
neuper@37906
|
134 |
complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \
|
neuper@37906
|
135 |
\(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
|
neuper@37906
|
136 |
|
neuper@37906
|
137 |
square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
|
neuper@37906
|
138 |
square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
|
neuper@37906
|
139 |
|
neuper@37906
|
140 |
bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
|
neuper@37906
|
141 |
bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
|
neuper@37906
|
142 |
bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)"
|
neuper@37906
|
143 |
|
neuper@37906
|
144 |
plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
|
neuper@37906
|
145 |
minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*)
|
neuper@37906
|
146 |
|
neuper@37906
|
147 |
(*-- normalize --*)
|
neuper@37906
|
148 |
(*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
|
neuper@37906
|
149 |
all_left
|
neuper@37906
|
150 |
"[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
|
neuper@37906
|
151 |
makex1_x
|
neuper@37906
|
152 |
"a^^^1 = a"
|
neuper@37906
|
153 |
real_assoc_1
|
neuper@37906
|
154 |
"a+(b+c) = a+b+c"
|
neuper@37906
|
155 |
real_assoc_2
|
neuper@37906
|
156 |
"a*(b*c) = a*b*c"
|
neuper@37906
|
157 |
|
neuper@37906
|
158 |
(* ---- degree 0 ----*)
|
neuper@37906
|
159 |
d0_true
|
neuper@37906
|
160 |
"(0=0) = True"
|
neuper@37906
|
161 |
d0_false
|
neuper@37906
|
162 |
"[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
|
neuper@37906
|
163 |
(* ---- degree 1 ----*)
|
neuper@37906
|
164 |
d1_isolate_add1
|
neuper@37906
|
165 |
"[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
|
neuper@37906
|
166 |
d1_isolate_add2
|
neuper@37906
|
167 |
"[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
|
neuper@37906
|
168 |
d1_isolate_div
|
neuper@37906
|
169 |
"[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
|
neuper@37906
|
170 |
(* ---- degree 2 ----*)
|
neuper@37906
|
171 |
d2_isolate_add1
|
neuper@37906
|
172 |
"[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
|
neuper@37906
|
173 |
d2_isolate_add2
|
neuper@37906
|
174 |
"[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
|
neuper@37906
|
175 |
d2_isolate_div
|
neuper@37906
|
176 |
"[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
|
neuper@37906
|
177 |
d2_prescind1
|
neuper@37906
|
178 |
"(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
|
neuper@37906
|
179 |
d2_prescind2
|
neuper@37906
|
180 |
"(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
|
neuper@37906
|
181 |
d2_prescind3
|
neuper@37906
|
182 |
"( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
|
neuper@37906
|
183 |
d2_prescind4
|
neuper@37906
|
184 |
"( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
|
neuper@37906
|
185 |
(* eliminate degree 2 *)
|
neuper@37906
|
186 |
(* thm for neg arguments in sqroot have postfix _neg *)
|
neuper@37906
|
187 |
d2_sqrt_equation1
|
neuper@37906
|
188 |
"[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
|
neuper@37906
|
189 |
d2_sqrt_equation1_neg
|
neuper@37906
|
190 |
"[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
|
neuper@37906
|
191 |
d2_sqrt_equation2
|
neuper@37906
|
192 |
"(bdv^^^2=0) = (bdv=0)"
|
neuper@37906
|
193 |
d2_sqrt_equation3
|
neuper@37906
|
194 |
"(b*bdv^^^2=0) = (bdv=0)"
|
neuper@37906
|
195 |
d2_reduce_equation1
|
neuper@37906
|
196 |
"(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
|
neuper@37906
|
197 |
d2_reduce_equation2
|
neuper@37906
|
198 |
"(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
|
neuper@37906
|
199 |
d2_pqformula1
|
neuper@37906
|
200 |
"[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
|
neuper@37906
|
201 |
((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
|
neuper@37906
|
202 |
| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
|
neuper@37906
|
203 |
d2_pqformula1_neg
|
neuper@37906
|
204 |
"[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
|
neuper@37906
|
205 |
d2_pqformula2
|
neuper@37906
|
206 |
"[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
|
neuper@37906
|
207 |
((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
|
neuper@37906
|
208 |
| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
|
neuper@37906
|
209 |
d2_pqformula2_neg
|
neuper@37906
|
210 |
"[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
|
neuper@37906
|
211 |
d2_pqformula3
|
neuper@37906
|
212 |
"[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
|
neuper@37906
|
213 |
((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
|
neuper@37906
|
214 |
| (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
|
neuper@37906
|
215 |
d2_pqformula3_neg
|
neuper@37906
|
216 |
"[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
|
neuper@37906
|
217 |
d2_pqformula4
|
neuper@37906
|
218 |
"[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
|
neuper@37906
|
219 |
((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
|
neuper@37906
|
220 |
| (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
|
neuper@37906
|
221 |
d2_pqformula4_neg
|
neuper@37906
|
222 |
"[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
|
neuper@37906
|
223 |
d2_pqformula5
|
neuper@37906
|
224 |
"[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
|
neuper@37906
|
225 |
((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
|
neuper@37906
|
226 |
| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
|
neuper@37906
|
227 |
(* d2_pqformula5_neg not need p^2 never less zero in R *)
|
neuper@37906
|
228 |
d2_pqformula6
|
neuper@37906
|
229 |
"[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
|
neuper@37906
|
230 |
((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
|
neuper@37906
|
231 |
| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
|
neuper@37906
|
232 |
(* d2_pqformula6_neg not need p^2 never less zero in R *)
|
neuper@37906
|
233 |
d2_pqformula7
|
neuper@37906
|
234 |
"[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
|
neuper@37906
|
235 |
((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
|
neuper@37906
|
236 |
| (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
|
neuper@37906
|
237 |
(* d2_pqformula7_neg not need, because 1<0 ==> False*)
|
neuper@37906
|
238 |
d2_pqformula8
|
neuper@37906
|
239 |
"[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
|
neuper@37906
|
240 |
((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
|
neuper@37906
|
241 |
| (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
|
neuper@37906
|
242 |
(* d2_pqformula8_neg not need, because 1<0 ==> False*)
|
neuper@37906
|
243 |
d2_pqformula9
|
neuper@37906
|
244 |
"[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ 1*bdv^^^2=0) =
|
neuper@37906
|
245 |
((bdv= 0 + sqrt(0 - 4*q)/2)
|
neuper@37906
|
246 |
| (bdv= 0 - sqrt(0 - 4*q)/2))"
|
neuper@37906
|
247 |
d2_pqformula9_neg
|
neuper@37906
|
248 |
"[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False"
|
neuper@37906
|
249 |
d2_pqformula10
|
neuper@37906
|
250 |
"[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
|
neuper@37906
|
251 |
((bdv= 0 + sqrt(0 - 4*q)/2)
|
neuper@37906
|
252 |
| (bdv= 0 - sqrt(0 - 4*q)/2))"
|
neuper@37906
|
253 |
d2_pqformula10_neg
|
neuper@37906
|
254 |
"[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False"
|
neuper@37906
|
255 |
d2_abcformula1
|
neuper@37906
|
256 |
"[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
|
neuper@37906
|
257 |
((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
|
neuper@37906
|
258 |
| (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
|
neuper@37906
|
259 |
d2_abcformula1_neg
|
neuper@37906
|
260 |
"[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
|
neuper@37906
|
261 |
d2_abcformula2
|
neuper@37906
|
262 |
"[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
|
neuper@37906
|
263 |
((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
|
neuper@37906
|
264 |
| (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
|
neuper@37906
|
265 |
d2_abcformula2_neg
|
neuper@37906
|
266 |
"[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False"
|
neuper@37906
|
267 |
d2_abcformula3
|
neuper@37906
|
268 |
"[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
|
neuper@37906
|
269 |
((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
|
neuper@37906
|
270 |
| (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
|
neuper@37906
|
271 |
d2_abcformula3_neg
|
neuper@37906
|
272 |
"[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False"
|
neuper@37906
|
273 |
d2_abcformula4
|
neuper@37906
|
274 |
"[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
|
neuper@37906
|
275 |
((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
|
neuper@37906
|
276 |
| (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
|
neuper@37906
|
277 |
d2_abcformula4_neg
|
neuper@37906
|
278 |
"[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False"
|
neuper@37906
|
279 |
d2_abcformula5
|
neuper@37906
|
280 |
"[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
|
neuper@37906
|
281 |
((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
|
neuper@37906
|
282 |
| (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
|
neuper@37906
|
283 |
d2_abcformula5_neg
|
neuper@37906
|
284 |
"[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False"
|
neuper@37906
|
285 |
d2_abcformula6
|
neuper@37906
|
286 |
"[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
|
neuper@37906
|
287 |
((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
|
neuper@37906
|
288 |
| (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
|
neuper@37906
|
289 |
d2_abcformula6_neg
|
neuper@37906
|
290 |
"[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False"
|
neuper@37906
|
291 |
d2_abcformula7
|
neuper@37906
|
292 |
"[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
|
neuper@37906
|
293 |
((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
|
neuper@37906
|
294 |
| (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
|
neuper@37906
|
295 |
(* d2_abcformula7_neg not need b^2 never less zero in R *)
|
neuper@37906
|
296 |
d2_abcformula8
|
neuper@37906
|
297 |
"[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
|
neuper@37906
|
298 |
((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
|
neuper@37906
|
299 |
| (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
|
neuper@37906
|
300 |
(* d2_abcformula8_neg not need b^2 never less zero in R *)
|
neuper@37906
|
301 |
d2_abcformula9
|
neuper@37906
|
302 |
"[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
|
neuper@37906
|
303 |
((bdv=( -1 + sqrt(1 - 0))/(2*a))
|
neuper@37906
|
304 |
| (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
|
neuper@37906
|
305 |
(* d2_abcformula9_neg not need, because 1<0 ==> False*)
|
neuper@37906
|
306 |
d2_abcformula10
|
neuper@37906
|
307 |
"[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
|
neuper@37906
|
308 |
((bdv=( -1 + sqrt(1 - 0))/(2*1))
|
neuper@37906
|
309 |
| (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
|
neuper@37906
|
310 |
(* d2_abcformula10_neg not need, because 1<0 ==> False*)
|
neuper@37906
|
311 |
|
neuper@37906
|
312 |
(* ---- degree 3 ----*)
|
neuper@37906
|
313 |
d3_reduce_equation1
|
neuper@37906
|
314 |
"(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
|
neuper@37906
|
315 |
d3_reduce_equation2
|
neuper@37906
|
316 |
"( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
|
neuper@37906
|
317 |
d3_reduce_equation3
|
neuper@37906
|
318 |
"(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
|
neuper@37906
|
319 |
d3_reduce_equation4
|
neuper@37906
|
320 |
"( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
|
neuper@37906
|
321 |
d3_reduce_equation5
|
neuper@37906
|
322 |
"(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
|
neuper@37906
|
323 |
d3_reduce_equation6
|
neuper@37906
|
324 |
"( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
|
neuper@37906
|
325 |
d3_reduce_equation7
|
neuper@37906
|
326 |
"(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
|
neuper@37906
|
327 |
d3_reduce_equation8
|
neuper@37906
|
328 |
"( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
|
neuper@37906
|
329 |
d3_reduce_equation9
|
neuper@37906
|
330 |
"(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
|
neuper@37906
|
331 |
d3_reduce_equation10
|
neuper@37906
|
332 |
"( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
|
neuper@37906
|
333 |
d3_reduce_equation11
|
neuper@37906
|
334 |
"(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
|
neuper@37906
|
335 |
d3_reduce_equation12
|
neuper@37906
|
336 |
"( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
|
neuper@37906
|
337 |
d3_reduce_equation13
|
neuper@37906
|
338 |
"( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
|
neuper@37906
|
339 |
d3_reduce_equation14
|
neuper@37906
|
340 |
"( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
|
neuper@37906
|
341 |
d3_reduce_equation15
|
neuper@37906
|
342 |
"( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
|
neuper@37906
|
343 |
d3_reduce_equation16
|
neuper@37906
|
344 |
"( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
|
neuper@37906
|
345 |
d3_isolate_add1
|
neuper@37906
|
346 |
"[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
|
neuper@37906
|
347 |
d3_isolate_add2
|
neuper@37906
|
348 |
"[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
|
neuper@37906
|
349 |
d3_isolate_div
|
neuper@37906
|
350 |
"[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
|
neuper@37906
|
351 |
d3_root_equation2
|
neuper@37906
|
352 |
"(bdv^^^3=0) = (bdv=0)"
|
neuper@37906
|
353 |
d3_root_equation1
|
neuper@37906
|
354 |
"(bdv^^^3=c) = (bdv = nroot 3 c)"
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(* ---- degree 4 ----*)
|
neuper@37906
|
357 |
(* RL03.FIXME es wir nicht getestet ob u>0 *)
|
neuper@37906
|
358 |
d4_sub_u1
|
neuper@37906
|
359 |
"(c+b*bdv^^^2+a*bdv^^^4=0) =
|
neuper@37906
|
360 |
((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
|
neuper@37906
|
361 |
|
neuper@37906
|
362 |
(* ---- 7.3.02 von Termorder ---- *)
|
neuper@37906
|
363 |
|
neuper@37906
|
364 |
bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
|
neuper@37906
|
365 |
bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
|
neuper@37906
|
366 |
bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
|
neuper@37906
|
367 |
|
neuper@37906
|
368 |
(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
|
neuper@37906
|
369 |
bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
|
neuper@37906
|
370 |
bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
|
neuper@37906
|
371 |
*)
|
neuper@37906
|
372 |
bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
|
neuper@37906
|
373 |
bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
|
neuper@37906
|
374 |
bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
|
neuper@37906
|
375 |
|
neuper@37906
|
376 |
bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
|
neuper@37906
|
377 |
bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
|
neuper@37906
|
378 |
bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
|
neuper@37906
|
379 |
|
neuper@37906
|
380 |
|
neuper@37906
|
381 |
bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
|
neuper@37906
|
382 |
bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
|
neuper@37906
|
383 |
bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
|
neuper@37906
|
384 |
|
neuper@37906
|
385 |
bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
|
neuper@37906
|
386 |
bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
|
neuper@37906
|
387 |
bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
|
neuper@37906
|
388 |
|
neuper@37906
|
389 |
bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
|
neuper@37906
|
390 |
bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
|
neuper@37906
|
391 |
bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
|
neuper@37906
|
392 |
|
neuper@37906
|
393 |
(*WN.14.3.03*)
|
neuper@37906
|
394 |
real_minus_div "- (a / b) = (-1 * a) / b"
|
neuper@37906
|
395 |
|
neuper@37906
|
396 |
separate_bdv "(a * bdv) / b = (a / b) * bdv"
|
neuper@37906
|
397 |
separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
|
neuper@37906
|
398 |
separate_1_bdv "bdv / b = (1 / b) * bdv"
|
neuper@37906
|
399 |
separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
|
neuper@37906
|
400 |
|
neuper@37906
|
401 |
end
|
neuper@37906
|
402 |
|
neuper@37906
|
403 |
|
neuper@37906
|
404 |
|
neuper@37906
|
405 |
|
neuper@37906
|
406 |
|
neuper@37906
|
407 |
|