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