wneuper@59550
|
1 |
(* Title: Inverse_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 |
|
wneuper@59550
|
8 |
axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close>
|
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
|
walther@60242
|
12 |
rule4: "c * (z / (z - \<alpha>)) = c * \<alpha> \<up> n * u [n]" and
|
walther@60242
|
13 |
rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
|
walther@60242
|
14 |
rule6: "|| z || > 1 ==> z/(z - 1) \<up> 2 = n * u [n]" (*and
|
walther@60242
|
15 |
rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b \<up> n * u [n] + c * d \<up> 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"
|
wneuper@59550
|
26 |
stepResponse :: "bool => una" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close>
|
neuper@42279
|
27 |
|
wneuper@59472
|
28 |
ML \<open>
|
s1210629013@55444
|
29 |
val inverse_z = prep_rls'(
|
walther@59857
|
30 |
Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@59851
|
31 |
erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
jan@42366
|
32 |
rules =
|
jan@42367
|
33 |
[
|
wenzelm@60298
|
34 |
\<^rule_thm>\<open>rule4\<close>
|
jan@42366
|
35 |
],
|
walther@59878
|
36 |
scr = Rule.Empty_Prog});
|
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 |
|
wenzelm@60289
|
42 |
rule_set_knowledge inverse_z = inverse_z
|
jan@42366
|
43 |
|
wneuper@59472
|
44 |
subsection\<open>Define the Specification\<close>
|
wenzelm@60291
|
45 |
|
wenzelm@60306
|
46 |
problem pbl_SP : "SignalProcessing" = \<open>Rule_Set.empty\<close>
|
wenzelm@60306
|
47 |
|
wenzelm@60306
|
48 |
problem pbl_SP_Ztrans : "Z_Transform/SignalProcessing" = \<open>Rule_Set.empty\<close>
|
wenzelm@60306
|
49 |
|
wenzelm@60306
|
50 |
problem pbl_SP_Ztrans_inv : "Inverse/Z_Transform/SignalProcessing" =
|
wenzelm@60306
|
51 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
wenzelm@60306
|
52 |
Method: "SignalProcessing/Z_Transform/Inverse"
|
wenzelm@60306
|
53 |
Given: "filterExpression X_eq"
|
wenzelm@60306
|
54 |
Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
wenzelm@60306
|
55 |
|
neuper@42256
|
56 |
|
walther@60154
|
57 |
subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
|
wenzelm@60290
|
58 |
|
wenzelm@60303
|
59 |
method met_SP : "SignalProcessing" =
|
wenzelm@60303
|
60 |
\<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
wenzelm@60303
|
61 |
errpats = [], nrls = Rule_Set.empty}\<close>
|
wenzelm@60303
|
62 |
|
wenzelm@60303
|
63 |
method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
|
wenzelm@60303
|
64 |
\<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
wenzelm@60303
|
65 |
errpats = [], nrls = Rule_Set.empty}\<close>
|
wneuper@59545
|
66 |
|
wneuper@59545
|
67 |
partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
|
wneuper@59504
|
68 |
where
|
walther@59635
|
69 |
"inverse_ztransform X_eq X_z = (
|
walther@59635
|
70 |
let
|
walther@59635
|
71 |
X = Take X_eq;
|
walther@59635
|
72 |
X' = Rewrite ''ruleZY'' X; \<comment> \<open>z * denominator\<close>
|
walther@59635
|
73 |
X' = (Rewrite_Set ''norm_Rational'' ) X'; \<comment> \<open>simplify\<close>
|
walther@59635
|
74 |
funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
|
walther@59635
|
75 |
denom = (Rewrite_Set ''partial_fraction'' ) funterm; \<comment> \<open>get_denominator\<close>
|
walther@59635
|
76 |
equ = (denom = (0::real));
|
walther@59635
|
77 |
fun_arg = Take (lhs X');
|
walther@59635
|
78 |
arg = (Rewrite_Set ''partial_fraction'' ) X'; \<comment> \<open>get_argument TODO\<close>
|
walther@59635
|
79 |
(L_L::bool list) = \<comment> \<open>'bool list' inhibits:
|
walther@59635
|
80 |
WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
|
walther@59635
|
81 |
SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
|
walther@59635
|
82 |
[BOOL equ, REAL X_z]
|
wneuper@59504
|
83 |
in X) "
|
wenzelm@60303
|
84 |
|
wenzelm@60303
|
85 |
method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
|
wenzelm@60303
|
86 |
\<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
wenzelm@60303
|
87 |
errpats = [], nrls = Rule_Set.empty}\<close>
|
wenzelm@60303
|
88 |
Program: inverse_ztransform.simps
|
wenzelm@60303
|
89 |
Given: "filterExpression X_eq" "functionName X_z"
|
wenzelm@60303
|
90 |
Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
wneuper@59538
|
91 |
|
wneuper@59538
|
92 |
partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
|
wneuper@59504
|
93 |
where
|
walther@59635
|
94 |
"inverse_ztransform2 X_eq X_z = (
|
walther@59635
|
95 |
let
|
walther@59635
|
96 |
X = Take X_eq;
|
walther@59635
|
97 |
X' = Rewrite ''ruleZY'' X;
|
walther@60278
|
98 |
X_z = lhs X';
|
walther@60278
|
99 |
zzz = argument_in X_z;
|
wneuper@59538
|
100 |
funterm = rhs X';
|
wneuper@59592
|
101 |
pbz = SubProblem (''Isac_Knowledge'',
|
walther@59635
|
102 |
[''partial_fraction'',''rational'',''simplification''],
|
walther@59635
|
103 |
[''simplification'',''of_rationals'',''to_partial_fraction''])
|
wneuper@59538
|
104 |
[REAL funterm, REAL zzz];
|
walther@60278
|
105 |
pbz_eq = Take (X_z = pbz);
|
walther@59635
|
106 |
pbz_eq = Rewrite ''ruleYZ'' pbz_eq;
|
wneuper@59538
|
107 |
X_zeq = Take (X_z = rhs pbz_eq);
|
walther@59635
|
108 |
n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
|
wneuper@59538
|
109 |
in n_eq)"
|
wenzelm@60303
|
110 |
|
wenzelm@60303
|
111 |
method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
|
wenzelm@60303
|
112 |
\<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
|
wenzelm@60303
|
113 |
srls = Rule_Def.Repeat {id="srls_partial_fraction",
|
wenzelm@60303
|
114 |
preconds = [], rew_ord = ("termlessI",termlessI),
|
wenzelm@60303
|
115 |
erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
|
wenzelm@60303
|
116 |
[(*for asm in NTH_CONS ...*)
|
wenzelm@60303
|
117 |
\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
|
wenzelm@60303
|
118 |
(*2nd NTH_CONS pushes n+-1 into asms*)
|
wenzelm@60303
|
119 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
|
wenzelm@60303
|
120 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
wenzelm@60303
|
121 |
rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
|
wenzelm@60303
|
122 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
wenzelm@60303
|
123 |
\<^rule_thm>\<open>NTH_NIL\<close>,
|
wenzelm@60303
|
124 |
\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
|
wenzelm@60303
|
125 |
\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
|
wenzelm@60303
|
126 |
\<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
|
wenzelm@60303
|
127 |
\<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
|
wenzelm@60303
|
128 |
\<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
|
wenzelm@60303
|
129 |
\<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
|
wenzelm@60303
|
130 |
], scr = Rule.Empty_Prog},
|
wenzelm@60303
|
131 |
prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
|
wenzelm@60303
|
132 |
Program: inverse_ztransform2.simps
|
wenzelm@60303
|
133 |
Given: "filterExpression X_eq" "functionName X_z"
|
wenzelm@60303
|
134 |
Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
wenzelm@60303
|
135 |
|
wneuper@59550
|
136 |
ML \<open>
|
wneuper@59550
|
137 |
\<close> ML \<open>
|
walther@60278
|
138 |
\<close> ML \<open>
|
wneuper@59550
|
139 |
\<close>
|
neuper@42256
|
140 |
|
neuper@42256
|
141 |
end
|
neuper@42256
|
142 |
|