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