1 (* Title: collecting all knowledge for Root and Rational
2 Author: Richard Lang 02.10 last change by: rlang date: 02.10.20
3 (c) due to copyright terms
6 theory RootRat imports Root Rational begin
12 Rule_Set.merge "rootrat_erls" Root_erls
13 (Rule_Set.merge "" rational_erls
14 (Rule_Set.append_rules "" Rule_Set.empty []));
16 (*.calculate numeral groundterms.*)
17 val calculate_RootRat =
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational
19 [\<^rule_thm>\<open>distrib_left\<close>,
20 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
21 \<^rule_thm>\<open>mult_1_left\<close>,
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_")
28 val prep_rls' = Auto_Prog.prep_rls @{theory};
31 rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and
32 calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close>