1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -28,13 +28,13 @@
1.4
1.5 ML {*
1.6 val inverse_z = prep_rls'(
1.7 - Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.8 - erls = Erls, srls = Erls, calc = [], errpatts = [],
1.9 + Celem.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.10 + erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.11 rules =
1.12 [
1.13 - Thm ("rule4", @{thm rule4})
1.14 + Celem.Thm ("rule4", @{thm rule4})
1.15 ],
1.16 - scr = EmptyScr}:rls);
1.17 + scr = Celem.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" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
1.26 - (Specify.prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
1.27 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),
1.28 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
1.29 + [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Celem.e_rls, NONE, [])),
1.30 + (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
1.31 + (["Z_Transform","SignalProcessing"], [], Celem.e_rls, NONE, [])),
1.32 + (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.33 (["Inverse", "Z_Transform", "SignalProcessing"],
1.34 (*^ capital letter breaks coding standard
1.35 because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
1.36 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.37 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.38 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
1.39 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], NONE,
1.40 [["SignalProcessing","Z_Transform","Inverse"]])),
1.41 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
1.42 + (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.43 (["Inverse", "Z_Transform", "SignalProcessing"],
1.44 [("#Given" ,["filterExpression X_eq"]),
1.45 ("#Find" ,["stepResponse n_eq"])],
1.46 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
1.47 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], NONE,
1.48 [["SignalProcessing","Z_Transform","Inverse"]]))] *}
1.49
1.50 subsection {*Define Name and Signature for the Method*}
1.51 @@ -73,20 +73,20 @@
1.52 subsection {*Setup Parent Nodes in Hierarchy of Method*}
1.53 ML {* val thy = @{theory}; (*latest version of thy required*) *}
1.54 setup {* KEStore_Elems.add_mets
1.55 - [Specify.prep_met thy "met_SP" [] e_metID
1.56 + [Specify.prep_met thy "met_SP" [] Celem.e_metID
1.57 (["SignalProcessing"], [],
1.58 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.59 - errpats = [], nrls = e_rls}, "empty_script"),
1.60 - Specify.prep_met thy "met_SP_Ztrans" [] e_metID
1.61 + {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.62 + errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.63 + Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
1.64 (["SignalProcessing", "Z_Transform"], [],
1.65 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.66 - errpats = [], nrls = e_rls}, "empty_script"),
1.67 - Specify.prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.68 + {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.69 + errpats = [], nrls = Celem.e_rls}, "empty_script"),
1.70 + Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.71 (["SignalProcessing", "Z_Transform", "Inverse"],
1.72 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.73 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.74 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.75 - errpats = [], nrls = e_rls},
1.76 + {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls, crls = Celem.e_rls,
1.77 + errpats = [], nrls = Celem.e_rls},
1.78 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.79 " (let X = Take X_eq;" ^
1.80 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
1.81 @@ -102,12 +102,12 @@
1.82 " [Test,solve_linear]) " ^
1.83 " [BOOL equ, REAL z]) " ^
1.84 " in X)"),
1.85 - Specify.prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.86 + Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.87 (["SignalProcessing", "Z_Transform", "Inverse"],
1.88 [("#Given" ,["filterExpression X_eq"]),
1.89 ("#Find" ,["stepResponse n_eq"])],
1.90 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
1.91 - crls = e_rls, errpats = [], nrls = e_rls},
1.92 + {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = srls_partial_fraction, prls = Celem.e_rls,
1.93 + crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls},
1.94 "Script InverseZTransform (X_eq::bool) = "^
1.95 (*(1/z) instead of z ^^^ -1*)
1.96 "(let X = Take X_eq; "^
1.97 @@ -175,32 +175,32 @@
1.98 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1.99 " n_eq = drop_questionmarks n_eq "^
1.100 "in n_eq)"),
1.101 - Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
1.102 + Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.103 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.104 [("#Given" ,["filterExpression X_eq"]),
1.105 ("#Find" ,["stepResponse n_eq"])],
1.106 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.107 - srls = Rls {id="srls_partial_fraction",
1.108 + {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [],
1.109 + srls = Celem.Rls {id="srls_partial_fraction",
1.110 preconds = [], rew_ord = ("termlessI",termlessI),
1.111 - erls = append_rls "erls_in_srls_partial_fraction" e_rls
1.112 + erls = Celem.append_rls "erls_in_srls_partial_fraction" Celem.e_rls
1.113 [(*for asm in NTH_CONS ...*)
1.114 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.115 + Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.116 (*2nd NTH_CONS pushes n+-1 into asms*)
1.117 - Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.118 - srls = Erls, calc = [], errpatts = [],
1.119 - rules = [Thm ("NTH_CONS", @{thm NTH_CONS}),
1.120 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.121 - Thm ("NTH_NIL", @{thm NTH_NIL}),
1.122 - Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
1.123 - Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
1.124 - Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.125 - Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.126 - Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.127 - Calc ("Partial_Fractions.factors_from_solution",
1.128 + Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")],
1.129 + srls = Celem.Erls, calc = [], errpatts = [],
1.130 + rules = [Celem.Thm ("NTH_CONS", @{thm NTH_CONS}),
1.131 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.132 + Celem.Thm ("NTH_NIL", @{thm NTH_NIL}),
1.133 + Celem.Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
1.134 + Celem.Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
1.135 + Celem.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
1.136 + Celem.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.137 + Celem.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.138 + Celem.Calc ("Partial_Fractions.factors_from_solution",
1.139 eval_factors_from_solution "#factors_from_solution"),
1.140 - Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.141 - scr = EmptyScr},
1.142 - prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
1.143 + Celem.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.144 + scr = Celem.EmptyScr},
1.145 + prls = Celem.e_rls, crls = Celem.e_rls, errpats = [], nrls = norm_Rational},
1.146 (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.147 "Script InverseZTransform (X_eq::bool) = "^
1.148 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)