1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Sep 05 18:09:56 2018 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Nov 21 12:32:54 2018 +0100
1.3 @@ -7,7 +7,7 @@
1.4
1.5 begin
1.6
1.7 -text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
1.8 +text\<open>We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
1.9 exercise. Because Subsection~\ref{sec:stepcheck} requires
1.10 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
1.11 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
1.12 @@ -20,15 +20,15 @@
1.13 \ttfamily (Thm.derivation\_name @{thm rule1} =
1.14 "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
1.15 but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
1.16 -*}
1.17 +\<close>
1.18
1.19 -section {*Trials towards the Z-Transform\label{sec:trials}*}
1.20 +section \<open>Trials towards the Z-Transform\label{sec:trials}\<close>
1.21
1.22 -ML {*val thy = @{theory};*}
1.23 +ML \<open>val thy = @{theory};\<close>
1.24
1.25 -subsection {*Notations and Terms*}
1.26 -text{*\noindent Try which notations we are able to use.*}
1.27 -ML {*
1.28 +subsection \<open>Notations and Terms\<close>
1.29 +text\<open>\noindent Try which notations we are able to use.\<close>
1.30 +ML \<open>
1.31 @{term "1 < || z ||"};
1.32 @{term "z / (z - 1)"};
1.33 @{term "-u -n - 1"};
1.34 @@ -36,18 +36,18 @@
1.35 @{term "z /(z - 1) = -u [-n - 1]"};
1.36 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.37 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.38 -*}
1.39 -text{*\noindent Try which symbols we are able to use and how we generate them.*}
1.40 -ML {*
1.41 +\<close>
1.42 +text\<open>\noindent Try which symbols we are able to use and how we generate them.\<close>
1.43 +ML \<open>
1.44 (*alpha --> "</alpha>" *)
1.45 @{term "\<alpha> "};
1.46 @{term "\<delta> "};
1.47 @{term "\<phi> "};
1.48 @{term "\<rho> "};
1.49 term2str @{term "\<rho> "};
1.50 -*}
1.51 +\<close>
1.52
1.53 -subsection {*Rules*}
1.54 +subsection \<open>Rules\<close>
1.55 (*axiomatization "z / (z - 1) = -u [-n - 1]"
1.56 Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
1.57 (*definition "z / (z - 1) = -u [-n - 1]"
1.58 @@ -60,19 +60,19 @@
1.59 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
1.60 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
1.61
1.62 -text{*\noindent Check the rules for their correct notation.
1.63 - (See the machine output.)*}
1.64 -ML {*
1.65 +text\<open>\noindent Check the rules for their correct notation.
1.66 + (See the machine output.)\<close>
1.67 +ML \<open>
1.68 @{thm rule1};
1.69 @{thm rule2};
1.70 @{thm rule3};
1.71 @{thm rule4};
1.72 -*}
1.73 +\<close>
1.74
1.75 -subsection {*Apply Rules*}
1.76 -text{*\noindent We try to apply the rules to a given expression.*}
1.77 +subsection \<open>Apply Rules\<close>
1.78 +text\<open>\noindent We try to apply the rules to a given expression.\<close>
1.79
1.80 -ML {*
1.81 +ML \<open>
1.82 val inverse_Z = append_rls "inverse_Z" e_rls
1.83 [ Thm ("rule3",TermC.num_str @{thm rule3}),
1.84 Thm ("rule4",TermC.num_str @{thm rule4}),
1.85 @@ -86,10 +86,10 @@
1.86 * Attention rule1 is applied before the expression is
1.87 * checked for rule4 which would be correct!!!
1.88 *)
1.89 -*}
1.90 +\<close>
1.91
1.92 -ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}
1.93 -ML {*
1.94 +ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
1.95 +ML \<open>
1.96 val SOME (t, asm1) =
1.97 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
1.98 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.99 @@ -107,11 +107,11 @@
1.100 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.101 (*- real *)
1.102 term2str t;
1.103 -*}
1.104 -ML {* terms2str (asm1 @ asm2 @ asm3); *}
1.105 +\<close>
1.106 +ML \<open>terms2str (asm1 @ asm2 @ asm3);\<close>
1.107
1.108 -section{*Prepare Steps for TP-based programming Language\label{sec:prepstep}*}
1.109 -text{*
1.110 +section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
1.111 +text\<open>
1.112 \par \noindent The following sections are challenging with the CTP-based
1.113 possibilities of building the program. The goal is realized in
1.114 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
1.115 @@ -119,12 +119,12 @@
1.116 the respective steps in Section~\ref{prog-steps}. By comparing
1.117 Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
1.118 by step.
1.119 -*}
1.120 +\<close>
1.121
1.122 -subsection {*Prepare Expression\label{prep-expr}*}
1.123 -text{*\noindent We try two different notations and check which of them
1.124 - Isabelle can handle best.*}
1.125 -ML {*
1.126 +subsection \<open>Prepare Expression\label{prep-expr}\<close>
1.127 +text\<open>\noindent We try two different notations and check which of them
1.128 + Isabelle can handle best.\<close>
1.129 +ML \<open>
1.130 val ctxt = Proof_Context.init_global @{theory};
1.131 val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;
1.132
1.133 @@ -132,18 +132,18 @@
1.134 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.135 val SOME fun1' =
1.136 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.137 -*}
1.138 +\<close>
1.139
1.140 -subsubsection {*Prepare Numerator and Denominator*}
1.141 -text{*\noindent The partial fraction decomposition is only possible if we
1.142 +subsubsection \<open>Prepare Numerator and Denominator\<close>
1.143 +text\<open>\noindent The partial fraction decomposition is only possible if we
1.144 get the bound variable out of the numerator. Therefor we divide
1.145 the expression by $z$. Follow up the Calculation at
1.146 - Section~\ref{sec:calc:ztrans} line number 02.*}
1.147 + Section~\ref{sec:calc:ztrans} line number 02.\<close>
1.148
1.149 axiomatization where
1.150 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
1.151
1.152 -ML {*
1.153 +ML \<open>
1.154 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.155 val SOME (fun2, asm1) =
1.156 Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.157 @@ -163,10 +163,10 @@
1.158 (*
1.159 * OK - workaround!
1.160 *)
1.161 -*}
1.162 +\<close>
1.163
1.164 -subsubsection {*Get the Argument of the Expression X'*}
1.165 -text{*\noindent We use \texttt{grep} for finding possibilities how we can
1.166 +subsubsection \<open>Get the Argument of the Expression X'\<close>
1.167 +text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
1.168 extract the bound variable in the expression. \ttfamily Atools.thy,
1.169 Tools.thy \normalfont contain general utilities: \ttfamily
1.170 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
1.171 @@ -174,30 +174,30 @@
1.172 witch can be used in a script. Lookup this files how to build
1.173 and handle such functions.
1.174 \par The next section shows how to introduce such a function.
1.175 -*}
1.176 +\<close>
1.177
1.178 -subsubsection{*Decompose the Given Term Into lhs and rhs*}
1.179 -ML {*
1.180 +subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
1.181 +ML \<open>
1.182 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
1.183 val (_, denom) =
1.184 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
1.185 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.186 -*}
1.187 +\<close>
1.188
1.189 -text{*\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.190 +text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.191 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
1.192 the left or the right part of an equation.} in the Script language, but
1.193 - we need a function which gets the denominator of a fraction.*}
1.194 + we need a function which gets the denominator of a fraction.\<close>
1.195
1.196 -subsubsection{*Get the Denominator and Numerator out of a Fraction*}
1.197 -text{*\noindent The self written functions in e.g. \texttt{get\_denominator}
1.198 - should become a constant for the Isabelle parser:*}
1.199 +subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
1.200 +text\<open>\noindent The self written functions in e.g. \texttt{get\_denominator}
1.201 + should become a constant for the Isabelle parser:\<close>
1.202
1.203 consts
1.204 get_denominator :: "real => real"
1.205 get_numerator :: "real => real"
1.206
1.207 -text {*\noindent With the above definition we run into problems when we parse
1.208 +text \<open>\noindent With the above definition we run into problems when we parse
1.209 the Script \texttt{InverseZTransform}. This leads to \em ambiguous
1.210 parse trees. \normalfont We avoid this by moving the definition
1.211 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
1.212 @@ -205,9 +205,9 @@
1.213 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
1.214 it only works due to re-building {\sisac} several times (indicated
1.215 explicitly).
1.216 -*}
1.217 +\<close>
1.218
1.219 -ML {*
1.220 +ML \<open>
1.221 (*
1.222 *("get_denominator",
1.223 * ("Rational.get_denominator", eval_get_denominator ""))
1.224 @@ -219,15 +219,15 @@
1.225 SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
1.226 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.227 | eval_get_denominator _ _ _ _ = NONE;
1.228 -*}
1.229 -text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
1.230 - see \ttfamily test/Knowledge/rational.sml\normalfont*}
1.231 +\<close>
1.232 +text \<open>\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
1.233 + see \ttfamily test/Knowledge/rational.sml\normalfont\<close>
1.234
1.235 -text {*\noindent \ttfamily get\_numerator \normalfont should also become a
1.236 +text \<open>\noindent \ttfamily get\_numerator \normalfont should also become a
1.237 constant for the Isabelle parser, follow up the \texttt{const}
1.238 - declaration above.*}
1.239 + declaration above.\<close>
1.240
1.241 -ML {*
1.242 +ML \<open>
1.243 (*
1.244 *("get_numerator",
1.245 * ("Rational.get_numerator", eval_get_numerator ""))
1.246 @@ -239,15 +239,15 @@
1.247 SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
1.248 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.249 | eval_get_numerator _ _ _ _ = NONE;
1.250 -*}
1.251 +\<close>
1.252
1.253 -text {*\noindent We discovered several problems by implementing the
1.254 +text \<open>\noindent We discovered several problems by implementing the
1.255 \ttfamily get\_numerator \normalfont function. Remember when
1.256 putting new functions to {\sisac}, put them in a thy file and rebuild
1.257 - {\sisac}, also put them in the ruleset for the script!*}
1.258 + {\sisac}, also put them in the ruleset for the script!\<close>
1.259
1.260 -subsection {*Solve Equation\label{sec:solveq}*}
1.261 -text {*\noindent We have to find the zeros of the term, therefor we use our
1.262 +subsection \<open>Solve Equation\label{sec:solveq}\<close>
1.263 +text \<open>\noindent We have to find the zeros of the term, therefor we use our
1.264 \ttfamily get\_denominator \normalfont function from the step before
1.265 and try to solve the second order equation. (Follow up the Calculation
1.266 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
1.267 @@ -255,24 +255,24 @@
1.268 \par We know that this equation can be categorized as \em univariate
1.269 equation \normalfont and solved with the functions {\sisac} provides
1.270 for this equation type. Later on {\sisac} should determine the type
1.271 - of the given equation self.*}
1.272 -ML {*
1.273 + of the given equation self.\<close>
1.274 +ML \<open>
1.275 val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
1.276 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
1.277 "solveFor z",
1.278 "solutions L"];
1.279 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.280 -*}
1.281 -text {*\noindent Check if the given equation matches the specification of this
1.282 - equation type.*}
1.283 -ML {*
1.284 +\<close>
1.285 +text \<open>\noindent Check if the given equation matches the specification of this
1.286 + equation type.\<close>
1.287 +ML \<open>
1.288 Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
1.289 -*}
1.290 +\<close>
1.291
1.292 -text{*\noindent We switch up to the {\sisac} Context and try to solve the
1.293 - equation with a more specific type definition.*}
1.294 +text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
1.295 + equation with a more specific type definition.\<close>
1.296
1.297 -ML {*
1.298 +ML \<open>
1.299 Context.theory_name thy = "Isac";
1.300 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
1.301 val fmz = (*specification*)
1.302 @@ -284,20 +284,20 @@
1.303 ("Isac",
1.304 ["abcFormula","degree_2","polynomial","univariate","equation"],
1.305 ["no_met"]);
1.306 -*}
1.307 +\<close>
1.308
1.309 -text {*\noindent Check if the (other) given equation matches the
1.310 - specification of this equation type.*}
1.311 +text \<open>\noindent Check if the (other) given equation matches the
1.312 + specification of this equation type.\<close>
1.313
1.314 -ML {*
1.315 +ML \<open>
1.316 Specify.match_pbl fmz (Specify.get_pbt
1.317 ["abcFormula","degree_2","polynomial","univariate","equation"]);
1.318 -*}
1.319 +\<close>
1.320
1.321 -text {*\noindent We stepwise solve the equation. This is done by the
1.322 - use of a so called calc tree seen downwards.*}
1.323 +text \<open>\noindent We stepwise solve the equation. This is done by the
1.324 + use of a so called calc tree seen downwards.\<close>
1.325
1.326 -ML {*
1.327 +ML \<open>
1.328 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.329 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.330 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.331 @@ -321,37 +321,37 @@
1.332 *)
1.333 Chead.show_pt pt;
1.334 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
1.335 -*}
1.336 +\<close>
1.337
1.338 -subsection {*Partial Fraction Decomposition\label{sec:pbz}*}
1.339 -text{*\noindent We go on with the decomposition of our expression. Follow up the
1.340 +subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
1.341 +text\<open>\noindent We go on with the decomposition of our expression. Follow up the
1.342 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
1.343 - Subproblem~1.*}
1.344 -subsubsection {*Solutions of the Equation*}
1.345 -text{*\noindent We get the solutions of the before solved equation in a list.*}
1.346 + Subproblem~1.\<close>
1.347 +subsubsection \<open>Solutions of the Equation\<close>
1.348 +text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
1.349
1.350 -ML {*
1.351 +ML \<open>
1.352 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
1.353 term2str solutions;
1.354 atomty solutions;
1.355 -*}
1.356 +\<close>
1.357
1.358 -subsubsection {*Get Solutions out of a List*}
1.359 -text {*\noindent In {\sisac}'s TP-based programming language:
1.360 +subsubsection \<open>Get Solutions out of a List\<close>
1.361 +text \<open>\noindent In {\sisac}'s TP-based programming language:
1.362 \begin{verbatim}
1.363 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
1.364 \end{verbatim}
1.365 can be useful.
1.366 - *}
1.367 +\<close>
1.368
1.369 -ML {*
1.370 +ML \<open>
1.371 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
1.372 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
1.373 term2str s_1;
1.374 term2str s_2;
1.375 -*}
1.376 +\<close>
1.377
1.378 -text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
1.379 +text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
1.380 requires to get the denominators of the partial fractions out of the
1.381 Solutions as:
1.382 \begin{itemize}
1.383 @@ -359,27 +359,27 @@
1.384 \item $Denominator_{2}=z-Zeropoint_{2}$
1.385 \item \ldots
1.386 \end{itemize}
1.387 -*}
1.388 +\<close>
1.389
1.390 -ML {*
1.391 +ML \<open>
1.392 val xx = HOLogic.dest_eq s_1;
1.393 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.394 val xx = HOLogic.dest_eq s_2;
1.395 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.396 term2str s_1';
1.397 term2str s_2';
1.398 -*}
1.399 +\<close>
1.400
1.401 -text {*\noindent For the programming language a function collecting all the
1.402 - above manipulations is helpful.*}
1.403 +text \<open>\noindent For the programming language a function collecting all the
1.404 + above manipulations is helpful.\<close>
1.405
1.406 -ML {*
1.407 +ML \<open>
1.408 fun fac_from_sol s =
1.409 let val (lhs, rhs) = HOLogic.dest_eq s
1.410 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
1.411 -*}
1.412 +\<close>
1.413
1.414 -ML {*
1.415 +ML \<open>
1.416 fun mk_prod prod [] =
1.417 if prod = e_term
1.418 then error "mk_prod called with []"
1.419 @@ -398,7 +398,7 @@
1.420 let val p =
1.421 HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
1.422 in mk_prod p (t2 :: ts) end
1.423 -*}
1.424 +\<close>
1.425 (* ML {*
1.426 probably keep these test in test/Tools/isac/...
1.427 (*mk_prod e_term [];*)
1.428 @@ -416,23 +416,23 @@
1.429 mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
1.430 term2str prod = "(x + 1) * (x + 2) * (x + 3)";
1.431 *} *)
1.432 -ML {*
1.433 +ML \<open>
1.434 fun factors_from_solution sol =
1.435 let val ts = HOLogic.dest_list sol
1.436 in mk_prod e_term (map fac_from_sol ts) end;
1.437 -*}
1.438 +\<close>
1.439 (* ML {*
1.440 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
1.441 val fs = factors_from_solution sol;
1.442 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.443 *} *)
1.444 -text {*\noindent This function needs to be packed such that it can be evaluated
1.445 +text \<open>\noindent This function needs to be packed such that it can be evaluated
1.446 by the Lucas-Interpreter. Therefor we moved the function to the
1.447 corresponding \ttfamily Equation.thy \normalfont in our case
1.448 \ttfamily PartialFractions.thy \normalfont. The necessary steps
1.449 are quit the same as we have done with \ttfamily get\_denominator
1.450 - \normalfont before.*}
1.451 -ML {*
1.452 + \normalfont before.\<close>
1.453 +ML \<open>
1.454 (*("factors_from_solution",
1.455 ("Partial_Fractions.factors_from_solution",
1.456 eval_factors_from_solution ""))*)
1.457 @@ -445,9 +445,9 @@
1.458 end)
1.459 handle _ => NONE)
1.460 | eval_factors_from_solution _ _ _ _ = NONE;
1.461 -*}
1.462 +\<close>
1.463
1.464 -text {*\noindent The tracing output of the calc tree after applying this
1.465 +text \<open>\noindent The tracing output of the calc tree after applying this
1.466 function was:
1.467 \begin{verbatim}
1.468 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
1.469 @@ -459,9 +459,9 @@
1.470 These observations indicate, that the Lucas-Interpreter (LIP)
1.471 does not know how to evaluate \ttfamily factors\_from\_solution
1.472 \normalfont, so we knew that there is something wrong or missing.
1.473 - *}
1.474 +\<close>
1.475
1.476 -text{*\noindent First we isolate the difficulty in the program as follows:
1.477 +text\<open>\noindent First we isolate the difficulty in the program as follows:
1.478 \begin{verbatim}
1.479 " (L_L::bool list) = (SubProblem (PolyEq', " ^
1.480 " [abcFormula, degree_2, polynomial, " ^
1.481 @@ -569,14 +569,14 @@
1.482 \end{verbatim}
1.483
1.484 After rebuilding {\sisac} again it worked.
1.485 -*}
1.486 +\<close>
1.487
1.488 -subsubsection {*Build Expression*}
1.489 -text {*\noindent In {\sisac}'s TP-based programming language we can build
1.490 +subsubsection \<open>Build Expression\<close>
1.491 +text \<open>\noindent In {\sisac}'s TP-based programming language we can build
1.492 expressions by:\\
1.493 - \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont*}
1.494 + \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
1.495
1.496 -ML {*
1.497 +ML \<open>
1.498 (*
1.499 * The main denominator is the multiplication of the denominators of
1.500 * all partial fractions.
1.501 @@ -589,69 +589,69 @@
1.502 val expr' = HOLogic.mk_binop
1.503 "Rings.divide_class.divide" (numerator, denominator');
1.504 term2str expr';
1.505 -*}
1.506 +\<close>
1.507
1.508 -subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}
1.509 +subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
1.510
1.511 -text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our
1.512 +text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
1.513 expression 2nd order. Follow up the calculation in
1.514 - Section~\ref{sec:calc:ztrans} Step~03.*}
1.515 + Section~\ref{sec:calc:ztrans} Step~03.\<close>
1.516
1.517 -ML {*Context.theory_name thy = "Isac"*}
1.518 +ML \<open>Context.theory_name thy = "Isac"\<close>
1.519
1.520 -text{*\noindent We define two axiomatization, the first one is the main ansatz,
1.521 +text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
1.522 the next one is just an equivalent transformation of the resulting
1.523 equation. Both axiomatizations were moved to \ttfamily
1.524 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
1.525 programs it is possible to use the rulesets and the machine will find
1.526 - the correct ansatz and equivalent transformation itself.*}
1.527 + the correct ansatz and equivalent transformation itself.\<close>
1.528
1.529 axiomatization where
1.530 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
1.531 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
1.532
1.533 -text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
1.534 +text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
1.535 our expression and get an equation with our expression on the left
1.536 - and the partial fractions of it on the right hand side.*}
1.537 + and the partial fractions of it on the right hand side.\<close>
1.538
1.539 -ML {*
1.540 +ML \<open>
1.541 val SOME (t1,_) =
1.542 rewrite_ @{theory} e_rew_ord e_rls false
1.543 @{thm ansatz_2nd_order} expr';
1.544 term2str t1; atomty t1;
1.545 val eq1 = HOLogic.mk_eq (expr', t1);
1.546 term2str eq1;
1.547 -*}
1.548 +\<close>
1.549
1.550 -text{*\noindent Eliminate the denominators by multiplying the left and the
1.551 +text\<open>\noindent Eliminate the denominators by multiplying the left and the
1.552 right hand side of the equation with the main denominator. This is an
1.553 simple equivalent transformation. Later on we use an own ruleset
1.554 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
1.555 - Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.*}
1.556 + Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
1.557
1.558 -ML {*
1.559 +ML \<open>
1.560 val SOME (eq2,_) =
1.561 rewrite_ @{theory} e_rew_ord e_rls false
1.562 @{thm equival_trans_2nd_order} eq1;
1.563 term2str eq2;
1.564 -*}
1.565 +\<close>
1.566
1.567 -text{*\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
1.568 - for simplifications on expressions.*}
1.569 +text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
1.570 + for simplifications on expressions.\<close>
1.571
1.572 -ML {*
1.573 +ML \<open>
1.574 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
1.575 term2str eq3;
1.576 (*
1.577 * ?A ?B not simplified
1.578 *)
1.579 -*}
1.580 +\<close>
1.581
1.582 -text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
1.583 +text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
1.584 simplifications. The problem that we would like to have only a specific degree
1.585 - of simplification occurs right here, in the next step.*}
1.586 + of simplification occurs right here, in the next step.\<close>
1.587
1.588 -ML {*
1.589 +ML \<open>
1.590 trace_rewrite := false;
1.591 val SOME fract1 =
1.592 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
1.593 @@ -665,11 +665,11 @@
1.594 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.595 * would be more traditional...
1.596 *)
1.597 -*}
1.598 +\<close>
1.599
1.600 -text{*\noindent We walk around this problem by generating our new equation first.*}
1.601 +text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
1.602
1.603 -ML {*
1.604 +ML \<open>
1.605 val (numerator, denominator) = HOLogic.dest_eq eq3;
1.606 val eq3' = HOLogic.mk_eq (numerator, fract1);
1.607 (*
1.608 @@ -682,21 +682,21 @@
1.609 val SOME (eq3'' ,_) =
1.610 rewrite_set_ @{theory} false norm_Rational eq3';
1.611 term2str eq3'';
1.612 -*}
1.613 +\<close>
1.614
1.615 -text{*\noindent Still working at {\sisac}\ldots*}
1.616 +text\<open>\noindent Still working at {\sisac}\ldots\<close>
1.617
1.618 -ML {* Context.theory_name thy = "Isac" *}
1.619 +ML \<open>Context.theory_name thy = "Isac"\<close>
1.620
1.621 -subsubsection {*Build a Rule-Set for the Ansatz*}
1.622 -text {*\noindent The \emph{ansatz} rules violate the principle that each
1.623 +subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
1.624 +text \<open>\noindent The \emph{ansatz} rules violate the principle that each
1.625 variable on the right-hand-side must also occur on the
1.626 left-hand-side of the rule: A, B, etc. don't do that. Thus the
1.627 rewriter marks these variables with question marks: ?A, ?B, etc.
1.628 These question marks can be dropped by \ttfamily fun
1.629 - drop\_questionmarks\normalfont.*}
1.630 + drop\_questionmarks\normalfont.\<close>
1.631
1.632 -ML {*
1.633 +ML \<open>
1.634 val ansatz_rls = prep_rls @{theory} (
1.635 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.636 erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.637 @@ -705,32 +705,32 @@
1.638 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
1.639 ],
1.640 scr = EmptyScr});
1.641 -*}
1.642 +\<close>
1.643
1.644 -text{*\noindent We apply the ruleset\ldots*}
1.645 +text\<open>\noindent We apply the ruleset\ldots\<close>
1.646
1.647 -ML {*
1.648 +ML \<open>
1.649 val SOME (ttttt,_) =
1.650 rewrite_set_ @{theory} false ansatz_rls expr';
1.651 -*}
1.652 +\<close>
1.653
1.654 -text{*\noindent And check the output\ldots*}
1.655 +text\<open>\noindent And check the output\ldots\<close>
1.656
1.657 -ML {*
1.658 +ML \<open>
1.659 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.660 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.661 -*}
1.662 +\<close>
1.663
1.664 -subsubsection {*Get the First Coefficient*}
1.665 +subsubsection \<open>Get the First Coefficient\<close>
1.666
1.667 -text{*\noindent Now it's up to get the two coefficients A and B, which will be
1.668 +text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
1.669 the numerators of our partial fractions. Continue following up the
1.670 - Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
1.671 + Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
1.672
1.673 -text{*\noindent To get the first coefficient we substitute $z$ with the first
1.674 - zero-point we determined in Section~\ref{sec:solveq}.*}
1.675 +text\<open>\noindent To get the first coefficient we substitute $z$ with the first
1.676 + zero-point we determined in Section~\ref{sec:solveq}.\<close>
1.677
1.678 -ML {*
1.679 +ML \<open>
1.680 val SOME (eq4_1,_) =
1.681 rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
1.682 term2str eq4_1;
1.683 @@ -798,19 +798,19 @@
1.684 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.685 (*End_Proof'*)
1.686 f2str fa;
1.687 -*}
1.688 +\<close>
1.689
1.690 -subsubsection {*Get Second Coefficient*}
1.691 +subsubsection \<open>Get Second Coefficient\<close>
1.692
1.693 -text{*\noindent With the use of \texttt{thy} we check which theories the
1.694 - interpreter knows.*}
1.695 +text\<open>\noindent With the use of \texttt{thy} we check which theories the
1.696 + interpreter knows.\<close>
1.697
1.698 -ML {*thy*}
1.699 +ML \<open>thy\<close>
1.700
1.701 -text{*\noindent To get the second coefficient we substitute $z$ with the second
1.702 - zero-point we determined in Section~\ref{sec:solveq}.*}
1.703 +text\<open>\noindent To get the second coefficient we substitute $z$ with the second
1.704 + zero-point we determined in Section~\ref{sec:solveq}.\<close>
1.705
1.706 -ML {*
1.707 +ML \<open>
1.708 val SOME (eq4b_1,_) =
1.709 rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
1.710 term2str eq4b_1;
1.711 @@ -849,78 +849,78 @@
1.712 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.713 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.714 f2str fb;
1.715 -*}
1.716 +\<close>
1.717
1.718 -text{*\noindent We compare our results with the pre calculated upshot.*}
1.719 +text\<open>\noindent We compare our results with the pre calculated upshot.\<close>
1.720
1.721 -ML {*
1.722 +ML \<open>
1.723 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
1.724 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
1.725 -*}
1.726 +\<close>
1.727
1.728 -section {*Implement the Specification and the Method \label{spec-meth}*}
1.729 +section \<open>Implement the Specification and the Method \label{spec-meth}\<close>
1.730
1.731 -text{*\noindent Now everything we need for solving the problem has been
1.732 +text\<open>\noindent Now everything we need for solving the problem has been
1.733 tested out. We now start by creating new nodes for our methods and
1.734 - further on our new program in the interpreter.*}
1.735 + further on our new program in the interpreter.\<close>
1.736
1.737 -subsection{*Define the Field Descriptions for the
1.738 - Specification\label{sec:deffdes}*}
1.739 +subsection\<open>Define the Field Descriptions for the
1.740 + Specification\label{sec:deffdes}\<close>
1.741
1.742 -text{*\noindent We define the fields \em filterExpression \normalfont and
1.743 +text\<open>\noindent We define the fields \em filterExpression \normalfont and
1.744 \em stepResponse \normalfont both as equations, they represent the in- and
1.745 - output of the program.*}
1.746 + output of the program.\<close>
1.747
1.748 consts
1.749 filterExpression :: "bool => una"
1.750 stepResponse :: "bool => una"
1.751
1.752 -subsection{*Define the Specification*}
1.753 +subsection\<open>Define the Specification\<close>
1.754
1.755 -text{*\noindent The next step is defining the specifications as nodes in the
1.756 +text\<open>\noindent The next step is defining the specifications as nodes in the
1.757 designated part. We have to create the hierarchy node by node and start
1.758 with \em SignalProcessing \normalfont and go on by creating the node
1.759 - \em Z\_Transform\normalfont.*}
1.760 + \em Z\_Transform\normalfont.\<close>
1.761
1.762 -setup {* KEStore_Elems.add_pbts
1.763 +setup \<open>KEStore_Elems.add_pbts
1.764 [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
1.765 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
1.766 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
1.767 + (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])]\<close>
1.768
1.769 -text{*\noindent For the suddenly created node we have to define the input
1.770 +text\<open>\noindent For the suddenly created node we have to define the input
1.771 and output parameters. We already prepared their definition in
1.772 - Section~\ref{sec:deffdes}.*}
1.773 + Section~\ref{sec:deffdes}.\<close>
1.774
1.775 -setup {* KEStore_Elems.add_pbts
1.776 +setup \<open>KEStore_Elems.add_pbts
1.777 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
1.778 (["Inverse", "Z_Transform", "SignalProcessing"],
1.779 [("#Given", ["filterExpression X_eq"]),
1.780 ("#Find", ["stepResponse n_eq"])],
1.781 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.782 NONE,
1.783 - [["SignalProcessing","Z_Transform","Inverse"]])] *}
1.784 -ML {*
1.785 + [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
1.786 +ML \<open>
1.787 show_ptyps ();
1.788 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
1.789 -*}
1.790 +\<close>
1.791
1.792 -subsection {*Define Name and Signature for the Method*}
1.793 +subsection \<open>Define Name and Signature for the Method\<close>
1.794
1.795 -text{*\noindent As a next step we store the definition of our new method as a
1.796 - constant for the interpreter.*}
1.797 +text\<open>\noindent As a next step we store the definition of our new method as a
1.798 + constant for the interpreter.\<close>
1.799
1.800 consts
1.801 InverseZTransform :: "[bool, bool] => bool"
1.802 ("((Script InverseZTransform (_ =))// (_))" 9)
1.803
1.804 -subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}
1.805 +subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
1.806
1.807 -text{*\noindent Again we have to generate the nodes step by step, first the
1.808 +text\<open>\noindent Again we have to generate the nodes step by step, first the
1.809 parent node and then the originally \em Z\_Transformation
1.810 \normalfont node. We have to define both nodes first with an empty script
1.811 - as content.*}
1.812 + as content.\<close>
1.813
1.814 -setup {* KEStore_Elems.add_mets
1.815 +setup \<open>KEStore_Elems.add_mets
1.816 [prep_met thy "met_SP" [] e_metID
1.817 (["SignalProcessing"], [],
1.818 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.819 @@ -931,26 +931,26 @@
1.820 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.821 errpats = [], nrls = e_rls},
1.822 "empty_script")]
1.823 -*}
1.824 +\<close>
1.825
1.826 -text{*\noindent After we generated both nodes, we can fill the containing
1.827 +text\<open>\noindent After we generated both nodes, we can fill the containing
1.828 script we want to implement later. First we define the specifications
1.829 - of the script in e.g. the in- and output.*}
1.830 + of the script in e.g. the in- and output.\<close>
1.831
1.832 -setup {* KEStore_Elems.add_mets
1.833 +setup \<open>KEStore_Elems.add_mets
1.834 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.835 (["SignalProcessing", "Z_Transform", "Inverse"],
1.836 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
1.837 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.838 errpats = [], nrls = e_rls},
1.839 "empty_script")]
1.840 -*}
1.841 +\<close>
1.842
1.843 -text{*\noindent After we stored the definition we can start implementing the
1.844 +text\<open>\noindent After we stored the definition we can start implementing the
1.845 script itself. As a first try we define only three rows containing one
1.846 - simple operation.*}
1.847 + simple operation.\<close>
1.848
1.849 -setup {* KEStore_Elems.add_mets
1.850 +setup \<open>KEStore_Elems.add_mets
1.851 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.852 (["SignalProcessing", "Z_Transform", "Inverse"],
1.853 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
1.854 @@ -960,39 +960,39 @@
1.855 " (let X = Take Xeq;" ^
1.856 " X = Rewrite ruleZY False X" ^
1.857 " in X)")]
1.858 -*}
1.859 +\<close>
1.860
1.861 -text{*\noindent Check if the method has been stored correctly\ldots*}
1.862 +text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
1.863
1.864 -ML {*
1.865 +ML \<open>
1.866 show_mets();
1.867 -*}
1.868 +\<close>
1.869
1.870 -text{*\noindent If yes we can get the method by stepping backwards through
1.871 - the hierarchy.*}
1.872 +text\<open>\noindent If yes we can get the method by stepping backwards through
1.873 + the hierarchy.\<close>
1.874
1.875 -ML {*
1.876 +ML \<open>
1.877 get_met ["SignalProcessing","Z_Transform","Inverse"];
1.878 -*}
1.879 +\<close>
1.880
1.881 -section {*Program in TP-based language \label{prog-steps}*}
1.882 +section \<open>Program in TP-based language \label{prog-steps}\<close>
1.883
1.884 -text{*\noindent We start stepwise expanding our program. The script is a
1.885 +text\<open>\noindent We start stepwise expanding our program. The script is a
1.886 simple string containing several manipulation instructions.
1.887 \par The first script we try contains no instruction, we only test if
1.888 - building scripts that way work.*}
1.889 + building scripts that way work.\<close>
1.890
1.891 -subsection {*Stepwise Extend the Program*}
1.892 -ML {*
1.893 +subsection \<open>Stepwise Extend the Program\<close>
1.894 +ML \<open>
1.895 val str =
1.896 "Script InverseZTransform (Xeq::bool) = "^
1.897 " Xeq";
1.898 -*}
1.899 +\<close>
1.900
1.901 -text{*\noindent Next we put some instructions in the script and try if we are
1.902 - able to solve our first equation.*}
1.903 +text\<open>\noindent Next we put some instructions in the script and try if we are
1.904 + able to solve our first equation.\<close>
1.905
1.906 -ML {*
1.907 +ML \<open>
1.908 val str =
1.909 "Script InverseZTransform (Xeq::bool) = "^
1.910 (*
1.911 @@ -1029,13 +1029,13 @@
1.912 " [no_met]) "^
1.913 " [BOOL e_e, REAL v_v]) "^
1.914 " in X)";
1.915 -*}
1.916 +\<close>
1.917
1.918 -text{*\noindent To solve the equation it is necessary to drop the left hand
1.919 +text\<open>\noindent To solve the equation it is necessary to drop the left hand
1.920 side, now we only need the denominator of the right hand side. The first
1.921 - equation solves the zeros of our expression.*}
1.922 + equation solves the zeros of our expression.\<close>
1.923
1.924 -ML {*
1.925 +ML \<open>
1.926 val str =
1.927 "Script InverseZTransform (Xeq::bool) = "^
1.928 " (let X = Take Xeq; "^
1.929 @@ -1046,13 +1046,13 @@
1.930 * drop X'= for equation solving
1.931 *)
1.932 " in X)";
1.933 -*}
1.934 +\<close>
1.935
1.936 -text{*\noindent As mentioned above, we need the denominator of the right hand
1.937 +text\<open>\noindent As mentioned above, we need the denominator of the right hand
1.938 side. The equation itself consists of this denominator and tries to find
1.939 - a $z$ for this the denominator is equal to zero.*}
1.940 + a $z$ for this the denominator is equal to zero.\<close>
1.941
1.942 -ML {*
1.943 +ML \<open>
1.944 val str =
1.945 "Script InverseZTransform (X_eq::bool) = "^
1.946 " (let X = Take X_eq; "^
1.947 @@ -1076,12 +1076,12 @@
1.948 parse thy str;
1.949 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1.950 atomty sc;
1.951 -*}
1.952 +\<close>
1.953
1.954 -text {*\noindent This ruleset contains all functions that are in the script;
1.955 - The evaluation of the functions is done by rewriting using this ruleset.*}
1.956 +text \<open>\noindent This ruleset contains all functions that are in the script;
1.957 + The evaluation of the functions is done by rewriting using this ruleset.\<close>
1.958
1.959 -ML {*
1.960 +ML \<open>
1.961 val srls =
1.962 Rls {id="srls_InverseZTransform",
1.963 preconds = [],
1.964 @@ -1113,18 +1113,18 @@
1.965 eval_drop_questionmarks "#drop_?")
1.966 ],
1.967 scr = EmptyScr};
1.968 -*}
1.969 +\<close>
1.970
1.971
1.972 -subsection {*Store Final Version of Program for Execution*}
1.973 +subsection \<open>Store Final Version of Program for Execution\<close>
1.974
1.975 -text{*\noindent After we also tested how to write scripts and run them,
1.976 +text\<open>\noindent After we also tested how to write scripts and run them,
1.977 we start creating the final version of our script and store it into
1.978 the method for which we created a node in Section~\ref{sec:cparentnode}
1.979 Note that we also did this stepwise, but we didn't kept every
1.980 - subversion.*}
1.981 + subversion.\<close>
1.982
1.983 -setup {* KEStore_Elems.add_mets
1.984 +setup \<open>KEStore_Elems.add_mets
1.985 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.986 (["SignalProcessing", "Z_Transform", "Inverse"],
1.987 [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
1.988 @@ -1197,16 +1197,16 @@
1.989 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1.990 " n_eq = drop_questionmarks n_eq "^
1.991 "in n_eq)")]
1.992 -*}
1.993 +\<close>
1.994
1.995
1.996 -subsection {*Check the Program*}
1.997 -text{*\noindent When the script is ready we can start checking our work.*}
1.998 -subsubsection {*Check the Formalization*}
1.999 -text{*\noindent First we want to check the formalization of the in and
1.1000 - output of our program.*}
1.1001 +subsection \<open>Check the Program\<close>
1.1002 +text\<open>\noindent When the script is ready we can start checking our work.\<close>
1.1003 +subsubsection \<open>Check the Formalization\<close>
1.1004 +text\<open>\noindent First we want to check the formalization of the in and
1.1005 + output of our program.\<close>
1.1006
1.1007 -ML {*
1.1008 +ML \<open>
1.1009 val fmz =
1.1010 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1.1011 "stepResponse (x[n::real]::bool)"];
1.1012 @@ -1237,13 +1237,13 @@
1.1013 "Z_Transform",
1.1014 "Inverse"];
1.1015 atomty sc;
1.1016 -*}
1.1017 +\<close>
1.1018
1.1019 -subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
1.1020 -text{*\noindent We start to stepwise execute our new program in a calculation
1.1021 - tree and check if every node implements that what we have wanted.*}
1.1022 +subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
1.1023 +text\<open>\noindent We start to stepwise execute our new program in a calculation
1.1024 + tree and check if every node implements that what we have wanted.\<close>
1.1025
1.1026 -ML {*
1.1027 +ML \<open>
1.1028 trace_rewrite := false; (*true*)
1.1029 trace_script := false; (*true*)
1.1030 print_depth 9;
1.1031 @@ -1281,9 +1281,9 @@
1.1032 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1033 "SubProblem";
1.1034 print_depth 3;
1.1035 -*}
1.1036 +\<close>
1.1037
1.1038 -text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1.1039 +text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
1.1040 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1.1041 the following points:\begin{itemize}
1.1042 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1.1043 @@ -1318,14 +1318,14 @@
1.1044 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1.1045 no\_meth by [no\_meth] \normalfont in Script
1.1046 \end{itemize}
1.1047 -*}
1.1048 +\<close>
1.1049
1.1050 -ML {*
1.1051 +ML \<open>
1.1052 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1053 (*Model_Problem";*)
1.1054 -*}
1.1055 +\<close>
1.1056
1.1057 -text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1.1058 +text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
1.1059 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
1.1060 considered the following points:\begin{itemize}
1.1061 \item Difference in the arguments
1.1062 @@ -1333,9 +1333,9 @@
1.1063 equation works, so there must be some difference in the arguments
1.1064 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
1.1065 instead of \ttfamily [no\_met] \normalfont ;-)
1.1066 - \end{itemize}*}
1.1067 + \end{itemize}\<close>
1.1068
1.1069 -ML {*
1.1070 +ML \<open>
1.1071 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1072 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1.1073 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1074 @@ -1344,9 +1344,9 @@
1.1075 (*Add_Find solutions z_i";*)
1.1076 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1077 (*Specify_Theory Isac";*)
1.1078 -*}
1.1079 +\<close>
1.1080
1.1081 -text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1.1082 +text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
1.1083 \normalfont The search for the reason considered the following points:
1.1084 \begin{itemize}
1.1085 \item Was there an error message? NO -- ok
1.1086 @@ -1380,9 +1380,9 @@
1.1087 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1.1088 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1.1089 selection of the appropriate type to isac as done in the final Script ;-))
1.1090 - \end{itemize}*}
1.1091 + \end{itemize}\<close>
1.1092
1.1093 -ML {*
1.1094 +ML \<open>
1.1095 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1096 (*Specify_Problem [abcFormula,...";*)
1.1097 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1098 @@ -1473,53 +1473,53 @@
1.1099 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
1.1100 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
1.1101 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
1.1102 -*}
1.1103 -ML {*
1.1104 +\<close>
1.1105 +ML \<open>
1.1106 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1107 -*}
1.1108 -ML {*
1.1109 +\<close>
1.1110 +ML \<open>
1.1111 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1112 -*}
1.1113 -ML {*
1.1114 +\<close>
1.1115 +ML \<open>
1.1116 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1117 -*}
1.1118 -ML {*
1.1119 +\<close>
1.1120 +ML \<open>
1.1121 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1122 -*}
1.1123 -ML {*
1.1124 +\<close>
1.1125 +ML \<open>
1.1126 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1127 -*}
1.1128 -ML {*
1.1129 +\<close>
1.1130 +ML \<open>
1.1131 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1132 -*}
1.1133 +\<close>
1.1134
1.1135 -ML {*
1.1136 +ML \<open>
1.1137 trace_script := true;
1.1138 -*}
1.1139 -ML {*
1.1140 +\<close>
1.1141 +ML \<open>
1.1142 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.1143 -*}
1.1144 -ML {*
1.1145 +\<close>
1.1146 +ML \<open>
1.1147 Chead.show_pt pt;
1.1148 -*}
1.1149 -ML {*
1.1150 -*}
1.1151 -ML {*
1.1152 -*}
1.1153 -ML {*
1.1154 -*}
1.1155 -ML {*
1.1156 -*}
1.1157 -ML {*
1.1158 -*}
1.1159 -ML {*
1.1160 -*}
1.1161 +\<close>
1.1162 +ML \<open>
1.1163 +\<close>
1.1164 +ML \<open>
1.1165 +\<close>
1.1166 +ML \<open>
1.1167 +\<close>
1.1168 +ML \<open>
1.1169 +\<close>
1.1170 +ML \<open>
1.1171 +\<close>
1.1172 +ML \<open>
1.1173 +\<close>
1.1174
1.1175 -text{*\noindent As a last step we check the tracing output of the last calc
1.1176 - tree instruction and compare it with the pre-calculated result.*}
1.1177 +text\<open>\noindent As a last step we check the tracing output of the last calc
1.1178 + tree instruction and compare it with the pre-calculated result.\<close>
1.1179
1.1180 -section {* Improve and Transfer into Knowledge *}
1.1181 -text {*
1.1182 +section \<open>Improve and Transfer into Knowledge\<close>
1.1183 +text \<open>
1.1184 We want to improve the very long program \ttfamily InverseZTransform
1.1185 \normalfont by modularisation: partial fraction decomposition shall
1.1186 become a sub-problem.
1.1187 @@ -1538,10 +1538,10 @@
1.1188 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
1.1189 \normalfont and the respective tests to:
1.1190 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
1.1191 -*}
1.1192 +\<close>
1.1193
1.1194 -subsection {* Transfer to Partial\_Fractions.thy *}
1.1195 -text {*
1.1196 +subsection \<open>Transfer to Partial\_Fractions.thy\<close>
1.1197 +text \<open>
1.1198 First we transfer both, knowledge and tests into:
1.1199 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
1.1200 in order to immediately have the test results.
1.1201 @@ -1559,10 +1559,10 @@
1.1202 \normalfont\\ and cut out the respective part from the program. First we ensure that
1.1203 the string is correct. When we insert the string into (2)
1.1204 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
1.1205 -*}
1.1206 +\<close>
1.1207
1.1208 -subsubsection {* 'Programming' in ISAC's TP-based Language *}
1.1209 -text {*
1.1210 +subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
1.1211 +text \<open>
1.1212 At the present state writing programs in {\sisac} is particularly cumbersome.
1.1213 So we give hints how to cope with the many obstacles. Below we describe the
1.1214 steps we did in making (2) run.
1.1215 @@ -1604,12 +1604,12 @@
1.1216 test are performed simplest in a file which is loaded with Isac.
1.1217 See \ttfamily tests/../partial\_fractions.sml \normalfont.
1.1218 \end{enumerate}
1.1219 -*}
1.1220 +\<close>
1.1221
1.1222 -subsection {* Transfer to Inverse\_Z\_Transform.thy *}
1.1223 -text {*
1.1224 +subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
1.1225 +text \<open>
1.1226 It was not possible to complete this task, because we ran out of time.
1.1227 -*}
1.1228 +\<close>
1.1229
1.1230
1.1231 end