1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Apr 10 18:32:36 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 - UnparseC.term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.8 + UnparseC.term @{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 - UnparseC.term2str @{term "\<rho> "};
1.17 + UnparseC.term @{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 - UnparseC.term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.26 + UnparseC.term 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 - UnparseC.term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.35 + UnparseC.term t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.36 (*- real *)
1.37 - UnparseC.term2str t;
1.38 + UnparseC.term 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 - UnparseC.term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.43 + UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.44 (*- real *)
1.45 - UnparseC.term2str t;
1.46 + UnparseC.term 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 - UnparseC.term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.51 + UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.52 (*- real *)
1.53 - UnparseC.term2str t;
1.54 + UnparseC.term t;
1.55 \<close>
1.56 -ML \<open>UnparseC.terms2str (asm1 @ asm2 @ asm3);\<close>
1.57 +ML \<open>UnparseC.terms (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)"; UnparseC.term2str fun1;
1.66 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; UnparseC.term fun1;
1.67 val SOME fun1' =
1.68 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term2str fun1';
1.69 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term 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; UnparseC.term2str fun2;
1.78 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; UnparseC.term fun2;
1.79 val SOME (fun2', asm1) =
1.80 - Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term2str fun2';
1.81 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term fun2';
1.82
1.83 val SOME (fun3,_) =
1.84 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
1.85 - UnparseC.term2str fun3;
1.86 + UnparseC.term 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 - UnparseC.term2str fun3';
1.94 + UnparseC.term 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'; UnparseC.term2str expr;
1.103 + val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr;
1.104 val (_, denom) =
1.105 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
1.106 - UnparseC.term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.107 + UnparseC.term 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 (UnparseC.term_to_string''' thy denom) "",
1.116 + SOME (TermC.mk_thmid thmid (UnparseC.term_thy 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 (UnparseC.term_to_string''' thy num) "",
1.125 + SOME (TermC.mk_thmid thmid (UnparseC.term_thy 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 - UnparseC.term2str solutions;
1.134 + UnparseC.term 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 - UnparseC.term2str s_1;
1.143 - UnparseC.term2str s_2;
1.144 + UnparseC.term s_1;
1.145 + UnparseC.term 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 - UnparseC.term2str s_1';
1.154 - UnparseC.term2str s_2';
1.155 + UnparseC.term s_1';
1.156 + UnparseC.term s_2';
1.157 \<close>
1.158
1.159 text \<open>\noindent For the programming language a function collecting all the
1.160 @@ -404,17 +404,17 @@
1.161 (*mk_prod TermC.empty [];*)
1.162
1.163 val prod = mk_prod TermC.empty [str2term "x + 123"];
1.164 -UnparseC.term2str prod = "x + 123";
1.165 +UnparseC.term prod = "x + 123";
1.166
1.167 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
1.168 val sols = HOLogic.dest_list sol;
1.169 val facs = map fac_from_sol sols;
1.170 val prod = mk_prod TermC.empty facs;
1.171 -UnparseC.term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.172 +UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.173
1.174 val prod =
1.175 mk_prod TermC.empty [str2term "x + 1", str2term "x + 2", str2term "x + 3"];
1.176 -UnparseC.term2str prod = "(x + 1) * (x + 2) * (x + 3)";
1.177 +UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)";
1.178 *} *)
1.179 ML \<open>
1.180 fun factors_from_solution sol =
1.181 @@ -424,7 +424,7 @@
1.182 (* ML {*
1.183 val sol = str2term "[z = 1 / 2, z = -1 / 4]";
1.184 val fs = factors_from_solution sol;
1.185 -UnparseC.term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.186 +UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.187 *} *)
1.188 text \<open>\noindent This function needs to be packed such that it can be evaluated
1.189 by the Lucas-Interpreter. Therefor we moved the function to the
1.190 @@ -440,7 +440,7 @@
1.191 fun eval_factors_from_solution (thmid:string) _
1.192 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
1.193 thy = ((let val prod = factors_from_solution sol
1.194 - in SOME (mk_thmid thmid "" (UnparseC.term_to_string''' thy prod) "",
1.195 + in SOME (mk_thmid thmid "" (UnparseC.term_thy thy prod) "",
1.196 Trueprop $ (mk_equality (t, prod)))
1.197 end)
1.198 handle _ => NONE)
1.199 @@ -588,7 +588,7 @@
1.200
1.201 val expr' = HOLogic.mk_binop
1.202 "Rings.divide_class.divide" (numerator, denominator');
1.203 - UnparseC.term2str expr';
1.204 + UnparseC.term expr';
1.205 \<close>
1.206
1.207 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
1.208 @@ -618,9 +618,9 @@
1.209 val SOME (t1,_) =
1.210 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.211 @{thm ansatz_2nd_order} expr';
1.212 - UnparseC.term2str t1; atomty t1;
1.213 + UnparseC.term t1; atomty t1;
1.214 val eq1 = HOLogic.mk_eq (expr', t1);
1.215 - UnparseC.term2str eq1;
1.216 + UnparseC.term eq1;
1.217 \<close>
1.218
1.219 text\<open>\noindent Eliminate the denominators by multiplying the left and the
1.220 @@ -633,7 +633,7 @@
1.221 val SOME (eq2,_) =
1.222 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.223 @{thm equival_trans_2nd_order} eq1;
1.224 - UnparseC.term2str eq2;
1.225 + UnparseC.term eq2;
1.226 \<close>
1.227
1.228 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
1.229 @@ -641,7 +641,7 @@
1.230
1.231 ML \<open>
1.232 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
1.233 - UnparseC.term2str eq3;
1.234 + UnparseC.term eq3;
1.235 (*
1.236 * ?A ?B not simplified
1.237 *)
1.238 @@ -660,9 +660,9 @@
1.239 *)
1.240 val SOME (fract2,_) =
1.241 rewrite_set_ @{theory} false norm_Rational fract1;
1.242 - UnparseC.term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.243 + UnparseC.term fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.244 (*
1.245 - * UnparseC.term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.246 + * UnparseC.term fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.247 * would be more traditional...
1.248 *)
1.249 \<close>
1.250 @@ -675,13 +675,13 @@
1.251 (*
1.252 * A B !
1.253 *)
1.254 - UnparseC.term2str eq3';
1.255 + UnparseC.term eq3';
1.256 (*
1.257 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
1.258 *)
1.259 val SOME (eq3'' ,_) =
1.260 rewrite_set_ @{theory} false norm_Rational eq3';
1.261 - UnparseC.term2str eq3'';
1.262 + UnparseC.term eq3'';
1.263 \<close>
1.264
1.265 text\<open>\noindent Still working at {\sisac}\ldots\<close>
1.266 @@ -717,8 +717,8 @@
1.267 text\<open>\noindent And check the output\ldots\<close>
1.268
1.269 ML \<open>
1.270 - UnparseC.term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.271 - UnparseC.term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.272 + UnparseC.term expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.273 + UnparseC.term ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.274 \<close>
1.275
1.276 subsubsection \<open>Get the First Coefficient\<close>
1.277 @@ -733,10 +733,10 @@
1.278 ML \<open>
1.279 val SOME (eq4_1,_) =
1.280 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
1.281 - UnparseC.term2str eq4_1;
1.282 + UnparseC.term eq4_1;
1.283 val SOME (eq4_2,_) =
1.284 rewrite_set_ @{theory} false norm_Rational eq4_1;
1.285 - UnparseC.term2str eq4_2;
1.286 + UnparseC.term eq4_2;
1.287
1.288 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
1.289 val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.290 @@ -813,10 +813,10 @@
1.291 ML \<open>
1.292 val SOME (eq4b_1,_) =
1.293 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
1.294 - UnparseC.term2str eq4b_1;
1.295 + UnparseC.term eq4b_1;
1.296 val SOME (eq4b_2,_) =
1.297 rewrite_set_ @{theory} false norm_Rational eq4b_1;
1.298 - UnparseC.term2str eq4b_2;
1.299 + UnparseC.term eq4b_2;
1.300
1.301 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
1.302 val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.303 @@ -1310,7 +1310,7 @@
1.304 (#scr o get_met) ["SignalProcessing",
1.305 "Z_Transform",
1.306 "Inverse"];
1.307 - writeln (UnparseC.term2str s);
1.308 + writeln (UnparseC.term s);
1.309 \end{verbatim}
1.310 \ldots shows the right script. Difference in the arguments.
1.311 \item Test --- Why helpless here ? --- shows: \ttfamily replace