1 (* Title: Test_Z_Transform
3 (c) copyright due to lincense terms.
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 theory Test_Z_Transform imports Isac begin
10 section {*trials towards Z transform *}
11 text{*===============================*}
14 @{term "1 < || z ||"};
15 @{term "z / (z - 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]"};
23 (*alpha --> "</alpha>" *)
29 term2str @{term "\<rho> "};
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 /"*)
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]"
49 subsection {*apply rules*}
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})
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 !!!*)
62 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
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 *)
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 *)
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 *)
80 terms2str (asm1 @ asm2 @ asm3);
83 section {*Prepare steps in CTP-based programming language*}
84 text{*===================================================*}
85 subsection {*prepare expression*}
87 val ctxt = ProofContext.init_global @{theory};
88 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
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';
95 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
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';
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*)
107 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
110 subsection {*solve equation*}
111 text {*this type of equation if too general for the present program*}
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*)
119 text {*Does the Equation Match the Specification ?*}
121 match_pbl fmz (get_pbt ["univariate","equation"]);
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)*)
132 ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
134 text {*Does the Other Equation Match the Specification ?*}
136 match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]);
138 text {*Solve Equation Stepwise*}
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*)
157 val SOME f = parseNEW ctxt "[z = 1 / 8 + 3 / 8, z = 1 / 8 + -3 / 8]";
160 subsection {*partial fraction decomposition*}
161 subsubsection {*solution of the equation*}
163 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
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...*}
171 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $
172 s_2 $ Const ("List.list.Nil", _)) = solutions;
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;
186 subsubsection {*build expression*}
187 text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}
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";
193 val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');
197 subsubsection {*Ansatz - create partial fractions out of our expression*}
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))"
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);
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;
217 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
218 term2str eq3; (*?A ?B not simplified*)
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*)
228 val (numerator, denominator) = HOLogic.dest_eq eq3;
229 val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)
231 (*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*)
232 val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
236 subsubsection {*get first koeffizient*}
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'';
243 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
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;
280 subsubsection {*get second koeffizient*}
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'';
287 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
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;
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";
330 subsubsection {*substitute expression with solutions*}
334 section {*Implement the Specification and the Method*}
335 text{*==============================================*}
336 subsection{*Define the Specification*}
342 (prep_pbt thy "pbl_SP" [] e_pblID
343 (["SignalProcessing"], [], e_rls, NONE, []));
345 (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
346 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
348 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
349 (["inverse", "Z_Transform", "SignalProcessing"],
350 [("#Given" ,["equality X_eq"]),
351 ("#Find" ,["equality n_eq"])
353 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
354 [["TODO: path to method"]]));
357 get_pbt ["inverse","Z_Transform","SignalProcessing"];
360 subsection{*Define the (Dummy-)Method*}
361 subsection {*Define Name and Signature for the Method*}
363 InverseZTransform :: "[bool, bool] => bool"
364 ("((Script InverseZTransform (_ =))// (_))" 9)
368 (prep_met thy "met_SP" [] e_metID
369 (["SignalProcessing"], [],
370 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
371 crls = e_rls, nrls = e_rls}, "empty_script"));
373 (prep_met thy "met_SP_Ztrans" [] e_metID
374 (["SignalProcessing", "Z_Transform"], [],
375 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
376 crls = e_rls, nrls = e_rls}, "empty_script"));
380 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
381 (["SignalProcessing", "Z_Transform", "inverse"], [],
382 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
383 crls = e_rls, nrls = e_rls},
386 val thy = @{theory}; (*latest version of thy required*)
388 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
389 (["SignalProcessing", "Z_Transform", "inverse"],
390 [("#Given" ,["equality X_eq"]),
391 ("#Find" ,["equality n_eq"])
393 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
394 crls = e_rls, nrls = e_rls},
395 "Script InverseZTransform (Xeq::bool) =" ^
396 " (let X = Take Xeq;" ^
397 " X = Rewrite ruleZY False X" ^
402 get_met ["SignalProcessing","Z_Transform","inverse"];
406 section {*Program in CTP-based language*}
407 text{*=================================*}
408 subsection {*Stepwise extend Program*}
411 "Script InverseZTransform (Xeq::bool) =" ^
416 "Script InverseZTransform (Xeq::bool) =" ^
417 " (let X = Take Xeq;" ^
418 " X = Rewrite ruleZY False X" ^
423 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
431 subsection {*Store Final Version of Program for Execution*}
434 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
435 (["SignalProcessing", "Z_Transform", "inverse"],
436 [("#Given" ,["equality X_eq"]),
437 ("#Find" ,["equality n_eq"])
439 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
440 crls = e_rls, nrls = e_rls},
441 "Script InverseZTransform (Xeq::bool) =" ^
442 " (let X = Take Xeq;" ^
443 " X = Rewrite ruleZY False X" ^
449 subsection {*Stepwise Execute the Program*}
458 section {*Write Tests for Crucial Details*}
459 text{*===================================*}
464 section {*Integrate Program into Knowledge*}