1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -46,14 +46,14 @@
     1.4  val thy = @{theory};
     1.5  \<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule_Set.e_rls, NONE, [])),
     1.8 +  [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.9      (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
    1.10 -      (["Z_Transform","SignalProcessing"], [], Rule_Set.e_rls, NONE, [])),
    1.11 +      (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.12      (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
    1.13        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.14          [("#Given" , ["filterExpression X_eq"]),
    1.15            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.16 -        Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], NONE, 
    1.17 +        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE, 
    1.18          [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
    1.19  
    1.20  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    1.21 @@ -61,12 +61,12 @@
    1.22  setup \<open>KEStore_Elems.add_mets
    1.23      [Specify.prep_met thy "met_SP" [] Celem.e_metID
    1.24        (["SignalProcessing"], [],
    1.25 -        {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, crls = Rule_Set.e_rls,
    1.26 -          errpats = [], nrls = Rule_Set.e_rls}, @{thm refl}),
    1.27 +        {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.28 +          errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
    1.29      Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
    1.30        (["SignalProcessing", "Z_Transform"], [],
    1.31 -        {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, crls = Rule_Set.e_rls,
    1.32 -          errpats = [], nrls = Rule_Set.e_rls}, @{thm refl})]
    1.33 +        {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.34 +          errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
    1.35  \<close>
    1.36  
    1.37  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
    1.38 @@ -91,8 +91,8 @@
    1.39        (["SignalProcessing", "Z_Transform", "Inverse"],
    1.40          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.41            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.42 -        {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, crls = Rule_Set.e_rls,
    1.43 -          errpats = [], nrls = Rule_Set.e_rls},
    1.44 +        {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.45 +          errpats = [], nrls = Rule_Set.empty},
    1.46          @{thm inverse_ztransform.simps})]
    1.47  \<close>
    1.48  
    1.49 @@ -119,10 +119,10 @@
    1.50        (["SignalProcessing", "Z_Transform", "Inverse_sub"],
    1.51          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.52            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.53 -        {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [],
    1.54 +        {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
    1.55            srls = Rule_Def.Repeat {id="srls_partial_fraction", 
    1.56                preconds = [], rew_ord = ("termlessI",termlessI),
    1.57 -              erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
    1.58 +              erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
    1.59                    [(*for asm in NTH_CONS ...*)
    1.60                      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.61                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.62 @@ -139,7 +139,7 @@
    1.63                    Rule.Num_Calc ("Partial_Fractions.factors_from_solution",
    1.64                      eval_factors_from_solution "#factors_from_solution")
    1.65                    ], scr = Rule.EmptyScr},
    1.66 -          prls = Rule_Set.e_rls, crls = Rule_Set.e_rls, errpats = [], nrls = norm_Rational},
    1.67 +          prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
    1.68          @{thm inverse_ztransform2.simps})]
    1.69  \<close>
    1.70  ML \<open>