neuper@42301: (* Title: Build_Inverse_Z_Transform neuper@42279: Author: Jan Rocnik neuper@42376: (c) copyright due to license terms. neuper@42279: *) neuper@42279: wneuper@59465: theory Build_Inverse_Z_Transform imports Isac.Inverse_Z_Transform neuper@42289: neuper@42289: begin neuper@42279: wneuper@59472: text\We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an jan@42381: exercise. Because Subsection~\ref{sec:stepcheck} requires jan@42371: \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily jan@42368: Isac.thy\normalfont, the setup has been changed from \ttfamily theory jan@42371: Inverse\_Z\_Transform imports Isac \normalfont to the above one. jan@42368: \par \noindent jan@42368: \begin{center} jan@42381: \textbf{Attention with the names of identifiers when going into internals!} jan@42368: \end{center} jan@42368: Here in this theory there are the internal names twice, for instance we have jan@42368: \ttfamily (Thm.derivation\_name @{thm rule1} = jan@42368: "Build\_Inverse\_Z\_Transform.rule1") = true; \normalfont jan@42368: but actually in us will be \ttfamily Inverse\_Z\_Transform.rule1 \normalfont wneuper@59472: \ neuper@42279: wneuper@59472: section \Trials towards the Z-Transform\label{sec:trials}\ jan@42368: wneuper@59472: ML \val thy = @{theory};\ neuper@42279: wneuper@59472: subsection \Notations and Terms\ wneuper@59472: text\\noindent Try which notations we are able to use.\ wneuper@59472: ML \ jan@42368: @{term "1 < || z ||"}; jan@42368: @{term "z / (z - 1)"}; jan@42368: @{term "-u -n - 1"}; jan@42368: @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*) neuper@42389: @{term "z /(z - 1) = -u [-n - 1]"}; jan@42368: @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"}; walther@59868: UnparseC.term @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"}; wneuper@59472: \ wneuper@59472: text\\noindent Try which symbols we are able to use and how we generate them.\ wneuper@59472: ML \ jan@42368: (*alpha --> "" *) jan@42368: @{term "\ "}; jan@42368: @{term "\ "}; jan@42368: @{term "\ "}; jan@42368: @{term "\ "}; walther@59868: UnparseC.term @{term "\ "}; wneuper@59472: \ neuper@42279: wneuper@59472: subsection \Rules\ jan@42368: (*axiomatization "z / (z - 1) = -u [-n - 1]" jan@42368: Illegal variable name: "z / (z - 1) = -u [-n - 1]" *) jan@42368: (*definition "z / (z - 1) = -u [-n - 1]" jan@42368: Bad head of lhs: existing constant "op /"*) neuper@42279: axiomatization where neuper@42279: rule1: "1 = \[n]" and neuper@42279: rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and neuper@42279: rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and walther@60242: rule4: "|| z || > || \ || ==> z / (z - \) = \ \ n * u [n]" and walther@60242: rule5: "|| z || < || \ || ==> z / (z - \) = -(\ \ n) * u [-n - 1]" and walther@60242: rule6: "|| z || > 1 ==> z/(z - 1) \ 2 = n * u [n]" jan@42368: wneuper@59472: text\\noindent Check the rules for their correct notation. wneuper@59472: (See the machine output.)\ wneuper@59472: ML \ jan@42368: @{thm rule1}; jan@42368: @{thm rule2}; jan@42368: @{thm rule3}; jan@42368: @{thm rule4}; wneuper@59472: \ neuper@42279: wneuper@59472: subsection \Apply Rules\ wneuper@59472: text\\noindent We try to apply the rules to a given expression.\ jan@42368: wneuper@59472: ML \ walther@60278: val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls wenzelm@60297: [ \<^rule_thm>\rule3\, wenzelm@60297: \<^rule_thm>\rule4\, wenzelm@60297: \<^rule_thm>\rule1\ jan@42368: ]; neuper@42279: walther@60278: \ ML \ Walther@60565: val t = TermC.parse_test @{context} "z / (z - 1) + z / (z - \) + 1::real"; walther@60278: \ ML \ wneuper@59395: val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t; walther@60336: (*rewrite__set_ called with 'Erls' for '|| z || < 1'*) walther@60336: \ ML \ walther@59868: UnparseC.term t' = "z / (z - ?\ [?n]) + z / (z - \) + ?\ [?n]"; jan@42368: (* jan@42368: * Attention rule1 is applied before the expression is jan@42368: * checked for rule4 which would be correct!!! jan@42368: *) walther@60278: \ ML \ wneuper@59472: \ neuper@42279: wneuper@59472: ML \val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\ wneuper@59472: ML \ jan@42368: val SOME (t, asm1) = walther@59871: Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule3}) t; walther@59868: UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \) + 1"; jan@42368: (*- real *) walther@59868: UnparseC.term t; jan@42296: jan@42368: val SOME (t, asm2) = walther@59871: Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t; walther@60242: UnparseC.term t = "- ?u [- ?n - 1] + \ \ ?n * ?u [?n] + 1"; jan@42368: (*- real *) walther@59868: UnparseC.term t; jan@42296: jan@42368: val SOME (t, asm3) = walther@59871: Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t; walther@60242: UnparseC.term t = "- ?u [- ?n - 1] + \ \ ?n * ?u [?n] + ?\ [?n]"; jan@42368: (*- real *) walther@59868: UnparseC.term t; wneuper@59472: \ walther@59868: ML \UnparseC.terms (asm1 @ asm2 @ asm3);\ jan@42296: wneuper@59472: section\Prepare Steps for TP-based programming Language\label{sec:prepstep}\ wneuper@59472: text\ neuper@42376: \par \noindent The following sections are challenging with the CTP-based neuper@42376: possibilities of building the program. The goal is realized in jan@42368: Section~\ref{spec-meth} and Section~\ref{prog-steps}. jan@42368: \par The reader is advised to jump between the subsequent subsections and jan@42368: the respective steps in Section~\ref{prog-steps}. By comparing jan@42368: Section~\ref{sec:calc:ztrans} the calculation can be comprehended step jan@42368: by step. wneuper@59472: \ neuper@42279: wneuper@59472: subsection \Prepare Expression\label{prep-expr}\ wneuper@59472: text\\noindent We try two different notations and check which of them wneuper@59472: Isabelle can handle best.\ wneuper@59472: ML \ neuper@48761: val ctxt = Proof_Context.init_global @{theory}; wneuper@59582: (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*) jan@42368: jan@42368: val SOME fun1 = walther@60242: TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \ -1)"; UnparseC.term fun1; jan@42368: val SOME fun1' = walther@59868: TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1'; wneuper@59472: \ jan@42368: wneuper@59472: subsubsection \Prepare Numerator and Denominator\ wneuper@59472: text\\noindent The partial fraction decomposition is only possible if we jan@42368: get the bound variable out of the numerator. Therefor we divide jan@42368: the expression by $z$. Follow up the Calculation at wneuper@59472: Section~\ref{sec:calc:ztrans} line number 02.\ jan@42368: neuper@42279: axiomatization where neuper@42279: ruleZY: "(X z = a / b) = (X' z = a / (z * b))" neuper@42279: wneuper@59472: ML \ neuper@42384: val (thy, ro, er) = (@{theory}, tless_true, eval_rls); jan@42368: val SOME (fun2, asm1) = walther@59868: Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; UnparseC.term fun2; jan@42368: val SOME (fun2', asm1) = walther@59868: Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term fun2'; neuper@42279: jan@42368: val SOME (fun3,_) = wneuper@59395: Rewrite.rewrite_set_ @{theory} false norm_Rational fun2; walther@59868: UnparseC.term fun3; jan@42368: (* walther@60242: * Fails on x \ (-1) jan@42368: * We solve this problem by using 1/x as a workaround. jan@42368: *) jan@42368: val SOME (fun3',_) = wneuper@59395: Rewrite.rewrite_set_ @{theory} false norm_Rational fun2'; walther@59868: UnparseC.term fun3'; jan@42368: (* jan@42368: * OK - workaround! jan@42368: *) wneuper@59472: \ neuper@42279: wneuper@59472: subsubsection \Get the Argument of the Expression X'\ wneuper@59472: text\\noindent We use \texttt{grep} for finding possibilities how we can walther@59603: extract the bound variable in the expression. \ttfamily Prog_Expr.thy, jan@42368: Tools.thy \normalfont contain general utilities: \ttfamily jan@42368: eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont jan@42368: \ttfamily grep -r "fun eva\_" * \normalfont shows all functions jan@42371: witch can be used in a script. Lookup this files how to build jan@42368: and handle such functions. jan@42368: \par The next section shows how to introduce such a function. wneuper@59472: \ jan@42298: wneuper@59472: subsubsection\Decompose the Given Term Into lhs and rhs\ wneuper@59472: ML \ walther@59868: val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr; jan@42368: val (_, denom) = wenzelm@60309: HOLogic.dest_bin \<^const_name>\divide\ (type_of expr) expr; walther@60242: UnparseC.term denom = "-1 + -2 * z + 8 * z \ 2"; wneuper@59472: \ jan@42298: wneuper@59472: text\\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side jan@42370: \normalfont and rhs means \em Right Hand Side \normalfont and indicates wneuper@59585: the left or the right part of an equation.} in the Program language, but wneuper@59472: we need a function which gets the denominator of a fraction.\ jan@42298: wneuper@59472: subsubsection\Get the Denominator and Numerator out of a Fraction\ wneuper@59472: text\\noindent The self written functions in e.g. \texttt{get\_denominator} wneuper@59472: should become a constant for the Isabelle parser:\ jan@42298: jan@42298: consts jan@42345: get_denominator :: "real => real" jan@42344: get_numerator :: "real => real" jan@42298: wneuper@59472: text \\noindent With the above definition we run into problems when we parse wneuper@59585: the Program \texttt{InverseZTransform}. This leads to \em ambiguous jan@42368: parse trees. \normalfont We avoid this by moving the definition jan@42369: to \ttfamily Rational.thy \normalfont and re-building {\sisac}. jan@42368: \par \noindent ATTENTION: From now on \ttfamily jan@42368: Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch; jan@42369: it only works due to re-building {\sisac} several times (indicated neuper@42376: explicitly). wneuper@59472: \ jan@42300: wneuper@59472: ML \ jan@42368: (* jan@42368: *("get_denominator", jan@42368: * ("Rational.get_denominator", eval_get_denominator "")) jan@42368: *) jan@42298: fun eval_get_denominator (thmid:string) _ walther@60336: (t as Const (\<^const_name>\get_denominator\, _) $ wenzelm@60309: (Const (\<^const_name>\divide\, _) $num jan@42369: $denom)) thy = walther@59870: SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", wneuper@59395: HOLogic.Trueprop $ (TermC.mk_equality (t, denom))) jan@42300: | eval_get_denominator _ _ _ _ = NONE; wneuper@59472: \ wneuper@59472: text \\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont wneuper@59472: see \ttfamily test/Knowledge/rational.sml\normalfont\ neuper@42289: wneuper@59472: text \\noindent \ttfamily get\_numerator \normalfont should also become a neuper@42376: constant for the Isabelle parser, follow up the \texttt{const} wneuper@59472: declaration above.\ jan@42337: wneuper@59472: ML \ jan@42369: (* jan@42369: *("get_numerator", jan@42369: * ("Rational.get_numerator", eval_get_numerator "")) jan@42369: *) jan@42337: fun eval_get_numerator (thmid:string) _ walther@60336: (t as Const (\<^const_name>\Rational.get_numerator\, _) $ wenzelm@60309: (Const (\<^const_name>\divide\, _) $num jan@42338: $denom )) thy = walther@59870: SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "", wneuper@59395: HOLogic.Trueprop $ (TermC.mk_equality (t, num))) jan@42337: | eval_get_numerator _ _ _ _ = NONE; wneuper@59472: \ jan@42337: wneuper@59472: text \\noindent We discovered several problems by implementing the jan@42369: \ttfamily get\_numerator \normalfont function. Remember when jan@42369: putting new functions to {\sisac}, put them in a thy file and rebuild wneuper@59472: {\sisac}, also put them in the ruleset for the script!\ jan@42369: wneuper@59472: subsection \Solve Equation\label{sec:solveq}\ wneuper@59472: text \\noindent We have to find the zeros of the term, therefor we use our jan@42369: \ttfamily get\_denominator \normalfont function from the step before neuper@42376: and try to solve the second order equation. (Follow up the Calculation jan@42369: in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of jan@42369: equation is too general for the present program. jan@42369: \par We know that this equation can be categorized as \em univariate jan@42369: equation \normalfont and solved with the functions {\sisac} provides jan@42369: for this equation type. Later on {\sisac} should determine the type wneuper@59472: of the given equation self.\ wneuper@59472: ML \ walther@60242: val denominator = TermC.parseNEW ctxt "z \ 2 - 1/4*z - 1/8 = 0"; walther@60242: val fmz = ["equality (z \ 2 - 1/4*z - 1/8 = (0::real))", jan@42369: "solveFor z", jan@42369: "solutions L"]; walther@59997: val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]); wneuper@59472: \ wneuper@59472: text \\noindent Check if the given equation matches the specification of this wneuper@59472: equation type.\ wneuper@59472: ML \ walther@59997: M_Match.match_pbl fmz (Problem.from_store ["univariate", "equation"]); wneuper@59472: \ jan@42345: wneuper@59472: text\\noindent We switch up to the {\sisac} Context and try to solve the wneuper@59472: equation with a more specific type definition.\ neuper@42279: wneuper@59472: ML \ wneuper@59592: Context.theory_name thy = "Isac_Knowledge"; walther@60242: val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \ 2 = 0"; jan@42369: val fmz = (*specification*) walther@60242: ["equality (-1 + -2 * z + 8 * z \ 2 = (0::real))",(*equality*) jan@42369: "solveFor z", (*bound variable*) jan@42369: "solutions L"]; (*identifier for jan@42369: solution*) jan@42369: val (dI',pI',mI') = wneuper@59592: ("Isac_Knowledge", walther@59997: ["abcFormula", "degree_2", "polynomial", "univariate", "equation"], jan@42369: ["no_met"]); wneuper@59472: \ neuper@42279: wneuper@59472: text \\noindent Check if the (other) given equation matches the wneuper@59472: specification of this equation type.\ jan@42369: wneuper@59472: ML \ walther@59984: M_Match.match_pbl fmz (Problem.from_store walther@59997: ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]); wneuper@59472: \ neuper@42279: wneuper@59472: text \\noindent We stepwise solve the equation. This is done by the wneuper@59472: use of a so called calc tree seen downwards.\ jan@42369: wneuper@59472: ML \ Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: (* jan@42369: * nxt =..,Check_elementwise "Assumptions") jan@42369: *) jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; jan@42369: (* jan@42369: * [z = 1 / 2, z = -1 / 4] jan@42369: *) walther@59983: Test_Tool.show_pt pt; jan@42369: val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]"; wneuper@59472: \ neuper@42279: wneuper@59472: subsection \Partial Fraction Decomposition\label{sec:pbz}\ wneuper@59472: text\\noindent We go on with the decomposition of our expression. Follow up the jan@42369: Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on wneuper@59472: Subproblem~1.\ wneuper@59472: subsubsection \Solutions of the Equation\ wneuper@59472: text\\noindent We get the solutions of the before solved equation in a list.\ jan@42369: wneuper@59472: ML \ jan@42369: val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]"; walther@59868: UnparseC.term solutions; Walther@60650: TermC.atom_trace_detail @{context} solutions; wneuper@59472: \ jan@42369: wneuper@59472: subsubsection \Get Solutions out of a List\ wneuper@59472: text \\noindent In {\sisac}'s TP-based programming language: jan@42381: \begin{verbatim} jan@42381: let $ $ s_1 = NTH 1 $ solutions; $ s_2 = NTH 2... $ jan@42381: \end{verbatim} jan@42381: can be useful. wneuper@59472: \ jan@42369: wneuper@59472: ML \ wenzelm@60309: val Const (\<^const_name>\Cons\, _) $ s_1 $ (Const (\<^const_name>\Cons\, _) wenzelm@60309: $ s_2 $ Const (\<^const_name>\Nil\, _)) = solutions; walther@59868: UnparseC.term s_1; walther@59868: UnparseC.term s_2; wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont jan@42369: requires to get the denominators of the partial fractions out of the jan@42369: Solutions as: jan@42369: \begin{itemize} jan@42381: \item $Denominator_{1}=z-Zeropoint_{1}$ jan@42381: \item $Denominator_{2}=z-Zeropoint_{2}$ jan@42381: \item \ldots jan@42381: \end{itemize} wneuper@59472: \ jan@42369: wneuper@59472: ML \ jan@42369: val xx = HOLogic.dest_eq s_1; wenzelm@60309: val s_1' = HOLogic.mk_binop \<^const_name>\minus\ xx; jan@42369: val xx = HOLogic.dest_eq s_2; wenzelm@60309: val s_2' = HOLogic.mk_binop \<^const_name>\minus\ xx; walther@59868: UnparseC.term s_1'; walther@59868: UnparseC.term s_2'; wneuper@59472: \ jan@42369: wneuper@59472: text \\noindent For the programming language a function collecting all the wneuper@59472: above manipulations is helpful.\ jan@42369: wneuper@59472: ML \ jan@42369: fun fac_from_sol s = jan@42369: let val (lhs, rhs) = HOLogic.dest_eq s wenzelm@60309: in HOLogic.mk_binop \<^const_name>\minus\ (lhs, rhs) end; wneuper@59472: \ jan@42369: wneuper@59472: ML \ jan@42369: fun mk_prod prod [] = walther@59861: if prod = TermC.empty jan@42369: then error "mk_prod called with []" jan@42369: else prod jan@42369: | mk_prod prod (t :: []) = walther@59861: if prod = TermC.empty jan@42369: then t wenzelm@60309: else HOLogic.mk_binop \<^const_name>\times\ (prod, t) jan@42369: | mk_prod prod (t1 :: t2 :: ts) = walther@59861: if prod = TermC.empty jan@42369: then jan@42369: let val p = wenzelm@60309: HOLogic.mk_binop \<^const_name>\times\ (t1, t2) jan@42369: in mk_prod p ts end jan@42369: else jan@42369: let val p = wenzelm@60309: HOLogic.mk_binop \<^const_name>\times\ (prod, t1) jan@42369: in mk_prod p (t2 :: ts) end wneuper@59472: \ jan@42369: (* ML {* neuper@42376: probably keep these test in test/Tools/isac/... walther@59861: (*mk_prod TermC.empty [];*) neuper@42335: Walther@60565: val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"]; walther@59868: UnparseC.term prod = "x + 123"; neuper@42335: Walther@60565: val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]"; neuper@42335: val sols = HOLogic.dest_list sol; neuper@42335: val facs = map fac_from_sol sols; walther@59861: val prod = mk_prod TermC.empty facs; walther@59868: UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"; neuper@42335: jan@42369: val prod = Walther@60565: mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"]; walther@59868: UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)"; jan@42369: *} *) wneuper@59472: ML \ jan@42369: fun factors_from_solution sol = jan@42369: let val ts = HOLogic.dest_list sol walther@59861: in mk_prod TermC.empty (map fac_from_sol ts) end; wneuper@59472: \ jan@42369: (* ML {* Walther@60565: val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]"; neuper@42335: val fs = factors_from_solution sol; walther@59868: UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))" jan@42369: *} *) wneuper@59472: text \\noindent This function needs to be packed such that it can be evaluated jan@42369: by the Lucas-Interpreter. Therefor we moved the function to the jan@42369: corresponding \ttfamily Equation.thy \normalfont in our case neuper@42376: \ttfamily PartialFractions.thy \normalfont. The necessary steps jan@42381: are quit the same as we have done with \ttfamily get\_denominator wneuper@59472: \normalfont before.\ wneuper@59472: ML \ jan@42369: (*("factors_from_solution", jan@42369: ("Partial_Fractions.factors_from_solution", jan@42369: eval_factors_from_solution ""))*) jan@42369: jan@42369: fun eval_factors_from_solution (thmid:string) _ walther@60270: (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy = walther@60270: let val prod = factors_from_solution sol walther@60270: in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "", walther@60270: HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) walther@60270: end walther@60270: | eval_factors_from_solution _ _ _ _ = NONE; wneuper@59472: \ jan@42352: wneuper@59472: text \\noindent The tracing output of the calc tree after applying this jan@42381: function was: jan@42381: \begin{verbatim} jan@42381: 24 / factors_from_solution [z = 1/ 2, z = -1 / 4])] jan@42381: \end{verbatim} jan@42381: and the next step: jan@42381: \begin{verbatim} jan@42381: val nxt = ("Empty_Tac", ...): tac'_) jan@42381: \end{verbatim} jan@42381: These observations indicate, that the Lucas-Interpreter (LIP) jan@42381: does not know how to evaluate \ttfamily factors\_from\_solution jan@42381: \normalfont, so we knew that there is something wrong or missing. wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent First we isolate the difficulty in the program as follows: jan@42381: \begin{verbatim} wneuper@59476: " (L_L::bool list) = (SubProblem (PolyEqX, " ^ jan@42381: " [abcFormula, degree_2, polynomial, " ^ jan@42381: " univariate,equation], " ^ jan@42381: " [no_met]) " ^ jan@42381: " [BOOL equ, REAL zzz]); " ^ jan@42381: " (facs::real) = factors_from_solution L_L; " ^ jan@42381: " (foo::real) = Take facs " ^ jan@42381: \end{verbatim} jan@42381: jan@42381: \par \noindent And see the tracing output: jan@42381: jan@42381: \begin{verbatim} jan@42381: [(([], Frm), Problem (Isac, [inverse, jan@42381: Z_Transform, jan@42381: SignalProcessing])), jan@42381: (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))), jan@42381: (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), walther@60242: (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \ 2)), walther@60242: (([3], Pbl), solve (-1 + -2 * z + 8 * z \ 2 = 0, z)), walther@60242: (([3,1], Frm), -1 + -2 * z + 8 * z \ 2 = 0), walther@60242: (([3,1], Res), z = (- -2 + sqrt (-2 \ 2 - 4 * 8 * -1)) / (2 * 8)| walther@60242: z = (- -2 - sqrt (-2 \ 2 - 4 * 8 * -1)) / (2 * 8)), jan@42381: (([3,2], Res), z = 1 / 2 | z = -1 / 4), jan@42381: (([3,3], Res), [ z = 1 / 2, z = -1 / 4]), jan@42381: (([3,4], Res), [ z = 1 / 2, z = -1 / 4]), jan@42381: (([3], Res), [ z = 1 / 2, z = -1 / 4]), jan@42381: (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])] jan@42381: \end{verbatim} jan@42381: jan@42381: \par \noindent In particular that: jan@42381: jan@42381: \begin{verbatim} walther@60242: (([3], Pbl), solve (-1 + -2 * z + 8 * z \ 2 = 0, z)), jan@42381: \end{verbatim} jan@42381: \par \noindent Shows the equation which has been created in jan@42381: the program by: jan@42381: \begin{verbatim} jan@42381: "(denom::real) = get_denominator funterm; " ^ jan@42381: (* get_denominator *) jan@42381: "(equ::bool) = (denom = (0::real)); " ^ jan@42381: \end{verbatim} jan@42369: jan@42381: \noindent \ttfamily get\_denominator \normalfont has been evaluated successfully, jan@42369: but not\\ \ttfamily factors\_from\_solution.\normalfont jan@42369: So we stepwise compare with an analogous case, \ttfamily get\_denominator jan@42369: \normalfont successfully done above: We know that LIP evaluates Walther@60586: expressions in the program by use of the \emph{prog_rls}, so we try to get Walther@60586: the original \emph{prog_rls}.\\ jan@42352: jan@42381: \begin{verbatim} Walther@60586: val {prog_rls,...} = MethodC.from_store ctxt ["SignalProcessing", jan@42381: "Z_Transform", neuper@42405: "Inverse"]; jan@42381: \end{verbatim} jan@42369: jan@42381: \par \noindent Create 2 good example terms: jan@42352: jan@42381: \begin{verbatim} jan@42381: val SOME t1 = jan@42381: parseNEW ctxt "get_denominator ((111::real) / 222)"; jan@42381: val SOME t2 = jan@42381: parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]"; jan@42381: \end{verbatim} jan@42381: Walther@60586: \par \noindent Rewrite the terms using prog_rls:\\ Walther@60586: \ttfamily \par \noindent rewrite\_set\_ thy true prog_rls t1;\\ Walther@60586: rewrite\_set\_ thy true prog_rls t2;\\ jan@42369: \par \noindent \normalfont Now we see a difference: \texttt{t1} gives jan@42369: \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the Walther@60586: \emph{prog_rls}: jan@42381: \begin{verbatim} Walther@60586: val prog_rls = walther@59851: Rule_Set.Repeat{id = "srls_InverseZTransform", walther@59878: rules = [Eval("Rational.get_numerator", jan@42381: eval_get_numerator "Rational.get_numerator"), walther@59878: Eval("Partial_Fractions.factors_from_solution", jan@42381: eval_factors_from_solution jan@42381: "Partial_Fractions.factors_from_solution")]} jan@42381: \end{verbatim} jan@42381: \par \noindent Here everthing is perfect. So the error can jan@42369: only be in the SML code of \ttfamily eval\_factors\_from\_solution. jan@42369: \normalfont We try to check the code with an existing test; since the jan@42369: \emph{code} is in jan@42369: \begin{center}\ttfamily src/Tools/isac/Knowledge/Partial\_Fractions.thy jan@42369: \normalfont\end{center} jan@42369: the \emph{test} should be in jan@42369: \begin{center}\ttfamily test/Tools/isac/Knowledge/partial\_fractions.sml jan@42369: \normalfont\end{center} jan@42369: \par \noindent After updating the function \ttfamily jan@42369: factors\_from\_solution \normalfont to a new version and putting a neuper@42376: test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again jan@42369: to evaluate the term with the same result. jan@42369: \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that jan@42369: everything is working fine. Also we checked that the test \ttfamily jan@42369: partial\_fractions.sml \normalfont is used in \ttfamily Test\_Isac.thy jan@42369: \normalfont jan@42369: \begin{center}use \ttfamily "Knowledge/partial\_fractions.sml" jan@42369: \normalfont \end{center} jan@42369: and \ttfamily Partial\_Fractions.thy \normalfont is part is part of jan@42381: {\sisac} by evaluating jan@42352: jan@42381: \begin{verbatim} neuper@42389: val thy = @{theory "Inverse_Z_Transform"}; jan@42381: \end{verbatim} jan@42352: jan@42381: After rebuilding {\sisac} again it worked. wneuper@59472: \ neuper@42279: wneuper@59472: subsubsection \Build Expression\ wneuper@59472: text \\noindent In {\sisac}'s TP-based programming language we can build jan@42369: expressions by:\\ wneuper@59472: \ttfamily let s\_1 = Take numerator / (s\_1 * s\_2) \normalfont\ jan@42369: wneuper@59472: ML \ jan@42369: (* neuper@42376: * The main denominator is the multiplication of the denominators of jan@42369: * all partial fractions. jan@42369: *) jan@42369: jan@42369: val denominator' = HOLogic.mk_binop wenzelm@60309: \<^const_name>\times\ (s_1', s_2') ; jan@42369: val SOME numerator = parseNEW ctxt "3::real"; neuper@42279: jan@42369: val expr' = HOLogic.mk_binop wenzelm@60309: \<^const_name>\divide\ (numerator, denominator'); walther@59868: UnparseC.term expr'; wneuper@59472: \ neuper@42279: wneuper@59472: subsubsection \Apply the Partial Fraction Decomposion Ansatz\ jan@42369: wneuper@59472: text\\noindent We use the Ansatz of the Partial Fraction Decomposition for our jan@42369: expression 2nd order. Follow up the calculation in wneuper@59472: Section~\ref{sec:calc:ztrans} Step~03.\ jan@42369: wneuper@59592: ML \Context.theory_name thy = "Isac_Knowledge"\ neuper@42279: wneuper@59472: text\\noindent We define two axiomatization, the first one is the main ansatz, neuper@42376: the next one is just an equivalent transformation of the resulting jan@42369: equation. Both axiomatizations were moved to \ttfamily jan@42369: Partial\_Fractions.thy \normalfont and got their own rulesets. In later neuper@42376: programs it is possible to use the rulesets and the machine will find wneuper@59472: the correct ansatz and equivalent transformation itself.\ jan@42369: neuper@42279: axiomatization where jan@42369: ansatz_2nd_order: "n / (a*b) = A/a + B/b" and jan@42369: equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)" jan@42369: wneuper@59472: text\\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite neuper@42376: our expression and get an equation with our expression on the left wneuper@59472: and the partial fractions of it on the right hand side.\ jan@42369: wneuper@59472: ML \ jan@42369: val SOME (t1,_) = walther@59852: rewrite_ @{theory} e_rew_ord Rule_Set.empty false jan@42369: @{thm ansatz_2nd_order} expr'; Walther@60650: UnparseC.term t1; TermC.atom_trace_detail @{context} t1; jan@42369: val eq1 = HOLogic.mk_eq (expr', t1); walther@59868: UnparseC.term eq1; wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent Eliminate the denominators by multiplying the left and the jan@42369: right hand side of the equation with the main denominator. This is an jan@42369: simple equivalent transformation. Later on we use an own ruleset jan@42369: defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this. wneuper@59472: Follow up the calculation in Section~\ref{sec:calc:ztrans} Step~04.\ neuper@42279: wneuper@59472: ML \ jan@42369: val SOME (eq2,_) = walther@59852: rewrite_ @{theory} e_rew_ord Rule_Set.empty false jan@42369: @{thm equival_trans_2nd_order} eq1; walther@59868: UnparseC.term eq2; wneuper@59472: \ neuper@42342: wneuper@59472: text\\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont wneuper@59472: for simplifications on expressions.\ neuper@42279: wneuper@59472: ML \ neuper@42384: val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2; walther@59868: UnparseC.term eq3; jan@42369: (* jan@42369: * ?A ?B not simplified jan@42369: *) wneuper@59472: \ neuper@42279: wneuper@59472: text\\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about jan@42369: simplifications. The problem that we would like to have only a specific degree wneuper@59472: of simplification occurs right here, in the next step.\ jan@42369: wneuper@59472: ML \ walther@60330: Rewrite.trace_on := false; (*true false*) jan@42369: val SOME fract1 = jan@42369: parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))"; jan@42369: (* jan@42369: * A B ! jan@42369: *) jan@42369: val SOME (fract2,_) = neuper@42384: rewrite_set_ @{theory} false norm_Rational fract1; walther@59868: UnparseC.term fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4"; jan@42369: (* walther@59868: * UnparseC.term fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" jan@42369: * would be more traditional... jan@42369: *) wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent We walk around this problem by generating our new equation first.\ jan@42369: wneuper@59472: ML \ jan@42369: val (numerator, denominator) = HOLogic.dest_eq eq3; jan@42369: val eq3' = HOLogic.mk_eq (numerator, fract1); jan@42369: (* jan@42369: * A B ! jan@42369: *) walther@59868: UnparseC.term eq3'; jan@42369: (* jan@42369: * MANDATORY: simplify (and remove denominator) otherwise 3 = 0 jan@42369: *) jan@42369: val SOME (eq3'' ,_) = neuper@42384: rewrite_set_ @{theory} false norm_Rational eq3'; walther@59868: UnparseC.term eq3''; wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent Still working at {\sisac}\ldots\ jan@42369: wneuper@59592: ML \Context.theory_name thy = "Isac_Knowledge"\ jan@42369: wneuper@59472: subsubsection \Build a Rule-Set for the Ansatz\ wneuper@59472: text \\noindent The \emph{ansatz} rules violate the principle that each jan@42369: variable on the right-hand-side must also occur on the jan@42369: left-hand-side of the rule: A, B, etc. don't do that. Thus the jan@42369: rewriter marks these variables with question marks: ?A, ?B, etc. jan@42369: These question marks can be dropped by \ttfamily fun wneuper@59472: drop\_questionmarks\normalfont.\ jan@42369: wneuper@59472: ML \ s1210629013@55444: val ansatz_rls = prep_rls @{theory} ( walther@59851: Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), Walther@60586: asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [], jan@42369: rules = [ walther@59871: Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}), walther@59871: Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order}) jan@42369: ], Walther@60586: program = Empty_Prog}); wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent We apply the ruleset\ldots\ jan@42369: wneuper@59472: ML \ jan@42369: val SOME (ttttt,_) = neuper@42384: rewrite_set_ @{theory} false ansatz_rls expr'; wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent And check the output\ldots\ jan@42369: wneuper@59472: ML \ walther@59868: UnparseC.term expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))"; walther@59868: UnparseC.term ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)"; wneuper@59472: \ jan@42369: wneuper@59472: subsubsection \Get the First Coefficient\ jan@42369: wneuper@59472: text\\noindent Now it's up to get the two coefficients A and B, which will be neuper@42376: the numerators of our partial fractions. Continue following up the wneuper@59472: Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.\ jan@42369: wneuper@59472: text\\noindent To get the first coefficient we substitute $z$ with the first wneuper@59472: zero-point we determined in Section~\ref{sec:solveq}.\ jan@42369: wneuper@59472: ML \ jan@42369: val SOME (eq4_1,_) = walther@59852: rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3''; walther@59868: UnparseC.term eq4_1; jan@42369: val SOME (eq4_2,_) = neuper@42384: rewrite_set_ @{theory} false norm_Rational eq4_1; walther@59868: UnparseC.term eq4_2; jan@42369: walther@59997: val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"]; walther@59997: val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]); jan@42369: (* neuper@42377: * Solve the simple linear equation for A: jan@42369: * Return eq, not list of eq's jan@42369: *) Walther@60571: val (p,_,fa,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Given "equality (3=3*A/4)"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Given "solveFor A"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Find "solutions L"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; wneuper@59592: (*Specify_Theory "Isac_Knowledge"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Specify_Problem ["normalise", "polynomial", walther@59997: "univariate", "equation"])*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (* Specify_Method["PolyEq", "normalise_poly"]*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Apply_Method["PolyEq", "normalise_poly"]*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Rewrite ("all_left", "PolyEq.all_left")*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; wneuper@59497: (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Rewrite_Set "polyeq_simplify"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Given "equality (3 + -3 / 4 * A =0)"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Given "solveFor A"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Add_Find "solutions A_i"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; wneuper@59497: (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Rewrite_Set "polyeq_simplify"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Rewrite_Set "norm_Rational_parenthesized"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Or_to_List*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*Check_elementwise "Assumptions"*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Check_Postcond ["degree_1", "polynomial", walther@59997: "univariate", "equation"]*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Check_Postcond ["normalise", "polynomial", walther@59997: "univariate", "equation"]*) jan@42369: val (p,_,fa,nxt,_,pt) = me nxt p [] pt; jan@42369: (*End_Proof'*) jan@42369: f2str fa; wneuper@59472: \ jan@42369: wneuper@59472: subsubsection \Get Second Coefficient\ jan@42369: wneuper@59472: text\\noindent With the use of \texttt{thy} we check which theories the wneuper@59472: interpreter knows.\ jan@42369: wneuper@59472: ML \thy\ neuper@42279: wneuper@59472: text\\noindent To get the second coefficient we substitute $z$ with the second wneuper@59472: zero-point we determined in Section~\ref{sec:solveq}.\ jan@42369: wneuper@59472: ML \ jan@42369: val SOME (eq4b_1,_) = walther@59852: rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3''; walther@59868: UnparseC.term eq4b_1; jan@42369: val SOME (eq4b_2,_) = neuper@42384: rewrite_set_ @{theory} false norm_Rational eq4b_1; walther@59868: UnparseC.term eq4b_2; neuper@42279: walther@59997: val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"]; walther@59997: val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]); Walther@60571: val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: val (p,_,fb,nxt,_,pt) = me nxt p [] pt; jan@42369: f2str fb; wneuper@59472: \ neuper@42279: Walther@60586: text\\noindent We compare our results with the where_ calculated upshot.\ jan@42369: wneuper@59472: ML \ jan@42369: if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1"; jan@42369: if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1"; wneuper@59472: \ neuper@42279: walther@60154: section \Implement the Specification and the MethodC \label{spec-meth}\ neuper@42279: wneuper@59472: text\\noindent Now everything we need for solving the problem has been jan@42369: tested out. We now start by creating new nodes for our methods and wneuper@59472: further on our new program in the interpreter.\ jan@42369: wneuper@59472: subsection\Define the Field Descriptions for the wneuper@59472: Specification\label{sec:deffdes}\ jan@42369: wneuper@59472: text\\noindent We define the fields \em filterExpression \normalfont and neuper@42376: \em stepResponse \normalfont both as equations, they represent the in- and wneuper@59472: output of the program.\ jan@42369: neuper@42279: consts neuper@42279: filterExpression :: "bool => una" neuper@42279: stepResponse :: "bool => una" neuper@42279: wneuper@59472: subsection\Define the Specification\ jan@42369: wneuper@59472: text\\noindent The next step is defining the specifications as nodes in the neuper@42376: designated part. We have to create the hierarchy node by node and start jan@42369: with \em SignalProcessing \normalfont and go on by creating the node wneuper@59472: \em Z\_Transform\normalfont.\ jan@42369: Walther@60588: setup \Know_Store.add_pbls wenzelm@60290: [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []), wenzelm@60290: Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty walther@59997: (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\ jan@42369: wneuper@59472: text\\noindent For the suddenly created node we have to define the input neuper@42376: and output parameters. We already prepared their definition in wneuper@59472: Section~\ref{sec:deffdes}.\ jan@42369: Walther@60588: setup \Know_Store.add_pbls wenzelm@60290: [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty s1210629013@55355: (["Inverse", "Z_Transform", "SignalProcessing"], wneuper@59550: [("#Given" ,["filterExpression X_eq"]), s1210629013@55355: ("#Find", ["stepResponse n_eq"])], walther@59852: Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], s1210629013@55355: NONE, walther@59997: [["SignalProcessing", "Z_Transform", "Inverse"]])]\ wneuper@59472: ML \ walther@59971: Test_Tool.show_ptyps() (); walther@59997: Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"]; wneuper@59472: \ neuper@42279: walther@60154: subsection \Define Name and Signature for the MethodC\ jan@42369: wneuper@59472: text\\noindent As a next step we store the definition of our new method as a wneuper@59472: constant for the interpreter.\ jan@42369: neuper@42279: consts neuper@42279: InverseZTransform :: "[bool, bool] => bool" wneuper@59585: ("((Program InverseZTransform (_ =))// (_))" 9) neuper@42279: walther@60154: subsection \Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\ jan@42369: wneuper@59472: text\\noindent Again we have to generate the nodes step by step, first the jan@42369: parent node and then the originally \em Z\_Transformation jan@42369: \normalfont node. We have to define both nodes first with an empty script wneuper@59472: as content.\ jan@42369: Walther@60588: setup \Know_Store.add_mets wenzelm@60290: [MethodC.prep_input @{theory} "met_SP" [] e_metID s1210629013@55377: (["SignalProcessing"], [], Walther@60586: {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty, Walther@60586: errpats = [], rew_rls = Rule_Set.empty}, s1210629013@55377: "empty_script"), wenzelm@60290: MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID s1210629013@55377: (["SignalProcessing", "Z_Transform"], [], Walther@60586: {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty, Walther@60586: errpats = [], rew_rls = Rule_Set.empty}, s1210629013@55377: "empty_script")] wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent After we generated both nodes, we can fill the containing jan@42369: script we want to implement later. First we define the specifications wneuper@59472: of the script in e.g. the in- and output.\ jan@42369: Walther@60588: setup \Know_Store.add_mets walther@60154: [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID s1210629013@55377: (["SignalProcessing", "Z_Transform", "Inverse"], wneuper@59550: [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]), wneuper@59550: ("#Find", ["stepResponse n_eq"])], Walther@60586: {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty, Walther@60586: errpats = [], rew_rls = Rule_Set.empty}, s1210629013@55377: "empty_script")] wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent After we stored the definition we can start implementing the jan@42369: script itself. As a first try we define only three rows containing one wneuper@59472: simple operation.\ jan@42369: Walther@60588: setup \Know_Store.add_mets walther@60154: [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID s1210629013@55377: (["SignalProcessing", "Z_Transform", "Inverse"], wneuper@59550: [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]), wneuper@59550: ("#Find", ["stepResponse n_eq"])], Walther@60586: {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty, Walther@60586: errpats = [], rew_rls = Rule_Set.empty}, wneuper@59585: "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*) s1210629013@55377: " (let X = Take Xeq;" ^ walther@59635: " X = Rewrite ruleZY X" ^ s1210629013@55377: " in X)")] wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent Check if the method has been stored correctly\ldots\ jan@42369: wneuper@59472: ML \ jan@42369: show_mets(); wneuper@59472: \ jan@42369: wneuper@59472: text\\noindent If yes we can get the method by stepping backwards through wneuper@59472: the hierarchy.\ jan@42369: wneuper@59472: ML \ Walther@60559: MethodC.from_store ctxt ["SignalProcessing", "Z_Transform", "Inverse"]; wneuper@59472: \ neuper@42279: wneuper@59472: section \Program in TP-based language \label{prog-steps}\ jan@42369: wneuper@59472: text\\noindent We start stepwise expanding our program. The script is a neuper@42376: simple string containing several manipulation instructions. jan@42370: \par The first script we try contains no instruction, we only test if wneuper@59472: building scripts that way work.\ jan@42369: wneuper@59472: subsection \Stepwise Extend the Program\ wneuper@59472: ML \ jan@42370: val str = wneuper@59585: "Program InverseZTransform (Xeq::bool) = "^ jan@42370: " Xeq"; wneuper@59472: \ jan@42300: wneuper@59472: text\\noindent Next we put some instructions in the script and try if we are wneuper@59472: able to solve our first equation.\ jan@42370: wneuper@59472: ML \ jan@42370: val str = wneuper@59585: "Program InverseZTransform (Xeq::bool) = "^ jan@42370: (* walther@60242: * 1/z) instead of z \ -1 jan@42370: *) jan@42381: " (let X = Take Xeq; "^ jan@42381: " X' = Rewrite ruleZY False X; "^ jan@42370: (* jan@42370: * z * denominator jan@42370: *) jan@42381: " X' = (Rewrite_Set norm_Rational False) X' "^ jan@42370: (* jan@42370: * simplify jan@42370: *) jan@42370: " in X)"; jan@42370: (* jan@42370: * NONE jan@42370: *) wneuper@59585: "Program InverseZTransform (Xeq::bool) = "^ jan@42370: (* walther@60242: * (1/z) instead of z \ -1 jan@42370: *) jan@42381: " (let X = Take Xeq; "^ jan@42381: " X' = Rewrite ruleZY False X; "^ jan@42370: (* jan@42370: * z * denominator jan@42370: *) jan@42381: " X' = (Rewrite_Set norm_Rational False) X'; "^ jan@42370: (* jan@42370: * simplify jan@42370: *) wneuper@59476: " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^ jan@42381: " polynomial,univariate,equation], "^ jan@42381: " [no_met]) "^ jan@42381: " [BOOL e_e, REAL v_v]) "^ jan@42370: " in X)"; wneuper@59472: \ jan@42370: wneuper@59472: text\\noindent To solve the equation it is necessary to drop the left hand jan@42370: side, now we only need the denominator of the right hand side. The first wneuper@59472: equation solves the zeros of our expression.\ jan@42370: wneuper@59472: ML \ jan@42370: val str = wneuper@59585: "Program InverseZTransform (Xeq::bool) = "^ jan@42381: " (let X = Take Xeq; "^ jan@42381: " X' = Rewrite ruleZY False X; "^ jan@42381: " X' = (Rewrite_Set norm_Rational False) X'; "^ jan@42381: " funterm = rhs X' "^ jan@42370: (* jan@42370: * drop X'= for equation solving jan@42370: *) jan@42370: " in X)"; wneuper@59472: \ jan@42370: wneuper@59472: text\\noindent As mentioned above, we need the denominator of the right hand jan@42370: side. The equation itself consists of this denominator and tries to find wneuper@59472: a $z$ for this the denominator is equal to zero.\ jan@42370: wneuper@59585: text \ dropped during switch from Program to partial_function: jan@42370: val str = wneuper@59585: "Program InverseZTransform (X_eq::bool) = "^ jan@42381: " (let X = Take X_eq; "^ jan@42381: " X' = Rewrite ruleZY False X; "^ jan@42381: " X' = (Rewrite_Set norm_Rational False) X'; "^ jan@42381: " (X'_z::real) = lhs X'; "^ jan@42381: " (z::real) = argument_in X'_z; "^ jan@42381: " (funterm::real) = rhs X'; "^ jan@42381: " (denom::real) = get_denominator funterm; "^ jan@42370: (* jan@42370: * get_denominator jan@42370: *) jan@42381: " (equ::bool) = (denom = (0::real)); "^ jan@42381: " (L_L::bool list) = "^ wneuper@59546: " (SubProblem (Test, "^ neuper@55279: " [LINEAR,univariate,equation,test], "^ jan@42381: " [Test,solve_linear]) "^ jan@42381: " [BOOL equ, REAL z]) "^ jan@42370: " in X)"; jan@42370: jan@42370: parse thy str; wneuper@59395: val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; Walther@60650: TermC.atom_trace_detail @{context} sc; wneuper@59472: \ jan@42370: wneuper@59472: text \\noindent This ruleset contains all functions that are in the script; wneuper@59472: The evaluation of the functions is done by rewriting using this ruleset.\ jan@42370: wneuper@59472: ML \ Walther@60586: val prog_rls = walther@59851: Rule_Set.Repeat {id="srls_InverseZTransform", jan@42381: preconds = [], jan@42381: rew_ord = ("termlessI",termlessI), Walther@60586: asm_rls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty jan@42381: [(*for asm in NTH_CONS ...*) wenzelm@60309: Eval (\<^const_name>\less\,eval_equ "#less_"), jan@42381: (*2nd NTH_CONS pushes n+-1 into asms*) Walther@60516: Eval(\<^const_name>\plus\, Calc_Binop.numeric "#add_") jan@42381: ], Walther@60586: prog_rls = Rule_Set.Empty, calc = [], errpatts = [], jan@42381: rules = [ walther@59871: Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), Walther@60516: Eval(\<^const_name>\plus\, Calc_Binop.numeric "#add_"), walther@59871: Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}), walther@59878: Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"), walther@59878: Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"), walther@59878: Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in"), walther@59878: Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"), walther@59878: Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"), walther@59878: Eval("Partial_Fractions.factors_from_solution", walther@59603: eval_factors_from_solution "#factors_from_solution"), walther@59878: Eval("Partial_Fractions.drop_questionmarks", jan@42381: eval_drop_questionmarks "#drop_?") jan@42381: ], Walther@60586: program = Empty_Prog}; wneuper@59472: \ jan@42370: jan@42370: wneuper@59472: subsection \Store Final Version of Program for Execution\ jan@42370: wneuper@59472: text\\noindent After we also tested how to write scripts and run them, jan@42370: we start creating the final version of our script and store it into jan@42381: the method for which we created a node in Section~\ref{sec:cparentnode} jan@42370: Note that we also did this stepwise, but we didn't kept every wneuper@59472: subversion.\ jan@42370: Walther@60588: setup \Know_Store.add_mets walther@60154: [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID s1210629013@55377: (["SignalProcessing", "Z_Transform", "Inverse"], wneuper@59550: [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*) wneuper@59550: ("#Find", ["stepResponse n_eq"])], Walther@60586: {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = prog_rls, where_rls = Rule_Set.empty, crls = Rule_Set.empty, Walther@60586: errpats = [], rew_rls = Rule_Set.empty}, wneuper@59585: "Program InverseZTransform (X_eq::bool) = "^ walther@60242: (*(1/z) instead of z \ -1*) s1210629013@55377: "(let X = Take X_eq; "^ s1210629013@55377: " X' = Rewrite ruleZY False X; "^ s1210629013@55377: (*z * denominator*) s1210629013@55377: " (num_orig::real) = get_numerator (rhs X'); "^ s1210629013@55377: " X' = (Rewrite_Set norm_Rational False) X'; "^ s1210629013@55377: (*simplify*) s1210629013@55377: " (X'_z::real) = lhs X'; "^ s1210629013@55377: " (zzz::real) = argument_in X'_z; "^ s1210629013@55377: " (funterm::real) = rhs X'; "^ s1210629013@55377: (*drop X' z = for equation solving*) s1210629013@55377: " (denom::real) = get_denominator funterm; "^ s1210629013@55377: (*get_denominator*) s1210629013@55377: " (num::real) = get_numerator funterm; "^ s1210629013@55377: (*get_numerator*) s1210629013@55377: " (equ::bool) = (denom = (0::real)); "^ wneuper@59476: " (L_L::bool list) = (SubProblem (PolyEqX, "^ s1210629013@55377: " [abcFormula,degree_2,polynomial,univariate,equation], "^ s1210629013@55377: " [no_met]) "^ s1210629013@55377: " [BOOL equ, REAL zzz]); "^ s1210629013@55377: " (facs::real) = factors_from_solution L_L; "^ s1210629013@55377: " (eql::real) = Take (num_orig / facs); "^ s1210629013@55377: s1210629013@55377: " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^ s1210629013@55377: s1210629013@55377: " (eq::bool) = Take (eql = eqr); "^ s1210629013@55377: (*Maybe possible to use HOLogic.mk_eq ??*) s1210629013@55377: " eq = (Try (Rewrite_Set equival_trans False)) eq; "^ s1210629013@55377: s1210629013@55377: " eq = drop_questionmarks eq; "^ s1210629013@55377: " (z1::real) = (rhs (NTH 1 L_L)); "^ s1210629013@55377: (* s1210629013@55377: * prepare equation for a - eq_a s1210629013@55377: * therefor substitute z with solution 1 - z1 s1210629013@55377: *) s1210629013@55377: " (z2::real) = (rhs (NTH 2 L_L)); "^ s1210629013@55377: s1210629013@55377: " (eq_a::bool) = Take eq; "^ s1210629013@55377: " eq_a = (Substitute [zzz=z1]) eq; "^ s1210629013@55377: " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^ s1210629013@55377: " (sol_a::bool list) = "^ wneuper@59476: " (SubProblem (IsacX, "^ s1210629013@55377: " [univariate,equation],[no_met]) "^ s1210629013@55377: " [BOOL eq_a, REAL (A::real)]); "^ s1210629013@55377: " (a::real) = (rhs(NTH 1 sol_a)); "^ s1210629013@55377: s1210629013@55377: " (eq_b::bool) = Take eq; "^ s1210629013@55377: " eq_b = (Substitute [zzz=z2]) eq_b; "^ s1210629013@55377: " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^ s1210629013@55377: " (sol_b::bool list) = "^ wneuper@59476: " (SubProblem (IsacX, "^ s1210629013@55377: " [univariate,equation],[no_met]) "^ s1210629013@55377: " [BOOL eq_b, REAL (B::real)]); "^ s1210629013@55377: " (b::real) = (rhs(NTH 1 sol_b)); "^ s1210629013@55377: s1210629013@55377: " eqr = drop_questionmarks eqr; "^ s1210629013@55377: " (pbz::real) = Take eqr; "^ s1210629013@55377: " pbz = ((Substitute [A=a, B=b]) pbz); "^ s1210629013@55377: s1210629013@55377: " pbz = Rewrite ruleYZ False pbz; "^ s1210629013@55377: " pbz = drop_questionmarks pbz; "^ s1210629013@55377: s1210629013@55377: " (X_z::bool) = Take (X_z = pbz); "^ s1210629013@55377: " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^ s1210629013@55377: " n_eq = drop_questionmarks n_eq "^ s1210629013@55377: "in n_eq)")] wneuper@59472: \ jan@42370: jan@42370: wneuper@59472: subsection \Check the Program\ wneuper@59472: text\\noindent When the script is ready we can start checking our work.\ wneuper@59472: subsubsection \Check the Formalization\ wneuper@59472: text\\noindent First we want to check the formalization of the in and wneuper@59472: output of our program.\ jan@42370: wneuper@59472: ML \ jan@42370: val fmz = jan@42370: ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", jan@42370: "stepResponse (x[n::real]::bool)"]; jan@42370: val (dI,pI,mI) = wneuper@59592: ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], walther@59997: ["SignalProcessing", "Z_Transform", "Inverse"]); jan@42370: jan@42370: val ([ jan@42370: ( jan@42370: 1, jan@42370: [1], jan@42370: "#Given", jan@42370: Const ("Inverse_Z_Transform.filterExpression", _), wenzelm@60309: [Const (\<^const_name>\HOL.eq\, _) $ _ $ _] jan@42370: ), jan@42370: ( jan@42370: 2, jan@42370: [1], jan@42370: "#Find", jan@42370: Const ("Inverse_Z_Transform.stepResponse", _), jan@42370: [Free ("x", _) $ _] jan@42370: ) jan@42370: ],_ Walther@60586: ) = O_Model.init thy fmz ((#model o Problem.from_store) pI); jan@42370: neuper@48790: val Prog sc Walther@60586: = (#program o MethodC.from_store ctxt) ["SignalProcessing", jan@42370: "Z_Transform", neuper@42405: "Inverse"]; Walther@60650: TermC.atom_trace_detail @{context} sc; wneuper@59472: \ jan@42370: wneuper@59472: subsubsection \Stepwise Check the Program\label{sec:stepcheck}\ wneuper@59472: text\\noindent We start to stepwise execute our new program in a calculation wneuper@59472: tree and check if every node implements that what we have wanted.\ jan@42370: wneuper@59472: ML \ walther@60330: Rewrite.trace_on := false; (*true false*) walther@59901: LItool.trace_on := false; (*true*) jan@42370: print_depth 9; jan@42370: jan@42370: val fmz = jan@42418: ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", jan@42370: "stepResponse (x[n::real]::bool)"]; jan@42370: jan@42370: val (dI,pI,mI) = wneuper@59592: ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], walther@59997: ["SignalProcessing", "Z_Transform", "Inverse"]); jan@42370: Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))]; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Add_Given"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Add_Find"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Specify_Theory"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Specify_Problem"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Specify_Method"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Apply_Method"; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Rewrite (ruleZY, Inverse_Z_Transform.ruleZY)"; jan@42370: "--> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; jan@42370: (* jan@42370: * TODO naming! jan@42370: *) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "Rewrite_Set norm_Rational"; jan@42370: " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; jan@42371: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: "SubProblem"; neuper@52101: print_depth 3; wneuper@59472: \ jan@42370: wneuper@59472: text \\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had jan@42370: \ttfamily Empty\_Tac; \normalfont the search for the reason considered jan@42370: the following points:\begin{itemize} jan@42381: \item What shows \ttfamily show\_pt pt;\normalfont\ldots? walther@60242: \begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \ 2))]\end{verbatim} jan@42370: The calculation is ok but no \ttfamily next \normalfont step found: jan@42370: Should be\\ \ttfamily nxt = Subproblem\normalfont! jan@42370: \item What shows \ttfamily trace\_script := true; \normalfont we read jan@42381: bottom up\ldots jan@42381: \begin{verbatim} jan@42381: @@@next leaf 'SubProblem jan@42381: (PolyEq',[abcFormula, degree_2, polynomial, jan@42381: univariate, equation], no_meth) jan@42381: [BOOL equ, REAL z]' walther@59717: ---> Program.Tac 'SubProblem (PolyEq', jan@42381: [abcFormula, degree_2, polynomial, jan@42381: univariate, equation], no_meth) jan@42381: [BOOL (-1 + -2 * z + 8 * z \^\^\^ ~2 = 0), REAL z]' jan@42381: \end{verbatim} jan@42370: We see the SubProblem with correct arguments from searching next walther@59717: step (program text !!!--->!!! Program.Tac (script tactic) with arguments jan@42370: evaluated.) wneuper@59585: \item Do we have the right Program \ldots difference in the jan@42381: arguments in the arguments\ldots jan@42381: \begin{verbatim} neuper@48790: val Prog s = Walther@60586: (#program o MethodC.from_store ctxt) ["SignalProcessing", jan@42381: "Z_Transform", neuper@42405: "Inverse"]; walther@59868: writeln (UnparseC.term s); jan@42381: \end{verbatim} jan@42370: \ldots shows the right script. Difference in the arguments. jan@42370: \item Test --- Why helpless here ? --- shows: \ttfamily replace wneuper@59585: no\_meth by [no\_meth] \normalfont in Program jan@42370: \end{itemize} wneuper@59472: \ jan@42300: wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Model_Problem";*) wneuper@59472: \ neuper@42279: wneuper@59472: text \\noindent Instead of \ttfamily nxt = Model\_Problem \normalfont above jan@42370: we had \ttfamily Empty\_Tac; \normalfont the search for the reason jan@42370: considered the following points:\begin{itemize} jan@42370: \item Difference in the arguments jan@42381: \item Comparison with Subsection~\ref{sec:solveq}: There solving this jan@42370: equation works, so there must be some difference in the arguments jan@42370: of the Subproblem: RIGHT: we had \ttfamily [no\_meth] \normalfont jan@42370: instead of \ttfamily [no\_met] \normalfont ;-) wneuper@59472: \end{itemize}\ jan@42338: wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; walther@60242: (*Add_Given equality (-1 + -2 * z + 8 * z \ 2 = 0)";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Add_Given solveFor z";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Add_Find solutions z_i";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Specify_Theory Isac";*) wneuper@59472: \ neuper@42279: wneuper@59472: text \\noindent We had \ttfamily nxt = Empty\_Tac instead Specify\_Theory; jan@42370: \normalfont The search for the reason considered the following points: jan@42370: \begin{itemize} jan@42370: \item Was there an error message? NO -- ok jan@42370: \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\ jan@42370: \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok jan@42381: \item What is the returned formula: jan@42381: \begin{verbatim} neuper@52101: print_depth 999; f; print_depth 3; jan@42381: { Find = [ Correct "solutions z_i"], jan@42381: With = [], walther@60242: Given = [Correct "equality (-1 + -2*z + 8*z \ 2 = 0)", jan@42381: Correct "solveFor z"], jan@42381: Where = [...], jan@42381: Relate = [] } jan@42381: \end{verbatim} jan@42370: \normalfont The only False is the reason: the Where (the precondition) is jan@42370: False for good reasons: The precondition seems to check for linear jan@42370: equations, not for the one we want to solve! Removed this error by wneuper@59585: correcting the Program from \ttfamily SubProblem (PolyEq', jan@42370: \lbrack linear,univariate,equation, jan@42370: test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to jan@42370: \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2, jan@42370: polynomial,univariate,equation\rbrack,\\ jan@42370: \lbrack PolyEq,solve\_d2\_polyeq\_abc\_equation jan@42370: \rbrack\normalfont jan@42370: You find the appropriate type of equation at the jan@42370: {\sisac}-WEB-Page\footnote{ jan@42370: \href{http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html} jan@42370: {http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html} jan@42370: } jan@42370: And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont jan@42370: at the respective \ttfamily store\_pbt. \normalfont Or you leave the wneuper@59585: selection of the appropriate type to isac as done in the final Program ;-)) wneuper@59472: \end{itemize}\ jan@42370: wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Specify_Problem [abcFormula,...";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59497: (*Rewrite_Set_Inst [(''bdv'', z)], d2_polyeq_abcFormula_simplify";*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59370: (*Specify_Method ["PolyEq", "normalise_poly"]*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59370: (*Apply_Method ["PolyEq", "normalise_poly"]*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Rewrite ("all_left", "PolyEq.all_left")*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59497: (*Rewrite_Set_Inst (["(''bdv'', A)"], "make_ratpoly_in")*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: (*Rewrite_Set "polyeq_simplify"*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; walther@59997: (*Subproblem("Isac_Knowledge",["degree_1", "polynomial", "univariate", "equation"])*) jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4, 5], Res) Check_Postcond*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11, 4], Res) Check_Postcond*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([11], Res) Take*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Frm) Substitute*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([12], Res) Rewrite*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([13], Res) Take*) neuper@42451: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([14], Frm) Empty_Tac*) wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ jan@42370: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ neuper@42281: wneuper@59472: ML \ walther@59901: LItool.trace_on := true; wneuper@59472: \ wneuper@59472: ML \ jan@42418: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59472: \ wneuper@59472: ML \ walther@59983: Test_Tool.show_pt pt; wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ wneuper@59472: ML \ wneuper@59472: \ jan@42418: wneuper@59472: text\\noindent As a last step we check the tracing output of the last calc Walther@60586: tree instruction and compare it with the where_-calculated result.\ neuper@42315: wneuper@59472: section \Improve and Transfer into Knowledge\ wneuper@59472: text \ neuper@42376: We want to improve the very long program \ttfamily InverseZTransform neuper@42376: \normalfont by modularisation: partial fraction decomposition shall neuper@42376: become a sub-problem. neuper@42376: neuper@42376: We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy neuper@42376: \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy neuper@42376: \normalfont and then modularise. In this case TODO problems?!? neuper@42376: neuper@42376: We chose another way and go bottom up: first we build the sub-problem in jan@42381: \ttfamily Partial\_Fractions.thy \normalfont with the term: neuper@42376: jan@42381: $$\frac{3}{x\cdot(z - \frac{1}{4} + \frac{-1}{8}\cdot\frac{1}{z})}$$ neuper@42376: jan@42381: \noindent (how this still can be improved see \ttfamily Partial\_Fractions.thy\normalfont), neuper@42376: and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy: jan@42381: \normalfont The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy jan@42381: \normalfont and the respective tests to: jan@42381: \begin{center}\ttfamily test/../sartial\_fractions.sml\normalfont\end{center} wneuper@59472: \ neuper@42279: wneuper@59472: subsection \Transfer to Partial\_Fractions.thy\ wneuper@59472: text \ jan@42381: First we transfer both, knowledge and tests into: jan@42381: \begin{center}\ttfamily src/../Partial\_Fractions.thy\normalfont\end{center} jan@42381: in order to immediately have the test results. neuper@42376: jan@42381: We copy \ttfamily factors\_from\_solution, drop\_questionmarks,\\ jan@42381: ansatz\_2nd\_order \normalfont and rule-sets --- no problem. jan@42381: jan@42381: Also \ttfamily store\_pbt ..\\ "pbl\_simp\_rat\_partfrac" neuper@42376: \normalfont is easy. neuper@42376: jan@42381: But then we copy from:\\ jan@42381: (1) \ttfamily Build\_Inverse\_Z\_Transform.thy store\_met\ldots "met\_SP\_Ztrans\_inv" jan@42381: \normalfont\\ to\\ jan@42381: (2) \ttfamily Partial\_Fractions.thy store\_met\ldots "met\_SP\_Ztrans\_inv" jan@42381: \normalfont\\ and cut out the respective part from the program. First we ensure that neuper@42376: the string is correct. When we insert the string into (2) jan@42381: \ttfamily store\_met .. "met\_partial\_fraction" \normalfont --- and get an error. wneuper@59472: \ neuper@42376: wneuper@59472: subsubsection \'Programming' in ISAC's TP-based Language\ wneuper@59472: text \ neuper@42376: At the present state writing programs in {\sisac} is particularly cumbersome. neuper@42376: So we give hints how to cope with the many obstacles. Below we describe the neuper@42376: steps we did in making (2) run. neuper@42376: neuper@42376: \begin{enumerate} neuper@42376: \item We check if the \textbf{string} containing the program is correct. neuper@42376: \item We check if the \textbf{types in the program} are correct. neuper@42376: For this purpose we start start with the first and last lines jan@42381: \begin{verbatim} jan@42381: "PartFracScript (f_f::real) (v_v::real) = " ^ jan@42381: " (let X = Take f_f; " ^ jan@42381: " pbz = ((Substitute []) X) " ^ jan@42381: " in pbz)" jan@42381: \end{verbatim} neuper@42376: The last but one line helps not to bother with ';'. neuper@42376: \item Then we add line by line. Already the first line causes the error. neuper@42376: So we investigate it by jan@42381: \begin{verbatim} neuper@48761: val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ; jan@42381: val SOME t = jan@42381: parseNEW ctxt "(num_orig::real) = jan@42381: get_numerator(rhs f_f)"; jan@42381: \end{verbatim} neuper@42376: and see a type clash: \ttfamily rhs \normalfont from (1) requires type jan@42381: \ttfamily bool \normalfont while (2) wants to have \ttfamily (f\_f::real). neuper@42376: \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore. neuper@42376: \item Type-checking can be very tedious. One might even inspect the jan@42381: parse-tree of the program with {\sisac}'s specific debug tools: jan@42381: \begin{verbatim} Walther@60586: val {program = Prog t,...} = Walther@60559: MethodC.from_store ctxt ["simplification", jan@42381: "of_rationals", jan@42381: "to_partial_fraction"]; neuper@42389: atomty_thy @{theory "Inverse_Z_Transform"} t ; jan@42381: \end{verbatim} neuper@42376: \item We check if the \textbf{semantics of the program} by stepwise evaluation neuper@42376: of the program. Evaluation is done by the Lucas-Interpreter, which works wneuper@59592: using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the neuper@42376: test are performed simplest in a file which is loaded with Isac. jan@42381: See \ttfamily tests/../partial\_fractions.sml \normalfont. neuper@42376: \end{enumerate} wneuper@59472: \ neuper@42376: wneuper@59472: subsection \Transfer to Inverse\_Z\_Transform.thy\ wneuper@59472: text \ neuper@42388: It was not possible to complete this task, because we ran out of time. wneuper@59472: \ neuper@42376: neuper@42376: neuper@42279: end neuper@42279: