1 (* theory Test_Complex imports Isac begin |
1 theory Test_Complex imports Isac begin |
2 ERROR TODO ^^^^: |
2 |
|
3 section {*terms and operations*} |
3 ML {* |
4 ML {* |
4 @{term "Complex 1 2 ^ Complex 3 4"}; |
5 print_depth 999; @{term "Complex 1 (2::real)"}; |
5 *} |
6 *} |
6 Type unification failed: Clash of types "complex" and "nat" |
|
7 Operator: op ^ (Complex 1 2) :: nat \<Rightarrow> complex |
|
8 Operand: Complex 3 4 :: complex |
|
9 *) |
|
10 |
|
11 theory Test_Complex imports Main begin |
|
12 |
|
13 ML {* |
7 ML {* |
14 @{term "Complex 1 2"}; |
|
15 @{term "Complex 1 2 + Complex 3 4"}; |
8 @{term "Complex 1 2 + Complex 3 4"}; |
16 @{term "Complex 1 2 * Complex 3 4"}; |
9 @{term "Complex 1 2 * Complex 3 4"}; |
17 @{term "Complex 1 2 - Complex 3 4"}; |
10 @{term "Complex 1 2 - Complex 3 4"}; |
18 @{term "Complex 1 2 / Complex 3 4"}; |
11 @{term "Complex 1 2 / Complex 3 4"}; |
19 @{term "Complex 1 2 ^ Complex 3 4"}; |
12 (*@{term "Complex 1 2 ^ Complex 3 4"}; |
|
13 Type unification failed: Clash of types "complex" and "nat" |
|
14 Operator: op ^ (Complex 1 2) :: nat \<Rightarrow> complex |
|
15 Operand: Complex 3 4 :: complex*) |
20 *} |
16 *} |
|
17 ML {* |
|
18 term2str @{term "Complex 1 2 + Complex 3 4"}; |
|
19 term2str @{term "Complex 1 2 / Complex 3 4"}; |
|
20 *} |
|
21 |
21 ML {* |
22 ML {* |
22 val a = @{term "Complex 1 2"}; |
23 val a = @{term "Complex 1 2"}; |
23 val b = @{term "Complex 3 4"}; |
24 val b = @{term "Complex 3 4"}; |
24 (*a + (b::complex); ERROR: term + term*) |
25 (*a + (b::complex); ERROR: term + term*) |
25 *} |
26 *} |
|
27 |
|
28 section {*use the operations for simplification*} |
|
29 subsection {*example 1*} |
26 ML {* |
30 ML {* |
27 @{term "let a = Complex 1 2; b = Complex 3 4 in a + b"}; |
31 print_depth 1; |
|
32 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
28 *} |
33 *} |
29 ML {* |
34 ML {* |
30 (*TODO rules for simplification*) |
35 val thm = @{thm "complex_add"}; |
|
36 val t = @{term "Complex 1 2 + Complex 3 4"}; |
|
37 val SOME _ = rewrite_ thy ro er true thm t; |
|
38 val SOME (t', _) = rewrite_ thy ro er true thm t; |
|
39 "Complex (1 + 3) (2 + 4)" = term2str t'; |
|
40 *} |
|
41 |
|
42 subsection {*example 2*} |
|
43 ML {* |
|
44 val Simplify_complex = append_rls "Simplify_complex" norm_Poly |
|
45 [ Thm ("complex_add",num_str @{thm complex_add}), |
|
46 Thm ("complex_mult",num_str @{thm complex_mult}) |
|
47 ]; |
|
48 *} |
|
49 ML {* |
|
50 val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"}; |
|
51 *} |
|
52 ML {* |
|
53 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t; |
|
54 *} |
|
55 ML {* |
|
56 term2str t |
|
57 *} |
|
58 ML {* |
31 *} |
59 *} |
32 |
60 |
33 end |
61 end |
34 |
62 |