wneuper/isa: comparison test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z

equal deleted inserted replaced

-:f2b3681fafb9
+:3e904f8ec16c
 theory Build_Inverse_Z_Transform imports Isac.Inverse_Z_Transform
 begin
-text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
+text\<open>We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
 exercise. Because Subsection~\ref{sec:stepcheck} requires
 \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
 Inverse\_Z\_Transform imports Isac \normalfont to the above one.
 \par \noindent
 \end{center}
 Here in this theory there are the internal names twice, for instance we have
 \ttfamily (Thm.derivation\_name @{thm rule1} =
 "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont
 but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont
-*}
+\<close>
-section {*Trials towards the Z-Transform\label{sec:trials}*}
+section \<open>Trials towards the Z-Transform\label{sec:trials}\<close>
-ML {*val thy = @{theory};*}
+ML \<open>val thy = @{theory};\<close>
-subsection {*Notations and Terms*}
+subsection \<open>Notations and Terms\<close>
-text{*\noindent Try which notations we are able to use.*}
+text\<open>\noindent Try which notations we are able to use.\<close>
-ML {*
+ML \<open>
 @{term "1 < || z ||"};
 @{term "z / (z - 1)"};
 @{term "-u -n - 1"};
 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
 @{term "z /(z - 1) = -u [-n - 1]"};
 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
-*}
+\<close>
-text{*\noindent Try which symbols we are able to use and how we generate them.*}
+text\<open>\noindent Try which symbols we are able to use and how we generate them.\<close>
-ML {*
+ML \<open>
 (*alpha -->  "</alpha>" *)
 @{term "\<alpha> "};
 @{term "\<delta> "};
 @{term "\<phi> "};
 @{term "\<rho> "};
 term2str @{term "\<rho> "};
-*}
+\<close>
-subsection {*Rules*}
+subsection \<open>Rules\<close>
 (*axiomatization "z / (z - 1) = -u [-n - 1]"
 Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
 (*definition     "z / (z - 1) = -u [-n - 1]"
 Bad head of lhs: existing constant "op /"*)
 axiomatization where
 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
-text{*\noindent Check the rules for their correct notation.
+text\<open>\noindent Check the rules for their correct notation.
-(See the machine output.)*}
+(See the machine output.)\<close>
-ML {*
+ML \<open>
 @{thm rule1};
 @{thm rule2};
 @{thm rule3};
 @{thm rule4};
-*}
+\<close>
-subsection {*Apply Rules*}
+subsection \<open>Apply Rules\<close>
-text{*\noindent We try to apply the rules to a given expression.*}
+text\<open>\noindent We try to apply the rules to a given expression.\<close>
-ML {*
+ML \<open>
 val inverse_Z = append_rls "inverse_Z" e_rls
 [ Thm  ("rule3",TermC.num_str @{thm rule3}),
 Thm  ("rule4",TermC.num_str @{thm rule4}),
 Thm  ("rule1",TermC.num_str @{thm rule1})
 ];
 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
 (*
 * Attention rule1 is applied before the expression is
 * checked for rule4 which would be correct!!!
 *)
-*}
+\<close>
-ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}
+ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
-ML {*
+ML \<open>
 val SOME (t, asm1) =
 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
 (*- real *)
 term2str t;
 val SOME (t, asm3) =
 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;
 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
 (*- real *)
 term2str t;
-*}
+\<close>
-ML {* terms2str (asm1 @ asm2 @ asm3); *}
+ML \<open>terms2str (asm1 @ asm2 @ asm3);\<close>
-section{*Prepare Steps for TP-based programming Language\label{sec:prepstep}*}
+section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
-text{*
+text\<open>
 \par \noindent The following sections are challenging with the CTP-based
 possibilities of building the program. The goal is realized in
 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
 \par The reader is advised to jump between the subsequent subsections and
 the respective steps in Section~\ref{prog-steps}. By comparing
 Section~\ref{sec:calc:ztrans} the calculation can be comprehended step
 by step.
-*}
+\<close>
-subsection {*Prepare Expression\label{prep-expr}*}
+subsection \<open>Prepare Expression\label{prep-expr}\<close>
-text{*\noindent We try two different notations and check which of them
+text\<open>\noindent We try two different notations and check which of them
-Isabelle can handle best.*}
+Isabelle can handle best.\<close>
-ML {*
+ML \<open>
 val ctxt = Proof_Context.init_global @{theory};
 val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;
 val SOME fun1 =
 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
 val SOME fun1' =
 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
-*}
+\<close>
-subsubsection {*Prepare Numerator and Denominator*}
+subsubsection \<open>Prepare Numerator and Denominator\<close>
-text{*\noindent The partial fraction decomposition is only possible if we
+text\<open>\noindent The partial fraction decomposition is only possible if we
 get the bound variable out of the numerator. Therefor we divide
 the expression by $z$. Follow up the Calculation at
-Section~\ref{sec:calc:ztrans} line number 02.*}
+Section~\ref{sec:calc:ztrans} line number 02.\<close>
 axiomatization where
 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
