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