1.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy Tue Jul 26 09:53:53 2011 +0200
1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy Wed Jul 27 08:00:24 2011 +0200
1.3 @@ -2,7 +2,7 @@
1.4
1.5 section {*terms and operations*}
1.6 ML {*
1.7 -print_depth 999; @{term "Complex 1 (2::real)"};
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 @@ -35,31 +35,64 @@
1.13 *}
1.14
1.15 section {*use the operations for simplification*}
1.16 -subsection {*example 1*}
1.17 +
1.18 +
1.19 +
1.20 +subsection {*example 1 -- ADD*}
1.21 ML {*
1.22 -print_depth 1;
1.23 -val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.24 + print_depth 1;
1.25 + val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.26 *}
1.27 ML {*
1.28 -val thm = @{thm "complex_add"};
1.29 -val t = str2term "Complex 1 2 + Complex 3 4";
1.30 -val SOME _ = rewrite_ thy ro er true thm t;
1.31 -val SOME (t', _) = rewrite_ thy ro er true thm t;
1.32 -"Complex (1 + 3) (2 + 4)" = term2str t';
1.33 + val thm = @{thm "complex_add"};
1.34 + val t = str2term "Complex 1 2 + Complex 3 4";
1.35 + val SOME _ = rewrite_ thy ro er true thm t;
1.36 + val SOME (t', _) = rewrite_ thy ro er true thm t;
1.37 + "Complex (1 + 3) (2 + 4)" = term2str t';
1.38 *}
1.39
1.40 -subsection {*example 2*}
1.41 +
1.42 +
1.43 +
1.44 +subsection {*example 2 -- ADD, MULT*}
1.45 ML {*
1.46 +
1.47 val Simplify_complex = append_rls "Simplify_complex" e_rls
1.48 [ Thm ("complex_add",num_str @{thm complex_add}),
1.49 Thm ("complex_mult",num_str @{thm complex_mult}),
1.50 Rls_ norm_Poly
1.51 ];
1.52 +
1.53 *}
1.54 ML {*
1.55 +
1.56 val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
1.57 term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
1.58 atomty t;
1.59 +
1.60 +*}
1.61 +ML {*
1.62 +
1.63 +
1.64 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
1.65 +
1.66 +term2str t = "Complex -12 26";
1.67 +atomty t;
1.68 +
1.69 +*}
1.70 +
1.71 +subsection {*example 3*}
1.72 +ML {*
1.73 +val Simplify_complex = append_rls "Simplify_complex" e_rls
1.74 + [ Thm ("complex_mult",num_str @{thm complex_mult}),
1.75 + Thm ("complex_inverse",num_str @{thm complex_inverse}),
1.76 + Rls_ norm_Poly
1.77 + ];
1.78 +*}
1.79 +ML {*
1.80 +val t = str2term "inverse (Complex (2::real) (4::real))";
1.81 +term2str t = "inverse Complex (2) (4)";
1.82 +atomty t;
1.83 *}
1.84 ML {*
1.85 trace_rewrite := true;
1.86 @@ -68,9 +101,9 @@
1.87 term2str t = "Complex -12 26";
1.88 atomty t;
1.89 *}
1.90 -ML {*
1.91
1.92 -*}
1.93 +
1.94 +
1.95 ML {*
1.96 trace_rewrite := true;
1.97 trace_rewrite := false;
2.1 --- a/doc-src/isac/jrocnik/present-1.tex Tue Jul 26 09:53:53 2011 +0200
2.2 +++ b/doc-src/isac/jrocnik/present-1.tex Wed Jul 27 08:00:24 2011 +0200
2.3 @@ -306,7 +306,7 @@
2.4 \begin{tabbing}
2.5 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
2.6 \>given \>:\> Expression of z \\
2.7 -\> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
2.8 +\> \> \> \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\
2.9 \>precond \>:\> TODO\\
2.10 \>find \>:\> Expression of n\\
2.11 \> \> \> \>$h[n]$\\
2.12 @@ -388,7 +388,7 @@
2.13
2.14 \item Pre and Post conditions
2.15 \item Exact mathematic behind functions
2.16 -\item accurate mathematic notation
2.17 +\item Accurate mathematic notation
2.18
2.19 \end{itemize}
2.20 }