-ML {*
+ML \<open>
 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
 val SOME (fun2, asm1) =
 Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1; term2str fun2;
 val SOME (fun2', asm1) =
 Rewrite.rewrite_ thy ro er true  @{thm ruleZY} fun1'; term2str fun2';
 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
 term2str fun3';
 (*
 * OK - workaround!
 *)
-*}
+\<close>
-subsubsection {*Get the Argument of the Expression X'*}
+subsubsection \<open>Get the Argument of the Expression X'\<close>
-text{*\noindent We use \texttt{grep} for finding possibilities how we can
+text\<open>\noindent We use \texttt{grep} for finding possibilities how we can
 extract the bound variable in the expression. \ttfamily Atools.thy,
 Tools.thy \normalfont contain general utilities: \ttfamily
 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
 \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
 witch can be used in a script. Lookup this files how to build
 and handle such functions.
 \par The next section shows how to introduce such a function.
-*}
+\<close>
-subsubsection{*Decompose the Given Term Into lhs and rhs*}
+subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
-ML {*
+ML \<open>
 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
 val (_, denom) =
 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
-*}
+\<close>
-text{*\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
+text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
 the left or the right part of an equation.} in the Script language, but
-we need a function which gets the denominator of a fraction.*}
+we need a function which gets the denominator of a fraction.\<close>
-subsubsection{*Get the Denominator and Numerator out of a Fraction*}
+subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
-text{*\noindent The self written functions in e.g. \texttt{get\_denominator}
+text\<open>\noindent The self written functions in e.g. \texttt{get\_denominator}
-should become a constant for the Isabelle parser:*}
+should become a constant for the Isabelle parser:\<close>
 consts
 get_denominator :: "real => real"
 get_numerator :: "real => real"
-text {*\noindent With the above definition we run into problems when we parse
+text \<open>\noindent With the above definition we run into problems when we parse
 the Script \texttt{InverseZTransform}. This leads to \em ambiguous
 parse trees. \normalfont We avoid this by moving the definition
 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
 \par \noindent ATTENTION: From now on \ttfamily
 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
 it only works due to re-building {\sisac} several times (indicated
 explicitly).
-*}
+\<close>
-ML {*
+ML \<open>
 (*
 *("get_denominator",
 *  ("Rational.get_denominator", eval_get_denominator ""))
 *)
 fun eval_get_denominator (thmid:string) _
 (Const ("Rings.divide_class.divide", _) $num
 $denom)) thy =
 SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
 	        HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
 | eval_get_denominator _ _ _ _ = NONE;
-*}
+\<close>
-text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
+text \<open>\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
-see \ttfamily test/Knowledge/rational.sml\normalfont*}
+see \ttfamily test/Knowledge/rational.sml\normalfont\<close>
-text {*\noindent \ttfamily get\_numerator \normalfont should also become a
+text \<open>\noindent \ttfamily get\_numerator \normalfont should also become a
 constant for the Isabelle parser, follow up the \texttt{const}
-declaration above.*}
+declaration above.\<close>
-ML {*
+ML \<open>
 (*
 *("get_numerator",
 *  ("Rational.get_numerator", eval_get_numerator ""))
 *)
 fun eval_get_numerator (thmid:string) _
 (Const ("Rings.divide_class.divide", _) $num
 $denom )) thy =
 SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
 	        HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
 | eval_get_numerator _ _ _ _ = NONE;
-*}
+\<close>
-text {*\noindent We discovered several problems by implementing the
+text \<open>\noindent We discovered several problems by implementing the
 \ttfamily get\_numerator \normalfont function. Remember when
 putting new functions to {\sisac}, put them in a thy file and rebuild
-{\sisac}, also put them in the ruleset for the script!*}
+{\sisac}, also put them in the ruleset for the script!\<close>
-subsection {*Solve Equation\label{sec:solveq}*}
+subsection \<open>Solve Equation\label{sec:solveq}\<close>
-text {*\noindent We have to find the zeros of the term, therefor we use our
+text \<open>\noindent We have to find the zeros of the term, therefor we use our
 \ttfamily get\_denominator \normalfont function from the step before
 and try to solve the second order equation. (Follow up the Calculation
 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
 equation is too general for the present program.
 \par We know that this equation can be categorized as \em univariate
 equation \normalfont and solved with the functions {\sisac} provides
 for this equation type. Later on {\sisac} should determine the type
-of the given equation self.*}
+of the given equation self.\<close>
-ML {*
+ML \<open>
 val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
 "solveFor z",
 "solutions L"];
 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
-*}
+\<close>
-text {*\noindent Check if the given equation matches the specification of this
+text \<open>\noindent Check if the given equation matches the specification of this
-equation type.*}
+equation type.\<close>
-ML {*
+ML \<open>
 Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
-*}
+\<close>
-text{*\noindent We switch up to the {\sisac} Context and try to solve the
+text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
-equation with a more specific type definition.*}
+equation with a more specific type definition.\<close>
-ML {*
+ML \<open>
 Context.theory_name thy = "Isac";
 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
 val fmz =                                             (*specification*)
 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
 "solveFor z",                                      (*bound variable*)
 solution*)
 val (dI',pI',mI') =
 ("Isac",
 ["abcFormula","degree_2","polynomial","univariate","equation"],
 ["no_met"]);
-*}
+\<close>
-text {*\noindent Check if the (other) given equation matches the
+text \<open>\noindent Check if the (other) given equation matches the
-specification of this equation type.*}
+specification of this equation type.\<close>
-ML {*
+ML \<open>
 Specify.match_pbl fmz (Specify.get_pbt
 ["abcFormula","degree_2","polynomial","univariate","equation"]);
-*}
+\<close>
-text {*\noindent We stepwise solve the equation. This is done by the
+text \<open>\noindent We stepwise solve the equation. This is done by the
-use of a so called calc tree seen downwards.*}
+use of a so called calc tree seen downwards.\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*
 * [z = 1 / 2, z = -1 / 4]
 *)
 Chead.show_pt pt;
 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
-*}
+\<close>
-subsection {*Partial Fraction Decomposition\label{sec:pbz}*}
+subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
-text{*\noindent We go on with the decomposition of our expression. Follow up the
+text\<open>\noindent We go on with the decomposition of our expression. Follow up the
 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
-Subproblem~1.*}
+Subproblem~1.\<close>
-subsubsection {*Solutions of the Equation*}
+subsubsection \<open>Solutions of the Equation\<close>
-text{*\noindent We get the solutions of the before solved equation in a list.*}
+text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
-ML {*
+ML \<open>
 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
 term2str solutions;
 atomty solutions;
-*}
+\<close>
-subsubsection {*Get Solutions out of a List*}
+subsubsection \<open>Get Solutions out of a List\<close>
-text {*\noindent In {\sisac}'s TP-based programming language:
+text \<open>\noindent In {\sisac}'s TP-based programming language:
 \begin{verbatim}
 let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $
 \end{verbatim}
 can be useful.
-*}
+\<close>
-ML {*
+ML \<open>
 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
 term2str s_1;
 term2str s_2;
-*}
+\<close>
-text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
+text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
 requires to get the denominators of the partial fractions out of the
 Solutions as:
 \begin{itemize}
 \item $Denominator_{1}=z-Zeropoint_{1}$
 \item $Denominator_{2}=z-Zeropoint_{2}$
 \item \ldots
 \end{itemize}
-*}
+\<close>
-ML {*
+ML \<open>
 val xx = HOLogic.dest_eq s_1;
 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
 val xx = HOLogic.dest_eq s_2;
 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
 term2str s_1';
 term2str s_2';
-*}
+\<close>
-text {*\noindent For the programming language a function collecting all the
+text \<open>\noindent For the programming language a function collecting all the
-above manipulations is helpful.*}
+above manipulations is helpful.\<close>
-ML {*
+ML \<open>
 fun fac_from_sol s =
 let val (lhs, rhs) = HOLogic.dest_eq s
 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
-*}
+\<close>
-ML {*
+ML \<open>
 fun mk_prod prod [] =
 if prod = e_term
 then error "mk_prod called with []"
 else prod
 | mk_prod prod (t :: []) =
 in mk_prod p ts end
 else
 let val p =
 HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
 in mk_prod p (t2 :: ts) end
-*}
+\<close>
 (* ML {*
 probably keep these test in test/Tools/isac/...
 (*mk_prod e_term [];*)
 val prod = mk_prod e_term [str2term "x + 123"];
 val prod =
 mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
 term2str prod = "(x + 1) * (x + 2) * (x + 3)";
 *} *)
-ML {*
+ML \<open>
 fun factors_from_solution sol =
 let val ts = HOLogic.dest_list sol
 in mk_prod e_term (map fac_from_sol ts) end;
-*}
+\<close>
 (* ML {*
 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
 val fs = factors_from_solution sol;
 term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
 *} *)
-text {*\noindent This function needs to be packed such that it can be evaluated
+text \<open>\noindent This function needs to be packed such that it can be evaluated
 by the Lucas-Interpreter. Therefor we moved the function to the
 corresponding \ttfamily Equation.thy \normalfont in our case
 \ttfamily PartialFractions.thy \normalfont. The necessary steps
 are quit the same as we have done with \ttfamily get\_denominator
-\normalfont before.*}
+\normalfont before.\<close>
-ML {*
+ML \<open>
 (*("factors_from_solution",
 ("Partial_Fractions.factors_from_solution",
 eval_factors_from_solution ""))*)
 fun eval_factors_from_solution (thmid:string) _
 in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
 Trueprop $ (mk_equality (t, prod)))
 end)
 handle _ => NONE)
 | eval_factors_from_solution _ _ _ _ = NONE;
-*}
+\<close>
-text {*\noindent The tracing output of the calc tree after applying this
+text \<open>\noindent The tracing output of the calc tree after applying this
 function was:
 \begin{verbatim}
 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]
 \end{verbatim}
 and the next step:
 val nxt = ("Empty_Tac", ...): tac'_)
 \end{verbatim}
 These observations indicate, that the Lucas-Interpreter (LIP)
 does not know how to evaluate \ttfamily factors\_from\_solution
 \normalfont, so we knew that there is something wrong or missing.
-*}
+\<close>
-text{*\noindent First we isolate the difficulty in the program as follows:
+text\<open>\noindent First we isolate the difficulty in the program as follows:
 \begin{verbatim}
 " (L_L::bool list) = (SubProblem (PolyEq',      " ^
 "   [abcFormula, degree_2, polynomial,          " ^
 "    univariate,equation],                      " ^
 "   [no_met])                                   " ^
 \begin{verbatim}
 val thy = @{theory "Inverse_Z_Transform"};
 \end{verbatim}
 After rebuilding {\sisac} again it worked.
-*}
+\<close>
-subsubsection {*Build Expression*}
+subsubsection \<open>Build Expression\<close>
-text {*\noindent In {\sisac}'s TP-based programming language we can build
+text \<open>\noindent In {\sisac}'s TP-based programming language we can build
 expressions by:\\
-\ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont*}
+\ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\<close>
-ML {*
+ML \<open>
 (*
 * The main denominator is the multiplication of the denominators of
 * all partial fractions.
 *)
 val SOME numerator = parseNEW ctxt "3::real";
 val expr' = HOLogic.mk_binop
 "Rings.divide_class.divide" (numerator, denominator');
 term2str expr';
-*}
+\<close>
-subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}
+subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
-text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our
+text\<open>\noindent We use the Ansatz of the Partial Fraction Decomposition for our
 expression 2nd order. Follow up the calculation in
-Section~\ref{sec:calc:ztrans} Step~03.*}
+Section~\ref{sec:calc:ztrans} Step~03.\<close>
-ML {*Context.theory_name thy = "Isac"*}
+ML \<open>Context.theory_name thy = "Isac"\<close>
-text{*\noindent We define two axiomatization, the first one is the main ansatz,
+text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
 the next one is just an equivalent transformation of the resulting
 equation. Both axiomatizations were moved to \ttfamily
 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
 programs it is possible to use the rulesets and the machine will find
-the correct ansatz and equivalent transformation itself.*}
+the correct ansatz and equivalent transformation itself.\<close>
 axiomatization where
 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
-text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
+text\<open>\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
 our expression and get an equation with our expression on the left
-and the partial fractions of it on the right hand side.*}
+and the partial fractions of it on the right hand side.\<close>
-ML {*
+ML \<open>
 val SOME (t1,_) =
 rewrite_ @{theory} e_rew_ord e_rls false
 @{thm ansatz_2nd_order} expr';
 term2str t1; atomty t1;
 val eq1 = HOLogic.mk_eq (expr', t1);
 term2str eq1;
-*}
+\<close>
-text{*\noindent Eliminate the denominators by multiplying the left and the
+text\<open>\noindent Eliminate the denominators by multiplying the left and the
 right hand side of the equation with the main denominator. This is an
 simple equivalent transformation. Later on we use an own ruleset
 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
-Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.*}
+Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\<close>
-ML {*
+ML \<open>
 val SOME (eq2,_) =
 rewrite_ @{theory} e_rew_ord e_rls false
 @{thm equival_trans_2nd_order} eq1;
 term2str eq2;
-*}
+\<close>
-text{*\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
+text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
-for simplifications on expressions.*}
+for simplifications on expressions.\<close>
-ML {*
+ML \<open>
 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
 term2str eq3;
 (*
 * ?A ?B not simplified
 *)
-*}
+\<close>
-text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
+text\<open>\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
 simplifications. The problem that we would like to have only a specific degree
-of simplification occurs right here, in the next step.*}
+of simplification occurs right here, in the next step.\<close>
-ML {*
+ML \<open>
 trace_rewrite := false;
 val SOME fract1 =
 parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
 (*
 * A B !
 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
 (*
 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
 * would be more traditional...
 *)
-*}
+\<close>
-text{*\noindent We walk around this problem by generating our new equation first.*}
+text\<open>\noindent We walk around this problem by generating our new equation first.\<close>
-ML {*
+ML \<open>
 val (numerator, denominator) = HOLogic.dest_eq eq3;
 val eq3' = HOLogic.mk_eq (numerator, fract1);
 (*
 * A B !
 *)
 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
 *)
 val SOME (eq3'' ,_) =
 rewrite_set_ @{theory} false norm_Rational eq3';
 term2str eq3'';
-*}
+\<close>
-text{*\noindent Still working at {\sisac}\ldots*}
+text\<open>\noindent Still working at {\sisac}\ldots\<close>
-ML {* Context.theory_name thy = "Isac" *}
+ML \<open>Context.theory_name thy = "Isac"\<close>
-subsubsection {*Build a Rule-Set for the Ansatz*}
+subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
-text {*\noindent The \emph{ansatz} rules violate the principle that each
+text \<open>\noindent The \emph{ansatz} rules violate the principle that each
 variable on the right-hand-side must also occur on the
 left-hand-side of the rule: A, B, etc. don't do that. Thus the
 rewriter marks these variables with question marks: ?A, ?B, etc.
 These question marks can be dropped by \ttfamily fun
-drop\_questionmarks\normalfont.*}
+drop\_questionmarks\normalfont.\<close>
-ML {*
+ML \<open>
 val ansatz_rls = prep_rls @{theory} (
 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
 erls = e_rls, srls = Erls, calc = [], errpatts = [],
 rules = [
 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
 ],
 scr = EmptyScr});
