neuper@42256
|
1 |
(* Title: Test_Z_Transform
|
neuper@42256
|
2 |
Author: Jan Rocnik
|
neuper@42256
|
3 |
(c) copyright due to lincense terms.
|
neuper@42256
|
4 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@42256
|
5 |
10 20 30 40 50 60 70 80
|
neuper@42256
|
6 |
*)
|
neuper@42256
|
7 |
|
neuper@42290
|
8 |
theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
|
neuper@42256
|
9 |
|
neuper@42256
|
10 |
axiomatization where
|
neuper@42256
|
11 |
rule1: "1 = \<delta>[n]" and
|
neuper@42256
|
12 |
rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
|
neuper@42256
|
13 |
rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
|
jan@42367
|
14 |
rule4: "c * (z / (z - \<alpha>)) = c * \<alpha>^^^n * u [n]" and
|
neuper@42256
|
15 |
rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
|
jan@42367
|
16 |
rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and
|
jan@42367
|
17 |
rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
|
neuper@42256
|
18 |
|
neuper@42256
|
19 |
axiomatization where
|
jan@42367
|
20 |
ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
|
jan@42367
|
21 |
ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))"
|
neuper@42256
|
22 |
|
neuper@42279
|
23 |
subsection{*Define the Field Descriptions for the specification*}
|
neuper@42279
|
24 |
consts
|
neuper@42279
|
25 |
filterExpression :: "bool => una"
|
neuper@42279
|
26 |
stepResponse :: "bool => una"
|
neuper@42279
|
27 |
|
jan@42366
|
28 |
|
jan@42366
|
29 |
ML {*
|
jan@42366
|
30 |
val inverse_z = prep_rls(
|
jan@42366
|
31 |
Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
neuper@42451
|
32 |
erls = Erls, srls = Erls, calc = [], errpatts = [],
|
jan@42366
|
33 |
rules =
|
jan@42367
|
34 |
[
|
jan@42367
|
35 |
Thm ("rule4",num_str @{thm rule4})
|
jan@42366
|
36 |
],
|
jan@42366
|
37 |
scr = EmptyScr}:rls);
|
jan@42366
|
38 |
*}
|
jan@42366
|
39 |
|
jan@42366
|
40 |
|
jan@42366
|
41 |
text {*store the rule set for math engine*}
|
jan@42366
|
42 |
|
jan@42366
|
43 |
ML {*
|
jan@42366
|
44 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
jan@42366
|
45 |
[("inverse_z", inverse_z)
|
jan@42366
|
46 |
]);
|
jan@42366
|
47 |
*}
|
jan@42366
|
48 |
|
neuper@42256
|
49 |
subsection{*Define the Specification*}
|
neuper@42256
|
50 |
ML {*
|
neuper@42256
|
51 |
val thy = @{theory};
|
neuper@42278
|
52 |
|
neuper@42256
|
53 |
store_pbt
|
neuper@42256
|
54 |
(prep_pbt thy "pbl_SP" [] e_pblID
|
neuper@42256
|
55 |
(["SignalProcessing"], [], e_rls, NONE, []));
|
neuper@42256
|
56 |
store_pbt
|
neuper@42256
|
57 |
(prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
|
neuper@42256
|
58 |
(["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
|
neuper@42256
|
59 |
store_pbt
|
neuper@42256
|
60 |
(prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
|
neuper@42405
|
61 |
(["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42407
|
62 |
(*^ capital letter breaks coding standard
|
neuper@42407
|
63 |
because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
|
neuper@42278
|
64 |
[("#Given" ,["filterExpression (X_eq::bool)"]),
|
neuper@42278
|
65 |
("#Find" ,["stepResponse (n_eq::bool)"])
|
neuper@42256
|
66 |
],
|
neuper@42256
|
67 |
append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
|
neuper@42405
|
68 |
[["SignalProcessing","Z_Transform","Inverse"]]));
|
neuper@42256
|
69 |
*}
|
neuper@42412
|
70 |
ML {*
|
neuper@42412
|
71 |
store_pbt
|
neuper@42412
|
72 |
(prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
|
neuper@42412
|
73 |
(["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42412
|
74 |
[("#Given" ,["filterExpression X_eq"]),
|
neuper@42412
|
75 |
("#Find" ,["stepResponse n_eq"])
|
neuper@42412
|
76 |
],
|
neuper@42412
|
77 |
append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
|
neuper@42412
|
78 |
[["SignalProcessing","Z_Transform","Inverse"]]));
|
neuper@42412
|
79 |
*}
|
neuper@42256
|
80 |
|
neuper@42256
|
81 |
subsection {*Define Name and Signature for the Method*}
|
neuper@42256
|
82 |
consts
|
neuper@42256
|
83 |
InverseZTransform :: "[bool, bool] => bool"
|
neuper@42256
|
84 |
("((Script InverseZTransform (_ =))// (_))" 9)
|
neuper@42256
|
85 |
|
neuper@42277
|
86 |
subsection {*Setup Parent Nodes in Hierarchy of Method*}
|
neuper@42256
|
87 |
ML {*
|
neuper@42256
|
88 |
store_met
|
neuper@42256
|
89 |
(prep_met thy "met_SP" [] e_metID
|
neuper@42256
|
90 |
(["SignalProcessing"], [],
|
neuper@42256
|
91 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42425
|
92 |
crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
|
neuper@42256
|
93 |
store_met
|
neuper@42256
|
94 |
(prep_met thy "met_SP_Ztrans" [] e_metID
|
neuper@42256
|
95 |
(["SignalProcessing", "Z_Transform"], [],
|
neuper@42256
|
96 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42425
|
97 |
crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
|
neuper@42256
|
98 |
val thy = @{theory}; (*latest version of thy required*)
|
neuper@42256
|
99 |
store_met
|
neuper@42256
|
100 |
(prep_met thy "met_SP_Ztrans_inv" [] e_metID
|
neuper@42405
|
101 |
(["SignalProcessing", "Z_Transform", "Inverse"],
|
neuper@42278
|
102 |
[("#Given" ,["filterExpression (X_eq::bool)"]),
|
neuper@42278
|
103 |
("#Find" ,["stepResponse (n_eq::bool)"])
|
neuper@42256
|
104 |
],
|
neuper@42256
|
105 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42425
|
106 |
crls = e_rls, errpats = [], nrls = e_rls},
|
neuper@42281
|
107 |
"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
|
neuper@42281
|
108 |
" (let X = Take X_eq;" ^
|
neuper@42281
|
109 |
" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
|
neuper@42281
|
110 |
" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
|
neuper@42290
|
111 |
" funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
|
neuper@42290
|
112 |
" denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
|
neuper@42290
|
113 |
" equ = (denom = (0::real));" ^
|
neuper@42290
|
114 |
" fun_arg = Take (lhs X');" ^
|
neuper@42290
|
115 |
" arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
|
neuper@42290
|
116 |
" (L_L::bool list) = " ^
|
neuper@42290
|
117 |
" (SubProblem (Test', " ^
|
neuper@42290
|
118 |
" [linear,univariate,equation,test]," ^
|
neuper@42290
|
119 |
" [Test,solve_linear]) " ^
|
neuper@42290
|
120 |
" [BOOL equ, REAL z]) " ^
|
neuper@42281
|
121 |
" in X)"
|
neuper@42256
|
122 |
));
|
neuper@42256
|
123 |
*}
|
neuper@42412
|
124 |
ML {*
|
neuper@42412
|
125 |
store_met(
|
neuper@42412
|
126 |
prep_met thy "met_SP_Ztrans_inv" [] e_metID
|
neuper@42412
|
127 |
(["SignalProcessing",
|
neuper@42412
|
128 |
"Z_Transform",
|
neuper@42412
|
129 |
"Inverse"],
|
neuper@42412
|
130 |
[
|
neuper@42412
|
131 |
("#Given" ,["filterExpression X_eq"]),
|
neuper@42412
|
132 |
("#Find" ,["stepResponse n_eq"])
|
neuper@42412
|
133 |
],
|
neuper@42412
|
134 |
{
|
neuper@42412
|
135 |
rew_ord'="tless_true",
|
neuper@42412
|
136 |
rls'= e_rls, calc = [],
|
neuper@42413
|
137 |
srls = srls_partial_fraction,
|
neuper@42412
|
138 |
prls = e_rls,
|
neuper@42425
|
139 |
crls = e_rls, errpats = [], nrls = e_rls
|
neuper@42412
|
140 |
},
|
neuper@42412
|
141 |
"Script InverseZTransform (X_eq::bool) = "^
|
neuper@42412
|
142 |
(*(1/z) instead of z ^^^ -1*)
|
neuper@42412
|
143 |
"(let X = Take X_eq; "^
|
neuper@42412
|
144 |
" X' = Rewrite ruleZY False X; "^
|
neuper@42412
|
145 |
(*z * denominator*)
|
neuper@42412
|
146 |
" (num_orig::real) = get_numerator (rhs X'); "^
|
neuper@42412
|
147 |
" X' = (Rewrite_Set norm_Rational False) X'; "^
|
neuper@42412
|
148 |
(*simplify*)
|
neuper@42412
|
149 |
" (X'_z::real) = lhs X'; "^
|
neuper@42412
|
150 |
" (zzz::real) = argument_in X'_z; "^
|
neuper@42412
|
151 |
" (funterm::real) = rhs X'; "^
|
neuper@42412
|
152 |
(*drop X' z = for equation solving*)
|
neuper@42412
|
153 |
" (denom::real) = get_denominator funterm; "^
|
neuper@42412
|
154 |
(*get_denominator*)
|
neuper@42412
|
155 |
" (num::real) = get_numerator funterm; "^
|
neuper@42412
|
156 |
(*get_numerator*)
|
neuper@42412
|
157 |
" (equ::bool) = (denom = (0::real)); "^
|
neuper@42412
|
158 |
" (L_L::bool list) = (SubProblem (PolyEq', "^
|
neuper@42412
|
159 |
" [abcFormula,degree_2,polynomial,univariate,equation], "^
|
neuper@42412
|
160 |
" [no_met]) "^
|
neuper@42412
|
161 |
" [BOOL equ, REAL zzz]); "^
|
neuper@42412
|
162 |
" (facs::real) = factors_from_solution L_L; "^
|
neuper@42412
|
163 |
" (eql::real) = Take (num_orig / facs); "^
|
neuper@42412
|
164 |
|
neuper@42412
|
165 |
" (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
|
neuper@42412
|
166 |
|
neuper@42412
|
167 |
" (eq::bool) = Take (eql = eqr); "^
|
neuper@42412
|
168 |
(*Maybe possible to use HOLogic.mk_eq ??*)
|
neuper@42412
|
169 |
" eq = (Try (Rewrite_Set equival_trans False)) eq; "^
|
neuper@42412
|
170 |
|
neuper@42412
|
171 |
" eq = drop_questionmarks eq; "^
|
neuper@42412
|
172 |
" (z1::real) = (rhs (NTH 1 L_L)); "^
|
neuper@42412
|
173 |
(*
|
neuper@42412
|
174 |
* prepare equation for a - eq_a
|
neuper@42412
|
175 |
* therefor substitute z with solution 1 - z1
|
neuper@42412
|
176 |
*)
|
neuper@42412
|
177 |
" (z2::real) = (rhs (NTH 2 L_L)); "^
|
neuper@42412
|
178 |
|
neuper@42412
|
179 |
" (eq_a::bool) = Take eq; "^
|
neuper@42412
|
180 |
" eq_a = (Substitute [zzz=z1]) eq; "^
|
neuper@42412
|
181 |
" eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
|
neuper@42412
|
182 |
" (sol_a::bool list) = "^
|
neuper@42412
|
183 |
" (SubProblem (Isac', "^
|
neuper@42412
|
184 |
" [univariate,equation],[no_met]) "^
|
neuper@42412
|
185 |
" [BOOL eq_a, REAL (A::real)]); "^
|
neuper@42412
|
186 |
" (a::real) = (rhs(NTH 1 sol_a)); "^
|
neuper@42412
|
187 |
|
neuper@42412
|
188 |
" (eq_b::bool) = Take eq; "^
|
neuper@42412
|
189 |
" eq_b = (Substitute [zzz=z2]) eq_b; "^
|
neuper@42412
|
190 |
" eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
|
neuper@42412
|
191 |
" (sol_b::bool list) = "^
|
neuper@42412
|
192 |
" (SubProblem (Isac', "^
|
neuper@42412
|
193 |
" [univariate,equation],[no_met]) "^
|
neuper@42412
|
194 |
" [BOOL eq_b, REAL (B::real)]); "^
|
neuper@42412
|
195 |
" (b::real) = (rhs(NTH 1 sol_b)); "^
|
neuper@42412
|
196 |
|
neuper@42412
|
197 |
" eqr = drop_questionmarks eqr; "^
|
neuper@42412
|
198 |
" (pbz::real) = Take eqr; "^
|
neuper@42412
|
199 |
" pbz = ((Substitute [A=a, B=b]) pbz); "^
|
neuper@42412
|
200 |
|
neuper@42412
|
201 |
" pbz = Rewrite ruleYZ False pbz; "^
|
neuper@42412
|
202 |
" pbz = drop_questionmarks pbz; "^
|
neuper@42412
|
203 |
|
neuper@42412
|
204 |
" (X_z::bool) = Take (X_z = pbz); "^
|
neuper@42412
|
205 |
" (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
|
neuper@42412
|
206 |
" n_eq = drop_questionmarks n_eq "^
|
neuper@42412
|
207 |
"in n_eq)"
|
neuper@42412
|
208 |
)
|
neuper@42412
|
209 |
);
|
neuper@42417
|
210 |
|
neuper@42417
|
211 |
store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
|
neuper@42417
|
212 |
(["SignalProcessing", "Z_Transform", "Inverse_sub"],
|
neuper@42417
|
213 |
[("#Given" ,["filterExpression X_eq"]),
|
neuper@42417
|
214 |
("#Find" ,["stepResponse n_eq"])],
|
neuper@42417
|
215 |
{rew_ord'="tless_true",
|
neuper@42417
|
216 |
rls'= e_rls, calc = [],
|
neuper@42417
|
217 |
srls = Rls {id="srls_partial_fraction",
|
neuper@42417
|
218 |
preconds = [],
|
neuper@42417
|
219 |
rew_ord = ("termlessI",termlessI),
|
neuper@42417
|
220 |
erls = append_rls "erls_in_srls_partial_fraction" e_rls
|
neuper@42417
|
221 |
[(*for asm in NTH_CONS ...*)
|
neuper@42417
|
222 |
Calc ("Orderings.ord_class.less",eval_equ "#less_"),
|
neuper@42417
|
223 |
(*2nd NTH_CONS pushes n+-1 into asms*)
|
neuper@42417
|
224 |
Calc("Groups.plus_class.plus", eval_binop "#add_")],
|
neuper@42451
|
225 |
srls = Erls, calc = [], errpatts = [],
|
neuper@42417
|
226 |
rules = [
|
neuper@42417
|
227 |
Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
|
neuper@42417
|
228 |
Calc("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@42417
|
229 |
Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
|
neuper@42417
|
230 |
Calc("Tools.lhs", eval_lhs "eval_lhs_"),
|
neuper@42417
|
231 |
Calc("Tools.rhs", eval_rhs"eval_rhs_"),
|
neuper@42417
|
232 |
Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
|
neuper@42417
|
233 |
Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
|
neuper@42417
|
234 |
Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
|
neuper@42417
|
235 |
Calc("Partial_Fractions.factors_from_solution",
|
neuper@42417
|
236 |
eval_factors_from_solution "#factors_from_solution"),
|
neuper@42417
|
237 |
Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
|
neuper@42417
|
238 |
scr = EmptyScr},
|
neuper@42425
|
239 |
prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
|
neuper@42417
|
240 |
"Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
neuper@42417
|
241 |
"(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
neuper@42417
|
242 |
" X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42417
|
243 |
" (X'_z::real) = lhs X'; "^(* ?X' z*)
|
neuper@42417
|
244 |
" (zzz::real) = argument_in X'_z; "^(* z *)
|
neuper@42417
|
245 |
" (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
neuper@42417
|
246 |
|
neuper@42417
|
247 |
" (pbz::real) = (SubProblem (Isac', "^(**)
|
neuper@42417
|
248 |
" [partial_fraction,rational,simplification], "^
|
neuper@42417
|
249 |
" [simplification,of_rationals,to_partial_fraction]) "^
|
neuper@42421
|
250 |
" [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42417
|
251 |
|
neuper@42421
|
252 |
" (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
neuper@42421
|
253 |
" pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
neuper@42421
|
254 |
" pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42421
|
255 |
" (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
neuper@42421
|
256 |
" 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]*)
|
neuper@42421
|
257 |
" n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42417
|
258 |
"in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
neuper@42417
|
259 |
));
|
neuper@42417
|
260 |
|
neuper@42412
|
261 |
*}
|
neuper@42256
|
262 |
|
neuper@42256
|
263 |
end
|
neuper@42256
|
264 |
|