1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/Test_Complex.thy Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,113 @@
1.4 +theory Test_Complex imports Isac begin
1.5 +
1.6 +section {*terms and operations*}
1.7 +ML {*
1.8 + print_depth 999; @{term "Complex 1 (2::real)"};
1.9 +*}
1.10 +ML {*
1.11 +@{term "Complex 1 2 + Complex 3 4"};
1.12 +print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
1.13 +*}
1.14 +ML {*
1.15 +@{term "Complex 1 2 * Complex 3 4"};
1.16 +@{term "Complex 1 2 - Complex 3 4"};
1.17 +@{term "Complex 1 2 / Complex 3 4"};
1.18 +(*@{term "Complex 1 2 ^ Complex 3 4"};
1.19 + Type unification failed: Clash of types "complex" and "nat"
1.20 + Operator: op ^ (Complex 1 2) :: nat \<Rightarrow> complex
1.21 + Operand: Complex 3 4 :: complex*)
1.22 +*}
1.23 +ML {*
1.24 +term2str @{term "Complex 1 2 + Complex 3 4"};
1.25 +term2str @{term "Complex 1 2 / Complex 3 4"};
1.26 +*}
1.27 +
1.28 +ML {*
1.29 +val a = @{term "Complex 1 2"};
1.30 +atomty a;
1.31 +val a = str2term "Complex 1 2";
1.32 +atomty a;
1.33 +*}
1.34 +ML {*
1.35 +val b = @{term "Complex 3 4"};
1.36 +val b = str2term "Complex 3 4";
1.37 +(*a + (b::complex); ERROR: term + term*)
1.38 +*}
1.39 +
1.40 +section {*use the operations for simplification*}
1.41 +
1.42 +
1.43 +
1.44 +subsection {*example 1 -- ADD*}
1.45 +ML {*
1.46 + print_depth 1;
1.47 + val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.48 +*}
1.49 +ML {*
1.50 + val thm = @{thm "complex_add"};
1.51 + val t = str2term "Complex 1 2 + Complex 3 4";
1.52 + val SOME _ = rewrite_ thy ro er true thm t;
1.53 + val SOME (t', _) = rewrite_ thy ro er true thm t;
1.54 + "Complex (1 + 3) (2 + 4)" = term2str t';
1.55 +*}
1.56 +
1.57 +
1.58 +
1.59 +
1.60 +subsection {*example 2 -- ADD, MULT*}
1.61 +ML {*
1.62 +
1.63 +val Simplify_complex = append_rls "Simplify_complex" e_rls
1.64 + [ Thm ("complex_add",num_str @{thm complex_add}),
1.65 + Thm ("complex_mult",num_str @{thm complex_mult}),
1.66 + Rls_ norm_Poly
1.67 + ];
1.68 +
1.69 +*}
1.70 +ML {*
1.71 +
1.72 +val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
1.73 +term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
1.74 +atomty t;
1.75 +
1.76 +*}
1.77 +ML {*
1.78 +
1.79 +
1.80 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
1.81 +
1.82 +term2str t = "Complex -12 26";
1.83 +atomty t;
1.84 +
1.85 +*}
1.86 +
1.87 +subsection {*example 3*}
1.88 +ML {*
1.89 +val Simplify_complex = append_rls "Simplify_complex" e_rls
1.90 + [ Thm ("complex_mult",num_str @{thm complex_mult}),
1.91 + Thm ("complex_inverse",num_str @{thm complex_inverse}),
1.92 + Rls_ norm_Poly
1.93 + ];
1.94 +*}
1.95 +ML {*
1.96 +val t = str2term "inverse (Complex (2::real) (4::real))";
1.97 +term2str t = "inverse Complex (2) (4)";
1.98 +atomty t;
1.99 +*}
1.100 +ML {*
1.101 +trace_rewrite := true;
1.102 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
1.103 +trace_rewrite := false;
1.104 +term2str t = "Complex -12 26";
1.105 +atomty t;
1.106 +*}
1.107 +
1.108 +
1.109 +
1.110 +ML {*
1.111 +trace_rewrite := true;
1.112 +trace_rewrite := false;
1.113 +*}
1.114 +
1.115 +end
1.116 +