1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Feb 13 17:40:30 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Feb 14 22:55:03 2012 +0100
1.3 @@ -9,43 +9,51 @@
1.4
1.5 begin
1.6
1.7 -text{* We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise.
1.8 - Because subsection "Stepwise Check the Program" requires
1.9 - \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed
1.10 - from "theory Inverse_Z_Transform imports Isac begin.." to the above.
1.11 +text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
1.12 + exercise. Because subsection~\ref{sec:stepcheck} requires
1.13 + \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
1.14 + Isac.thy\normalfont, the setup has been changed from \ttfamily theory
1.15 + Inverse\_Z\_Transform imports Isac \normalfont to the above one.
1.16 + \par \noindent
1.17 + \begin{center}
1.18 + \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
1.19 + \end{center}
1.20 + Here in this theory there are the internal names twice, for instance we have
1.21 + \ttfamily (Thm.derivation\_name @{thm rule1} =
1.22 + "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
1.23 + but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
1.24 +*}
1.25
1.26 - ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
1.27 - Here in this theory there are the internal names twice, for instance we have
1.28 - (Thm.derivation_name @{thm rule1} = "Build_Inverse_Z_Transform.rule1") = true;
1.29 - but actually in us will be "Inverse_Z_Transform.rule1"
1.30 -*}
1.31 +section {*Trials towards the Z-Transform\label{sec:trials}*}
1.32 +
1.33 ML {*val thy = @{theory Isac};*}
1.34
1.35 -
1.36 -section {*trials towards Z transform *}
1.37 -text{*===============================*}
1.38 -subsection {*terms*}
1.39 +subsection {*Notations and Terms*}
1.40 +text{*\noindent Try which notations we are able to use.*}
1.41 ML {*
1.42 -@{term "1 < || z ||"};
1.43 -@{term "z / (z - 1)"};
1.44 -@{term "-u -n - 1"};
1.45 -@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
1.46 -@{term "z /(z - 1) = -u [-n - 1]"};Isac
1.47 -@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.48 -term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.49 + @{term "1 < || z ||"};
1.50 + @{term "z / (z - 1)"};
1.51 + @{term "-u -n - 1"};
1.52 + @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
1.53 + @{term "z /(z - 1) = -u [-n - 1]"};Isac
1.54 + @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.55 + term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.56 *}
1.57 +text{*\noindent Try which symbols we are able to use and how we generate them.*}
1.58 ML {*
1.59 -(*alpha --> "</alpha>" *)
1.60 -@{term "\<alpha> "};
1.61 -@{term "\<delta> "};
1.62 -@{term "\<phi> "};
1.63 -@{term "\<rho> "};
1.64 -term2str @{term "\<rho> "};
1.65 + (*alpha --> "</alpha>" *)
1.66 + @{term "\<alpha> "};
1.67 + @{term "\<delta> "};
1.68 + @{term "\<phi> "};
1.69 + @{term "\<rho> "};
1.70 + term2str @{term "\<rho> "};
1.71 *}
1.72
1.73 -subsection {*rules*}
1.74 -(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
1.75 -(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
1.76 +subsection {*Rules*}
1.77 +(*axiomatization "z / (z - 1) = -u [-n - 1]"
1.78 + Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
1.79 +(*definition "z / (z - 1) = -u [-n - 1]"
1.80 + Bad head of lhs: existing constant "op /"*)
1.81 axiomatization where
1.82 rule1: "1 = \<delta>[n]" and
1.83 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
1.84 @@ -53,122 +61,167 @@
1.85 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
1.86 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
1.87 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
1.88 +
1.89 +text{*\noindent Check the rules for their correct notation.
1.90 + (See the machine output.)*}
1.91 ML {*
1.92 -@{thm rule1};
1.93 -@{thm rule2};
1.94 -@{thm rule3};
1.95 -@{thm rule4};
1.96 + @{thm rule1};
1.97 + @{thm rule2};
1.98 + @{thm rule3};
1.99 + @{thm rule4};
1.100 *}
1.101
1.102 -subsection {*apply rules*}
1.103 +subsection {*Apply Rules*}
1.104 +text{*\noindent We try to apply the rules to a given expression.*}
1.105 +
1.106 ML {*
1.107 -val inverse_Z = append_rls "inverse_Z" e_rls
1.108 - [ Thm ("rule3",num_str @{thm rule3}),
1.109 - Thm ("rule4",num_str @{thm rule4}),
1.110 - Thm ("rule1",num_str @{thm rule1})
1.111 - ];
1.112 + val inverse_Z = append_rls "inverse_Z" e_rls
1.113 + [ Thm ("rule3",num_str @{thm rule3}),
1.114 + Thm ("rule4",num_str @{thm rule4}),
1.115 + Thm ("rule1",num_str @{thm rule1})
1.116 + ];
1.117
1.118 -val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.119 -val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
1.120 -term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
1.121 -*}
1.122 -ML {*
1.123 -val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
1.124 -*}
1.125 -ML {*
1.126 -val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.127 -term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
1.128 -term2str t;*}
1.129 -ML {*
1.130 -val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
1.131 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
1.132 -term2str t;
1.133 -*}
1.134 -ML {*
1.135 -val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
1.136 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
1.137 -term2str t;
1.138 -*}
1.139 -ML {*
1.140 -terms2str (asm1 @ asm2 @ asm3);
1.141 + val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.142 + val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
1.143 + term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.144 + (*
1.145 + * Attention rule1 is applied before the expression is
1.146 + * checked for rule4 which would be correct!!!
1.147 + *)
1.148 *}
1.149
1.150 -section {*Prepare steps for CTP-based programming language*}
1.151 -text{*TODO insert Calculation (Referenz?!)
1.152 +ML {* val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls); *}
1.153 +ML {*
1.154 + val SOME (t, asm1) =
1.155 + rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.156 + term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.157 + (*- real *)
1.158 + term2str t;
1.159
1.160 -The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps}
1.161 + val SOME (t, asm2) =
1.162 + rewrite_ thy ro er true (num_str @{thm rule4}) t;
1.163 + term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.164 + (*- real *)
1.165 + term2str t;
1.166
1.167 -the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}
1.168 + val SOME (t, asm3) =
1.169 + rewrite_ thy ro er true (num_str @{thm rule1}) t;
1.170 + term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.171 + (*- real *)
1.172 + term2str t;
1.173 +*}
1.174 +ML {* terms2str (asm1 @ asm2 @ asm3); *}
1.175
1.176 -*}
1.177 -subsection {*prepare expression \label{prep-expr}*}
1.178 -ML {*
1.179 -val ctxt = ProofContext.init_global @{theory Isac};
1.180 -val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
1.181 -
1.182 -val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.183 -val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.184 +section{*Prepare Steps for CTP-based programming Language\label{sec:prepstep}*}
1.185 +text{*
1.186 + \par \noindent The following sections are challanging with the CTP-based
1.187 + possibilities of building the programm. The goal is realized in
1.188 + Section~\ref{spec-meth} and Section~\ref{prog-steps}.
1.189 + \par The reader is advised to jump between the subsequent subsections and
1.190 + the respective steps in Section~\ref{prog-steps}. By comparing
1.191 + Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
1.192 + by step.
1.193 *}
1.194
1.195 -subsubsection {*multply with z*}
1.196 +subsection {*Prepare Expression\label{prep-expr}*}
1.197 +ML {*
1.198 + val ctxt = ProofContext.init_global @{theory Isac};
1.199 + val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
1.200 +
1.201 + val SOME fun1 =
1.202 + parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.203 + val SOME fun1' =
1.204 + parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.205 +*}
1.206 +
1.207 +subsubsection {*Prepare Numerator and Denominator*}
1.208 +text{*\noindent The partial fraction decomposion is only possible ig we
1.209 + get the bound variable out of the numerator. Therefor we divide
1.210 + the expression by $z$. Follow up the Calculation at
1.211 + Section~\ref{sec:calc:ztrans} line number 02.*}
1.212 +
1.213 axiomatization where
1.214 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
1.215
1.216 ML {*
1.217 -val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
1.218 -val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.219 -val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.220 + val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
1.221 + val SOME (fun2, asm1) =
1.222 + rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.223 + val SOME (fun2', asm1) =
1.224 + rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.225
1.226 -val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
1.227 -term2str fun3; (*fails on x^^^(-1) TODO*)
1.228 -val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
1.229 -term2str fun3'; (*OK*)
1.230 + val SOME (fun3,_) =
1.231 + rewrite_set_ @{theory Isac} false norm_Rational fun2;
1.232 + term2str fun3;
1.233 + (*
1.234 + * Fails on x^^^(-1)
1.235 + * We solve this problem by using 1/x as a workaround.
1.236 + *)
1.237 + val SOME (fun3',_) =
1.238 + rewrite_set_ @{theory Isac} false norm_Rational fun2';
1.239 + term2str fun3';
1.240 + (*
1.241 + * OK - workaround!
1.242 + *)
1.243 *}
1.244
1.245 -subsubsection {*get argument of X': z is the variable the equation is solved for*}
1.246 -text{*grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...
1.247 -
1.248 -grep -r "fun eva_" ... shows all functions witch can be used in a script.
1.249 -lookup this files how to build and handle such functions.
1.250 -
1.251 -the next section shows how to introduce such a function.
1.252 +subsubsection {*Get the Argument of the Expression X'*}
1.253 +text{*\noindent We use \texttt{grep} for finding possibilities how we can
1.254 + extract the bound variable in the expression. \ttfamily Atools.thy,
1.255 + Tools.thy \normalfont contain general utilities: \ttfamily
1.256 + eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
1.257 + \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
1.258 + witch can be used in a script. Lookup this files how to build
1.259 + and handle such functions.
1.260 + \par The next section shows how to introduce such a function.
1.261 *}
1.262
1.263 -subsubsection {*Decompose given term into lhs = rhs*}
1.264 +subsubsection{*Decompose the Given Term Into lhs and rhs\footnote{Note:
1.265 + lhs means \em Left Hand Side \normalfont and rhs means
1.266 + \em Right Hand Side \normalfont and indicates the left or
1.267 + the right part of an equation.}*}
1.268 ML {*
1.269 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
1.270 - val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
1.271 + val (_, denom) =
1.272 + HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
1.273 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.274 *}
1.275 -text {*we have rhs in the Script language, but we need a function
1.276 - which gets the denominator of a fraction*}
1.277
1.278 +text{*\noindent We have rhs in the Script language, but we need a function
1.279 + which gets the denominator of a fraction.*}
1.280
1.281 -subsubsection {*get the denominator and numerator out of a fraction*}
1.282 -text {*get denominator should become a constant for the isabelle parser: *}
1.283 +subsubsection{*Get the Denominator and Numerator out of a Fraction*}
1.284 +text{*\noindent The selv written functions in e.g. \texttt{get\_denominator}
1.285 + should become a constant for the isabelle parser:*}
1.286
1.287 consts
1.288 get_denominator :: "real => real"
1.289 get_numerator :: "real => real"
1.290
1.291 -text {* With the above definition we run into problems with parsing the Script InverseZTransform:
1.292 - This leads to "ambiguous parse trees" and we avoid this by shifting the definition
1.293 - to Rational.thy and re-building Isac.
1.294 - ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;
1.295 - it only works due to re-building Isac several times (indicated explicityl).
1.296 +text {*\noindent With the above definition we run into problems when we parse
1.297 + the Script \texttt{InverseZTransform}. This leads to \em ambiguous
1.298 + parse trees. \normalfont We avoid this by moving the definition
1.299 + to \ttfamily Rational.thy \normalfont and re-building Isac.
1.300 + \par \noindent ATTENTION: From now on \ttfamily
1.301 + Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
1.302 + it only works due to re-building Isac several times (indicated
1.303 + explicityl).
1.304 *}
1.305
1.306 ML {*
1.307 -(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
1.308 +(*
1.309 + *("get_denominator",
1.310 + * ("Rational.get_denominator", eval_get_denominator ""))
1.311 + *)
1.312 fun eval_get_denominator (thmid:string) _
1.313 (t as Const ("Rational.get_denominator", _) $
1.314 (Const ("Rings.inverse_class.divide", _) $ num $
1.315 denom)) thy =
1.316 SOME (mk_thmid thmid ""
1.317 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.318 + (Print_Mode.setmp []
1.319 + (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.320 Trueprop $ (mk_equality (t, denom)))
1.321 | eval_get_denominator _ _ _ _ = NONE;
1.322 -
1.323 *}
1.324 text {* tests of eval_get_denominator see test/Knowledge/rational.sml*}
1.325
1.326 @@ -888,7 +941,7 @@
1.327 atomty sc;
1.328 *}
1.329
1.330 -subsubsection {*Stepwise check the program*}
1.331 +subsubsection {*Stepwise check the program\label{sec:stepcheck}*}
1.332 ML {*
1.333 trace_rewrite := false;
1.334 trace_script := false; print_depth 9;