221 (* sqrt (a \<up> 2) -> a *) |
221 (* sqrt (a \<up> 2) -> a *) |
222 \<^rule_thm>\<open>sqrt_times_root_1\<close>, |
222 \<^rule_thm>\<open>sqrt_times_root_1\<close>, |
223 (* sqrt a sqrt b -> sqrt(ab) *) |
223 (* sqrt a sqrt b -> sqrt(ab) *) |
224 \<^rule_thm>\<open>sqrt_times_root_2\<close>, |
224 \<^rule_thm>\<open>sqrt_times_root_2\<close>, |
225 (* a sqrt b sqrt c -> a sqrt(bc) *) |
225 (* a sqrt b sqrt c -> a sqrt(bc) *) |
226 Rule.Thm("sqrt_square_equation_both_1", |
226 \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>, |
227 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}), |
|
228 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> |
227 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> |
229 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
228 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
230 Rule.Thm("sqrt_square_equation_both_2", |
229 \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>, |
231 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}), |
|
232 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> |
230 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> |
233 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
231 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
234 Rule.Thm("sqrt_square_equation_both_3", |
232 \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>, |
235 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}), |
|
236 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> |
233 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> |
237 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
234 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
238 Rule.Thm("sqrt_square_equation_both_4", |
235 \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>, |
239 ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}), |
|
240 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> |
236 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> |
241 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
237 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
242 Rule.Thm("sqrt_isolate_l_add1", |
238 \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, |
243 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}), |
|
244 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
239 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
245 Rule.Thm("sqrt_isolate_l_add2", |
240 \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, |
246 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}), |
|
247 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
241 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
248 Rule.Thm("sqrt_isolate_l_add3", |
242 \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, |
249 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}), |
|
250 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
243 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
251 Rule.Thm("sqrt_isolate_l_add4", |
244 \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, |
252 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}), |
|
253 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
245 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
254 Rule.Thm("sqrt_isolate_l_add5", |
246 \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, |
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 *) |
247 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) |
257 Rule.Thm("sqrt_isolate_l_add6", |
248 \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, |
258 ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}), |
|
259 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
249 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
260 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*) |
250 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*) |
261 (* b*sqrt(x) = d sqrt(x) d/b *) |
251 (* b*sqrt(x) = d sqrt(x) d/b *) |
262 Rule.Thm("sqrt_isolate_r_add1", |
252 \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, |
263 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}), |
|
264 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
253 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
265 Rule.Thm("sqrt_isolate_r_add2", |
254 \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, |
266 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}), |
|
267 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
255 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
268 Rule.Thm("sqrt_isolate_r_add3", |
256 \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, |
269 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}), |
|
270 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
257 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
271 Rule.Thm("sqrt_isolate_r_add4", |
258 \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, |
272 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}), |
|
273 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
259 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
274 Rule.Thm("sqrt_isolate_r_add5", |
260 \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, |
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)*) |
261 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) |
277 Rule.Thm("sqrt_isolate_r_add6", |
262 \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, |
278 ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}), |
|
279 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
263 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
280 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*) |
264 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*) |
281 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
265 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
282 Rule.Thm("sqrt_square_equation_left_1", |
266 \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, |
283 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}), |
|
284 (* sqrt(x)=b -> x=b^2 *) |
267 (* sqrt(x)=b -> x=b^2 *) |
285 Rule.Thm("sqrt_square_equation_left_2", |
268 \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, |
286 ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}), |
|
287 (* c*sqrt(x)=b -> c^2*x=b^2 *) |
269 (* c*sqrt(x)=b -> c^2*x=b^2 *) |
288 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, |
270 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, |
289 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
271 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
290 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, |
272 \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, |
291 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
273 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |