1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Jan 08 08:41:35 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jan 14 16:07:07 2012 +0100
1.3 @@ -815,28 +815,34 @@
1.4 " (L_L::bool list) = (SubProblem (PolyEq'," ^
1.5 " [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
1.6 " [BOOL equ, REAL zzz]); " ^
1.7 +
1.8 (*([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
1.9 (*([3], Res), [z = 1 / 2, z = -1 / 4]*)
1.10 +
1.11 " (facs::real) = factors_from_solution L_L;" ^
1.12 - " (eql::real) = Take (num / facs);" ^
1.13 -(*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
1.14 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^
1.15 -(*([4], Res), ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
1.16 - " (eq::bool) = Take (eql = eqr);"^ (*Maybe possible to use HOLogic.mk_eq ??*)
1.17 -(*([5], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))) = ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
1.18 - " eq = (Try (Rewrite_Set equival_trans False)) eq;"^
1.19 -(*([5], Res), 24 = ?A * (z + -1 * (-1 / 4)) + ?B * (z + -1 * (1 / 2))*)
1.20 + " (eql::real) = Take (num / facs);" ^ (*([4], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4)))*)
1.21 +
1.22 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^ (*([4], Res), ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
1.23 +
1.24 + " (eq::bool) = Take (eql = eqr);"^ (*Maybe possible to use HOLogic.mk_eq ??*) (*([5], Frm), 24 / ((z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))) = ?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))*)
1.25 +
1.26 + " eq = (Try (Rewrite_Set equival_trans False)) eq;"^ (*([5], Res), 24 = ?A * (z + -1 * (-1 / 4)) + ?B * (z + -1 * (1 / 2))*)
1.27 +
1.28 " eq = drop_questionmarks eq;"^
1.29 - " (z1::real) = (rhs (NTH 1 L_L));"^ (*prepare equliation for a - eq_a therfor subsitude z with solution 1 - z1*)
1.30 - " (eq_a::bool) = (Substitute [zzz=z1]) eq;"^
1.31 -(*([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;"^
1.33 -(*([7], Res), 24 = ?A * 3 / 4*)
1.34 - (*" (aaa::real) = argument_in (rhs eq_a);"^
1.35 - " x = Take aaa;"^*)
1.36 - " (num1::bool list) = (SubProblem (Isac'," ^
1.37 + " (z1::real) = (rhs (NTH 1 L_L));"^ (*prepare equliation for a - eq_a therfor subsitude z with solution 1 - z1*)
1.38 + " (z2::real) = (rhs (NTH 1 L_L));"^
1.39 +
1.40 +
1.41 + " (eq_a::bool) = (Substitute [zzz=z1]) eq;"^ (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
1.42 + " eq_a = (Rewrite_Set norm_Rational False) eq_a;"^ (*([7], Res), 24 = ?A * 3 / 4*)
1.43 + " (sol_a::bool list) = (SubProblem (Isac'," ^
1.44 " [univariate,equation],[no_met])" ^
1.45 " [BOOL eq_a, REAL (A::real)]);"^
1.46 + " (a::real) = (rhs(NTH 1 sol_a));"^
1.47 +
1.48 + " (eq_b::bool) = eq;"^
1.49 +(*" eq_b = (Substitute [zzz=z1]) eq_b;"^*)
1.50 +
1.51 " (x::real) = 3"^(*only here that the last step of the ptree is visible in tracing output*)
1.52 " in X)"
1.53 ));
1.54 @@ -988,12 +994,44 @@
1.55 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["degree_1", "polynomial",
1.56 "univariate", "equation"])*)
1.57 *}
1.58 +
1.59 +
1.60 ML {*
1.61 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.62 show_pt pt;
1.63 *}
1.64 +
1.65 ML {*
1.66 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.67 +show_pt pt;
1.68 *}
1.69
1.70 +ML {*
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 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 +show_pt pt;
1.88 +*}
1.89 +
1.90 +ML {*
1.91 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.92 +show_pt pt;
1.93 +*}
1.94 +
1.95 +
1.96 section {*Write Tests for Crucial Details*}
1.97 text{*===================================*}
1.98 ML {*