1 (* theory collecting all knowledge
2 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
3 for PolynomialEquations.
4 alternative dependencies see @{theory "Isac_Knowledge"}
10 (c) by Richard Lang, 2003
13 theory PolyEq imports LinEq RootRatEq begin
15 (*-------------------- rules -------------------------------------------------*)
16 (* type real enforced by op " \<up> " *)
18 cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv \<up> 2 = 0) =
19 (a/c + b/c*bdv + bdv \<up> 2 = 0)" and
20 cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv \<up> 2 = 0) =
21 (a/c - b/c*bdv + bdv \<up> 2 = 0)" and
22 cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv \<up> 2 = 0) =
23 (a/c + b/c*bdv - bdv \<up> 2 = 0)" and
25 cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv \<up> 2 = 0) =
26 (a/c + 1/c*bdv + bdv \<up> 2 = 0)" and
27 cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv \<up> 2 = 0) =
28 (a/c - 1/c*bdv + bdv \<up> 2 = 0)" and
29 cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv \<up> 2 = 0) =
30 (a/c + 1/c*bdv - bdv \<up> 2 = 0)" and
32 cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv \<up> 2 = 0) =
33 ( b/c*bdv + bdv \<up> 2 = 0)" and
34 cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv \<up> 2 = 0) =
35 ( b/c*bdv - bdv \<up> 2 = 0)" and
37 cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv \<up> 2 = 0) =
38 ( 1/c*bdv + bdv \<up> 2 = 0)" and
39 cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv \<up> 2 = 0) =
40 ( 1/c*bdv - bdv \<up> 2 = 0)" and
42 cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv \<up> 2 = 0) =
43 (a/b + bdv \<up> 2 = 0)" and
44 cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv \<up> 2 = 0) =
45 (a/b - bdv \<up> 2 = 0)" and
46 cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv \<up> 2 = 0) =
47 ( bdv \<up> 2 = 0/b)" and
49 complete_square1: "(q + p*bdv + bdv \<up> 2 = 0) =
50 (q + (p/2 + bdv) \<up> 2 = (p/2) \<up> 2)" and
51 complete_square2: "( p*bdv + bdv \<up> 2 = 0) =
52 ( (p/2 + bdv) \<up> 2 = (p/2) \<up> 2)" and
53 complete_square3: "( bdv + bdv \<up> 2 = 0) =
54 ( (1/2 + bdv) \<up> 2 = (1/2) \<up> 2)" and
56 complete_square4: "(q - p*bdv + bdv \<up> 2 = 0) =
57 (q + (p/2 - bdv) \<up> 2 = (p/2) \<up> 2)" and
58 complete_square5: "(q + p*bdv - bdv \<up> 2 = 0) =
59 (q + (p/2 - bdv) \<up> 2 = (p/2) \<up> 2)" and
61 square_explicit1: "(a + b \<up> 2 = c) = ( b \<up> 2 = c - a)" and
62 square_explicit2: "(a - b \<up> 2 = c) = (-(b \<up> 2) = c - a)" and
64 (*bdv_explicit* required type constrain to real in --- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---*)
65 bdv_explicit1: "(a + bdv = b) = (bdv = - a + (b::real))" and
66 bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + (b::real))" and
67 bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*(b::real))" and
69 plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) and
70 minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) and
73 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
74 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
75 makex1_x: "a\<up>1 = a" and
76 real_assoc_1: "a+(b+c) = a+b+c" and
77 real_assoc_2: "a*(b*c) = a*b*c" and
79 (* ---- degree 0 ----*)
80 d0_true: "(0=0) = True" and
81 d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" and
82 (* ---- degree 1 ----*)
84 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" and
86 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" and
88 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" and
89 (* ---- degree 2 ----*)
91 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv \<up> 2=0) = (b*bdv \<up> 2= (-1)*a)" and
93 "[|Not(bdv occurs_in a)|] ==> (a + bdv \<up> 2=0) = ( bdv \<up> 2= (-1)*a)" and
95 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv \<up> 2=c) = (bdv \<up> 2=c/b)" and
97 d2_prescind1: "(a*bdv + b*bdv \<up> 2 = 0) = (bdv*(a +b*bdv)=0)" and
98 d2_prescind2: "(a*bdv + bdv \<up> 2 = 0) = (bdv*(a + bdv)=0)" and
99 d2_prescind3: "( bdv + b*bdv \<up> 2 = 0) = (bdv*(1+b*bdv)=0)" and
100 d2_prescind4: "( bdv + bdv \<up> 2 = 0) = (bdv*(1+ bdv)=0)" and
101 (* eliminate degree 2 *)
102 (* thm for neg arguments in sqroot have postfix _neg *)
103 d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==>
104 (bdv \<up> 2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" and
105 d2_sqrt_equation1_neg:
106 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv \<up> 2=c) = False" and
107 d2_sqrt_equation2: "(bdv \<up> 2=0) = (bdv=0)" and
108 d2_sqrt_equation3: "(b*bdv \<up> 2=0) = (bdv=0)"
109 axiomatization where (*AK..if replaced by "and" we get errors:
110 exception PTREE "nth _ []" raised
111 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
112 'fun nth _ [] = raise PTREE "nth _ []"'
114 exception Bind raised
115 (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
116 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
117 (* WN120315 these 2 thms need "::real", because no " \<up> " constrains type as
118 required in test --- rls d2_polyeq_bdv_only_simplify --- *)
119 d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" and
120 d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=(0::real)))"
122 axiomatization where (*..if replaced by "and" we get errors:
123 exception PTREE "nth _ []" raised
124 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
125 'fun nth _ [] = raise PTREE "nth _ []"'
127 exception Bind raised
128 (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
129 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
130 d2_pqformula1: "[|0<=p \<up> 2 - 4*q|] ==> (q+p*bdv+ bdv \<up> 2=0) =
131 ((bdv= (-1)*(p/2) + sqrt(p \<up> 2 - 4*q)/2)
132 | (bdv= (-1)*(p/2) - sqrt(p \<up> 2 - 4*q)/2))" and
133 d2_pqformula1_neg: "[|p \<up> 2 - 4*q<0|] ==> (q+p*bdv+ bdv \<up> 2=0) = False" and
134 d2_pqformula2: "[|0<=p \<up> 2 - 4*q|] ==> (q+p*bdv+1*bdv \<up> 2=0) =
135 ((bdv= (-1)*(p/2) + sqrt(p \<up> 2 - 4*q)/2)
136 | (bdv= (-1)*(p/2) - sqrt(p \<up> 2 - 4*q)/2))" and
137 d2_pqformula2_neg: "[|p \<up> 2 - 4*q<0|] ==> (q+p*bdv+1*bdv \<up> 2=0) = False" and
138 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv \<up> 2=0) =
139 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
140 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
141 d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv \<up> 2=0) = False" and
142 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv \<up> 2=0) =
143 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
144 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
145 d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv \<up> 2=0) = False" and
146 d2_pqformula5: "[|0<=p \<up> 2 - 0|] ==> ( p*bdv+ bdv \<up> 2=0) =
147 ((bdv= (-1)*(p/2) + sqrt(p \<up> 2 - 0)/2)
148 | (bdv= (-1)*(p/2) - sqrt(p \<up> 2 - 0)/2))" and
149 (* d2_pqformula5_neg not need p^2 never less zero in R *)
150 d2_pqformula6: " ( p*bdv+1*bdv \<up> 2=0) =
151 ((bdv= (-1)*(p/2) + sqrt(p \<up> 2 - 0)/2)
152 | (bdv= (-1)*(p/2) - sqrt(p \<up> 2 - 0)/2))" and
153 (* d2_pqformula6_neg not need p^2 never less zero in R *)
154 d2_pqformula7: " ( bdv+ bdv \<up> 2=0) =
155 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
156 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
157 (* d2_pqformula7_neg not need, because 1<0 ==> False*)
158 d2_pqformula8: " ( bdv+1*bdv \<up> 2=0) =
159 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
160 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
161 (* d2_pqformula8_neg not need, because 1<0 ==> False*)
162 d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
163 (q+ 1*bdv \<up> 2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2)
164 | (bdv= 0 - sqrt(0 - 4*q)/2))" and
166 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv \<up> 2=0) = False" and
168 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv \<up> 2=0) =
169 ((bdv= 0 + sqrt(0 - 4*q)/2)
170 | (bdv= 0 - sqrt(0 - 4*q)/2))" and
172 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv \<up> 2=0) = False" and
174 "[|0<=b \<up> 2 - 4*a*c|] ==> (c + b*bdv+a*bdv \<up> 2=0) =
175 ((bdv=( -b + sqrt(b \<up> 2 - 4*a*c))/(2*a))
176 | (bdv=( -b - sqrt(b \<up> 2 - 4*a*c))/(2*a)))" and
178 "[|b \<up> 2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv \<up> 2=0) = False" and
180 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv \<up> 2=0) =
181 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
182 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" and
184 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv \<up> 2=0) = False" and
186 "[|0<=b \<up> 2 - 4*1*c|] ==> (c + b*bdv+ bdv \<up> 2=0) =
187 ((bdv=( -b + sqrt(b \<up> 2 - 4*1*c))/(2*1))
188 | (bdv=( -b - sqrt(b \<up> 2 - 4*1*c))/(2*1)))" and
190 "[|b \<up> 2 - 4*1*c<0|] ==> (c + b*bdv+ bdv \<up> 2=0) = False" and
192 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv \<up> 2=0) =
193 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
194 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" and
196 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv \<up> 2=0) = False" and
198 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv \<up> 2=0) =
199 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
200 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" and
202 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv \<up> 2=0) = False" and
204 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv \<up> 2=0) =
205 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
206 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" and
208 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv \<up> 2=0) = False" and
210 " ( b*bdv+a*bdv \<up> 2=0) =
211 ((bdv=( -b + sqrt(b \<up> 2 - 0))/(2*a))
212 | (bdv=( -b - sqrt(b \<up> 2 - 0))/(2*a)))" and
213 (* d2_abcformula7_neg not need b^2 never less zero in R *)
215 " ( b*bdv+ bdv \<up> 2=0) =
216 ((bdv=( -b + sqrt(b \<up> 2 - 0))/(2*1))
217 | (bdv=( -b - sqrt(b \<up> 2 - 0))/(2*1)))" and
218 (* d2_abcformula8_neg not need b^2 never less zero in R *)
220 " ( bdv+a*bdv \<up> 2=0) =
221 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
222 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" and
223 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
225 " ( bdv+ bdv \<up> 2=0) =
226 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
227 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" and
228 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
231 (* ---- degree 3 ----*)
233 "(a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0))" and
235 "( bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + c*bdv \<up> 2=0))" and
237 "(a*bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + bdv + c*bdv \<up> 2=0))" and
239 "( bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + bdv + c*bdv \<up> 2=0))" and
241 "(a*bdv + b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + bdv \<up> 2=0))" and
243 "( bdv + b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + bdv \<up> 2=0))" and
245 "(a*bdv + bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + bdv + bdv \<up> 2=0))" and
247 "( bdv + bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + bdv + bdv \<up> 2=0))" and
249 "(a*bdv + c*bdv \<up> 3=0) = (bdv=0 | (a + c*bdv \<up> 2=0))" and
250 d3_reduce_equation10:
251 "( bdv + c*bdv \<up> 3=0) = (bdv=0 | (1 + c*bdv \<up> 2=0))" and
252 d3_reduce_equation11:
253 "(a*bdv + bdv \<up> 3=0) = (bdv=0 | (a + bdv \<up> 2=0))" and
254 d3_reduce_equation12:
255 "( bdv + bdv \<up> 3=0) = (bdv=0 | (1 + bdv \<up> 2=0))" and
256 d3_reduce_equation13:
257 "( b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | ( b*bdv + c*bdv \<up> 2=0))" and
258 d3_reduce_equation14:
259 "( bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | ( bdv + c*bdv \<up> 2=0))" and
260 d3_reduce_equation15:
261 "( b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | ( b*bdv + bdv \<up> 2=0))" and
262 d3_reduce_equation16:
263 "( bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | ( bdv + bdv \<up> 2=0))" and
265 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv \<up> 3=0) = (b*bdv \<up> 3= (-1)*a)" and
267 "[|Not(bdv occurs_in a)|] ==> (a + bdv \<up> 3=0) = ( bdv \<up> 3= (-1)*a)" and
269 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv \<up> 3=c) = (bdv \<up> 3=c/b)" and
271 "(bdv \<up> 3=0) = (bdv=0)" and
273 "(bdv \<up> 3=c) = (bdv = nroot 3 c)" and
275 (* ---- degree 4 ----*)
276 (* RL03.FIXME es wir nicht getestet ob u>0 *)
278 "(c+b*bdv \<up> 2+a*bdv \<up> 4=0) =
279 ((a*u \<up> 2+b*u+c=0) & (bdv \<up> 2=u))" and
281 (* ---- 7.3.02 von Termorder ---- *)
283 bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" and
284 bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" and
285 bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" and
287 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
288 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
289 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
291 bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" and
292 bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" and
293 bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" and
295 bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" and
296 bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" and
297 bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" and
300 bdv_n_collect_1: "l * bdv \<up> n + m * bdv \<up> n = (l + m) * bdv \<up> n" and
301 bdv_n_collect_2: " bdv \<up> n + m * bdv \<up> n = (1 + m) * bdv \<up> n" and
302 bdv_n_collect_3: "l * bdv \<up> n + bdv \<up> n = (l + 1) * bdv \<up> n" (*order!*) and
304 bdv_n_collect_assoc1_1: "l * bdv \<up> n + (m * bdv \<up> n + k) = (l + m) * bdv \<up> n + k" and
305 bdv_n_collect_assoc1_2: "bdv \<up> n + (m * bdv \<up> n + k) = (1 + m) * bdv \<up> n + k" and
306 bdv_n_collect_assoc1_3: "l * bdv \<up> n + (bdv \<up> n + k) = (l + 1) * bdv \<up> n + k" and
308 bdv_n_collect_assoc2_1: "k + l * bdv \<up> n + m * bdv \<up> n = k +(l + m) * bdv \<up> n" and
309 bdv_n_collect_assoc2_2: "k + bdv \<up> n + m * bdv \<up> n = k + (1 + m) * bdv \<up> n" and
310 bdv_n_collect_assoc2_3: "k + l * bdv \<up> n + bdv \<up> n = k + (l + 1) * bdv \<up> n" and
313 real_minus_div: "- (a / b) = (-1 * a) / b" and
315 separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)" and
316 separate_bdv_n: "(a * bdv \<up> n) / b = (a / b) * bdv \<up> n" and
317 separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)" and
318 separate_1_bdv_n: "bdv \<up> n / b = (1 / b) * bdv \<up> n"
321 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
322 Rule_Set.append_rules "PolyEq_prls" Rule_Set.empty [
323 \<^rule_eval>\<open>ident\<close> (Prog_Expr.eval_ident "#ident_"),
324 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
325 \<^rule_eval>\<open>lhs\<close> (Prog_Expr.eval_lhs ""),
326 \<^rule_eval>\<open>rhs\<close> (Prog_Expr.eval_rhs ""),
327 \<^rule_eval>\<open>is_expanded_in\<close> (eval_is_expanded_in ""),
328 \<^rule_eval>\<open>is_poly_in\<close> (eval_is_poly_in ""),
329 \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
330 \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
331 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
332 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
333 \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
334 \<^rule_thm>\<open>not_true\<close>,
335 \<^rule_thm>\<open>not_false\<close>,
336 \<^rule_thm>\<open>and_true\<close>,
337 \<^rule_thm>\<open>and_false\<close>,
338 \<^rule_thm>\<open>or_true\<close>,
339 \<^rule_thm>\<open>or_false\<close>];
342 Rule_Set.merge "PolyEq_erls" LinEq_erls
343 (Rule_Set.append_rules "ops_preds" calculate_Rational [
344 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
345 \<^rule_thm>\<open>plus_leq\<close>,
346 \<^rule_thm>\<open>minus_leq\<close>,
347 \<^rule_thm>\<open>rat_leq1\<close>,
348 \<^rule_thm>\<open>rat_leq2\<close>,
349 \<^rule_thm>\<open>rat_leq3\<close>]);
352 Rule_Set.merge "PolyEq_crls" LinEq_crls
353 (Rule_Set.append_rules "ops_preds" calculate_Rational [
354 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
355 \<^rule_thm>\<open>plus_leq\<close>,
356 \<^rule_thm>\<open>minus_leq\<close>,
357 \<^rule_thm>\<open>rat_leq1\<close>,
358 \<^rule_thm>\<open>rat_leq2\<close>,
359 \<^rule_thm>\<open>rat_leq3\<close>
362 val cancel_leading_coeff = prep_rls'(
363 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [],
364 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
365 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
367 \<^rule_thm>\<open>cancel_leading_coeff1\<close>,
368 \<^rule_thm>\<open>cancel_leading_coeff2\<close>,
369 \<^rule_thm>\<open>cancel_leading_coeff3\<close>,
370 \<^rule_thm>\<open>cancel_leading_coeff4\<close>,
371 \<^rule_thm>\<open>cancel_leading_coeff5\<close>,
372 \<^rule_thm>\<open>cancel_leading_coeff6\<close>,
373 \<^rule_thm>\<open>cancel_leading_coeff7\<close>,
374 \<^rule_thm>\<open>cancel_leading_coeff8\<close>,
375 \<^rule_thm>\<open>cancel_leading_coeff9\<close>,
376 \<^rule_thm>\<open>cancel_leading_coeff10\<close>,
377 \<^rule_thm>\<open>cancel_leading_coeff11\<close>,
378 \<^rule_thm>\<open>cancel_leading_coeff12\<close>,
379 \<^rule_thm>\<open>cancel_leading_coeff13\<close> ],
380 scr = Rule.Empty_Prog});
382 val prep_rls' = Auto_Prog.prep_rls @{theory};
385 val complete_square = prep_rls'(
386 Rule_Def.Repeat {id = "complete_square", preconds = [],
387 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
388 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
390 \<^rule_thm>\<open>complete_square1\<close>,
391 \<^rule_thm>\<open>complete_square2\<close>,
392 \<^rule_thm>\<open>complete_square3\<close>,
393 \<^rule_thm>\<open>complete_square4\<close>,
394 \<^rule_thm>\<open>complete_square5\<close>],
395 scr = Rule.Empty_Prog});
397 val polyeq_simplify = prep_rls'(
398 Rule_Def.Repeat {id = "polyeq_simplify", preconds = [],
399 rew_ord = ("termlessI",termlessI),
401 srls = Rule_Set.Empty,
402 calc = [], errpatts = [],
404 \<^rule_thm>\<open>real_assoc_1\<close>,
405 \<^rule_thm>\<open>real_assoc_2\<close>,
406 \<^rule_thm>\<open>real_diff_minus\<close>,
407 \<^rule_thm>\<open>real_unari_minus\<close>,
408 \<^rule_thm>\<open>realpow_multI\<close>,
409 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
410 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
411 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
412 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
413 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
414 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
415 Rule.Rls_ reduce_012],
416 scr = Rule.Empty_Prog});
419 cancel_leading_coeff = cancel_leading_coeff and
420 complete_square = complete_square and
421 PolyEq_erls = PolyEq_erls and
422 polyeq_simplify = polyeq_simplify
425 (* the subsequent rule-sets are caused by the lack of rewriting at the time of implementation *)
427 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
428 val d0_polyeq_simplify = prep_rls'(
429 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
430 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
432 srls = Rule_Set.Empty,
433 calc = [], errpatts = [],
435 \<^rule_thm>\<open>d0_true\<close>,
436 \<^rule_thm>\<open>d0_false\<close>],
437 scr = Rule.Empty_Prog});
440 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
441 val d1_polyeq_simplify = prep_rls'(
442 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
443 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
445 srls = Rule_Set.Empty,
446 calc = [], errpatts = [],
448 \<^rule_thm>\<open>d1_isolate_add1\<close>, (* a+bx=0 -> bx=-a *)
449 \<^rule_thm>\<open>d1_isolate_add2\<close>, (* a+ x=0 -> x=-a *)
450 \<^rule_thm>\<open>d1_isolate_div\<close> (* bx=c -> x=c/b *)],
451 scr = Rule.Empty_Prog});
454 subsection \<open>degree 2\<close>
456 (* isolate the bound variable in an d2 equation with bdv only;
457 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
458 val d2_polyeq_bdv_only_simplify = prep_rls'(
459 Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
460 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
462 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *)
463 \<^rule_thm>\<open>d2_prescind2\<close>, (* ax+ x^2=0 -> x(a+ x)=0 *)
464 \<^rule_thm>\<open>d2_prescind3\<close>, (* x+bx^2=0 -> x(1+bx)=0 *)
465 \<^rule_thm>\<open>d2_prescind4\<close>, (* x+ x^2=0 -> x(1+ x)=0 *)
466 \<^rule_thm>\<open>d2_sqrt_equation1\<close>, (* x^2=c -> x=+-sqrt(c) *)
467 \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>, (* [0<c] x^2=c -> []*)
468 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *)
469 \<^rule_thm>\<open>d2_reduce_equation1\<close>,(* x(a+bx)=0 -> x=0 |a+bx=0*)
470 \<^rule_thm>\<open>d2_reduce_equation2\<close>,(* x(a+ x)=0 -> x=0 |a+ x=0*)
471 \<^rule_thm>\<open>d2_isolate_div\<close>], (* bx^2=c -> x^2=c/b *)
472 scr = Rule.Empty_Prog});
474 (* isolate the bound variable in an d2 equation with sqrt only;
475 'bdv' is a meta-constant*)
476 val d2_polyeq_sq_only_simplify = prep_rls'(
477 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
478 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
479 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
481 \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+ bx^2=0 -> bx^2=(-1)a*)
482 \<^rule_thm>\<open>d2_isolate_add2\<close>, (* a+ x^2=0 -> x^2=(-1)a*)
483 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *)
484 \<^rule_thm>\<open>d2_sqrt_equation1\<close>, (* x^2=c -> x=+-sqrt(c)*)
485 \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>,(* [c<0] x^2=c -> x=[] *)
486 \<^rule_thm>\<open>d2_isolate_div\<close>], (* bx^2=c -> x^2=c/b*)
487 scr = Rule.Empty_Prog});
490 (* isolate the bound variable in an d2 equation with pqFormula;
491 'bdv' is a meta-constant*)
492 val d2_polyeq_pqFormula_simplify = prep_rls'(
493 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
494 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
495 srls = Rule_Set.Empty, calc = [], errpatts = [],
497 \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *)
498 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* q+px+ x^2=0 *)
499 \<^rule_thm>\<open>d2_pqformula2\<close>, (* q+px+1x^2=0 *)
500 \<^rule_thm>\<open>d2_pqformula2_neg\<close>, (* q+px+1x^2=0 *)
501 \<^rule_thm>\<open>d2_pqformula3\<close>, (* q+ x+ x^2=0 *)
502 \<^rule_thm>\<open>d2_pqformula3_neg\<close>, (* q+ x+ x^2=0 *)
503 \<^rule_thm>\<open>d2_pqformula4\<close>, (* q+ x+1x^2=0 *)
504 \<^rule_thm>\<open>d2_pqformula4_neg\<close>, (* q+ x+1x^2=0 *)
505 \<^rule_thm>\<open>d2_pqformula5\<close>, (* qx+ x^2=0 *)
506 \<^rule_thm>\<open>d2_pqformula6\<close>, (* qx+1x^2=0 *)
507 \<^rule_thm>\<open>d2_pqformula7\<close>, (* x+ x^2=0 *)
508 \<^rule_thm>\<open>d2_pqformula8\<close>, (* x+1x^2=0 *)
509 \<^rule_thm>\<open>d2_pqformula9\<close>, (* q +1x^2=0 *)
510 \<^rule_thm>\<open>d2_pqformula9_neg\<close>, (* q +1x^2=0 *)
511 \<^rule_thm>\<open>d2_pqformula10\<close>, (* q + x^2=0 *)
512 \<^rule_thm>\<open>d2_pqformula10_neg\<close>, (* q + x^2=0 *)
513 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 *)
514 \<^rule_thm>\<open>d2_sqrt_equation3\<close>], (* 1x^2=0 *)
515 scr = Rule.Empty_Prog});
517 (* isolate the bound variable in an d2 equation with abcFormula;
518 'bdv' is a meta-constant*)
519 val d2_polyeq_abcFormula_simplify = prep_rls'(
520 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
521 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
522 srls = Rule_Set.Empty, calc = [], errpatts = [],
524 \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *)
525 \<^rule_thm>\<open>d2_abcformula1_neg\<close>, (*c+bx+cx^2=0 *)
526 \<^rule_thm>\<open>d2_abcformula2\<close>, (*c+ x+cx^2=0 *)
527 \<^rule_thm>\<open>d2_abcformula2_neg\<close>, (*c+ x+cx^2=0 *)
528 \<^rule_thm>\<open>d2_abcformula3\<close>, (*c+bx+ x^2=0 *)
529 \<^rule_thm>\<open>d2_abcformula3_neg\<close>, (*c+bx+ x^2=0 *)
530 \<^rule_thm>\<open>d2_abcformula4\<close>, (*c+ x+ x^2=0 *)
531 \<^rule_thm>\<open>d2_abcformula4_neg\<close>, (*c+ x+ x^2=0 *)
532 \<^rule_thm>\<open>d2_abcformula5\<close>, (*c+ cx^2=0 *)
533 \<^rule_thm>\<open>d2_abcformula5_neg\<close>, (*c+ cx^2=0 *)
534 \<^rule_thm>\<open>d2_abcformula6\<close>, (*c+ x^2=0 *)
535 \<^rule_thm>\<open>d2_abcformula6_neg\<close>, (*c+ x^2=0 *)
536 \<^rule_thm>\<open>d2_abcformula7\<close>, (* bx+ax^2=0 *)
537 \<^rule_thm>\<open>d2_abcformula8\<close>, (* bx+ x^2=0 *)
538 \<^rule_thm>\<open>d2_abcformula9\<close>, (* x+ax^2=0 *)
539 \<^rule_thm>\<open>d2_abcformula10\<close>, (* x+ x^2=0 *)
540 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 *)
541 \<^rule_thm>\<open>d2_sqrt_equation3\<close>], (* bx^2=0 *)
542 scr = Rule.Empty_Prog});
544 (* isolate the bound variable in an d2 equation;
545 'bdv' is a meta-constant*)
546 val d2_polyeq_simplify = prep_rls'(
547 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
548 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
549 srls = Rule_Set.Empty, calc = [], errpatts = [],
551 \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *)
552 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* p+qx+ x^2=0 *)
553 \<^rule_thm>\<open>d2_pqformula2\<close>, (* p+qx+1x^2=0 *)
554 \<^rule_thm>\<open>d2_pqformula2_neg\<close>, (* p+qx+1x^2=0 *)
555 \<^rule_thm>\<open>d2_pqformula3\<close>, (* p+ x+ x^2=0 *)
556 \<^rule_thm>\<open>d2_pqformula3_neg\<close>, (* p+ x+ x^2=0 *)
557 \<^rule_thm>\<open>d2_pqformula4\<close>, (* p+ x+1x^2=0 *)
558 \<^rule_thm>\<open>d2_pqformula4_neg\<close>, (* p+ x+1x^2=0 *)
559 \<^rule_thm>\<open>d2_abcformula1\<close>, (* c+bx+cx^2=0 *)
560 \<^rule_thm>\<open>d2_abcformula1_neg\<close>, (* c+bx+cx^2=0 *)
561 \<^rule_thm>\<open>d2_abcformula2\<close>, (* c+ x+cx^2=0 *)
562 \<^rule_thm>\<open>d2_abcformula2_neg\<close>, (* c+ x+cx^2=0 *)
563 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *)
564 \<^rule_thm>\<open>d2_prescind2\<close>, (* ax+ x^2=0 -> x(a+ x)=0 *)
565 \<^rule_thm>\<open>d2_prescind3\<close>, (* x+bx^2=0 -> x(1+bx)=0 *)
566 \<^rule_thm>\<open>d2_prescind4\<close>, (* x+ x^2=0 -> x(1+ x)=0 *)
567 \<^rule_thm>\<open>d2_isolate_add1\<close>, (* a+ bx^2=0 -> bx^2=(-1)a*)
568 \<^rule_thm>\<open>d2_isolate_add2\<close>, (* a+ x^2=0 -> x^2=(-1)a*)
569 \<^rule_thm>\<open>d2_sqrt_equation1\<close>, (* x^2=c -> x=+-sqrt(c)*)
570 \<^rule_thm>\<open>d2_sqrt_equation1_neg\<close>, (* [c<0] x^2=c -> x=[]*)
571 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *)
572 \<^rule_thm>\<open>d2_reduce_equation1\<close>, (* x(a+bx)=0 -> x=0 | a+bx=0*)
573 \<^rule_thm>\<open>d2_reduce_equation2\<close>, (* x(a+ x)=0 -> x=0 | a+ x=0*)
574 \<^rule_thm>\<open>d2_isolate_div\<close>], (* bx^2=c -> x^2=c/b*)
575 scr = Rule.Empty_Prog});
578 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
579 val d3_polyeq_simplify = prep_rls'(
580 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
581 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
582 srls = Rule_Set.Empty, calc = [], errpatts = [],
584 \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*)
585 \<^rule_thm>\<open>d3_reduce_equation2\<close>, (* bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + c*bdv \<up> 2=0)*)
586 \<^rule_thm>\<open>d3_reduce_equation3\<close>, (*a*bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + bdv + c*bdv \<up> 2=0)*)
587 \<^rule_thm>\<open>d3_reduce_equation4\<close>, (* bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + bdv + c*bdv \<up> 2=0)*)
588 \<^rule_thm>\<open>d3_reduce_equation5\<close>, (*a*bdv + b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + bdv \<up> 2=0)*)
589 \<^rule_thm>\<open>d3_reduce_equation6\<close>, (* bdv + b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + bdv \<up> 2=0)*)
590 \<^rule_thm>\<open>d3_reduce_equation7\<close>, (*a*bdv + bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + bdv + bdv \<up> 2=0)*)
591 \<^rule_thm>\<open>d3_reduce_equation8\<close>, (* bdv + bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | (1 + bdv + bdv \<up> 2=0)*)
592 \<^rule_thm>\<open>d3_reduce_equation9\<close>, (*a*bdv + c*bdv \<up> 3=0) = (bdv=0 | (a + c*bdv \<up> 2=0)*)
593 \<^rule_thm>\<open>d3_reduce_equation10\<close>, (* bdv + c*bdv \<up> 3=0) = (bdv=0 | (1 + c*bdv \<up> 2=0)*)
594 \<^rule_thm>\<open>d3_reduce_equation11\<close>, (*a*bdv + bdv \<up> 3=0) = (bdv=0 | (a + bdv \<up> 2=0)*)
595 \<^rule_thm>\<open>d3_reduce_equation12\<close>, (* bdv + bdv \<up> 3=0) = (bdv=0 | (1 + bdv \<up> 2=0)*)
596 \<^rule_thm>\<open>d3_reduce_equation13\<close>, (* b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | ( b*bdv + c*bdv \<up> 2=0)*)
597 \<^rule_thm>\<open>d3_reduce_equation14\<close>, (* bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | ( bdv + c*bdv \<up> 2=0)*)
598 \<^rule_thm>\<open>d3_reduce_equation15\<close>, (* b*bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | ( b*bdv + bdv \<up> 2=0)*)
599 \<^rule_thm>\<open>d3_reduce_equation16\<close>, (* bdv \<up> 2 + bdv \<up> 3=0) = (bdv=0 | ( bdv + bdv \<up> 2=0)*)
600 \<^rule_thm>\<open>d3_isolate_add1\<close>, (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv \<up> 3=0) = (bdv=0 | (b*bdv \<up> 3=a)*)
601 \<^rule_thm>\<open>d3_isolate_add2\<close>, (*[|Not(bdv occurs_in a)|] ==> (a + bdv \<up> 3=0) = (bdv=0 | ( bdv \<up> 3=a)*)
602 \<^rule_thm>\<open>d3_isolate_div\<close>, (*[|Not(b=0)|] ==> (b*bdv \<up> 3=c) = (bdv \<up> 3=c/b*)
603 \<^rule_thm>\<open>d3_root_equation2\<close>, (*(bdv \<up> 3=0) = (bdv=0) *)
604 \<^rule_thm>\<open>d3_root_equation1\<close>], (*bdv \<up> 3=c) = (bdv = nroot 3 c*)
605 scr = Rule.Empty_Prog});
608 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
609 val d4_polyeq_simplify = prep_rls'(
610 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
611 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
612 srls = Rule_Set.Empty, calc = [], errpatts = [],
614 \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)],
615 scr = Rule.Empty_Prog});
618 d0_polyeq_simplify = d0_polyeq_simplify and
619 d1_polyeq_simplify = d1_polyeq_simplify and
620 d2_polyeq_simplify = d2_polyeq_simplify and
621 d2_polyeq_bdv_only_simplify = d2_polyeq_bdv_only_simplify and
622 d2_polyeq_sq_only_simplify = d2_polyeq_sq_only_simplify and
624 d2_polyeq_pqFormula_simplify = d2_polyeq_pqFormula_simplify and
625 d2_polyeq_abcFormula_simplify = d2_polyeq_abcFormula_simplify and
626 d3_polyeq_simplify = d3_polyeq_simplify and
627 d4_polyeq_simplify = d4_polyeq_simplify
629 problem pbl_equ_univ_poly : "polynomial/univariate/equation" =
630 \<open>PolyEq_prls\<close>
631 CAS: "solve (e_e::bool, v_v)"
632 Given: "equality e_e" "solveFor v_v"
634 "~((e_e::bool) is_ratequation_in (v_v::real))"
635 "~((lhs e_e) is_rootTerm_in (v_v::real))"
636 "~((rhs e_e) is_rootTerm_in (v_v::real))"
637 Find: "solutions v_v'i'"
640 problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" =
641 \<open>PolyEq_prls\<close>
642 Method_Ref: "PolyEq/solve_d0_polyeq_equation"
643 CAS: "solve (e_e::bool, v_v)"
644 Given: "equality e_e" "solveFor v_v"
646 "matches (?a = 0) e_e"
647 "(lhs e_e) is_poly_in v_v"
648 "((lhs e_e) has_degree_in v_v ) = 0"
649 Find: "solutions v_v'i'"
652 problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" =
653 \<open>PolyEq_prls\<close>
654 Method_Ref: "PolyEq/solve_d1_polyeq_equation"
655 CAS: "solve (e_e::bool, v_v)"
656 Given: "equality e_e" "solveFor v_v"
658 "matches (?a = 0) e_e"
659 "(lhs e_e) is_poly_in v_v"
660 "((lhs e_e) has_degree_in v_v ) = 1"
661 Find: "solutions v_v'i'"
664 problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" =
665 \<open>PolyEq_prls\<close>
666 Method_Ref: "PolyEq/solve_d2_polyeq_equation"
667 CAS: "solve (e_e::bool, v_v)"
668 Given: "equality e_e" "solveFor v_v"
670 "matches (?a = 0) e_e"
671 "(lhs e_e) is_poly_in v_v "
672 "((lhs e_e) has_degree_in v_v ) = 2"
673 Find: "solutions v_v'i'"
675 problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" =
676 \<open>PolyEq_prls\<close>
677 Method_Ref: "PolyEq/solve_d2_polyeq_sqonly_equation"
678 CAS: "solve (e_e::bool, v_v)"
679 Given: "equality e_e" "solveFor v_v"
681 "matches ( ?a + ?v_ \<up> 2 = 0) e_e |
682 matches ( ?a + ?b*?v_ \<up> 2 = 0) e_e |
683 matches ( ?v_ \<up> 2 = 0) e_e |
684 matches ( ?b*?v_ \<up> 2 = 0) e_e"
685 "Not (matches (?a + ?v_ + ?v_ \<up> 2 = 0) e_e) &
686 Not (matches (?a + ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &
687 Not (matches (?a + ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
688 Not (matches (?a + ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
689 Not (matches ( ?v_ + ?v_ \<up> 2 = 0) e_e) &
690 Not (matches ( ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &
691 Not (matches ( ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
692 Not (matches ( ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e)"
693 Find: "solutions v_v'i'"
695 problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" =
696 \<open>PolyEq_prls\<close>
697 Method_Ref: "PolyEq/solve_d2_polyeq_bdvonly_equation"
698 CAS: "solve (e_e::bool, v_v)"
699 Given: "equality e_e" "solveFor v_v"
701 "matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e |
702 matches ( ?v_ + ?v_ \<up> 2 = 0) e_e |
703 matches ( ?v_ + ?b*?v_ \<up> 2 = 0) e_e |
704 matches (?a*?v_ + ?b*?v_ \<up> 2 = 0) e_e |
705 matches ( ?v_ \<up> 2 = 0) e_e |
706 matches ( ?b*?v_ \<up> 2 = 0) e_e "
707 Find: "solutions v_v'i'"
709 problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" =
710 \<open>PolyEq_prls\<close>
711 Method_Ref: "PolyEq/solve_d2_polyeq_pq_equation"
712 CAS: "solve (e_e::bool, v_v)"
713 Given: "equality e_e" "solveFor v_v"
715 "matches (?a + 1*?v_ \<up> 2 = 0) e_e |
716 matches (?a + ?v_ \<up> 2 = 0) e_e"
717 Find: "solutions v_v'i'"
719 problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" =
720 \<open>PolyEq_prls\<close>
721 Method_Ref: "PolyEq/solve_d2_polyeq_abc_equation"
722 CAS: "solve (e_e::bool, v_v)"
723 Given: "equality e_e" "solveFor v_v"
725 "matches (?a + ?v_ \<up> 2 = 0) e_e |
726 matches (?a + ?b*?v_ \<up> 2 = 0) e_e"
727 Find: "solutions v_v'i'"
730 problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" =
731 \<open>PolyEq_prls\<close>
732 Method_Ref: "PolyEq/solve_d3_polyeq_equation"
733 CAS: "solve (e_e::bool, v_v)"
734 Given: "equality e_e" "solveFor v_v"
736 "matches (?a = 0) e_e"
737 "(lhs e_e) is_poly_in v_v"
738 "((lhs e_e) has_degree_in v_v) = 3"
739 Find: "solutions v_v'i'"
742 problem pbl_equ_univ_poly_deg4 : "degree_4/polynomial/univariate/equation" =
743 \<open>PolyEq_prls\<close>
744 (*Method: "PolyEq/solve_d4_polyeq_equation"*)
745 CAS: "solve (e_e::bool, v_v)"
746 Given: "equality e_e" "solveFor v_v"
748 "matches (?a = 0) e_e"
749 "(lhs e_e) is_poly_in v_v"
750 "((lhs e_e) has_degree_in v_v) = 4"
751 Find: "solutions v_v'i'"
753 (*--- normalise ---*)
754 problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" =
755 \<open>PolyEq_prls\<close>
756 Method_Ref: "PolyEq/normalise_poly"
757 CAS: "solve (e_e::bool, v_v)"
758 Given: "equality e_e" "solveFor v_v"
760 "(Not((matches (?a = 0 ) e_e ))) |
761 (Not(((lhs e_e) is_poly_in v_v)))"
762 Find: "solutions v_v'i'"
764 (*-------------------------expanded-----------------------*)
765 problem "pbl_equ_univ_expand" : "expanded/univariate/equation" =
766 \<open>PolyEq_prls\<close>
767 CAS: "solve (e_e::bool, v_v)"
768 Given: "equality e_e" "solveFor v_v"
770 "matches (?a = 0) e_e"
771 "(lhs e_e) is_expanded_in v_v "
772 Find: "solutions v_v'i'"
775 problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" =
776 \<open>PolyEq_prls\<close>
777 Method_Ref: "PolyEq/complete_square"
778 CAS: "solve (e_e::bool, v_v)"
779 Given: "equality e_e" "solveFor v_v"
780 Where: "((lhs e_e) has_degree_in v_v) = 2"
781 Find: "solutions v_v'i'"
783 text \<open>"-------------------------methods-----------------------"\<close>
785 method met_polyeq : "PolyEq" =
786 \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
787 crls=PolyEq_crls, errpats = [], nrls = norm_Rational}\<close>
789 partial_function (tailrec) normalize_poly_eq :: "bool \<Rightarrow> real \<Rightarrow> bool"
791 "normalize_poly_eq e_e v_v = (
794 (Try (Rewrite ''all_left'')) #>
795 (Try (Repeat (Rewrite ''makex1_x''))) #>
796 (Try (Repeat (Rewrite_Set ''expand_binoms''))) #>
797 (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) #>
798 (Try (Repeat (Rewrite_Set ''polyeq_simplify''))) ) e_e
800 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
801 [BOOL e_e, REAL v_v])"
803 method met_polyeq_norm : "PolyEq/normalise_poly" =
804 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, calc=[],
805 crls=PolyEq_crls, errpats = [], nrls = norm_Rational}\<close>
806 Program: normalize_poly_eq.simps
807 Given: "equality e_e" "solveFor v_v"
808 Where: "(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"
809 Find: "solutions v_v'i'"
811 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
813 "solve_poly_equ e_e v_v = (
815 e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'')) e_e
819 method met_polyeq_d0 : "PolyEq/solve_d0_polyeq_equation" =
820 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
821 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
822 nrls = norm_Rational}\<close>
823 Program: solve_poly_equ.simps
824 Given: "equality e_e" "solveFor v_v"
825 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 0"
826 Find: "solutions v_v'i'"
828 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
830 "solve_poly_eq1 e_e v_v = (
833 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) #>
834 (Try (Rewrite_Set ''polyeq_simplify'')) #>
835 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
838 Check_elementwise L_L {(v_v::real). Assumptions})"
840 method met_polyeq_d1 : "PolyEq/solve_d1_polyeq_equation" =
841 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
842 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
843 nrls = norm_Rational}\<close>
844 Program: solve_poly_eq1.simps
845 Given: "equality e_e" "solveFor v_v"
846 Where: "(lhs e_e) is_poly_in v_v" "((lhs e_e) has_degree_in v_v) = 1"
847 Find: "solutions v_v'i'"
849 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
851 "solve_poly_equ2 e_e v_v = (
854 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) #>
855 (Try (Rewrite_Set ''polyeq_simplify'')) #>
856 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) #>
857 (Try (Rewrite_Set ''polyeq_simplify'')) #>
858 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
861 Check_elementwise L_L {(v_v::real). Assumptions})"
863 method met_polyeq_d22 : "PolyEq/solve_d2_polyeq_equation" =
864 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
865 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
866 nrls = norm_Rational}\<close>
867 Program: solve_poly_equ2.simps
868 Given: "equality e_e" "solveFor v_v"
869 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
870 Find: "solutions v_v'i'"
872 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
874 "solve_poly_equ0 e_e v_v = (
877 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'')) #>
878 (Try (Rewrite_Set ''polyeq_simplify'')) #>
879 (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'')) #>
880 (Try (Rewrite_Set ''polyeq_simplify'')) #>
881 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
884 Check_elementwise L_L {(v_v::real). Assumptions})"
886 method met_polyeq_d2_bdvonly : "PolyEq/solve_d2_polyeq_bdvonly_equation" =
887 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
888 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
889 nrls = norm_Rational}\<close>
890 Program: solve_poly_equ0.simps
891 Given: "equality e_e" "solveFor v_v"
892 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
893 Find: "solutions v_v'i'"
895 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
897 "solve_poly_equ_sqrt e_e v_v = (
900 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'')) #>
901 (Try (Rewrite_Set ''polyeq_simplify'')) #>
902 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
905 Check_elementwise L_L {(v_v::real). Assumptions})"
907 method met_polyeq_d2_sqonly : "PolyEq/solve_d2_polyeq_sqonly_equation" =
908 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
909 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
910 nrls = norm_Rational}\<close>
911 Program: solve_poly_equ_sqrt.simps
912 Given: "equality e_e" "solveFor v_v"
913 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
914 Find: "solutions v_v'i'"
916 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
918 "solve_poly_equ_pq e_e v_v = (
921 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'')) #>
922 (Try (Rewrite_Set ''polyeq_simplify'')) #>
923 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
926 Check_elementwise L_L {(v_v::real). Assumptions})"
928 method met_polyeq_d2_pq : "PolyEq/solve_d2_polyeq_pq_equation" =
929 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
930 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
931 nrls = norm_Rational}\<close>
932 Program: solve_poly_equ_pq.simps
933 Given: "equality e_e" "solveFor v_v"
934 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
935 Find: "solutions v_v'i'"
937 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
939 "solve_poly_equ_abc e_e v_v = (
942 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'')) #>
943 (Try (Rewrite_Set ''polyeq_simplify'')) #>
944 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
946 in Check_elementwise L_L {(v_v::real). Assumptions})"
948 method met_polyeq_d2_abc : "PolyEq/solve_d2_polyeq_abc_equation" =
949 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule_Set.empty, prls=PolyEq_prls,
950 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
951 nrls = norm_Rational}\<close>
952 Program: solve_poly_equ_abc.simps
953 Given: "equality e_e" "solveFor v_v"
954 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
955 Find: "solutions v_v'i'"
957 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
959 "solve_poly_equ3 e_e v_v = (
962 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'')) #>
963 (Try (Rewrite_Set ''polyeq_simplify'')) #>
964 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) #>
965 (Try (Rewrite_Set ''polyeq_simplify'')) #>
966 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''d1_polyeq_simplify'')) #>
967 (Try (Rewrite_Set ''polyeq_simplify'')) #>
968 (Try (Rewrite_Set ''norm_Rational_parenthesized''))) e_e;
971 Check_elementwise L_L {(v_v::real). Assumptions})"
973 method met_polyeq_d3 : "PolyEq/solve_d3_polyeq_equation" =
974 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
975 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
976 nrls = norm_Rational}\<close>
977 Program: solve_poly_equ3.simps
978 Given: "equality e_e" "solveFor v_v"
979 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 3"
980 Find: "solutions v_v'i'"
982 (*.solves all expanded (ie. normalised) terms of degree 2.*)
983 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
984 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
985 partial_function (tailrec) solve_by_completing_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
987 "solve_by_completing_square e_e v_v = (
989 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'')) #>
990 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'')) #>
991 (Try (Rewrite ''square_explicit1'')) #>
992 (Try (Rewrite ''square_explicit2'')) #>
993 (Rewrite ''root_plus_minus'') #>
994 (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1''))) #>
995 (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2''))) #>
996 (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3''))) #>
997 (Try (Rewrite_Set ''calculate_RootRat'')) #>
998 (Try (Repeat (Calculate ''SQRT'')))) e_e
1002 method met_polyeq_complsq : "PolyEq/complete_square" =
1003 \<open>{rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule_Set.empty,prls=PolyEq_prls,
1004 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1005 nrls = norm_Rational}\<close>
1006 Program: solve_by_completing_square.simps
1007 Given: "equality e_e" "solveFor v_v"
1008 Where: "matches (?a = 0) e_e" "((lhs e_e) has_degree_in v_v) = 2"
1009 Find: "solutions v_v'i'"
1013 (* termorder hacked by MG, adapted later by WN *)
1014 (**)local (*. for make_polynomial_in .*)
1016 open Term; (* for type order = EQUAL | LESS | GREATER *)
1018 fun pr_ord EQUAL = "EQUAL"
1019 | pr_ord LESS = "LESS"
1020 | pr_ord GREATER = "GREATER";
1022 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
1023 | dest_hd' x (t as Free (a, T)) =
1024 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
1025 else (((a, 0), T), 1)
1026 | dest_hd' _ (Var v) = (v, 2)
1027 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
1028 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
1029 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
1031 fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $
1032 Free (var, _) $ Free (pot, _)) =
1033 (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
1037 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
1038 1000 * (the (TermC.int_opt_of_string pot)))
1039 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
1040 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1041 | size_of_term' i pr x (t as Abs (_, _, body)) =
1042 (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
1043 1 + size_of_term' (i + 1) pr x body)
1044 | size_of_term' i pr x (f $ t) =
1046 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
1047 val s1 = size_of_term' (i + 1) pr x f
1048 val s2 = size_of_term' (i + 1) pr x t
1049 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
1051 | size_of_term' i pr x t =
1052 (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
1058 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
1059 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
1060 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1061 | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
1063 fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1065 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
1067 case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
1068 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
1070 | term_ord' i pr x _ (t, u) =
1072 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
1074 case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
1076 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1078 (case hd_ord (i + 1) pr x (f, g) of
1079 EQUAL => (terms_ord x (i + 1) pr) (ts, us)
1083 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
1085 and hd_ord i pr x (f, g) = (* ~ term.ML *)
1087 val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
1089 (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
1090 (dest_hd' x f, dest_hd' x g)
1091 val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
1093 and terms_ord x i pr (ts, us) =
1095 val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
1096 val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1097 val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
1102 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
1103 ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
1106 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
1107 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
1113 val order_add_mult_in = prep_rls'(
1114 Rule_Def.Repeat{id = "order_add_mult_in", preconds = [],
1115 rew_ord = ("ord_make_polynomial_in", ord_make_polynomial_in false @{theory "Poly"}),
1116 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1117 calc = [], errpatts = [],
1119 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
1120 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1121 \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1122 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
1123 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
1124 \<^rule_thm>\<open>add.assoc\<close>], (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1125 scr = Rule.Empty_Prog});
1129 val collect_bdv = prep_rls'(
1130 Rule_Def.Repeat{id = "collect_bdv", preconds = [],
1131 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1132 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1133 calc = [], errpatts = [],
1134 rules = [\<^rule_thm>\<open>bdv_collect_1\<close>,
1135 \<^rule_thm>\<open>bdv_collect_2\<close>,
1136 \<^rule_thm>\<open>bdv_collect_3\<close>,
1138 \<^rule_thm>\<open>bdv_collect_assoc1_1\<close>,
1139 \<^rule_thm>\<open>bdv_collect_assoc1_2\<close>,
1140 \<^rule_thm>\<open>bdv_collect_assoc1_3\<close>,
1142 \<^rule_thm>\<open>bdv_collect_assoc2_1\<close>,
1143 \<^rule_thm>\<open>bdv_collect_assoc2_2\<close>,
1144 \<^rule_thm>\<open>bdv_collect_assoc2_3\<close>,
1147 \<^rule_thm>\<open>bdv_n_collect_1\<close>,
1148 \<^rule_thm>\<open>bdv_n_collect_2\<close>,
1149 \<^rule_thm>\<open>bdv_n_collect_3\<close>,
1151 \<^rule_thm>\<open>bdv_n_collect_assoc1_1\<close>,
1152 \<^rule_thm>\<open>bdv_n_collect_assoc1_2\<close>,
1153 \<^rule_thm>\<open>bdv_n_collect_assoc1_3\<close>,
1155 \<^rule_thm>\<open>bdv_n_collect_assoc2_1\<close>,
1156 \<^rule_thm>\<open>bdv_n_collect_assoc2_2\<close>,
1157 \<^rule_thm>\<open>bdv_n_collect_assoc2_3\<close>],
1158 scr = Rule.Empty_Prog});
1162 (*.transforms an arbitrary term without roots to a polynomial [4]
1163 according to knowledge/Poly.sml.*)
1164 val make_polynomial_in = prep_rls'(
1166 id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1167 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1169 Rule.Rls_ expand_poly,
1170 Rule.Rls_ order_add_mult_in,
1171 Rule.Rls_ simplify_power,
1172 Rule.Rls_ collect_numerals,
1173 Rule.Rls_ reduce_012,
1174 \<^rule_thm>\<open>realpow_oneI\<close>,
1175 Rule.Rls_ discard_parentheses,
1176 Rule.Rls_ collect_bdv],
1177 scr = Rule.Empty_Prog});
1181 val separate_bdvs = Rule_Set.append_rules "separate_bdvs" collect_bdv [
1182 \<^rule_thm>\<open>separate_bdv\<close>, (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1183 \<^rule_thm>\<open>separate_bdv_n\<close>,
1184 \<^rule_thm>\<open>separate_1_bdv\<close>, (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1185 \<^rule_thm>\<open>separate_1_bdv_n\<close>, (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1186 \<^rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1187 WN051031 DOES NOT BELONG TO HERE*)];
1190 val make_ratpoly_in = prep_rls'(
1192 id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1193 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1195 Rule.Rls_ norm_Rational,
1196 Rule.Rls_ order_add_mult_in,
1197 Rule.Rls_ discard_parentheses,
1198 Rule.Rls_ separate_bdvs,
1199 (* Rule.Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1201 (*\<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e") too weak!*)],
1202 scr = Rule.Empty_Prog});
1205 order_add_mult_in = order_add_mult_in and
1206 collect_bdv = collect_bdv and
1207 make_polynomial_in = make_polynomial_in and
1208 make_ratpoly_in = make_ratpoly_in and
1209 separate_bdvs = separate_bdvs