-*}
+\<close>
-text{*\noindent We apply the ruleset\ldots*}
+text\<open>\noindent We apply the ruleset\ldots\<close>
-ML {*
+ML \<open>
 val SOME (ttttt,_) =
 rewrite_set_ @{theory} false ansatz_rls expr';
-*}
+\<close>
-text{*\noindent And check the output\ldots*}
+text\<open>\noindent And check the output\ldots\<close>
-ML {*
+ML \<open>
 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
-*}
+\<close>
-subsubsection {*Get the First Coefficient*}
+subsubsection \<open>Get the First Coefficient\<close>
-text{*\noindent Now it's up to get the two coefficients A and B, which will be
+text\<open>\noindent Now it's up to get the two coefficients A and B, which will be
 the numerators of our partial fractions. Continue following up the
-Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
+Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\<close>
-text{*\noindent To get the first coefficient we substitute $z$ with the first
+text\<open>\noindent To get the first coefficient we substitute $z$ with the first
-zero-point we determined in Section~\ref{sec:solveq}.*}
+zero-point we determined in Section~\ref{sec:solveq}.\<close>
-ML {*
+ML \<open>
 val SOME (eq4_1,_) =
 rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
 term2str eq4_1;
 val SOME (eq4_2,_) =
 rewrite_set_ @{theory} false norm_Rational eq4_1;
 (*Check_Postcond ["normalise","polynomial",
 "univariate","equation"]*)
 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
 (*End_Proof'*)
 f2str fa;
-*}
+\<close>
-subsubsection {*Get Second Coefficient*}
+subsubsection \<open>Get Second Coefficient\<close>
-text{*\noindent With the use of \texttt{thy} we check which theories the
+text\<open>\noindent With the use of \texttt{thy} we check which theories the
-interpreter knows.*}
+interpreter knows.\<close>
-ML {*thy*}
+ML \<open>thy\<close>
-text{*\noindent To get the second coefficient we substitute $z$ with the second
+text\<open>\noindent To get the second coefficient we substitute $z$ with the second
-zero-point we determined in Section~\ref{sec:solveq}.*}
+zero-point we determined in Section~\ref{sec:solveq}.\<close>
-ML {*
+ML \<open>
 val SOME (eq4b_1,_) =
 rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
 term2str eq4b_1;
 val SOME (eq4b_2,_) =
 rewrite_set_ @{theory} false norm_Rational eq4b_1;
 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
 f2str fb;
-*}
+\<close>
-text{*\noindent We compare our results with the pre calculated upshot.*}
+text\<open>\noindent We compare our results with the pre calculated upshot.\<close>
-ML {*
+ML \<open>
 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
-*}
+\<close>
-section {*Implement the Specification and the Method \label{spec-meth}*}
+section \<open>Implement the Specification and the Method \label{spec-meth}\<close>
-text{*\noindent Now everything we need for solving the problem has been
+text\<open>\noindent Now everything we need for solving the problem has been
 tested out. We now start by creating new nodes for our methods and
-further on our new program in the interpreter.*}
+further on our new program in the interpreter.\<close>
-subsection{*Define the Field Descriptions for the
+subsection\<open>Define the Field Descriptions for the
-Specification\label{sec:deffdes}*}
+Specification\label{sec:deffdes}\<close>
-text{*\noindent We define the fields \em filterExpression \normalfont and
+text\<open>\noindent We define the fields \em filterExpression \normalfont and
 \em stepResponse \normalfont both as equations, they represent the in- and
-output of the program.*}
+output of the program.\<close>
 consts
 filterExpression  :: "bool => una"
 stepResponse      :: "bool => una"
-subsection{*Define the Specification*}
+subsection\<open>Define the Specification\<close>
-text{*\noindent The next step is defining the specifications as nodes in the
+text\<open>\noindent The next step is defining the specifications as nodes in the
 designated part. We have to create the hierarchy node by node and start
 with \em SignalProcessing \normalfont and go on by creating the node
-\em Z\_Transform\normalfont.*}
+\em Z\_Transform\normalfont.\<close>
-setup {* KEStore_Elems.add_pbts
+setup \<open>KEStore_Elems.add_pbts
 [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
-(["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
+(["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])]\<close>
-text{*\noindent For the suddenly created node we have to define the input
+text\<open>\noindent For the suddenly created node we have to define the input
 and output parameters. We already prepared their definition in
-Section~\ref{sec:deffdes}.*}
+Section~\ref{sec:deffdes}.\<close>
-setup {* KEStore_Elems.add_pbts
+setup \<open>KEStore_Elems.add_pbts
 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
 (["Inverse", "Z_Transform", "SignalProcessing"],
 [("#Given", ["filterExpression X_eq"]),
 ("#Find", ["stepResponse n_eq"])],
 append_rls "e_rls" e_rls [(*for preds in where_*)],
 NONE,
-[["SignalProcessing","Z_Transform","Inverse"]])] *}
+[["SignalProcessing","Z_Transform","Inverse"]])]\<close>
-ML {*
+ML \<open>
 show_ptyps ();
 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
-*}
+\<close>
-subsection {*Define Name and Signature for the Method*}
+subsection \<open>Define Name and Signature for the Method\<close>
-text{*\noindent As a next step we store the definition of our new method as a
+text\<open>\noindent As a next step we store the definition of our new method as a
-constant for the interpreter.*}
+constant for the interpreter.\<close>
 consts
 InverseZTransform :: "[bool, bool] => bool"
 ("((Script InverseZTransform (_ =))// (_))" 9)
-subsection {*Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}*}
+subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
-text{*\noindent Again we have to generate the nodes step by step, first the
+text\<open>\noindent Again we have to generate the nodes step by step, first the
 parent node and then the originally \em Z\_Transformation
 \normalfont node. We have to define both nodes first with an empty script
-as content.*}
+as content.\<close>
-setup {* KEStore_Elems.add_mets
+setup \<open>KEStore_Elems.add_mets
 [prep_met thy "met_SP" [] e_metID
 (["SignalProcessing"], [],
 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
 errpats = [], nrls = e_rls},
 "empty_script"),
 prep_met thy "met_SP_Ztrans" [] e_metID
 (["SignalProcessing", "Z_Transform"], [],
 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
 errpats = [], nrls = e_rls},
 "empty_script")]
-*}
+\<close>
-text{*\noindent After we generated both nodes, we can fill the containing
+text\<open>\noindent After we generated both nodes, we can fill the containing
 script we want to implement later. First we define the specifications
-of the script in e.g. the in- and output.*}
+of the script in e.g. the in- and output.\<close>
-setup {* KEStore_Elems.add_mets
+setup \<open>KEStore_Elems.add_mets
 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
 (["SignalProcessing", "Z_Transform", "Inverse"],
 [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
 errpats = [], nrls = e_rls},
 "empty_script")]
-*}
+\<close>
-text{*\noindent After we stored the definition we can start implementing the
+text\<open>\noindent After we stored the definition we can start implementing the
 script itself. As a first try we define only three rows containing one
-simple operation.*}
+simple operation.\<close>
-setup {* KEStore_Elems.add_mets
+setup \<open>KEStore_Elems.add_mets
 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
 (["SignalProcessing", "Z_Transform", "Inverse"],
 [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
 errpats = [], nrls = e_rls},
 "Script InverseZTransform (Xeq::bool) =" ^
 " (let X = Take Xeq;" ^
 "      X = Rewrite ruleZY False X" ^
 "  in X)")]
-*}
+\<close>
-text{*\noindent Check if the method has been stored correctly\ldots*}
+text\<open>\noindent Check if the method has been stored correctly\ldots\<close>
-ML {*
+ML \<open>
 show_mets();
-*}
+\<close>
-text{*\noindent If yes we can get the method by stepping backwards through
+text\<open>\noindent If yes we can get the method by stepping backwards through
-the hierarchy.*}
+the hierarchy.\<close>
-ML {*
+ML \<open>
 get_met ["SignalProcessing","Z_Transform","Inverse"];
-*}
+\<close>
-section {*Program in TP-based language \label{prog-steps}*}
+section \<open>Program in TP-based language \label{prog-steps}\<close>
-text{*\noindent We start stepwise expanding our program. The script is a
+text\<open>\noindent We start stepwise expanding our program. The script is a
 simple string containing several manipulation instructions.
 \par The first script we try contains no instruction, we only test if
-building scripts that way work.*}
+building scripts that way work.\<close>
-subsection {*Stepwise Extend the Program*}
+subsection \<open>Stepwise Extend the Program\<close>
-ML {*
+ML \<open>
 val str =
 "Script InverseZTransform (Xeq::bool) =                          "^
 " Xeq";
-*}
+\<close>
-text{*\noindent Next we put some instructions in the script and try if we are
+text\<open>\noindent Next we put some instructions in the script and try if we are
-able to solve our first equation.*}
+able to solve our first equation.\<close>
-ML {*
+ML \<open>
 val str =
 "Script InverseZTransform (Xeq::bool) =                          "^
 (*
 * 1/z) instead of z ^^^ -1
 *)
 "      X' = (SubProblem (Isac',[pqFormula,degree_2,              "^
 "                               polynomial,univariate,equation], "^
 "                              [no_met])                         "^
 "                              [BOOL e_e, REAL v_v])             "^
 "            in X)";
