1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Oct 06 15:01:42 2011 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Oct 06 16:15:29 2011 +0200
     1.3 @@ -149,21 +149,23 @@
     1.4  
     1.5  get_denominator :: "real => real"
     1.6  
     1.7 +text {*Attention Build_Inverse_Z_Transform
     1.8 +       works only because definition was copied into Rationals.thy
     1.9 +     *}
    1.10 +
    1.11  ML {*
    1.12  
    1.13  (*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
    1.14  fun eval_get_denominator (thmid:string) _ 
    1.15 -		      (  t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $
    1.16 +		      (t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $
    1.17                (Const ("Rings.inverse_class.divide", _) $ num $
    1.18                  denom)) thy = 
    1.19 -( writeln "found";
    1.20 +
    1.21      SOME (mk_thmid thmid "" 
    1.22              (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    1.23  	          Trueprop $ (mk_equality (t, denom)))
    1.24 -)
    1.25 -  | eval_get_denominator _ _ _ _ = 
    1.26 -( writeln "NOT found";
    1.27 -NONE); 
    1.28 +
    1.29 +  | eval_get_denominator _ _ _ _ = NONE; 
    1.30  
    1.31  *}
    1.32  
    1.33 @@ -172,7 +174,8 @@
    1.34  
    1.35  ML {*
    1.36  val t = @{term "get_denominator ((a +x)/b)"};
    1.37 -eval_get_denominator "" 0 t @{theory}
    1.38 +val SOME (_, t') = eval_get_denominator "" 0 t @{theory};
    1.39 +term2str t';
    1.40  *}
    1.41  
    1.42  
    1.43 @@ -226,7 +229,7 @@
    1.44    ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*)
    1.45     "solveFor z",                                     (*bound variable*)
    1.46     "solutions L"];                                   (*identifier for solution*)
    1.47 -(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
    1.48 +
    1.49  val (dI',pI',mI') =
    1.50    ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
    1.51  *}
    1.52 @@ -574,6 +577,12 @@
    1.53  atomty sc;
    1.54  
    1.55  *}
    1.56 +
    1.57 +text {*
    1.58 +This ruleset contains all functions that are in the script; 
    1.59 +The evaluation of the functions is done by rewriting using this ruleset.
    1.60 +*}
    1.61 +
    1.62  ML {*
    1.63  val srls = Rls {id="srls_InverseZTransform", 
    1.64  		  preconds = [], rew_ord = ("termlessI",termlessI), 
    1.65 @@ -588,7 +597,8 @@
    1.66  			     Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.67  			     Calc("Tools.lhs", eval_lhs"eval_lhs_"), (*<=== ONLY USED*)
    1.68  			     Calc("Tools.rhs", eval_rhs"eval_rhs_"), (*<=== ONLY USED*)
    1.69 -			     Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
    1.70 +			     Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
    1.71 +     Calc("Rationals.get'_denominator", eval_get_denominator "Rationals.get'_denominator")
    1.72  			    ],
    1.73  		  scr = EmptyScr};
    1.74  *}
    1.75 @@ -623,8 +633,9 @@
    1.76   ));
    1.77  *}
    1.78  ML {*
    1.79 -(*GOON tip for eval_get_argument: compare eval_get_denominator*)
    1.80 -val funId $ arg = @{term "X (z::real)"};
    1.81 +
    1.82 +val Script scr = (#scr o get_met) ["SignalProcessing", "Z_Transform", "inverse"];
    1.83 +atomty scr
    1.84  
    1.85  *}
    1.86  
    1.87 @@ -664,8 +675,12 @@
    1.88  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
    1.89  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; (*TODO naming!*)
    1.90  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
    1.91 +*}
    1.92 +ML {*
    1.93  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Take 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
    1.94 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "   Empty_Tac!   ";
    1.95 +*}
    1.96 +ML {*
    1.97 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.98  *}
    1.99  ML {*
   1.100  show_pt pt;