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 ("Root.nroot",_) $ _ $ t3) v = Prog_Expr.occurs_in v t3
116 | findroot (_ $ t2 $ t3) v = findroot t2 v orelse findroot t3 v
117 | findroot (Const ("NthRoot.sqrt", _) $ 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 ("NthRoot.sqrt", _) $ 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 ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
143 | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
144 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) _ = false
145 | isnorm (Const ("Rings.divide_class.divide",_) $ t1 $ t2) v =
146 is_sqrtTerm_in t1 v orelse is_sqrtTerm_in t2 v
147 | isnorm (Const ("NthRoot.sqrt", _) $ 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 ("RootEq.is_rootTerm_in",_) $ 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 ("RootEq.is_sqrtTerm_in",_) $ 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 ("RootEq.is_normSqrtTerm_in",_) $ 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 setup \<open>KEStore_Elems.add_calcs
173 [("is_rootTerm_in", ("RootEq.is_rootTerm_in", eval_is_rootTerm_in"")),
174 ("is_sqrtTerm_in", ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in"")),
175 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))]\<close>
177 subsection \<open>rule-sets\<close>
179 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
180 Rule_Set.append_rules "RootEq_prls" Rule_Set.empty
181 [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
182 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
183 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
184 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
185 \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
186 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
187 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
188 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
189 \<^rule_thm>\<open>not_true\<close>,
190 \<^rule_thm>\<open>not_false\<close>,
191 \<^rule_thm>\<open>and_true\<close>,
192 \<^rule_thm>\<open>and_false\<close>,
193 \<^rule_thm>\<open>or_true\<close>,
194 \<^rule_thm>\<open>or_false\<close>
198 Rule_Set.append_rules "RootEq_erls" Root_erls
199 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
202 Rule_Set.append_rules "RootEq_crls" Root_crls
203 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
206 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
207 [\<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
208 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),
209 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];
213 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
214 val sqrt_isolate = prep_rls'(
215 Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
216 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
218 \<^rule_thm>\<open>sqrt_square_1\<close>,
219 (* (sqrt a) \<up> 2 -> a *)
220 \<^rule_thm>\<open>sqrt_square_2\<close>,
221 (* sqrt (a \<up> 2) -> a *)
222 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
223 (* sqrt a sqrt b -> sqrt(ab) *)
224 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
225 (* a sqrt b sqrt c -> a sqrt(bc) *)
226 \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
227 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
228 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
229 \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
230 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
231 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
232 \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
233 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
234 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
235 \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
236 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
237 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
238 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
239 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
240 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
241 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
242 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
243 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
244 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
245 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
246 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
247 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
248 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
249 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
250 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
251 (* b*sqrt(x) = d sqrt(x) d/b *)
252 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
253 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
254 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
255 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
256 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
257 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
258 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
259 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
260 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
261 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
262 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
263 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
264 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
265 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
266 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
267 (* sqrt(x)=b -> x=b^2 *)
268 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
269 (* c*sqrt(x)=b -> c^2*x=b^2 *)
270 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
271 (* c/sqrt(x)=b -> c^2/x=b^2 *)
272 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
273 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
274 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
275 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
276 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>,
277 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
278 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
279 (* a=sqrt(x) ->a^2=x *)
280 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
281 (* a=c*sqrt(x) ->a^2=c^2*x *)
282 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
283 (* a=c/sqrt(x) ->a^2=c^2/x *)
284 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
285 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
286 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
287 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
288 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
289 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
290 ],scr = Rule.Empty_Prog
294 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
295 val l_sqrt_isolate = prep_rls'(
296 Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
297 rew_ord = ("termlessI",termlessI),
298 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
300 \<^rule_thm>\<open>sqrt_square_1\<close>,
301 (* (sqrt a) \<up> 2 -> a *)
302 \<^rule_thm>\<open>sqrt_square_2\<close>,
303 (* sqrt (a \<up> 2) -> a *)
304 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
305 (* sqrt a sqrt b -> sqrt(ab) *)
306 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
307 (* a sqrt b sqrt c -> a sqrt(bc) *)
308 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
309 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
310 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
311 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
312 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
313 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
314 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
315 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
316 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
317 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
318 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
319 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
320 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
321 (* b*sqrt(x) = d sqrt(x) d/b *)
322 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
323 (* sqrt(x)=b -> x=b^2 *)
324 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
325 (* a*sqrt(x)=b -> a^2*x=b^2*)
326 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
327 (* c/sqrt(x)=b -> c^2/x=b^2 *)
328 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
329 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
330 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
331 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
332 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>
333 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
335 scr = Rule.Empty_Prog
339 (* -- right 28.8.02--*)
340 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
341 val r_sqrt_isolate = prep_rls'(
342 Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
343 rew_ord = ("termlessI",termlessI),
344 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
346 \<^rule_thm>\<open>sqrt_square_1\<close>,
347 (* (sqrt a) \<up> 2 -> a *)
348 \<^rule_thm>\<open>sqrt_square_2\<close>,
349 (* sqrt (a \<up> 2) -> a *)
350 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
351 (* sqrt a sqrt b -> sqrt(ab) *)
352 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
353 (* a sqrt b sqrt c -> a sqrt(bc) *)
354 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
355 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
356 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
357 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
358 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
359 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
360 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
361 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
362 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
363 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
364 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
365 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
366 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
367 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
368 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
369 (* a=sqrt(x) ->a^2=x *)
370 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
371 (* a=c*sqrt(x) ->a^2=c^2*x *)
372 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
373 (* a=c/sqrt(x) ->a^2=c^2/x *)
374 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
375 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
376 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
377 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
378 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
379 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
381 scr = Rule.Empty_Prog
385 val rooteq_simplify = prep_rls'(
386 Rule_Def.Repeat {id = "rooteq_simplify",
387 preconds = [], rew_ord = ("termlessI",termlessI),
388 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
389 (*asm_thm = [("sqrt_square_1", "")],*)
390 rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
391 (* a+(b+c) = a+b+c *)
392 \<^rule_thm>\<open>real_assoc_2\<close>,
393 (* a*(b*c) = a*b*c *)
394 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
395 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
396 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
397 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
398 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
399 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
400 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
401 \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
402 \<^rule_thm>\<open>realpow_mul\<close>,
403 (* (a * b)^n = a^n * b^n*)
404 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
405 (* sqrt b * sqrt c = sqrt(b*c) *)
406 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
407 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
408 \<^rule_thm>\<open>sqrt_square_2\<close>,
409 (* sqrt (a \<up> 2) = a *)
410 \<^rule_thm>\<open>sqrt_square_1\<close>
411 (* sqrt a \<up> 2 = a *)
413 scr = Rule.Empty_Prog
417 RootEq_erls = RootEq_erls and
418 rooteq_srls = rooteq_srls and
419 sqrt_isolate = sqrt_isolate and
420 l_sqrt_isolate = l_sqrt_isolate and
421 r_sqrt_isolate = r_sqrt_isolate and
422 rooteq_simplify = rooteq_simplify
424 subsection \<open>problems\<close>
425 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
426 setup \<open>KEStore_Elems.add_pbts
427 (* ---------root----------- *)
428 [(Problem.prep_input @{theory} "pbl_equ_univ_root" [] Problem.id_empty
429 (["rootX", "univariate", "equation"],
430 [("#Given" ,["equality e_e", "solveFor v_v"]),
431 ("#Where" ,["(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'"])],
434 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
435 (* ---------sqrt----------- *)
436 (Problem.prep_input @{theory} "pbl_equ_univ_root_sq" [] Problem.id_empty
437 (["sq", "rootX", "univariate", "equation"],
438 [("#Given" ,["equality e_e", "solveFor v_v"]),
439 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
440 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
441 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
442 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
443 ("#Find" ,["solutions v_v'i'"])],
444 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
445 (* ---------normalise----------- *)
446 (Problem.prep_input @{theory} "pbl_equ_univ_root_norm" [] Problem.id_empty
447 (["normalise", "rootX", "univariate", "equation"],
448 [("#Given" ,["equality e_e", "solveFor v_v"]),
449 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
450 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
451 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
452 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
453 ("#Find" ,["solutions v_v'i'"])],
454 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close>
455 (*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
457 subsection \<open>methods\<close>
458 setup \<open>KEStore_Elems.add_mets
459 [MethodC.prep_input @{theory} "met_rooteq" [] MethodC.id_empty
461 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
462 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
464 (*-- normalise 20.10.02 --*)
465 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
467 "norm_sqrt_equ e_e v_v = (
470 (Repeat(Try (Rewrite ''makex1_x''))) #>
471 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
472 (Try (Rewrite_Set ''rooteq_simplify'')) #>
473 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
474 (Try (Rewrite_Set ''rooteq_simplify''))
477 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
478 [BOOL e_e, REAL v_v])"
479 setup \<open>KEStore_Elems.add_mets
480 [MethodC.prep_input @{theory} "met_rooteq_norm" [] MethodC.id_empty
481 (["RootEq", "norm_sq_root_equation"],
482 [("#Given" ,["equality e_e", "solveFor v_v"]),
483 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
484 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
485 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
486 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
487 ("#Find" ,["solutions v_v'i'"])],
488 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
489 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
490 @{thm norm_sqrt_equ.simps})]
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})"
512 setup \<open>KEStore_Elems.add_mets
513 [MethodC.prep_input @{theory} "met_rooteq_sq" [] MethodC.id_empty
514 (["RootEq", "solve_sq_root_equation"],
515 [("#Given" ,["equality e_e", "solveFor v_v"]),
516 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
517 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
518 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
519 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
520 ("#Find" ,["solutions v_v'i'"])],
521 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
522 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
523 @{thm solve_sqrt_equ.simps})]
525 (*-- right 28.08.02 --*)
526 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
528 "solve_sqrt_equ_right e_e v_v =
531 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
532 (Try (Rewrite_Set ''rooteq_simplify'')) #>
533 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
534 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
535 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
537 if (rhs e_e) is_sqrtTerm_in v_v
539 SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
542 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
543 [BOOL e_e, REAL v_v])"
544 setup \<open>KEStore_Elems.add_mets
545 [MethodC.prep_input @{theory} "met_rooteq_sq_right" [] MethodC.id_empty
546 (["RootEq", "solve_right_sq_root_equation"],
547 [("#Given" ,["equality e_e", "solveFor v_v"]),
548 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
549 ("#Find" ,["solutions v_v'i'"])],
550 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
551 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
552 @{thm solve_sqrt_equ_right.simps})]
554 (*-- left 28.08.02 --*)
555 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
557 "solve_sqrt_equ_left e_e v_v =
560 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
561 (Try (Rewrite_Set ''rooteq_simplify'')) #>
562 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
563 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
564 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
566 if (lhs e_e) is_sqrtTerm_in v_v
568 SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
571 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
572 [BOOL e_e, REAL v_v])"
573 setup \<open>KEStore_Elems.add_mets
574 [MethodC.prep_input @{theory} "met_rooteq_sq_left" [] MethodC.id_empty
575 (["RootEq", "solve_left_sq_root_equation"],
576 [("#Given" ,["equality e_e", "solveFor v_v"]),
577 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
578 ("#Find" ,["solutions v_v'i'"])],
579 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
580 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
581 @{thm solve_sqrt_equ_left.simps})]