1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 09 17:13:17 2020 +0200
1.3 @@ -35,7 +35,7 @@
1.4 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)
1.5 @{term "z /(z - 1) = -u [-n - 1]"};
1.6 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.7 - term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.8 + UnparseC.term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.9 \<close>
1.10 text\<open>\noindent Try which symbols we are able to use and how we generate them.\<close>
1.11 ML \<open>
1.12 @@ -44,7 +44,7 @@
1.13 @{term "\<delta> "};
1.14 @{term "\<phi> "};
1.15 @{term "\<rho> "};
1.16 - term2str @{term "\<rho> "};
1.17 + UnparseC.term2str @{term "\<rho> "};
1.18 \<close>
1.19
1.20 subsection \<open>Rules\<close>
1.21 @@ -81,7 +81,7 @@
1.22
1.23 val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.24 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
1.25 - term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.26 + UnparseC.term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.27 (*
1.28 * Attention rule1 is applied before the expression is
1.29 * checked for rule4 which would be correct!!!
1.30 @@ -92,23 +92,23 @@
1.31 ML \<open>
1.32 val SOME (t, asm1) =
1.33 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
1.34 - term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.35 + UnparseC.term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.36 (*- real *)
1.37 - term2str t;
1.38 + UnparseC.term2str t;
1.39
1.40 val SOME (t, asm2) =
1.41 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule4}) t;
1.42 - term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.43 + UnparseC.term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.44 (*- real *)
1.45 - term2str t;
1.46 + UnparseC.term2str t;
1.47
1.48 val SOME (t, asm3) =
1.49 Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;
1.50 - term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.51 + UnparseC.term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.52 (*- real *)
1.53 - term2str t;
1.54 + UnparseC.term2str t;
1.55 \<close>
1.56 -ML \<open>terms2str (asm1 @ asm2 @ asm3);\<close>
1.57 +ML \<open>UnparseC.terms2str (asm1 @ asm2 @ asm3);\<close>
1.58
1.59 section\<open>Prepare Steps for TP-based programming Language\label{sec:prepstep}\<close>
1.60 text\<open>
1.61 @@ -129,9 +129,9 @@
1.62 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
1.63
1.64 val SOME fun1 =
1.65 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.66 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; UnparseC.term2str fun1;
1.67 val SOME fun1' =
1.68 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.69 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term2str fun1';
1.70 \<close>
1.71
1.72 subsubsection \<open>Prepare Numerator and Denominator\<close>
1.73 @@ -146,20 +146,20 @@
1.74 ML \<open>
1.75 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.76 val SOME (fun2, asm1) =
1.77 - Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.78 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; UnparseC.term2str fun2;
1.79 val SOME (fun2', asm1) =
1.80 - Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.81 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term2str fun2';
1.82
1.83 val SOME (fun3,_) =
1.84 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
1.85 - term2str fun3;
1.86 + UnparseC.term2str fun3;
1.87 (*
1.88 * Fails on x^^^(-1)
1.89 * We solve this problem by using 1/x as a workaround.
1.90 *)
1.91 val SOME (fun3',_) =
1.92 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
1.93 - term2str fun3';
1.94 + UnparseC.term2str fun3';
1.95 (*
1.96 * OK - workaround!
1.97 *)
1.98 @@ -178,10 +178,10 @@
1.99
1.100 subsubsection\<open>Decompose the Given Term Into lhs and rhs\<close>
1.101 ML \<open>
1.102 - val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
1.103 + val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term2str expr;
1.104 val (_, denom) =
1.105 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
1.106 - term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.107 + UnparseC.term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.108 \<close>
1.109
1.110 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.111 @@ -216,7 +216,7 @@
1.112 (t as Const ("Rational.get_denominator", _) $
1.113 (Const ("Rings.divide_class.divide", _) $num
1.114 $denom)) thy =
1.115 - SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
1.116 + SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy denom) "",
1.117 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.118 | eval_get_denominator _ _ _ _ = NONE;
1.119 \<close>
1.120 @@ -236,7 +236,7 @@
1.121 (t as Const ("Rational.get_numerator", _) $
1.122 (Const ("Rings.divide_class.divide", _) $num
1.123 $denom )) thy =
1.124 - SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
1.125 + SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy num) "",
1.126 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.127 | eval_get_numerator _ _ _ _ = NONE;
1.128 \<close>
1.129 @@ -332,7 +332,7 @@
1.130
1.131 ML \<open>
1.132 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
1.133 - term2str solutions;
1.134 + UnparseC.term2str solutions;
1.135 atomty solutions;
1.136 \<close>
1.137
1.138 @@ -347,8 +347,8 @@
1.139 ML \<open>
1.140 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
1.141 $ s_2 $ Const ("List.list.Nil", _)) = solutions;
1.142 - term2str s_1;
1.143 - term2str s_2;
1.144 + UnparseC.term2str s_1;
1.145 + UnparseC.term2str s_2;
1.146 \<close>
1.147
1.148 text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
1.149 @@ -366,8 +366,8 @@
1.150 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.151 val xx = HOLogic.dest_eq s_2;
1.152 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
1.153 - term2str s_1';
1.154 - term2str s_2';
1.155 + UnparseC.term2str s_1';
1.156 + UnparseC.term2str s_2';
1.157 \<close>
1.158
1.159 text \<open>\noindent For the programming language a function collecting all the
1.160 @@ -381,15 +381,15 @@
1.161
1.162 ML \<open>
1.163 fun mk_prod prod [] =
1.164 - if prod = e_term
1.165 + if prod = TermC.empty
1.166 then error "mk_prod called with []"
1.167 else prod
1.168 | mk_prod prod (t :: []) =
1.169 - if prod = e_term
1.170 + if prod = TermC.empty
1.171 then t
1.172 else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
1.173 | mk_prod prod (t1 :: t2 :: ts) =
1.174 - if prod = e_term
1.175 + if prod = TermC.empty
1.176 then
1.177 let val p =
1.178 HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
1.179 @@ -401,30 +401,30 @@
1.180 \<close>
1.181 (* ML {*
1.182 probably keep these test in test/Tools/isac/...
1.183 -(*mk_prod e_term [];*)
1.184 +(*mk_prod TermC.empty [];*)
1.185
1.186 -val prod = mk_prod e_term [str2term "x + 123"];
1.187 -term2str prod = "x + 123";
1.188 +val prod = mk_prod TermC.empty [str2term "x + 123"];
1.189 +UnparseC.term2str prod = "x + 123";
1.190
1.191 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
1.192 val sols = HOLogic.dest_list sol;
1.193 val facs = map fac_from_sol sols;
1.194 -val prod = mk_prod e_term facs;
1.195 -term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.196 +val prod = mk_prod TermC.empty facs;
1.197 +UnparseC.term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.198
1.199 val prod =
1.200 - mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
1.201 -term2str prod = "(x + 1) * (x + 2) * (x + 3)";
1.202 + mk_prod TermC.empty [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
1.203 +UnparseC.term2str prod = "(x + 1) * (x + 2) * (x + 3)";
1.204 *} *)
1.205 ML \<open>
1.206 fun factors_from_solution sol =
1.207 let val ts = HOLogic.dest_list sol
1.208 - in mk_prod e_term (map fac_from_sol ts) end;
1.209 + in mk_prod TermC.empty (map fac_from_sol ts) end;
1.210 \<close>
1.211 (* ML {*
1.212 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
1.213 val fs = factors_from_solution sol;
1.214 -term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.215 +UnparseC.term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.216 *} *)
1.217 text \<open>\noindent This function needs to be packed such that it can be evaluated
1.218 by the Lucas-Interpreter. Therefor we moved the function to the
1.219 @@ -440,7 +440,7 @@
1.220 fun eval_factors_from_solution (thmid:string) _
1.221 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
1.222 thy = ((let val prod = factors_from_solution sol
1.223 - in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
1.224 + in SOME (mk_thmid thmid "" (UnparseC.term_to_string''' thy prod) "",
1.225 Trueprop $ (mk_equality (t, prod)))
1.226 end)
1.227 handle _ => NONE)
1.228 @@ -588,7 +588,7 @@
1.229
1.230 val expr' = HOLogic.mk_binop
1.231 "Rings.divide_class.divide" (numerator, denominator');
1.232 - term2str expr';
1.233 + UnparseC.term2str expr';
1.234 \<close>
1.235
1.236 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
1.237 @@ -618,9 +618,9 @@
1.238 val SOME (t1,_) =
1.239 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.240 @{thm ansatz_2nd_order} expr';
1.241 - term2str t1; atomty t1;
1.242 + UnparseC.term2str t1; atomty t1;
1.243 val eq1 = HOLogic.mk_eq (expr', t1);
1.244 - term2str eq1;
1.245 + UnparseC.term2str eq1;
1.246 \<close>
1.247
1.248 text\<open>\noindent Eliminate the denominators by multiplying the left and the
1.249 @@ -633,7 +633,7 @@
1.250 val SOME (eq2,_) =
1.251 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.252 @{thm equival_trans_2nd_order} eq1;
1.253 - term2str eq2;
1.254 + UnparseC.term2str eq2;
1.255 \<close>
1.256
1.257 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
1.258 @@ -641,7 +641,7 @@
1.259
1.260 ML \<open>
1.261 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
1.262 - term2str eq3;
1.263 + UnparseC.term2str eq3;
1.264 (*
1.265 * ?A ?B not simplified
1.266 *)
1.267 @@ -660,9 +660,9 @@
1.268 *)
1.269 val SOME (fract2,_) =
1.270 rewrite_set_ @{theory} false norm_Rational fract1;
1.271 - term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.272 + UnparseC.term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.273 (*
1.274 - * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.275 + * UnparseC.term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.276 * would be more traditional...
1.277 *)
1.278 \<close>
1.279 @@ -675,13 +675,13 @@
1.280 (*
1.281 * A B !
1.282 *)
1.283 - term2str eq3';
1.284 + UnparseC.term2str eq3';
1.285 (*
1.286 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
1.287 *)
1.288 val SOME (eq3'' ,_) =
1.289 rewrite_set_ @{theory} false norm_Rational eq3';
1.290 - term2str eq3'';
1.291 + UnparseC.term2str eq3'';
1.292 \<close>
1.293
1.294 text\<open>\noindent Still working at {\sisac}\ldots\<close>
1.295 @@ -717,8 +717,8 @@
1.296 text\<open>\noindent And check the output\ldots\<close>
1.297
1.298 ML \<open>
1.299 - term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.300 - term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.301 + UnparseC.term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.302 + UnparseC.term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.303 \<close>
1.304
1.305 subsubsection \<open>Get the First Coefficient\<close>
1.306 @@ -733,10 +733,10 @@
1.307 ML \<open>
1.308 val SOME (eq4_1,_) =
1.309 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
1.310 - term2str eq4_1;
1.311 + UnparseC.term2str eq4_1;
1.312 val SOME (eq4_2,_) =
1.313 rewrite_set_ @{theory} false norm_Rational eq4_1;
1.314 - term2str eq4_2;
1.315 + UnparseC.term2str eq4_2;
1.316
1.317 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
1.318 val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.319 @@ -813,10 +813,10 @@
1.320 ML \<open>
1.321 val SOME (eq4b_1,_) =
1.322 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
1.323 - term2str eq4b_1;
1.324 + UnparseC.term2str eq4b_1;
1.325 val SOME (eq4b_2,_) =
1.326 rewrite_set_ @{theory} false norm_Rational eq4b_1;
1.327 - term2str eq4b_2;
1.328 + UnparseC.term2str eq4b_2;
1.329
1.330 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
1.331 val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.332 @@ -1310,7 +1310,7 @@
1.333 (#scr o get_met) ["SignalProcessing",
1.334 "Z_Transform",
1.335 "Inverse"];
1.336 - writeln (term2str s);
1.337 + writeln (UnparseC.term2str s);
1.338 \end{verbatim}
1.339 \ldots shows the right script. Difference in the arguments.
1.340 \item Test --- Why helpless here ? --- shows: \ttfamily replace