-*}
+\<close>
-text{*\noindent To solve the equation it is necessary to drop the left hand
+text\<open>\noindent To solve the equation it is necessary to drop the left hand
 side, now we only need the denominator of the right hand side. The first
-equation solves the zeros of our expression.*}
+equation solves the zeros of our expression.\<close>
-ML {*
+ML \<open>
 val str =
 "Script InverseZTransform (Xeq::bool) =                          "^
 " (let X = Take Xeq;                                             "^
 "      X' = Rewrite ruleZY False X;                              "^
 "      X' = (Rewrite_Set norm_Rational False) X';                "^
 "      funterm = rhs X'                                          "^
 (*
 * drop X'= for equation solving
 *)
 "  in X)";
-*}
+\<close>
-text{*\noindent As mentioned above, we need the denominator of the right hand
+text\<open>\noindent As mentioned above, we need the denominator of the right hand
 side. The equation itself consists of this denominator and tries to find
-a $z$ for this the denominator is equal to zero.*}
+a $z$ for this the denominator is equal to zero.\<close>
-ML {*
+ML \<open>
 val str =
 "Script InverseZTransform (X_eq::bool) =                         "^
 " (let X = Take X_eq;                                            "^
 "      X' = Rewrite ruleZY False X;                              "^
 "      X' = (Rewrite_Set norm_Rational False) X';                "^
 "  in X)";
 parse thy str;
 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
 atomty sc;
-*}
+\<close>
-text {*\noindent This ruleset contains all functions that are in the script;
+text \<open>\noindent This ruleset contains all functions that are in the script;
-The evaluation of the functions is done by rewriting using this ruleset.*}
+The evaluation of the functions is done by rewriting using this ruleset.\<close>
-ML {*
+ML \<open>
 val srls =
 Rls {id="srls_InverseZTransform",
 preconds = [],
 rew_ord = ("termlessI",termlessI),
 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
 "#factors_from_solution"),
 Calc("Partial_Fractions.drop_questionmarks",
 eval_drop_questionmarks "#drop_?")
 ],
 scr = EmptyScr};
