1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Aug 09 14:20:20 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Aug 10 09:43:07 2021 +0200
     1.3 @@ -110,24 +110,23 @@
     1.4  
     1.5  method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
     1.6    \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
     1.7 -    srls = Rule_Def.Repeat {id="srls_partial_fraction", 
     1.8 -        preconds = [], rew_ord = ("termlessI",termlessI),
     1.9 -        erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
    1.10 -            [(*for asm in NTH_CONS ...*)
    1.11 -              \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.12 -              (*2nd NTH_CONS pushes n+-1 into asms*)
    1.13 -              \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
    1.14 -        srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.15 -        rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.16 -            \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.17 -            \<^rule_thm>\<open>NTH_NIL\<close>,
    1.18 -            \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
    1.19 -            \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
    1.20 -            \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
    1.21 -            \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
    1.22 -            \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
    1.23 -            \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
    1.24 -            ], scr = Rule.Empty_Prog},
    1.25 +    srls = Rule_Def.Repeat {
    1.26 +      id = "srls_partial_fraction",  preconds = [], rew_ord = ("termlessI",termlessI),
    1.27 +      erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
    1.28 +        \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
    1.29 +        (*2nd NTH_CONS pushes n+-1 into asms*)
    1.30 +        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
    1.31 +      srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.32 +      rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.33 +        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.34 +        \<^rule_thm>\<open>NTH_NIL\<close>,
    1.35 +        \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
    1.36 +        \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
    1.37 +        \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
    1.38 +        \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
    1.39 +        \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
    1.40 +        \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")],
    1.41 +      scr = Rule.Empty_Prog},
    1.42      prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
    1.43    Program: inverse_ztransform2.simps
    1.44    Given: "filterExpression X_eq" "functionName X_z"