1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jan 31 17:50:50 2014 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Feb 01 16:44:45 2014 +0100
1.3 @@ -246,6 +246,169 @@
1.4 ));
1.5
1.6 *}
1.7 +setup {* KEStore_Elems.add_mets
1.8 + [prep_met thy "met_SP" [] e_metID
1.9 + (["SignalProcessing"], [],
1.10 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.11 + errpats = [], nrls = e_rls}, "empty_script"),
1.12 + prep_met thy "met_SP_Ztrans" [] e_metID
1.13 + (["SignalProcessing", "Z_Transform"], [],
1.14 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.15 + errpats = [], nrls = e_rls}, "empty_script"),
1.16 + prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.17 + (["SignalProcessing", "Z_Transform", "Inverse"],
1.18 + [("#Given" ,["filterExpression (X_eq::bool)"]),
1.19 + ("#Find" ,["stepResponse (n_eq::bool)"])],
1.20 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.21 + errpats = [], nrls = e_rls},
1.22 + "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.23 + " (let X = Take X_eq;" ^
1.24 + " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
1.25 + " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
1.26 + " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
1.27 + " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
1.28 + " equ = (denom = (0::real));" ^
1.29 + " fun_arg = Take (lhs X');" ^
1.30 + " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
1.31 + " (L_L::bool list) = " ^
1.32 + " (SubProblem (Test', " ^
1.33 + " [LINEAR,univariate,equation,test]," ^
1.34 + " [Test,solve_linear]) " ^
1.35 + " [BOOL equ, REAL z]) " ^
1.36 + " in X)"),
1.37 + prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.38 + (["SignalProcessing", "Z_Transform", "Inverse"],
1.39 + [("#Given" ,["filterExpression X_eq"]),
1.40 + ("#Find" ,["stepResponse n_eq"])],
1.41 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
1.42 + crls = e_rls, errpats = [], nrls = e_rls},
1.43 + "Script InverseZTransform (X_eq::bool) = "^
1.44 + (*(1/z) instead of z ^^^ -1*)
1.45 + "(let X = Take X_eq; "^
1.46 + " X' = Rewrite ruleZY False X; "^
1.47 + (*z * denominator*)
1.48 + " (num_orig::real) = get_numerator (rhs X'); "^
1.49 + " X' = (Rewrite_Set norm_Rational False) X'; "^
1.50 + (*simplify*)
1.51 + " (X'_z::real) = lhs X'; "^
1.52 + " (zzz::real) = argument_in X'_z; "^
1.53 + " (funterm::real) = rhs X'; "^
1.54 + (*drop X' z = for equation solving*)
1.55 + " (denom::real) = get_denominator funterm; "^
1.56 + (*get_denominator*)
1.57 + " (num::real) = get_numerator funterm; "^
1.58 + (*get_numerator*)
1.59 + " (equ::bool) = (denom = (0::real)); "^
1.60 + " (L_L::bool list) = (SubProblem (PolyEq', "^
1.61 + " [abcFormula,degree_2,polynomial,univariate,equation], "^
1.62 + " [no_met]) "^
1.63 + " [BOOL equ, REAL zzz]); "^
1.64 + " (facs::real) = factors_from_solution L_L; "^
1.65 + " (eql::real) = Take (num_orig / facs); "^
1.66 +
1.67 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
1.68 +
1.69 + " (eq::bool) = Take (eql = eqr); "^
1.70 + (*Maybe possible to use HOLogic.mk_eq ??*)
1.71 + " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1.72 +
1.73 + " eq = drop_questionmarks eq; "^
1.74 + " (z1::real) = (rhs (NTH 1 L_L)); "^
1.75 + (*
1.76 + * prepare equation for a - eq_a
1.77 + * therefor substitute z with solution 1 - z1
1.78 + *)
1.79 + " (z2::real) = (rhs (NTH 2 L_L)); "^
1.80 +
1.81 + " (eq_a::bool) = Take eq; "^
1.82 + " eq_a = (Substitute [zzz=z1]) eq; "^
1.83 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1.84 + " (sol_a::bool list) = "^
1.85 + " (SubProblem (Isac', "^
1.86 + " [univariate,equation],[no_met]) "^
1.87 + " [BOOL eq_a, REAL (A::real)]); "^
1.88 + " (a::real) = (rhs(NTH 1 sol_a)); "^
1.89 +
1.90 + " (eq_b::bool) = Take eq; "^
1.91 + " eq_b = (Substitute [zzz=z2]) eq_b; "^
1.92 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1.93 + " (sol_b::bool list) = "^
1.94 + " (SubProblem (Isac', "^
1.95 + " [univariate,equation],[no_met]) "^
1.96 + " [BOOL eq_b, REAL (B::real)]); "^
1.97 + " (b::real) = (rhs(NTH 1 sol_b)); "^
1.98 +
1.99 + " eqr = drop_questionmarks eqr; "^
1.100 + " (pbz::real) = Take eqr; "^
1.101 + " pbz = ((Substitute [A=a, B=b]) pbz); "^
1.102 +
1.103 + " pbz = Rewrite ruleYZ False pbz; "^
1.104 + " pbz = drop_questionmarks pbz; "^
1.105 +
1.106 + " (X_z::bool) = Take (X_z = pbz); "^
1.107 + " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1.108 + " n_eq = drop_questionmarks n_eq "^
1.109 + "in n_eq)"),
1.110 + prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
1.111 + (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.112 + [("#Given" ,["filterExpression X_eq"]),
1.113 + ("#Find" ,["stepResponse n_eq"])],
1.114 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.115 + srls = Rls {id="srls_partial_fraction",
1.116 + preconds = [], rew_ord = ("termlessI",termlessI),
1.117 + erls = append_rls "erls_in_srls_partial_fraction" e_rls
1.118 + [(*for asm in NTH_CONS ...*)
1.119 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.120 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.121 + Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.122 + srls = Erls, calc = [], errpatts = [],
1.123 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.124 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.125 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.126 + Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
1.127 + Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
1.128 + Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.129 + Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.130 + Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.131 + Calc ("Partial_Fractions.factors_from_solution",
1.132 + eval_factors_from_solution "#factors_from_solution"),
1.133 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.134 + scr = EmptyScr},
1.135 + prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
1.136 + (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.137 + "Script InverseZTransform (X_eq::bool) = "^
1.138 + (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.139 + "(let X = Take X_eq; "^
1.140 + (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.141 + " X' = Rewrite ruleZY False X; "^
1.142 + (* ?X' z*)
1.143 + " (X'_z::real) = lhs X'; "^
1.144 + (* z *)
1.145 + " (zzz::real) = argument_in X'_z; "^
1.146 + (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.147 + " (funterm::real) = rhs X'; "^
1.148 +
1.149 + " (pbz::real) = (SubProblem (Isac', "^
1.150 + " [partial_fraction,rational,simplification], "^
1.151 + " [simplification,of_rationals,to_partial_fraction]) "^
1.152 + (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.153 + " [REAL funterm, REAL zzz]); "^
1.154 +
1.155 + (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.156 + " (pbz_eq::bool) = Take (X'_z = pbz); "^
1.157 + (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.158 + " pbz_eq = Rewrite ruleYZ False pbz_eq; "^
1.159 + (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.160 + " pbz_eq = drop_questionmarks pbz_eq; "^
1.161 + (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.162 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
1.163 + (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.164 + " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^
1.165 + (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.166 + " n_eq = drop_questionmarks n_eq "^
1.167 + (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.168 + "in n_eq)")]
1.169 +*}
1.170
1.171 end
1.172