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: neuper@42279: 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: jan@42366: ML {* jan@42366: val inverse_z = prep_rls( jan@42366: Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), neuper@42451: erls = Erls, srls = Erls, calc = [], errpatts = [], jan@42366: rules = jan@42367: [ jan@42367: Thm ("rule4",num_str @{thm rule4}) jan@42366: ], jan@42366: scr = EmptyScr}:rls); jan@42366: *} jan@42366: jan@42366: jan@42366: text {*store the rule set for math engine*} jan@42366: jan@42366: ML {* jan@42366: ruleset' := overwritelthy @{theory} (!ruleset', jan@42366: [("inverse_z", inverse_z) jan@42366: ]); jan@42366: *} jan@42366: neuper@42256: subsection{*Define the Specification*} neuper@42256: ML {* neuper@42256: val thy = @{theory}; neuper@42278: neuper@42256: store_pbt neuper@42256: (prep_pbt thy "pbl_SP" [] e_pblID neuper@42256: (["SignalProcessing"], [], e_rls, NONE, [])); neuper@42256: store_pbt neuper@42256: (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID neuper@42256: (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])); neuper@42256: store_pbt neuper@42256: (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID neuper@42405: (["Inverse", "Z_Transform", "SignalProcessing"], neuper@42407: (*^ capital letter breaks coding standard neuper@42407: because "inverse" = Const ("Rings.inverse_class.inverse", ..*) neuper@42278: [("#Given" ,["filterExpression (X_eq::bool)"]), neuper@42278: ("#Find" ,["stepResponse (n_eq::bool)"]) neuper@42256: ], neuper@42256: append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, neuper@42405: [["SignalProcessing","Z_Transform","Inverse"]])); neuper@42256: *} neuper@42412: ML {* neuper@42412: store_pbt neuper@42412: (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID neuper@42412: (["Inverse", "Z_Transform", "SignalProcessing"], neuper@42412: [("#Given" ,["filterExpression X_eq"]), neuper@42412: ("#Find" ,["stepResponse n_eq"]) neuper@42412: ], neuper@42412: append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, neuper@42412: [["SignalProcessing","Z_Transform","Inverse"]])); neuper@42412: *} neuper@42256: neuper@42256: subsection {*Define Name and Signature for the Method*} neuper@42256: consts neuper@42256: InverseZTransform :: "[bool, bool] => bool" neuper@42256: ("((Script InverseZTransform (_ =))// (_))" 9) neuper@42256: neuper@42277: subsection {*Setup Parent Nodes in Hierarchy of Method*} neuper@42256: ML {* neuper@42256: store_met neuper@42256: (prep_met thy "met_SP" [] e_metID neuper@42256: (["SignalProcessing"], [], neuper@42256: {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, neuper@42425: crls = e_rls, errpats = [], nrls = e_rls}, "empty_script")); neuper@42256: store_met neuper@42256: (prep_met thy "met_SP_Ztrans" [] e_metID neuper@42256: (["SignalProcessing", "Z_Transform"], [], neuper@42256: {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, neuper@42425: crls = e_rls, errpats = [], nrls = e_rls}, "empty_script")); neuper@42256: val thy = @{theory}; (*latest version of thy required*) neuper@42256: store_met neuper@42256: (prep_met thy "met_SP_Ztrans_inv" [] e_metID neuper@42405: (["SignalProcessing", "Z_Transform", "Inverse"], neuper@42278: [("#Given" ,["filterExpression (X_eq::bool)"]), neuper@42278: ("#Find" ,["stepResponse (n_eq::bool)"]) neuper@42256: ], neuper@42256: {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, neuper@42425: crls = e_rls, errpats = [], nrls = e_rls}, neuper@42281: "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) neuper@42281: " (let X = Take X_eq;" ^ neuper@42281: " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) neuper@42281: " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) neuper@42290: " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) neuper@42290: " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*) neuper@42290: " equ = (denom = (0::real));" ^ neuper@42290: " fun_arg = Take (lhs X');" ^ neuper@42290: " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*) neuper@42290: " (L_L::bool list) = " ^ neuper@42290: " (SubProblem (Test', " ^ neuper@42290: " [linear,univariate,equation,test]," ^ neuper@42290: " [Test,solve_linear]) " ^ neuper@42290: " [BOOL equ, REAL z]) " ^ neuper@42281: " in X)" neuper@42256: )); neuper@42256: *} neuper@42412: ML {* neuper@42412: store_met( neuper@42412: prep_met thy "met_SP_Ztrans_inv" [] e_metID neuper@42412: (["SignalProcessing", neuper@42412: "Z_Transform", neuper@42412: "Inverse"], neuper@42412: [ neuper@42412: ("#Given" ,["filterExpression X_eq"]), neuper@42412: ("#Find" ,["stepResponse n_eq"]) neuper@42412: ], neuper@42412: { neuper@42412: rew_ord'="tless_true", neuper@42412: rls'= e_rls, calc = [], neuper@42413: srls = srls_partial_fraction, neuper@42412: prls = e_rls, neuper@42425: crls = e_rls, errpats = [], nrls = e_rls neuper@42412: }, neuper@42412: "Script InverseZTransform (X_eq::bool) = "^ neuper@42412: (*(1/z) instead of z ^^^ -1*) neuper@42412: "(let X = Take X_eq; "^ neuper@42412: " X' = Rewrite ruleZY False X; "^ neuper@42412: (*z * denominator*) neuper@42412: " (num_orig::real) = get_numerator (rhs X'); "^ neuper@42412: " X' = (Rewrite_Set norm_Rational False) X'; "^ neuper@42412: (*simplify*) neuper@42412: " (X'_z::real) = lhs X'; "^ neuper@42412: " (zzz::real) = argument_in X'_z; "^ neuper@42412: " (funterm::real) = rhs X'; "^ neuper@42412: (*drop X' z = for equation solving*) neuper@42412: " (denom::real) = get_denominator funterm; "^ neuper@42412: (*get_denominator*) neuper@42412: " (num::real) = get_numerator funterm; "^ neuper@42412: (*get_numerator*) neuper@42412: " (equ::bool) = (denom = (0::real)); "^ neuper@42412: " (L_L::bool list) = (SubProblem (PolyEq', "^ neuper@42412: " [abcFormula,degree_2,polynomial,univariate,equation], "^ neuper@42412: " [no_met]) "^ neuper@42412: " [BOOL equ, REAL zzz]); "^ neuper@42412: " (facs::real) = factors_from_solution L_L; "^ neuper@42412: " (eql::real) = Take (num_orig / facs); "^ neuper@42412: neuper@42412: " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^ neuper@42412: neuper@42412: " (eq::bool) = Take (eql = eqr); "^ neuper@42412: (*Maybe possible to use HOLogic.mk_eq ??*) neuper@42412: " eq = (Try (Rewrite_Set equival_trans False)) eq; "^ neuper@42412: neuper@42412: " eq = drop_questionmarks eq; "^ neuper@42412: " (z1::real) = (rhs (NTH 1 L_L)); "^ neuper@42412: (* neuper@42412: * prepare equation for a - eq_a neuper@42412: * therefor substitute z with solution 1 - z1 neuper@42412: *) neuper@42412: " (z2::real) = (rhs (NTH 2 L_L)); "^ neuper@42412: neuper@42412: " (eq_a::bool) = Take eq; "^ neuper@42412: " eq_a = (Substitute [zzz=z1]) eq; "^ neuper@42412: " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^ neuper@42412: " (sol_a::bool list) = "^ neuper@42412: " (SubProblem (Isac', "^ neuper@42412: " [univariate,equation],[no_met]) "^ neuper@42412: " [BOOL eq_a, REAL (A::real)]); "^ neuper@42412: " (a::real) = (rhs(NTH 1 sol_a)); "^ neuper@42412: neuper@42412: " (eq_b::bool) = Take eq; "^ neuper@42412: " eq_b = (Substitute [zzz=z2]) eq_b; "^ neuper@42412: " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^ neuper@42412: " (sol_b::bool list) = "^ neuper@42412: " (SubProblem (Isac', "^ neuper@42412: " [univariate,equation],[no_met]) "^ neuper@42412: " [BOOL eq_b, REAL (B::real)]); "^ neuper@42412: " (b::real) = (rhs(NTH 1 sol_b)); "^ neuper@42412: neuper@42412: " eqr = drop_questionmarks eqr; "^ neuper@42412: " (pbz::real) = Take eqr; "^ neuper@42412: " pbz = ((Substitute [A=a, B=b]) pbz); "^ neuper@42412: neuper@42412: " pbz = Rewrite ruleYZ False pbz; "^ neuper@42412: " pbz = drop_questionmarks pbz; "^ neuper@42412: neuper@42412: " (X_z::bool) = Take (X_z = pbz); "^ neuper@42412: " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^ neuper@42412: " n_eq = drop_questionmarks n_eq "^ neuper@42412: "in n_eq)" neuper@42412: ) neuper@42412: ); neuper@42417: neuper@42417: store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID neuper@42417: (["SignalProcessing", "Z_Transform", "Inverse_sub"], neuper@42417: [("#Given" ,["filterExpression X_eq"]), neuper@42417: ("#Find" ,["stepResponse n_eq"])], neuper@42417: {rew_ord'="tless_true", neuper@42417: rls'= e_rls, calc = [], neuper@42417: srls = Rls {id="srls_partial_fraction", neuper@42417: preconds = [], neuper@42417: rew_ord = ("termlessI",termlessI), neuper@42417: erls = append_rls "erls_in_srls_partial_fraction" e_rls neuper@42417: [(*for asm in NTH_CONS ...*) neuper@42417: Calc ("Orderings.ord_class.less",eval_equ "#less_"), neuper@42417: (*2nd NTH_CONS pushes n+-1 into asms*) neuper@42417: Calc("Groups.plus_class.plus", eval_binop "#add_")], neuper@42451: srls = Erls, calc = [], errpatts = [], neuper@42417: rules = [ neuper@42417: Thm ("NTH_CONS",num_str @{thm NTH_CONS}), neuper@42417: Calc("Groups.plus_class.plus", eval_binop "#add_"), neuper@42417: Thm ("NTH_NIL",num_str @{thm NTH_NIL}), neuper@42417: Calc("Tools.lhs", eval_lhs "eval_lhs_"), neuper@42417: Calc("Tools.rhs", eval_rhs"eval_rhs_"), neuper@42417: Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), neuper@42417: Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), neuper@42417: Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), neuper@42417: Calc("Partial_Fractions.factors_from_solution", neuper@42417: eval_factors_from_solution "#factors_from_solution"), neuper@42417: Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")], neuper@42417: scr = EmptyScr}, neuper@42425: prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational}, neuper@42417: "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) neuper@42417: "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) neuper@42417: " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42417: " (X'_z::real) = lhs X'; "^(* ?X' z*) neuper@42417: " (zzz::real) = argument_in X'_z; "^(* z *) neuper@42417: " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) neuper@42417: neuper@42417: " (pbz::real) = (SubProblem (Isac', "^(**) neuper@42417: " [partial_fraction,rational,simplification], "^ neuper@42417: " [simplification,of_rationals,to_partial_fraction]) "^ neuper@42421: " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42417: neuper@42421: " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) neuper@42421: " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) neuper@42421: " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42421: " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) neuper@42421: " 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]*) neuper@42421: " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42417: "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) neuper@42417: )); neuper@42417: neuper@42412: *} neuper@42256: neuper@42256: end neuper@42256: