1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Sep 28 10:18:20 2011 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Sep 28 10:42:48 2011 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4  
     1.5  *}
     1.6  subsection {*prepare expression \label{prep-expr}*}
     1.7 +
     1.8  ML {*
     1.9  val ctxt = ProofContext.init_global @{theory Isac};
    1.10  val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
    1.11 @@ -138,9 +139,37 @@
    1.12  (*GOON ===================================================*)
    1.13  
    1.14  *}
    1.15 +
    1.16 +text{*---------------------------begin partial fractions snip--------------------------*}
    1.17 +
    1.18 +subsection {*get the denominator out of a fraction*}
    1.19 +text {*this function can be put into rule sets*}
    1.20  ML {*
    1.21 +(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
    1.22 +fun eval_get_denominator (thmid:string) _ 
    1.23 +		      (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = 
    1.24 +    SOME (mk_thmid thmid "" 
    1.25 +            (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    1.26 +	          Trueprop $ (mk_equality (t, denom)))
    1.27 +  | eval_get_denominator _ _ _ _ = NONE; 
    1.28  *}
    1.29 -ML {**}
    1.30 +text {*rule set for partial fractions*}
    1.31 +ML {*
    1.32 +val partial_fraction = 
    1.33 +  Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.34 +	  erls = Erls, srls = Erls, calc = [],
    1.35 +	  rules = [
    1.36 +				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
    1.37 +		  ],
    1.38 +	 scr = EmptyScr};
    1.39 +*}
    1.40 +text {*store the rule set for math engine*}
    1.41 +ML {*
    1.42 +  overwritelthy @{theory} (!ruleset', 
    1.43 +	    [("partial_fraction", prep_rls partial_fraction)
    1.44 +	     ]);
    1.45 +*}
    1.46 +text{*---------------------------end partial fractions snip--------------------------*}
    1.47  
    1.48  subsection {*solve equation*}
    1.49  text {*this type of equation if too general for the present program*}
    1.50 @@ -596,7 +625,7 @@
    1.51  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.52  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.53  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
    1.54 -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))";
    1.55 +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.56  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.57  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Take 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
    1.58  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "   Empty_Tac!   ";