neuper@42256: (* Title: Test_Z_Transform neuper@42256: Author: Jan Rocnik neuper@42256: (c) copyright due to lincense terms. neuper@42256: 12345678901234567890123456789012345678901234567890123456789012345678901234567890 neuper@42256: 10 20 30 40 50 60 70 80 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 jan@42367: ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and jan@42367: ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" 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: jan@42366: 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: (*^ capital letter breaks coding standard s1210629013@55339: because "inverse" = Const ("Rings.inverse_class.inverse", ..*) s1210629013@55339: [("#Given" ,["filterExpression (X_eq::bool)"]), s1210629013@55339: ("#Find" ,["stepResponse (n_eq::bool)"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, s1210629013@55339: [["SignalProcessing","Z_Transform","Inverse"]])), 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@59472: [["SignalProcessing","Z_Transform","Inverse"]]))]\ neuper@42256: wneuper@59472: subsection \Define Name and Signature for the Method\ neuper@42256: consts neuper@42256: InverseZTransform :: "[bool, bool] => bool" neuper@42256: ("((Script InverseZTransform (_ =))// (_))" 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@59416: errpats = [], nrls = Rule.e_rls}, "empty_script"), 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@59473: errpats = [], nrls = Rule.e_rls}, "empty_script")] wneuper@59473: \ wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID s1210629013@55373: (["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}, s1210629013@55373: "Script InverseZTransform (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@59473: " in X)")] wneuper@59473: \ wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform", "Inverse"], s1210629013@55373: [("#Given" ,["filterExpression X_eq"]), s1210629013@55373: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls, wneuper@59416: crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, s1210629013@55373: "Script InverseZTransform (X_eq::bool) = "^ s1210629013@55373: (*(1/z) instead of z ^^^ -1*) s1210629013@55373: "(let X = Take X_eq; "^ wneuper@59489: " X' = Rewrite ''ruleZY'' False X; "^ s1210629013@55373: (*z * denominator*) s1210629013@55373: " (num_orig::real) = get_numerator (rhs X'); "^ wneuper@59489: " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^ s1210629013@55373: (*simplify*) s1210629013@55373: " (X'_z::real) = lhs X'; "^ s1210629013@55373: " (zzz::real) = argument_in X'_z; "^ s1210629013@55373: " (funterm::real) = rhs X'; "^ s1210629013@55373: (*drop X' z = for equation solving*) s1210629013@55373: " (denom::real) = get_denominator funterm; "^ s1210629013@55373: (*get_denominator*) s1210629013@55373: " (num::real) = get_numerator funterm; "^ s1210629013@55373: (*get_numerator*) s1210629013@55373: " (equ::bool) = (denom = (0::real)); "^ wneuper@59489: " (L_L::bool list) = (SubProblem (''PolyEq'', "^ wneuper@59489: " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^ wneuper@59489: " [''no_met'']) "^ s1210629013@55373: " [BOOL equ, REAL zzz]); "^ s1210629013@55373: " (facs::real) = factors_from_solution L_L; "^ s1210629013@55373: " (eql::real) = Take (num_orig / facs); "^ s1210629013@55373: wneuper@59499: " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; "^ s1210629013@55373: s1210629013@55373: " (eq::bool) = Take (eql = eqr); "^ s1210629013@55373: (*Maybe possible to use HOLogic.mk_eq ??*) wneuper@59489: " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^ s1210629013@55373: s1210629013@55373: " eq = drop_questionmarks eq; "^ s1210629013@55373: " (z1::real) = (rhs (NTH 1 L_L)); "^ s1210629013@55373: (* s1210629013@55373: * prepare equation for a - eq_a s1210629013@55373: * therefor substitute z with solution 1 - z1 s1210629013@55373: *) s1210629013@55373: " (z2::real) = (rhs (NTH 2 L_L)); "^ s1210629013@55373: s1210629013@55373: " (eq_a::bool) = Take eq; "^ s1210629013@55373: " eq_a = (Substitute [zzz=z1]) eq; "^ wneuper@59499: " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; "^ s1210629013@55373: " (sol_a::bool list) = "^ wneuper@59489: " (SubProblem (''Isac'', "^ wneuper@59489: " [''univariate'',''equation''],[''no_met'']) "^ s1210629013@55373: " [BOOL eq_a, REAL (A::real)]); "^ s1210629013@55373: " (a::real) = (rhs(NTH 1 sol_a)); "^ s1210629013@55373: s1210629013@55373: " (eq_b::bool) = Take eq; "^ s1210629013@55373: " eq_b = (Substitute [zzz=z2]) eq_b; "^ wneuper@59489: " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^ s1210629013@55373: " (sol_b::bool list) = "^ wneuper@59489: " (SubProblem (''Isac'', "^ wneuper@59489: " [''univariate'',''equation''],[''no_met'']) "^ s1210629013@55373: " [BOOL eq_b, REAL (B::real)]); "^ s1210629013@55373: " (b::real) = (rhs(NTH 1 sol_b)); "^ s1210629013@55373: s1210629013@55373: " eqr = drop_questionmarks eqr; "^ s1210629013@55373: " (pbz::real) = Take eqr; "^ s1210629013@55373: " pbz = ((Substitute [A=a, B=b]) pbz); "^ s1210629013@55373: wneuper@59489: " pbz = Rewrite ''ruleYZ'' False pbz; "^ s1210629013@55373: " pbz = drop_questionmarks pbz; "^ s1210629013@55373: s1210629013@55373: " (X_z::bool) = Take (X_z = pbz); "^ wneuper@59489: " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z; "^ s1210629013@55373: " n_eq = drop_questionmarks n_eq "^ wneuper@59473: "in n_eq)")] wneuper@59473: \ wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform", "Inverse_sub"], s1210629013@55373: [("#Given" ,["filterExpression X_eq"]), 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", s1210629013@55373: eval_factors_from_solution "#factors_from_solution"), wneuper@59416: Rule.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")], wneuper@59416: scr = Rule.EmptyScr}, wneuper@59416: prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, s1210629013@55373: (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) s1210629013@55373: "Script InverseZTransform (X_eq::bool) = "^ s1210629013@55373: (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) s1210629013@55373: "(let X = Take X_eq; "^ s1210629013@55373: (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59489: " X' = Rewrite ''ruleZY'' False X; "^ s1210629013@55373: (* ?X' z*) s1210629013@55373: " (X'_z::real) = lhs X'; "^ s1210629013@55373: (* z *) s1210629013@55373: " (zzz::real) = argument_in X'_z; "^ s1210629013@55373: (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) s1210629013@55373: " (funterm::real) = rhs X'; "^ s1210629013@55373: wneuper@59489: " (pbz::real) = (SubProblem (''Isac'', "^ wneuper@59489: " [''partial_fraction'',''rational'',''simplification''], "^ wneuper@59489: " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^ s1210629013@55373: (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) s1210629013@55373: " [REAL funterm, REAL zzz]); "^ s1210629013@55373: s1210629013@55373: (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) s1210629013@55373: " (pbz_eq::bool) = Take (X'_z = pbz); "^ s1210629013@55373: (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) wneuper@59489: " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ s1210629013@55373: (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) s1210629013@55373: " pbz_eq = drop_questionmarks pbz_eq; "^ s1210629013@55373: (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) s1210629013@55373: " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ s1210629013@55373: (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) wneuper@59489: " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq; "^ s1210629013@55373: (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) s1210629013@55373: " n_eq = drop_questionmarks n_eq "^ s1210629013@55373: (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) s1210629013@55373: "in n_eq)")] wneuper@59472: \ neuper@42256: neuper@42256: end neuper@42256: