73 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close> |
73 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close> |
74 setup \<open>KEStore_Elems.add_mets |
74 setup \<open>KEStore_Elems.add_mets |
75 [Specify.prep_met thy "met_SP" [] Celem.e_metID |
75 [Specify.prep_met thy "met_SP" [] Celem.e_metID |
76 (["SignalProcessing"], [], |
76 (["SignalProcessing"], [], |
77 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
77 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
78 errpats = [], nrls = Rule.e_rls}, "empty_script"), |
78 errpats = [], nrls = Rule.e_rls}, @{thm refl}), |
79 Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID |
79 Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID |
80 (["SignalProcessing", "Z_Transform"], [], |
80 (["SignalProcessing", "Z_Transform"], [], |
81 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
81 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
82 errpats = [], nrls = Rule.e_rls}, "empty_script")] |
82 errpats = [], nrls = Rule.e_rls}, @{thm refl})] |
83 \<close> |
83 \<close> |
84 (*ok |
84 |
85 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool" |
85 (*WARNING: Additional type variable(s) in specification of "inverse_ztransform": 'a *) |
|
86 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool" |
86 where |
87 where |
87 "inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close> |
88 "inverse_ztransform X_eq z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close> |
88 (let X = Take X_eq; |
89 (let X = Take X_eq; |
89 X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close> |
90 X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close> |
90 X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close> |
91 X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close> |
91 funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close> |
92 funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close> |
92 denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close> |
93 denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close> |
94 fun_arg = Take (lhs X'); |
95 fun_arg = Take (lhs X'); |
95 arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close> |
96 arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close> |
96 L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], |
97 L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], |
97 [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG string\<close> |
98 [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG string\<close> |
98 in X) " |
99 in X) " |
99 *) |
|
100 setup \<open>KEStore_Elems.add_mets |
100 setup \<open>KEStore_Elems.add_mets |
101 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID |
101 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID |
102 (["SignalProcessing", "Z_Transform", "Inverse"], |
102 (["SignalProcessing", "Z_Transform", "Inverse"], |
103 [("#Given" ,["filterExpression (X_eq::bool)"]), |
103 [("#Given" ,["filterExpression (X_eq::bool)"]), |
104 ("#Find" ,["stepResponse (n_eq::bool)"])], |
104 ("#Find" ,["stepResponse (n_eq::bool)"])], |
105 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
105 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, |
106 errpats = [], nrls = Rule.e_rls}, |
106 errpats = [], nrls = Rule.e_rls}, |
107 "Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
107 @{thm inverse_ztransform.simps} |
|
108 (*"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
108 " (let X = Take X_eq;" ^ |
109 " (let X = Take X_eq;" ^ |
109 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) |
110 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) |
110 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) |
111 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) |
111 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
112 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
112 " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) |
113 " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) |
116 " (L_L::bool list) = " ^ |
117 " (L_L::bool list) = " ^ |
117 " (SubProblem (''Test'', " ^ |
118 " (SubProblem (''Test'', " ^ |
118 " [''LINEAR'',''univariate'',''equation'',''test'']," ^ |
119 " [''LINEAR'',''univariate'',''equation'',''test'']," ^ |
119 " [''Test'',''solve_linear'']) " ^ |
120 " [''Test'',''solve_linear'']) " ^ |
120 " [BOOL equ, REAL z]) " ^ |
121 " [BOOL equ, REAL z]) " ^ |
121 " in X)")] |
122 " in X)"*))] |
122 \<close> |
123 \<close> |
123 |
124 |
124 (* ok |
|
125 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool" |
125 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool" |
126 where |
126 where |
127 "inverse_ztransform2 X_eq X_z = |
127 "inverse_ztransform2 X_eq X_z = |
128 (let X = Take X_eq; |
128 (let X = Take X_eq; |
129 X' = Rewrite ''ruleZY'' False X; |
129 X' = Rewrite ''ruleZY'' False X; |
137 pbz_eq = Take (X'_z = pbz); |
137 pbz_eq = Take (X'_z = pbz); |
138 pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; |
138 pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; |
139 X_zeq = Take (X_z = rhs pbz_eq); |
139 X_zeq = Take (X_z = rhs pbz_eq); |
140 n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq |
140 n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq |
141 in n_eq)" |
141 in n_eq)" |
142 *) |
|
143 setup \<open>KEStore_Elems.add_mets |
142 setup \<open>KEStore_Elems.add_mets |
144 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID |
143 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID |
145 (["SignalProcessing", "Z_Transform", "Inverse_sub"], |
144 (["SignalProcessing", "Z_Transform", "Inverse_sub"], |
146 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]), |
145 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]), |
147 ("#Find" ,["stepResponse n_eq"])], |
146 ("#Find" ,["stepResponse n_eq"])], |
164 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
163 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
165 Rule.Calc ("Partial_Fractions.factors_from_solution", |
164 Rule.Calc ("Partial_Fractions.factors_from_solution", |
166 eval_factors_from_solution "#factors_from_solution") |
165 eval_factors_from_solution "#factors_from_solution") |
167 ], scr = Rule.EmptyScr}, |
166 ], scr = Rule.EmptyScr}, |
168 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, |
167 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, |
169 " Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
168 @{thm simplify.simps} |
|
169 (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) |
170 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
170 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) |
171 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
171 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
172 " (X'_z::real) = lhs X'; "^ (* ?X' z*) |
172 " (X'_z::real) = lhs X'; "^ (* ?X' z*) |
173 " (zzz::real) = argument_in X'_z; "^ (* z *) |
173 " (zzz::real) = argument_in X'_z; "^ (* z *) |
174 " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
174 " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) |
178 " [REAL funterm, REAL zzz]); "^ |
178 " [REAL funterm, REAL zzz]); "^ |
179 " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
179 " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
180 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
180 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) |
181 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
181 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) |
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]*) |
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]*) |
183 " in n_eq) ")](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
183 " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) |
184 \<close> |
184 \<close> |
185 |
185 |
186 end |
186 end |
187 |
187 |