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 |
*)
|
neuper@42256
|
5 |
|
neuper@42290
|
6 |
theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
|
neuper@42256
|
7 |
|
neuper@42256
|
8 |
axiomatization where
|
neuper@42256
|
9 |
rule1: "1 = \<delta>[n]" and
|
neuper@42256
|
10 |
rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
|
neuper@42256
|
11 |
rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
|
jan@42367
|
12 |
rule4: "c * (z / (z - \<alpha>)) = c * \<alpha>^^^n * u [n]" and
|
neuper@42256
|
13 |
rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
|
jan@42367
|
14 |
rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and
|
jan@42367
|
15 |
rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
|
neuper@42256
|
16 |
|
neuper@42256
|
17 |
axiomatization where
|
wneuper@59537
|
18 |
(*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))" ..looks better, but types are flawed*)
|
jan@42367
|
19 |
ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
|
wneuper@59537
|
20 |
ruleYZ: "a / (z - b) + c / (z - d) = a * (z / (z - b)) + c * (z / (z - d))" and
|
wneuper@59537
|
21 |
ruleYZa: "(a / b + c / d) = (a * (z / b) + c * (z / d))" \<comment> \<open>that is what students learn\<close>
|
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 |
|
wneuper@59472
|
28 |
ML \<open>
|
s1210629013@55444
|
29 |
val inverse_z = prep_rls'(
|
wneuper@59416
|
30 |
Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
|
wneuper@59416
|
31 |
erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
|
jan@42366
|
32 |
rules =
|
jan@42367
|
33 |
[
|
wneuper@59416
|
34 |
Rule.Thm ("rule4", @{thm rule4})
|
jan@42366
|
35 |
],
|
wneuper@59416
|
36 |
scr = Rule.EmptyScr});
|
wneuper@59472
|
37 |
\<close>
|
jan@42366
|
38 |
|
jan@42366
|
39 |
|
wneuper@59472
|
40 |
text \<open>store the rule set for math engine\<close>
|
jan@42366
|
41 |
|
wneuper@59472
|
42 |
setup \<open>KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))]\<close>
|
jan@42366
|
43 |
|
wneuper@59472
|
44 |
subsection\<open>Define the Specification\<close>
|
wneuper@59472
|
45 |
ML \<open>
|
neuper@42256
|
46 |
val thy = @{theory};
|
wneuper@59472
|
47 |
\<close>
|
wneuper@59472
|
48 |
setup \<open>KEStore_Elems.add_pbts
|
wneuper@59416
|
49 |
[(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])),
|
wneuper@59406
|
50 |
(Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
|
wneuper@59416
|
51 |
(["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
|
wneuper@59406
|
52 |
(Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
|
s1210629013@55339
|
53 |
(["Inverse", "Z_Transform", "SignalProcessing"],
|
s1210629013@55339
|
54 |
[("#Given" ,["filterExpression X_eq"]),
|
s1210629013@55339
|
55 |
("#Find" ,["stepResponse n_eq"])],
|
wneuper@59416
|
56 |
Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
|
wneuper@59538
|
57 |
[["SignalProcessing","Z_Transform","Inverse"]])),
|
wneuper@59538
|
58 |
(Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID
|
wneuper@59538
|
59 |
(["Inverse_sub", "Z_Transform", "SignalProcessing"],
|
wneuper@59538
|
60 |
[("#Given" ,["filterExpression X_eq"]),
|
wneuper@59538
|
61 |
("#Find" ,["stepResponse n_eq"])],
|
wneuper@59538
|
62 |
Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
|
wneuper@59538
|
63 |
[["SignalProcessing","Z_Transform","Inverse_sub"]]))]\<close>
|
neuper@42256
|
64 |
|
wneuper@59472
|
65 |
subsection \<open>Define Name and Signature for the Method\<close>
|
neuper@42256
|
66 |
consts
|
wneuper@59538
|
67 |
InverseZTransform1 :: "[bool, bool] => bool"
|
wneuper@59538
|
68 |
("((Script InverseZTransform1 (_ =))// (_))" 9)
|
wneuper@59538
|
69 |
InverseZTransform2 :: "[bool, real, bool] => bool"
|
wneuper@59538
|
70 |
("((Script InverseZTransform2 (_ _ =))// (_))" 9)
|
neuper@42256
|
71 |
|
wneuper@59472
|
72 |
subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
|
wneuper@59472
|
73 |
ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
|
wneuper@59472
|
74 |
setup \<open>KEStore_Elems.add_mets
|
wneuper@59473
|
75 |
[Specify.prep_met thy "met_SP" [] Celem.e_metID
|
s1210629013@55373
|
76 |
(["SignalProcessing"], [],
|
wneuper@59416
|
77 |
{rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
|
wneuper@59416
|
78 |
errpats = [], nrls = Rule.e_rls}, "empty_script"),
|
wneuper@59406
|
79 |
Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
|
s1210629013@55373
|
80 |
(["SignalProcessing", "Z_Transform"], [],
|
wneuper@59416
|
81 |
{rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
|
wneuper@59473
|
82 |
errpats = [], nrls = Rule.e_rls}, "empty_script")]
|
wneuper@59473
|
83 |
\<close>
|
wneuper@59505
|
84 |
(*ok
|
wneuper@59504
|
85 |
partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool"
|
wneuper@59504
|
86 |
where
|
wneuper@59504
|
87 |
"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
|
wneuper@59504
|
88 |
(let X = Take X_eq;
|
wneuper@59504
|
89 |
X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
|
wneuper@59504
|
90 |
X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
|
wneuper@59504
|
91 |
funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
|
wneuper@59504
|
92 |
denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
|
wneuper@59504
|
93 |
equ = (denom = (0::real));
|
wneuper@59504
|
94 |
fun_arg = Take (lhs X');
|
wneuper@59504
|
95 |
arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
|
wneuper@59504
|
96 |
L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
|
wneuper@59537
|
97 |
[''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG --> as arg\<close>
|
wneuper@59504
|
98 |
in X) "
|
wneuper@59505
|
99 |
*)
|
wneuper@59473
|
100 |
setup \<open>KEStore_Elems.add_mets
|
wneuper@59473
|
101 |
[Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
|
wneuper@59538
|
102 |
(["SignalProcessing", "Z_Transform", "Inverse"],
|
s1210629013@55373
|
103 |
[("#Given" ,["filterExpression (X_eq::bool)"]),
|
s1210629013@55373
|
104 |
("#Find" ,["stepResponse (n_eq::bool)"])],
|
wneuper@59416
|
105 |
{rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
|
wneuper@59416
|
106 |
errpats = [], nrls = Rule.e_rls},
|
wneuper@59538
|
107 |
"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
|
s1210629013@55373
|
108 |
" (let X = Take X_eq;" ^
|
wneuper@59489
|
109 |
" X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
|
wneuper@59489
|
110 |
" X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
|
s1210629013@55373
|
111 |
" funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
|
wneuper@59489
|
112 |
" denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*)
|
s1210629013@55373
|
113 |
" equ = (denom = (0::real));" ^
|
s1210629013@55373
|
114 |
" fun_arg = Take (lhs X');" ^
|
wneuper@59489
|
115 |
" arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*)
|
s1210629013@55373
|
116 |
" (L_L::bool list) = " ^
|
wneuper@59489
|
117 |
" (SubProblem (''Test'', " ^
|
wneuper@59489
|
118 |
" [''LINEAR'',''univariate'',''equation'',''test'']," ^
|
wneuper@59489
|
119 |
" [''Test'',''solve_linear'']) " ^
|
s1210629013@55373
|
120 |
" [BOOL equ, REAL z]) " ^
|
wneuper@59473
|
121 |
" in X)")]
|
wneuper@59473
|
122 |
\<close>
|
wneuper@59538
|
123 |
|
wneuper@59538
|
124 |
(* ok
|
wneuper@59538
|
125 |
partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
|
wneuper@59504
|
126 |
where
|
wneuper@59538
|
127 |
"inverse_ztransform2 X_eq X_z =
|
wneuper@59504
|
128 |
(let X = Take X_eq;
|
wneuper@59538
|
129 |
X' = Rewrite ''ruleZY'' False X;
|
wneuper@59538
|
130 |
X'_z = lhs X';
|
wneuper@59538
|
131 |
zzz = argument_in X'_z;
|
wneuper@59538
|
132 |
funterm = rhs X';
|
wneuper@59538
|
133 |
pbz = SubProblem (''Isac'',
|
wneuper@59538
|
134 |
[''partial_fraction'',''rational'',''simplification''],
|
wneuper@59538
|
135 |
[''simplification'',''of_rationals'',''to_partial_fraction''])
|
wneuper@59538
|
136 |
[REAL funterm, REAL zzz];
|
wneuper@59538
|
137 |
pbz_eq = Take (X'_z = pbz);
|
wneuper@59538
|
138 |
pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
|
wneuper@59538
|
139 |
X_zeq = Take (X_z = rhs pbz_eq);
|
wneuper@59538
|
140 |
n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
|
wneuper@59538
|
141 |
in n_eq)"
|
wneuper@59504
|
142 |
*)
|
wneuper@59473
|
143 |
setup \<open>KEStore_Elems.add_mets
|
wneuper@59473
|
144 |
[Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
|
wneuper@59538
|
145 |
(["SignalProcessing", "Z_Transform", "Inverse_sub"],
|
wneuper@59538
|
146 |
[("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
|
s1210629013@55373
|
147 |
("#Find" ,["stepResponse n_eq"])],
|
wneuper@59416
|
148 |
{rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
|
wneuper@59416
|
149 |
srls = Rule.Rls {id="srls_partial_fraction",
|
s1210629013@55373
|
150 |
preconds = [], rew_ord = ("termlessI",termlessI),
|
wneuper@59416
|
151 |
erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls
|
s1210629013@55373
|
152 |
[(*for asm in NTH_CONS ...*)
|
wneuper@59416
|
153 |
Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
|
s1210629013@55373
|
154 |
(*2nd NTH_CONS pushes n+-1 into asms*)
|
wneuper@59416
|
155 |
Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")],
|
wneuper@59416
|
156 |
srls = Rule.Erls, calc = [], errpatts = [],
|
wneuper@59416
|
157 |
rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
|
wneuper@59416
|
158 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
159 |
Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
|
wneuper@59491
|
160 |
Rule.Calc ("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
|
wneuper@59491
|
161 |
Rule.Calc ("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
|
wneuper@59416
|
162 |
Rule.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
|
wneuper@59416
|
163 |
Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
|
wneuper@59416
|
164 |
Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
|
wneuper@59416
|
165 |
Rule.Calc ("Partial_Fractions.factors_from_solution",
|
wneuper@59512
|
166 |
eval_factors_from_solution "#factors_from_solution")
|
wneuper@59512
|
167 |
], scr = Rule.EmptyScr},
|
wneuper@59416
|
168 |
prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
|
wneuper@59538
|
169 |
" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
|
wneuper@59538
|
170 |
" (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
|
wneuper@59538
|
171 |
" X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
wneuper@59538
|
172 |
" (X'_z::real) = lhs X'; "^ (* ?X' z*)
|
wneuper@59538
|
173 |
" (zzz::real) = argument_in X'_z; "^ (* z *)
|
wneuper@59538
|
174 |
" (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
|
wneuper@59538
|
175 |
" (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
wneuper@59538
|
176 |
" [''partial_fraction'',''rational'',''simplification''], "^
|
wneuper@59538
|
177 |
" [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
|
wneuper@59538
|
178 |
" [REAL funterm, REAL zzz]); "^
|
wneuper@59538
|
179 |
" (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
|
wneuper@59538
|
180 |
" pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
|
wneuper@59538
|
181 |
" (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
|
wneuper@59538
|
182 |
" 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]*)
|
wneuper@59538
|
183 |
" in n_eq) ")](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
|
wneuper@59472
|
184 |
\<close>
|
neuper@42256
|
185 |
|
neuper@42256
|
186 |
end
|
neuper@42256
|
187 |
|