1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 12 18:33:15 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Jun 15 22:24:20 2021 +0200
1.3 @@ -56,16 +56,13 @@
1.4
1.5 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
1.6
1.7 -setup \<open>KEStore_Elems.add_mets
1.8 - [MethodC.prep_input @{theory} "met_SP" [] MethodC.id_empty
1.9 - (["SignalProcessing"], [],
1.10 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.11 - errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
1.12 - MethodC.prep_input @{theory} "met_SP_Ztrans" [] MethodC.id_empty
1.13 - (["SignalProcessing", "Z_Transform"], [],
1.14 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.15 - errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
1.16 -\<close>
1.17 +method met_SP : "SignalProcessing" =
1.18 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.19 + errpats = [], nrls = Rule_Set.empty}\<close>
1.20 +
1.21 +method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
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
1.25 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.26 where
1.27 @@ -84,15 +81,13 @@
1.28 SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
1.29 [BOOL equ, REAL X_z]
1.30 in X) "
1.31 -setup \<open>KEStore_Elems.add_mets
1.32 - [MethodC.prep_input @{theory} "met_SP_Ztrans_inv" [] MethodC.id_empty
1.33 - (["SignalProcessing", "Z_Transform", "Inverse"],
1.34 - [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.35 - ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.36 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.37 - errpats = [], nrls = Rule_Set.empty},
1.38 - @{thm inverse_ztransform.simps})]
1.39 -\<close>
1.40 +
1.41 +method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
1.42 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.43 + errpats = [], nrls = Rule_Set.empty}\<close>
1.44 + Program: inverse_ztransform.simps
1.45 + Given: "filterExpression X_eq" "functionName X_z"
1.46 + Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.47
1.48 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.49 where
1.50 @@ -112,33 +107,32 @@
1.51 X_zeq = Take (X_z = rhs pbz_eq);
1.52 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
1.53 in n_eq)"
1.54 -setup \<open>KEStore_Elems.add_mets
1.55 - [MethodC.prep_input @{theory} "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
1.56 - (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.57 - [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.58 - ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.59 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
1.60 - srls = Rule_Def.Repeat {id="srls_partial_fraction",
1.61 - preconds = [], rew_ord = ("termlessI",termlessI),
1.62 - erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
1.63 - [(*for asm in NTH_CONS ...*)
1.64 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.65 - (*2nd NTH_CONS pushes n+-1 into asms*)
1.66 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.67 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.68 - rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.69 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.70 - \<^rule_thm>\<open>NTH_NIL\<close>,
1.71 - \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
1.72 - \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
1.73 - \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
1.74 - \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
1.75 - \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
1.76 - \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
1.77 - ], scr = Rule.Empty_Prog},
1.78 - prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
1.79 - @{thm inverse_ztransform2.simps})]
1.80 -\<close>
1.81 +
1.82 +method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
1.83 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
1.84 + srls = Rule_Def.Repeat {id="srls_partial_fraction",
1.85 + preconds = [], rew_ord = ("termlessI",termlessI),
1.86 + erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
1.87 + [(*for asm in NTH_CONS ...*)
1.88 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.89 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.90 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.91 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.92 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.93 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.94 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.95 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
1.96 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
1.97 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
1.98 + \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
1.99 + \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
1.100 + \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
1.101 + ], scr = Rule.Empty_Prog},
1.102 + prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
1.103 + Program: inverse_ztransform2.simps
1.104 + Given: "filterExpression X_eq" "functionName X_z"
1.105 + Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.106 +
1.107 ML \<open>
1.108 \<close> ML \<open>
1.109 \<close> ML \<open>