cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for Root Equations
10 theory RootEq imports Root Equation begin
12 text {* univariate equations containing real square roots:
13 This type of equations has been used to bootstrap Lucas-Interpretation.
14 In 2003 this type has been extended and integrated into ISAC's equation solver
15 by Richard Lang in 2003.
16 The assumptions (all containing "<") didn't pass the xml-parsers at the
17 interface between math-engine and front-end.
18 The migration Isabelle2002 --> 2011 dropped this type of equation, see
19 test/../rooteq.sml, rootrateq.sml.
24 is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
25 is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
26 is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
28 (*----------------------scripts-----------------------*)
29 Norm'_sq'_root'_equation
31 bool list] => bool list"
32 ("((Script Norm'_sq'_root'_equation (_ _ =))//
34 Solve'_sq'_root'_equation
36 bool list] => bool list"
37 ("((Script Solve'_sq'_root'_equation (_ _ =))//
39 Solve'_left'_sq'_root'_equation
41 bool list] => bool list"
42 ("((Script Solve'_left'_sq'_root'_equation (_ _ =))//
44 Solve'_right'_sq'_root'_equation
46 bool list] => bool list"
47 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
53 makex1_x: "a^^^1 = a" and
54 real_assoc_1: "a+(b+c) = a+b+c" and
55 real_assoc_2: "a*(b*c) = a*b*c" and
57 (* simplification of root*)
58 sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" and
59 sqrt_square_2: "sqrt (a ^^^ 2) = a" and
60 sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" and
61 sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" and
63 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
64 sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
65 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" and
66 sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
67 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" and
68 sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
69 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" and
70 sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
71 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" and
72 sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
73 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" and
74 sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
75 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" and
76 sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
77 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and
78 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
79 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and
80 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
81 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
82 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and
83 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
84 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" and
85 sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
86 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" and
87 sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
88 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" and
90 (* eliminate isolates sqrt *)
91 sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
92 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
93 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
94 sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
95 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
96 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
97 sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
98 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
99 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
100 sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
101 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
102 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
103 sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
104 ( (sqrt (a) = b) = (a = (b^^^2)))" and
105 sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
106 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and
107 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
108 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and
109 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
110 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
111 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" and
112 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
113 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" and
114 sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
115 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" and
116 sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
117 ( (a = sqrt (b)) = (a^^^2 = b))" and
118 sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
119 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and
120 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
121 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and
122 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
123 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
124 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" and
125 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
126 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" and
127 sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
128 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
133 (*-------------------------functions---------------------*)
134 (* true if bdv is under sqrt of a Equation*)
135 fun is_rootTerm_in t v =
137 fun coeff_in c v = member op = (vars c) v;
138 fun findroot (_ $ _ $ _ $ _) v = error("is_rootTerm_in:")
139 (* at the moment there is no term like this, but ....*)
140 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
141 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
142 | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v
143 | findroot (_ $ t2) v = (findroot t2 v)
144 | findroot _ _ = false;
149 fun is_sqrtTerm_in t v =
151 fun coeff_in c v = member op = (vars c) v;
152 fun findsqrt (_ $ _ $ _ $ _) v = error("is_sqrteqation_in:")
153 (* at the moment there is no term like this, but ....*)
154 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
155 | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v
156 | findsqrt (_ $ t1) v = (findsqrt t1 v)
157 | findsqrt _ _ = false;
162 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
163 and the subterm ist connected with + or * --> is normalized*)
164 fun is_normSqrtTerm_in t v =
166 fun coeff_in c v = member op = (vars c) v;
167 fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:")
168 (* at the moment there is no term like this, but ....*)
169 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
170 | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
171 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
172 | isnorm (Const ("Fields.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
173 (is_sqrtTerm_in t2 v)
174 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
175 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
176 | isnorm _ _ = false;
181 fun eval_is_rootTerm_in _ _
182 (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
183 if is_rootTerm_in t v then
184 SOME ((term2str p) ^ " = True",
185 Trueprop $ (mk_equality (p, @{term True})))
186 else SOME ((term2str p) ^ " = True",
187 Trueprop $ (mk_equality (p, @{term False})))
188 | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
190 fun eval_is_sqrtTerm_in _ _
191 (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
192 if is_sqrtTerm_in t v then
193 SOME ((term2str p) ^ " = True",
194 Trueprop $ (mk_equality (p, @{term True})))
195 else SOME ((term2str p) ^ " = True",
196 Trueprop $ (mk_equality (p, @{term False})))
197 | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
199 fun eval_is_normSqrtTerm_in _ _
200 (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
201 if is_normSqrtTerm_in t v then
202 SOME ((term2str p) ^ " = True",
203 Trueprop $ (mk_equality (p, @{term True})))
204 else SOME ((term2str p) ^ " = True",
205 Trueprop $ (mk_equality (p, @{term False})))
206 | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
208 (*-------------------------rulse-------------------------*)
209 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
210 append_rls "RootEq_prls" e_rls
211 [Calc ("Atools.ident",eval_ident "#ident_"),
212 Calc ("Tools.matches",eval_matches ""),
213 Calc ("Tools.lhs" ,eval_lhs ""),
214 Calc ("Tools.rhs" ,eval_rhs ""),
215 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
216 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
217 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
218 Calc ("HOL.eq",eval_equal "#equal_"),
219 Thm ("not_true",num_str @{thm not_true}),
220 Thm ("not_false",num_str @{thm not_false}),
221 Thm ("and_true",num_str @{thm and_true}),
222 Thm ("and_false",num_str @{thm and_false}),
223 Thm ("or_true",num_str @{thm or_true}),
224 Thm ("or_false",num_str @{thm or_false})
228 append_rls "RootEq_erls" Root_erls
229 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
233 append_rls "RootEq_crls" Root_crls
234 [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
238 append_rls "rooteq_srls" e_rls
239 [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
240 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
241 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
244 setup {* KEStore_Elems.add_rlss
245 [("RootEq_erls", (Context.theory_name @{theory}, RootEq_erls)),
246 ("rooteq_srls", (Context.theory_name @{theory}, rooteq_srls))] *}
249 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
250 val sqrt_isolate = prep_rls(
251 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
252 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
254 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
255 (* (sqrt a)^^^2 -> a *)
256 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
257 (* sqrt (a^^^2) -> a *)
258 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
259 (* sqrt a sqrt b -> sqrt(ab) *)
260 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
261 (* a sqrt b sqrt c -> a sqrt(bc) *)
262 Thm("sqrt_square_equation_both_1",
263 num_str @{thm sqrt_square_equation_both_1}),
264 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
265 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
266 Thm("sqrt_square_equation_both_2",
267 num_str @{thm sqrt_square_equation_both_2}),
268 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
269 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
270 Thm("sqrt_square_equation_both_3",
271 num_str @{thm sqrt_square_equation_both_3}),
272 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
273 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
274 Thm("sqrt_square_equation_both_4",
275 num_str @{thm sqrt_square_equation_both_4}),
276 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
277 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
278 Thm("sqrt_isolate_l_add1",
279 num_str @{thm sqrt_isolate_l_add1}),
280 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
281 Thm("sqrt_isolate_l_add2",
282 num_str @{thm sqrt_isolate_l_add2}),
283 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
284 Thm("sqrt_isolate_l_add3",
285 num_str @{thm sqrt_isolate_l_add3}),
286 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
287 Thm("sqrt_isolate_l_add4",
288 num_str @{thm sqrt_isolate_l_add4}),
289 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
290 Thm("sqrt_isolate_l_add5",
291 num_str @{thm sqrt_isolate_l_add5}),
292 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
293 Thm("sqrt_isolate_l_add6",
294 num_str @{thm sqrt_isolate_l_add6}),
295 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
296 (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
297 (* b*sqrt(x) = d sqrt(x) d/b *)
298 Thm("sqrt_isolate_r_add1",
299 num_str @{thm sqrt_isolate_r_add1}),
300 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
301 Thm("sqrt_isolate_r_add2",
302 num_str @{thm sqrt_isolate_r_add2}),
303 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
304 Thm("sqrt_isolate_r_add3",
305 num_str @{thm sqrt_isolate_r_add3}),
306 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
307 Thm("sqrt_isolate_r_add4",
308 num_str @{thm sqrt_isolate_r_add4}),
309 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
310 Thm("sqrt_isolate_r_add5",
311 num_str @{thm sqrt_isolate_r_add5}),
312 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
313 Thm("sqrt_isolate_r_add6",
314 num_str @{thm sqrt_isolate_r_add6}),
315 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
316 (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
317 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
318 Thm("sqrt_square_equation_left_1",
319 num_str @{thm sqrt_square_equation_left_1}),
320 (* sqrt(x)=b -> x=b^2 *)
321 Thm("sqrt_square_equation_left_2",
322 num_str @{thm sqrt_square_equation_left_2}),
323 (* c*sqrt(x)=b -> c^2*x=b^2 *)
324 Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),
325 (* c/sqrt(x)=b -> c^2/x=b^2 *)
326 Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),
327 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
328 Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),
329 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
330 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6}),
331 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
332 Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
333 (* a=sqrt(x) ->a^2=x *)
334 Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
335 (* a=c*sqrt(x) ->a^2=c^2*x *)
336 Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
337 (* a=c/sqrt(x) ->a^2=c^2/x *)
338 Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}),
339 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
340 Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
341 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
342 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
343 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
344 ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
347 setup {* KEStore_Elems.add_rlss
348 [("sqrt_isolate", (Context.theory_name @{theory}, sqrt_isolate))] *}
351 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
352 val l_sqrt_isolate = prep_rls(
353 Rls {id = "l_sqrt_isolate", preconds = [],
354 rew_ord = ("termlessI",termlessI),
355 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
357 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
358 (* (sqrt a)^^^2 -> a *)
359 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
360 (* sqrt (a^^^2) -> a *)
361 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
362 (* sqrt a sqrt b -> sqrt(ab) *)
363 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
364 (* a sqrt b sqrt c -> a sqrt(bc) *)
365 Thm("sqrt_isolate_l_add1",num_str @{thm sqrt_isolate_l_add1}),
366 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
367 Thm("sqrt_isolate_l_add2",num_str @{thm sqrt_isolate_l_add2}),
368 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
369 Thm("sqrt_isolate_l_add3",num_str @{thm sqrt_isolate_l_add3}),
370 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
371 Thm("sqrt_isolate_l_add4",num_str @{thm sqrt_isolate_l_add4}),
372 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
373 Thm("sqrt_isolate_l_add5",num_str @{thm sqrt_isolate_l_add5}),
374 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
375 Thm("sqrt_isolate_l_add6",num_str @{thm sqrt_isolate_l_add6}),
376 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
377 (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
378 (* b*sqrt(x) = d sqrt(x) d/b *)
379 Thm("sqrt_square_equation_left_1",num_str @{thm sqrt_square_equation_left_1}),
380 (* sqrt(x)=b -> x=b^2 *)
381 Thm("sqrt_square_equation_left_2",num_str @{thm sqrt_square_equation_left_2}),
382 (* a*sqrt(x)=b -> a^2*x=b^2*)
383 Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),
384 (* c/sqrt(x)=b -> c^2/x=b^2 *)
385 Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),
386 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
387 Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),
388 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
389 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})
390 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
392 scr = Prog ((term_of o the o (parse thy)) "empty_script")
395 setup {* KEStore_Elems.add_rlss
396 [("l_sqrt_isolate", (Context.theory_name @{theory}, l_sqrt_isolate))] *}
399 (* -- right 28.8.02--*)
400 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
401 val r_sqrt_isolate = prep_rls(
402 Rls {id = "r_sqrt_isolate", preconds = [],
403 rew_ord = ("termlessI",termlessI),
404 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
406 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
407 (* (sqrt a)^^^2 -> a *)
408 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
409 (* sqrt (a^^^2) -> a *)
410 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
411 (* sqrt a sqrt b -> sqrt(ab) *)
412 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
413 (* a sqrt b sqrt c -> a sqrt(bc) *)
414 Thm("sqrt_isolate_r_add1",num_str @{thm sqrt_isolate_r_add1}),
415 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
416 Thm("sqrt_isolate_r_add2",num_str @{thm sqrt_isolate_r_add2}),
417 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
418 Thm("sqrt_isolate_r_add3",num_str @{thm sqrt_isolate_r_add3}),
419 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
420 Thm("sqrt_isolate_r_add4",num_str @{thm sqrt_isolate_r_add4}),
421 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
422 Thm("sqrt_isolate_r_add5",num_str @{thm sqrt_isolate_r_add5}),
423 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
424 Thm("sqrt_isolate_r_add6",num_str @{thm sqrt_isolate_r_add6}),
425 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
426 (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
427 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
428 Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
429 (* a=sqrt(x) ->a^2=x *)
430 Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
431 (* a=c*sqrt(x) ->a^2=c^2*x *)
432 Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
433 (* a=c/sqrt(x) ->a^2=c^2/x *)
434 Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}),
435 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
436 Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
437 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
438 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
439 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
441 scr = Prog ((term_of o the o (parse thy)) "empty_script")
444 setup {* KEStore_Elems.add_rlss
445 [("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate))] *}
448 val rooteq_simplify = prep_rls(
449 Rls {id = "rooteq_simplify",
450 preconds = [], rew_ord = ("termlessI",termlessI),
451 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
452 (*asm_thm = [("sqrt_square_1","")],*)
453 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
454 (* a+(b+c) = a+b+c *)
455 Thm ("real_assoc_2",num_str @{thm real_assoc_2}),
456 (* a*(b*c) = a*b*c *)
457 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
458 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
459 Calc ("Groups.times_class.times",eval_binop "#mult_"),
460 Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
461 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
462 Calc ("Atools.pow" ,eval_binop "#power_"),
463 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
464 Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}),
465 Thm("realpow_mul",num_str @{thm realpow_mul}),
466 (* (a * b)^n = a^n * b^n*)
467 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
468 (* sqrt b * sqrt c = sqrt(b*c) *)
469 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
470 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
471 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
472 (* sqrt (a^^^2) = a *)
473 Thm("sqrt_square_1",num_str @{thm sqrt_square_1})
474 (* sqrt a ^^^ 2 = a *)
476 scr = Prog ((term_of o the o (parse thy)) "empty_script")
479 setup {* KEStore_Elems.add_rlss
480 [("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))] *}
483 (*-------------------------Problem-----------------------*)
485 (get_pbt ["root'","univariate","equation"]);
488 (* ---------root----------- *)
490 (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
491 (["root'","univariate","equation"],
492 [("#Given" ,["equality e_e","solveFor v_v"]),
493 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
494 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
495 ("#Find" ,["solutions v_v'i'"])
497 RootEq_prls, SOME "solve (e_e::bool, v_v)",
499 (* ---------sqrt----------- *)
501 (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
502 (["sq","root'","univariate","equation"],
503 [("#Given" ,["equality e_e","solveFor v_v"]),
504 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
505 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
506 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
507 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
508 ("#Find" ,["solutions v_v'i'"])
510 RootEq_prls, SOME "solve (e_e::bool, v_v)",
511 [["RootEq","solve_sq_root_equation"]]));
512 (* ---------normalize----------- *)
514 (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
515 (["normalize","root'","univariate","equation"],
516 [("#Given" ,["equality e_e","solveFor v_v"]),
517 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
518 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
519 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
520 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
521 ("#Find" ,["solutions v_v'i'"])
523 RootEq_prls, SOME "solve (e_e::bool, v_v)",
524 [["RootEq","norm_sq_root_equation"]]));
526 setup {* KEStore_Elems.add_pbts
527 [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
528 (["root'","univariate","equation"],
529 [("#Given" ,["equality e_e","solveFor v_v"]),
530 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
531 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
532 ("#Find" ,["solutions v_v'i'"])],
533 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
534 (* ---------sqrt----------- *)
535 (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
536 (["sq","root'","univariate","equation"],
537 [("#Given" ,["equality e_e","solveFor v_v"]),
538 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
539 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
540 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
541 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
542 ("#Find" ,["solutions v_v'i'"])],
543 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),
544 (* ---------normalize----------- *)
545 (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
546 (["normalize","root'","univariate","equation"],
547 [("#Given" ,["equality e_e","solveFor v_v"]),
548 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
549 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
550 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
551 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
552 ("#Find" ,["solutions v_v'i'"])],
553 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]]))] *}
556 (*-------------------------methods-----------------------*)
557 (* ---- root 20.8.02 ---*)
559 (prep_met thy "met_rooteq" [] e_metID
562 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
563 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
565 (*-- normalize 20.10.02 --*)
567 (prep_met thy "met_rooteq_norm" [] e_metID
568 (["RootEq","norm_sq_root_equation"],
569 [("#Given" ,["equality e_e","solveFor v_v"]),
570 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
571 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
572 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
573 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
574 ("#Find" ,["solutions v_v'i'"])
576 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
577 calc=[], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
578 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
579 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
580 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
581 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
582 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
583 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
584 " in ((SubProblem (RootEq',[univariate,equation], " ^
585 " [no_met]) [BOOL e_e, REAL v_v])))"
591 val -------------------------------------------------- = "00000";
593 (prep_met thy "met_rooteq_sq" [] e_metID
594 (["RootEq","solve_sq_root_equation"],
595 [("#Given" ,["equality e_e", "solveFor v_v"]),
596 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
597 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
598 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
599 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
600 ("#Find" ,["solutions v_v'i'"])
602 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
603 prls = RootEq_prls, calc = [], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
604 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
606 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
607 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
608 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
609 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
610 " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
611 " (L_L::bool list) = " ^
612 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
613 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
614 " [no_met]) [BOOL e_e, REAL v_v]) " ^
615 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
616 " [BOOL e_e, REAL v_v])) " ^
617 "in Check_elementwise L_L {(v_v::real). Assumptions})"
622 (*-- right 28.08.02 --*)
624 (prep_met thy "met_rooteq_sq_right" [] e_metID
625 (["RootEq","solve_right_sq_root_equation"],
626 [("#Given" ,["equality e_e","solveFor v_v"]),
627 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
628 ("#Find" ,["solutions v_v'i'"])
630 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
631 prls = RootEq_prls, calc = [], crls = RootEq_crls, errpats = [], nrls = norm_Poly},
632 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
634 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
635 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
636 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
637 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
638 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
639 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
640 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
641 " [no_met]) [BOOL e_e, REAL v_v]) " ^
642 " else ((SubProblem (RootEq',[univariate,equation], " ^
643 " [no_met]) [BOOL e_e, REAL v_v])))"
645 val --------------------------------------------------+++ = "33333";
647 (*-- left 28.08.02 --*)
649 (prep_met thy "met_rooteq_sq_left" [] e_metID
650 (["RootEq","solve_left_sq_root_equation"],
651 [("#Given" ,["equality e_e","solveFor v_v"]),
652 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
653 ("#Find" ,["solutions v_v'i'"])
655 {rew_ord'="termlessI",
660 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
661 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
663 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
664 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
665 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
666 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
667 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
668 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
669 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
670 " [no_met]) [BOOL e_e, REAL v_v]) " ^
671 " else ((SubProblem (RootEq',[univariate,equation], " ^
672 " [no_met]) [BOOL e_e, REAL v_v])))"
674 val --------------------------------------------------++++ = "44444";
676 setup {* KEStore_Elems.add_calcs
677 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),
678 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in"")),
679 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))] *}