1 (* Title: Knowledge/Inverse_Z_Transform/inverse_z_transform.sml
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
10 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
11 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
12 "-----------------------------------------------------------------";
13 "-----------------------------------------------------------------";
15 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
16 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
17 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
18 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
19 MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
21 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
22 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
23 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
24 (* the ONLY Test_Isac, which uses Rewrite !!! *)
25 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))",
26 "functionName X_z", "stepResponse (x[n::real]::bool)"];
27 val (dI, pI, mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
28 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
29 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
30 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
31 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
32 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac_Knowledge"*)
33 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem ["Inverse_sub", "Z_Transform", "SignalProcessing"]*)
34 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse_sub"]*)
35 (*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "boundVariable X_z"*)
36 (*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Me["SignalProcessing", "Z_Transform", "Inverse_sub"]*)
37 (*[1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleZY", "Inverse_Z_Transform.ruleZY")*)
38 (*[1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac_Knowledge", ["partial_fraction", "rational..*)
39 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
40 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "functionTerm (X' z)"*)
41 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
42 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "decomposedFunction p_p'''"*)
43 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory*)
44 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
45 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
46 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["simplification", "of_rationals", "to_partial_fraction"]*)
48 (*[2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
49 if p = ([2, 1], Frm) andalso f2str fb = "3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z)))"
50 then () else error "Z_Transform,inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
52 (*[2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac_Knowledge", ["abcFormula", "degree_2", "po...a*)
53 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
54 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
55 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
56 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
57 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
58 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
59 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
60 (*[2,2], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"*)
61 (*[2,2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
62 if p = ([2, 2, 1], Frm) andalso f2str fb = "- 1 + - 2 * z + 8 * z \<up> 2 = 0"
63 then () else error "Z_Transform,inverse_sub] me 2";
65 (*[2,2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
66 (*[2,2,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
67 (*[2,2,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
68 (*[2,2,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]*)
69 (*[2,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Take "3 / ((z - 1 / 2) * (z - - 1 / 4))"*)
70 (*[2,3], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "ansatz_rls"*)
71 (*[2,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Take "3 / ((z - 1 / 2) * (z - - 1 / 4)) = AA / (z - 1 / 2) + BB / (z - - 1 / 4)*)
72 (*[2,4], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "equival_trans"*)
73 (*[2,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Take "3 = A * (z - - 1 / 4) + B * (z - 1 / 2)"*)
74 (*[2,5], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*"Substitute ["z = 1 / 2"]*)
75 (*[2,5], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
76 if p = ([2, 5], Res) andalso f2str fb = "3 = AA * (1 / 2 - - 1 / 4) + BB * (1 / 2 - 1 / 2)"
77 then () else error "Z_Transform,inverse_sub] me 3"; (*Rewrite_Set "norm_Rational"*)
79 (*[2, 6], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem (Isac, ["normalise", "polynomial", "univariate", "equation"]*)
80 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
81 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
82 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
83 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
84 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
85 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
86 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
87 (*[2,7], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
88 (*[2,7,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
89 (*[2,7,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
90 (*[2,7,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
91 if p = ([2, 7, 2], Res) andalso f2str fb = "3 / 1 + -3 / 4 * AA = 0"
92 then () else error "Z_Transform,inverse_sub] me 5";
94 (*[2,7,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
95 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
96 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
97 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
98 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
99 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
100 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
101 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
102 (*[2,7,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
103 (*[2,7,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
104 if p = ([2, 7, 4, 1], Frm) andalso f2str fb = "3 + -3 / 4 * AA = 0"
105 then () else error "Z_Transform,inverse_sub] me 6";
107 (*[2,7,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
108 (*[2,7,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
109 (*[2,7,4,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
110 (*[2,7,4,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
111 (*[2,7,4,5], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
112 (*[2,7,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
113 (*[2,7], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
114 (*[2,8], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
115 (*[2,8], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
116 if p = ([2, 8], Res) andalso f2str fb = "3 = AA * (- 1 / 4 - - 1 / 4) + BB * (- 1 / 4 - 1 / 2)"
117 then () else error "Z_Transform,inverse_sub] me 7";
119 (*[2,9], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
120 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
121 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
122 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
123 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
124 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
125 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
126 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
127 (*[2,10], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
128 (*[2,10,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
129 if p = ([2, 10, 1], Frm) andalso f2str fb = "3 = -3 * BB / 4"
130 then () else error "Z_Transform,inverse_sub] me 8";
132 (*[2,10,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
133 (*[2,10,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
134 if p = ([2, 10, 2], Res) andalso f2str fb = "3 / 1 + 3 / 4 * BB = 0"
135 then () else error "Z_Transform,inverse_sub] me 9";
137 (*[2,10,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
138 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
139 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
140 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
141 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
142 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
143 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
144 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
146 (*[2,10,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
147 (*[2,10,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
148 if p = ([2, 10, 4, 1], Frm) andalso f2str fb = "3 + 3 / 4 * BB = 0"
149 then () else error "Z_Transform,inverse_sub] me 10";
151 ((*[2,10,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
152 (*[2,10,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
153 (*[2,10,4,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
154 (*[2,10,4,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
155 (*[2,10,4,5], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
156 (*[2,10,4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
157 (*[2,10], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
158 (*[2,11], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
159 (*[2,11], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["partial_fraction", "rational", "simplification"]*)
160 (*[2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
161 f2str fb = "X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - - 1 / 4))"; (*Take "?X' z = 4 / (z - 1 / 2) + -4 / (z - - 1 / 4)"*)
163 (*[3], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
164 f2str fb = "?X' z = 4 / (z - 1 / 2) + -4 / (z - - 1 / 4)"; (*Rewrite ("ruleYZ", "?a / ?b + ?c / ?d = ?a * (?z / ?b) + ?c * (?z / ?d)")*)
166 (*[3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
167 f2str fb = "?X' z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - - 1 / 4))";(*Take "X_z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - - 1 / 4))"*)
169 (*[4], Frm)*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
170 (*[4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
171 (*[], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
173 case nxt of (_, End_Proof') =>
174 if p = ([], Res) andalso
175 f2str fb = "X_z = 4 * (1 / 2) \<up> ?n * ?u [?n] + -4 * (- 1 / 4) \<up> ?n * ?u [?n]"
176 then () else error "[SignalProcessing,Z_Transform,Inverse_sub] changed 1"
177 | _ => error "[SignalProcessing,Z_Transform,Inverse_sub] changed 2";
180 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
181 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
182 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
184 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))",
185 "functionName X_z", "stepResponse (x[n::real]::bool)"];
186 val (dI, pI, mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
187 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
188 CalcTree [(fmz, (dI,pI,mI))];
191 autoCalculate 1 CompleteCalc;
193 val ((pt,_),_) = States.get_calc 1; val p = States.get_pos 1 1;
194 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
195 if UnparseC.term f = "X_z = 4 * (1 / 2) \<up> ?n * ?u [?n] + -4 * (- 1 / 4) \<up> ?n * ?u [?n]"
196 andalso p = ([], Res) then ()
197 else error "inv Z, exp 1 autoCalculate changed";