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>];
196 Rule_Set.append_rules "RootEq_erls" Root_erls
197 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
200 Rule_Set.append_rules "RootEq_crls" Root_crls
201 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
204 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty [
205 \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
206 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),
207 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];
211 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
212 val sqrt_isolate = prep_rls'(
214 id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
215 asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
217 \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
218 \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
219 \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
220 \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
221 \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>, (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
222 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
223 \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>, (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
224 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
225 \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>, (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
226 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
227 \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>, (* (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_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
230 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
231 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
232 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
233 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
234 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
236 \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)
237 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
238 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
239 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
240 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
241 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
242 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
244 \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)
245 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)
246 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* c*sqrt(x)=b -> c^2*x=b^2 *)
247 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)
248 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
249 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
250 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>, (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
251 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)
252 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)
253 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)
254 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
255 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
256 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
257 program = Rule.Empty_Prog});
260 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
261 val l_sqrt_isolate = prep_rls'(
263 id = "l_sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
264 asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
266 \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
267 \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
268 \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
269 \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
270 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
271 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
272 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
273 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
274 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
275 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
277 \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)
278 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)
279 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* a*sqrt(x)=b -> a^2*x=b^2*)
280 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)
281 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
282 \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
283 \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>], (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
284 program = Rule.Empty_Prog});
287 (* -- right 28.8.02--*)
288 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
289 val r_sqrt_isolate = prep_rls'(
290 Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
291 asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
293 \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
294 \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
295 \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
296 \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
297 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
298 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
299 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
300 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
301 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
302 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
304 \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)
305 \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)
306 \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)
307 \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)
308 \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
309 \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
310 \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
311 program = Rule.Empty_Prog});
314 val rooteq_simplify = prep_rls'(
316 id = "rooteq_simplify", preconds = [], rew_ord = ("termlessI",termlessI),
317 asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
319 \<^rule_thm>\<open>real_assoc_1\<close>, (* a+(b+c) = a+b+c *)
320 \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *)
321 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
322 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
323 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
324 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
325 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
326 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
327 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
328 \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
329 \<^rule_thm>\<open>realpow_mul\<close>, (* (a * b)^n = a^n * b^n*)
330 \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt b * sqrt c = sqrt(b*c) *)
331 \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
332 \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) = a *)
333 \<^rule_thm>\<open>sqrt_square_1\<close>], (* sqrt a \<up> 2 = a *)
334 program = Rule.Empty_Prog});
337 RootEq_erls = RootEq_erls and
338 rooteq_srls = rooteq_srls and
339 sqrt_isolate = sqrt_isolate and
340 l_sqrt_isolate = l_sqrt_isolate and
341 r_sqrt_isolate = r_sqrt_isolate and
342 rooteq_simplify = rooteq_simplify
344 subsection \<open>problems\<close>
346 problem pbl_equ_univ_root : "rootX/univariate/equation" =
347 \<open>RootEq_prls\<close>
348 CAS: "solve (e_e::bool, v_v)"
349 Given: "equality e_e" "solveFor v_v"
351 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
352 "(lhs e_e) is_rootTerm_in (v_v::real) |
353 (rhs e_e) is_rootTerm_in (v_v::real)"
354 Find: "solutions v_v'i'"
356 problem pbl_equ_univ_root_sq : "sq/rootX/univariate/equation" =
357 \<open>RootEq_prls\<close>
358 Method_Ref: "RootEq/solve_sq_root_equation"
359 CAS: "solve (e_e::bool, v_v)"
360 Given: "equality e_e" "solveFor v_v"
362 "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
363 ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |
364 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
365 ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"
366 Find: "solutions v_v'i'"
368 (* ---------normalise----------- *)
369 problem pbl_equ_univ_root_norm : "normalise/rootX/univariate/equation" =
370 \<open>RootEq_prls\<close>
371 Method_Ref: "RootEq/norm_sq_root_equation"
372 CAS: "solve (e_e::bool, v_v)"
373 Given: "equality e_e" "solveFor v_v"
375 "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
376 Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
377 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
378 Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
379 Find: "solutions v_v'i'"
381 subsection \<open>methods\<close>
383 method met_rooteq : "RootEq" =
384 \<open>{rew_ord="tless_true",rls'=Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
385 errpats = [], rew_rls = norm_Poly}\<close>
387 (*-- normalise 20.10.02 --*)
388 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
390 "norm_sqrt_equ e_e v_v = (
393 (Repeat(Try (Rewrite ''makex1_x''))) #>
394 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
395 (Try (Rewrite_Set ''rooteq_simplify'')) #>
396 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
397 (Try (Rewrite_Set ''rooteq_simplify''))
400 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
401 [BOOL e_e, REAL v_v])"
403 method met_rooteq_norm : "RootEq/norm_sq_root_equation" =
404 \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls=Rule_Set.empty, where_rls=RootEq_prls, calc =[],
405 errpats = [], rew_rls = norm_Poly}\<close>
406 Program: norm_sqrt_equ.simps
407 Given: "equality e_e" "solveFor v_v"
408 Where: "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
409 Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
410 ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
411 Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
412 Find: "solutions v_v'i'"
414 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
416 "solve_sqrt_equ e_e v_v =
419 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #>
420 (Try (Rewrite_Set ''rooteq_simplify'')) #>
421 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
422 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
423 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
425 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
427 SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])
430 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
431 [BOOL e_e, REAL v_v])
432 in Check_elementwise L_L {(v_v::real). Assumptions})"
434 method met_rooteq_sq : "RootEq/solve_sq_root_equation" =
435 \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls = rooteq_srls, where_rls = RootEq_prls, calc = [],
436 errpats = [], rew_rls = norm_Poly}\<close>
437 Program: solve_sqrt_equ.simps
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'"
445 (*-- right 28.08.02 --*)
446 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
448 "solve_sqrt_equ_right e_e v_v =
451 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
452 (Try (Rewrite_Set ''rooteq_simplify'')) #>
453 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
454 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
455 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
457 if (rhs e_e) is_sqrtTerm_in v_v
459 SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
462 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
463 [BOOL e_e, REAL v_v])"
465 method met_rooteq_sq_right : "RootEq/solve_right_sq_root_equation" =
466 \<open>{rew_ord = "termlessI", rls' = RootEq_erls, prog_rls = Rule_Set.empty, where_rls = RootEq_prls, calc = [],
467 errpats = [], rew_rls = norm_Poly}\<close>
468 Program: solve_sqrt_equ_right.simps
469 Given: "equality e_e" "solveFor v_v"
470 Where: "(rhs e_e) is_sqrtTerm_in v_v"
471 Find: "solutions v_v'i'"
473 (*-- left 28.08.02 --*)
474 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
476 "solve_sqrt_equ_left e_e v_v =
479 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
480 (Try (Rewrite_Set ''rooteq_simplify'')) #>
481 (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
482 (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
483 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
485 if (lhs e_e) is_sqrtTerm_in v_v
487 SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
490 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
491 [BOOL e_e, REAL v_v])"
493 method met_rooteq_sq_left : "RootEq/solve_left_sq_root_equation" =
494 \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls=Rule_Set.empty, where_rls=RootEq_prls, calc =[],
495 errpats = [], rew_rls = norm_Poly}\<close>
496 Program: solve_sqrt_equ_left.simps
497 Given: "equality e_e" "solveFor v_v"
498 Where: "(lhs e_e) is_sqrtTerm_in v_v"
499 Find: "solutions v_v'i'"