33 val b = str2term "Complex 3 4"; |
33 val b = str2term "Complex 3 4"; |
34 (*a + (b::complex); ERROR: term + term*) |
34 (*a + (b::complex); ERROR: term + term*) |
35 *} |
35 *} |
36 |
36 |
37 section {*use the operations for simplification*} |
37 section {*use the operations for simplification*} |
38 subsection {*example 1*} |
38 |
|
39 |
|
40 |
|
41 subsection {*example 1 -- ADD*} |
39 ML {* |
42 ML {* |
40 print_depth 1; |
43 print_depth 1; |
41 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
44 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
42 *} |
45 *} |
43 ML {* |
46 ML {* |
44 val thm = @{thm "complex_add"}; |
47 val thm = @{thm "complex_add"}; |
45 val t = str2term "Complex 1 2 + Complex 3 4"; |
48 val t = str2term "Complex 1 2 + Complex 3 4"; |
46 val SOME _ = rewrite_ thy ro er true thm t; |
49 val SOME _ = rewrite_ thy ro er true thm t; |
47 val SOME (t', _) = rewrite_ thy ro er true thm t; |
50 val SOME (t', _) = rewrite_ thy ro er true thm t; |
48 "Complex (1 + 3) (2 + 4)" = term2str t'; |
51 "Complex (1 + 3) (2 + 4)" = term2str t'; |
49 *} |
52 *} |
50 |
53 |
51 subsection {*example 2*} |
54 |
|
55 |
|
56 |
|
57 subsection {*example 2 -- ADD, MULT*} |
52 ML {* |
58 ML {* |
|
59 |
53 val Simplify_complex = append_rls "Simplify_complex" e_rls |
60 val Simplify_complex = append_rls "Simplify_complex" e_rls |
54 [ Thm ("complex_add",num_str @{thm complex_add}), |
61 [ Thm ("complex_add",num_str @{thm complex_add}), |
55 Thm ("complex_mult",num_str @{thm complex_mult}), |
62 Thm ("complex_mult",num_str @{thm complex_mult}), |
56 Rls_ norm_Poly |
63 Rls_ norm_Poly |
57 ]; |
64 ]; |
|
65 |
58 *} |
66 *} |
59 ML {* |
67 ML {* |
|
68 |
60 val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"; |
69 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)"; |
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)"; |
62 atomty t; |
95 atomty t; |
63 *} |
96 *} |
64 ML {* |
97 ML {* |
65 trace_rewrite := true; |
98 trace_rewrite := true; |
66 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t; |
99 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t; |
67 trace_rewrite := false; |
100 trace_rewrite := false; |
68 term2str t = "Complex -12 26"; |
101 term2str t = "Complex -12 26"; |
69 atomty t; |
102 atomty t; |
70 *} |
103 *} |
71 ML {* |
|
72 |
104 |
73 *} |
105 |
|
106 |
74 ML {* |
107 ML {* |
75 trace_rewrite := true; |
108 trace_rewrite := true; |
76 trace_rewrite := false; |
109 trace_rewrite := false; |
77 *} |
110 *} |
78 |
111 |