funpack: rename xxx' to xxxX preparing ''xxxX'' (''xxx''' not accepted by funpack)
1 (* Title: Knowledge/Inverse_Z_Transform/inverse_z_transform.sml
3 (c) copyright due to lincense terms.
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 "-----------------------------------------------------------------";
9 "table of contents -----------------------------------------------";
10 "-----------------------------------------------------------------";
11 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
12 "----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
13 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
14 "----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
15 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
16 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
20 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
21 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
22 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
23 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
24 get_met ["SignalProcessing","Z_Transform","Inverse"];
26 "----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
27 "----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
28 "----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
30 "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
31 "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
32 " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
33 " (X'_z::real) = lhs X'; "^(* ?X' z*)
34 " (zzz::real) = argument_in X'_z; "^(* z *)
35 " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
37 " (pbz::real) = (SubProblem (IsacX, "^(**)
38 " [partial_fraction,rational,simplification], "^
39 " [simplification,of_rationals,to_partial_fraction]) "^
40 " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
42 " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
43 " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
44 " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
45 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
46 " 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]*)
47 " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
48 "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
50 val sc = (inst_abs o Thm.term_of o the o (parse @{theory Isac})) str;
51 writeln (term2str sc);
53 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
54 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
55 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
56 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
57 "stepResponse (x[n::real]::bool)"];
58 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
59 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
60 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
61 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
62 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *)
63 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
64 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
65 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
66 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Me["SignalProcessing","Z_Transform","Inverse_sub"]*)
67 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleZY", "Inverse_Z_Transform.ruleZY")*)
68 (*([1], Frm)*)f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
69 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["partial_fraction", "rational..*)
70 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
71 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "functionTerm (X' z)"*)
72 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
73 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "decomposedFunction p_p'''"*)
74 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory*)
75 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
76 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
77 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method
78 ["simplification", "of_rationals", "to_partial_fraction"]*)
79 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "norm_Rational"*)
80 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
81 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
82 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
83 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
84 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
85 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
86 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
87 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
88 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"*)
89 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
90 if f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0"andalso p = ([2, 2, 1], Frm)
91 then () else error "begin of 'inv Z', exp 1 me changed";
93 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
94 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
95 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
96 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond", ...*)
97 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
98 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
99 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
100 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
101 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
102 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*"Substitute*)
103 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
104 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
105 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
106 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
107 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
108 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
109 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
110 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
111 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
112 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
113 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
114 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
115 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
116 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
117 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
118 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
119 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
120 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
121 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
122 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
123 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
124 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
125 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
126 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
127 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
128 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
129 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
130 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond *)
131 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond *)
132 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
133 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
134 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
135 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
136 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
137 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
138 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
139 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
140 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
141 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
142 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
143 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
144 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
145 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
146 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
147 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
148 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
149 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
150 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
151 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
152 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
153 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
154 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
155 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
156 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
157 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
158 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
159 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
160 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
161 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond*)
162 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond*)
163 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
164 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
165 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2, 11], Res) Check_Postcond*)
166 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Take*)
167 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Frm) Rewrite*)
168 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res) Take*)
169 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set*)
170 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond*)
171 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*End_Proof*)
172 if p = ([], Res) andalso f2str fb = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
173 then () else error "z-trans (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real)))) changed";
176 (([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
177 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
178 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
179 (([2], Pbl), Problem (Isac, [partial_fraction, rational, simplification])),
180 (([2,1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
181 (([2,1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
182 (([2,2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
183 (([2,2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
184 (([2,2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
185 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
186 (([2,2,2], Res), z = 1 / 2 | z = -1 / 4),
187 (([2,2,3], Res), [z = 1 / 2, z = -1 / 4]),
188 (([2,2,4], Res), [z = 1 / 2, z = -1 / 4]),
189 (([2,2], Res), [z = 1 / 2, z = -1 / 4]),
190 (([2,3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
191 (([2,3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
192 (([2,4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
193 (([2,4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
194 (([2,5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
195 (([2,5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
196 (([2,6], Res), 3 = 3 * A / 4),
197 (([2,7], Pbl), solve (3 = 3 * A / 4, A)),
198 (([2,7,1], Frm), 3 = 3 * A / 4),
199 (([2,7,1], Res), 3 - 3 * A / 4 = 0),
200 (([2,7,2], Res), 3 / 1 + -3 / 4 * A = 0),
201 (([2,7,3], Res), 3 + -3 / 4 * A = 0),
202 (([2,7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
203 (([2,7,4,1], Frm), 3 + -3 / 4 * A = 0),
204 (([2,7,4,1], Res), A = -1 * 3 / (-3 / 4)),
205 (([2,7,4,2], Res), A = -3 / (-3 / 4)),
206 (([2,7,4,3], Res), A = 4),
207 (([2,7,4,4], Res), [A = 4]),
208 (([2,7,4,5], Res), [A = 4]),
209 (([2,7,4], Res), [A = 4]),
210 (([2,7], Res), [A = 4]),
211 (([2,8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
212 (([2,8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
213 (([2,9], Res), 3 = -3 * B / 4),
214 (([2,10], Pbl), solve (3 = -3 * B / 4, B)),
215 (([2,10,1], Frm), 3 = -3 * B / 4),
216 (([2,10,1], Res), 3 - -3 * B / 4 = 0),
217 (([2,10,2], Res), 3 / 1 + 3 / 4 * B = 0),
218 (([2,10,3], Res), 3 + 3 / 4 * B = 0),
219 (([2,10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
220 (([2,10,4,1], Frm), 3 + 3 / 4 * B = 0),
221 (([2,10,4,1], Res), B = -1 * 3 / (3 / 4)),
222 (([2,10,4,2], Res), B = -3 / (3 / 4)),
223 (([2,10,4,3], Res), B = -4),
224 (([2,10,4,4], Res), [B = -4]),
225 (([2,10,4,5], Res), [B = -4]),
226 (([2,10,4], Res), [B = -4]),
227 (([2,10], Res), [B = -4]),
228 (([2,11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
229 (([2,11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
230 (([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
231 (([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
232 (([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))),
233 (([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))),
234 (([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]),
235 (([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n])]
238 "----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
239 "----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
240 "----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
242 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
243 "stepResponse (x[n::real]::bool)"];
244 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
245 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
246 CalcTree [(fmz, (dI,pI,mI))];
249 autoCalculate 1 CompleteCalc;
251 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
252 val (Form f, tac, asms) = pt_extract (pt, p);
253 if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
254 andalso p = ([], Res) then ()
255 else error "inv Z, exp 1 autoCalculate changed"
258 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
259 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
260 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
262 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
263 "stepResponse (x[n::real]::bool)"];
264 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
265 ["SignalProcessing", "Z_Transform", "Inverse"]);
266 CalcTree [(fmz, (dI,pI,mI))];
269 autoCalculate 1 CompleteCalc;
271 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
272 val (Form f, tac, asms) = pt_extract (pt, p);
273 if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
274 andalso p = ([], Res) then ()
275 else error "inv Z, exp 1 autoCalculate changed"
279 (([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
280 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
281 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
282 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
283 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
284 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
285 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
286 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
287 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
288 (([3,3], Res), [z = 1 / 2, z = -1 / 4]),
289 (([3,4], Res), [z = 1 / 2, z = -1 / 4]),
290 (([3], Res), [z = 1 / 2, z = -1 / 4]),
291 (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
292 (([4], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
293 (([5], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
294 (([5], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
295 (([6], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
296 (([6], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
297 (([7], Res), 3 = 3 * A / 4),
298 (([8], Pbl), solve (3 = 3 * A / 4, A)),
299 (([8,1], Frm), 3 = 3 * A / 4),
300 (([8,1], Res), 3 - 3 * A / 4 = 0),
301 (([8,2], Res), 3 / 1 + -3 / 4 * A = 0),
302 (([8,3], Res), 3 + -3 / 4 * A = 0),
303 (([8,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
304 (([8,4,1], Frm), 3 + -3 / 4 * A = 0),
305 (([8,4,1], Res), A = -1 * 3 / (-3 / 4)),
306 (([8,4,2], Res), A = -3 / (-3 / 4)),
307 (([8,4,3], Res), A = 4),
308 (([8,4,4], Res), [A = 4]),
309 (([8,4,5], Res), [A = 4]),
310 (([8,4], Res), [A = 4]),
311 (([8], Res), [A = 4]),
312 (([9], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
313 (([9], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
314 (([10], Res), 3 = -3 * B / 4),
315 (([11], Pbl), solve (3 = -3 * B / 4, B)),
316 (([11,1], Frm), 3 = -3 * B / 4),
317 (([11,1], Res), 3 - -3 * B / 4 = 0),
318 (([11,2], Res), 3 / 1 + 3 / 4 * B = 0),
319 (([11,3], Res), 3 + 3 / 4 * B = 0),
320 (([11,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
321 (([11,4,1], Frm), 3 + 3 / 4 * B = 0),
322 (([11,4,1], Res), B = -1 * 3 / (3 / 4)),
323 (([11,4,2], Res), B = -3 / (3 / 4)),
324 (([11,4,3], Res), B = -4),
325 (([11,4,4], Res), [B = -4]),
326 (([11,4,5], Res), [B = -4]),
327 (([11,4], Res), [B = -4]),
328 (([11], Res), [B = -4]),
329 (([12], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
330 (([12], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
331 (([13], Res), 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))),
332 (([14], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))),
333 (([14], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]),
334 (([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n])] *)
336 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
337 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
338 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
339 (*====================================================================
340 (* Below are _all_ steps from BridgeLog; _superfluous_ ones and output are text.
341 REASON FOR THE ERROR: Inverse_Z_Transform.thy did not contain final version of method.
343 [[to sml: theory TTY_Communication imports Isac.Isac begin
344 ML {* reset_states (); *}
346 ML {* CalcTree [(["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
347 "stepResponse (x[n::real]::bool)"],("Isac",["Inverse","Z_Transform","SignalProcessing"],
348 ["SignalProcessing","Z_Transform","Inverse"]))]; *}
350 ML {* moveActiveRoot 1; *}
351 ML {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
352 text {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
353 ML {* "##### 1.<NEXT> ############################################" *}
354 ML {* (*completeCalcHead*)autoCalculate 1 CompleteCalcHead; *}
355 text {* (*completeCalcHead*)getActiveFormula 1 ; *}
356 text {* (*completeCalcHead*)refFormula 1 ([],Met); *}
357 text {* refFormula 1 ([],Pbl); *}
358 text {* fetchProposedTactic 1; *}
359 ML {* autoCalculate 1 (Step 1); *}
360 text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
361 text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
362 ML {* refFormula 1 ([1],Frm); *}
363 text {*<ISA> ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) </ISA>*}
364 text {* refFormula 1 ([1],Frm); *}
365 ML {* "##### 2.<NEXT> ############################################" *}
366 text {* refFormula 1 ([1],Frm); *}
367 ML {* autoCalculate 1 (Step 1); *}
368 text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
369 text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
370 ML {* refFormula 1 ([1],Res); *}
371 text {*<ISA> ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) </ISA>*}
372 ML {* refFormula 1 ([1],Res); *}
373 ML {* "##### 3.<NEXT> ############################################" *}
374 text {* refFormula 1 ([1],Res); *}
375 ML {* autoCalculate 1 (Step 1); *}
376 text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
377 text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
378 ML {* refFormula 1 ([2],Res); *}
379 text {*<ISA> rhs (?X' z = 24 / (-1 + -2 * z + 8 * z ^ 2)) </ISA>*}
380 text {* refFormula 1 ([2],Res); *}
381 ML {* "##### 4.<NEXT> ############################################" *}
382 text {* refFormula 1 ([2],Res); *}
383 ML {* autoCalculate 1 (Step 1); *}
384 text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
385 text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
386 ML {* refFormula 1 ([3],Frm); *}
387 text {*<ISA> rhs (?X' z = 24 / (-1 + -2 * z + 8 * z ^ 2)) </ISA>*}
388 text {* refFormula 1 ([3],Frm); *}
389 ML {* "##### 5.<NEXT> ############################################" *}
390 text {* refFormula 1 ([3],Frm); *}
391 ML {* autoCalculate 1 (Step 1); *}
392 text {*<CALCMESSAGE> helpless </CALCMESSAGE>*}
393 ====================================================================*)