neuper@42164
|
1 |
theory Test_Complex imports Isac begin
|
neuper@42164
|
2 |
|
neuper@42164
|
3 |
section {*terms and operations*}
|
neuper@42160
|
4 |
ML {*
|
jan@42207
|
5 |
print_depth 999; @{term "Complex 1 (2::real)"};
|
neuper@42160
|
6 |
*}
|
neuper@42160
|
7 |
ML {*
|
neuper@42160
|
8 |
@{term "Complex 1 2 + Complex 3 4"};
|
neuper@42185
|
9 |
print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
|
neuper@42185
|
10 |
*}
|
neuper@42185
|
11 |
ML {*
|
neuper@42160
|
12 |
@{term "Complex 1 2 * Complex 3 4"};
|
neuper@42160
|
13 |
@{term "Complex 1 2 - Complex 3 4"};
|
neuper@42160
|
14 |
@{term "Complex 1 2 / Complex 3 4"};
|
neuper@42164
|
15 |
(*@{term "Complex 1 2 ^ Complex 3 4"};
|
neuper@42164
|
16 |
Type unification failed: Clash of types "complex" and "nat"
|
neuper@42164
|
17 |
Operator: op ^ (Complex 1 2) :: nat \<Rightarrow> complex
|
neuper@42164
|
18 |
Operand: Complex 3 4 :: complex*)
|
neuper@42160
|
19 |
*}
|
neuper@42160
|
20 |
ML {*
|
neuper@42164
|
21 |
term2str @{term "Complex 1 2 + Complex 3 4"};
|
neuper@42164
|
22 |
term2str @{term "Complex 1 2 / Complex 3 4"};
|
neuper@42164
|
23 |
*}
|
neuper@42164
|
24 |
|
neuper@42164
|
25 |
ML {*
|
neuper@42160
|
26 |
val a = @{term "Complex 1 2"};
|
neuper@42185
|
27 |
atomty a;
|
neuper@42185
|
28 |
val a = str2term "Complex 1 2";
|
neuper@42185
|
29 |
atomty a;
|
neuper@42185
|
30 |
*}
|
neuper@42185
|
31 |
ML {*
|
neuper@42160
|
32 |
val b = @{term "Complex 3 4"};
|
neuper@42185
|
33 |
val b = str2term "Complex 3 4";
|
neuper@42160
|
34 |
(*a + (b::complex); ERROR: term + term*)
|
neuper@42160
|
35 |
*}
|
neuper@42164
|
36 |
|
neuper@42164
|
37 |
section {*use the operations for simplification*}
|
jan@42207
|
38 |
|
jan@42207
|
39 |
|
jan@42207
|
40 |
|
jan@42207
|
41 |
subsection {*example 1 -- ADD*}
|
neuper@42160
|
42 |
ML {*
|
jan@42207
|
43 |
print_depth 1;
|
jan@42207
|
44 |
val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
|
neuper@42160
|
45 |
*}
|
neuper@42160
|
46 |
ML {*
|
jan@42207
|
47 |
val thm = @{thm "complex_add"};
|
jan@42207
|
48 |
val t = str2term "Complex 1 2 + Complex 3 4";
|
jan@42207
|
49 |
val SOME _ = rewrite_ thy ro er true thm t;
|
jan@42207
|
50 |
val SOME (t', _) = rewrite_ thy ro er true thm t;
|
jan@42207
|
51 |
"Complex (1 + 3) (2 + 4)" = term2str t';
|
neuper@42164
|
52 |
*}
|
neuper@42164
|
53 |
|
jan@42207
|
54 |
|
jan@42207
|
55 |
|
jan@42207
|
56 |
|
jan@42207
|
57 |
subsection {*example 2 -- ADD, MULT*}
|
neuper@42164
|
58 |
ML {*
|
jan@42207
|
59 |
|
neuper@42185
|
60 |
val Simplify_complex = append_rls "Simplify_complex" e_rls
|
neuper@42164
|
61 |
[ Thm ("complex_add",num_str @{thm complex_add}),
|
neuper@42185
|
62 |
Thm ("complex_mult",num_str @{thm complex_mult}),
|
neuper@42185
|
63 |
Rls_ norm_Poly
|
neuper@42164
|
64 |
];
|
jan@42207
|
65 |
|
neuper@42164
|
66 |
*}
|
neuper@42164
|
67 |
ML {*
|
jan@42207
|
68 |
|
neuper@42185
|
69 |
val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
|
neuper@42185
|
70 |
term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
|
neuper@42185
|
71 |
atomty t;
|
jan@42207
|
72 |
|
jan@42207
|
73 |
*}
|
jan@42207
|
74 |
ML {*
|
jan@42207
|
75 |
|
jan@42207
|
76 |
|
jan@42207
|
77 |
val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
|
jan@42207
|
78 |
|
jan@42207
|
79 |
term2str t = "Complex -12 26";
|
jan@42207
|
80 |
atomty t;
|
jan@42207
|
81 |
|
jan@42207
|
82 |
*}
|
jan@42207
|
83 |
|
jan@42207
|
84 |
subsection {*example 3*}
|
jan@42207
|
85 |
ML {*
|
jan@42207
|
86 |
val Simplify_complex = append_rls "Simplify_complex" e_rls
|
jan@42207
|
87 |
[ Thm ("complex_mult",num_str @{thm complex_mult}),
|
jan@42207
|
88 |
Thm ("complex_inverse",num_str @{thm complex_inverse}),
|
jan@42207
|
89 |
Rls_ norm_Poly
|
jan@42207
|
90 |
];
|
jan@42207
|
91 |
*}
|
jan@42207
|
92 |
ML {*
|
jan@42207
|
93 |
val t = str2term "inverse (Complex (2::real) (4::real))";
|
jan@42207
|
94 |
term2str t = "inverse Complex (2) (4)";
|
jan@42207
|
95 |
atomty t;
|
neuper@42164
|
96 |
*}
|
neuper@42164
|
97 |
ML {*
|
neuper@42185
|
98 |
trace_rewrite := true;
|
neuper@42164
|
99 |
val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
|
neuper@42185
|
100 |
trace_rewrite := false;
|
neuper@42185
|
101 |
term2str t = "Complex -12 26";
|
neuper@42185
|
102 |
atomty t;
|
neuper@42164
|
103 |
*}
|
neuper@42185
|
104 |
|
jan@42207
|
105 |
|
jan@42207
|
106 |
|
neuper@42164
|
107 |
ML {*
|
neuper@42185
|
108 |
trace_rewrite := true;
|
neuper@42185
|
109 |
trace_rewrite := false;
|
neuper@42160
|
110 |
*}
|
neuper@42160
|
111 |
|
neuper@42160
|
112 |
end
|
neuper@42160
|
113 |
|