1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Feb 12 12:17:48 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Feb 12 22:57:17 2012 +0100
     1.3 @@ -16,13 +16,38 @@
     1.4    rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
     1.5  
     1.6  axiomatization where
     1.7 -  ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
     1.8 +  ruleZY: "(X z = a / b) = (X' z = a / (z * b))" 
     1.9  
    1.10  subsection{*Define the Field Descriptions for the specification*}
    1.11  consts
    1.12    filterExpression  :: "bool => una"
    1.13    stepResponse      :: "bool => una"
    1.14  
    1.15 +
    1.16 +ML {*
    1.17 +val inverse_z = prep_rls(
    1.18 +  Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    1.19 +	  erls = Erls, srls = Erls, calc = [],
    1.20 +	  rules = 
    1.21 +	   [Thm ("rule1",num_str @{thm rule1}),
    1.22 +    Thm ("rule2",num_str @{thm rule2}),
    1.23 +    Thm ("rule3",num_str @{thm rule3}),
    1.24 +    Thm ("rule4",num_str @{thm rule4}),
    1.25 +    Thm ("rule5",num_str @{thm rule5}),
    1.26 +    Thm ("rule6",num_str @{thm rule6})
    1.27 +	   ], 
    1.28 +	 scr = EmptyScr}:rls);
    1.29 +*}
    1.30 +
    1.31 +
    1.32 +text {*store the rule set for math engine*}
    1.33 +
    1.34 +ML {*
    1.35 +ruleset' := overwritelthy @{theory} (!ruleset',
    1.36 +  [("inverse_z", inverse_z)
    1.37 +   ]);
    1.38 +*}
    1.39 +
    1.40  subsection{*Define the Specification*}
    1.41  ML {*
    1.42  val thy = @{theory};

     2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Feb 12 12:17:48 2012 +0100
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Feb 12 22:57:17 2012 +0100
     2.3 @@ -840,8 +840,6 @@
     2.4        "          [univariate,equation],[no_met])" ^
     2.5        "        [BOOL eq_a, REAL (A::real)]);"^
     2.6        "      (a::real) = (rhs(NTH 1 sol_a));"^
     2.7 -"(aarg::real) = (lhs(NTH 1 sol_a));"^
     2.8 -
     2.9  
    2.10        "      (eq_b::bool) = Take eq;"^
    2.11        "      eq_b =  (Substitute [zzz=z2]) eq_b;"^
    2.12 @@ -849,15 +847,21 @@
    2.13        "      (sol_b::bool list) = (SubProblem (Isac'," ^
    2.14        "          [univariate,equation],[no_met])" ^
    2.15        "        [BOOL eq_b, REAL (B::real)]);"^
    2.16 +      "      (b::real) = (rhs(NTH 1 sol_b));"^
    2.17  
    2.18 +
    2.19 +      "      eqr = drop_questionmarks eqr;"^
    2.20        "      (pbz::real) = Take eqr;"^
    2.21 -      "      pbz = drop_questionmarks pbz;"^
    2.22 +      "      pbz = ((Substitute [A=a]) pbz);"^
    2.23 +      "      pbz = ((Substitute [B=b]) pbz);"^
    2.24  
    2.25 -      "      (pbz2::real) = (Substitute [A=a]) pbz;"^
    2.26 +(*      "      pbz = Rewrite ruleYZ False pbz;"^*)
    2.27  
    2.28 -      "      (x::real) = Take pbz2"^
    2.29 +      "      (pbz1::real) = Take pbz;"^
    2.30 +"(pbz2::real) = (Rewrite_Set inverse_z False) pbz1;"^
    2.31 +      "      (n_eq::bool) = Take (X_n = pbz2)"^ 
    2.32  
    2.33 -      "  in X)" 
    2.34 +      "  in n_eq)" 
    2.35        ));
    2.36  *}
    2.37