1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for Root Equations
10 theory RootEq imports Root end
13 (*-------------------------root-----------------------*)
14 is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
15 is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
16 is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
18 (*----------------------scripts-----------------------*)
19 Norm'_sq'_root'_equation
21 bool list] => bool list"
22 ("((Script Norm'_sq'_root'_equation (_ _ =))//
24 Solve'_sq'_root'_equation
26 bool list] => bool list"
27 ("((Script Solve'_sq'_root'_equation (_ _ =))//
29 Solve'_left'_sq'_root'_equation
31 bool list] => bool list"
32 ("((Script Solve'_left'_sq'_root'_equation (_ _ =))//
34 Solve'_right'_sq'_root'_equation
36 bool list] => bool list"
37 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
44 real_assoc_1 "a+(b+c) = a+b+c"
45 real_assoc_2 "a*(b*c) = a*b*c"
47 (* simplification of root*)
48 sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a"
49 sqrt_square_2 "sqrt (a ^^^ 2) = a"
50 sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)"
51 sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)"
53 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
54 sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==>
55 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
56 sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==>
57 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
58 sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==>
59 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
60 sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==>
61 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
62 sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==>
63 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
64 sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==>
65 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
66 sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==>
67 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
68 sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==>
69 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
70 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
71 sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==>
72 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
73 sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==>
74 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
75 sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==>
76 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
77 sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==>
78 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
80 (* eliminate isolates sqrt *)
81 sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==>
82 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
83 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
84 sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==>
85 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
86 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
87 sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==>
88 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
89 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
90 sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==>
91 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
92 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
93 sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
94 ( (sqrt (a) = b) = (a = (b^^^2)))"
95 sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
96 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
97 sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
98 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
99 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
100 sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
101 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
102 sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
103 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
104 sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
105 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
106 sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
107 ( (a = sqrt (b)) = (a^^^2 = b))"
108 sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
109 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
110 sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
111 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
112 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
113 sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
114 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
115 sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
116 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
117 sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
118 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
121 (*-------------------------functions---------------------*)
122 (* true if bdv is under sqrt of a Equation*)
123 fun is_rootTerm_in t v =
125 fun coeff_in c v = member op = (vars c) v;
126 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
127 (* at the moment there is no term like this, but ....*)
128 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
129 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
130 | findroot (t as (Const ("Root.sqrt",_) $ t2)) v = coeff_in t2 v
131 | findroot (_ $ t2) v = (findroot t2 v)
132 | findroot _ _ = false;
137 fun is_sqrtTerm_in t v =
139 fun coeff_in c v = member op = (vars c) v;
140 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
141 (* at the moment there is no term like this, but ....*)
142 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
143 | findsqrt (t as (Const ("Root.sqrt",_) $ a)) v = coeff_in a v
144 | findsqrt (_ $ t1) v = (findsqrt t1 v)
145 | findsqrt _ _ = false;
150 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
151 and the subterm ist connected with + or * --> is normalized*)
152 fun is_normSqrtTerm_in t v =
154 fun coeff_in c v = member op = (vars c) v;
155 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
156 (* at the moment there is no term like this, but ....*)
157 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
158 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
159 | isnorm (Const ("op -",_) $ _ $ _) v = false
160 | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
161 (is_sqrtTerm_in t2 v)
162 | isnorm (Const ("Root.sqrt",_) $ t1) v = coeff_in t1 v
163 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
164 | isnorm _ _ = false;
169 fun eval_is_rootTerm_in _ _
170 (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
171 if is_rootTerm_in t v then
172 SOME ((term2str p) ^ " = True",
173 Trueprop $ (mk_equality (p, HOLogic.true_const)))
174 else SOME ((term2str p) ^ " = True",
175 Trueprop $ (mk_equality (p, HOLogic.false_const)))
176 | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
178 fun eval_is_sqrtTerm_in _ _
179 (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
180 if is_sqrtTerm_in t v then
181 SOME ((term2str p) ^ " = True",
182 Trueprop $ (mk_equality (p, HOLogic.true_const)))
183 else SOME ((term2str p) ^ " = True",
184 Trueprop $ (mk_equality (p, HOLogic.false_const)))
185 | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
187 fun eval_is_normSqrtTerm_in _ _
188 (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
189 if is_normSqrtTerm_in t v then
190 SOME ((term2str p) ^ " = True",
191 Trueprop $ (mk_equality (p, HOLogic.true_const)))
192 else SOME ((term2str p) ^ " = True",
193 Trueprop $ (mk_equality (p, HOLogic.false_const)))
194 | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
196 (*-------------------------rulse-------------------------*)
197 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
198 append_rls "RootEq_prls" e_rls
199 [Calc ("Atools.ident",eval_ident "#ident_"),
200 Calc ("Tools.matches",eval_matches ""),
201 Calc ("Tools.lhs" ,eval_lhs ""),
202 Calc ("Tools.rhs" ,eval_rhs ""),
203 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
204 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
205 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
206 Calc ("op =",eval_equal "#equal_"),
207 Thm ("not_true",num_str @{not_true),
208 Thm ("not_false",num_str @{not_false),
209 Thm ("and_true",num_str @{and_true),
210 Thm ("and_false",num_str @{and_false),
211 Thm ("or_true",num_str @{or_true),
212 Thm ("or_false",num_str @{or_false)
216 append_rls "RootEq_erls" Root_erls
217 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
221 append_rls "RootEq_crls" Root_crls
222 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
226 append_rls "rooteq_srls" e_rls
227 [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
228 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
229 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
232 ruleset' := overwritelthy @{theory} (!ruleset',
233 [("RootEq_erls",RootEq_erls),
234 (*FIXXXME:del with rls.rls'*)
235 ("rooteq_srls",rooteq_srls)
238 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
239 val sqrt_isolate = prep_rls(
240 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
241 erls = RootEq_erls, srls = Erls, calc = [],
243 Thm("sqrt_square_1",num_str @{sqrt_square_1),
244 (* (sqrt a)^^^2 -> a *)
245 Thm("sqrt_square_2",num_str @{sqrt_square_2),
246 (* sqrt (a^^^2) -> a *)
247 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
248 (* sqrt a sqrt b -> sqrt(ab) *)
249 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
250 (* a sqrt b sqrt c -> a sqrt(bc) *)
251 Thm("sqrt_square_equation_both_1",
252 num_str @{sqrt_square_equation_both_1),
253 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
254 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
255 Thm("sqrt_square_equation_both_2",
256 num_str @{sqrt_square_equation_both_2),
257 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
258 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
259 Thm("sqrt_square_equation_both_3",
260 num_str @{sqrt_square_equation_both_3),
261 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
262 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
263 Thm("sqrt_square_equation_both_4",
264 num_str @{sqrt_square_equation_both_4),
265 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
266 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
267 Thm("sqrt_isolate_l_add1",
268 num_str @{sqrt_isolate_l_add1),
269 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
270 Thm("sqrt_isolate_l_add2",
271 num_str @{sqrt_isolate_l_add2),
272 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
273 Thm("sqrt_isolate_l_add3",
274 num_str @{sqrt_isolate_l_add3),
275 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
276 Thm("sqrt_isolate_l_add4",
277 num_str @{sqrt_isolate_l_add4),
278 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
279 Thm("sqrt_isolate_l_add5",
280 num_str @{sqrt_isolate_l_add5),
281 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
282 Thm("sqrt_isolate_l_add6",
283 num_str @{sqrt_isolate_l_add6),
284 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
285 (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*)
286 (* b*sqrt(x) = d sqrt(x) d/b *)
287 Thm("sqrt_isolate_r_add1",
288 num_str @{sqrt_isolate_r_add1),
289 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
290 Thm("sqrt_isolate_r_add2",
291 num_str @{sqrt_isolate_r_add2),
292 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
293 Thm("sqrt_isolate_r_add3",
294 num_str @{sqrt_isolate_r_add3),
295 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
296 Thm("sqrt_isolate_r_add4",
297 num_str @{sqrt_isolate_r_add4),
298 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
299 Thm("sqrt_isolate_r_add5",
300 num_str @{sqrt_isolate_r_add5),
301 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
302 Thm("sqrt_isolate_r_add6",
303 num_str @{sqrt_isolate_r_add6),
304 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
305 (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*)
306 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
307 Thm("sqrt_square_equation_left_1",
308 num_str @{sqrt_square_equation_left_1),
309 (* sqrt(x)=b -> x=b^2 *)
310 Thm("sqrt_square_equation_left_2",
311 num_str @{sqrt_square_equation_left_2),
312 (* c*sqrt(x)=b -> c^2*x=b^2 *)
313 Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3),
314 (* c/sqrt(x)=b -> c^2/x=b^2 *)
315 Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4),
316 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
317 Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5),
318 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
319 Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6),
320 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
321 Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1),
322 (* a=sqrt(x) ->a^2=x *)
323 Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2),
324 (* a=c*sqrt(x) ->a^2=c^2*x *)
325 Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3),
326 (* a=c/sqrt(x) ->a^2=c^2/x *)
327 Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4),
328 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
329 Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5),
330 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
331 Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6)
332 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
333 ],scr = Script ((term_of o the o (parse thy)) "empty_script")
336 ruleset' := overwritelthy @{theory} (!ruleset',
337 [("sqrt_isolate",sqrt_isolate)
339 (* -- left 28.08.02--*)
340 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
341 val l_sqrt_isolate = prep_rls(
342 Rls {id = "l_sqrt_isolate", preconds = [],
343 rew_ord = ("termlessI",termlessI),
344 erls = RootEq_erls, srls = Erls, calc = [],
346 Thm("sqrt_square_1",num_str @{sqrt_square_1),
347 (* (sqrt a)^^^2 -> a *)
348 Thm("sqrt_square_2",num_str @{sqrt_square_2),
349 (* sqrt (a^^^2) -> a *)
350 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
351 (* sqrt a sqrt b -> sqrt(ab) *)
352 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
353 (* a sqrt b sqrt c -> a sqrt(bc) *)
354 Thm("sqrt_isolate_l_add1",num_str @{sqrt_isolate_l_add1),
355 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
356 Thm("sqrt_isolate_l_add2",num_str @{sqrt_isolate_l_add2),
357 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
358 Thm("sqrt_isolate_l_add3",num_str @{sqrt_isolate_l_add3),
359 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
360 Thm("sqrt_isolate_l_add4",num_str @{sqrt_isolate_l_add4),
361 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
362 Thm("sqrt_isolate_l_add5",num_str @{sqrt_isolate_l_add5),
363 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
364 Thm("sqrt_isolate_l_add6",num_str @{sqrt_isolate_l_add6),
365 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
366 (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*)
367 (* b*sqrt(x) = d sqrt(x) d/b *)
368 Thm("sqrt_square_equation_left_1",num_str @{sqrt_square_equation_left_1),
369 (* sqrt(x)=b -> x=b^2 *)
370 Thm("sqrt_square_equation_left_2",num_str @{sqrt_square_equation_left_2),
371 (* a*sqrt(x)=b -> a^2*x=b^2*)
372 Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3),
373 (* c/sqrt(x)=b -> c^2/x=b^2 *)
374 Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4),
375 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
376 Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5),
377 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
378 Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6)
379 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
381 scr = Script ((term_of o the o (parse thy)) "empty_script")
384 ruleset' := overwritelthy @{theory} (!ruleset',
385 [("l_sqrt_isolate",l_sqrt_isolate)
388 (* -- right 28.8.02--*)
389 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
390 val r_sqrt_isolate = prep_rls(
391 Rls {id = "r_sqrt_isolate", preconds = [],
392 rew_ord = ("termlessI",termlessI),
393 erls = RootEq_erls, srls = Erls, calc = [],
395 Thm("sqrt_square_1",num_str @{sqrt_square_1),
396 (* (sqrt a)^^^2 -> a *)
397 Thm("sqrt_square_2",num_str @{sqrt_square_2),
398 (* sqrt (a^^^2) -> a *)
399 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
400 (* sqrt a sqrt b -> sqrt(ab) *)
401 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
402 (* a sqrt b sqrt c -> a sqrt(bc) *)
403 Thm("sqrt_isolate_r_add1",num_str @{sqrt_isolate_r_add1),
404 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
405 Thm("sqrt_isolate_r_add2",num_str @{sqrt_isolate_r_add2),
406 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
407 Thm("sqrt_isolate_r_add3",num_str @{sqrt_isolate_r_add3),
408 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
409 Thm("sqrt_isolate_r_add4",num_str @{sqrt_isolate_r_add4),
410 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
411 Thm("sqrt_isolate_r_add5",num_str @{sqrt_isolate_r_add5),
412 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
413 Thm("sqrt_isolate_r_add6",num_str @{sqrt_isolate_r_add6),
414 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
415 (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*)
416 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
417 Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1),
418 (* a=sqrt(x) ->a^2=x *)
419 Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2),
420 (* a=c*sqrt(x) ->a^2=c^2*x *)
421 Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3),
422 (* a=c/sqrt(x) ->a^2=c^2/x *)
423 Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4),
424 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
425 Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5),
426 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
427 Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6)
428 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
430 scr = Script ((term_of o the o (parse thy)) "empty_script")
433 ruleset' := overwritelthy @{theory} (!ruleset',
434 [("r_sqrt_isolate",r_sqrt_isolate)
437 val rooteq_simplify = prep_rls(
438 Rls {id = "rooteq_simplify",
439 preconds = [], rew_ord = ("termlessI",termlessI),
440 erls = RootEq_erls, srls = Erls, calc = [],
441 (*asm_thm = [("sqrt_square_1","")],*)
442 rules = [Thm ("real_assoc_1",num_str @{real_assoc_1),
443 (* a+(b+c) = a+b+c *)
444 Thm ("real_assoc_2",num_str @{real_assoc_2),
445 (* a*(b*c) = a*b*c *)
446 Calc ("op +",eval_binop "#add_"),
447 Calc ("op -",eval_binop "#sub_"),
448 Calc ("op *",eval_binop "#mult_"),
449 Calc ("HOL.divide", eval_cancel "#divide_"),
450 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
451 Calc ("Atools.pow" ,eval_binop "#power_"),
452 Thm("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
453 Thm("real_minus_binom_pow2",num_str @{real_minus_binom_pow2),
454 Thm("realpow_mul",num_str @{realpow_mul),
455 (* (a * b)^n = a^n * b^n*)
456 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
457 (* sqrt b * sqrt c = sqrt(b*c) *)
458 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
459 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
460 Thm("sqrt_square_2",num_str @{sqrt_square_2),
461 (* sqrt (a^^^2) = a *)
462 Thm("sqrt_square_1",num_str @{sqrt_square_1)
463 (* sqrt a ^^^ 2 = a *)
465 scr = Script ((term_of o the o (parse thy)) "empty_script")
467 ruleset' := overwritelthy @{theory} (!ruleset',
468 [("rooteq_simplify",rooteq_simplify)
471 (*-------------------------Problem-----------------------*)
473 (get_pbt ["root","univariate","equation"]);
476 (* ---------root----------- *)
478 (prep_pbt (theory "RootEq") "pbl_equ_univ_root" [] e_pblID
479 (["root","univariate","equation"],
480 [("#Given" ,["equality e_","solveFor v_"]),
481 ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | " ^
482 "(rhs e_) is_rootTerm_in (v_::real)"]),
483 ("#Find" ,["solutions v_i_"])
485 RootEq_prls, SOME "solve (e_::bool, v_)",
487 (* ---------sqrt----------- *)
489 (prep_pbt (theory "RootEq") "pbl_equ_univ_root_sq" [] e_pblID
490 (["sq","root","univariate","equation"],
491 [("#Given" ,["equality e_","solveFor v_"]),
492 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
493 " ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |" ^
494 "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
495 " ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
496 ("#Find" ,["solutions v_i_"])
498 RootEq_prls, SOME "solve (e_::bool, v_)",
499 [["RootEq","solve_sq_root_equation"]]));
500 (* ---------normalize----------- *)
502 (prep_pbt (theory "RootEq") "pbl_equ_univ_root_norm" [] e_pblID
503 (["normalize","root","univariate","equation"],
504 [("#Given" ,["equality e_","solveFor v_"]),
505 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
506 " Not((lhs e_) is_normSqrtTerm_in (v_::real))) | " ^
507 "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
508 " Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
509 ("#Find" ,["solutions v_i_"])
511 RootEq_prls, SOME "solve (e_::bool, v_)",
512 [["RootEq","norm_sq_root_equation"]]));
514 (*-------------------------methods-----------------------*)
515 (* ---- root 20.8.02 ---*)
517 (prep_met (theory "RootEq") "met_rooteq" [] e_metID
520 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
521 crls=RootEq_crls, nrls=norm_Poly(*,
522 asm_rls=[],asm_thm=[]*)}, "empty_script"));
523 (*-- normalize 20.10.02 --*)
525 (prep_met (theory "RootEq") "met_rooteq_norm" [] e_metID
526 (["RootEq","norm_sq_root_equation"],
527 [("#Given" ,["equality e_","solveFor v_"]),
528 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
529 " Not((lhs e_) is_normSqrtTerm_in (v_::real))) | " ^
530 "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
531 " Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
532 ("#Find" ,["solutions v_i_"])
534 {rew_ord'="termlessI",
539 crls=RootEq_crls, nrls=norm_Poly(*,
541 asm_thm=[("sqrt_square_1","")]*)},
542 "Script Norm_sq_root_equation (e_::bool) (v_::real) = " ^
543 "(let e_ = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
544 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
545 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
546 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
547 " (Try (Rewrite_Set rooteq_simplify True))) e_ " ^
548 " in ((SubProblem (RootEq_,[univariate,equation], " ^
549 " [no_met]) [bool_ e_, real_ v_])))"
553 (prep_met (theory "RootEq") "met_rooteq_sq" [] e_metID
554 (["RootEq","solve_sq_root_equation"],
555 [("#Given" ,["equality e_","solveFor v_"]),
556 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
557 " ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |" ^
558 "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
559 " ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
560 ("#Find" ,["solutions v_i_"])
562 {rew_ord'="termlessI",
567 crls=RootEq_crls, nrls=norm_Poly},
568 "Script Solve_sq_root_equation (e_::bool) (v_::real) = " ^
570 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ " ^
571 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
572 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
573 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
574 " (Try (Rewrite_Set rooteq_simplify True))) e_;" ^
575 " (L_::bool list) = " ^
576 " (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))" ^
577 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
578 " [no_met]) [bool_ e_, real_ v_]) " ^
579 " else (SubProblem (RootEq_,[univariate,equation], " ^
580 " [no_met]) [bool_ e_, real_ v_])) " ^
581 " in Check_elementwise L_ {(v_::real). Assumptions})"
584 (*-- right 28.08.02 --*)
586 (prep_met (theory "RootEq") "met_rooteq_sq_right" [] e_metID
587 (["RootEq","solve_right_sq_root_equation"],
588 [("#Given" ,["equality e_","solveFor v_"]),
589 ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
590 ("#Find" ,["solutions v_i_"])
592 {rew_ord'="termlessI",
597 crls=RootEq_crls, nrls=norm_Poly},
598 "Script Solve_right_sq_root_equation (e_::bool) (v_::real) = " ^
600 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ " ^
601 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
602 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
603 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
604 " (Try (Rewrite_Set rooteq_simplify False))) e_ " ^
605 " in if ((rhs e_) is_sqrtTerm_in v_) " ^
606 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
607 " [no_met]) [bool_ e_, real_ v_]) " ^
608 " else ((SubProblem (RootEq_,[univariate,equation], " ^
609 " [no_met]) [bool_ e_, real_ v_])))"
612 (*-- left 28.08.02 --*)
614 (prep_met (theory "RootEq") "met_rooteq_sq_left" [] e_metID
615 (["RootEq","solve_left_sq_root_equation"],
616 [("#Given" ,["equality e_","solveFor v_"]),
617 ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
618 ("#Find" ,["solutions v_i_"])
620 {rew_ord'="termlessI",
625 crls=RootEq_crls, nrls=norm_Poly},
626 "Script Solve_left_sq_root_equation (e_::bool) (v_::real) = " ^
628 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ " ^
629 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
630 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
631 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
632 " (Try (Rewrite_Set rooteq_simplify False))) e_ " ^
633 " in if ((lhs e_) is_sqrtTerm_in v_) " ^
634 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
635 " [no_met]) [bool_ e_, real_ v_]) " ^
636 " else ((SubProblem (RootEq_,[univariate,equation], " ^
637 " [no_met]) [bool_ e_, real_ v_])))"
640 calclist':= overwritel (!calclist',
641 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
642 eval_is_rootTerm_in"")),
643 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
644 eval_is_sqrtTerm_in"")),
645 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
646 eval_is_normSqrtTerm_in""))
647 ]);(*("", ("", "")),*)