|
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@37972
|
9 |
val thy = @{theory};
|
|
neuper@37972
|
10 |
|
|
neuper@37954
|
11 |
val rootrat_erls =
|
|
walther@59850
|
12 |
Rule_Set.merge_rls "rootrat_erls" Root_erls
|
|
walther@59850
|
13 |
(Rule_Set.merge_rls "" rational_erls
|
|
walther@59850
|
14 |
(Rule_Set.append_rls "" Rule_Set.e_rls []));
|
|
neuper@37954
|
15 |
|
|
neuper@37954
|
16 |
(*.calculate numeral groundterms.*)
|
|
neuper@37954
|
17 |
val calculate_RootRat =
|
|
walther@59850
|
18 |
Rule_Set.append_rls "calculate_RootRat" calculate_Rational
|
|
wneuper@59416
|
19 |
[Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
|
|
neuper@42318
|
20 |
(* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
|
|
wneuper@59416
|
21 |
Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
|
|
neuper@42318
|
22 |
(* 1 * z = z *)
|
|
wneuper@59416
|
23 |
Rule.Thm ("sym_real_mult_minus1",TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
|
|
neuper@42318
|
24 |
(* "- z1 = -1 * z1" *)
|
|
walther@59773
|
25 |
Rule.Num_Calc ("NthRoot.sqrt", eval_sqrt "#sqrt_")
|
|
neuper@42318
|
26 |
];
|
|
s1210629013@55444
|
27 |
|
|
walther@59618
|
28 |
val prep_rls' = Auto_Prog.prep_rls @{theory};
|
|
wneuper@59472
|
29 |
\<close>
|
|
wneuper@59472
|
30 |
setup \<open>KEStore_Elems.add_rlss
|
|
s1210629013@55444
|
31 |
[("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)),
|
|
wneuper@59472
|
32 |
("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))]\<close>
|
|
neuper@37906
|
33 |
|
|
neuper@37906
|
34 |
end
|