1.1 --- a/src/Doc/isac/jrocnik/Test_Complex.thy Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,113 +0,0 @@
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 -