1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Feb 04 16:49:08 2023 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Feb 04 17:00:25 2023 +0100
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.term_in_ctxt @{context} @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
1.8 + UnparseC.term @{context} @{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.term_in_ctxt @{context} @{term "\<rho> "};
1.17 + UnparseC.term @{context} @{term "\<rho> "};
1.18 \<close>
1.19
1.20 subsection \<open>Rules\<close>
1.21 @@ -85,7 +85,7 @@
1.22 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
1.23 (*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
1.24 \<close> ML \<open>
1.25 - UnparseC.term_in_ctxt @{context} t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.26 + UnparseC.term @{context} 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 @@ -97,23 +97,23 @@
1.31 ML \<open>
1.32 val SOME (t, asm1) =
1.33 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule3}) t;
1.34 - UnparseC.term_in_ctxt @{context} t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.35 + UnparseC.term @{context} t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.36 (*- real *)
1.37 - UnparseC.term_in_ctxt @{context} t;
1.38 + UnparseC.term @{context} t;
1.39
1.40 val SOME (t, asm2) =
1.41 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
1.42 - UnparseC.term_in_ctxt @{context} t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
1.43 + UnparseC.term @{context} t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
1.44 (*- real *)
1.45 - UnparseC.term_in_ctxt @{context} t;
1.46 + UnparseC.term @{context} t;
1.47
1.48 val SOME (t, asm3) =
1.49 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
1.50 - UnparseC.term_in_ctxt @{context} t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
1.51 + UnparseC.term @{context} t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
1.52 (*- real *)
1.53 - UnparseC.term_in_ctxt @{context} t;
1.54 + UnparseC.term @{context} t;
1.55 \<close>
1.56 -ML \<open>UnparseC.terms_in_ctxt @{context} (asm1 @ asm2 @ asm3);\<close>
1.57 +ML \<open>UnparseC.terms @{context} (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 @@ -134,9 +134,9 @@
1.62 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
1.63
1.64 val fun1 =
1.65 - TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term_in_ctxt ctxt fun1;
1.66 + TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term ctxt fun1;
1.67 val fun1' =
1.68 - TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term_in_ctxt ctxt fun1';
1.69 + TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term ctxt fun1';
1.70 \<close>
1.71
1.72 subsubsection \<open>Prepare Numerator and Denominator\<close>
1.73 @@ -151,20 +151,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.term_in_ctxt @{context} fun2;
1.78 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; UnparseC.term @{context} fun2;
1.79 val SOME (fun2', asm1) =
1.80 - Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term_in_ctxt @{context} fun2';
1.81 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; UnparseC.term @{context} fun2';
1.82
1.83 val SOME (fun3,_) =
1.84 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
1.85 - UnparseC.term_in_ctxt @{context} fun3;
1.86 + UnparseC.term @{context} fun3;
1.87 (*
1.88 * Fails on x \<up> (-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.term_in_ctxt @{context} fun3';
1.94 + UnparseC.term @{context} fun3';
1.95 (*
1.96 * OK - workaround!
1.97 *)
1.98 @@ -183,10 +183,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.term_in_ctxt @{context} expr;
1.103 + val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term @{context} expr;
1.104 val (_, denom) =
1.105 HOLogic.dest_bin \<^const_name>\<open>divide\<close> (type_of expr) expr;
1.106 - UnparseC.term_in_ctxt @{context} denom = "-1 + -2 * z + 8 * z \<up> 2";
1.107 + UnparseC.term @{context} denom = "-1 + -2 * z + 8 * z \<up> 2";
1.108 \<close>
1.109
1.110 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.111 @@ -337,7 +337,7 @@
1.112
1.113 ML \<open>
1.114 val SOME solutions = ParseC.term_opt ctxt "[z=1/2, z=-1/4]";
1.115 - UnparseC.term_in_ctxt @{context} solutions;
1.116 + UnparseC.term @{context} solutions;
1.117 TermC.atom_trace_detail @{context} solutions;
1.118 \<close>
1.119
1.120 @@ -352,8 +352,8 @@
1.121 ML \<open>
1.122 val Const (\<^const_name>\<open>Cons\<close>, _) $ s_1 $ (Const (\<^const_name>\<open>Cons\<close>, _)
1.123 $ s_2 $ Const (\<^const_name>\<open>Nil\<close>, _)) = solutions;
1.124 - UnparseC.term_in_ctxt @{context} s_1;
1.125 - UnparseC.term_in_ctxt @{context} s_2;
1.126 + UnparseC.term @{context} s_1;
1.127 + UnparseC.term @{context} s_2;
1.128 \<close>
1.129
1.130 text\<open>\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
1.131 @@ -371,8 +371,8 @@
1.132 val s_1' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
1.133 val xx = HOLogic.dest_eq s_2;
1.134 val s_2' = HOLogic.mk_binop \<^const_name>\<open>minus\<close> xx;
1.135 - UnparseC.term_in_ctxt @{context} s_1';
1.136 - UnparseC.term_in_ctxt @{context} s_2';
1.137 + UnparseC.term @{context} s_1';
1.138 + UnparseC.term @{context} s_2';
1.139 \<close>
1.140
1.141 text \<open>\noindent For the programming language a function collecting all the
1.142 @@ -409,17 +409,17 @@
1.143 (*mk_prod TermC.empty [];*)
1.144
1.145 val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"];
1.146 -UnparseC.term_in_ctxt @{context} prod = "x + 123";
1.147 +UnparseC.term @{context} prod = "x + 123";
1.148
1.149 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
1.150 val sols = HOLogic.dest_list sol;
1.151 val facs = map fac_from_sol sols;
1.152 val prod = mk_prod TermC.empty facs;
1.153 -UnparseC.term_in_ctxt @{context} prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.154 +UnparseC.term @{context} prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
1.155
1.156 val prod =
1.157 mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"];
1.158 -UnparseC.term_in_ctxt @{context} prod = "(x + 1) * (x + 2) * (x + 3)";
1.159 +UnparseC.term @{context} prod = "(x + 1) * (x + 2) * (x + 3)";
1.160 *} *)
1.161 ML \<open>
1.162 fun factors_from_solution sol =
1.163 @@ -429,7 +429,7 @@
1.164 (* ML {*
1.165 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
1.166 val fs = factors_from_solution sol;
1.167 -UnparseC.term_in_ctxt @{context} fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.168 +UnparseC.term @{context} fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
1.169 *} *)
1.170 text \<open>\noindent This function needs to be packed such that it can be evaluated
1.171 by the Lucas-Interpreter. Therefor we moved the function to the
1.172 @@ -592,7 +592,7 @@
1.173
1.174 val expr' = HOLogic.mk_binop
1.175 \<^const_name>\<open>divide\<close> (numerator, denominator');
1.176 - UnparseC.term_in_ctxt @{context} expr';
1.177 + UnparseC.term @{context} expr';
1.178 \<close>
1.179
1.180 subsubsection \<open>Apply the Partial Fraction Decomposion Ansatz\<close>
1.181 @@ -622,9 +622,9 @@
1.182 val SOME (t1,_) =
1.183 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.184 @{thm ansatz_2nd_order} expr';
1.185 - UnparseC.term_in_ctxt @{context} t1; TermC.atom_trace_detail @{context} t1;
1.186 + UnparseC.term @{context} t1; TermC.atom_trace_detail @{context} t1;
1.187 val eq1 = HOLogic.mk_eq (expr', t1);
1.188 - UnparseC.term_in_ctxt @{context} eq1;
1.189 + UnparseC.term @{context} eq1;
1.190 \<close>
1.191
1.192 text\<open>\noindent Eliminate the denominators by multiplying the left and the
1.193 @@ -637,7 +637,7 @@
1.194 val SOME (eq2,_) =
1.195 rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.196 @{thm equival_trans_2nd_order} eq1;
1.197 - UnparseC.term_in_ctxt @{context} eq2;
1.198 + UnparseC.term @{context} eq2;
1.199 \<close>
1.200
1.201 text\<open>\noindent We use the existing ruleset \ttfamily norm\_Rational \normalfont
1.202 @@ -645,7 +645,7 @@
1.203
1.204 ML \<open>
1.205 val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
1.206 - UnparseC.term_in_ctxt @{context} eq3;
1.207 + UnparseC.term @{context} eq3;
1.208 (*
1.209 * ?A ?B not simplified
1.210 *)
1.211 @@ -664,9 +664,9 @@
1.212 *)
1.213 val SOME (fract2,_) =
1.214 rewrite_set_ @{theory} false norm_Rational fract1;
1.215 - UnparseC.term_in_ctxt @{context} fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.216 + UnparseC.term @{context} fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
1.217 (*
1.218 - * UnparseC.term_in_ctxt @{context} fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.219 + * UnparseC.term @{context} fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
1.220 * would be more traditional...
1.221 *)
1.222 \<close>
1.223 @@ -679,13 +679,13 @@
1.224 (*
1.225 * A B !
1.226 *)
1.227 - UnparseC.term_in_ctxt @{context} eq3';
1.228 + UnparseC.term @{context} eq3';
1.229 (*
1.230 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
1.231 *)
1.232 val SOME (eq3'' ,_) =
1.233 rewrite_set_ @{theory} false norm_Rational eq3';
1.234 - UnparseC.term_in_ctxt @{context} eq3'';
1.235 + UnparseC.term @{context} eq3'';
1.236 \<close>
1.237
1.238 text\<open>\noindent Still working at {\sisac}\ldots\<close>
1.239 @@ -721,8 +721,8 @@
1.240 text\<open>\noindent And check the output\ldots\<close>
1.241
1.242 ML \<open>
1.243 - UnparseC.term_in_ctxt @{context} expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.244 - UnparseC.term_in_ctxt @{context} ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.245 + UnparseC.term @{context} expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";
1.246 + UnparseC.term @{context} ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.247 \<close>
1.248
1.249 subsubsection \<open>Get the First Coefficient\<close>
1.250 @@ -737,10 +737,10 @@
1.251 ML \<open>
1.252 val SOME (eq4_1,_) =
1.253 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
1.254 - UnparseC.term_in_ctxt @{context} eq4_1;
1.255 + UnparseC.term @{context} eq4_1;
1.256 val SOME (eq4_2,_) =
1.257 rewrite_set_ @{theory} false norm_Rational eq4_1;
1.258 - UnparseC.term_in_ctxt @{context} eq4_2;
1.259 + UnparseC.term @{context} eq4_2;
1.260
1.261 val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
1.262 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.263 @@ -817,10 +817,10 @@
1.264 ML \<open>
1.265 val SOME (eq4b_1,_) =
1.266 rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
1.267 - UnparseC.term_in_ctxt @{context} eq4b_1;
1.268 + UnparseC.term @{context} eq4b_1;
1.269 val SOME (eq4b_2,_) =
1.270 rewrite_set_ @{theory} false norm_Rational eq4b_1;
1.271 - UnparseC.term_in_ctxt @{context} eq4b_2;
1.272 + UnparseC.term @{context} eq4b_2;
1.273
1.274 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
1.275 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.276 @@ -1314,7 +1314,7 @@
1.277 (#program o MethodC.from_store ctxt) ["SignalProcessing",
1.278 "Z_Transform",
1.279 "Inverse"];
1.280 - writeln (UnparseC.term_in_ctxt @{context} s);
1.281 + writeln (UnparseC.term @{context} s);
1.282 \end{verbatim}
1.283 \ldots shows the right script. Difference in the arguments.
1.284 \item Test --- Why helpless here ? --- shows: \ttfamily replace