1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/jrocnik/Inverse_Z_Transform/Inverse_Z_Transform.thy Thu Sep 08 23:17:35 2011 +0200
1.3 @@ -0,0 +1,449 @@
1.4 +(* Title: Test_Z_Transform
1.5 + Author: Jan Rocnik
1.6 + (c) copyright due to lincense terms.
1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 + 10 20 30 40 50 60 70 80
1.9 +*)
1.10 +
1.11 +theory Inverse_Z_Transform imports Isac begin
1.12 +
1.13 +section {*trials towards Z transform *}
1.14 +text{*===============================*}
1.15 +subsection {*terms*}
1.16 +ML {*
1.17 +@{term "1 < || z ||"};
1.18 +@{term "z / (z - 1)"};
1.19 +@{term "-u -n - 1"};
1.20 +@{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
1.21 +@{term "z /(z - 1) = -u [-n - 1]"};Isac
1.22 +@{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.23 +term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.24 +*}
1.25 +ML {*
1.26 +(*alpha --> "</alpha>" *)
1.27 +
1.28 +@{term "\<alpha> "};
1.29 +@{term "\<delta> "};
1.30 +@{term "\<phi> "};
1.31 +@{term "\<rho> "};
1.32 +term2str @{term "\<rho> "};
1.33 +*}
1.34 +
1.35 +subsection {*rules*}
1.36 +(*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
1.37 +(*definition "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
1.38 +axiomatization where
1.39 + rule1: "1 = \<delta>[n]" and
1.40 + rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
1.41 + rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
1.42 + rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^n * u [n]" and
1.43 + rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^n) * u [-n - 1]" and
1.44 + rule6: "|| z || > 1 ==> z/(z - 1)^2 = n * u [n]"
1.45 +ML {*
1.46 +@{thm rule1};
1.47 +@{thm rule2};
1.48 +@{thm rule3};
1.49 +@{thm rule4};
1.50 +*}
1.51 +
1.52 +subsection {*apply rules*}
1.53 +ML {*
1.54 +val inverse_Z = append_rls "inverse_Z" e_rls
1.55 + [ Thm ("rule3",num_str @{thm rule3}),
1.56 + Thm ("rule4",num_str @{thm rule4}),
1.57 + Thm ("rule1",num_str @{thm rule1})
1.58 + ];
1.59 +
1.60 +val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.61 +val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
1.62 +term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)
1.63 +*}
1.64 +ML {*
1.65 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.66 +*}
1.67 +ML {*
1.68 +val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.69 +term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
1.70 +term2str t;
1.71 +*}
1.72 +ML {*
1.73 +val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
1.74 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + 1"; (*- real *)
1.75 +term2str t;
1.76 +*}
1.77 +ML {*
1.78 +val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
1.79 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
1.80 +term2str t;
1.81 +*}
1.82 +ML {*
1.83 +terms2str (asm1 @ asm2 @ asm3);
1.84 +*}
1.85 +
1.86 +section {*Prepare steps in CTP-based programming language*}
1.87 +text{*===================================================*}
1.88 +subsection {*prepare expression*}
1.89 +ML {*
1.90 +val ctxt = ProofContext.init_global @{theory};
1.91 +val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
1.92 +
1.93 +val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^ -1)"; term2str fun1;
1.94 +val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.95 +*}
1.96 +
1.97 +axiomatization where
1.98 + ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
1.99 +
1.100 +ML {*
1.101 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.102 +val SOME (fun2, asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.103 +val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.104 +
1.105 +val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
1.106 +term2str fun3; (*fails on x^(-1) TODO*)
1.107 +val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
1.108 +term2str fun3'; (*OK*)
1.109 +
1.110 +val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
1.111 +*}
1.112 +
1.113 +subsection {*solve equation*}
1.114 +ML {*(*from test/Tools/isac/Minisubpbl/100-init-rootpbl.sml*)
1.115 +"----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------";
1.116 +val denominator = parseNEW ctxt "z^2 - 1/4*z - 1/8 = 0";
1.117 +val fmz = ["equality (z^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];
1.118 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.119 +(* ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*)
1.120 +*}
1.121 +ML {*
1.122 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.123 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.124 +(*[
1.125 +(([], Frm), solve (z ^ 2 - 1 / 4 * z - 1 / 8 = 0, z)),
1.126 +(([1], Frm), z ^ 2 - 1 / 4 * z - 1 / 8 = 0), bad rewrite order
1.127 +(([1], Res), -1 / 8 + z ^ 2 + -1 / 4 * z = 0), bad pattern
1.128 +(([2], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.129 +(([2,1], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.130 +(([2,1,1], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.131 +(([2,1,1,1], Frm), -1 / 8 + z ^ 2 + -1 / 4 * z = 0)]
1.132 +*)
1.133 +*}
1.134 +ML {*
1.135 +val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^2 = 0";
1.136 +(*ergebnis: [gleichung, was tun?, lösung]*)
1.137 +val fmz = ["equality (-1/8 + -1/4*z + z^2 = (0::real))", "solveFor z","solutions L"];
1.138 +(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
1.139 +val (dI',pI',mI') =
1.140 + ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
1.141 +(*schritte abarbeiten*)
1.142 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.143 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.144 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.145 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.146 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*val nxt = ("Empty_Tac", ...): tac'_*)
1.147 +show_pt pt;
1.148 +*}
1.149 +
1.150 +subsection {*partial fraction decomposition*}
1.151 +subsubsection {*solution of the equation*}
1.152 +ML {*
1.153 +val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
1.154 +term2str solutions;
1.155 +atomty solutions;
1.156 +*}
1.157 +
1.158 +subsubsection {*get solutions out of list*}
1.159 +text {*in isac's CTP-based programming language: $let s_1 = NTH 1 solutions; s_2 = NTH 2...$*}
1.160 +ML {*
1.161 +val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $
1.162 + s_2 $ Const ("List.list.Nil", _)) = solutions;
1.163 +term2str s_1;
1.164 +term2str s_2;
1.165 +*}
1.166 +
1.167 +ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*)
1.168 +val xx = HOLogic.dest_eq s_1;
1.169 +val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.170 +val xx = HOLogic.dest_eq s_2;
1.171 +val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.172 +term2str s_1';
1.173 +term2str s_2';
1.174 +*}
1.175 +
1.176 +subsubsection {*build expression*}
1.177 +text {*in isac's CTP-based programming language: $let s_1 = Take numerator / (s_1 * s_2)$*}
1.178 +ML {*
1.179 +(*The Main Denominator is the multiplikation of the partial fraction denominators*)
1.180 +val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ;
1.181 +val SOME numerator = parseNEW ctxt "3::real";
1.182 +
1.183 +val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');
1.184 +term2str expr';
1.185 +*}
1.186 +
1.187 +subsubsection {*Ansatz - create partial fractions out of our expression*}
1.188 +
1.189 +axiomatization where
1.190 + ansatz2: "n / (a*b) = A/a + B/(b::real)" and
1.191 + multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))"
1.192 +
1.193 +ML {*
1.194 +(*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*)
1.195 +val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr';
1.196 +term2str t1;
1.197 +atomty t1;
1.198 +val eq1 = HOLogic.mk_eq (expr', t1);
1.199 +term2str eq1;
1.200 +*}
1.201 +ML {*
1.202 +(*eliminate the demoninators by multiplying the left and the right side with the main denominator*)
1.203 +val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1;
1.204 +term2str eq2;
1.205 +*}
1.206 +ML {*
1.207 +(*simplificatoin*)
1.208 +val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
1.209 +term2str eq3; (*?A ?B not simplified*)
1.210 +*}
1.211 +ML {*
1.212 +val SOME fract1 =
1.213 + parseNEW ctxt "(z - 1 / 2) * (z - -1 / 4) * (A / (z - 1 / 2) + B / (z - -1 / 4))"; (*A B !*)
1.214 +val SOME (fract2,_) = rewrite_set_ @{theory Isac} false norm_Rational fract1;
1.215 +term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.216 +(*term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" would be more traditional*)
1.217 +*}
1.218 +ML {*
1.219 +val (numerator, denominator) = HOLogic.dest_eq eq3;
1.220 +val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)
1.221 +term2str eq3';
1.222 +*}
1.223 +ML {* (*MANDATORY: otherwise 3 = 0*)
1.224 +val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
1.225 +term2str eq3'';
1.226 +*}
1.227 +
1.228 +subsubsection {*get first koeffizient*}
1.229 +
1.230 +ML {*
1.231 +(*substitude z with the first zeropoint to get A*)
1.232 +val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
1.233 +term2str eq4_1;
1.234 +*}
1.235 +ML {*
1.236 +val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
1.237 +term2str eq4_2;
1.238 +*}
1.239 +ML {*
1.240 +val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"];
1.241 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.242 +
1.243 +*}
1.244 +ML {*
1.245 +(*solve the simple linear equilation for A TODO: return eq, not list of eq*)
1.246 +val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.247 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.248 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.249 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.250 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.251 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.252 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.253 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.254 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.255 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.256 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.257 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.258 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.259 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.260 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.261 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.262 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.263 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.264 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.265 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.266 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.267 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.268 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.269 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.270 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.271 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.272 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.273 +*}
1.274 +ML {*
1.275 +val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.276 +f2str fa;
1.277 +*}
1.278 +
1.279 +subsubsection {*get second koeffizient*}
1.280 +
1.281 +ML {*
1.282 +(*substitude z with the second zeropoint to get B*)
1.283 +val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
1.284 +term2str eq4b_1;
1.285 +*}
1.286 +
1.287 +ML {*
1.288 +val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
1.289 +term2str eq4b_2;
1.290 +*}
1.291 +
1.292 +ML {*
1.293 +(*solve the simple linear equilation for B TODO: return eq, not list of eq*)
1.294 +val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
1.295 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.296 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.297 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.298 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.299 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.300 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.301 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.302 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.303 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.304 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.305 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.306 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.307 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.308 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.309 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.310 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.311 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.312 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.313 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.314 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.315 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.316 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.317 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.318 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.319 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.320 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.321 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.322 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.323 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.324 +f2str fb;
1.325 +*}
1.326 +
1.327 +ML {* (*check koeffizients*)
1.328 +if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
1.329 +if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
1.330 +*}
1.331 +
1.332 +subsubsection {*substitute expression with solutions*}
1.333 +ML {*
1.334 +*}
1.335 +
1.336 +section {*Implement the Specification and the Method*}
1.337 +text{*==============================================*}
1.338 +subsection{*Define the Specification*}
1.339 +ML {*
1.340 +val thy = @{theory};
1.341 +*}
1.342 +ML {*
1.343 +store_pbt
1.344 + (prep_pbt thy "pbl_SP" [] e_pblID
1.345 + (["SignalProcessing"], [], e_rls, NONE, []));
1.346 +store_pbt
1.347 + (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
1.348 + (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
1.349 +store_pbt
1.350 + (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
1.351 + (["inverse", "Z_Transform", "SignalProcessing"],
1.352 + [("#Given" ,["equality X_eq"]),
1.353 + ("#Find" ,["equality n_eq"])
1.354 + ],
1.355 + append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
1.356 + [["TODO: path to method"]]));
1.357 +
1.358 +show_ptyps();
1.359 +get_pbt ["inverse","Z_Transform","SignalProcessing"];
1.360 +*}
1.361 +
1.362 +subsection{*Define the (Dummy-)Method*}
1.363 +subsection {*Define Name and Signature for the Method*}
1.364 +consts
1.365 + InverseZTransform :: "[bool, bool] => bool"
1.366 + ("((Script InverseZTransform (_ =))// (_))" 9)
1.367 +
1.368 +ML {*
1.369 +store_met
1.370 + (prep_met thy "met_SP" [] e_metID
1.371 + (["SignalProcessing"], [],
1.372 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.373 + crls = e_rls, nrls = e_rls}, "empty_script"));
1.374 +store_met
1.375 + (prep_met thy "met_SP_Ztrans" [] e_metID
1.376 + (["SignalProcessing", "Z_Transform"], [],
1.377 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.378 + crls = e_rls, nrls = e_rls}, "empty_script"));
1.379 +*}
1.380 +ML {*
1.381 +store_met
1.382 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.383 + (["SignalProcessing", "Z_Transform", "inverse"], [],
1.384 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.385 + crls = e_rls, nrls = e_rls},
1.386 + "empty_script"
1.387 + ));
1.388 +*}
1.389 +ML {*(*
1.390 +store_met
1.391 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.392 + (["SignalProcessing", "Z_Transform", "inverse"], [],
1.393 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.394 + crls = e_rls, nrls = e_rls},
1.395 + "Script InverseZTransform (Xeq::bool) =" ^
1.396 + " (let X = Take Xeq;" ^
1.397 + " X = Rewrite ruleZY False X" ^
1.398 + " in X)"
1.399 + ));
1.400 +*)*}
1.401 +ML {*
1.402 +show_mets();
1.403 +get_met ["SignalProcessing","Z_Transform","inverse"];
1.404 +*}
1.405 +
1.406 +
1.407 +section {*Program in CTP-based language*}
1.408 +text{*=================================*}
1.409 +subsection {*Stepwise extend Program*}
1.410 +ML {*
1.411 +val str =
1.412 +"Script InverseZTransform (Xeq::bool) =" ^
1.413 +" Xeq";
1.414 +*}
1.415 +ML {*
1.416 +val str =
1.417 +"Script InverseZTransform (Xeq::bool) =" ^
1.418 +" (let X = Take Xeq;" ^
1.419 +" X = Rewrite ruleZY False X" ^
1.420 +" in X)";
1.421 +*}
1.422 +ML {*
1.423 +val thy = @{theory};
1.424 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.425 +*}
1.426 +ML {*
1.427 +term2str sc;
1.428 +atomty sc
1.429 +*}
1.430 +
1.431 +subsection {*Stepwise Execute the Program*}
1.432 +
1.433 +
1.434 +
1.435 +
1.436 +
1.437 +
1.438 +
1.439 +
1.440 +section {*Write Tests for Crucial Details*}
1.441 +text{*===================================*}
1.442 +ML {*
1.443 +
1.444 +*}
1.445 +
1.446 +section {*Integrate Program into Knowledge*}
1.447 +ML {*
1.448 +
1.449 +*}
1.450 +
1.451 +end
1.452 +