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