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 |
[
|
wneuper@59416
|
34 |
Rule.Thm ("rule4", @{thm rule4})
|
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@60286
|
42 |
setup_rule inverse_z = inverse_z
|
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
|
walther@59973
|
49 |
[(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
|
walther@59973
|
50 |
(Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
|
walther@59997
|
51 |
(["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
|
walther@59973
|
52 |
(Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
|
s1210629013@55339
|
53 |
(["Inverse", "Z_Transform", "SignalProcessing"],
|
wneuper@59550
|
54 |
[("#Given" , ["filterExpression X_eq"]),
|
wneuper@59550
|
55 |
("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
walther@59852
|
56 |
Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE,
|
walther@59997
|
57 |
[["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
|
neuper@42256
|
58 |
|
walther@60154
|
59 |
subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
|
wneuper@59472
|
60 |
ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
|
wneuper@59472
|
61 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
62 |
[MethodC.prep_input thy "met_SP" [] MethodC.id_empty
|
s1210629013@55373
|
63 |
(["SignalProcessing"], [],
|
walther@59852
|
64 |
{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
walther@59852
|
65 |
errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
|
walther@60154
|
66 |
MethodC.prep_input thy "met_SP_Ztrans" [] MethodC.id_empty
|
s1210629013@55373
|
67 |
(["SignalProcessing", "Z_Transform"], [],
|
walther@59852
|
68 |
{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
walther@59852
|
69 |
errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
|
wneuper@59473
|
70 |
\<close>
|
wneuper@59545
|
71 |
|
wneuper@59545
|
72 |
partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
|
wneuper@59504
|
73 |
where
|
walther@59635
|
74 |
"inverse_ztransform X_eq X_z = (
|
walther@59635
|
75 |
let
|
walther@59635
|
76 |
X = Take X_eq;
|
walther@59635
|
77 |
X' = Rewrite ''ruleZY'' X; \<comment> \<open>z * denominator\<close>
|
walther@59635
|
78 |
X' = (Rewrite_Set ''norm_Rational'' ) X'; \<comment> \<open>simplify\<close>
|
walther@59635
|
79 |
funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
|
walther@59635
|
80 |
denom = (Rewrite_Set ''partial_fraction'' ) funterm; \<comment> \<open>get_denominator\<close>
|
walther@59635
|
81 |
equ = (denom = (0::real));
|
walther@59635
|
82 |
fun_arg = Take (lhs X');
|
walther@59635
|
83 |
arg = (Rewrite_Set ''partial_fraction'' ) X'; \<comment> \<open>get_argument TODO\<close>
|
walther@59635
|
84 |
(L_L::bool list) = \<comment> \<open>'bool list' inhibits:
|
walther@59635
|
85 |
WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
|
walther@59635
|
86 |
SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
|
walther@59635
|
87 |
[BOOL equ, REAL X_z]
|
wneuper@59504
|
88 |
in X) "
|
wneuper@59473
|
89 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
90 |
[MethodC.prep_input thy "met_SP_Ztrans_inv" [] MethodC.id_empty
|
wneuper@59538
|
91 |
(["SignalProcessing", "Z_Transform", "Inverse"],
|
wneuper@59550
|
92 |
[("#Given" ,["filterExpression X_eq", "functionName X_z"]),
|
wneuper@59550
|
93 |
("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
walther@59852
|
94 |
{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
|
walther@59852
|
95 |
errpats = [], nrls = Rule_Set.empty},
|
wneuper@59551
|
96 |
@{thm inverse_ztransform.simps})]
|
wneuper@59473
|
97 |
\<close>
|
wneuper@59538
|
98 |
|
wneuper@59538
|
99 |
partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
|
wneuper@59504
|
100 |
where
|
walther@59635
|
101 |
"inverse_ztransform2 X_eq X_z = (
|
walther@59635
|
102 |
let
|
walther@59635
|
103 |
X = Take X_eq;
|
walther@59635
|
104 |
X' = Rewrite ''ruleZY'' X;
|
walther@60278
|
105 |
X_z = lhs X';
|
walther@60278
|
106 |
zzz = argument_in X_z;
|
wneuper@59538
|
107 |
funterm = rhs X';
|
wneuper@59592
|
108 |
pbz = SubProblem (''Isac_Knowledge'',
|
walther@59635
|
109 |
[''partial_fraction'',''rational'',''simplification''],
|
walther@59635
|
110 |
[''simplification'',''of_rationals'',''to_partial_fraction''])
|
wneuper@59538
|
111 |
[REAL funterm, REAL zzz];
|
walther@60278
|
112 |
pbz_eq = Take (X_z = pbz);
|
walther@59635
|
113 |
pbz_eq = Rewrite ''ruleYZ'' pbz_eq;
|
wneuper@59538
|
114 |
X_zeq = Take (X_z = rhs pbz_eq);
|
walther@59635
|
115 |
n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
|
wneuper@59538
|
116 |
in n_eq)"
|
wneuper@59473
|
117 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
118 |
[MethodC.prep_input thy "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
|
wneuper@59538
|
119 |
(["SignalProcessing", "Z_Transform", "Inverse_sub"],
|
wneuper@59550
|
120 |
[("#Given" ,["filterExpression X_eq", "functionName X_z"]),
|
wneuper@59550
|
121 |
("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
|
walther@59852
|
122 |
{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
|
walther@59851
|
123 |
srls = Rule_Def.Repeat {id="srls_partial_fraction",
|
s1210629013@55373
|
124 |
preconds = [], rew_ord = ("termlessI",termlessI),
|
walther@59852
|
125 |
erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
|
s1210629013@55373
|
126 |
[(*for asm in NTH_CONS ...*)
|
walther@59878
|
127 |
Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
|
s1210629013@55373
|
128 |
(*2nd NTH_CONS pushes n+-1 into asms*)
|
walther@59878
|
129 |
Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")],
|
walther@59851
|
130 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
wneuper@59416
|
131 |
rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
|
walther@59878
|
132 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
wneuper@59416
|
133 |
Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
|
walther@59878
|
134 |
Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
|
walther@59878
|
135 |
Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
|
walther@60278
|
136 |
Rule.Eval ("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
|
walther@59878
|
137 |
Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
|
walther@59878
|
138 |
Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
|
walther@59878
|
139 |
Rule.Eval ("Partial_Fractions.factors_from_solution",
|
wneuper@59512
|
140 |
eval_factors_from_solution "#factors_from_solution")
|
walther@59878
|
141 |
], scr = Rule.Empty_Prog},
|
walther@59852
|
142 |
prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
|
wneuper@59551
|
143 |
@{thm inverse_ztransform2.simps})]
|
wneuper@59472
|
144 |
\<close>
|
wneuper@59550
|
145 |
ML \<open>
|
wneuper@59550
|
146 |
\<close> ML \<open>
|
walther@60278
|
147 |
\<close> ML \<open>
|
wneuper@59550
|
148 |
\<close>
|
neuper@42256
|
149 |
|
neuper@42256
|
150 |
end
|
neuper@42256
|
151 |
|