1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for Root Equations
10 theory RootEq imports Root begin
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))))"
123 (*-------------------------functions---------------------*)
124 (* true if bdv is under sqrt of a Equation*)
125 fun is_rootTerm_in t v =
127 fun coeff_in c v = member op = (vars c) v;
128 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
129 (* at the moment there is no term like this, but ....*)
130 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
131 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
132 | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v
133 | findroot (_ $ t2) v = (findroot t2 v)
134 | findroot _ _ = false;
139 fun is_sqrtTerm_in t v =
141 fun coeff_in c v = member op = (vars c) v;
142 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
143 (* at the moment there is no term like this, but ....*)
144 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
145 | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v
146 | findsqrt (_ $ t1) v = (findsqrt t1 v)
147 | findsqrt _ _ = false;
152 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
153 and the subterm ist connected with + or * --> is normalized*)
154 fun is_normSqrtTerm_in t v =
156 fun coeff_in c v = member op = (vars c) v;
157 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
158 (* at the moment there is no term like this, but ....*)
159 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
160 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
161 | isnorm (Const ("op -",_) $ _ $ _) v = false
162 | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
163 (is_sqrtTerm_in t2 v)
164 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
165 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
166 | isnorm _ _ = false;
171 fun eval_is_rootTerm_in _ _
172 (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
173 if is_rootTerm_in t v then
174 SOME ((term2str p) ^ " = True",
175 Trueprop $ (mk_equality (p, HOLogic.true_const)))
176 else SOME ((term2str p) ^ " = True",
177 Trueprop $ (mk_equality (p, HOLogic.false_const)))
178 | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
180 fun eval_is_sqrtTerm_in _ _
181 (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
182 if is_sqrtTerm_in t v then
183 SOME ((term2str p) ^ " = True",
184 Trueprop $ (mk_equality (p, HOLogic.true_const)))
185 else SOME ((term2str p) ^ " = True",
186 Trueprop $ (mk_equality (p, HOLogic.false_const)))
187 | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
189 fun eval_is_normSqrtTerm_in _ _
190 (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
191 if is_normSqrtTerm_in t v then
192 SOME ((term2str p) ^ " = True",
193 Trueprop $ (mk_equality (p, HOLogic.true_const)))
194 else SOME ((term2str p) ^ " = True",
195 Trueprop $ (mk_equality (p, HOLogic.false_const)))
196 | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
198 (*-------------------------rulse-------------------------*)
199 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
200 append_rls "RootEq_prls" e_rls
201 [Calc ("Atools.ident",eval_ident "#ident_"),
202 Calc ("Tools.matches",eval_matches ""),
203 Calc ("Tools.lhs" ,eval_lhs ""),
204 Calc ("Tools.rhs" ,eval_rhs ""),
205 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
206 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
207 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
208 Calc ("op =",eval_equal "#equal_"),
209 Thm ("not_true",num_str @{thm not_true}),
210 Thm ("not_false",num_str @{thm not_false}),
211 Thm ("and_true",num_str @{thm and_true}),
212 Thm ("and_false",num_str @{thm and_false}),
213 Thm ("or_true",num_str @{thm or_true}),
214 Thm ("or_false",num_str @{thm or_false})
218 append_rls "RootEq_erls" Root_erls
219 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
223 append_rls "RootEq_crls" Root_crls
224 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
228 append_rls "rooteq_srls" e_rls
229 [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
230 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
231 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
234 ruleset' := overwritelthy @{theory} (!ruleset',
235 [("RootEq_erls",RootEq_erls),
236 (*FIXXXME:del with rls.rls'*)
237 ("rooteq_srls",rooteq_srls)
240 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
241 val sqrt_isolate = prep_rls(
242 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
243 erls = RootEq_erls, srls = Erls, calc = [],
245 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
246 (* (sqrt a)^^^2 -> a *)
247 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
248 (* sqrt (a^^^2) -> a *)
249 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
250 (* sqrt a sqrt b -> sqrt(ab) *)
251 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
252 (* a sqrt b sqrt c -> a sqrt(bc) *)
253 Thm("sqrt_square_equation_both_1",
254 num_str @{thm sqrt_square_equation_both_1}),
255 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
256 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
257 Thm("sqrt_square_equation_both_2",
258 num_str @{thm sqrt_square_equation_both_2}),
259 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
260 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
261 Thm("sqrt_square_equation_both_3",
262 num_str @{thm sqrt_square_equation_both_3}),
263 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
264 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
265 Thm("sqrt_square_equation_both_4",
266 num_str @{thm sqrt_square_equation_both_4}),
267 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
268 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
269 Thm("sqrt_isolate_l_add1",
270 num_str @{thm sqrt_isolate_l_add1}),
271 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
272 Thm("sqrt_isolate_l_add2",
273 num_str @{thm sqrt_isolate_l_add2}),
274 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
275 Thm("sqrt_isolate_l_add3",
276 num_str @{thm sqrt_isolate_l_add3}),
277 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
278 Thm("sqrt_isolate_l_add4",
279 num_str @{thm sqrt_isolate_l_add4}),
280 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
281 Thm("sqrt_isolate_l_add5",
282 num_str @{thm sqrt_isolate_l_add5}),
283 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
284 Thm("sqrt_isolate_l_add6",
285 num_str @{thm sqrt_isolate_l_add6}),
286 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
287 (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
288 (* b*sqrt(x) = d sqrt(x) d/b *)
289 Thm("sqrt_isolate_r_add1",
290 num_str @{thm sqrt_isolate_r_add1}),
291 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
292 Thm("sqrt_isolate_r_add2",
293 num_str @{thm sqrt_isolate_r_add2}),
294 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
295 Thm("sqrt_isolate_r_add3",
296 num_str @{thm sqrt_isolate_r_add3}),
297 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
298 Thm("sqrt_isolate_r_add4",
299 num_str @{thm sqrt_isolate_r_add4}),
300 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
301 Thm("sqrt_isolate_r_add5",
302 num_str @{thm sqrt_isolate_r_add5}),
303 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
304 Thm("sqrt_isolate_r_add6",
305 num_str @{thm sqrt_isolate_r_add6}),
306 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
307 (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
308 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
309 Thm("sqrt_square_equation_left_1",
310 num_str @{thm sqrt_square_equation_left_1}),
311 (* sqrt(x)=b -> x=b^2 *)
312 Thm("sqrt_square_equation_left_2",
313 num_str @{thm sqrt_square_equation_left_2}),
314 (* c*sqrt(x)=b -> c^2*x=b^2 *)
315 Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),
316 (* c/sqrt(x)=b -> c^2/x=b^2 *)
317 Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),
318 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
319 Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),
320 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
321 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6}),
322 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
323 Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
324 (* a=sqrt(x) ->a^2=x *)
325 Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
326 (* a=c*sqrt(x) ->a^2=c^2*x *)
327 Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
328 (* a=c/sqrt(x) ->a^2=c^2/x *)
329 Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}),
330 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
331 Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
332 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
333 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
334 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
335 ],scr = Script ((term_of o the o (parse thy)) "empty_script")
338 ruleset' := overwritelthy @{theory} (!ruleset',
339 [("sqrt_isolate",sqrt_isolate)
341 (* -- left 28.08.02--*)
342 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
343 val l_sqrt_isolate = prep_rls(
344 Rls {id = "l_sqrt_isolate", preconds = [],
345 rew_ord = ("termlessI",termlessI),
346 erls = RootEq_erls, srls = Erls, calc = [],
348 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
349 (* (sqrt a)^^^2 -> a *)
350 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
351 (* sqrt (a^^^2) -> a *)
352 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
353 (* sqrt a sqrt b -> sqrt(ab) *)
354 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
355 (* a sqrt b sqrt c -> a sqrt(bc) *)
356 Thm("sqrt_isolate_l_add1",num_str @{thm sqrt_isolate_l_add1}),
357 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
358 Thm("sqrt_isolate_l_add2",num_str @{thm sqrt_isolate_l_add2}),
359 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
360 Thm("sqrt_isolate_l_add3",num_str @{thm sqrt_isolate_l_add3}),
361 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
362 Thm("sqrt_isolate_l_add4",num_str @{thm sqrt_isolate_l_add4}),
363 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
364 Thm("sqrt_isolate_l_add5",num_str @{thm sqrt_isolate_l_add5}),
365 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
366 Thm("sqrt_isolate_l_add6",num_str @{thm sqrt_isolate_l_add6}),
367 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
368 (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
369 (* b*sqrt(x) = d sqrt(x) d/b *)
370 Thm("sqrt_square_equation_left_1",num_str @{thm sqrt_square_equation_left_1}),
371 (* sqrt(x)=b -> x=b^2 *)
372 Thm("sqrt_square_equation_left_2",num_str @{thm sqrt_square_equation_left_2}),
373 (* a*sqrt(x)=b -> a^2*x=b^2*)
374 Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),
375 (* c/sqrt(x)=b -> c^2/x=b^2 *)
376 Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),
377 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
378 Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),
379 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
380 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})
381 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
383 scr = Script ((term_of o the o (parse thy)) "empty_script")
386 ruleset' := overwritelthy @{theory} (!ruleset',
387 [("l_sqrt_isolate",l_sqrt_isolate)
390 (* -- right 28.8.02--*)
391 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
392 val r_sqrt_isolate = prep_rls(
393 Rls {id = "r_sqrt_isolate", preconds = [],
394 rew_ord = ("termlessI",termlessI),
395 erls = RootEq_erls, srls = Erls, calc = [],
397 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
398 (* (sqrt a)^^^2 -> a *)
399 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
400 (* sqrt (a^^^2) -> a *)
401 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
402 (* sqrt a sqrt b -> sqrt(ab) *)
403 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
404 (* a sqrt b sqrt c -> a sqrt(bc) *)
405 Thm("sqrt_isolate_r_add1",num_str @{thm sqrt_isolate_r_add1}),
406 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
407 Thm("sqrt_isolate_r_add2",num_str @{thm sqrt_isolate_r_add2}),
408 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
409 Thm("sqrt_isolate_r_add3",num_str @{thm sqrt_isolate_r_add3}),
410 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
411 Thm("sqrt_isolate_r_add4",num_str @{thm sqrt_isolate_r_add4}),
412 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
413 Thm("sqrt_isolate_r_add5",num_str @{thm sqrt_isolate_r_add5}),
414 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
415 Thm("sqrt_isolate_r_add6",num_str @{thm sqrt_isolate_r_add6}),
416 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
417 (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
418 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
419 Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
420 (* a=sqrt(x) ->a^2=x *)
421 Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
422 (* a=c*sqrt(x) ->a^2=c^2*x *)
423 Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
424 (* a=c/sqrt(x) ->a^2=c^2/x *)
425 Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}),
426 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
427 Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
428 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
429 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
430 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
432 scr = Script ((term_of o the o (parse thy)) "empty_script")
435 ruleset' := overwritelthy @{theory} (!ruleset',
436 [("r_sqrt_isolate",r_sqrt_isolate)
439 val rooteq_simplify = prep_rls(
440 Rls {id = "rooteq_simplify",
441 preconds = [], rew_ord = ("termlessI",termlessI),
442 erls = RootEq_erls, srls = Erls, calc = [],
443 (*asm_thm = [("sqrt_square_1","")],*)
444 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
445 (* a+(b+c) = a+b+c *)
446 Thm ("real_assoc_2",num_str @{thm real_assoc_2}),
447 (* a*(b*c) = a*b*c *)
448 Calc ("op +",eval_binop "#add_"),
449 Calc ("op -",eval_binop "#sub_"),
450 Calc ("op *",eval_binop "#mult_"),
451 Calc ("HOL.divide", eval_cancel "#divide_e"),
452 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
453 Calc ("Atools.pow" ,eval_binop "#power_"),
454 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
455 Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}),
456 Thm("realpow_mul",num_str @{thm realpow_mul}),
457 (* (a * b)^n = a^n * b^n*)
458 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
459 (* sqrt b * sqrt c = sqrt(b*c) *)
460 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
461 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
462 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
463 (* sqrt (a^^^2) = a *)
464 Thm("sqrt_square_1",num_str @{thm sqrt_square_1})
465 (* sqrt a ^^^ 2 = a *)
467 scr = Script ((term_of o the o (parse thy)) "empty_script")
469 ruleset' := overwritelthy @{theory} (!ruleset',
470 [("rooteq_simplify",rooteq_simplify)
473 (*-------------------------Problem-----------------------*)
475 (get_pbt ["root'","univariate","equation"]);
478 (* ---------root----------- *)
480 (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
481 (["root'","univariate","equation"],
482 [("#Given" ,["equality e_e","solveFor v_v"]),
483 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
484 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
485 ("#Find" ,["solutions v'i'"])
487 RootEq_prls, SOME "solve (e_e::bool, v_v)",
489 (* ---------sqrt----------- *)
491 (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
492 (["sq","root'","univariate","equation"],
493 [("#Given" ,["equality e_e","solveFor v_v"]),
494 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
495 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
496 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
497 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
498 ("#Find" ,["solutions v'i'"])
500 RootEq_prls, SOME "solve (e_e::bool, v_v)",
501 [["RootEq","solve_sq_root_equation"]]));
502 (* ---------normalize----------- *)
504 (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
505 (["normalize","root'","univariate","equation"],
506 [("#Given" ,["equality e_e","solveFor v_v"]),
507 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
508 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
509 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
510 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
511 ("#Find" ,["solutions v'i'"])
513 RootEq_prls, SOME "solve (e_e::bool, v_v)",
514 [["RootEq","norm_sq_root_equation"]]));
516 (*-------------------------methods-----------------------*)
517 (* ---- root 20.8.02 ---*)
519 (prep_met thy "met_rooteq" [] e_metID
522 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
523 crls=RootEq_crls, nrls=norm_Poly(*,
524 asm_rls=[],asm_thm=[]*)}, "empty_script"));
526 (*-- normalize 20.10.02 --*)
528 (prep_met thy "met_rooteq_norm" [] e_metID
529 (["RootEq","norm_sq_root_equation"],
530 [("#Given" ,["equality e_e","solveFor v_v"]),
531 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
532 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
533 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
534 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
535 ("#Find" ,["solutions v'i'"])
537 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
538 calc=[], crls=RootEq_crls, nrls=norm_Poly},
539 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
540 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
541 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
542 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
543 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
544 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
545 " in ((SubProblem (RootEq',[univariate,equation], " ^
546 " [no_met]) [BOOL e_e, REAL v_v])))"
552 val -------------------------------------------------- = "00000";
554 (prep_met thy "met_rooteq_sq" [] e_metID
555 (["RootEq","solve_sq_root_equation"],
556 [("#Given" ,["equality e_e", "solveFor v_v"]),
557 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
558 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
559 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
560 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
561 ("#Find" ,["solutions v'i'"])
563 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
564 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
565 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
567 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
568 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
569 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
570 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
571 " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
572 " (L_L::bool list) = " ^
573 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
574 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
575 " [no_met]) [BOOL e_e, REAL v_v]) " ^
576 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
577 " [BOOL e_e, REAL v_v])) " ^
578 "in Check_elementwise L_LL {(v_v::real). Assumptions})"
583 (*-- right 28.08.02 --*)
585 (prep_met thy "met_rooteq_sq_right" [] e_metID
586 (["RootEq","solve_right_sq_root_equation"],
587 [("#Given" ,["equality e_e","solveFor v_v"]),
588 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
589 ("#Find" ,["solutions v'i'"])
591 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
592 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
593 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
595 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
596 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
597 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
598 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
599 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
600 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
601 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
602 " [no_met]) [BOOL e_e, REAL v_v]) " ^
603 " else ((SubProblem (RootEq',[univariate,equation], " ^
604 " [no_met]) [BOOL e_e, REAL v_v])))"
606 val --------------------------------------------------+++ = "33333";
608 (*-- left 28.08.02 --*)
610 (prep_met thy "met_rooteq_sq_left" [] e_metID
611 (["RootEq","solve_left_sq_root_equation"],
612 [("#Given" ,["equality e_e","solveFor v_v"]),
613 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
614 ("#Find" ,["solutions v'i'"])
616 {rew_ord'="termlessI",
621 crls=RootEq_crls, nrls=norm_Poly},
622 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
624 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
625 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
626 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
627 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
628 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
629 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
630 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
631 " [no_met]) [BOOL e_e, REAL v_v]) " ^
632 " else ((SubProblem (RootEq',[univariate,equation], " ^
633 " [no_met]) [BOOL e_e, REAL v_v])))"
635 val --------------------------------------------------++++ = "44444";
637 calclist':= overwritel (!calclist',
638 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
639 eval_is_rootTerm_in"")),
640 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
641 eval_is_sqrtTerm_in"")),
642 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
643 eval_is_normSqrtTerm_in""))
644 ]);(*("", ("", "")),*)