-*}
+\<close>
-subsection {*Store Final Version of Program for Execution*}
+subsection \<open>Store Final Version of Program for Execution\<close>
-text{*\noindent After we also tested how to write scripts and run them,
+text\<open>\noindent After we also tested how to write scripts and run them,
 we start creating the final version of our script and store it into
 the method for which we created a node in Section~\ref{sec:cparentnode}
 Note that we also did this stepwise, but we didn't kept every
-subversion.*}
+subversion.\<close>
-setup {* KEStore_Elems.add_mets
+setup \<open>KEStore_Elems.add_mets
 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
 (["SignalProcessing", "Z_Transform", "Inverse"],
 [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
 errpats = [], nrls = e_rls},
 "      (X_z::bool) = Take (X_z = pbz);                          "^
 "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^
 "      n_eq = drop_questionmarks n_eq                           "^
 "in n_eq)")]
-*}
+\<close>
-subsection {*Check the Program*}
+subsection \<open>Check the Program\<close>
-text{*\noindent When the script is ready we can start checking our work.*}
+text\<open>\noindent When the script is ready we can start checking our work.\<close>
-subsubsection {*Check the Formalization*}
+subsubsection \<open>Check the Formalization\<close>
-text{*\noindent First we want to check the formalization of the in and
+text\<open>\noindent First we want to check the formalization of the in and
-output of our program.*}
+output of our program.\<close>
-ML {*
+ML \<open>
 val fmz =
 ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
 "stepResponse (x[n::real]::bool)"];
 val (dI,pI,mI) =
 ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
 val Prog sc
 = (#scr o get_met) ["SignalProcessing",
 "Z_Transform",
 "Inverse"];
 atomty sc;
