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("sqrt_square_equation_both_1",
227 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
228 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
229 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
230 Rule.Thm("sqrt_square_equation_both_2",
231 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}),
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("sqrt_square_equation_both_3",
235 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}),
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("sqrt_square_equation_both_4",
239 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}),
240 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
241 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
242 Rule.Thm("sqrt_isolate_l_add1",
243 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}),
244 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
245 Rule.Thm("sqrt_isolate_l_add2",
246 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}),
247 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
248 Rule.Thm("sqrt_isolate_l_add3",
249 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}),
250 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
251 Rule.Thm("sqrt_isolate_l_add4",
252 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}),
253 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
254 Rule.Thm("sqrt_isolate_l_add5",
255 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}),
256 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
257 Rule.Thm("sqrt_isolate_l_add6",
258 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
259 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
260 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
261 (* b*sqrt(x) = d sqrt(x) d/b *)
262 Rule.Thm("sqrt_isolate_r_add1",
263 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
264 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
265 Rule.Thm("sqrt_isolate_r_add2",
266 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
267 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
268 Rule.Thm("sqrt_isolate_r_add3",
269 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
270 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
271 Rule.Thm("sqrt_isolate_r_add4",
272 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
273 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
274 Rule.Thm("sqrt_isolate_r_add5",
275 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
276 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
277 Rule.Thm("sqrt_isolate_r_add6",
278 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
279 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
280 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
281 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
282 Rule.Thm("sqrt_square_equation_left_1",
283 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
284 (* sqrt(x)=b -> x=b^2 *)
285 Rule.Thm("sqrt_square_equation_left_2",
286 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
287 (* c*sqrt(x)=b -> c^2*x=b^2 *)
288 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
289 (* c/sqrt(x)=b -> c^2/x=b^2 *)
290 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
291 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
292 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
293 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
294 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>,
295 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
296 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
297 (* a=sqrt(x) ->a^2=x *)
298 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
299 (* a=c*sqrt(x) ->a^2=c^2*x *)
300 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
301 (* a=c/sqrt(x) ->a^2=c^2/x *)
302 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
303 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
304 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
305 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
306 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
307 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
308 ],scr = Rule.Empty_Prog
312 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
313 val l_sqrt_isolate = prep_rls'(
314 Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
315 rew_ord = ("termlessI",termlessI),
316 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
318 \<^rule_thm>\<open>sqrt_square_1\<close>,
319 (* (sqrt a) \<up> 2 -> a *)
320 \<^rule_thm>\<open>sqrt_square_2\<close>,
321 (* sqrt (a \<up> 2) -> a *)
322 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
323 (* sqrt a sqrt b -> sqrt(ab) *)
324 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
325 (* a sqrt b sqrt c -> a sqrt(bc) *)
326 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
327 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
328 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
329 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
330 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
331 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
332 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
333 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
334 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
335 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
336 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
337 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
338 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
339 (* b*sqrt(x) = d sqrt(x) d/b *)
340 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
341 (* sqrt(x)=b -> x=b^2 *)
342 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
343 (* a*sqrt(x)=b -> a^2*x=b^2*)
344 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
345 (* c/sqrt(x)=b -> c^2/x=b^2 *)
346 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
347 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
348 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
349 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
350 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>
351 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
353 scr = Rule.Empty_Prog
357 (* -- right 28.8.02--*)
358 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
359 val r_sqrt_isolate = prep_rls'(
360 Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
361 rew_ord = ("termlessI",termlessI),
362 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
364 \<^rule_thm>\<open>sqrt_square_1\<close>,
365 (* (sqrt a) \<up> 2 -> a *)
366 \<^rule_thm>\<open>sqrt_square_2\<close>,
367 (* sqrt (a \<up> 2) -> a *)
368 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
369 (* sqrt a sqrt b -> sqrt(ab) *)
370 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
371 (* a sqrt b sqrt c -> a sqrt(bc) *)
372 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
373 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
374 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
375 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
376 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
377 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
378 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
379 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
380 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
381 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
382 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
383 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
384 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
385 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
386 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
387 (* a=sqrt(x) ->a^2=x *)
388 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
389 (* a=c*sqrt(x) ->a^2=c^2*x *)
390 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
391 (* a=c/sqrt(x) ->a^2=c^2/x *)
392 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
393 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
394 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
395 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
396 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
397 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
399 scr = Rule.Empty_Prog
403 val rooteq_simplify = prep_rls'(
404 Rule_Def.Repeat {id = "rooteq_simplify",
405 preconds = [], rew_ord = ("termlessI",termlessI),
406 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
407 (*asm_thm = [("sqrt_square_1", "")],*)
408 rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
409 (* a+(b+c) = a+b+c *)
410 \<^rule_thm>\<open>real_assoc_2\<close>,
411 (* a*(b*c) = a*b*c *)
412 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
413 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
414 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
415 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
416 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
417 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
418 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
419 \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
420 \<^rule_thm>\<open>realpow_mul\<close>,
421 (* (a * b)^n = a^n * b^n*)
422 \<^rule_thm>\<open>sqrt_times_root_1\<close>,
423 (* sqrt b * sqrt c = sqrt(b*c) *)
424 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
425 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
426 \<^rule_thm>\<open>sqrt_square_2\<close>,
427 (* sqrt (a \<up> 2) = a *)
428 \<^rule_thm>\<open>sqrt_square_1\<close>
429 (* sqrt a \<up> 2 = a *)
431 scr = Rule.Empty_Prog
435 RootEq_erls = RootEq_erls and
436 rooteq_srls = rooteq_srls and
437 sqrt_isolate = sqrt_isolate and
438 l_sqrt_isolate = l_sqrt_isolate and
439 r_sqrt_isolate = r_sqrt_isolate and
440 rooteq_simplify = rooteq_simplify
442 subsection \<open>problems\<close>
443 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
444 setup \<open>KEStore_Elems.add_pbts
445 (* ---------root----------- *)
446 [(Problem.prep_input @{theory} "pbl_equ_univ_root" [] Problem.id_empty
447 (["rootX", "univariate", "equation"],
448 [("#Given" ,["equality e_e", "solveFor v_v"]),
449 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
450 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
451 ("#Find" ,["solutions v_v'i'"])],
452 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
453 (* ---------sqrt----------- *)
454 (Problem.prep_input @{theory} "pbl_equ_univ_root_sq" [] Problem.id_empty
455 (["sq", "rootX", "univariate", "equation"],
456 [("#Given" ,["equality e_e", "solveFor v_v"]),
457 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
458 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
459 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
460 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
461 ("#Find" ,["solutions v_v'i'"])],
462 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
463 (* ---------normalise----------- *)
464 (Problem.prep_input @{theory} "pbl_equ_univ_root_norm" [] Problem.id_empty
465 (["normalise", "rootX", "univariate", "equation"],
466 [("#Given" ,["equality e_e", "solveFor v_v"]),
467 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
468 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
469 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
470 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
471 ("#Find" ,["solutions v_v'i'"])],
472 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close>
473 (*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
475 subsection \<open>methods\<close>
476 setup \<open>KEStore_Elems.add_mets
477 [MethodC.prep_input @{theory} "met_rooteq" [] MethodC.id_empty
479 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
480 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
482 (*-- normalise 20.10.02 --*)
483 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
485 "norm_sqrt_equ e_e v_v = (
488 (Repeat(Try (Rewrite ''makex1_x''))) #>
489 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
490 (Try (Rewrite_Set ''rooteq_simplify'')) #>
491 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
492 (Try (Rewrite_Set ''rooteq_simplify''))
495 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
496 [BOOL e_e, REAL v_v])"
497 setup \<open>KEStore_Elems.add_mets
498 [MethodC.prep_input @{theory} "met_rooteq_norm" [] MethodC.id_empty
499 (["RootEq", "norm_sq_root_equation"],
500 [("#Given" ,["equality e_e", "solveFor v_v"]),
501 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
502 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
503 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
504 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
505 ("#Find" ,["solutions v_v'i'"])],
506 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
507 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
508 @{thm norm_sqrt_equ.simps})]
511 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
513 "solve_sqrt_equ e_e v_v =
516 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #>
517 (Try (Rewrite_Set ''rooteq_simplify'')) #>
518 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
519 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
520 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
522 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
524 SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])
527 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
528 [BOOL e_e, REAL v_v])
529 in Check_elementwise L_L {(v_v::real). Assumptions})"
530 setup \<open>KEStore_Elems.add_mets
531 [MethodC.prep_input @{theory} "met_rooteq_sq" [] MethodC.id_empty
532 (["RootEq", "solve_sq_root_equation"],
533 [("#Given" ,["equality e_e", "solveFor v_v"]),
534 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
535 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
536 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
537 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
538 ("#Find" ,["solutions v_v'i'"])],
539 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
540 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
541 @{thm solve_sqrt_equ.simps})]
543 (*-- right 28.08.02 --*)
544 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
546 "solve_sqrt_equ_right e_e v_v =
549 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
550 (Try (Rewrite_Set ''rooteq_simplify'')) #>
551 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
552 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
553 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
555 if (rhs e_e) is_sqrtTerm_in v_v
557 SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
560 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
561 [BOOL e_e, REAL v_v])"
562 setup \<open>KEStore_Elems.add_mets
563 [MethodC.prep_input @{theory} "met_rooteq_sq_right" [] MethodC.id_empty
564 (["RootEq", "solve_right_sq_root_equation"],
565 [("#Given" ,["equality e_e", "solveFor v_v"]),
566 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
567 ("#Find" ,["solutions v_v'i'"])],
568 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
569 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
570 @{thm solve_sqrt_equ_right.simps})]
572 (*-- left 28.08.02 --*)
573 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
575 "solve_sqrt_equ_left e_e v_v =
578 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
579 (Try (Rewrite_Set ''rooteq_simplify'')) #>
580 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
581 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
582 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
584 if (lhs e_e) is_sqrtTerm_in v_v
586 SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
589 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
590 [BOOL e_e, REAL v_v])"
591 setup \<open>KEStore_Elems.add_mets
592 [MethodC.prep_input @{theory} "met_rooteq_sq_left" [] MethodC.id_empty
593 (["RootEq", "solve_left_sq_root_equation"],
594 [("#Given" ,["equality e_e", "solveFor v_v"]),
595 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
596 ("#Find" ,["solutions v_v'i'"])],
597 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
598 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
599 @{thm solve_sqrt_equ_left.simps})]