1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Apr 09 11:38:26 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 08 18:45:25 2019 +0200
1.3 @@ -1,8 +1,6 @@
1.4 (* Title: Test_Z_Transform
1.5 Author: Jan Rocnik
1.6 (c) copyright due to lincense terms.
1.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 - 10 20 30 40 50 60 70 80
1.9 *)
1.10
1.11 theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
1.12 @@ -27,7 +25,6 @@
1.13 filterExpression :: "bool => una"
1.14 stepResponse :: "bool => una"
1.15
1.16 -
1.17 ML \<open>
1.18 val inverse_z = prep_rls'(
1.19 Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
1.20 @@ -54,23 +51,23 @@
1.21 (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
1.22 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.23 (["Inverse", "Z_Transform", "SignalProcessing"],
1.24 - (*^ capital letter breaks coding standard
1.25 - because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
1.26 - [("#Given" ,["filterExpression (X_eq::bool)"]),
1.27 - ("#Find" ,["stepResponse (n_eq::bool)"])],
1.28 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.29 - [["SignalProcessing","Z_Transform","Inverse"]])),
1.30 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.31 - (["Inverse", "Z_Transform", "SignalProcessing"],
1.32 [("#Given" ,["filterExpression X_eq"]),
1.33 ("#Find" ,["stepResponse n_eq"])],
1.34 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.35 - [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
1.36 + [["SignalProcessing","Z_Transform","Inverse"]])),
1.37 + (Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID
1.38 + (["Inverse_sub", "Z_Transform", "SignalProcessing"],
1.39 + [("#Given" ,["filterExpression X_eq"]),
1.40 + ("#Find" ,["stepResponse n_eq"])],
1.41 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.42 + [["SignalProcessing","Z_Transform","Inverse_sub"]]))]\<close>
1.43
1.44 subsection \<open>Define Name and Signature for the Method\<close>
1.45 consts
1.46 - InverseZTransform :: "[bool, bool] => bool"
1.47 - ("((Script InverseZTransform (_ =))// (_))" 9)
1.48 + InverseZTransform1 :: "[bool, bool] => bool"
1.49 + ("((Script InverseZTransform1 (_ =))// (_))" 9)
1.50 + InverseZTransform2 :: "[bool, real, bool] => bool"
1.51 + ("((Script InverseZTransform2 (_ _ =))// (_))" 9)
1.52
1.53 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
1.54 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
1.55 @@ -102,12 +99,12 @@
1.56 *)
1.57 setup \<open>KEStore_Elems.add_mets
1.58 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.59 - (["SignalProcessing", "Z_Transform", "Inverse"],
1.60 + (["SignalProcessing", "Z_Transform", "Inverse"],
1.61 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.62 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.63 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.64 errpats = [], nrls = Rule.e_rls},
1.65 - "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.66 + "Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.67 " (let X = Take X_eq;" ^
1.68 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
1.69 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
1.70 @@ -123,168 +120,30 @@
1.71 " [BOOL equ, REAL z]) " ^
1.72 " in X)")]
1.73 \<close>
1.74 -(*
1.75 -Type unification failed: Clash of types "bool" and "_ itself"
1.76 -Type error in application: incompatible operand type
1.77 -Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b
1.78 -Operand:
1.79 - \<lambda>X. let X' = Rewrite ''ruleZY'' ...
1.80 -:
1.81 -:partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> bool"
1.82 +
1.83 +(* ok
1.84 +partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.85 where
1.86 -"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
1.87 +"inverse_ztransform2 X_eq X_z =
1.88 (let X = Take X_eq;
1.89 - X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
1.90 - (num_orig::real) = get_numerator (rhs X');
1.91 - X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
1.92 - (X'_z::real) = lhs X';
1.93 - (zzz::real) = argument_in X'_z;
1.94 - (funterm::real) = rhs X'; \<comment> \<open>drop X' z = for equation solving\<close>
1.95 - (denom::real) = get_denominator funterm; \<comment> \<open>get_denominator\<close>
1.96 - (num::real) = get_numerator funterm; \<comment> \<open>get_numerator\<close>
1.97 - (equ::bool) = (denom = (0::real));
1.98 - (L_L::bool list) = (SubProblem (''Partial_Fractions'',
1.99 - [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''],
1.100 - [''no_met''])
1.101 - [BOOL equ, REAL zzz]);
1.102 - (facs::real) = factors_from_solution L_L;
1.103 - (eql::real) = Take (num_orig / facs); \<comment> \<open>---\<close>
1.104 - (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \<comment> \<open>---\<close>
1.105 - (eq::bool) = Take (eql = eqr); \<comment> \<open>Maybe possible to use HOLogic.mk_eq ??\<close>
1.106 - eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \<comment> \<open>---\<close>
1.107 - (z1::real) = (rhs (NTH 1 L_L)); \<comment> \<open>prepare equation for a - eq_a therefor substitute z with solution 1 - z1\<close>
1.108 - (z2::real) = (rhs (NTH 2 L_L)); \<comment> \<open>---\<close>
1.109 - (eq_a::bool) = Take eq;
1.110 - eq_a = (Substitute [zzz=z1]) eq;
1.111 - eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
1.112 - (sol_a::bool list) =
1.113 - (SubProblem (''Isac'',
1.114 - [''univariate'',''equation''],[''no_met''])
1.115 - [BOOL eq_a, REAL (A::real)]);
1.116 - (a::real) = (rhs(NTH 1 sol_a)); \<comment> \<open>---\<close>
1.117 - (eq_b::bool) = Take eq;
1.118 - eq_b = (Substitute [zzz=z2]) eq_b;
1.119 - eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b;
1.120 - (sol_b::bool list) =
1.121 - (SubProblem (''Isac'',
1.122 - [''univariate'',''equation''],[''no_met''])
1.123 - [BOOL eq_b, REAL (B::real)]);
1.124 - (b::real) = (rhs(NTH 1 sol_b)); \<comment> \<open>---\<close>
1.125 - (pbz::real) = Take eqr;
1.126 - pbz = ((Substitute [A=a, B=b]) pbz); \<comment> \<open>---\<close>
1.127 - pbz = Rewrite ''ruleYZ'' False pbz;
1.128 - (X_z::bool) = Take (X_z = pbz);
1.129 - (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z
1.130 -in n_eq)"
1.131 -*)
1.132 -setup \<open>KEStore_Elems.add_mets
1.133 - [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.134 - (["SignalProcessing", "Z_Transform", "Inverse"],
1.135 - [("#Given" ,["filterExpression X_eq"]),
1.136 - ("#Find" ,["stepResponse n_eq"])],
1.137 - {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls,
1.138 - crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
1.139 - "Script InverseZTransform (X_eq::bool) = "^
1.140 - (*(1/z) instead of z ^^^ -1*)
1.141 - "(let X = Take X_eq; "^
1.142 - " X' = Rewrite ''ruleZY'' False X; "^
1.143 - (*z * denominator*)
1.144 - " (num_orig::real) = get_numerator (rhs X'); "^
1.145 - " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^
1.146 - (*simplify*)
1.147 - " (X'_z::real) = lhs X'; "^
1.148 - " (zzz::real) = argument_in X'_z; "^
1.149 - " (funterm::real) = rhs X'; "^
1.150 - (*drop X' z = for equation solving*)
1.151 - " (denom::real) = get_denominator funterm; "^
1.152 - (*get_denominator*)
1.153 - " (num::real) = get_numerator funterm; "^
1.154 - (*get_numerator*)
1.155 - " (equ::bool) = (denom = (0::real)); "^
1.156 - " (L_L::bool list) = (SubProblem (''Partial_Fractions'', "^
1.157 - " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^
1.158 - " [''no_met'']) "^
1.159 - " [BOOL equ, REAL zzz]); "^
1.160 - " (facs::real) = factors_from_solution L_L; "^
1.161 - " (eql::real) = Take (num_orig / facs); "^
1.162 -
1.163 - " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; "^
1.164 -
1.165 - " (eq::bool) = Take (eql = eqr); "^
1.166 - (*Maybe possible to use HOLogic.mk_eq ??*)
1.167 - " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^
1.168 -
1.169 - " (z1::real) = (rhs (NTH 1 L_L)); "^
1.170 - (*
1.171 - * prepare equation for a - eq_a
1.172 - * therefor substitute z with solution 1 - z1
1.173 - *)
1.174 - " (z2::real) = (rhs (NTH 2 L_L)); "^
1.175 -
1.176 - " (eq_a::bool) = Take eq; "^
1.177 - " eq_a = (Substitute [zzz=z1]) eq; "^
1.178 - " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; "^
1.179 - " (sol_a::bool list) = "^
1.180 - " (SubProblem (''Isac'', "^
1.181 - " [''univariate'',''equation''],[''no_met'']) "^
1.182 - " [BOOL eq_a, REAL (A::real)]); "^
1.183 - " (a::real) = (rhs(NTH 1 sol_a)); "^
1.184 -
1.185 - " (eq_b::bool) = Take eq; "^
1.186 - " eq_b = (Substitute [zzz=z2]) eq_b; "^
1.187 - " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^
1.188 - " (sol_b::bool list) = "^
1.189 - " (SubProblem (''Isac'', "^
1.190 - " [''univariate'',''equation''],[''no_met'']) "^
1.191 - " [BOOL eq_b, REAL (B::real)]); "^
1.192 - " (b::real) = (rhs(NTH 1 sol_b)); "^
1.193 -
1.194 - " (pbz::real) = Take eqr; "^
1.195 - " pbz = ((Substitute [A=a, B=b]) pbz); "^
1.196 -
1.197 - " pbz = Rewrite ''ruleYZ'' False pbz; "^
1.198 -
1.199 - " (X_z::bool) = Take (X_z = pbz); "^
1.200 - " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z "^
1.201 - "in n_eq)")]
1.202 -\<close>
1.203 -(* same error as in inverse_ztransform2
1.204 -:partial_function (tailrec) inverse_ztransform3 :: "bool \<Rightarrow> bool"
1.205 - where
1.206 -"inverse_ztransform X_eq =
1.207 -(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.208 -(let X = Take X_eq;
1.209 -(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.210 - X' = Rewrite ''ruleZY'' False X;
1.211 -(* ?X' z*)
1.212 - (X'_z::real) = lhs X';
1.213 -(* z *)
1.214 - (zzz::real) = argument_in X'_z;
1.215 -(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.216 - (funterm::real) = rhs X';
1.217 -(*-----*)
1.218 - (pbz::real) = (SubProblem (''Isac'',
1.219 - [''partial_fraction'',''rational'',''simplification''],
1.220 - [''simplification'',''of_rationals'',''to_partial_fraction''])
1.221 -(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.222 - [REAL funterm, REAL zzz]);
1.223 -(*-----*)
1.224 -(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.225 - (pbz_eq::bool) = Take (X'_z = pbz);
1.226 -(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.227 - pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
1.228 -(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.229 -(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.230 - (X_zeq::bool) = Take (X_z = rhs pbz_eq);
1.231 -(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.232 - n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
1.233 -(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.234 -in n_eq) "
1.235 + X' = Rewrite ''ruleZY'' False X;
1.236 + X'_z = lhs X';
1.237 + zzz = argument_in X'_z;
1.238 + funterm = rhs X';
1.239 + pbz = SubProblem (''Isac'',
1.240 + [''partial_fraction'',''rational'',''simplification''],
1.241 + [''simplification'',''of_rationals'',''to_partial_fraction''])
1.242 + [REAL funterm, REAL zzz];
1.243 + pbz_eq = Take (X'_z = pbz);
1.244 + pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
1.245 + X_zeq = Take (X_z = rhs pbz_eq);
1.246 + n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
1.247 + in n_eq)"
1.248 *)
1.249 setup \<open>KEStore_Elems.add_mets
1.250 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.251 - (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.252 - [("#Given" ,["filterExpression X_eq"]),
1.253 + (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.254 + [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
1.255 ("#Find" ,["stepResponse n_eq"])],
1.256 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
1.257 srls = Rule.Rls {id="srls_partial_fraction",
1.258 @@ -307,37 +166,21 @@
1.259 eval_factors_from_solution "#factors_from_solution")
1.260 ], scr = Rule.EmptyScr},
1.261 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
1.262 - (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.263 - "Script InverseZTransform (X_eq::bool) = "^
1.264 - (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.265 - "(let X = Take X_eq; "^
1.266 - (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.267 - " X' = Rewrite ''ruleZY'' False X; "^
1.268 - (* ?X' z*)
1.269 - " (X'_z::real) = lhs X'; "^
1.270 - (* z *)
1.271 - " (zzz::real) = argument_in X'_z; "^
1.272 - (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.273 - " (funterm::real) = rhs X'; "^
1.274 -
1.275 - " (pbz::real) = (SubProblem (''Isac'', "^
1.276 - " [''partial_fraction'',''rational'',''simplification''], "^
1.277 - " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
1.278 - (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.279 - " [REAL funterm, REAL zzz]); "^
1.280 -
1.281 - (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.282 - " (pbz_eq::bool) = Take (X'_z = pbz); "^
1.283 - (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.284 - " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^
1.285 - (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.286 - (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.287 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
1.288 - (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.289 - " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^
1.290 - (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.291 - (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.292 - "in n_eq)")]
1.293 + " Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.294 + " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.295 + " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.296 + " (X'_z::real) = lhs X'; "^ (* ?X' z*)
1.297 + " (zzz::real) = argument_in X'_z; "^ (* z *)
1.298 + " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.299 + " (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.300 + " [''partial_fraction'',''rational'',''simplification''], "^
1.301 + " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
1.302 + " [REAL funterm, REAL zzz]); "^
1.303 + " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.304 + " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.305 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.306 + " 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.307 + " in n_eq) ")](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.308 \<close>
1.309
1.310 end
2.1 --- a/src/Tools/isac/TODO.thy Tue Apr 09 11:38:26 2019 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Wed May 08 18:45:25 2019 +0200
2.3 @@ -17,9 +17,15 @@
2.4 \begin{itemize}
2.5 \item differentiateX --> differentiate after removal of script-constant
2.6 \end{itemize}
2.7 -\item Inverse_Z_Transform.thy: thm ruleZY introduces a new variable on the rhs of the rewrite-rule.
2.8 +\item Inverse_Z_Transform.thy:
2.9 + \begin{itemize}
2.10 + \item thm ruleZY introduces a new variable on the rhs of the rewrite-rule.
2.11 The problem is related to the decision of typing for "d_d" and making bound variables free (while
2.12 - shifting specific handling in equation solving etc. to the metalogic.
2.13 + shifting specific handling in equation solving etc. to the metalogic).
2.14 + \item Find "stepResponse (x[n::real]::bool)" not reflected in met ?!
2.15 + \item Reconsider whole problem:
2.16 + input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
2.17 + \end{itemize}
2.18 \item Test.thy: met_test_sqrt2: deleted?!
2.19 \item
2.20 \begin{itemize}
3.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Tue Apr 09 11:38:26 2019 +0200
3.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Wed May 08 18:45:25 2019 +0200
3.3 @@ -7,7 +7,6 @@
3.4 "table of contents -----------------------------------------------";
3.5 "-----------------------------------------------------------------";
3.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
3.7 -"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
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 @@ -21,47 +20,22 @@
3.12 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
3.13 get_met ["SignalProcessing","Z_Transform","Inverse"];
3.14
3.15 -"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.16 -"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.17 -"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.18 -val str =
3.19 -"Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
3.20 - "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
3.21 - " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
3.22 - " (X'_z::real) = lhs X'; "^(* ?X' z*)
3.23 - " (zzz::real) = argument_in X'_z; "^(* z *)
3.24 - " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
3.25 -
3.26 - " (pbz::real) = (SubProblem (IsacX, "^(**)
3.27 - " [partial_fraction,rational,simplification], "^
3.28 - " [simplification,of_rationals,to_partial_fraction]) "^
3.29 - " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
3.30 -
3.31 - " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
3.32 - " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
3.33 - " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
3.34 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
3.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]*)
3.36 - " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
3.37 - "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
3.38 -;
3.39 -val sc = (inst_abs o Thm.term_of o the o (parse @{theory Isac})) str;
3.40 -writeln (term2str sc);
3.41 -
3.42 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
3.43 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
3.44 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
3.45 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.46 + "boundVariable X_z" (*special case: formal arg. = actual arg.*),
3.47 "stepResponse (x[n::real]::bool)"];
3.48 -(*[], Frm*)val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.49 +(*[], Frm*)val (dI, pI, mI) = ("Isac", ["Inverse_sub", "Z_Transform", "SignalProcessing"],
3.50 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
3.51 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
3.52 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
3.53 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *)
3.54 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
3.55 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
3.56 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
3.57 -(*[], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Me["SignalProcessing","Z_Transform","Inverse_sub"]*)
3.58 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
3.59 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
3.60 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
3.61 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac"*)
3.62 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem ["Inverse_sub", "Z_Transform", "SignalProcessing"]*)
3.63 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse_sub"]*)
3.64 +(*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "boundVariable X_z"*)
3.65 +(*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Me["SignalProcessing","Z_Transform","Inverse_sub"]*)
3.66 (*[1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleZY", "Inverse_Z_Transform.ruleZY")*)
3.67 (*[1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["partial_fraction", "rational..*)
3.68 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
3.69 @@ -75,7 +49,7 @@
3.70
3.71 (*[2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.72 if p = ([2, 1], Frm) andalso f2str fb = "3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"
3.73 -then () else error "Z_Transform,Inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
3.74 +then () else error "Z_Transform,inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
3.75
3.76 (*[2, 1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
3.77 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.78 @@ -88,7 +62,7 @@
3.79 (*[2,2], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"*)
3.80 (*[2,2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.81 if p = ([2, 2, 1], Frm) andalso f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0"
3.82 -then () else error "Z_Transform,Inverse_sub] me 2";
3.83 +then () else error "Z_Transform,inverse_sub] me 2";
3.84
3.85 (*[2,2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.86 (*[2,2,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.87 @@ -102,7 +76,7 @@
3.88 (*[2,5], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*"Substitute ["z = 1 / 2"]*)
3.89 (*[2,5], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.90 if p = ([2, 5], Res) andalso f2str fb = "3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)"
3.91 -then () else error "Z_Transform,Inverse_sub] me 3"; (*Rewrite_Set "norm_Rational"*)
3.92 +then () else error "Z_Transform,inverse_sub] me 3"; (*Rewrite_Set "norm_Rational"*)
3.93
3.94 (*[2, 6], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem (Isac, ["normalise","polynomial","univariate","equation"]*)
3.95 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.96 @@ -117,7 +91,7 @@
3.97 (*[2,7,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.98 (*[2,7,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.99 if p = ([2, 7, 2], Res) andalso f2str fb = "3 / 1 + -3 / 4 * AA = 0"
3.100 -then () else error "Z_Transform,Inverse_sub] me 5";
3.101 +then () else error "Z_Transform,inverse_sub] me 5";
3.102
3.103 (*[2,7,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.104 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.105 @@ -130,7 +104,7 @@
3.106 (*[2,7,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
3.107 (*[2,7,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.108 if p = ([2, 7, 4, 1], Frm) andalso f2str fb = "3 + -3 / 4 * AA = 0"
3.109 -then () else error "Z_Transform,Inverse_sub] me 6";
3.110 +then () else error "Z_Transform,inverse_sub] me 6";
3.111
3.112 (*[2,7,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.113 (*[2,7,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.114 @@ -142,7 +116,7 @@
3.115 (*[2,8], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.116 (*[2,8], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.117 if p = ([2, 8], Res) andalso f2str fb = "3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)"
3.118 -then () else error "Z_Transform,Inverse_sub] me 7";
3.119 +then () else error "Z_Transform,inverse_sub] me 7";
3.120
3.121 (*[2,9], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.122 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.123 @@ -155,12 +129,12 @@
3.124 (*[2,10], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
3.125 (*[2,10,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.126 if p = ([2, 10, 1], Frm) andalso f2str fb = "3 = -3 * BB / 4"
3.127 -then () else error "Z_Transform,Inverse_sub] me 8";
3.128 +then () else error "Z_Transform,inverse_sub] me 8";
3.129
3.130 (*[2,10,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.131 (*[2,10,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.132 if p = ([2, 10, 2], Res) andalso f2str fb = "3 / 1 + 3 / 4 * BB = 0"
3.133 -then () else error "Z_Transform,Inverse_sub] me 9";
3.134 +then () else error "Z_Transform,inverse_sub] me 9";
3.135
3.136 (*[2,10,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.137 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.138 @@ -174,7 +148,7 @@
3.139 (*[2,10,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
3.140 (*[2,10,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.141 if p = ([2, 10, 4, 1], Frm) andalso f2str fb = "3 + 3 / 4 * BB = 0"
3.142 -then () else error "Z_Transform,Inverse_sub] me 10";
3.143 +then () else error "Z_Transform,inverse_sub] me 10";
3.144
3.145 (*[2,10,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.146 (*[2,10,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.147 @@ -337,6 +311,7 @@
3.148 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
3.149 reset_states ();
3.150 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.151 + "boundVariable X_z" (*special case: formal arg. = actual arg.*),
3.152 "stepResponse (x[n::real]::bool)"];
3.153 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.154 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
3.155 @@ -356,6 +331,7 @@
3.156 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
3.157 reset_states ();
3.158 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.159 + "boundVariable X_z" (*special case: formal arg. = actual arg.*),
3.160 "stepResponse (x[n::real]::bool)"];
3.161 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.162 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);