1 (*.(c) by Richard Lang, 2003 .*)
2 (* theory collecting all knowledge for RootEquations
10 (* use"Knowledge/RootEq.ML";
17 use_thy"Knowledge/Isac";
19 "******* RootEq.ML begin *******";
21 theory' := overwritel (!theory', [("RootEq.thy",RootEq.thy)]);
22 (*-------------------------functions---------------------*)
23 (* true if bdv is under sqrt of a Equation*)
24 fun is_rootTerm_in t v =
26 fun coeff_in c v = member op = (vars c) v;
27 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
28 (* at the moment there is no term like this, but ....*)
29 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
30 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
31 | findroot (t as (Const ("Root.sqrt",_) $ t2)) v = coeff_in t2 v
32 | findroot (_ $ t2) v = (findroot t2 v)
33 | findroot _ _ = false;
38 fun is_sqrtTerm_in t v =
40 fun coeff_in c v = member op = (vars c) v;
41 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
42 (* at the moment there is no term like this, but ....*)
43 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
44 | findsqrt (t as (Const ("Root.sqrt",_) $ a)) v = coeff_in a v
45 | findsqrt (_ $ t1) v = (findsqrt t1 v)
46 | findsqrt _ _ = false;
51 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
52 and the subterm ist connected with + or * --> is normalized*)
53 fun is_normSqrtTerm_in t v =
55 fun coeff_in c v = member op = (vars c) v;
56 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
57 (* at the moment there is no term like this, but ....*)
58 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
59 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
60 | isnorm (Const ("op -",_) $ _ $ _) v = false
61 | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
63 | isnorm (Const ("Root.sqrt",_) $ t1) v = coeff_in t1 v
64 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
70 fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
71 if is_rootTerm_in t v then
72 SOME ((term2str p) ^ " = True",
73 Trueprop $ (mk_equality (p, HOLogic.true_const)))
74 else SOME ((term2str p) ^ " = True",
75 Trueprop $ (mk_equality (p, HOLogic.false_const)))
76 | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
78 fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
79 if is_sqrtTerm_in t v then
80 SOME ((term2str p) ^ " = True",
81 Trueprop $ (mk_equality (p, HOLogic.true_const)))
82 else SOME ((term2str p) ^ " = True",
83 Trueprop $ (mk_equality (p, HOLogic.false_const)))
84 | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
86 fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
87 if is_normSqrtTerm_in t v then
88 SOME ((term2str p) ^ " = True",
89 Trueprop $ (mk_equality (p, HOLogic.true_const)))
90 else SOME ((term2str p) ^ " = True",
91 Trueprop $ (mk_equality (p, HOLogic.false_const)))
92 | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
94 (*-------------------------rulse-------------------------*)
95 val RootEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
96 append_rls "RootEq_prls" e_rls
97 [Calc ("Atools.ident",eval_ident "#ident_"),
98 Calc ("Tools.matches",eval_matches ""),
99 Calc ("Tools.lhs" ,eval_lhs ""),
100 Calc ("Tools.rhs" ,eval_rhs ""),
101 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
102 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
103 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
104 Calc ("op =",eval_equal "#equal_"),
105 Thm ("not_true",num_str not_true),
106 Thm ("not_false",num_str not_false),
107 Thm ("and_true",num_str and_true),
108 Thm ("and_false",num_str and_false),
109 Thm ("or_true",num_str or_true),
110 Thm ("or_false",num_str or_false)
114 append_rls "RootEq_erls" Root_erls
115 [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
119 append_rls "RootEq_crls" Root_crls
120 [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
124 append_rls "rooteq_srls" e_rls
125 [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
126 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
127 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
130 ruleset' := overwritelthy thy (!ruleset',
131 [("RootEq_erls",RootEq_erls), (*FIXXXME:del with rls.rls'*)
132 ("rooteq_srls",rooteq_srls)
135 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
136 val sqrt_isolate = prep_rls(
137 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
138 erls = RootEq_erls, srls = Erls, calc = [],
139 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
140 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
141 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
142 ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),
143 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
144 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
145 ("sqrt_square_equation_right_6","")],*)
147 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
148 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
149 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
150 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
151 Thm("sqrt_square_equation_both_1",num_str sqrt_square_equation_both_1),
152 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
153 Thm("sqrt_square_equation_both_2",num_str sqrt_square_equation_both_2),
154 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
155 Thm("sqrt_square_equation_both_3",num_str sqrt_square_equation_both_3),
156 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
157 Thm("sqrt_square_equation_both_4",num_str sqrt_square_equation_both_4),
158 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
159 Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
160 Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
161 Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
162 Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
163 Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5), (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
164 Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
165 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *)
166 Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
167 Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
168 Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
169 Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
170 Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5), (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
171 Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
172 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *)
173 Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
174 (* sqrt(x)=b -> x=b^2 *)
175 Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
176 (* c*sqrt(x)=b -> c^2*x=b^2 *)
177 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
178 (* c/sqrt(x)=b -> c^2/x=b^2 *)
179 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
180 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
181 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
182 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
183 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6),
184 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
185 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
186 (* a=sqrt(x) ->a^2=x *)
187 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
188 (* a=c*sqrt(x) ->a^2=c^2*x *)
189 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
190 (* a=c/sqrt(x) ->a^2=c^2/x *)
191 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
192 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
193 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
194 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
195 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
196 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
198 scr = Script ((term_of o the o (parse thy)) "empty_script")
200 ruleset' := overwritelthy thy (!ruleset',
201 [("sqrt_isolate",sqrt_isolate)
203 (* -- left 28.08.02--*)
204 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
205 val l_sqrt_isolate = prep_rls(
206 Rls {id = "l_sqrt_isolate", preconds = [],
207 rew_ord = ("termlessI",termlessI),
208 erls = RootEq_erls, srls = Erls, calc = [],
209 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
210 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
211 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
212 ("sqrt_square_equation_left_6","")],*)
214 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
215 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
216 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
217 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
218 Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
219 Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
220 Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
221 Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
222 Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5), (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
223 Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
224 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *)
225 Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
226 (* sqrt(x)=b -> x=b^2 *)
227 Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
228 (* a*sqrt(x)=b -> a^2*x=b^2*)
229 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
230 (* c/sqrt(x)=b -> c^2/x=b^2 *)
231 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
232 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
233 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
234 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
235 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6)
236 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
238 scr = Script ((term_of o the o (parse thy)) "empty_script")
240 ruleset' := overwritelthy thy (!ruleset',
241 [("l_sqrt_isolate",l_sqrt_isolate)
244 (* -- right 28.8.02--*)
245 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
246 val r_sqrt_isolate = prep_rls(
247 Rls {id = "r_sqrt_isolate", preconds = [],
248 rew_ord = ("termlessI",termlessI),
249 erls = RootEq_erls, srls = Erls, calc = [],
250 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_right_1",""),
251 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
252 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
253 ("sqrt_square_equation_right_6","")],*)
255 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
256 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
257 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
258 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
259 Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
260 Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
261 Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
262 Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
263 Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5), (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
264 Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
265 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *)
266 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
267 (* a=sqrt(x) ->a^2=x *)
268 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
269 (* a=c*sqrt(x) ->a^2=c^2*x *)
270 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
271 (* a=c/sqrt(x) ->a^2=c^2/x *)
272 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
273 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
274 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
275 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
276 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
277 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
279 scr = Script ((term_of o the o (parse thy)) "empty_script")
281 ruleset' := overwritelthy thy (!ruleset',
282 [("r_sqrt_isolate",r_sqrt_isolate)
285 val rooteq_simplify = prep_rls(
286 Rls {id = "rooteq_simplify",
287 preconds = [], rew_ord = ("termlessI",termlessI),
288 erls = RootEq_erls, srls = Erls, calc = [],
289 (*asm_thm = [("sqrt_square_1","")],*)
290 rules = [Thm ("real_assoc_1",num_str real_assoc_1), (* a+(b+c) = a+b+c *)
291 Thm ("real_assoc_2",num_str real_assoc_2), (* a*(b*c) = a*b*c *)
292 Calc ("op +",eval_binop "#add_"),
293 Calc ("op -",eval_binop "#sub_"),
294 Calc ("op *",eval_binop "#mult_"),
295 Calc ("HOL.divide", eval_cancel "#divide_"),
296 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
297 Calc ("Atools.pow" ,eval_binop "#power_"),
298 Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2),
299 Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2),
300 Thm("realpow_mul",num_str realpow_mul), (* (a * b)^n = a^n * b^n*)
301 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt b * sqrt c = sqrt(b*c) *)
302 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
303 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) = a *)
304 Thm("sqrt_square_1",num_str sqrt_square_1) (* sqrt a ^^^ 2 = a *)
306 scr = Script ((term_of o the o (parse thy)) "empty_script")
308 ruleset' := overwritelthy thy (!ruleset',
309 [("rooteq_simplify",rooteq_simplify)
312 (*-------------------------Problem-----------------------*)
314 (get_pbt ["root","univariate","equation"]);
317 (* ---------root----------- *)
319 (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID
320 (["root","univariate","equation"],
321 [("#Given" ,["equality e_","solveFor v_"]),
322 ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | \
323 \(rhs e_) is_rootTerm_in (v_::real)"]),
324 ("#Find" ,["solutions v_i_"])
326 RootEq_prls, SOME "solve (e_::bool, v_)",
328 (* ---------sqrt----------- *)
330 (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID
331 (["sq","root","univariate","equation"],
332 [("#Given" ,["equality e_","solveFor v_"]),
333 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
334 \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\
335 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
336 \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
337 ("#Find" ,["solutions v_i_"])
339 RootEq_prls, SOME "solve (e_::bool, v_)",
340 [["RootEq","solve_sq_root_equation"]]));
341 (* ---------normalize----------- *)
343 (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID
344 (["normalize","root","univariate","equation"],
345 [("#Given" ,["equality e_","solveFor v_"]),
346 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
347 \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \
348 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
349 \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
350 ("#Find" ,["solutions v_i_"])
352 RootEq_prls, SOME "solve (e_::bool, v_)",
353 [["RootEq","norm_sq_root_equation"]]));
355 (*-------------------------methods-----------------------*)
356 (* ---- root 20.8.02 ---*)
358 (prep_met RootEq.thy "met_rooteq" [] e_metID
361 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
362 crls=RootEq_crls, nrls=norm_Poly(*,
363 asm_rls=[],asm_thm=[]*)}, "empty_script"));
364 (*-- normalize 20.10.02 --*)
366 (prep_met RootEq.thy "met_rooteq_norm" [] e_metID
367 (["RootEq","norm_sq_root_equation"],
368 [("#Given" ,["equality e_","solveFor v_"]),
369 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
370 \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \
371 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
372 \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
373 ("#Find" ,["solutions v_i_"])
375 {rew_ord'="termlessI",
380 crls=RootEq_crls, nrls=norm_Poly(*,
382 asm_thm=[("sqrt_square_1","")]*)},
383 "Script Norm_sq_root_equation (e_::bool) (v_::real) = \
384 \(let e_ = ((Repeat(Try (Rewrite makex1_x False))) @@ \
385 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
386 \ (Try (Rewrite_Set rooteq_simplify True)) @@ \
387 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
388 \ (Try (Rewrite_Set rooteq_simplify True))) e_ \
389 \ in ((SubProblem (RootEq_,[univariate,equation], \
390 \ [no_met]) [bool_ e_, real_ v_])))"
394 (prep_met RootEq.thy "met_rooteq_sq" [] e_metID
395 (["RootEq","solve_sq_root_equation"],
396 [("#Given" ,["equality e_","solveFor v_"]),
397 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
398 \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\
399 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
400 \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
401 ("#Find" ,["solutions v_i_"])
403 {rew_ord'="termlessI",
408 crls=RootEq_crls, nrls=norm_Poly(*,
410 asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
411 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
412 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
413 ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),
414 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
415 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
416 ("sqrt_square_equation_right_6","")]*)},
417 "Script Solve_sq_root_equation (e_::bool) (v_::real) = \
419 \ ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ \
420 \ (Try (Rewrite_Set rooteq_simplify True)) @@ \
421 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
422 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
423 \ (Try (Rewrite_Set rooteq_simplify True))) e_;\
424 \ (L_::bool list) = \
425 \ (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))\
426 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
427 \ [no_met]) [bool_ e_, real_ v_]) \
428 \ else (SubProblem (RootEq_,[univariate,equation], \
429 \ [no_met]) [bool_ e_, real_ v_])) \
430 \ in Check_elementwise L_ {(v_::real). Assumptions})"
433 (*-- right 28.08.02 --*)
435 (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID
436 (["RootEq","solve_right_sq_root_equation"],
437 [("#Given" ,["equality e_","solveFor v_"]),
438 ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
439 ("#Find" ,["solutions v_i_"])
441 {rew_ord'="termlessI",
446 crls=RootEq_crls, nrls=norm_Poly(*,
448 asm_thm=[("sqrt_square_1",""),("sqrt_square_1",""),("sqrt_square_equation_right_1",""),
449 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
450 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
451 ("sqrt_square_equation_right_6","")]*)},
452 "Script Solve_right_sq_root_equation (e_::bool) (v_::real) = \
453 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ \
454 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
455 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
456 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
457 \ (Try (Rewrite_Set rooteq_simplify False))) e_\
458 \ in if ((rhs e_) is_sqrtTerm_in v_) \
459 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
460 \ [no_met]) [bool_ e_, real_ v_]) \
461 \ else ((SubProblem (RootEq_,[univariate,equation], \
462 \ [no_met]) [bool_ e_, real_ v_])))"
465 (*-- left 28.08.02 --*)
467 (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID
468 (["RootEq","solve_left_sq_root_equation"],
469 [("#Given" ,["equality e_","solveFor v_"]),
470 ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
471 ("#Find" ,["solutions v_i_"])
473 {rew_ord'="termlessI",
478 crls=RootEq_crls, nrls=norm_Poly(*,
480 asm_thm=[("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
481 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
482 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
483 ("sqrt_square_equation_left_6","")]*)},
484 "Script Solve_left_sq_root_equation (e_::bool) (v_::real) = \
485 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ \
486 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
487 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
488 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
489 \ (Try (Rewrite_Set rooteq_simplify False))) e_\
490 \ in if ((lhs e_) is_sqrtTerm_in v_) \
491 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
492 \ [no_met]) [bool_ e_, real_ v_]) \
493 \ else ((SubProblem (RootEq_,[univariate,equation], \
494 \ [no_met]) [bool_ e_, real_ v_])))"
497 calclist':= overwritel (!calclist',
498 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
499 eval_is_rootTerm_in"")),
500 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
501 eval_is_sqrtTerm_in"")),
502 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
503 eval_is_normSqrtTerm_in""))
504 ]);(*("", ("", "")),*)
505 "******* RootEq.ML end *******";