4 ML {* |
4 ML {* |
5 print_depth 999; @{term "Complex 1 (2::real)"}; |
5 print_depth 999; @{term "Complex 1 (2::real)"}; |
6 *} |
6 *} |
7 ML {* |
7 ML {* |
8 @{term "Complex 1 2 + Complex 3 4"}; |
8 @{term "Complex 1 2 + Complex 3 4"}; |
|
9 print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999; |
|
10 *} |
|
11 ML {* |
9 @{term "Complex 1 2 * Complex 3 4"}; |
12 @{term "Complex 1 2 * Complex 3 4"}; |
10 @{term "Complex 1 2 - Complex 3 4"}; |
13 @{term "Complex 1 2 - Complex 3 4"}; |
11 @{term "Complex 1 2 / Complex 3 4"}; |
14 @{term "Complex 1 2 / Complex 3 4"}; |
12 (*@{term "Complex 1 2 ^ Complex 3 4"}; |
15 (*@{term "Complex 1 2 ^ Complex 3 4"}; |
13 Type unification failed: Clash of types "complex" and "nat" |
16 Type unification failed: Clash of types "complex" and "nat" |
19 term2str @{term "Complex 1 2 / Complex 3 4"}; |
22 term2str @{term "Complex 1 2 / Complex 3 4"}; |
20 *} |
23 *} |
21 |
24 |
22 ML {* |
25 ML {* |
23 val a = @{term "Complex 1 2"}; |
26 val a = @{term "Complex 1 2"}; |
|
27 atomty a; |
|
28 val a = str2term "Complex 1 2"; |
|
29 atomty a; |
|
30 *} |
|
31 ML {* |
24 val b = @{term "Complex 3 4"}; |
32 val b = @{term "Complex 3 4"}; |
|
33 val b = str2term "Complex 3 4"; |
25 (*a + (b::complex); ERROR: term + term*) |
34 (*a + (b::complex); ERROR: term + term*) |
26 *} |
35 *} |
27 |
36 |
28 section {*use the operations for simplification*} |
37 section {*use the operations for simplification*} |
29 subsection {*example 1*} |
38 subsection {*example 1*} |
31 print_depth 1; |
40 print_depth 1; |
32 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
41 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
33 *} |
42 *} |
34 ML {* |
43 ML {* |
35 val thm = @{thm "complex_add"}; |
44 val thm = @{thm "complex_add"}; |
36 val t = @{term "Complex 1 2 + Complex 3 4"}; |
45 val t = str2term "Complex 1 2 + Complex 3 4"; |
37 val SOME _ = rewrite_ thy ro er true thm t; |
46 val SOME _ = rewrite_ thy ro er true thm t; |
38 val SOME (t', _) = rewrite_ thy ro er true thm t; |
47 val SOME (t', _) = rewrite_ thy ro er true thm t; |
39 "Complex (1 + 3) (2 + 4)" = term2str t'; |
48 "Complex (1 + 3) (2 + 4)" = term2str t'; |
40 *} |
49 *} |
41 |
50 |
42 subsection {*example 2*} |
51 subsection {*example 2*} |
43 ML {* |
52 ML {* |
44 val Simplify_complex = append_rls "Simplify_complex" norm_Poly |
53 val Simplify_complex = append_rls "Simplify_complex" e_rls |
45 [ Thm ("complex_add",num_str @{thm complex_add}), |
54 [ Thm ("complex_add",num_str @{thm complex_add}), |
46 Thm ("complex_mult",num_str @{thm complex_mult}) |
55 Thm ("complex_mult",num_str @{thm complex_mult}), |
|
56 Rls_ norm_Poly |
47 ]; |
57 ]; |
48 *} |
58 *} |
49 ML {* |
59 ML {* |
50 val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"}; |
60 val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"; |
|
61 term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)"; |
|
62 atomty t; |
51 *} |
63 *} |
52 ML {* |
64 ML {* |
|
65 trace_rewrite := true; |
53 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t; |
66 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t; |
|
67 trace_rewrite := false; |
|
68 term2str t = "Complex -12 26"; |
|
69 atomty t; |
54 *} |
70 *} |
55 ML {* |
71 ML {* |
56 term2str t |
72 |
57 *} |
73 *} |
58 ML {* |
74 ML {* |
|
75 trace_rewrite := true; |
|
76 trace_rewrite := false; |
59 *} |
77 *} |
60 |
78 |
61 end |
79 end |
62 |
80 |