-*}
+\<close>
-subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
+subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>
-text{*\noindent We start to stepwise execute our new program in a calculation
+text\<open>\noindent We start to stepwise execute our new program in a calculation
-tree and check if every node implements that what we have wanted.*}
+tree and check if every node implements that what we have wanted.\<close>
-ML {*
+ML \<open>
 trace_rewrite := false; (*true*)
 trace_script := false; (*true*)
 print_depth 9;
 val fmz =
 "Rewrite_Set norm_Rational";
 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 "SubProblem";
 print_depth 3;
-*}
+\<close>
-text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
+text \<open>\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
 the following points:\begin{itemize}
 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
 \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
 The calculation is ok but no \ttfamily next \normalfont step found:
 \end{verbatim}
 \ldots shows the right script. Difference in the arguments.
 \item Test --- Why helpless here ? --- shows: \ttfamily replace
 no\_meth by [no\_meth] \normalfont in Script
 \end{itemize}
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Model_Problem";*)
-*}
+\<close>
-text {*\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
+text \<open>\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above
 we had \ttfamily Empty\_Tac; \normalfont the search for the reason
 considered the following points:\begin{itemize}
 \item Difference in the arguments
 \item Comparison with Subsection~\ref{sec:solveq}: There solving this
 equation works, so there must be some difference in the arguments
 of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont
 instead of \ttfamily [no\_met] \normalfont ;-)
-\end{itemize}*}
+\end{itemize}\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Add_Given solveFor z";*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Add_Find solutions z_i";*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Specify_Theory Isac";*)
-*}
+\<close>
-text {*\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
+text \<open>\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory;
 \normalfont The search for the reason considered the following points:
 \begin{itemize}
 \item Was there an error message? NO -- ok
 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\
 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
 {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}
 }
 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
 selection of the appropriate type to isac as done in the final Script ;-))
-\end{itemize}*}
+\end{itemize}\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Specify_Problem [abcFormula,...";*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*)
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 trace_script := true;
-*}
+\<close>
-ML {*
+ML \<open>
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
+\<close>
-ML {*
+ML \<open>
 Chead.show_pt pt;
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-ML {*
+ML \<open>
-*}
+\<close>
-text{*\noindent As a last step we check the tracing output of the last calc
+text\<open>\noindent As a last step we check the tracing output of the last calc
-tree instruction and compare it with the pre-calculated result.*}
+tree instruction and compare it with the pre-calculated result.\<close>
-section {* Improve and Transfer into Knowledge *}
+section \<open>Improve and Transfer into Knowledge\<close>
-text {*
+text \<open>
 We want to improve the very long program \ttfamily InverseZTransform
 \normalfont by modularisation: partial fraction decomposition shall
 become a sub-problem.
 We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
 \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont),
 and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
 \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
 \normalfont and the respective tests to:
 \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center}
-*}
+\<close>
-subsection {* Transfer to Partial\_Fractions.thy *}
+subsection \<open>Transfer to Partial\_Fractions.thy\<close>
-text {*
+text \<open>
 First we transfer both, knowledge and tests into:
 \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center}
 in order to immediately have the test results.
 We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\
 \normalfont\\ to\\
 (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv"
 \normalfont\\ and cut out the respective part from the program. First we ensure that
 the string is correct. When we insert the string into (2)
 \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error.
-*}
+\<close>
-subsubsection {* 'Programming' in ISAC's TP-based Language *}
+subsubsection \<open>'Programming' in ISAC's TP-based Language\<close>
-text {*
+text \<open>
 At the present state writing programs in {\sisac} is particularly cumbersome.
 So we give hints how to cope with the many obstacles. Below we describe the
 steps we did in making (2) run.
 \begin{enumerate}
 of the program. Evaluation is done by the Lucas-Interpreter, which works
 using the knowledge in theory Isac; so we have to re-build Isac. And the
 test are performed simplest in a file which is loaded with Isac.
 See \ttfamily tests/../partial\_fractions.sml \normalfont.
 \end{enumerate}
-*}
+\<close>
-subsection {* Transfer to Inverse\_Z\_Transform.thy *}
+subsection \<open>Transfer to Inverse\_Z\_Transform.thy\<close>
-text {*
+text \<open>
 It was not possible to complete this task, because we ran out of time.
-*}
+\<close>
 end

changeset 59472	3e904f8ec16c
parent 59465	b33dc41f4350
child 59476	863c3629ad24