1 theory Test_Complex imports Isac begin
3 section {*terms and operations*}
5 print_depth 999; @{term "Complex 1 (2::real)"};
8 @{term "Complex 1 2 + Complex 3 4"};
9 @{term "Complex 1 2 * Complex 3 4"};
10 @{term "Complex 1 2 - Complex 3 4"};
11 @{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*)
18 term2str @{term "Complex 1 2 + Complex 3 4"};
19 term2str @{term "Complex 1 2 / Complex 3 4"};
23 val a = @{term "Complex 1 2"};
24 val b = @{term "Complex 3 4"};
25 (*a + (b::complex); ERROR: term + term*)
28 section {*use the operations for simplification*}
29 subsection {*example 1*}
32 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
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';
42 subsection {*example 2*}
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})
50 val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
53 val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;