1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri May 11 14:48:27 2012 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon May 14 14:47:45 2012 +0200
1.3 @@ -247,13 +247,14 @@
1.4 " (pbz::real) = (SubProblem (Isac', "^(**)
1.5 " [partial_fraction,rational,simplification], "^
1.6 " [simplification,of_rationals,to_partial_fraction]) "^
1.7 - " [REAL funterm, REAL zzz]); "^(**)
1.8 + " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.9
1.10 - " pbz = Rewrite ruleYZ False pbz; "^(*([13], Res), 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.11 - " pbz = drop_questionmarks pbz; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.12 - " (X_z::bool) = Take (X_z = pbz); "^(*([14], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.13 - " (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.14 - " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.15 + " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.16 + " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.17 + " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.18 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.19 + " 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.20 + " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.21 "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.22 ));
1.23
2.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Fri May 11 14:48:27 2012 +0200
2.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon May 14 14:47:45 2012 +0200
2.3 @@ -9,6 +9,7 @@
2.4 "table of contents -----------------------------------------------";
2.5 "-----------------------------------------------------------------";
2.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
2.7 +"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
2.8 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
2.9 "----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
2.10 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
2.11 @@ -22,6 +23,33 @@
2.12 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
2.13 get_met ["SignalProcessing","Z_Transform","Inverse"];
2.14
2.15 +"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
2.16 +"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
2.17 +"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
2.18 +val str =
2.19 +"Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
2.20 + "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
2.21 + " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
2.22 + " (X'_z::real) = lhs X'; "^(* ?X' z*)
2.23 + " (zzz::real) = argument_in X'_z; "^(* z *)
2.24 + " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
2.25 +
2.26 + " (pbz::real) = (SubProblem (Isac', "^(**)
2.27 + " [partial_fraction,rational,simplification], "^
2.28 + " [simplification,of_rationals,to_partial_fraction]) "^
2.29 + " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
2.30 +
2.31 + " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
2.32 + " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
2.33 + " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
2.34 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
2.35 + " 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]*)
2.36 + " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
2.37 + "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
2.38 +;
2.39 +val sc = ((inst_abs thy) o term_of o the o (parse @{theory Isac})) str;
2.40 +writeln (term2str sc);
2.41 +
2.42 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
2.43 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
2.44 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
2.45 @@ -79,7 +107,7 @@
2.46 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
2.47 "stepResponse (x[n::real]::bool)"];
2.48 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
2.49 - ["SignalProcessing", "Z_Transform", "Inverse"]);
2.50 + ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
2.51 CalcTree [(fmz, (dI,pI,mI))];
2.52 Iterator 1;
2.53 moveActiveRoot 1;