1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform/Inverse_Z_Transform.thy Tue Sep 20 18:09:46 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform/Inverse_Z_Transform.thy Thu Sep 22 14:24:34 2011 +0200
1.3 @@ -18,6 +18,11 @@
1.4 axiomatization where
1.5 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
1.6
1.7 +subsection{*Define the Field Descriptions for the specification*}
1.8 +consts
1.9 + filterExpression :: "bool => una"
1.10 + stepResponse :: "bool => una"
1.11 +
1.12 subsection{*Define the Specification*}
1.13 ML {*
1.14 val thy = @{theory};
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/Build_Inverse_Z_Transform.thy Thu Sep 22 14:24:34 2011 +0200
2.3 @@ -0,0 +1,588 @@
2.4 +(* Title: Test_Z_Transform
2.5 + Author: Jan Rocnik
2.6 + (c) copyright due to lincense terms.
2.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.8 + 10 20 30 40 50 60 70 80
2.9 +*)
2.10 +
2.11 +theory Build_Inverse_Z_Transform imports Isac begin
2.12 +
2.13 +text{*We stepwise build Inverse_Z_Transform.thy as an exercise.
2.14 + Because subsection "Stepwise Check the Program" requires Inverse_Z_Transform.thy
2.15 + as a subtheory of Isac.thy, the setup has been changed from
2.16 + "theory Inverse_Z_Transform imports Isac begin.." to the above.
2.17 +
2.18 + ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
2.19 + Here in this theory there are the internal names twice, for instance we have
2.20 + (Thm.derivation_name @{thm rule1} = "Build_Inverse_Z_Transform.rule1") = true;
2.21 + but actually in us will be "Inverse_Z_Transform.rule1"
2.22 +*}
2.23 +ML {*val thy = @{theory Isac};*}
2.24 +
2.25 +
2.26 +section {*trials towards Z transform *}
2.27 +text{*===============================*}
2.28 +subsection {*terms*}
2.29 +ML {*
2.30 +@{term "1 < || z ||"};
2.31 +@{term "z / (z - 1)"};
2.32 +@{term "-u -n - 1"};
2.33 +@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
2.34 +@{term "z /(z - 1) = -u [-n - 1]"};Isac
2.35 +@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
2.36 +term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
2.37 +*}
2.38 +ML {*
2.39 +(*alpha --> "</alpha>" *)
2.40 +@{term "\<alpha> "};
2.41 +@{term "\<delta> "};
2.42 +@{term "\<phi> "};
2.43 +@{term "\<rho> "};
2.44 +term2str @{term "\<rho> "};
2.45 +*}
2.46 +
2.47 +subsection {*rules*}
2.48 +(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
2.49 +(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
2.50 +axiomatization where
2.51 + rule1: "1 = \<delta>[n]" and
2.52 + rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
2.53 + rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
2.54 + rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
2.55 + rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
2.56 + rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
2.57 +ML {*
2.58 +@{thm rule1};
2.59 +@{thm rule2};
2.60 +@{thm rule3};
2.61 +@{thm rule4};
2.62 +*}
2.63 +
2.64 +subsection {*apply rules*}
2.65 +ML {*
2.66 +val inverse_Z = append_rls "inverse_Z" e_rls
2.67 + [ Thm ("rule3",num_str @{thm rule3}),
2.68 + Thm ("rule4",num_str @{thm rule4}),
2.69 + Thm ("rule1",num_str @{thm rule1})
2.70 + ];
2.71 +
2.72 +val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
2.73 +val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
2.74 +term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
2.75 +*}
2.76 +ML {*
2.77 +val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
2.78 +*}
2.79 +ML {*
2.80 +val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
2.81 +term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
2.82 +term2str t;
2.83 +*}
2.84 +ML {*
2.85 +val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
2.86 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
2.87 +term2str t;
2.88 +*}
2.89 +ML {*
2.90 +val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
2.91 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
2.92 +term2str t;
2.93 +*}
2.94 +ML {*
2.95 +terms2str (asm1 @ asm2 @ asm3);
2.96 +*}
2.97 +
2.98 +section {*Prepare steps in CTP-based programming language*}
2.99 +text{*===================================================*}
2.100 +subsection {*prepare expression*}
2.101 +ML {*
2.102 +val ctxt = ProofContext.init_global @{theory Isac};
2.103 +val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
2.104 +
2.105 +val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
2.106 +val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
2.107 +*}
2.108 +
2.109 +axiomatization where
2.110 + ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
2.111 +
2.112 +ML {*
2.113 +val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
2.114 +val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
2.115 +val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
2.116 +
2.117 +val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
2.118 +term2str fun3; (*fails on x^^^(-1) TODO*)
2.119 +val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
2.120 +term2str fun3'; (*OK*)
2.121 +
2.122 +val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
2.123 +*}
2.124 +
2.125 +subsection {*solve equation*}
2.126 +text {*this type of equation if too general for the present program*}
2.127 +ML {*
2.128 +"----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------";
2.129 +val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
2.130 +val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];
2.131 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
2.132 +(* ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*)
2.133 +*}
2.134 +text {*Does the Equation Match the Specification ?*}
2.135 +ML {*
2.136 +match_pbl fmz (get_pbt ["univariate","equation"]);
2.137 +*}
2.138 +ML {*Context.theory_name thy = "Isac"(*==================================================*)*}
2.139 +
2.140 +ML {*
2.141 +val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^^^2 = 0";
2.142 +val fmz = (*specification*)
2.143 + ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*)
2.144 + "solveFor z", (*bound variable*)
2.145 + "solutions L"]; (*identifier for solution*)
2.146 +(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
2.147 +val (dI',pI',mI') =
2.148 + ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
2.149 +*}
2.150 +text {*Does the Other Equation Match the Specification ?*}
2.151 +ML {*
2.152 +match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]);
2.153 +*}
2.154 +text {*Solve Equation Stepwise*}
2.155 +ML {*
2.156 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.157 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.158 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.159 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.160 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.161 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.162 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.163 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.164 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.165 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.166 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.167 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.168 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
2.169 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.170 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
2.171 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
2.172 +show_pt pt;
2.173 +val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
2.174 +*}
2.175 +
2.176 +subsection {*partial fraction decomposition*}
2.177 +subsubsection {*solution of the equation*}
2.178 +ML {*
2.179 +val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
2.180 +term2str solutions;
2.181 +atomty solutions;
2.182 +*}
2.183 +
2.184 +subsubsection {*get solutions out of list*}
2.185 +text {*in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$*}
2.186 +ML {*
2.187 +val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $
2.188 + s_2 $ Const ("List.list.Nil", _)) = solutions;
2.189 +term2str s_1;
2.190 +term2str s_2;
2.191 +*}
2.192 +
2.193 +ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*)
2.194 +val xx = HOLogic.dest_eq s_1;
2.195 +val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
2.196 +val xx = HOLogic.dest_eq s_2;
2.197 +val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
2.198 +term2str s_1';
2.199 +term2str s_2';
2.200 +*}
2.201 +
2.202 +subsubsection {*build expression*}
2.203 +text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}
2.204 +ML {*
2.205 +(*The Main Denominator is the multiplikation of the partial fraction denominators*)
2.206 +val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ;
2.207 +val SOME numerator = parseNEW ctxt "3::real";
2.208 +
2.209 +val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');
2.210 +term2str expr';
2.211 +*}
2.212 +
2.213 +subsubsection {*Ansatz - create partial fractions out of our expression*}
2.214 +ML {*Context.theory_name thy = "Isac"(*==================================================*)*}
2.215 +
2.216 +axiomatization where
2.217 + ansatz2: "n / (a*b) = A/a + B/(b::real)" and
2.218 + multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))"
2.219 +
2.220 +ML {*
2.221 +(*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*)
2.222 +val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr';
2.223 +term2str t1; atomty t1;
2.224 +val eq1 = HOLogic.mk_eq (expr', t1);
2.225 +term2str eq1;
2.226 +*}
2.227 +ML {*
2.228 +(*eliminate the demoninators by multiplying the left and the right side with the main denominator*)
2.229 +val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1;
2.230 +term2str eq2;
2.231 +*}
2.232 +ML {*
2.233 +(*simplificatoin*)
2.234 +val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
2.235 +term2str eq3; (*?A ?B not simplified*)
2.236 +*}
2.237 +ML {*
2.238 +val SOME fract1 =
2.239 + parseNEW ctxt "(z - 1 / 2) * (z - -1 / 4) * (A / (z - 1 / 2) + B / (z - -1 / 4))"; (*A B !*)
2.240 +val SOME (fract2,_) = rewrite_set_ @{theory Isac} false norm_Rational fract1;
2.241 +term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
2.242 +(*term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" would be more traditional*)
2.243 +*}
2.244 +ML {*
2.245 +val (numerator, denominator) = HOLogic.dest_eq eq3;
2.246 +val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)
2.247 +term2str eq3';
2.248 +(*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*)
2.249 +val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
2.250 +term2str eq3'';
2.251 +*}
2.252 +ML {*Context.theory_name thy = "Isac"(*==================================================*)*}
2.253 +
2.254 +subsubsection {*get first koeffizient*}
2.255 +
2.256 +ML {*
2.257 +(*substitude z with the first zeropoint to get A*)
2.258 +val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
2.259 +term2str eq4_1;
2.260 +
2.261 +val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
2.262 +term2str eq4_2;
2.263 +
2.264 +val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"];
2.265 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
2.266 +(*solve the simple linear equilation for A TODO: return eq, not list of eq*)
2.267 +val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.268 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.269 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.270 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.271 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.272 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.273 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.274 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.275 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.276 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.277 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.278 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.279 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.280 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.281 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.282 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.283 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.284 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.285 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.286 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.287 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.288 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.289 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.290 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.291 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.292 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.293 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.294 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
2.295 +f2str fa;
2.296 +*}
2.297 +
2.298 +subsubsection {*get second koeffizient*}
2.299 +ML {*thy*}
2.300 +
2.301 +ML {*
2.302 +(*substitude z with the second zeropoint to get B*)
2.303 +val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
2.304 +term2str eq4b_1;
2.305 +
2.306 +val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
2.307 +term2str eq4b_2;
2.308 +*}
2.309 +ML {*
2.310 +(*solve the simple linear equilation for B TODO: return eq, not list of eq*)
2.311 +val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
2.312 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
2.313 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.314 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.315 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.316 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.317 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.318 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.319 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.320 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.321 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.322 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.323 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.324 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.325 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.326 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.327 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.328 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.329 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.330 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.331 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.332 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.333 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.334 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.335 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.336 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.337 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.338 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.339 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.340 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.341 +f2str fb;
2.342 +*}
2.343 +
2.344 +ML {* (*check koeffizients*)
2.345 +if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
2.346 +if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
2.347 +*}
2.348 +
2.349 +subsubsection {*substitute expression with solutions*}
2.350 +ML {*
2.351 +*}
2.352 +ML {*thy*}
2.353 +
2.354 +section {*Implement the Specification and the Method*}
2.355 +text{*==============================================*}
2.356 +subsection{*Define the Field Descriptions for the specification*}
2.357 +consts
2.358 + filterExpression :: "bool => una"
2.359 + stepResponse :: "bool => una"
2.360 +
2.361 +subsection{*Define the Specification*}
2.362 +ML {*
2.363 +store_pbt
2.364 + (prep_pbt thy "pbl_SP" [] e_pblID
2.365 + (["SignalProcessing"], [], e_rls, NONE, []));
2.366 +store_pbt
2.367 + (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
2.368 + (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
2.369 +*}
2.370 +ML {*thy*}
2.371 +ML {*
2.372 +store_pbt
2.373 + (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
2.374 + (["inverse", "Z_Transform", "SignalProcessing"],
2.375 + [("#Given" ,["filterExpression X_eq"]),
2.376 + ("#Find" ,["stepResponse n_eq"])
2.377 + ],
2.378 + append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
2.379 + [["SignalProcessing","Z_Transform","inverse"]]));
2.380 +
2.381 +show_ptyps();
2.382 +get_pbt ["inverse","Z_Transform","SignalProcessing"];
2.383 +*}
2.384 +
2.385 +subsection {*Define Name and Signature for the Method*}
2.386 +consts
2.387 + InverseZTransform :: "[bool, bool] => bool"
2.388 + ("((Script InverseZTransform (_ =))// (_))" 9)
2.389 +
2.390 +subsection {*Setup Parent Nodes in Hierarchy of Method*}
2.391 +ML {*
2.392 +store_met
2.393 + (prep_met thy "met_SP" [] e_metID
2.394 + (["SignalProcessing"], [],
2.395 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.396 + crls = e_rls, nrls = e_rls}, "empty_script"));
2.397 +store_met
2.398 + (prep_met thy "met_SP_Ztrans" [] e_metID
2.399 + (["SignalProcessing", "Z_Transform"], [],
2.400 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.401 + crls = e_rls, nrls = e_rls}, "empty_script"));
2.402 +*}
2.403 +ML {*
2.404 +store_met
2.405 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
2.406 + (["SignalProcessing", "Z_Transform", "inverse"],
2.407 + [("#Given" ,["filterExpression X_eq"]),
2.408 + ("#Find" ,["stepResponse n_eq"])
2.409 + ],
2.410 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.411 + crls = e_rls, nrls = e_rls},
2.412 + "empty_script"
2.413 + ));
2.414 +*}
2.415 +ML {*
2.416 +store_met
2.417 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
2.418 + (["SignalProcessing", "Z_Transform", "inverse"],
2.419 + [("#Given" ,["filterExpression X_eq"]),
2.420 + ("#Find" ,["stepResponse n_eq"])
2.421 + ],
2.422 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.423 + crls = e_rls, nrls = e_rls},
2.424 + "Script InverseZTransform (Xeq::bool) =" ^
2.425 + " (let X = Take Xeq;" ^
2.426 + " X = Rewrite ruleZY False X" ^
2.427 + " in X)"
2.428 + ));
2.429 +
2.430 +show_mets();
2.431 +get_met ["SignalProcessing","Z_Transform","inverse"];
2.432 +*}
2.433 +
2.434 +section {*Program in CTP-based language*}
2.435 +text{*=================================*}
2.436 +subsection {*Stepwise extend Program*}
2.437 +ML {*
2.438 +val str =
2.439 +"Script InverseZTransform (Xeq::bool) =" ^
2.440 +" Xeq";
2.441 +*}
2.442 +ML {*
2.443 +val str =
2.444 +"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.445 +" (let X = Take Xeq;" ^
2.446 +" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
2.447 +" X' = (Rewrite_Set norm_Rational False) X'" ^ (*simplify*)
2.448 +" in X)";
2.449 +(*NONE*)
2.450 +"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.451 +" (let X = Take Xeq;" ^
2.452 +" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
2.453 +" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
2.454 +" X' = (SubProblem (Isac',[pqFormula,degree_2,polynomial,univariate,equation], [no_met]) " ^
2.455 + " [BOOL e_e, REAL v_v])" ^
2.456 +" in X)";
2.457 +*}
2.458 +ML {*
2.459 +val str =
2.460 +"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.461 +" (let X = Take Xeq;" ^
2.462 +" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
2.463 +" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
2.464 +" funterm = rhs X'" ^ (*drop X'= for equation solving*)
2.465 +" in X)";
2.466 +*}
2.467 +ML {*
2.468 +parse thy str;
2.469 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.470 +atomty sc;
2.471 +
2.472 +*}
2.473 +ML {*
2.474 +term2str sc;
2.475 +atomty sc
2.476 +*}
2.477 +
2.478 +
2.479 +subsection {*Store Final Version of Program for Execution*}
2.480 +ML {*
2.481 +store_met
2.482 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
2.483 + (["SignalProcessing", "Z_Transform", "inverse"],
2.484 + [("#Given" ,["filterExpression X_eq"]),
2.485 + ("#Find" ,["stepResponse n_eq"])
2.486 + ],
2.487 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.488 + crls = e_rls, nrls = e_rls},
2.489 +"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.490 +" (let X = Take Xeq;" ^
2.491 +" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
2.492 +" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
2.493 +" funterm = rhs X'" ^ (*drop X'= for equation solving*)
2.494 +" in X)"
2.495 + ));
2.496 +*}
2.497 +
2.498 +
2.499 +subsection {*Stepwise Check the Program*}
2.500 +text {*At this section we got the error ME_Isa: thy 'Inverse_Z_Transform' not in system ?!?!?
2.501 + when working with "theory Inverse_Z_Transform imports Isac begin".
2.502 + Thus we switched to the present setting and separated Build_Inverse_Z_Transform.thy.
2.503 +*}
2.504 +
2.505 +subsubsection {*Check the formalization and start the program*}
2.506 +ML {*
2.507 +
2.508 +
2.509 +*}
2.510 +ML {*
2.511 +val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
2.512 + "stepResponse (x[n::real]::bool)"];
2.513 +val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
2.514 + ["SignalProcessing","Z_Transform","inverse"]);
2.515 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
2.516 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.517 +*}
2.518 +ML {*
2.519 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.520 +*}
2.521 +ML {*
2.522 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.523 +*}
2.524 +ML {*
2.525 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.526 +*}
2.527 +ML {*
2.528 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.529 +*}
2.530 +ML {*
2.531 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.532 +*}
2.533 +ML {*
2.534 +(*
2.535 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.536 +exception PTREE "get_obj: pos = [0] does not exist"
2.537 +raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
2.538 +*)
2.539 +*}
2.540 +
2.541 +
2.542 +ML {*
2.543 +
2.544 +*}
2.545 +ML {*
2.546 +
2.547 +*}
2.548 +ML {*
2.549 +
2.550 +*}
2.551 +ML {*
2.552 +
2.553 +*}
2.554 +
2.555 +ML {*
2.556 +
2.557 +*}
2.558 +ML {*
2.559 +
2.560 +*}
2.561 +
2.562 +ML {*
2.563 +
2.564 +*}
2.565 +ML {*
2.566 +
2.567 +*}
2.568 +ML {*
2.569 +
2.570 +*}
2.571 +
2.572 +
2.573 +
2.574 +
2.575 +
2.576 +
2.577 +
2.578 +
2.579 +section {*Write Tests for Crucial Details*}
2.580 +text{*===================================*}
2.581 +ML {*
2.582 +
2.583 +*}
2.584 +
2.585 +section {*Integrate Program into Knowledge*}
2.586 +ML {*
2.587 +
2.588 +*}
2.589 +
2.590 +end
2.591 +
3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/Inverse_Z_Transform.thy Tue Sep 20 18:09:46 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,530 +0,0 @@
3.4 -(* Title: Test_Z_Transform
3.5 - Author: Jan Rocnik
3.6 - (c) copyright due to lincense terms.
3.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.8 - 10 20 30 40 50 60 70 80
3.9 -*)
3.10 -
3.11 -theory Inverse_Z_Transform imports Isac begin
3.12 -
3.13 -section {*trials towards Z transform *}
3.14 -text{*===============================*}
3.15 -subsection {*terms*}
3.16 -ML {*
3.17 -@{term "1 < || z ||"};
3.18 -@{term "z / (z - 1)"};
3.19 -@{term "-u -n - 1"};
3.20 -@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
3.21 -@{term "z /(z - 1) = -u [-n - 1]"};Isac
3.22 -@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
3.23 -term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
3.24 -*}
3.25 -ML {*
3.26 -(*alpha --> "</alpha>" *)
3.27 -
3.28 -@{term "\<alpha> "};
3.29 -@{term "\<delta> "};
3.30 -@{term "\<phi> "};
3.31 -@{term "\<rho> "};
3.32 -term2str @{term "\<rho> "};
3.33 -*}
3.34 -
3.35 -subsection {*rules*}
3.36 -(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
3.37 -(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
3.38 -axiomatization where
3.39 - rule1: "1 = \<delta>[n]" and
3.40 - rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
3.41 - rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
3.42 - rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
3.43 - rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
3.44 - rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
3.45 -ML {*
3.46 -@{thm rule1};
3.47 -@{thm rule2};
3.48 -@{thm rule3};
3.49 -@{thm rule4};
3.50 -*}
3.51 -
3.52 -subsection {*apply rules*}
3.53 -ML {*
3.54 -val inverse_Z = append_rls "inverse_Z" e_rls
3.55 - [ Thm ("rule3",num_str @{thm rule3}),
3.56 - Thm ("rule4",num_str @{thm rule4}),
3.57 - Thm ("rule1",num_str @{thm rule1})
3.58 - ];
3.59 -
3.60 -val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
3.61 -val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
3.62 -term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
3.63 -*}
3.64 -ML {*
3.65 -val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
3.66 -*}
3.67 -ML {*
3.68 -val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
3.69 -term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
3.70 -term2str t;
3.71 -*}
3.72 -ML {*
3.73 -val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
3.74 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
3.75 -term2str t;
3.76 -*}
3.77 -ML {*
3.78 -val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
3.79 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
3.80 -term2str t;
3.81 -*}
3.82 -ML {*
3.83 -terms2str (asm1 @ asm2 @ asm3);
3.84 -*}
3.85 -
3.86 -section {*Prepare steps in CTP-based programming language*}
3.87 -text{*===================================================*}
3.88 -subsection {*prepare expression*}
3.89 -ML {*
3.90 -val ctxt = ProofContext.init_global @{theory};
3.91 -val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
3.92 -
3.93 -val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
3.94 -val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
3.95 -*}
3.96 -
3.97 -axiomatization where
3.98 - ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
3.99 -
3.100 -ML {*
3.101 -val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
3.102 -val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
3.103 -val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
3.104 -
3.105 -val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
3.106 -term2str fun3; (*fails on x^^^(-1) TODO*)
3.107 -val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
3.108 -term2str fun3'; (*OK*)
3.109 -
3.110 -val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
3.111 -*}
3.112 -
3.113 -subsection {*solve equation*}
3.114 -text {*this type of equation if too general for the present program*}
3.115 -ML {*
3.116 -"----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------";
3.117 -val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
3.118 -val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];
3.119 -val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
3.120 -(* ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*)
3.121 -*}
3.122 -text {*Does the Equation Match the Specification ?*}
3.123 -ML {*
3.124 -match_pbl fmz (get_pbt ["univariate","equation"]);
3.125 -*}
3.126 -
3.127 -ML {*
3.128 -val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^^^2 = 0";
3.129 -val fmz = (*specification*)
3.130 - ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*)
3.131 - "solveFor z", (*bound variable*)
3.132 - "solutions L"]; (*identifier for solution*)
3.133 -(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
3.134 -val (dI',pI',mI') =
3.135 - ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
3.136 -*}
3.137 -text {*Does the Other Equation Match the Specification ?*}
3.138 -ML {*
3.139 -match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]);
3.140 -*}
3.141 -text {*Solve Equation Stepwise*}
3.142 -ML {*
3.143 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.144 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.145 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.146 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.147 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.148 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.149 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.150 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.151 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.152 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.153 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.154 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.155 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
3.156 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.157 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
3.158 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
3.159 -show_pt pt;
3.160 -val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
3.161 -*}
3.162 -
3.163 -subsection {*partial fraction decomposition*}
3.164 -subsubsection {*solution of the equation*}
3.165 -ML {*
3.166 -val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
3.167 -term2str solutions;
3.168 -atomty solutions;
3.169 -*}
3.170 -
3.171 -subsubsection {*get solutions out of list*}
3.172 -text {*in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$*}
3.173 -ML {*
3.174 -val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $
3.175 - s_2 $ Const ("List.list.Nil", _)) = solutions;
3.176 -term2str s_1;
3.177 -term2str s_2;
3.178 -*}
3.179 -
3.180 -ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*)
3.181 -val xx = HOLogic.dest_eq s_1;
3.182 -val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
3.183 -val xx = HOLogic.dest_eq s_2;
3.184 -val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
3.185 -term2str s_1';
3.186 -term2str s_2';
3.187 -*}
3.188 -
3.189 -subsubsection {*build expression*}
3.190 -text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}
3.191 -ML {*
3.192 -(*The Main Denominator is the multiplikation of the partial fraction denominators*)
3.193 -val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ;
3.194 -val SOME numerator = parseNEW ctxt "3::real";
3.195 -
3.196 -val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');
3.197 -term2str expr';
3.198 -*}
3.199 -
3.200 -subsubsection {*Ansatz - create partial fractions out of our expression*}
3.201 -
3.202 -axiomatization where
3.203 - ansatz2: "n / (a*b) = A/a + B/(b::real)" and
3.204 - multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))"
3.205 -
3.206 -ML {*
3.207 -(*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*)
3.208 -val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr';
3.209 -term2str t1; atomty t1;
3.210 -val eq1 = HOLogic.mk_eq (expr', t1);
3.211 -term2str eq1;
3.212 -*}
3.213 -ML {*
3.214 -(*eliminate the demoninators by multiplying the left and the right side with the main denominator*)
3.215 -val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1;
3.216 -term2str eq2;
3.217 -*}
3.218 -ML {*
3.219 -(*simplificatoin*)
3.220 -val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
3.221 -term2str eq3; (*?A ?B not simplified*)
3.222 -*}
3.223 -ML {*
3.224 -val SOME fract1 =
3.225 - parseNEW ctxt "(z - 1 / 2) * (z - -1 / 4) * (A / (z - 1 / 2) + B / (z - -1 / 4))"; (*A B !*)
3.226 -val SOME (fract2,_) = rewrite_set_ @{theory Isac} false norm_Rational fract1;
3.227 -term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
3.228 -(*term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" would be more traditional*)
3.229 -*}
3.230 -ML {*
3.231 -val (numerator, denominator) = HOLogic.dest_eq eq3;
3.232 -val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)
3.233 -term2str eq3';
3.234 -(*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*)
3.235 -val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
3.236 -term2str eq3'';
3.237 -*}
3.238 -
3.239 -subsubsection {*get first koeffizient*}
3.240 -
3.241 -ML {*
3.242 -(*substitude z with the first zeropoint to get A*)
3.243 -val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
3.244 -term2str eq4_1;
3.245 -
3.246 -val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
3.247 -term2str eq4_2;
3.248 -
3.249 -val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"];
3.250 -val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
3.251 -(*solve the simple linear equilation for A TODO: return eq, not list of eq*)
3.252 -val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.253 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.254 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.255 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.256 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.257 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.258 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.259 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.260 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.261 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.262 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.263 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.264 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.265 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.266 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.267 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.268 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.269 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.270 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.271 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.272 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.273 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.274 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.275 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.276 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.277 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.278 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.279 -val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
3.280 -f2str fa;
3.281 -*}
3.282 -
3.283 -subsubsection {*get second koeffizient*}
3.284 -
3.285 -ML {*
3.286 -(*substitude z with the second zeropoint to get B*)
3.287 -val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
3.288 -term2str eq4b_1;
3.289 -
3.290 -val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
3.291 -term2str eq4b_2;
3.292 -*}
3.293 -ML {*
3.294 -(*solve the simple linear equilation for B TODO: return eq, not list of eq*)
3.295 -val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
3.296 -val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
3.297 -val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.298 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.299 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.300 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.301 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.302 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.303 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.304 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.305 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.306 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.307 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.308 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.309 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.310 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.311 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.312 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.313 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.314 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.315 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.316 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.317 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.318 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.319 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.320 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.321 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.322 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.323 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.324 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.325 -f2str fb;
3.326 -*}
3.327 -
3.328 -ML {* (*check koeffizients*)
3.329 -if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
3.330 -if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
3.331 -*}
3.332 -
3.333 -subsubsection {*substitute expression with solutions*}
3.334 -ML {*
3.335 -*}
3.336 -
3.337 -section {*Implement the Specification and the Method*}
3.338 -text{*==============================================*}
3.339 -subsection{*Define the Field Descriptions for the specification*}
3.340 -consts
3.341 - filterExpression :: "bool => una"
3.342 - stepResponse :: "bool => una"
3.343 -
3.344 -subsection{*Define the Specification*}
3.345 -ML {*
3.346 -val thy = @{theory};
3.347 -*}
3.348 -ML {*
3.349 -store_pbt
3.350 - (prep_pbt thy "pbl_SP" [] e_pblID
3.351 - (["SignalProcessing"], [], e_rls, NONE, []));
3.352 -store_pbt
3.353 - (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
3.354 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
3.355 -store_pbt
3.356 - (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
3.357 - (["inverse", "Z_Transform", "SignalProcessing"],
3.358 - [("#Given" ,["filterExpression X_eq"]),
3.359 - ("#Find" ,["stepResponse n_eq"])
3.360 - ],
3.361 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
3.362 - [["SignalProcessing","Z_Transform","inverse"]]));
3.363 -
3.364 -show_ptyps();
3.365 -get_pbt ["inverse","Z_Transform","SignalProcessing"];
3.366 -*}
3.367 -
3.368 -subsection {*Define Name and Signature for the Method*}
3.369 -consts
3.370 - InverseZTransform :: "[bool, bool] => bool"
3.371 - ("((Script InverseZTransform (_ =))// (_))" 9)
3.372 -
3.373 -subsection {*Setup Parent Nodes in Hierarchy of Method*}
3.374 -ML {*
3.375 -store_met
3.376 - (prep_met thy "met_SP" [] e_metID
3.377 - (["SignalProcessing"], [],
3.378 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
3.379 - crls = e_rls, nrls = e_rls}, "empty_script"));
3.380 -store_met
3.381 - (prep_met thy "met_SP_Ztrans" [] e_metID
3.382 - (["SignalProcessing", "Z_Transform"], [],
3.383 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
3.384 - crls = e_rls, nrls = e_rls}, "empty_script"));
3.385 -*}
3.386 -ML {*
3.387 -val thy = @{theory}; (*latest version of thy required*)
3.388 -store_met
3.389 - (prep_met thy "met_SP_Ztrans_inv" [] e_metID
3.390 - (["SignalProcessing", "Z_Transform", "inverse"],
3.391 - [("#Given" ,["filterExpression X_eq"]),
3.392 - ("#Find" ,["stepResponse n_eq"])
3.393 - ],
3.394 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
3.395 - crls = e_rls, nrls = e_rls},
3.396 - "Script InverseZTransform (Xeq::bool) =" ^
3.397 - " (let X = Take Xeq;" ^
3.398 - " X = Rewrite ruleZY False X" ^
3.399 - " in X)"
3.400 - ));
3.401 -
3.402 -show_mets();
3.403 -get_met ["SignalProcessing","Z_Transform","inverse"];
3.404 -*}
3.405 -
3.406 -
3.407 -section {*Program in CTP-based language*}
3.408 -text{*=================================*}
3.409 -subsection {*Stepwise extend Program*}
3.410 -ML {*
3.411 -val str =
3.412 -"Script InverseZTransform (Xeq::bool) =" ^
3.413 -" Xeq";
3.414 -*}
3.415 -ML {*
3.416 -val str =
3.417 -"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
3.418 -" (let X = Take Xeq;" ^
3.419 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
3.420 -" X' = (Rewrite_Set norm_Rational False) X'" ^ (*simplify*)
3.421 -" in X)";
3.422 -(*NONE*)
3.423 -"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
3.424 -" (let X = Take Xeq;" ^
3.425 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
3.426 -" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
3.427 -" X' = (SubProblem (Isac',[pqFormula,degree_2,polynomial,univariate,equation], [no_met]) " ^
3.428 - " [BOOL e_e, REAL v_v])" ^
3.429 -" in X)";
3.430 -*}
3.431 -ML {*
3.432 -val str =
3.433 -"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
3.434 -" (let X = Take Xeq;" ^
3.435 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
3.436 -" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
3.437 -" funterm = rhs X'" ^ (*drop X'= for equation solving*)
3.438 -" in X)";
3.439 -*}
3.440 -ML {*
3.441 -parse thy str;
3.442 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.443 -atomty sc;
3.444 -
3.445 -*}
3.446 -ML {*
3.447 -term2str sc;
3.448 -atomty sc
3.449 -*}
3.450 -
3.451 -
3.452 -subsection {*Store Final Version of Program for Execution*}
3.453 -ML {*
3.454 -store_met
3.455 - (prep_met thy "met_SP_Ztrans_inv" [] e_metID
3.456 - (["SignalProcessing", "Z_Transform", "inverse"],
3.457 - [("#Given" ,["filterExpression X_eq"]),
3.458 - ("#Find" ,["stepResponse n_eq"])
3.459 - ],
3.460 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
3.461 - crls = e_rls, nrls = e_rls},
3.462 -"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
3.463 -" (let X = Take Xeq;" ^
3.464 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
3.465 -" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
3.466 -" funterm = rhs X'" ^ (*drop X'= for equation solving*)
3.467 -" in X)"
3.468 - ));
3.469 -*}
3.470 -
3.471 -
3.472 -subsection {*Stepwise Execute the Program*}
3.473 -ML {*
3.474 -parseNEW ctxt "stepResponse x[n]";
3.475 -Thy_Info.get_theory "Inverse_Z_Transform";
3.476 -*}
3.477 -
3.478 -ML {*
3.479 -print_depth 999; Thy_Info.get_names(); print_depth 999;
3.480 -*}
3.481 -
3.482 -ML {*
3.483 -(*val SOME func = parseNEW ctxt "X = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1;*)
3.484 -val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/z)))", "stepResponse x[n]"];
3.485 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
3.486 - ["SignalProcessing","Z_Transform","inverse"]);
3.487 -val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
3.488 -*}
3.489 -
3.490 -ML {*
3.491 -get_met ["SignalProcessing","Z_Transform","inverse"];
3.492 -*}
3.493 -ML {*
3.494 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt
3.495 -*}
3.496 -
3.497 -ML {*
3.498 -f2str fb;
3.499 -*}
3.500 -
3.501 -ML {*
3.502 -val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
3.503 -val (dI,pI,mI) =("Isac", ["univariate","equation"], ["no_met"]);
3.504 -val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
3.505 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.506 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.507 -*}
3.508 -
3.509 -ML {*
3.510 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.511 -f2str fb;
3.512 -*}
3.513 -
3.514 -
3.515 -
3.516 -
3.517 -
3.518 -
3.519 -
3.520 -
3.521 -section {*Write Tests for Crucial Details*}
3.522 -text{*===================================*}
3.523 -ML {*
3.524 -
3.525 -*}
3.526 -
3.527 -section {*Integrate Program into Knowledge*}
3.528 -ML {*
3.529 -
3.530 -*}
3.531 -
3.532 -end
3.533 -
4.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 20 18:09:46 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Sep 22 14:24:34 2011 +0200
4.3 @@ -17,6 +17,7 @@
4.4 "--------- regression test fun is_copy_named ------------";
4.5 "--------- regr.test fun cpy_nam ------------------------";
4.6 "--------- check specify phase --------------------------";
4.7 +"--------- check: fmz matches pbt -----------------------";
4.8 "--------------------------------------------------------";
4.9 "--------------------------------------------------------";
4.10 "--------------------------------------------------------";
4.11 @@ -724,3 +725,51 @@
4.12 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
4.13 if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
4.14 else error "clchead.sml: check specify phase step 2";
4.15 +
4.16 +"--------- check: fmz matches pbt -----------------------";
4.17 +"--------- check: fmz matches pbt -----------------------";
4.18 +"--------- check: fmz matches pbt -----------------------";
4.19 +"101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
4.20 +"the following fmz caused the above error";
4.21 +val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
4.22 +val pI = ["plus_minus","polynom","vereinfachen"];
4.23 +
4.24 +"----- this fmz is transformed to this internal format (TERM --> Pure.term):";
4.25 +val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
4.26 + (*#############################^^^^^^^^^ defined by Isabelle*)
4.27 + (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
4.28 + [Free ("N", _ (*"RealDef.real"*))])],
4.29 + _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
4.30 +"#undef means: the element with description TERM in fmz did not match ";
4.31 +"with any element of pbl (fetched by pI), because there we have Simplify.Term";
4.32 +"defined in Simplify.thy";
4.33 +
4.34 +"So we try out how to create Simplify.Term:";
4.35 +"----- trial 1";
4.36 +val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";
4.37 +" ^^^^^^^^^ see above";
4.38 +atomwy t;
4.39 +
4.40 +"----- trial 2";
4.41 +val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";
4.42 +" ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";
4.43 +atomwy t;
4.44 +
4.45 +"----- trial 3";
4.46 +val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";
4.47 +" ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";
4.48 +" and unsed in pbl [plus_minus,polynom,vereinfachen]";
4.49 +atomwy t;
4.50 +
4.51 +"----- so this is the correct fmz:";
4.52 +val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
4.53 +val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),
4.54 + (*########################^^^^^^^^^ defined in Simplify.thy*)
4.55 + (2, [1], "#Find", Const ("Simplify.normalform", _ ),
4.56 + [Free ("N", _ )])],
4.57 + _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
4.58 +
4.59 +"----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
4.60 +val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
4.61 + ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
4.62 +
5.1 --- a/test/Tools/isac/Interpret/mathengine.sml Tue Sep 20 18:09:46 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Sep 22 14:24:34 2011 +0200
5.3 @@ -1,8 +1,5 @@
5.4 -
5.5 -
5.6 -
5.7 -(* test for sml/ME/mathengine.sml
5.8 - authors: Walther Neuper 2000, 2006
5.9 +(* Title: tests for Interpret/mathengine.sml
5.10 + Author: Walther Neuper 2000, 2006
5.11 (c) due to copyright terms
5.12 *)
5.13 "--------------------------------------------------------";
5.14 @@ -17,6 +14,7 @@
5.15 "----------- fun autoCalculate --------------------------";
5.16 "----------- fun autoCalculate..CompleteCalc ------------";
5.17 "----------- search for Or_to_List ----------------------";
5.18 +"----------- check thy in CalcTreeTEST ------------------";
5.19 "--------------------------------------------------------";
5.20 "--------------------------------------------------------";
5.21 "--------------------------------------------------------";
5.22 @@ -469,4 +467,50 @@
5.23 case tac_ of Or_to_List' _ => ()
5.24 | _ => error "Or_to_List broken ?"
5.25
5.26 +"----------- check thy in CalcTreeTEST ------------------";
5.27 +"----------- check thy in CalcTreeTEST ------------------";
5.28 +"----------- check thy in CalcTreeTEST ------------------";
5.29 +"WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
5.30 +"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
5.31 +"Below there are the steps which found out the reason: \n" ^
5.32 +"store_pbt mistakenly stored that theory.";
5.33 +val ctxt = ProofContext.init_global @{theory Isac};
5.34 +val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
5.35 +val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
5.36
5.37 +val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
5.38 + "stepResponse (x[n::real]::bool)"];
5.39 +val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
5.40 + ["SignalProcessing","Z_Transform","inverse"]);
5.41 +
5.42 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
5.43 +(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
5.44 +
5.45 +"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
5.46 +"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
5.47 + val thy = assoc_thy dI;
5.48 + mI = ["no_met"]; (*false*)
5.49 + val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
5.50 + val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
5.51 + "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
5.52 + val dI = theory2theory' (maxthy thy thy');
5.53 +"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
5.54 + cas = NONE; (*true*)
5.55 + val hdl = pblterm dI pI;
5.56 + val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
5.57 + (pors, (dI, pI, mI), hdl)
5.58 + val pt = update_ctxt pt [] pctxt;
5.59 +
5.60 +"~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
5.61 + val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
5.62 +"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
5.63 +
5.64 +"~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
5.65 +dI = e_domID; (*true*)
5.66 +odI = "Build_Inverse_Z_Transform"; (*true*)
5.67 +dI = "e_domID"; (*true*)
5.68 +"~~~~~ after fun some_spec:";
5.69 + val (dI, pI, mI) = some_spec ospec spec;
5.70 +"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
5.71 + val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
5.72 +
6.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Tue Sep 20 18:09:46 2011 +0200
6.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Thu Sep 22 14:24:34 2011 +0200
6.3 @@ -1,4 +1,4 @@
6.4 -(* Title: test_z_transform
6.5 +(* Title: inverse_z_transform
6.6 Author: Jan Rocnik
6.7 (c) copyright due to lincense terms.
6.8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Sep 20 18:09:46 2011 +0200
7.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Sep 22 14:24:34 2011 +0200
7.3 @@ -26,7 +26,6 @@
7.4 "----------- pbl binom polynom vereinfachen: cube -------";
7.5 "----------- refine Vereinfache -------------------------";
7.6 "----------- *** prep_pbt: syntax error in '#Where' of [v";
7.7 -"----------- check: fmz matches pbt ---------------------";
7.8 "--------------------------------------------------------";
7.9 "--------------------------------------------------------";
7.10 "--------------------------------------------------------";
7.11 @@ -641,30 +640,6 @@
7.12 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
7.13 show_types := false;
7.14
7.15 -"----------- check: fmz matches pbt ---------------------";
7.16 -"----------- check: fmz matches pbt ---------------------";
7.17 -"----------- check: fmz matches pbt ---------------------";
7.18 -"101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
7.19 -val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
7.20 -val pI = ["plus_minus","polynom","vereinfachen"];
7.21 -prep_ori fmz thy ((#ppc o get_pbt) pI);
7.22 -(*val it =
7.23 - [(1, [1], "#undef", Const (...), [...]), <<<===
7.24 - (2, [1], "#Find", Const (...), [...])]
7.25 - : ori list
7.26 -*)
7.27 -val t = str2term "TERM ttt";
7.28 -atomwy t;
7.29 -val t = str2term "term ttt";
7.30 -atomwy t;
7.31 -val t = str2term "Term ttt";
7.32 -atomwy t;
7.33 -val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
7.34 -prep_ori fmz thy ((#ppc o get_pbt) pI);
7.35 -(*val it =
7.36 - [(1, [1], "#Given", Const (...), [...]),
7.37 - (2, [1], "#Find", Const (...), [...])]
7.38 - : ori list
7.39 -*)
7.40 +
7.41 ============ inhibit exn 110719 ==============================================*)
7.42
8.1 --- a/test/Tools/isac/Test_Some.thy Tue Sep 20 18:09:46 2011 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Thu Sep 22 14:24:34 2011 +0200
8.3 @@ -6,34 +6,23 @@
8.4 *)
8.5
8.6 theory Test_Some imports Isac begin
8.7 -text{*
8.8 -use"../../../test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
8.9 -*}
8.10 +
8.11 +use"../../../test/Tools/isac/Interpret/mathengine.sml"
8.12
8.13 ML {*
8.14 -val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
8.15 - "stepResponse x[(n::real)]"];
8.16 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
8.17 - ["SignalProcessing","Z_Transform","inverse"]);
8.18 -*}
8.19 -ML {*
8.20 -prep_ori fmz @{theory} ((#ppc o get_pbt) pI);
8.21
8.22 *}
8.23 ML {*
8.24
8.25 *}
8.26 ML {*
8.27 -val SOME t = parseNEW ctxt "stepResponse x[(n::real)]";
8.28
8.29 *}
8.30 ML {*
8.31
8.32 *}
8.33 +ML {*
8.34
8.35 -ML {*
8.36 -val c = [];
8.37 -print_depth 5;
8.38 *}
8.39 ML {*
8.40