1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -28,12 +28,12 @@
     1.4  ML \<open>
     1.5  val inverse_z = prep_rls'(
     1.6    Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     1.7 -	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.8 +	  asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
     1.9  	  rules = 
    1.10  	   [
    1.11      \<^rule_thm>\<open>rule4\<close>
    1.12  	   ], 
    1.13 -	 scr = Rule.Empty_Prog});
    1.14 +	 program = Rule.Empty_Prog});
    1.15  \<close>
    1.16  
    1.17  
    1.18 @@ -57,12 +57,12 @@
    1.19  subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
    1.20  
    1.21  method met_SP : "SignalProcessing" =
    1.22 -  \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.23 -    errpats = [], nrls = Rule_Set.empty}\<close>
    1.24 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.25 +    errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.26  
    1.27  method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
    1.28 -  \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.29 -    errpats = [], nrls = Rule_Set.empty}\<close>
    1.30 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.31 +    errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.32  
    1.33  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
    1.34    where
    1.35 @@ -83,8 +83,8 @@
    1.36    in X) "
    1.37  
    1.38  method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
    1.39 -  \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.40 -    errpats = [], nrls = Rule_Set.empty}\<close>
    1.41 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.42 +    errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.43    Program: inverse_ztransform.simps
    1.44    Given: "filterExpression X_eq" "functionName X_z"
    1.45    Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.46 @@ -109,14 +109,14 @@
    1.47    in n_eq)"
    1.48  
    1.49  method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
    1.50 -  \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
    1.51 -    srls = Rule_Def.Repeat {
    1.52 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [],
    1.53 +    prog_rls = Rule_Def.Repeat {
    1.54        id = "srls_partial_fraction",  preconds = [], rew_ord = ("termlessI",termlessI),
    1.55 -      erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
    1.56 +      asm_rls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
    1.57          \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
    1.58          (*2nd NTH_CONS pushes n+-1 into asms*)
    1.59          \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], 
    1.60 -      srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.61 +      prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
    1.62        rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
    1.63          \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
    1.64          \<^rule_thm>\<open>NTH_NIL\<close>,
    1.65 @@ -126,8 +126,8 @@
    1.66          \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
    1.67          \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
    1.68          \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")],
    1.69 -      scr = Rule.Empty_Prog},
    1.70 -    prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
    1.71 +      program = Rule.Empty_Prog},
    1.72 +    where_rls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], rew_rls = norm_Rational}\<close>
    1.73    Program: inverse_ztransform2.simps
    1.74    Given: "filterExpression X_eq" "functionName X_z"
    1.75    Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>