clarified command name: this is to register already defined rule sets in the Knowledge Store;
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>
112 (* true if bdv is under sqrt of a Equation*)
113 fun is_rootTerm_in t v =
115 fun findroot (t as (_ $ _ $ _ $ _)) _ = raise TERM ( "is_rootTerm_in", [t])
116 (* at the moment there is no term like this, but ....*)
117 | findroot (Const ("Root.nroot",_) $ _ $ t3) v = Prog_Expr.occurs_in v t3
118 | findroot (_ $ t2 $ t3) v = findroot t2 v orelse findroot t3 v
119 | findroot (Const ("NthRoot.sqrt", _) $ t2) v = Prog_Expr.occurs_in v t2
120 | findroot (_ $ t2) v = findroot t2 v
121 | findroot _ _ = false;
126 fun is_sqrtTerm_in t v =
128 fun findsqrt (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_sqrteqation_in", [t])
129 (* at the moment there is no term like this, but ....*)
130 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
131 | findsqrt (Const ("NthRoot.sqrt", _) $ a) v = Prog_Expr.occurs_in v a
132 | findsqrt (_ $ t1) v = findsqrt t1 v
133 | findsqrt _ _ = false;
138 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
139 and the subterm ist connected with + or * --> is normalised*)
140 fun is_normSqrtTerm_in t v =
142 fun isnorm (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_normSqrtTerm_in", [t])
143 (* at the moment there is no term like this, but ....*)
144 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
145 | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
146 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) _ = false
147 | isnorm (Const ("Rings.divide_class.divide",_) $ t1 $ t2) v =
148 is_sqrtTerm_in t1 v orelse is_sqrtTerm_in t2 v
149 | isnorm (Const ("NthRoot.sqrt", _) $ t1) v = Prog_Expr.occurs_in v t1
150 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
151 | isnorm _ _ = false;
156 fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is_rootTerm_in",_) $ t $ v)) _ =
157 if is_rootTerm_in t v
158 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
159 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
160 | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
162 fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is_sqrtTerm_in",_) $ t $ v)) _ =
163 if is_sqrtTerm_in t v
164 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
165 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
166 | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
168 fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is_normSqrtTerm_in",_) $ t $ v)) _ =
169 if is_normSqrtTerm_in t v
170 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
171 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
172 | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
174 setup \<open>KEStore_Elems.add_calcs
175 [("is_rootTerm_in", ("RootEq.is_rootTerm_in", eval_is_rootTerm_in"")),
176 ("is_sqrtTerm_in", ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in"")),
177 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))]\<close>
179 subsection \<open>rule-sets\<close>
181 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
182 Rule_Set.append_rules "RootEq_prls" Rule_Set.empty
183 [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
184 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
185 Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""),
186 Rule.Eval ("Prog_Expr.rhs" , Prog_Expr.eval_rhs ""),
187 Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
188 Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
189 Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in ""),
190 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
191 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
192 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
193 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
194 Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
195 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
196 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false})
200 Rule_Set.append_rules "RootEq_erls" Root_erls
201 [Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left})];
204 Rule_Set.append_rules "RootEq_crls" Root_crls
205 [Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left})];
208 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
209 [Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
210 Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""),
211 Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in "")];
215 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
216 val sqrt_isolate = prep_rls'(
217 Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
218 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
220 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
221 (* (sqrt a) \<up> 2 -> a *)
222 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
223 (* sqrt (a \<up> 2) -> a *)
224 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
225 (* sqrt a sqrt b -> sqrt(ab) *)
226 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
227 (* a sqrt b sqrt c -> a sqrt(bc) *)
228 Rule.Thm("sqrt_square_equation_both_1",
229 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
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("sqrt_square_equation_both_2",
233 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}),
234 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
235 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
236 Rule.Thm("sqrt_square_equation_both_3",
237 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}),
238 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
239 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
240 Rule.Thm("sqrt_square_equation_both_4",
241 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}),
242 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
243 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
244 Rule.Thm("sqrt_isolate_l_add1",
245 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}),
246 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
247 Rule.Thm("sqrt_isolate_l_add2",
248 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}),
249 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
250 Rule.Thm("sqrt_isolate_l_add3",
251 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}),
252 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
253 Rule.Thm("sqrt_isolate_l_add4",
254 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}),
255 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
256 Rule.Thm("sqrt_isolate_l_add5",
257 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}),
258 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
259 Rule.Thm("sqrt_isolate_l_add6",
260 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
261 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
262 (*Rule.Thm("sqrt_isolate_l_div",ThmC.numerals_to_Free @{thm sqrt_isolate_l_div}),*)
263 (* b*sqrt(x) = d sqrt(x) d/b *)
264 Rule.Thm("sqrt_isolate_r_add1",
265 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
266 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
267 Rule.Thm("sqrt_isolate_r_add2",
268 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
269 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
270 Rule.Thm("sqrt_isolate_r_add3",
271 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
272 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
273 Rule.Thm("sqrt_isolate_r_add4",
274 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
275 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
276 Rule.Thm("sqrt_isolate_r_add5",
277 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
278 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
279 Rule.Thm("sqrt_isolate_r_add6",
280 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
281 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
282 (*Rule.Thm("sqrt_isolate_r_div",ThmC.numerals_to_Free @{thm sqrt_isolate_r_div}),*)
283 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
284 Rule.Thm("sqrt_square_equation_left_1",
285 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
286 (* sqrt(x)=b -> x=b^2 *)
287 Rule.Thm("sqrt_square_equation_left_2",
288 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
289 (* c*sqrt(x)=b -> c^2*x=b^2 *)
290 Rule.Thm("sqrt_square_equation_left_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_3}),
291 (* c/sqrt(x)=b -> c^2/x=b^2 *)
292 Rule.Thm("sqrt_square_equation_left_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_4}),
293 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
294 Rule.Thm("sqrt_square_equation_left_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_5}),
295 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
296 Rule.Thm("sqrt_square_equation_left_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_6}),
297 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
298 Rule.Thm("sqrt_square_equation_right_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_1}),
299 (* a=sqrt(x) ->a^2=x *)
300 Rule.Thm("sqrt_square_equation_right_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_2}),
301 (* a=c*sqrt(x) ->a^2=c^2*x *)
302 Rule.Thm("sqrt_square_equation_right_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_3}),
303 (* a=c/sqrt(x) ->a^2=c^2/x *)
304 Rule.Thm("sqrt_square_equation_right_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_4}),
305 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
306 Rule.Thm("sqrt_square_equation_right_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_5}),
307 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
308 Rule.Thm("sqrt_square_equation_right_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_6})
309 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
310 ],scr = Rule.Empty_Prog
314 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
315 val l_sqrt_isolate = prep_rls'(
316 Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
317 rew_ord = ("termlessI",termlessI),
318 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
320 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
321 (* (sqrt a) \<up> 2 -> a *)
322 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
323 (* sqrt (a \<up> 2) -> a *)
324 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
325 (* sqrt a sqrt b -> sqrt(ab) *)
326 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
327 (* a sqrt b sqrt c -> a sqrt(bc) *)
328 Rule.Thm("sqrt_isolate_l_add1",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}),
329 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
330 Rule.Thm("sqrt_isolate_l_add2",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}),
331 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
332 Rule.Thm("sqrt_isolate_l_add3",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}),
333 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
334 Rule.Thm("sqrt_isolate_l_add4",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}),
335 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
336 Rule.Thm("sqrt_isolate_l_add5",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}),
337 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
338 Rule.Thm("sqrt_isolate_l_add6",ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
339 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
340 (*Rule.Thm("sqrt_isolate_l_div",ThmC.numerals_to_Free @{thm sqrt_isolate_l_div}),*)
341 (* b*sqrt(x) = d sqrt(x) d/b *)
342 Rule.Thm("sqrt_square_equation_left_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
343 (* sqrt(x)=b -> x=b^2 *)
344 Rule.Thm("sqrt_square_equation_left_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
345 (* a*sqrt(x)=b -> a^2*x=b^2*)
346 Rule.Thm("sqrt_square_equation_left_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_3}),
347 (* c/sqrt(x)=b -> c^2/x=b^2 *)
348 Rule.Thm("sqrt_square_equation_left_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_4}),
349 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
350 Rule.Thm("sqrt_square_equation_left_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_5}),
351 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
352 Rule.Thm("sqrt_square_equation_left_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_left_6})
353 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
355 scr = Rule.Empty_Prog
359 (* -- right 28.8.02--*)
360 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
361 val r_sqrt_isolate = prep_rls'(
362 Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
363 rew_ord = ("termlessI",termlessI),
364 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
366 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1}),
367 (* (sqrt a) \<up> 2 -> a *)
368 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
369 (* sqrt (a \<up> 2) -> a *)
370 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
371 (* sqrt a sqrt b -> sqrt(ab) *)
372 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
373 (* a sqrt b sqrt c -> a sqrt(bc) *)
374 Rule.Thm("sqrt_isolate_r_add1",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
375 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
376 Rule.Thm("sqrt_isolate_r_add2",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
377 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
378 Rule.Thm("sqrt_isolate_r_add3",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
379 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
380 Rule.Thm("sqrt_isolate_r_add4",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
381 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
382 Rule.Thm("sqrt_isolate_r_add5",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
383 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
384 Rule.Thm("sqrt_isolate_r_add6",ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
385 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
386 (*Rule.Thm("sqrt_isolate_r_div",ThmC.numerals_to_Free @{thm sqrt_isolate_r_div}),*)
387 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
388 Rule.Thm("sqrt_square_equation_right_1",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_1}),
389 (* a=sqrt(x) ->a^2=x *)
390 Rule.Thm("sqrt_square_equation_right_2",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_2}),
391 (* a=c*sqrt(x) ->a^2=c^2*x *)
392 Rule.Thm("sqrt_square_equation_right_3",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_3}),
393 (* a=c/sqrt(x) ->a^2=c^2/x *)
394 Rule.Thm("sqrt_square_equation_right_4",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_4}),
395 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
396 Rule.Thm("sqrt_square_equation_right_5",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_5}),
397 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
398 Rule.Thm("sqrt_square_equation_right_6",ThmC.numerals_to_Free @{thm sqrt_square_equation_right_6})
399 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
401 scr = Rule.Empty_Prog
405 val rooteq_simplify = prep_rls'(
406 Rule_Def.Repeat {id = "rooteq_simplify",
407 preconds = [], rew_ord = ("termlessI",termlessI),
408 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
409 (*asm_thm = [("sqrt_square_1", "")],*)
410 rules = [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
411 (* a+(b+c) = a+b+c *)
412 Rule.Thm ("real_assoc_2",ThmC.numerals_to_Free @{thm real_assoc_2}),
413 (* a*(b*c) = a*b*c *)
414 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
415 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
416 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
417 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
418 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
419 Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
420 Rule.Thm("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
421 Rule.Thm("real_minus_binom_pow2",ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
422 Rule.Thm("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
423 (* (a * b)^n = a^n * b^n*)
424 Rule.Thm("sqrt_times_root_1",ThmC.numerals_to_Free @{thm sqrt_times_root_1}),
425 (* sqrt b * sqrt c = sqrt(b*c) *)
426 Rule.Thm("sqrt_times_root_2",ThmC.numerals_to_Free @{thm sqrt_times_root_2}),
427 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
428 Rule.Thm("sqrt_square_2",ThmC.numerals_to_Free @{thm sqrt_square_2}),
429 (* sqrt (a \<up> 2) = a *)
430 Rule.Thm("sqrt_square_1",ThmC.numerals_to_Free @{thm sqrt_square_1})
431 (* sqrt a \<up> 2 = a *)
433 scr = Rule.Empty_Prog
437 RootEq_erls = RootEq_erls and
438 rooteq_srls = rooteq_srls and
439 sqrt_isolate = sqrt_isolate and
440 l_sqrt_isolate = l_sqrt_isolate and
441 r_sqrt_isolate = r_sqrt_isolate and
442 rooteq_simplify = rooteq_simplify
444 subsection \<open>problems\<close>
445 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
446 setup \<open>KEStore_Elems.add_pbts
447 (* ---------root----------- *)
448 [(Problem.prep_input thy "pbl_equ_univ_root" [] Problem.id_empty
449 (["rootX", "univariate", "equation"],
450 [("#Given" ,["equality e_e", "solveFor v_v"]),
451 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
452 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
453 ("#Find" ,["solutions v_v'i'"])],
454 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
455 (* ---------sqrt----------- *)
456 (Problem.prep_input thy "pbl_equ_univ_root_sq" [] Problem.id_empty
457 (["sq", "rootX", "univariate", "equation"],
458 [("#Given" ,["equality e_e", "solveFor v_v"]),
459 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
460 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
461 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
462 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
463 ("#Find" ,["solutions v_v'i'"])],
464 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
465 (* ---------normalise----------- *)
466 (Problem.prep_input thy "pbl_equ_univ_root_norm" [] Problem.id_empty
467 (["normalise", "rootX", "univariate", "equation"],
468 [("#Given" ,["equality e_e", "solveFor v_v"]),
469 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
470 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
471 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
472 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
473 ("#Find" ,["solutions v_v'i'"])],
474 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close>
475 (*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
477 subsection \<open>methods\<close>
478 setup \<open>KEStore_Elems.add_mets
479 [MethodC.prep_input thy "met_rooteq" [] MethodC.id_empty
481 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
482 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
484 (*-- normalise 20.10.02 --*)
485 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
487 "norm_sqrt_equ e_e v_v = (
490 (Repeat(Try (Rewrite ''makex1_x''))) #>
491 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
492 (Try (Rewrite_Set ''rooteq_simplify'')) #>
493 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
494 (Try (Rewrite_Set ''rooteq_simplify''))
497 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
498 [BOOL e_e, REAL v_v])"
499 setup \<open>KEStore_Elems.add_mets
500 [MethodC.prep_input thy "met_rooteq_norm" [] MethodC.id_empty
501 (["RootEq", "norm_sq_root_equation"],
502 [("#Given" ,["equality e_e", "solveFor v_v"]),
503 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
504 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
505 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
506 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
507 ("#Find" ,["solutions v_v'i'"])],
508 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
509 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
510 @{thm norm_sqrt_equ.simps})]
513 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
515 "solve_sqrt_equ e_e v_v =
518 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #>
519 (Try (Rewrite_Set ''rooteq_simplify'')) #>
520 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
521 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
522 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
524 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
526 SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])
529 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
530 [BOOL e_e, REAL v_v])
531 in Check_elementwise L_L {(v_v::real). Assumptions})"
532 setup \<open>KEStore_Elems.add_mets
533 [MethodC.prep_input thy "met_rooteq_sq" [] MethodC.id_empty
534 (["RootEq", "solve_sq_root_equation"],
535 [("#Given" ,["equality e_e", "solveFor v_v"]),
536 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
537 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
538 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
539 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
540 ("#Find" ,["solutions v_v'i'"])],
541 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
542 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
543 @{thm solve_sqrt_equ.simps})]
545 (*-- right 28.08.02 --*)
546 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
548 "solve_sqrt_equ_right e_e v_v =
551 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
552 (Try (Rewrite_Set ''rooteq_simplify'')) #>
553 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
554 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
555 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
557 if (rhs e_e) is_sqrtTerm_in v_v
559 SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
562 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
563 [BOOL e_e, REAL v_v])"
564 setup \<open>KEStore_Elems.add_mets
565 [MethodC.prep_input thy "met_rooteq_sq_right" [] MethodC.id_empty
566 (["RootEq", "solve_right_sq_root_equation"],
567 [("#Given" ,["equality e_e", "solveFor v_v"]),
568 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
569 ("#Find" ,["solutions v_v'i'"])],
570 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
571 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
572 @{thm solve_sqrt_equ_right.simps})]
574 (*-- left 28.08.02 --*)
575 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
577 "solve_sqrt_equ_left e_e v_v =
580 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
581 (Try (Rewrite_Set ''rooteq_simplify'')) #>
582 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
583 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
584 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
586 if (lhs e_e) is_sqrtTerm_in v_v
588 SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
591 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
592 [BOOL e_e, REAL v_v])"
593 setup \<open>KEStore_Elems.add_mets
594 [MethodC.prep_input thy "met_rooteq_sq_left" [] MethodC.id_empty
595 (["RootEq", "solve_left_sq_root_equation"],
596 [("#Given" ,["equality e_e", "solveFor v_v"]),
597 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
598 ("#Find" ,["solutions v_v'i'"])],
599 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
600 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
601 @{thm solve_sqrt_equ_left.simps})]