1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 01 19:20:05 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Apr 04 12:11:32 2020 +0200
     1.3 @@ -27,8 +27,8 @@
     1.4  
     1.5  ML \<open>
     1.6  val inverse_z = prep_rls'(
     1.7 -  Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
     1.8 -	  erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
     1.9 +  Rule_Set.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.10 +	  erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.11  	  rules = 
    1.12  	   [
    1.13      Rule.Thm ("rule4", @{thm rule4})
    1.14 @@ -46,14 +46,14 @@
    1.15  val thy = @{theory};
    1.16  \<close>
    1.17  setup \<open>KEStore_Elems.add_pbts
    1.18 -  [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])),
    1.19 +  [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule_Set.e_rls, NONE, [])),
    1.20      (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
    1.21 -      (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
    1.22 +      (["Z_Transform","SignalProcessing"], [], Rule_Set.e_rls, NONE, [])),
    1.23      (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
    1.24        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.25          [("#Given" , ["filterExpression X_eq"]),
    1.26            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.27 -        Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, 
    1.28 +        Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], NONE, 
    1.29          [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
    1.30  
    1.31  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    1.32 @@ -61,12 +61,12 @@
    1.33  setup \<open>KEStore_Elems.add_mets
    1.34      [Specify.prep_met thy "met_SP" [] Celem.e_metID
    1.35        (["SignalProcessing"], [],
    1.36 -        {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.37 -          errpats = [], nrls = Rule.e_rls}, @{thm refl}),
    1.38 +        {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.39 +          errpats = [], nrls = Rule_Set.e_rls}, @{thm refl}),
    1.40      Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
    1.41        (["SignalProcessing", "Z_Transform"], [],
    1.42 -        {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.43 -          errpats = [], nrls = Rule.e_rls}, @{thm refl})]
    1.44 +        {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.45 +          errpats = [], nrls = Rule_Set.e_rls}, @{thm refl})]
    1.46  \<close>
    1.47  
    1.48  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
    1.49 @@ -91,8 +91,8 @@
    1.50        (["SignalProcessing", "Z_Transform", "Inverse"],
    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.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.54 -          errpats = [], nrls = Rule.e_rls},
    1.55 +        {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.56 +          errpats = [], nrls = Rule_Set.e_rls},
    1.57          @{thm inverse_ztransform.simps})]
    1.58  \<close>
    1.59  
    1.60 @@ -119,15 +119,15 @@
    1.61        (["SignalProcessing", "Z_Transform", "Inverse_sub"],
    1.62          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.63            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.64 -        {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
    1.65 -          srls = Rule.Rls {id="srls_partial_fraction", 
    1.66 +        {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [],
    1.67 +          srls = Rule_Set.Rls {id="srls_partial_fraction", 
    1.68                preconds = [], rew_ord = ("termlessI",termlessI),
    1.69 -              erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls
    1.70 +              erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
    1.71                    [(*for asm in NTH_CONS ...*)
    1.72                      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.73                      (*2nd NTH_CONS pushes n+-1 into asms*)
    1.74                      Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.75 -              srls = Rule.Erls, calc = [], errpatts = [],
    1.76 +              srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.77                rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
    1.78                    Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.79                    Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
    1.80 @@ -139,7 +139,7 @@
    1.81                    Rule.Num_Calc ("Partial_Fractions.factors_from_solution",
    1.82                      eval_factors_from_solution "#factors_from_solution")
    1.83                    ], scr = Rule.EmptyScr},
    1.84 -          prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
    1.85 +          prls = Rule_Set.e_rls, crls = Rule_Set.e_rls, errpats = [], nrls = norm_Rational},
    1.86          @{thm inverse_ztransform2.simps})]
    1.87  \<close>
    1.88  ML \<open>