52 [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])), |
49 [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])), |
53 (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID |
50 (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID |
54 (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])), |
51 (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])), |
55 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID |
52 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID |
56 (["Inverse", "Z_Transform", "SignalProcessing"], |
53 (["Inverse", "Z_Transform", "SignalProcessing"], |
57 (*^ capital letter breaks coding standard |
|
58 because "inverse" = Const ("Rings.inverse_class.inverse", ..*) |
|
59 [("#Given" ,["filterExpression (X_eq::bool)"]), |
|
60 ("#Find" ,["stepResponse (n_eq::bool)"])], |
|
61 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, |
|
62 [["SignalProcessing","Z_Transform","Inverse"]])), |
|
63 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID |
|
64 (["Inverse", "Z_Transform", "SignalProcessing"], |
|
65 [("#Given" ,["filterExpression X_eq"]), |
54 [("#Given" ,["filterExpression X_eq"]), |
66 ("#Find" ,["stepResponse n_eq"])], |
55 ("#Find" ,["stepResponse n_eq"])], |
67 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, |
56 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, |
68 [["SignalProcessing","Z_Transform","Inverse"]]))]\<close> |
57 [["SignalProcessing","Z_Transform","Inverse"]])), |
|
58 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID |
|
59 (["Inverse_sub", "Z_Transform", "SignalProcessing"], |
|
60 [("#Given" ,["filterExpression X_eq"]), |
|
61 ("#Find" ,["stepResponse n_eq"])], |
|
62 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, |
|
63 [["SignalProcessing","Z_Transform","Inverse_sub"]]))]\<close> |
69 |
64 |
70 subsection \<open>Define Name and Signature for the Method\<close> |
65 subsection \<open>Define Name and Signature for the Method\<close> |
71 consts |
66 consts |
72 InverseZTransform :: "[bool, bool] => bool" |
67 InverseZTransform1 :: "[bool, bool] => bool" |
73 ("((Script InverseZTransform (_ =))// (_))" 9) |
68 ("((Script InverseZTransform1 (_ =))// (_))" 9) |
|
69 InverseZTransform2 :: "[bool, real, bool] => bool" |
|
70 ("((Script InverseZTransform2 (_ _ =))// (_))" 9) |
74 |
71 |
75 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close> |
72 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close> |
76 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close> |
73 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close> |
77 setup \<open>KEStore_Elems.add_mets |
74 setup \<open>KEStore_Elems.add_mets |
78 [Specify.prep_met thy "met_SP" [] Celem.e_metID |
75 [Specify.prep_met thy "met_SP" [] Celem.e_metID |
100 [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG --> as arg\<close> |
97 [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG --> as arg\<close> |
101 in X) " |
98 in X) " |
102 *) |
99 *) |
103 setup \<open>KEStore_Elems.add_mets |
100 setup \<open>KEStore_Elems.add_mets |
104 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID |
101 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID |
105 (["SignalProcessing", "Z_Transform", "Inverse"], |
102 (["SignalProcessing", "Z_Transform", "Inverse"], |
106 [("#Given" ,["filterExpression (X_eq::bool)"]), |
103 [("#Given" ,["filterExpression (X_eq::bool)"]), |
107 ("#Find" ,["stepResponse (n_eq::bool)"])], |
104 ("#Find" ,["stepResponse (n_eq::bool)"])], |
108 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
105 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
109 errpats = [], nrls = Rule.e_rls}, |
106 errpats = [], nrls = Rule.e_rls}, |
110 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
107 "Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
111 " (let X = Take X_eq;" ^ |
108 " (let X = Take X_eq;" ^ |
112 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) |
109 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) |
113 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) |
110 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) |
114 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
111 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
115 " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) |
112 " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) |
121 " [''LINEAR'',''univariate'',''equation'',''test'']," ^ |
118 " [''LINEAR'',''univariate'',''equation'',''test'']," ^ |
122 " [''Test'',''solve_linear'']) " ^ |
119 " [''Test'',''solve_linear'']) " ^ |
123 " [BOOL equ, REAL z]) " ^ |
120 " [BOOL equ, REAL z]) " ^ |
124 " in X)")] |
121 " in X)")] |
125 \<close> |
122 \<close> |
126 (* |
123 |
127 Type unification failed: Clash of types "bool" and "_ itself" |
124 (* ok |
128 Type error in application: incompatible operand type |
125 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool" |
129 Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b |
|
130 Operand: |
|
131 \<lambda>X. let X' = Rewrite ''ruleZY'' ... |
|
132 : |
|
133 :partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> bool" |
|
134 where |
126 where |
135 "inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close> |
127 "inverse_ztransform2 X_eq X_z = |
136 (let X = Take X_eq; |
128 (let X = Take X_eq; |
137 X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close> |
129 X' = Rewrite ''ruleZY'' False X; |
138 (num_orig::real) = get_numerator (rhs X'); |
130 X'_z = lhs X'; |
139 X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close> |
131 zzz = argument_in X'_z; |
140 (X'_z::real) = lhs X'; |
132 funterm = rhs X'; |
141 (zzz::real) = argument_in X'_z; |
133 pbz = SubProblem (''Isac'', |
142 (funterm::real) = rhs X'; \<comment> \<open>drop X' z = for equation solving\<close> |
134 [''partial_fraction'',''rational'',''simplification''], |
143 (denom::real) = get_denominator funterm; \<comment> \<open>get_denominator\<close> |
135 [''simplification'',''of_rationals'',''to_partial_fraction'']) |
144 (num::real) = get_numerator funterm; \<comment> \<open>get_numerator\<close> |
136 [REAL funterm, REAL zzz]; |
145 (equ::bool) = (denom = (0::real)); |
137 pbz_eq = Take (X'_z = pbz); |
146 (L_L::bool list) = (SubProblem (''Partial_Fractions'', |
138 pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; |
147 [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], |
139 X_zeq = Take (X_z = rhs pbz_eq); |
148 [''no_met'']) |
140 n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq |
149 [BOOL equ, REAL zzz]); |
141 in n_eq)" |
150 (facs::real) = factors_from_solution L_L; |
|
151 (eql::real) = Take (num_orig / facs); \<comment> \<open>---\<close> |
|
152 (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \<comment> \<open>---\<close> |
|
153 (eq::bool) = Take (eql = eqr); \<comment> \<open>Maybe possible to use HOLogic.mk_eq ??\<close> |
|
154 eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \<comment> \<open>---\<close> |
|
155 (z1::real) = (rhs (NTH 1 L_L)); \<comment> \<open>prepare equation for a - eq_a therefor substitute z with solution 1 - z1\<close> |
|
156 (z2::real) = (rhs (NTH 2 L_L)); \<comment> \<open>---\<close> |
|
157 (eq_a::bool) = Take eq; |
|
158 eq_a = (Substitute [zzz=z1]) eq; |
|
159 eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; |
|
160 (sol_a::bool list) = |
|
161 (SubProblem (''Isac'', |
|
162 [''univariate'',''equation''],[''no_met'']) |
|
163 [BOOL eq_a, REAL (A::real)]); |
|
164 (a::real) = (rhs(NTH 1 sol_a)); \<comment> \<open>---\<close> |
|
165 (eq_b::bool) = Take eq; |
|
166 eq_b = (Substitute [zzz=z2]) eq_b; |
|
167 eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; |
|
168 (sol_b::bool list) = |
|
169 (SubProblem (''Isac'', |
|
170 [''univariate'',''equation''],[''no_met'']) |
|
171 [BOOL eq_b, REAL (B::real)]); |
|
172 (b::real) = (rhs(NTH 1 sol_b)); \<comment> \<open>---\<close> |
|
173 (pbz::real) = Take eqr; |
|
174 pbz = ((Substitute [A=a, B=b]) pbz); \<comment> \<open>---\<close> |
|
175 pbz = Rewrite ''ruleYZ'' False pbz; |
|
176 (X_z::bool) = Take (X_z = pbz); |
|
177 (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z |
|
178 in n_eq)" |
|
179 *) |
|
180 setup \<open>KEStore_Elems.add_mets |
|
181 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID |
|
182 (["SignalProcessing", "Z_Transform", "Inverse"], |
|
183 [("#Given" ,["filterExpression X_eq"]), |
|
184 ("#Find" ,["stepResponse n_eq"])], |
|
185 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls, |
|
186 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, |
|
187 "Script InverseZTransform (X_eq::bool) = "^ |
|
188 (*(1/z) instead of z ^^^ -1*) |
|
189 "(let X = Take X_eq; "^ |
|
190 " X' = Rewrite ''ruleZY'' False X; "^ |
|
191 (*z * denominator*) |
|
192 " (num_orig::real) = get_numerator (rhs X'); "^ |
|
193 " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^ |
|
194 (*simplify*) |
|
195 " (X'_z::real) = lhs X'; "^ |
|
196 " (zzz::real) = argument_in X'_z; "^ |
|
197 " (funterm::real) = rhs X'; "^ |
|
198 (*drop X' z = for equation solving*) |
|
199 " (denom::real) = get_denominator funterm; "^ |
|
200 (*get_denominator*) |
|
201 " (num::real) = get_numerator funterm; "^ |
|
202 (*get_numerator*) |
|
203 " (equ::bool) = (denom = (0::real)); "^ |
|
204 " (L_L::bool list) = (SubProblem (''Partial_Fractions'', "^ |
|
205 " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^ |
|
206 " [''no_met'']) "^ |
|
207 " [BOOL equ, REAL zzz]); "^ |
|
208 " (facs::real) = factors_from_solution L_L; "^ |
|
209 " (eql::real) = Take (num_orig / facs); "^ |
|
210 |
|
211 " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; "^ |
|
212 |
|
213 " (eq::bool) = Take (eql = eqr); "^ |
|
214 (*Maybe possible to use HOLogic.mk_eq ??*) |
|
215 " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^ |
|
216 |
|
217 " (z1::real) = (rhs (NTH 1 L_L)); "^ |
|
218 (* |
|
219 * prepare equation for a - eq_a |
|
220 * therefor substitute z with solution 1 - z1 |
|
221 *) |
|
222 " (z2::real) = (rhs (NTH 2 L_L)); "^ |
|
223 |
|
224 " (eq_a::bool) = Take eq; "^ |
|
225 " eq_a = (Substitute [zzz=z1]) eq; "^ |
|
226 " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; "^ |
|
227 " (sol_a::bool list) = "^ |
|
228 " (SubProblem (''Isac'', "^ |
|
229 " [''univariate'',''equation''],[''no_met'']) "^ |
|
230 " [BOOL eq_a, REAL (A::real)]); "^ |
|
231 " (a::real) = (rhs(NTH 1 sol_a)); "^ |
|
232 |
|
233 " (eq_b::bool) = Take eq; "^ |
|
234 " eq_b = (Substitute [zzz=z2]) eq_b; "^ |
|
235 " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^ |
|
236 " (sol_b::bool list) = "^ |
|
237 " (SubProblem (''Isac'', "^ |
|
238 " [''univariate'',''equation''],[''no_met'']) "^ |
|
239 " [BOOL eq_b, REAL (B::real)]); "^ |
|
240 " (b::real) = (rhs(NTH 1 sol_b)); "^ |
|
241 |
|
242 " (pbz::real) = Take eqr; "^ |
|
243 " pbz = ((Substitute [A=a, B=b]) pbz); "^ |
|
244 |
|
245 " pbz = Rewrite ''ruleYZ'' False pbz; "^ |
|
246 |
|
247 " (X_z::bool) = Take (X_z = pbz); "^ |
|
248 " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z "^ |
|
249 "in n_eq)")] |
|
250 \<close> |
|
251 (* same error as in inverse_ztransform2 |
|
252 :partial_function (tailrec) inverse_ztransform3 :: "bool \<Rightarrow> bool" |
|
253 where |
|
254 "inverse_ztransform X_eq = |
|
255 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
|
256 (let X = Take X_eq; |
|
257 (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
|
258 X' = Rewrite ''ruleZY'' False X; |
|
259 (* ?X' z*) |
|
260 (X'_z::real) = lhs X'; |
|
261 (* z *) |
|
262 (zzz::real) = argument_in X'_z; |
|
263 (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
|
264 (funterm::real) = rhs X'; |
|
265 (*-----*) |
|
266 (pbz::real) = (SubProblem (''Isac'', |
|
267 [''partial_fraction'',''rational'',''simplification''], |
|
268 [''simplification'',''of_rationals'',''to_partial_fraction'']) |
|
269 (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
270 [REAL funterm, REAL zzz]); |
|
271 (*-----*) |
|
272 (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
273 (pbz_eq::bool) = Take (X'_z = pbz); |
|
274 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
|
275 pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; |
|
276 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
277 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
278 (X_zeq::bool) = Take (X_z = rhs pbz_eq); |
|
279 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) |
|
280 n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq |
|
281 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
282 in n_eq) " |
|
283 *) |
142 *) |
284 setup \<open>KEStore_Elems.add_mets |
143 setup \<open>KEStore_Elems.add_mets |
285 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID |
144 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID |
286 (["SignalProcessing", "Z_Transform", "Inverse_sub"], |
145 (["SignalProcessing", "Z_Transform", "Inverse_sub"], |
287 [("#Given" ,["filterExpression X_eq"]), |
146 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]), |
288 ("#Find" ,["stepResponse n_eq"])], |
147 ("#Find" ,["stepResponse n_eq"])], |
289 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], |
148 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], |
290 srls = Rule.Rls {id="srls_partial_fraction", |
149 srls = Rule.Rls {id="srls_partial_fraction", |
291 preconds = [], rew_ord = ("termlessI",termlessI), |
150 preconds = [], rew_ord = ("termlessI",termlessI), |
292 erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls |
151 erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls |
305 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
164 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
306 Rule.Calc ("Partial_Fractions.factors_from_solution", |
165 Rule.Calc ("Partial_Fractions.factors_from_solution", |
307 eval_factors_from_solution "#factors_from_solution") |
166 eval_factors_from_solution "#factors_from_solution") |
308 ], scr = Rule.EmptyScr}, |
167 ], scr = Rule.EmptyScr}, |
309 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, |
168 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, |
310 (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
169 " Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
311 "Script InverseZTransform (X_eq::bool) = "^ |
170 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
312 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
171 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
313 "(let X = Take X_eq; "^ |
172 " (X'_z::real) = lhs X'; "^ (* ?X' z*) |
314 (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
173 " (zzz::real) = argument_in X'_z; "^ (* z *) |
315 " X' = Rewrite ''ruleZY'' False X; "^ |
174 " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
316 (* ?X' z*) |
175 " (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
317 " (X'_z::real) = lhs X'; "^ |
176 " [''partial_fraction'',''rational'',''simplification''], "^ |
318 (* z *) |
177 " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^ |
319 " (zzz::real) = argument_in X'_z; "^ |
178 " [REAL funterm, REAL zzz]); "^ |
320 (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
179 " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
321 " (funterm::real) = rhs X'; "^ |
180 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
322 |
181 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
323 " (pbz::real) = (SubProblem (''Isac'', "^ |
182 " 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]*) |
324 " [''partial_fraction'',''rational'',''simplification''], "^ |
183 " in n_eq) ")](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
325 " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^ |
|
326 (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
327 " [REAL funterm, REAL zzz]); "^ |
|
328 |
|
329 (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
330 " (pbz_eq::bool) = Take (X'_z = pbz); "^ |
|
331 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
|
332 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ |
|
333 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
334 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
|
335 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ |
|
336 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) |
|
337 " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ |
|
338 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
339 (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
|
340 "in n_eq)")] |
|
341 \<close> |
184 \<close> |
342 |
185 |
343 end |
186 end |
344 |
187 |