1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat May 05 15:16:13 2012 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat May 05 23:54:28 2012 +0200
1.3 @@ -207,6 +207,56 @@
1.4 "in n_eq)"
1.5 )
1.6 );
1.7 +
1.8 +store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
1.9 + (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.10 + [("#Given" ,["filterExpression X_eq"]),
1.11 + ("#Find" ,["stepResponse n_eq"])],
1.12 + {rew_ord'="tless_true",
1.13 + rls'= e_rls, calc = [],
1.14 + srls = Rls {id="srls_partial_fraction",
1.15 + preconds = [],
1.16 + rew_ord = ("termlessI",termlessI),
1.17 + erls = append_rls "erls_in_srls_partial_fraction" e_rls
1.18 + [(*for asm in NTH_CONS ...*)
1.19 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.20 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.21 + Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.22 + srls = Erls, calc = [],
1.23 + rules = [
1.24 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.25 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.26 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.27 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.28 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.29 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.30 + Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.31 + Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.32 + Calc("Partial_Fractions.factors_from_solution",
1.33 + eval_factors_from_solution "#factors_from_solution"),
1.34 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.35 + scr = EmptyScr},
1.36 + prls = e_rls, crls = e_rls, nrls = norm_Rational},
1.37 + "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.38 + "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.39 + " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.40 + " (X'_z::real) = lhs X'; "^(* ?X' z*)
1.41 + " (zzz::real) = argument_in X'_z; "^(* z *)
1.42 + " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.43 +
1.44 + " (pbz::real) = (SubProblem (Isac', "^(**)
1.45 + " [partial_fraction,rational,simplification], "^
1.46 + " [simplification,of_rationals,to_partial_fraction]) "^
1.47 + " [REAL funterm, REAL zzz]); "^(**)
1.48 +
1.49 + " pbz = Rewrite ruleYZ False pbz; "^(*([13], Res), 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.50 + " pbz = drop_questionmarks pbz; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.51 + " (X_z::bool) = Take (X_z = pbz); "^(*([14], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.52 + " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;"^(*([14], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.53 + " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.54 + "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.55 + ));
1.56 +
1.57 *}
1.58
1.59 end
2.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat May 05 15:16:13 2012 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat May 05 23:54:28 2012 +0200
2.3 @@ -184,7 +184,7 @@
2.4 leading coefficient of the denominator is 1: to be checked here! and..
2.5 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
2.6 ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
2.7 - ("#Find" ,["decomposedFunction p_p"])
2.8 + ("#Find" ,["decomposedFunction p_p'''"])
2.9 ],
2.10 append_rls "e_rls" e_rls [(*for preds in where_ TODO*)],
2.11 NONE,
2.12 @@ -229,7 +229,7 @@
2.13 val SOME t = parseNEW ctxt "eqr = drop_questionmarks eqr";
2.14 *}
2.15 ML {*
2.16 -parseNEW ctxt "decomposedFunction p_p";
2.17 +parseNEW ctxt "decomposedFunction p_p'''";
2.18 parseNEW ctxt "decomposedFunction";
2.19 *}
2.20 ML {*
2.21 @@ -241,7 +241,7 @@
2.22 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
2.23 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
2.24 ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
2.25 - ("#Find" ,["decomposedFunction p_p"])],
2.26 + ("#Find" ,["decomposedFunction p_p'''"])],
2.27 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
2.28 crls = e_rls, nrls = e_rls}, (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
2.29 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
3.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Sat May 05 15:16:13 2012 +0200
3.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Sat May 05 23:54:28 2012 +0200
3.3 @@ -9,7 +9,8 @@
3.4 "table of contents -----------------------------------------------";
3.5 "-----------------------------------------------------------------";
3.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
3.7 -"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
3.8 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
3.9 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.10 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
3.11 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
3.12 "-----------------------------------------------------------------";
3.13 @@ -21,13 +22,13 @@
3.14 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
3.15 get_met ["SignalProcessing","Z_Transform","Inverse"];
3.16
3.17 -"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
3.18 -"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
3.19 -"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
3.20 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
3.21 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
3.22 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
3.23 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.24 "stepResponse (x[n::real]::bool)"];
3.25 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.26 - ["SignalProcessing", "Z_Transform", "Inverse"]);
3.27 + ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
3.28 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
3.29 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
3.30 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *)
3.31 @@ -35,39 +36,60 @@
3.32 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
3.33 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
3.34 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method *)
3.35 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
3.36 - (*([1], Frm)*)
3.37 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
3.38 - (*([1], Res)*)
3.39 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Subproblem --- why NOT solve ?!?*)
3.40 - f2str fb = "?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
3.41 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res)Model_Problem*)
3.42 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
3.43 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleZY", "Inverse_Z_Transform.ruleZY")*)
3.44 + (*([1], Frm)*)f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
3.45 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["partial_fraction", "rational..*)
3.46 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
3.47 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "functionTerm (X' z)"*)
3.48 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
3.49 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions z_i"*)
3.50 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "decomposedFunction p_p'''"*)
3.51 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory*)
3.52 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
3.53 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
3.54 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method*)
3.55 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0";
3.56 - (*([3, 1], Frm)*)
3.57 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / "^
3.58 - "(2 * 8) |\nz = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)";
3.59 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = 1 / 2 | z = -1 / 4";
3.60 - (*([3, 2], Res)*)
3.61 -if f2str fb = "z = 1 / 2 | z = -1 / 4" andalso p = ([3, 2], Res)
3.62 - then () else error "begin of 'inv Z', exp 1 me changed"
3.63 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "norm_Rational"*)
3.64 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
3.65 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.66 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.67 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.68 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.69 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.70 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.71 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.72 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"*)
3.73 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.74 +if f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0"andalso p = ([2, 2, 1], Frm)
3.75 +then () else error "begin of 'inv Z', exp 1 me changed";
3.76 +
3.77 show_pt pt;
3.78 (*[
3.79 (([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
3.80 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
3.81 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
3.82 -(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
3.83 -(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
3.84 -(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)]
3.85 -(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
3.86 - z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
3.87 -(([3,2], Res), z = 1 / 2 | z = -1 / 4)] *)
3.88 +(([2], Pbl), Problem (Isac, [partial_fraction, rational, simplification])),
3.89 +(([2,1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
3.90 +(([2,1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
3.91 +(([2,2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
3.92 +(([2,2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)] *)
3.93 +
3.94 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.95 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.96 +"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.97 +states:= [];
3.98 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.99 + "stepResponse (x[n::real]::bool)"];
3.100 +val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.101 + ["SignalProcessing", "Z_Transform", "Inverse"]);
3.102 +CalcTree [(fmz, (dI,pI,mI))];
3.103 +Iterator 1;
3.104 +moveActiveRoot 1;
3.105 +autoCalculate 1 CompleteCalc;
3.106 +
3.107 +val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
3.108 +val (Form f, tac, asms) = pt_extract (pt, p);
3.109 +if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
3.110 + andalso p = ([], Res) then ()
3.111 + else error "inv Z, exp 1 autoCalculate changed"
3.112
3.113
3.114 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
4.1 --- a/test/Tools/isac/Test_Some.thy Sat May 05 15:16:13 2012 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Sat May 05 23:54:28 2012 +0200
4.3 @@ -9,185 +9,12 @@
4.4 print_depth 5;
4.5 *}
4.6 ML {* (*==================*)
4.7 -store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
4.8 - (["SignalProcessing", "Z_Transform", "Inverse_sub"],
4.9 - [("#Given" ,["filterExpression X_eq"]),
4.10 - ("#Find" ,["stepResponse n_eq"])],
4.11 - {rew_ord'="tless_true",
4.12 - rls'= e_rls, calc = [],
4.13 - srls = Rls {id="srls_partial_fraction",
4.14 - preconds = [],
4.15 - rew_ord = ("termlessI",termlessI),
4.16 - erls = append_rls "erls_in_srls_partial_fraction" e_rls
4.17 - [(*for asm in NTH_CONS ...*)
4.18 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.19 - (*2nd NTH_CONS pushes n+-1 into asms*)
4.20 - Calc("Groups.plus_class.plus", eval_binop "#add_")],
4.21 - srls = Erls, calc = [],
4.22 - rules = [
4.23 - Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
4.24 - Calc("Groups.plus_class.plus", eval_binop "#add_"),
4.25 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
4.26 - Calc("Tools.lhs", eval_lhs "eval_lhs_"),
4.27 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
4.28 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
4.29 - Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
4.30 - Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
4.31 - Calc("Partial_Fractions.factors_from_solution",
4.32 - eval_factors_from_solution "#factors_from_solution"),
4.33 - Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
4.34 - scr = EmptyScr},
4.35 - prls = e_rls, crls = e_rls, nrls = norm_Rational},
4.36 - "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
4.37 - "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
4.38 - " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.39 - " (X'_z::real) = lhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.40 - " (zzz::real) = argument_in X'_z; "^(* z *)
4.41 -
4.42 -(*--------------------------------------------------------------------
4.43 - " (pbz::real) = (SubProblem (Isac', "^(**)
4.44 - " [partial_fraction, rational, simplification], "^
4.45 - " [simplification, of_rationals, to_partial_fraction]) "^
4.46 - " [REAL X'_z, REAL zzz]); "^(**)
4.47 ---------------------------------------------------------------------*)
4.48 -
4.49 - " (num_orig::real) = get_numerator (rhs X'); "^(* num_orig = 3*)
4.50 - " X' = (Rewrite_Set norm_Rational False) X'; "^(*([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
4.51 -
4.52 - " (funterm::real) = rhs X'; "^(**)
4.53 - " (denom::real) = get_denominator funterm; "^(* denom = -1 + -2 * z + 8 * z ^^^ 2*)
4.54 - " (num::real) = get_numerator funterm; "^(**)
4.55 - " (equ::bool) = (denom = (0::real)); "^(* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*)
4.56 -
4.57 - " (L_L::bool list) = (SubProblem (PolyEq', "^(*([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
4.58 - " [abcFormula,degree_2,polynomial,univariate,equation], "^
4.59 - " [no_met]) "^
4.60 - " [BOOL equ, REAL zzz]); "^(*([3], Res), [z = 1 / 2, z = -1 / 4]*)
4.61 - " (facs::real) = factors_from_solution L_L; "^(**)
4.62 - " (eql::real) = Take (num_orig / facs); "^(*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))*)
4.63 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^(*([4], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
4.64 - " (eq::bool) = Take (eql = eqr); "^(*([5], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
4.65 - " eq = (Try (Rewrite_Set equival_trans False)) eq; "^(*([5], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
4.66 - " eq = drop_questionmarks eq; "^(**)
4.67 - " (z1::real) = (rhs (NTH 1 L_L)); "^(**)
4.68 - " (z2::real) = (rhs (NTH 2 L_L)); "^(**)
4.69 - " (eq_a::bool) = Take eq; "^(*([6], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
4.70 - " eq_a = (Substitute [zzz=z1]) eq; "^(*([6], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
4.71 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^(*([7], Res), 3 = 3 * A / 4*)
4.72 -
4.73 - " (sol_a::bool list) = (SubProblem (Isac', "^(*([8], Pbl), solve (3 = 3 * A / 4, A)*)
4.74 - " [univariate,equation],[no_met]) "^
4.75 - " [BOOL eq_a, REAL (A::real)]); "^(*([8], Res), [A = 4]*)
4.76 - " (a::real) = (rhs(NTH 1 sol_a)); "^(**)
4.77 - " (eq_b::bool) = Take eq; "^(*([9], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
4.78 - " eq_b = (Substitute [zzz=z2]) eq_b; "^(*([9], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)*)
4.79 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^(*([10], Res), 3 = -3 * B / 4)*)
4.80 - " (sol_b::bool list) = (SubProblem (Isac', "^(*([11], Pbl), solve (3 = -3 * B / 4, B)*)
4.81 - " [univariate,equation],[no_met]) "^
4.82 - " [BOOL eq_b, REAL (B::real)]); "^(*([11], Res), [B = -4]*)
4.83 - " (b::real) = (rhs(NTH 1 sol_b)); "^(**)
4.84 -
4.85 - " eqr = drop_questionmarks eqr; "^(**)
4.86 - " (pbz::real) = Take eqr; "^(*([12], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*)
4.87 - " pbz = ((Substitute [A=a, B=b]) pbz); "^(*([12], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
4.88 -
4.89 -(*--------------------------------------------------------------------
4.90 -THIS IS store_met + checked below
4.91 ---------------------------------------------------------------------*)
4.92 - " pbz = Rewrite ruleYZ False pbz; "^(*([13], Res), 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
4.93 - " pbz = drop_questionmarks pbz; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
4.94 - " (X_z::bool) = Take (X_z = pbz); "^(*([14], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
4.95 - " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;"^(*([14], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
4.96 - " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
4.97 - "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
4.98 - ));
4.99 -
4.100 *}
4.101 ML {*
4.102 -get_met ["SignalProcessing", "Z_Transform", "Inverse_sub"];
4.103 *}
4.104 ML {*
4.105 *}
4.106 ML {* (*==================*)
4.107 -"----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
4.108 -states:= [];
4.109 -val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
4.110 - "stepResponse (x[n::real]::bool)"];
4.111 -val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
4.112 - ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
4.113 -CalcTree [(fmz, (dI, pI, mI))];
4.114 -Iterator 1;
4.115 -moveActiveRoot 1;
4.116 -autoCalculate 1 CompleteCalc;
4.117 -
4.118 -*}
4.119 -ML {*
4.120 -val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
4.121 -val (Form f, tac, asms) = pt_extract (pt, p);
4.122 -if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
4.123 - andalso p = ([], Res) then ()
4.124 - else error "inv Z, exp 1 autoCalculate changed";
4.125 -
4.126 -*}
4.127 -ML {*
4.128 -*}
4.129 -ML {* (*==================*)
4.130 -"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
4.131 -val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
4.132 - "stepResponse (x[n::real]::bool)"];
4.133 -val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
4.134 - ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
4.135 -val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
4.136 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
4.137 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *)
4.138 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
4.139 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
4.140 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
4.141 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method *)
4.142 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
4.143 - (*([1], Frm)*)
4.144 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
4.145 - (*([1], Res)*)
4.146 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Subproblem --- why NOT solve ?!?*)
4.147 - f2str fb = "?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
4.148 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res)Model_Problem*)
4.149 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
4.150 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
4.151 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions z_i"*)
4.152 -*}
4.153 -ML {*
4.154 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory ?!? Empty_Tac
4.155 - ..., Given = [Correct "equality (get_denominator (24 / (-1 + -2 * z + 8 * z ^^^ 2)) = 0)"
4.156 - ^^^^^^^^^^^^^^^ why not evaluated ?*)
4.157 -*}
4.158 -ML {*
4.159 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
4.160 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
4.161 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method*)
4.162 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0";
4.163 - (*([3, 1], Frm)*)
4.164 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / "^
4.165 - "(2 * 8) |\nz = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)";
4.166 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = 1 / 2 | z = -1 / 4";
4.167 - (*([3, 2], Res)*)
4.168 -if f2str fb = "z = 1 / 2 | z = -1 / 4" andalso p = ([3, 2], Res)
4.169 - then () else error "begin of 'inv Z', exp 1 me changed";
4.170 -show_pt pt;
4.171 -(*[
4.172 -(([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
4.173 -(([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
4.174 -(([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
4.175 -(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
4.176 -(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
4.177 -(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)]
4.178 -(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
4.179 - z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
4.180 -(([3,2], Res), z = 1 / 2 | z = -1 / 4)] *)
4.181 -
4.182 -*}
4.183 -ML {* (*==================*)
4.184 -*}
4.185 -ML {*
4.186 *}
4.187 ML {*
4.188 *}