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