1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for Root Equations
10 theory RootEq imports Root Equation begin
12 text \<open>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.
22 subsection \<open>consts definition for predicates\<close>
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 subsection \<open>theorems not yet adopted from Isabelle\<close>
31 makex1_x: "a \<up> 1 = a" and
32 real_assoc_1: "a+(b+c) = a+b+c" and
33 real_assoc_2: "a*(b*c) = a*b*c" and
35 (* simplification of root*)
36 sqrt_square_1: "[|0 <= a|] ==> (sqrt a) \<up> 2 = a" and
37 sqrt_square_2: "sqrt (a \<up> 2) = a" and
38 sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" and
39 sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" and
41 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
42 sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
43 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" and
44 sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
45 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" and
46 sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
47 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" and
48 sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
49 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" and
50 sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
51 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" and
52 sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
53 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" and
54 sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
55 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and
56 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
57 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and
58 (* small hack: thm 3,5,6 are not needed if rootnormalise is well done*)
59 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
60 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and
61 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
62 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" and
63 sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
64 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" and
65 sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
66 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" and
68 (* eliminate isolates sqrt *)
69 sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
70 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
71 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
72 sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
73 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
74 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
75 sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
76 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
77 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
78 sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
79 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
80 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
81 sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
82 ( (sqrt (a) = b) = (a = (b \<up> 2)))" and
83 sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
84 ( (c*sqrt(a) = b) = (c \<up> 2*a = b \<up> 2))" and
85 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
86 ( c/sqrt(a) = b) = (c \<up> 2 / a = b \<up> 2)" and
87 (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
88 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
89 ( (c*(d/sqrt (a)) = b) = (c \<up> 2*(d \<up> 2/a) = b \<up> 2))" and
90 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
91 ( c/(d*sqrt(a)) = b) = (c \<up> 2 / (d \<up> 2*a) = b \<up> 2)" and
92 sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
93 ( (c*(d/(e*sqrt (a))) = b) = (c \<up> 2*(d \<up> 2/(e \<up> 2*a)) = b \<up> 2))" and
94 sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
95 ( (a = sqrt (b)) = (a \<up> 2 = b))" and
96 sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
97 ( (a = c*sqrt (b)) = ((a \<up> 2) = c \<up> 2*b))" and
98 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
99 ( (a = c/sqrt (b)) = (a \<up> 2 = c \<up> 2/b))" and
100 (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
101 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
102 ( (a = c*(d/sqrt (b))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/b)))" and
103 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
104 ( (a = c/(d*sqrt (b))) = (a \<up> 2 = c \<up> 2/(d \<up> 2*b)))" and
105 sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
106 ( (a = c*(d/(e*sqrt (b)))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/(e \<up> 2*b))))"
108 subsection \<open>predicates\<close>
110 (* true if bdv is under sqrt of a Equation*)
111 fun is_rootTerm_in t v =
113 fun findroot (t as (_ $ _ $ _ $ _)) _ = raise TERM ( "is_rootTerm_in", [t])
114 (* at the moment there is no term like this, but ....*)
115 | findroot (Const (\<^const_name>\<open>nroot\<close>, _) $ _ $ t3) v = Prog_Expr.occurs_in v t3
116 | findroot (_ $ t2 $ t3) v = findroot t2 v orelse findroot t3 v
117 | findroot (Const (\<^const_name>\<open>sqrt\<close>, _) $ t2) v = Prog_Expr.occurs_in v t2
118 | findroot (_ $ t2) v = findroot t2 v
119 | findroot _ _ = false;
124 fun is_sqrtTerm_in t v =
126 fun findsqrt (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_sqrteqation_in", [t])
127 (* at the moment there is no term like this, but ....*)
128 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
129 | findsqrt (Const (\<^const_name>\<open>sqrt\<close>, _) $ a) v = Prog_Expr.occurs_in v a
130 | findsqrt (_ $ t1) v = findsqrt t1 v
131 | findsqrt _ _ = false;
136 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
137 and the subterm ist connected with + or * --> is normalised*)
138 fun is_normSqrtTerm_in t v =
140 fun isnorm (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_normSqrtTerm_in", [t])
141 (* at the moment there is no term like this, but ....*)
142 | isnorm (Const (\<^const_name>\<open>plus\<close>,_) $ _ $ t2) v = is_sqrtTerm_in t2 v
143 | isnorm (Const (\<^const_name>\<open>times\<close>,_) $ _ $ t2) v = is_sqrtTerm_in t2 v
144 | isnorm (Const (\<^const_name>\<open>minus\<close>,_) $ _ $ _) _ = false
145 | isnorm (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) v =
146 is_sqrtTerm_in t1 v orelse is_sqrtTerm_in t2 v
147 | isnorm (Const (\<^const_name>\<open>sqrt\<close>, _) $ t1) v = Prog_Expr.occurs_in v t1
148 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
149 | isnorm _ _ = false;
154 fun eval_is_rootTerm_in _ _ (p as (Const (\<^const_name>\<open>RootEq.is_rootTerm_in\<close>,_) $ t $ v)) _ =
155 if is_rootTerm_in t v
156 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
157 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
158 | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
160 fun eval_is_sqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_sqrtTerm_in\<close>,_) $ t $ v)) _ =
161 if is_sqrtTerm_in t v
162 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
163 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
164 | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
166 fun eval_is_normSqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_normSqrtTerm_in\<close>,_) $ t $ v)) _ =
167 if is_normSqrtTerm_in t v
168 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
169 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
170 | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
172 calculation is_rootTerm_in = \<open>eval_is_rootTerm_in ""\<close>
173 calculation is_sqrtTerm_in = \<open>eval_is_sqrtTerm_in ""\<close>
174 calculation is_normSqrtTerm_in = \<open>eval_is_normSqrtTerm_in ""\<close>
176 subsection \<open>rule-sets\<close>
178 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
179 Rule_Set.append_rules "RootEq_prls" Rule_Set.empty
180 [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
181 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
182 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
183 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
184 \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
185 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
186 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
187 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
188 \<^rule_thm>\<open>not_true\<close>,
189 \<^rule_thm>\<open>not_false\<close>,
190 \<^rule_thm>\<open>and_true\<close>,
191 \<^rule_thm>\<open>and_false\<close>,
192 \<^rule_thm>\<open>or_true\<close>,
193 \<^rule_thm>\<open>or_false\<close>
197 Rule_Set.append_rules "RootEq_erls" Root_erls
198 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
201 Rule_Set.append_rules "RootEq_crls" Root_crls
202 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
205 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
206 [\<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
207 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),
208 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];
212 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
213 val sqrt_isolate = prep_rls'(
214 Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
215 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
217 \<^rule_thm>\<open>sqrt_square_1\<close>,
218 (* (sqrt a) \<up> 2 -> a *)
219 \<^rule_thm>\<open>sqrt_square_2\<close>,
220 (* sqrt (a \<up> 2) -> a *)
221 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
222 (* sqrt a sqrt b -> sqrt(ab) *)
223 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
224 (* a sqrt b sqrt c -> a sqrt(bc) *)
225 \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
226 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
227 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
228 \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
229 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
230 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
231 \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
232 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
233 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
234 \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
235 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
236 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
237 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
238 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
239 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
240 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
241 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
242 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
243 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
244 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
245 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
246 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
247 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
248 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
249 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
250 (* b*sqrt(x) = d sqrt(x) d/b *)
251 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
252 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
253 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
254 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
255 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
256 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
257 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
258 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
259 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
260 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
261 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
262 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
263 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
264 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
265 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
266 (* sqrt(x)=b -> x=b^2 *)
267 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
268 (* c*sqrt(x)=b -> c^2*x=b^2 *)
269 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
270 (* c/sqrt(x)=b -> c^2/x=b^2 *)
271 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
272 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
273 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
274 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
275 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>,
276 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
277 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
278 (* a=sqrt(x) ->a^2=x *)
279 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
280 (* a=c*sqrt(x) ->a^2=c^2*x *)
281 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
282 (* a=c/sqrt(x) ->a^2=c^2/x *)
283 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
284 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
285 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
286 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
287 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
288 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
289 ],scr = Rule.Empty_Prog
293 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
294 val l_sqrt_isolate = prep_rls'(
295 Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
296 rew_ord = ("termlessI",termlessI),
297 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
299 \<^rule_thm>\<open>sqrt_square_1\<close>,
300 (* (sqrt a) \<up> 2 -> a *)
301 \<^rule_thm>\<open>sqrt_square_2\<close>,
302 (* sqrt (a \<up> 2) -> a *)
303 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
304 (* sqrt a sqrt b -> sqrt(ab) *)
305 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
306 (* a sqrt b sqrt c -> a sqrt(bc) *)
307 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
308 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
309 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
310 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
311 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
312 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
313 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
314 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
315 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
316 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
317 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
318 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
319 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
320 (* b*sqrt(x) = d sqrt(x) d/b *)
321 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
322 (* sqrt(x)=b -> x=b^2 *)
323 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
324 (* a*sqrt(x)=b -> a^2*x=b^2*)
325 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
326 (* c/sqrt(x)=b -> c^2/x=b^2 *)
327 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
328 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
329 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
330 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
331 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>
332 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
334 scr = Rule.Empty_Prog
338 (* -- right 28.8.02--*)
339 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
340 val r_sqrt_isolate = prep_rls'(
341 Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
342 rew_ord = ("termlessI",termlessI),
343 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
345 \<^rule_thm>\<open>sqrt_square_1\<close>,
346 (* (sqrt a) \<up> 2 -> a *)
347 \<^rule_thm>\<open>sqrt_square_2\<close>,
348 (* sqrt (a \<up> 2) -> a *)
349 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
350 (* sqrt a sqrt b -> sqrt(ab) *)
351 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
352 (* a sqrt b sqrt c -> a sqrt(bc) *)
353 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
354 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
355 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
356 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
357 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
358 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
359 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
360 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
361 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
362 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
363 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
364 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
365 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
366 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
367 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
368 (* a=sqrt(x) ->a^2=x *)
369 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
370 (* a=c*sqrt(x) ->a^2=c^2*x *)
371 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
372 (* a=c/sqrt(x) ->a^2=c^2/x *)
373 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
374 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
375 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
376 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
377 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
378 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
380 scr = Rule.Empty_Prog
384 val rooteq_simplify = prep_rls'(
385 Rule_Def.Repeat {id = "rooteq_simplify",
386 preconds = [], rew_ord = ("termlessI",termlessI),
387 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
388 (*asm_thm = [("sqrt_square_1", "")],*)
389 rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
390 (* a+(b+c) = a+b+c *)
391 \<^rule_thm>\<open>real_assoc_2\<close>,
392 (* a*(b*c) = a*b*c *)
393 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
394 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
395 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
396 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
397 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
398 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
399 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
400 \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
401 \<^rule_thm>\<open>realpow_mul\<close>,
402 (* (a * b)^n = a^n * b^n*)
403 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
404 (* sqrt b * sqrt c = sqrt(b*c) *)
405 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
406 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
407 \<^rule_thm>\<open>sqrt_square_2\<close>,
408 (* sqrt (a \<up> 2) = a *)
409 \<^rule_thm>\<open>sqrt_square_1\<close>
410 (* sqrt a \<up> 2 = a *)
412 scr = Rule.Empty_Prog
416 RootEq_erls = RootEq_erls and
417 rooteq_srls = rooteq_srls and
418 sqrt_isolate = sqrt_isolate and
419 l_sqrt_isolate = l_sqrt_isolate and
420 r_sqrt_isolate = r_sqrt_isolate and
421 rooteq_simplify = rooteq_simplify
423 subsection \<open>problems\<close>
425 problem pbl_equ_univ_root : "rootX/univariate/equation" =
426 \<open>RootEq_prls\<close>
427 CAS: "solve (e_e::bool, v_v)"
428 Given: "equality e_e" "solveFor v_v"
430 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
431 "(lhs e_e) is_rootTerm_in (v_v::real) |
432 (rhs e_e) is_rootTerm_in (v_v::real)"
433 Find: "solutions v_v'i'"
435 problem pbl_equ_univ_root_sq : "sq/rootX/univariate/equation" =
436 \<open>RootEq_prls\<close>
437 Method: "RootEq/solve_sq_root_equation"
438 CAS: "solve (e_e::bool, v_v)"
439 Given: "equality e_e" "solveFor v_v"
441 "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
442 ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |
443 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
444 ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"
445 Find: "solutions v_v'i'"
447 (* ---------normalise----------- *)
448 problem pbl_equ_univ_root_norm : "normalise/rootX/univariate/equation" =
449 \<open>RootEq_prls\<close>
450 Method: "RootEq/norm_sq_root_equation"
451 CAS: "solve (e_e::bool, v_v)"
452 Given: "equality e_e" "solveFor v_v"
454 "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
455 Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
456 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
457 Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
458 Find: "solutions v_v'i'"
460 subsection \<open>methods\<close>
462 method met_rooteq : "RootEq" =
463 \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
464 crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
466 (*-- normalise 20.10.02 --*)
467 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
469 "norm_sqrt_equ e_e v_v = (
472 (Repeat(Try (Rewrite ''makex1_x''))) #>
473 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
474 (Try (Rewrite_Set ''rooteq_simplify'')) #>
475 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
476 (Try (Rewrite_Set ''rooteq_simplify''))
479 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
480 [BOOL e_e, REAL v_v])"
482 method met_rooteq_norm : "RootEq/norm_sq_root_equation" =
483 \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
484 crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
485 Program: norm_sqrt_equ.simps
486 Given: "equality e_e" "solveFor v_v"
487 Where: "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
488 Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
489 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
490 Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
491 Find: "solutions v_v'i'"
493 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
495 "solve_sqrt_equ e_e v_v =
498 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #>
499 (Try (Rewrite_Set ''rooteq_simplify'')) #>
500 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
501 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
502 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
504 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
506 SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])
509 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
510 [BOOL e_e, REAL v_v])
511 in Check_elementwise L_L {(v_v::real). Assumptions})"
513 method met_rooteq_sq : "RootEq/solve_sq_root_equation" =
514 \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
515 crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
516 Program: solve_sqrt_equ.simps
517 Given: "equality e_e" "solveFor v_v"
518 Where: "(((lhs e_e) is_sqrtTerm_in (v_v::real)) &
519 ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
520 (((rhs e_e) is_sqrtTerm_in (v_v::real)) &
521 ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
522 Find: "solutions v_v'i'"
524 (*-- right 28.08.02 --*)
525 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
527 "solve_sqrt_equ_right e_e v_v =
530 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
531 (Try (Rewrite_Set ''rooteq_simplify'')) #>
532 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
533 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
534 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
536 if (rhs e_e) is_sqrtTerm_in v_v
538 SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
541 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
542 [BOOL e_e, REAL v_v])"
544 method met_rooteq_sq_right : "RootEq/solve_right_sq_root_equation" =
545 \<open>{rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
546 crls = RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
547 Program: solve_sqrt_equ_right.simps
548 Given: "equality e_e" "solveFor v_v"
549 Where: "(rhs e_e) is_sqrtTerm_in v_v"
550 Find: "solutions v_v'i'"
552 (*-- left 28.08.02 --*)
553 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
555 "solve_sqrt_equ_left e_e v_v =
558 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
559 (Try (Rewrite_Set ''rooteq_simplify'')) #>
560 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
561 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
562 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
564 if (lhs e_e) is_sqrtTerm_in v_v
566 SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
569 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
570 [BOOL e_e, REAL v_v])"
572 method met_rooteq_sq_left : "RootEq/solve_left_sq_root_equation" =
573 \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
574 crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
575 Program: solve_sqrt_equ_left.simps
576 Given: "equality e_e" "solveFor v_v"
577 Where: "(lhs e_e) is_sqrtTerm_in v_v"
578 Find: "solutions v_v'i'"