|
wneuper@672
|
1 |
(* tests on simplification
|
|
wneuper@672
|
2 |
author: Walther Neuper
|
|
wneuper@672
|
3 |
061019
|
|
wneuper@672
|
4 |
(c) due to copyright terms
|
|
wneuper@672
|
5 |
|
|
wneuper@672
|
6 |
use"../smltest/IsacKnowledge/simplify.sml";
|
|
wneuper@672
|
7 |
use"simplify.sml";
|
|
wneuper@672
|
8 |
*)
|
|
wneuper@672
|
9 |
val thy = Simplify.thy;
|
|
wneuper@672
|
10 |
|
|
wneuper@672
|
11 |
"-----------------------------------------------------------------";
|
|
wneuper@672
|
12 |
"table of contents -----------------------------------------------";
|
|
wneuper@672
|
13 |
"-----------------------------------------------------------------";
|
|
wneuper@672
|
14 |
"----------- CAS-command Simplify --------------------------------";
|
|
wneuper@682
|
15 |
"----------- append inform with final result ---------------------";
|
|
wneuper@672
|
16 |
"-----------------------------------------------------------------";
|
|
wneuper@672
|
17 |
"-----------------------------------------------------------------";
|
|
wneuper@672
|
18 |
"-----------------------------------------------------------------";
|
|
wneuper@672
|
19 |
|
|
wneuper@672
|
20 |
|
|
wneuper@672
|
21 |
|
|
wneuper@672
|
22 |
"----------- CAS-command Simplify --------------------------------";
|
|
wneuper@672
|
23 |
"----------- CAS-command Simplify --------------------------------";
|
|
wneuper@672
|
24 |
"----------- CAS-command Simplify --------------------------------";
|
|
wneuper@672
|
25 |
states:=[];
|
|
wneuper@672
|
26 |
CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
|
|
wneuper@672
|
27 |
Iterator 1;
|
|
wneuper@672
|
28 |
moveActiveRoot 1;
|
|
wneuper@672
|
29 |
replaceFormula 1 "Simplify (2*a + 3*a)";
|
|
wneuper@672
|
30 |
autoCalculate 1 CompleteCalc;
|
|
wneuper@672
|
31 |
val ((pt,p),_) = get_calc 1;
|
|
wneuper@672
|
32 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
wneuper@672
|
33 |
show_pt pt;
|
|
wneuper@672
|
34 |
if p = ([], Res) andalso term2str res = "5 * a" then ()
|
|
wneuper@672
|
35 |
else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
|
|
wneuper@672
|
36 |
|
|
wneuper@672
|
37 |
|
|
wneuper@682
|
38 |
"----------- append inform with final result ---------------------";
|
|
wneuper@682
|
39 |
"----------- append inform with final result ---------------------";
|
|
wneuper@682
|
40 |
"----------- append inform with final result ---------------------";
|
|
wneuper@682
|
41 |
states:=[];
|
|
wneuper@682
|
42 |
CalcTree [(["term ((14 * x * y) / ( x * y ))", "normalform N"],
|
|
wneuper@682
|
43 |
("Rational.thy",["rational","simplification"],
|
|
wneuper@682
|
44 |
["simplification","of_rationals"]))];
|
|
wneuper@682
|
45 |
Iterator 1;
|
|
wneuper@682
|
46 |
moveActiveRoot 1;
|
|
wneuper@682
|
47 |
autoCalculate 1 CompleteCalcHead;
|
|
wneuper@682
|
48 |
autoCalculate 1 (Step 1);
|
|
wneuper@682
|
49 |
appendFormula 1 "14";
|
|
wneuper@682
|
50 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
wneuper@672
|
51 |
|
|
wneuper@682
|
52 |
autoCalculate 1 (Step 1);
|
|
wneuper@682
|
53 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
wneuper@682
|
54 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
wneuper@682
|
55 |
if p = ([], Res) andalso term2str res = "14" then ()
|
|
wneuper@682
|
56 |
else raise error "simplify.sml: append inform with final result ?!?";
|