1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Dec 18 15:17:00 2011 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Dec 19 14:41:41 2011 +0100
     1.3 @@ -790,22 +790,25 @@
     1.4      prls = e_rls,
     1.5      crls = e_rls, nrls = e_rls},
     1.6  "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
     1.7 -(*([1], Frm)*)" (let X = Take X_eq;" ^
     1.8 -(*([1], Res)*)"      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
     1.9 -(*([2], Res)*)"      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
    1.10 -              "      (X'_z::real) = lhs X';" ^ (**)
    1.11 -              "      (zzz::real) = argument_in X'_z;" ^ (**)
    1.12 -              "      (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)
    1.13 -              "      (denom::real) = get_denominator funterm;" ^ (*get_denominator*)
    1.14 -              "      (num::real) = get_numerator funterm; " ^ (*get_numerator*)
    1.15 -              "      (equ::bool) = (denom = (0::real));" ^
    1.16 -(*([3], Pbl)*)"      (L_L::bool list) = (SubProblem (PolyEq'," ^
    1.17 -              "          [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
    1.18 -              "        [BOOL equ, REAL zzz]);              " ^
    1.19 -(*([3], Res)*)
    1.20 -              "      (facs::real) = factors_from_solution L_L;" ^
    1.21 -(*([4], Frm)*)"      equ = Take (funterm = num / facs);" ^
    1.22 -(**)"      equ = (Rewrite_Set ansatz_rls False) equ;"^
    1.23 +" (let X = Take X_eq;" ^
    1.24 +"      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
    1.25 +"      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
    1.26 +"      (X'_z::real) = lhs X';" ^ (**)
    1.27 +"      (zzz::real) = argument_in X'_z;" ^ (**)
    1.28 +"      (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)
    1.29 +"      (denom::real) = get_denominator funterm;" ^ (*get_denominator*)
    1.30 +"      (num::real) = get_numerator funterm; " ^ (*get_numerator*)
    1.31 +"      (equ::bool) = (denom = (0::real));" ^
    1.32 +
    1.33 +"      (L_L::bool list) = (SubProblem (PolyEq'," ^
    1.34 +"          [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
    1.35 +"        [BOOL equ, REAL zzz]);              " ^
    1.36 +
    1.37 +
    1.38 +"      (facs::real) = factors_from_solution L_L;" ^
    1.39 +
    1.40 +"      (eql::real) = Take (num / facs);" ^
    1.41 +"      (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;"^
    1.42  
    1.43  "      (eq::bool) = Take (eql = eqr);"^ (*Maybe possible to use HOLogic.mk_eq ??*)
    1.44  "      eq = (Try (Rewrite_Set equival_trans False)) eq;"^
    1.45 @@ -814,7 +817,10 @@
    1.46  "      (eq_a::bool) = (Substitute [zzz=z1]) eq;"^
    1.47  "      eq_a = (Rewrite_Set norm_Rational False) eq_a;"^
    1.48  
    1.49 -"(*      (aaa::real) = Take argument_in eq_a;*)"^
    1.50 +"      (aaa::real) = argument_in (rhs eq_a);"^
    1.51 +
    1.52 +"       x = Take aaa;"^
    1.53 +
    1.54  
    1.55  "(*      (A::bool list) = (SubProblem (PolyEq'," ^
    1.56  "          [univariate,equation],[no_met])" ^
    1.57 @@ -933,22 +939,19 @@
    1.58  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";
    1.59  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";
    1.60  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";
    1.61 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.62 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.63 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.64 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([3,4], Res), [z = 1 / 2, z = -1 / 4])] *)
    1.65 -                                       "nxt = Check_Postcond";
    1.66 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([3], Res), [z = 1 / 2, z = -1 / 4])] *)
    1.67 -                                       "nxt = Take";
    1.68 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*([4], Frm), 24 / (-1 + -2 * z + 8 * z ^^^ 2) = ...*)
    1.69 -                                       "nxt = Specify_Problem";
    1.70  show_pt pt;
    1.71  *}
    1.72  ML {*
    1.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.74  *}
    1.75  ML {*
    1.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.77  *}
    1.78  ML {*
    1.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.80 +*}
    1.81 +ML {*
    1.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.83  *}
    1.84  ML {*
    1.85  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.86 @@ -971,8 +974,31 @@
    1.87  *}
    1.88  
    1.89  ML {*
    1.90 -trace_script := false;
    1.91 -trace_rewrite := false;
    1.92 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.93 +show_pt pt;
    1.94 +*}
    1.95 +
    1.96 +ML {*
    1.97 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.98 +show_pt pt;
    1.99 +*}
   1.100 +
   1.101 +ML {*
   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 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.107 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   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 +*}
   1.113 +
   1.114 +ML {*
   1.115 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.116 +show_pt pt;
   1.117  *}
   1.118  
   1.119  section {*Write Tests for Crucial Details*}