test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 59546 1ada701c4811
parent 59497 8952c43fdce3
child 59550 2e7631381921
equal deleted inserted replaced
59545:4035ec339062 59546:1ada701c4811
  1050 
  1050 
  1051 text\<open>\noindent As mentioned above, we need the denominator of the right hand
  1051 text\<open>\noindent As mentioned above, we need the denominator of the right hand
  1052       side. The equation itself consists of this denominator and tries to find
  1052       side. The equation itself consists of this denominator and tries to find
  1053       a $z$ for this the denominator is equal to zero.\<close>
  1053       a $z$ for this the denominator is equal to zero.\<close>
  1054 
  1054 
  1055 ML \<open>
  1055 text \<open> dropped during switch from Script to partial_function:
  1056   val str = 
  1056   val str = 
  1057     "Script InverseZTransform (X_eq::bool) =                         "^
  1057     "Script InverseZTransform (X_eq::bool) =                         "^
  1058     " (let X = Take X_eq;                                            "^
  1058     " (let X = Take X_eq;                                            "^
  1059     "      X' = Rewrite ruleZY False X;                              "^
  1059     "      X' = Rewrite ruleZY False X;                              "^
  1060     "      X' = (Rewrite_Set norm_Rational False) X';                "^
  1060     "      X' = (Rewrite_Set norm_Rational False) X';                "^
  1065     (*
  1065     (*
  1066      * get_denominator
  1066      * get_denominator
  1067      *)
  1067      *)
  1068     "      (equ::bool) = (denom = (0::real));                        "^
  1068     "      (equ::bool) = (denom = (0::real));                        "^
  1069     "      (L_L::bool list) =                                        "^
  1069     "      (L_L::bool list) =                                        "^
  1070     "            (SubProblem (TestX,                                 "^
  1070     "            (SubProblem (Test,                                 "^
  1071     "                         [LINEAR,univariate,equation,test],     "^
  1071     "                         [LINEAR,univariate,equation,test],     "^
  1072     "                         [Test,solve_linear])                   "^
  1072     "                         [Test,solve_linear])                   "^
  1073     "                         [BOOL equ, REAL z])                    "^
  1073     "                         [BOOL equ, REAL z])                    "^
  1074     "  in X)";
  1074     "  in X)";
  1075 
  1075