13 (Rule_Set.merge "" rational_erls |
13 (Rule_Set.merge "" rational_erls |
14 (Rule_Set.append_rules "" Rule_Set.empty [])); |
14 (Rule_Set.append_rules "" Rule_Set.empty [])); |
15 |
15 |
16 (*.calculate numeral groundterms.*) |
16 (*.calculate numeral groundterms.*) |
17 val calculate_RootRat = |
17 val calculate_RootRat = |
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational |
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational [ |
19 [\<^rule_thm>\<open>distrib_left\<close>, |
19 \<^rule_thm>\<open>distrib_left\<close> (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *), |
20 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) |
20 \<^rule_thm>\<open>mult_1_left\<close> (* 1 * z = z *), |
21 \<^rule_thm>\<open>mult_1_left\<close>, |
21 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*), |
22 (* 1 * z = z *) |
22 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")]; |
23 Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})), |
|
24 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*) |
|
25 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_") |
|
26 ]; |
|
27 |
23 |
28 val prep_rls' = Auto_Prog.prep_rls @{theory}; |
24 val prep_rls' = Auto_Prog.prep_rls @{theory}; |
29 \<close> |
25 \<close> |
30 rule_set_knowledge |
26 rule_set_knowledge |
31 rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and |
27 rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and |