1 (* Title: Test_Z_Transform |
|
2 Author: Jan Rocnik |
|
3 (c) copyright due to lincense terms. |
|
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
5 10 20 30 40 50 60 70 80 |
|
6 *) |
|
7 |
|
8 theory Inverse_Z_Transform imports Isac begin |
|
9 |
|
10 section {*trials towards Z transform *} |
|
11 text{*===============================*} |
|
12 subsection {*terms*} |
|
13 ML {* |
|
14 @{term "1 < || z ||"}; |
|
15 @{term "z / (z - 1)"}; |
|
16 @{term "-u -n - 1"}; |
|
17 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*) |
|
18 @{term "z /(z - 1) = -u [-n - 1]"};Isac |
|
19 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"}; |
|
20 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"}; |
|
21 *} |
|
22 ML {* |
|
23 (*alpha --> "</alpha>" *) |
|
24 |
|
25 @{term "\<alpha> "}; |
|
26 @{term "\<delta> "}; |
|
27 @{term "\<phi> "}; |
|
28 @{term "\<rho> "}; |
|
29 term2str @{term "\<rho> "}; |
|
30 *} |
|
31 |
|
32 subsection {*rules*} |
|
33 (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *) |
|
34 (*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*) |
|
35 axiomatization where |
|
36 rule1: "1 = \<delta>[n]" and |
|
37 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and |
|
38 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and |
|
39 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and |
|
40 rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and |
|
41 rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" |
|
42 ML {* |
|
43 @{thm rule1}; |
|
44 @{thm rule2}; |
|
45 @{thm rule3}; |
|
46 @{thm rule4}; |
|
47 *} |
|
48 |
|
49 subsection {*apply rules*} |
|
50 ML {* |
|
51 val inverse_Z = append_rls "inverse_Z" e_rls |
|
52 [ Thm ("rule3",num_str @{thm rule3}), |
|
53 Thm ("rule4",num_str @{thm rule4}), |
|
54 Thm ("rule1",num_str @{thm rule1}) |
|
55 ]; |
|
56 |
|
57 val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1"; |
|
58 val SOME (t', asm) = rewrite_set_ thy true inverse_Z t; |
|
59 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*) |
|
60 *} |
|
61 ML {* |
|
62 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
|
63 *} |
|
64 ML {* |
|
65 val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t; |
|
66 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *) |
|
67 term2str t; |
|
68 *} |
|
69 ML {* |
|
70 val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t; |
|
71 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *) |
|
72 term2str t; |
|
73 *} |
|
74 ML {* |
|
75 val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t; |
|
76 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *) |
|
77 term2str t; |
|
78 *} |
|
79 ML {* |
|
80 terms2str (asm1 @ asm2 @ asm3); |
|
81 *} |
|
82 |
|
83 section {*Prepare steps in CTP-based programming language*} |
|
84 text{*===================================================*} |
|
85 subsection {*prepare expression*} |
|
86 ML {* |
|
87 val ctxt = ProofContext.init_global @{theory}; |
|
88 val ctxt = declare_constraints' [@{term "z::real"}] ctxt; |
|
89 |
|
90 val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; |
|
91 val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1'; |
|
92 *} |
|
93 |
|
94 axiomatization where |
|
95 ruleZY: "(X z = a / b) = (X' z = a / (z * b))" |
|
96 |
|
97 ML {* |
|
98 val (thy, ro, er) = (@{theory}, tless_true, eval_rls); |
|
99 val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2; |
|
100 val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2'; |
|
101 |
|
102 val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2; |
|
103 term2str fun3; (*fails on x^^^(-1) TODO*) |
|
104 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2'; |
|
105 term2str fun3'; (*OK*) |
|
106 |
|
107 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr; |
|
108 *} |
|
109 |
|
110 subsection {*solve equation*} |
|
111 text {*this type of equation if too general for the present program*} |
|
112 ML {* |
|
113 "----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------"; |
|
114 val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0"; |
|
115 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"]; |
|
116 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
|
117 (* ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*) |
|
118 *} |
|
119 text {*Does the Equation Match the Specification ?*} |
|
120 ML {* |
|
121 match_pbl fmz (get_pbt ["univariate","equation"]); |
|
122 *} |
|
123 |
|
124 ML {* |
|
125 val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^^^2 = 0"; |
|
126 val fmz = (*specification*) |
|
127 ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*) |
|
128 "solveFor z", (*bound variable*) |
|
129 "solutions L"]; (*identifier for solution*) |
|
130 (*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*) |
|
131 val (dI',pI',mI') = |
|
132 ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]); |
|
133 *} |
|
134 text {*Does the Other Equation Match the Specification ?*} |
|
135 ML {* |
|
136 match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]); |
|
137 *} |
|
138 text {*Solve Equation Stepwise*} |
|
139 ML {* |
|
140 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
141 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
145 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
146 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
147 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
148 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
149 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) |
|
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
|
155 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*) |
|
156 show_pt pt; |
|
157 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]"; |
|
158 *} |
|
159 |
|
160 subsection {*partial fraction decomposition*} |
|
161 subsubsection {*solution of the equation*} |
|
162 ML {* |
|
163 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]"; |
|
164 term2str solutions; |
|
165 atomty solutions; |
|
166 *} |
|
167 |
|
168 subsubsection {*get solutions out of list*} |
|
169 text {*in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$*} |
|
170 ML {* |
|
171 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $ |
|
172 s_2 $ Const ("List.list.Nil", _)) = solutions; |
|
173 term2str s_1; |
|
174 term2str s_2; |
|
175 *} |
|
176 |
|
177 ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*) |
|
178 val xx = HOLogic.dest_eq s_1; |
|
179 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
|
180 val xx = HOLogic.dest_eq s_2; |
|
181 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
|
182 term2str s_1'; |
|
183 term2str s_2'; |
|
184 *} |
|
185 |
|
186 subsubsection {*build expression*} |
|
187 text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*} |
|
188 ML {* |
|
189 (*The Main Denominator is the multiplikation of the partial fraction denominators*) |
|
190 val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ; |
|
191 val SOME numerator = parseNEW ctxt "3::real"; |
|
192 |
|
193 val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator'); |
|
194 term2str expr'; |
|
195 *} |
|
196 |
|
197 subsubsection {*Ansatz - create partial fractions out of our expression*} |
|
198 |
|
199 axiomatization where |
|
200 ansatz2: "n / (a*b) = A/a + B/(b::real)" and |
|
201 multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))" |
|
202 |
|
203 ML {* |
|
204 (*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*) |
|
205 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr'; |
|
206 term2str t1; atomty t1; |
|
207 val eq1 = HOLogic.mk_eq (expr', t1); |
|
208 term2str eq1; |
|
209 *} |
|
210 ML {* |
|
211 (*eliminate the demoninators by multiplying the left and the right side with the main denominator*) |
|
212 val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1; |
|
213 term2str eq2; |
|
214 *} |
|
215 ML {* |
|
216 (*simplificatoin*) |
|
217 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2; |
|
218 term2str eq3; (*?A ?B not simplified*) |
|
219 *} |
|
220 ML {* |
|
221 val SOME fract1 = |
|
222 parseNEW ctxt "(z - 1 / 2) * (z - -1 / 4) * (A / (z - 1 / 2) + B / (z - -1 / 4))"; (*A B !*) |
|
223 val SOME (fract2,_) = rewrite_set_ @{theory Isac} false norm_Rational fract1; |
|
224 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4"; |
|
225 (*term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" would be more traditional*) |
|
226 *} |
|
227 ML {* |
|
228 val (numerator, denominator) = HOLogic.dest_eq eq3; |
|
229 val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*) |
|
230 term2str eq3'; |
|
231 (*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*) |
|
232 val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3'; |
|
233 term2str eq3''; |
|
234 *} |
|
235 |
|
236 subsubsection {*get first koeffizient*} |
|
237 |
|
238 ML {* |
|
239 (*substitude z with the first zeropoint to get A*) |
|
240 val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3''; |
|
241 term2str eq4_1; |
|
242 |
|
243 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1; |
|
244 term2str eq4_2; |
|
245 |
|
246 val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"]; |
|
247 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
|
248 (*solve the simple linear equilation for A TODO: return eq, not list of eq*) |
|
249 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
250 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
251 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
252 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
253 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
254 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
255 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
256 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
257 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
258 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
259 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
260 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
261 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
262 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
263 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
264 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
265 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
266 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
267 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
268 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
269 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
270 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
271 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
272 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
273 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
274 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
275 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
276 val (p,_,fa,nxt,_,pt) = me nxt p [] pt; |
|
277 f2str fa; |
|
278 *} |
|
279 |
|
280 subsubsection {*get second koeffizient*} |
|
281 |
|
282 ML {* |
|
283 (*substitude z with the second zeropoint to get B*) |
|
284 val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3''; |
|
285 term2str eq4b_1; |
|
286 |
|
287 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1; |
|
288 term2str eq4b_2; |
|
289 *} |
|
290 ML {* |
|
291 (*solve the simple linear equilation for B TODO: return eq, not list of eq*) |
|
292 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"]; |
|
293 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
|
294 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
295 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
296 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
297 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
298 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
299 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
300 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
301 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
302 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
303 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
304 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
305 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
306 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
307 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
308 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
309 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
310 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
311 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
312 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
313 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
314 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
315 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
316 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
317 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
318 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
319 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
320 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
321 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
322 f2str fb; |
|
323 *} |
|
324 |
|
325 ML {* (*check koeffizients*) |
|
326 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1"; |
|
327 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1"; |
|
328 *} |
|
329 |
|
330 subsubsection {*substitute expression with solutions*} |
|
331 ML {* |
|
332 *} |
|
333 |
|
334 section {*Implement the Specification and the Method*} |
|
335 text{*==============================================*} |
|
336 subsection{*Define the Field Descriptions for the specification*} |
|
337 consts |
|
338 filterExpression :: "bool => una" |
|
339 stepResponse :: "bool => una" |
|
340 |
|
341 subsection{*Define the Specification*} |
|
342 ML {* |
|
343 val thy = @{theory}; |
|
344 *} |
|
345 ML {* |
|
346 store_pbt |
|
347 (prep_pbt thy "pbl_SP" [] e_pblID |
|
348 (["SignalProcessing"], [], e_rls, NONE, [])); |
|
349 store_pbt |
|
350 (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID |
|
351 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])); |
|
352 store_pbt |
|
353 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID |
|
354 (["inverse", "Z_Transform", "SignalProcessing"], |
|
355 [("#Given" ,["filterExpression X_eq"]), |
|
356 ("#Find" ,["stepResponse n_eq"]) |
|
357 ], |
|
358 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, |
|
359 [["SignalProcessing","Z_Transform","inverse"]])); |
|
360 |
|
361 show_ptyps(); |
|
362 get_pbt ["inverse","Z_Transform","SignalProcessing"]; |
|
363 *} |
|
364 |
|
365 subsection {*Define Name and Signature for the Method*} |
|
366 consts |
|
367 InverseZTransform :: "[bool, bool] => bool" |
|
368 ("((Script InverseZTransform (_ =))// (_))" 9) |
|
369 |
|
370 subsection {*Setup Parent Nodes in Hierarchy of Method*} |
|
371 ML {* |
|
372 store_met |
|
373 (prep_met thy "met_SP" [] e_metID |
|
374 (["SignalProcessing"], [], |
|
375 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, |
|
376 crls = e_rls, nrls = e_rls}, "empty_script")); |
|
377 store_met |
|
378 (prep_met thy "met_SP_Ztrans" [] e_metID |
|
379 (["SignalProcessing", "Z_Transform"], [], |
|
380 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, |
|
381 crls = e_rls, nrls = e_rls}, "empty_script")); |
|
382 *} |
|
383 ML {* |
|
384 val thy = @{theory}; (*latest version of thy required*) |
|
385 store_met |
|
386 (prep_met thy "met_SP_Ztrans_inv" [] e_metID |
|
387 (["SignalProcessing", "Z_Transform", "inverse"], |
|
388 [("#Given" ,["filterExpression X_eq"]), |
|
389 ("#Find" ,["stepResponse n_eq"]) |
|
390 ], |
|
391 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, |
|
392 crls = e_rls, nrls = e_rls}, |
|
393 "Script InverseZTransform (Xeq::bool) =" ^ |
|
394 " (let X = Take Xeq;" ^ |
|
395 " X = Rewrite ruleZY False X" ^ |
|
396 " in X)" |
|
397 )); |
|
398 |
|
399 show_mets(); |
|
400 get_met ["SignalProcessing","Z_Transform","inverse"]; |
|
401 *} |
|
402 |
|
403 |
|
404 section {*Program in CTP-based language*} |
|
405 text{*=================================*} |
|
406 subsection {*Stepwise extend Program*} |
|
407 ML {* |
|
408 val str = |
|
409 "Script InverseZTransform (Xeq::bool) =" ^ |
|
410 " Xeq"; |
|
411 *} |
|
412 ML {* |
|
413 val str = |
|
414 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
|
415 " (let X = Take Xeq;" ^ |
|
416 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
|
417 " X' = (Rewrite_Set norm_Rational False) X'" ^ (*simplify*) |
|
418 " in X)"; |
|
419 (*NONE*) |
|
420 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
|
421 " (let X = Take Xeq;" ^ |
|
422 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
|
423 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
|
424 " X' = (SubProblem (Isac',[pqFormula,degree_2,polynomial,univariate,equation], [no_met]) " ^ |
|
425 " [BOOL e_e, REAL v_v])" ^ |
|
426 " in X)"; |
|
427 *} |
|
428 ML {* |
|
429 val str = |
|
430 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
|
431 " (let X = Take Xeq;" ^ |
|
432 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
|
433 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
|
434 " funterm = rhs X'" ^ (*drop X'= for equation solving*) |
|
435 " in X)"; |
|
436 *} |
|
437 ML {* |
|
438 parse thy str; |
|
439 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
440 atomty sc; |
|
441 |
|
442 *} |
|
443 ML {* |
|
444 term2str sc; |
|
445 atomty sc |
|
446 *} |
|
447 |
|
448 |
|
449 subsection {*Store Final Version of Program for Execution*} |
|
450 ML {* |
|
451 store_met |
|
452 (prep_met thy "met_SP_Ztrans_inv" [] e_metID |
|
453 (["SignalProcessing", "Z_Transform", "inverse"], |
|
454 [("#Given" ,["filterExpression X_eq"]), |
|
455 ("#Find" ,["stepResponse n_eq"]) |
|
456 ], |
|
457 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, |
|
458 crls = e_rls, nrls = e_rls}, |
|
459 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
|
460 " (let X = Take Xeq;" ^ |
|
461 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
|
462 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
|
463 " funterm = rhs X'" ^ (*drop X'= for equation solving*) |
|
464 " in X)" |
|
465 )); |
|
466 *} |
|
467 |
|
468 |
|
469 subsection {*Stepwise Execute the Program*} |
|
470 ML {* |
|
471 parseNEW ctxt "stepResponse x[n]"; |
|
472 Thy_Info.get_theory "Inverse_Z_Transform"; |
|
473 *} |
|
474 |
|
475 ML {* |
|
476 print_depth 999; Thy_Info.get_names(); print_depth 999; |
|
477 *} |
|
478 |
|
479 ML {* |
|
480 (*val SOME func = parseNEW ctxt "X = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1;*) |
|
481 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/z)))", "stepResponse x[n]"]; |
|
482 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], |
|
483 ["SignalProcessing","Z_Transform","inverse"]); |
|
484 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; |
|
485 *} |
|
486 |
|
487 ML {* |
|
488 get_met ["SignalProcessing","Z_Transform","inverse"]; |
|
489 *} |
|
490 ML {* |
|
491 val (p,_,fb,nxt,_,pt) = me nxt p [] pt |
|
492 *} |
|
493 |
|
494 ML {* |
|
495 f2str fb; |
|
496 *} |
|
497 |
|
498 ML {* |
|
499 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"]; |
|
500 val (dI,pI,mI) =("Isac", ["univariate","equation"], ["no_met"]); |
|
501 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; |
|
502 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
503 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
504 *} |
|
505 |
|
506 ML {* |
|
507 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
|
508 f2str fb; |
|
509 *} |
|
510 |
|
511 |
|
512 |
|
513 |
|
514 |
|
515 |
|
516 |
|
517 |
|
518 section {*Write Tests for Crucial Details*} |
|
519 text{*===================================*} |
|
520 ML {* |
|
521 |
|
522 *} |
|
523 |
|
524 section {*Integrate Program into Knowledge*} |
|
525 ML {* |
|
526 |
|
527 *} |
|
528 |
|
529 end |
|
530 |
|