neuper@42256: (* Title: Test_Z_Transform neuper@42256: Author: Jan Rocnik neuper@42256: (c) copyright due to lincense terms. neuper@42256: *) neuper@42256: neuper@42290: theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin neuper@42256: neuper@42256: axiomatization where neuper@42256: rule1: "1 = \[n]" and neuper@42256: rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and neuper@42256: rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and jan@42367: rule4: "c * (z / (z - \)) = c * \^^^n * u [n]" and neuper@42256: rule5: "|| z || < || \ || ==> z / (z - \) = -(\^^^n) * u [-n - 1]" and jan@42367: rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and jan@42367: rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*) neuper@42256: neuper@42256: axiomatization where wneuper@59537: (*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))" ..looks better, but types are flawed*) jan@42367: ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and wneuper@59537: ruleYZ: "a / (z - b) + c / (z - d) = a * (z / (z - b)) + c * (z / (z - d))" and wneuper@59537: ruleYZa: "(a / b + c / d) = (a * (z / b) + c * (z / d))" \ \that is what students learn\ neuper@42256: wneuper@59472: subsection\Define the Field Descriptions for the specification\ neuper@42279: consts neuper@42279: filterExpression :: "bool => una" neuper@42279: stepResponse :: "bool => una" neuper@42279: wneuper@59472: ML \ s1210629013@55444: val inverse_z = prep_rls'( wneuper@59416: Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), wneuper@59416: erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], jan@42366: rules = jan@42367: [ wneuper@59416: Rule.Thm ("rule4", @{thm rule4}) jan@42366: ], wneuper@59416: scr = Rule.EmptyScr}); wneuper@59472: \ jan@42366: jan@42366: wneuper@59472: text \store the rule set for math engine\ jan@42366: wneuper@59472: setup \KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))]\ jan@42366: wneuper@59472: subsection\Define the Specification\ wneuper@59472: ML \ neuper@42256: val thy = @{theory}; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_pbts wneuper@59416: [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])), wneuper@59406: (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID wneuper@59416: (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])), wneuper@59406: (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID s1210629013@55339: (["Inverse", "Z_Transform", "SignalProcessing"], s1210629013@55339: [("#Given" ,["filterExpression X_eq"]), s1210629013@55339: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, wneuper@59538: [["SignalProcessing","Z_Transform","Inverse"]])), wneuper@59538: (Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID wneuper@59538: (["Inverse_sub", "Z_Transform", "SignalProcessing"], wneuper@59538: [("#Given" ,["filterExpression X_eq"]), wneuper@59538: ("#Find" ,["stepResponse n_eq"])], wneuper@59538: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, wneuper@59538: [["SignalProcessing","Z_Transform","Inverse_sub"]]))]\ neuper@42256: wneuper@59472: subsection \Define Name and Signature for the Method\ neuper@42256: consts wneuper@59538: InverseZTransform1 :: "[bool, bool] => bool" wneuper@59538: ("((Script InverseZTransform1 (_ =))// (_))" 9) wneuper@59538: InverseZTransform2 :: "[bool, real, bool] => bool" wneuper@59538: ("((Script InverseZTransform2 (_ _ =))// (_))" 9) neuper@42256: wneuper@59472: subsection \Setup Parent Nodes in Hierarchy of Method\ wneuper@59472: ML \val thy = @{theory}; (*latest version of thy required*)\ wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP" [] Celem.e_metID s1210629013@55373: (["SignalProcessing"], [], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59545: errpats = [], nrls = Rule.e_rls}, @{thm refl}), wneuper@59406: Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform"], [], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59545: errpats = [], nrls = Rule.e_rls}, @{thm refl})] wneuper@59473: \ wneuper@59545: wneuper@59545: (*WARNING: Additional type variable(s) in specification of "inverse_ztransform": 'a *) wneuper@59545: partial_function (tailrec) inverse_ztransform :: "bool \ real \ bool" wneuper@59504: where wneuper@59545: "inverse_ztransform X_eq z = \ \(1/z) instead of z ^^^ -1\ wneuper@59504: (let X = Take X_eq; wneuper@59504: X' = Rewrite ''ruleZY'' False X; \ \z * denominator\ wneuper@59504: X' = (Rewrite_Set ''norm_Rational'' False) X'; \ \simplify\ wneuper@59504: funterm = Take (rhs X'); \ \drop X' z = for equation solving\ wneuper@59504: denom = (Rewrite_Set ''partial_fraction'' False) funterm; \ \get_denominator\ wneuper@59504: equ = (denom = (0::real)); wneuper@59504: fun_arg = Take (lhs X'); wneuper@59504: arg = (Rewrite_Set ''partial_fraction'' False) X'; \ \get_argument TODO\ wneuper@59504: L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], wneuper@59543: [''Test'',''solve_linear'']) [BOOL equ, REAL z] \ \PROG string\ wneuper@59504: in X) " wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID wneuper@59538: (["SignalProcessing", "Z_Transform", "Inverse"], s1210629013@55373: [("#Given" ,["filterExpression (X_eq::bool)"]), s1210629013@55373: ("#Find" ,["stepResponse (n_eq::bool)"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59416: errpats = [], nrls = Rule.e_rls}, wneuper@59545: @{thm inverse_ztransform.simps} wneuper@59545: (*"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) s1210629013@55373: " (let X = Take X_eq;" ^ wneuper@59489: " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) wneuper@59489: " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) s1210629013@55373: " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) wneuper@59489: " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) s1210629013@55373: " equ = (denom = (0::real));" ^ s1210629013@55373: " fun_arg = Take (lhs X');" ^ wneuper@59489: " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*) s1210629013@55373: " (L_L::bool list) = " ^ wneuper@59489: " (SubProblem (''Test'', " ^ wneuper@59489: " [''LINEAR'',''univariate'',''equation'',''test'']," ^ wneuper@59489: " [''Test'',''solve_linear'']) " ^ s1210629013@55373: " [BOOL equ, REAL z]) " ^ wneuper@59545: " in X)"*))] wneuper@59473: \ wneuper@59538: wneuper@59538: partial_function (tailrec) inverse_ztransform2 :: "bool \ real \ bool" wneuper@59504: where wneuper@59538: "inverse_ztransform2 X_eq X_z = wneuper@59504: (let X = Take X_eq; wneuper@59538: X' = Rewrite ''ruleZY'' False X; wneuper@59538: X'_z = lhs X'; wneuper@59538: zzz = argument_in X'_z; wneuper@59538: funterm = rhs X'; wneuper@59538: pbz = SubProblem (''Isac'', wneuper@59538: [''partial_fraction'',''rational'',''simplification''], wneuper@59538: [''simplification'',''of_rationals'',''to_partial_fraction'']) wneuper@59538: [REAL funterm, REAL zzz]; wneuper@59538: pbz_eq = Take (X'_z = pbz); wneuper@59538: pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; wneuper@59538: X_zeq = Take (X_z = rhs pbz_eq); wneuper@59538: n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq wneuper@59538: in n_eq)" wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID wneuper@59538: (["SignalProcessing", "Z_Transform", "Inverse_sub"], wneuper@59538: [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]), s1210629013@55373: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], wneuper@59416: srls = Rule.Rls {id="srls_partial_fraction", s1210629013@55373: preconds = [], rew_ord = ("termlessI",termlessI), wneuper@59416: erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls s1210629013@55373: [(*for asm in NTH_CONS ...*) wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), s1210629013@55373: (*2nd NTH_CONS pushes n+-1 into asms*) wneuper@59416: Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")], wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Thm ("NTH_NIL", @{thm NTH_NIL}), wneuper@59491: Rule.Calc ("Tools.lhs", Tools.eval_lhs "eval_lhs_"), wneuper@59491: Rule.Calc ("Tools.rhs", Tools.eval_rhs"eval_rhs_"), wneuper@59416: Rule.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), wneuper@59416: Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"), wneuper@59416: Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), wneuper@59416: Rule.Calc ("Partial_Fractions.factors_from_solution", wneuper@59512: eval_factors_from_solution "#factors_from_solution") wneuper@59512: ], scr = Rule.EmptyScr}, wneuper@59416: prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, wneuper@59545: @{thm simplify.simps} wneuper@59545: (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) wneuper@59538: " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) wneuper@59538: " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59538: " (X'_z::real) = lhs X'; "^ (* ?X' z*) wneuper@59538: " (zzz::real) = argument_in X'_z; "^ (* z *) wneuper@59538: " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59538: " (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) wneuper@59538: " [''partial_fraction'',''rational'',''simplification''], "^ wneuper@59538: " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^ wneuper@59538: " [REAL funterm, REAL zzz]); "^ wneuper@59538: " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) wneuper@59538: " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) wneuper@59538: " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) wneuper@59538: " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) wneuper@59545: " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) wneuper@59472: \ neuper@42256: neuper@42256: end neuper@42256: