1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jan 14 16:07:07 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Jan 22 21:42:56 2012 +0100
1.3 @@ -804,6 +804,7 @@
1.4 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.5 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
1.6 (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.7 + " (num_orig::real) = get_numerator (rhs X');"^
1.8 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
1.9 (*([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
1.10 " (X'_z::real) = lhs X';" ^ (**)
1.11 @@ -820,7 +821,7 @@
1.12 (*([3], Res), [z = 1 / 2, z = -1 / 4]*)
1.13
1.14 " (facs::real) = factors_from_solution L_L;" ^
1.15 - " (eql::real) = Take (num / facs);" ^ (*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
1.16 + " (eql::real) = Take (num_orig / facs);" ^ (*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
1.17
1.18 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^ (*([4], Res), ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
1.19
1.20 @@ -830,20 +831,25 @@
1.21
1.22 " eq = drop_questionmarks eq;"^
1.23 " (z1::real) = (rhs (NTH 1 L_L));"^ (*prepare equliation for a - eq_a therfor subsitude z with solution 1 - z1*)
1.24 - " (z2::real) = (rhs (NTH 1 L_L));"^
1.25 -
1.26 -
1.27 - " (eq_a::bool) = (Substitute [zzz=z1]) eq;"^ (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
1.28 + " (z2::real) = (rhs (NTH 2 L_L));"^
1.29 +
1.30 + " (eq_a::bool) = Take eq;"^
1.31 + " eq_a = (Substitute [zzz=z1]) eq;"^ (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
1.32 " eq_a = (Rewrite_Set norm_Rational False) eq_a;"^ (*([7], Res), 24 = ?A * 3 / 4*)
1.33 " (sol_a::bool list) = (SubProblem (Isac'," ^
1.34 " [univariate,equation],[no_met])" ^
1.35 " [BOOL eq_a, REAL (A::real)]);"^
1.36 " (a::real) = (rhs(NTH 1 sol_a));"^
1.37
1.38 - " (eq_b::bool) = eq;"^
1.39 -(*" eq_b = (Substitute [zzz=z1]) eq_b;"^*)
1.40
1.41 - " (x::real) = 3"^(*only here that the last step of the ptree is visible in tracing output*)
1.42 + " (eq_b::bool) = Take eq;"^
1.43 + " eq_b = (Substitute [zzz=z2]) eq_b;"^
1.44 + " eq_b = (Rewrite_Set norm_Rational False) eq_b;"^
1.45 + " (sol_b::bool list) = (SubProblem (Isac'," ^
1.46 + " [univariate,equation],[no_met])" ^
1.47 + " [BOOL eq_b, REAL (B::real)]);"^
1.48 +
1.49 + " (x::real) = Take num_orig"^(*only here that the last step of the ptree is visible in tracing output*)
1.50 " in X)"
1.51 ));
1.52 *}
1.53 @@ -1017,17 +1023,68 @@
1.54 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.55 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.56 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.57 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.58 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.59 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.60 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.61 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.62 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.63 -show_pt pt;
1.64 *}
1.65
1.66 ML {*
1.67 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.68 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.69 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.70 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.71 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.72 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.77 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.78 +*}
1.79 +
1.80 +ML {*
1.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.87 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.88 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.89 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.90 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.91 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.92 +*}
1.93 +
1.94 +ML {*
1.95 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.96 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.97 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.98 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.99 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.100 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.101 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.102 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.103 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.104 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.106 +*}
1.107 +
1.108 +ML {*
1.109 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.110 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.111 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.112 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.113 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.114 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.115 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.117 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.118 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.120 +*}
1.121 +
1.122 +
1.123 +ML {*
1.124 +(*trace_script := true;*)
1.125 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.126 show_pt pt;
1.127 *}
1.128