1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -28,13 +28,13 @@
1.4
1.5 ML {*
1.6 val inverse_z = prep_rls'(
1.7 - Celem.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.8 - erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.9 + Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
1.10 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.11 rules =
1.12 [
1.13 - Celem.Thm ("rule4", @{thm rule4})
1.14 + Rule.Thm ("rule4", @{thm rule4})
1.15 ],
1.16 - scr = Celem.EmptyScr});
1.17 + scr = Rule.EmptyScr});
1.18 *}
1.19
1.20
1.21 @@ -47,22 +47,22 @@
1.22 val thy = @{theory};
1.23 *}
1.24 setup {* KEStore_Elems.add_pbts
1.25 - [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Celem.e_rls, NONE, [])),
1.26 + [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])),
1.27 (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
1.28 - (["Z_Transform","SignalProcessing"], [], Celem.e_rls, NONE, [])),
1.29 + (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
1.30 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.31 (["Inverse", "Z_Transform", "SignalProcessing"],
1.32 (*^ capital letter breaks coding standard
1.33 because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
1.34 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.35 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.36 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], NONE,
1.37 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.38 [["SignalProcessing","Z_Transform","Inverse"]])),
1.39 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.40 (["Inverse", "Z_Transform", "SignalProcessing"],
1.41 [("#Given" ,["filterExpression X_eq"]),
1.42 ("#Find" ,["stepResponse n_eq"])],
1.43 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], NONE,
1.44 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.45 [["SignalProcessing","Z_Transform","Inverse"]]))] *}
1.46
1.47 subsection {*Define Name and Signature for the Method*}
1.48 @@ -75,18 +75,18 @@
1.49 setup {* KEStore_Elems.add_mets
1.50 [Specify.prep_met thy "met_SP" [] Celem.e_metID
1.51 (["SignalProcessing"], [],
1.52 - {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.53 - errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.54 + {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.55 + errpats = [], nrls = Rule.e_rls}, "empty_script"),
1.56 Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
1.57 (["SignalProcessing", "Z_Transform"], [],
1.58 - {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.59 - errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.60 + {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.61 + errpats = [], nrls = Rule.e_rls}, "empty_script"),
1.62 Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.63 (["SignalProcessing", "Z_Transform", "Inverse"],
1.64 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.65 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.66 - {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.67 - errpats = [], nrls = Celem.e_rls},
1.68 + {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.69 + errpats = [], nrls = Rule.e_rls},
1.70 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.71 " (let X = Take X_eq;" ^
1.72 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
1.73 @@ -106,8 +106,8 @@
1.74 (["SignalProcessing", "Z_Transform", "Inverse"],
1.75 [("#Given" ,["filterExpression X_eq"]),
1.76 ("#Find" ,["stepResponse n_eq"])],
1.77 - {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = srls_partial_fraction, prls = Celem.e_rls,
1.78 - crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls},
1.79 + {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls,
1.80 + crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
1.81 "Script InverseZTransform (X_eq::bool) = "^
1.82 (*(1/z) instead of z ^^^ -1*)
1.83 "(let X = Take X_eq; "^
1.84 @@ -179,28 +179,28 @@
1.85 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.86 [("#Given" ,["filterExpression X_eq"]),
1.87 ("#Find" ,["stepResponse n_eq"])],
1.88 - {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [],
1.89 - srls = Celem.Rls {id="srls_partial_fraction",
1.90 + {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
1.91 + srls = Rule.Rls {id="srls_partial_fraction",
1.92 preconds = [], rew_ord = ("termlessI",termlessI),
1.93 - erls = Celem.append_rls "erls_in_srls_partial_fraction" Celem.e_rls
1.94 + erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls
1.95 [(*for asm in NTH_CONS ...*)
1.96 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.97 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.98 (*2nd NTH_CONS pushes n+-1 into asms*)
1.99 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.100 - srls = Celem.Erls, calc = [], errpatts = [],
1.101 - rules = [Celem.Thm ("NTH_CONS", @{thm NTH_CONS}),
1.102 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.103 - Celem.Thm ("NTH_NIL", @{thm NTH_NIL}),
1.104 - Celem.Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
1.105 - Celem.Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
1.106 - Celem.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.107 - Celem.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.108 - Celem.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.109 - Celem.Calc ("Partial_Fractions.factors_from_solution",
1.110 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.111 + srls = Rule.Erls, calc = [], errpatts = [],
1.112 + rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
1.113 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.114 + Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
1.115 + Rule.Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
1.116 + Rule.Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
1.117 + Rule.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.118 + Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.119 + Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.120 + Rule.Calc ("Partial_Fractions.factors_from_solution",
1.121 eval_factors_from_solution "#factors_from_solution"),
1.122 - Celem.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.123 - scr = Celem.EmptyScr},
1.124 - prls = Celem.e_rls, crls = Celem.e_rls, errpats = [], nrls = norm_Rational},
1.125 + Rule.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.126 + scr = Rule.EmptyScr},
1.127 + prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
1.128 (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.129 "Script InverseZTransform (X_eq::bool) = "^
1.130 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)