neuper@37871
|
1 |
(*.(c) by Richard Lang, 2003 .*)
|
neuper@37871
|
2 |
(* collecting all knowledge for Root and Rational
|
neuper@37871
|
3 |
created by: rlang
|
neuper@37871
|
4 |
date: 02.10
|
neuper@37871
|
5 |
changed by: rlang
|
neuper@37871
|
6 |
last change by: rlang
|
neuper@37871
|
7 |
date: 02.10.21
|
neuper@37871
|
8 |
*)
|
neuper@37871
|
9 |
(* use"knowledge/RootRat.ML";
|
neuper@37871
|
10 |
use"RootRat.ML";
|
neuper@37871
|
11 |
|
neuper@37871
|
12 |
use"ROOT.ML";
|
neuper@37871
|
13 |
cd"knowledge";
|
neuper@37871
|
14 |
|
neuper@37871
|
15 |
remove_thy"RootRat";
|
neuper@37871
|
16 |
use_thy"Isac";
|
neuper@37871
|
17 |
*)
|
neuper@37871
|
18 |
|
neuper@37871
|
19 |
"******* RootRat.ML begin *******";
|
neuper@37871
|
20 |
theory' := overwritel (!theory', [("RootRat.thy",RootRat.thy)]);
|
neuper@37871
|
21 |
|
neuper@37871
|
22 |
(*-------------------------functions---------------------*)
|
neuper@37871
|
23 |
|
neuper@37871
|
24 |
(*-------------------------rulse-------------------------*)
|
neuper@37871
|
25 |
val rootrat_erls =
|
neuper@37871
|
26 |
merge_rls "rootrat_erls" Root_erls
|
neuper@37871
|
27 |
(merge_rls "" rational_erls
|
neuper@37871
|
28 |
(append_rls "" e_rls
|
neuper@37871
|
29 |
[]));
|
neuper@37871
|
30 |
|
neuper@37871
|
31 |
ruleset' := overwritelthy thy (!ruleset',
|
neuper@37871
|
32 |
[("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)
|
neuper@37871
|
33 |
]);
|
neuper@37871
|
34 |
|
neuper@37871
|
35 |
(*.calculate numeral groundterms.*)
|
neuper@37871
|
36 |
val calculate_RootRat =
|
neuper@37871
|
37 |
append_rls "calculate_RootRat" calculate_Rational
|
neuper@37871
|
38 |
[Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
|
neuper@37871
|
39 |
(* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
|
neuper@37871
|
40 |
Thm ("real_mult_1",num_str real_mult_1),
|
neuper@37871
|
41 |
(* 1 * z = z *)
|
neuper@37871
|
42 |
Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),
|
neuper@37871
|
43 |
(* "- z1 = -1 * z1" *)
|
neuper@37871
|
44 |
Calc ("Root.sqrt",eval_sqrt "#sqrt_")
|
neuper@37871
|
45 |
];
|
neuper@37871
|
46 |
ruleset' := overwritelthy thy (!ruleset',
|
neuper@37871
|
47 |
[("calculate_RootRat",calculate_RootRat)]);
|
neuper@37871
|
48 |
|
neuper@37871
|
49 |
|
neuper@37871
|
50 |
"******* RootRat.ML end *******";
|