|
agriesma@332
|
1 |
(* use"kbtest/complex.sml";
|
|
agriesma@332
|
2 |
*)
|
|
agriesma@332
|
3 |
|
|
agriesma@332
|
4 |
val t = str2term "I__";
|
|
agriesma@332
|
5 |
atomt t;
|
|
agriesma@332
|
6 |
val t = str2term "1 + 2 * I__";
|
|
agriesma@332
|
7 |
atomt t;
|
|
agriesma@332
|
8 |
val t = str2term "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
|
|
agriesma@332
|
9 |
atomt t;
|
|
agriesma@332
|
10 |
(*andere konkrete Syntax ???*)
|
|
agriesma@332
|
11 |
|
|
agriesma@332
|
12 |
val t = str2term "Float ((1,2),(0,0)) * I__";
|
|
agriesma@332
|
13 |
atomt t;
|
|
agriesma@332
|
14 |
term2str t;
|
|
agriesma@332
|
15 |
val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
|
|
agriesma@332
|
16 |
atomt t;
|
|
agriesma@332
|
17 |
term2str t;
|
|
agriesma@332
|
18 |
|
|
agriesma@332
|
19 |
(*--- (1.1 + 2.2 I) * (3.3 + 4.4 I) = - 6.05 + 12 I ---*)
|
|
agriesma@332
|
20 |
val t = str2term "(Float ((11,-1),(0,0)) + Float ((22,-1),(0,0)) * I__) *\
|
|
agriesma@332
|
21 |
\(Float ((33,-1),(0,0)) + Float ((44,-1),(0,0)) * I__)";
|
|
agriesma@332
|
22 |
val Some (t',_) =
|
|
agriesma@332
|
23 |
rewrite_set_ thy false
|
|
agriesma@332
|
24 |
(append_rls "simpl_complex" make_polynomial
|
|
agriesma@332
|
25 |
[Thm ("square_I", num_str square_I)]) t;
|
|
agriesma@332
|
26 |
term2str t';
|
|
agriesma@332
|
27 |
"Float ((363, -2), 0, 0) + I__ * Float ((484, -2), 0, 0) +\
|
|
agriesma@332
|
28 |
\I__ * Float ((726, -2), 0, 0) + -1 * Float ((968, -2), 0, 0)"
|
|
agriesma@332
|
29 |
(*--- mit dem rls make_polynomial geht ja schon allerhand !!!---*) |