316 id = "rooteq_simplify", preconds = [], rew_ord = ("termlessI",termlessI), |
316 id = "rooteq_simplify", preconds = [], rew_ord = ("termlessI",termlessI), |
317 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
317 erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
318 rules = [ |
318 rules = [ |
319 \<^rule_thm>\<open>real_assoc_1\<close>, (* a+(b+c) = a+b+c *) |
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 *) |
320 \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *) |
321 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
321 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
322 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
322 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
323 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
323 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
324 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
324 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
325 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
325 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
326 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
326 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
327 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
327 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
328 \<^rule_thm>\<open>real_minus_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*) |
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) *) |
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) *) |
331 \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a * sqrt a * sqrt b = a * sqrt(a*b) *) |