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
|
neuper@42256
|
14 |
rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
|
neuper@42256
|
15 |
rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
|
neuper@42256
|
16 |
rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
|
neuper@42256
|
17 |
|
neuper@42256
|
18 |
axiomatization where
|
jan@42366
|
19 |
ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
|
neuper@42256
|
20 |
|
neuper@42279
|
21 |
subsection{*Define the Field Descriptions for the specification*}
|
neuper@42279
|
22 |
consts
|
neuper@42279
|
23 |
filterExpression :: "bool => una"
|
neuper@42279
|
24 |
stepResponse :: "bool => una"
|
neuper@42279
|
25 |
|
jan@42366
|
26 |
|
jan@42366
|
27 |
ML {*
|
jan@42366
|
28 |
val inverse_z = prep_rls(
|
jan@42366
|
29 |
Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
jan@42366
|
30 |
erls = Erls, srls = Erls, calc = [],
|
jan@42366
|
31 |
rules =
|
jan@42366
|
32 |
[Thm ("rule1",num_str @{thm rule1}),
|
jan@42366
|
33 |
Thm ("rule2",num_str @{thm rule2}),
|
jan@42366
|
34 |
Thm ("rule3",num_str @{thm rule3}),
|
jan@42366
|
35 |
Thm ("rule4",num_str @{thm rule4}),
|
jan@42366
|
36 |
Thm ("rule5",num_str @{thm rule5}),
|
jan@42366
|
37 |
Thm ("rule6",num_str @{thm rule6})
|
jan@42366
|
38 |
],
|
jan@42366
|
39 |
scr = EmptyScr}:rls);
|
jan@42366
|
40 |
*}
|
jan@42366
|
41 |
|
jan@42366
|
42 |
|
jan@42366
|
43 |
text {*store the rule set for math engine*}
|
jan@42366
|
44 |
|
jan@42366
|
45 |
ML {*
|
jan@42366
|
46 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
jan@42366
|
47 |
[("inverse_z", inverse_z)
|
jan@42366
|
48 |
]);
|
jan@42366
|
49 |
*}
|
jan@42366
|
50 |
|
neuper@42256
|
51 |
subsection{*Define the Specification*}
|
neuper@42256
|
52 |
ML {*
|
neuper@42256
|
53 |
val thy = @{theory};
|
neuper@42278
|
54 |
|
neuper@42256
|
55 |
store_pbt
|
neuper@42256
|
56 |
(prep_pbt thy "pbl_SP" [] e_pblID
|
neuper@42256
|
57 |
(["SignalProcessing"], [], e_rls, NONE, []));
|
neuper@42256
|
58 |
store_pbt
|
neuper@42256
|
59 |
(prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
|
neuper@42256
|
60 |
(["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
|
neuper@42256
|
61 |
store_pbt
|
neuper@42256
|
62 |
(prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
|
neuper@42256
|
63 |
(["inverse", "Z_Transform", "SignalProcessing"],
|
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@42277
|
68 |
[["SignalProcessing","Z_Transform","inverse"]]));
|
neuper@42256
|
69 |
*}
|
neuper@42256
|
70 |
|
neuper@42256
|
71 |
subsection {*Define Name and Signature for the Method*}
|
neuper@42256
|
72 |
consts
|
neuper@42256
|
73 |
InverseZTransform :: "[bool, bool] => bool"
|
neuper@42256
|
74 |
("((Script InverseZTransform (_ =))// (_))" 9)
|
neuper@42256
|
75 |
|
neuper@42277
|
76 |
subsection {*Setup Parent Nodes in Hierarchy of Method*}
|
neuper@42256
|
77 |
ML {*
|
neuper@42256
|
78 |
store_met
|
neuper@42256
|
79 |
(prep_met thy "met_SP" [] e_metID
|
neuper@42256
|
80 |
(["SignalProcessing"], [],
|
neuper@42256
|
81 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42256
|
82 |
crls = e_rls, nrls = e_rls}, "empty_script"));
|
neuper@42256
|
83 |
store_met
|
neuper@42256
|
84 |
(prep_met thy "met_SP_Ztrans" [] e_metID
|
neuper@42256
|
85 |
(["SignalProcessing", "Z_Transform"], [],
|
neuper@42256
|
86 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42256
|
87 |
crls = e_rls, nrls = e_rls}, "empty_script"));
|
neuper@42256
|
88 |
val thy = @{theory}; (*latest version of thy required*)
|
neuper@42256
|
89 |
store_met
|
neuper@42256
|
90 |
(prep_met thy "met_SP_Ztrans_inv" [] e_metID
|
neuper@42256
|
91 |
(["SignalProcessing", "Z_Transform", "inverse"],
|
neuper@42278
|
92 |
[("#Given" ,["filterExpression (X_eq::bool)"]),
|
neuper@42278
|
93 |
("#Find" ,["stepResponse (n_eq::bool)"])
|
neuper@42256
|
94 |
],
|
neuper@42256
|
95 |
{rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
|
neuper@42256
|
96 |
crls = e_rls, nrls = e_rls},
|
neuper@42281
|
97 |
"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
|
neuper@42281
|
98 |
" (let X = Take X_eq;" ^
|
neuper@42281
|
99 |
" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
|
neuper@42281
|
100 |
" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
|
neuper@42290
|
101 |
" funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
|
neuper@42290
|
102 |
" denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
|
neuper@42290
|
103 |
" equ = (denom = (0::real));" ^
|
neuper@42290
|
104 |
" fun_arg = Take (lhs X');" ^
|
neuper@42290
|
105 |
" arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
|
neuper@42290
|
106 |
" (L_L::bool list) = " ^
|
neuper@42290
|
107 |
" (SubProblem (Test', " ^
|
neuper@42290
|
108 |
" [linear,univariate,equation,test]," ^
|
neuper@42290
|
109 |
" [Test,solve_linear]) " ^
|
neuper@42290
|
110 |
" [BOOL equ, REAL z]) " ^
|
neuper@42281
|
111 |
" in X)"
|
neuper@42256
|
112 |
));
|
neuper@42256
|
113 |
*}
|
neuper@42256
|
114 |
|
neuper@42256
|
115 |
end
|
neuper@42256
|
116 |
|