1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -56,9 +56,9 @@
1.4 rule1: "1 = \<delta>[n]" and
1.5 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
1.6 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
1.7 - rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
1.8 - rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
1.9 - rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
1.10 + rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha> \<up> n * u [n]" and
1.11 + rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
1.12 + rule6: "|| z || > 1 ==> z/(z - 1) \<up> 2 = n * u [n]"
1.13
1.14 text\<open>\noindent Check the rules for their correct notation.
1.15 (See the machine output.)\<close>
1.16 @@ -98,13 +98,13 @@
1.17
1.18 val SOME (t, asm2) =
1.19 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule4}) t;
1.20 - UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.21 + UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + 1";
1.22 (*- real *)
1.23 UnparseC.term t;
1.24
1.25 val SOME (t, asm3) =
1.26 Rewrite.rewrite_ thy ro er true (ThmC.numerals_to_Free @{thm rule1}) t;
1.27 - UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.28 + UnparseC.term t = "- ?u [- ?n - 1] + \<alpha> \<up> ?n * ?u [?n] + ?\<delta> [?n]";
1.29 (*- real *)
1.30 UnparseC.term t;
1.31 \<close>
1.32 @@ -129,7 +129,7 @@
1.33 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
1.34
1.35 val SOME fun1 =
1.36 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; UnparseC.term fun1;
1.37 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
1.38 val SOME fun1' =
1.39 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1';
1.40 \<close>
1.41 @@ -154,7 +154,7 @@
1.42 Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
1.43 UnparseC.term fun3;
1.44 (*
1.45 - * Fails on x^^^(-1)
1.46 + * Fails on x \<up> (-1)
1.47 * We solve this problem by using 1/x as a workaround.
1.48 *)
1.49 val SOME (fun3',_) =
1.50 @@ -181,7 +181,7 @@
1.51 val (_, expr) = HOLogic.dest_eq fun3'; UnparseC.term expr;
1.52 val (_, denom) =
1.53 HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
1.54 - UnparseC.term denom = "-1 + -2 * z + 8 * z ^^^ 2";
1.55 + UnparseC.term denom = "-1 + -2 * z + 8 * z \<up> 2";
1.56 \<close>
1.57
1.58 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.59 @@ -257,8 +257,8 @@
1.60 for this equation type. Later on {\sisac} should determine the type
1.61 of the given equation self.\<close>
1.62 ML \<open>
1.63 - val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
1.64 - val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
1.65 + val denominator = TermC.parseNEW ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
1.66 + val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
1.67 "solveFor z",
1.68 "solutions L"];
1.69 val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.70 @@ -274,9 +274,9 @@
1.71
1.72 ML \<open>
1.73 Context.theory_name thy = "Isac_Knowledge";
1.74 - val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
1.75 + val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
1.76 val fmz = (*specification*)
1.77 - ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
1.78 + ["equality (-1 + -2 * z + 8 * z \<up> 2 = (0::real))",(*equality*)
1.79 "solveFor z", (*bound variable*)
1.80 "solutions L"]; (*identifier for
1.81 solution*)
1.82 @@ -480,11 +480,11 @@
1.83 SignalProcessing])),
1.84 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
1.85 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
1.86 - (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
1.87 - (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.88 - (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
1.89 - (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)|
1.90 - z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
1.91 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2)),
1.92 + (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
1.93 + (([3,1], Frm), -1 + -2 * z + 8 * z \<up> 2 = 0),
1.94 + (([3,1], Res), z = (- -2 + sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)|
1.95 + z = (- -2 - sqrt (-2 \<up> 2 - 4 * 8 * -1)) / (2 * 8)),
1.96 (([3,2], Res), z = 1 / 2 | z = -1 / 4),
1.97 (([3,3], Res), [ z = 1 / 2, z = -1 / 4]),
1.98 (([3,4], Res), [ z = 1 / 2, z = -1 / 4]),
1.99 @@ -495,7 +495,7 @@
1.100 \par \noindent In particular that:
1.101
1.102 \begin{verbatim}
1.103 - (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.104 + (([3], Pbl), solve (-1 + -2 * z + 8 * z \<up> 2 = 0, z)),
1.105 \end{verbatim}
1.106 \par \noindent Shows the equation which has been created in
1.107 the program by:
1.108 @@ -998,7 +998,7 @@
1.109 val str =
1.110 "Program InverseZTransform (Xeq::bool) = "^
1.111 (*
1.112 - * 1/z) instead of z ^^^ -1
1.113 + * 1/z) instead of z \<up> -1
1.114 *)
1.115 " (let X = Take Xeq; "^
1.116 " X' = Rewrite ruleZY False X; "^
1.117 @@ -1015,7 +1015,7 @@
1.118 *)
1.119 "Program InverseZTransform (Xeq::bool) = "^
1.120 (*
1.121 - * (1/z) instead of z ^^^ -1
1.122 + * (1/z) instead of z \<up> -1
1.123 *)
1.124 " (let X = Take Xeq; "^
1.125 " X' = Rewrite ruleZY False X; "^
1.126 @@ -1129,7 +1129,7 @@
1.127 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.128 errpats = [], nrls = Rule_Set.empty},
1.129 "Program InverseZTransform (X_eq::bool) = "^
1.130 - (*(1/z) instead of z ^^^ -1*)
1.131 + (*(1/z) instead of z \<up> -1*)
1.132 "(let X = Take X_eq; "^
1.133 " X' = Rewrite ruleZY False X; "^
1.134 (*z * denominator*)
1.135 @@ -1285,7 +1285,7 @@
1.136 \ttfamily Empty\_Tac; \normalfont the search for the reason considered
1.137 the following points:\begin{itemize}
1.138 \item What shows \ttfamily show\_pt pt;\normalfont\ldots?
1.139 -\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2))]\end{verbatim}
1.140 +\begin{verbatim}(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z \<up> 2))]\end{verbatim}
1.141 The calculation is ok but no \ttfamily next \normalfont step found:
1.142 Should be\\ \ttfamily nxt = Subproblem\normalfont!
1.143 \item What shows \ttfamily trace\_script := true; \normalfont we read
1.144 @@ -1335,7 +1335,7 @@
1.145
1.146 ML \<open>
1.147 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.148 - (*Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";*)
1.149 + (*Add_Given equality (-1 + -2 * z + 8 * z \<up> 2 = 0)";*)
1.150 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.151 (*Add_Given solveFor z";*)
1.152 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.153 @@ -1355,7 +1355,7 @@
1.154 print_depth 999; f; print_depth 3;
1.155 { Find = [ Correct "solutions z_i"],
1.156 With = [],
1.157 - Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
1.158 + Given = [Correct "equality (-1 + -2*z + 8*z \<up> 2 = 0)",
1.159 Correct "solveFor z"],
1.160 Where = [...],
1.161 Relate = [] }