| author | wneuper <Walther.Neuper@jku.at> |
| Thu, 04 Aug 2022 12:48:37 +0200 | |
| changeset 60509 | 2e0b7ca391dc |
| parent 60385 | d3a3cc2f0382 |
| permissions | -rw-r--r-- |
| neuper@42318 | 1 |
(* Title: collecting all knowledge for Root and Rational |
| neuper@42318 | 2 |
Author: Richard Lang 02.10 last change by: rlang date: 02.10.20 |
| neuper@42318 | 3 |
(c) due to copyright terms |
| neuper@37906 | 4 |
*) |
| neuper@37906 | 5 |
|
| neuper@37954 | 6 |
theory RootRat imports Root Rational begin |
| neuper@37906 | 7 |
|
| wneuper@59472 | 8 |
ML \<open> |
| neuper@37954 | 9 |
val rootrat_erls = |
| walther@59852 | 10 |
Rule_Set.merge "rootrat_erls" Root_erls |
| walther@59852 | 11 |
(Rule_Set.merge "" rational_erls |
| walther@59852 | 12 |
(Rule_Set.append_rules "" Rule_Set.empty [])); |
| neuper@37954 | 13 |
|
| neuper@37954 | 14 |
(*.calculate numeral groundterms.*) |
| neuper@37954 | 15 |
val calculate_RootRat = |
| walther@60341 | 16 |
Rule_Set.append_rules "calculate_RootRat" calculate_Rational [ |
| walther@60341 | 17 |
\<^rule_thm>\<open>distrib_left\<close> (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *), |
| walther@60341 | 18 |
\<^rule_thm>\<open>mult_1_left\<close> (* 1 * z = z *), |
| walther@60385 | 19 |
\<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*), |
| walther@60341 | 20 |
\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")]; |
| s1210629013@55444 | 21 |
|
| walther@59618 | 22 |
val prep_rls' = Auto_Prog.prep_rls @{theory};
|
| wneuper@59472 | 23 |
\<close> |
| wenzelm@60289 | 24 |
rule_set_knowledge |
| wenzelm@60286 | 25 |
rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and |
| wenzelm@60286 | 26 |
calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close> |
| walther@60278 | 27 |
ML \<open> |
| walther@60278 | 28 |
\<close> ML \<open> |
| walther@60278 | 29 |
\<close> ML \<open> |
| walther@60278 | 30 |
\<close> |
| neuper@37906 | 31 |
end |