1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 01 11:09:19 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 13:15:52 2019 +0200
1.3 @@ -1,11 +1,11 @@
1.4 -(* Title: Test_Z_Transform
1.5 +(* Title: Inverse_Z_Transform
1.6 Author: Jan Rocnik
1.7 (c) copyright due to lincense terms.
1.8 *)
1.9
1.10 theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
1.11
1.12 -axiomatization where
1.13 +axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close>
1.14 rule1: "1 = \<delta>[n]" and
1.15 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
1.16 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
1.17 @@ -23,7 +23,7 @@
1.18 subsection\<open>Define the Field Descriptions for the specification\<close>
1.19 consts
1.20 filterExpression :: "bool => una"
1.21 - stepResponse :: "bool => una"
1.22 + stepResponse :: "bool => una" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close>
1.23
1.24 ML \<open>
1.25 val inverse_z = prep_rls'(
1.26 @@ -51,16 +51,10 @@
1.27 (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
1.28 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
1.29 (["Inverse", "Z_Transform", "SignalProcessing"],
1.30 - [("#Given" ,["filterExpression X_eq"]),
1.31 - ("#Find" ,["stepResponse n_eq"])],
1.32 + [("#Given" , ["filterExpression X_eq"]),
1.33 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.34 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.35 - [["SignalProcessing","Z_Transform","Inverse"]])),
1.36 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID
1.37 - (["Inverse_sub", "Z_Transform", "SignalProcessing"],
1.38 - [("#Given" ,["filterExpression X_eq"]),
1.39 - ("#Find" ,["stepResponse n_eq"])],
1.40 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.41 - [["SignalProcessing","Z_Transform","Inverse_sub"]]))]\<close>
1.42 + [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
1.43
1.44 subsection \<open>Define Name and Signature for the Method\<close>
1.45 consts
1.46 @@ -82,26 +76,27 @@
1.47 errpats = [], nrls = Rule.e_rls}, @{thm refl})]
1.48 \<close>
1.49
1.50 -(*WARNING: Additional type variable(s) in specification of "inverse_ztransform": 'a *)
1.51 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.52 where
1.53 -"inverse_ztransform X_eq z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
1.54 - (let X = Take X_eq;
1.55 - X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
1.56 - X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
1.57 - funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
1.58 - denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
1.59 - equ = (denom = (0::real));
1.60 - fun_arg = Take (lhs X');
1.61 - arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
1.62 - L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
1.63 - [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG string\<close>
1.64 +"inverse_ztransform X_eq X_z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
1.65 + (let X = Take X_eq;
1.66 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
1.67 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
1.68 + funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
1.69 + denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
1.70 + equ = (denom = (0::real));
1.71 + fun_arg = Take (lhs X');
1.72 + arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
1.73 + (L_L::bool list) = \<comment> \<open>'bool list' inhibits (?!?):
1.74 + WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
1.75 + SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
1.76 + [''Test'',''solve_linear'']) [BOOL equ, REAL X_z]
1.77 in X) "
1.78 setup \<open>KEStore_Elems.add_mets
1.79 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.80 (["SignalProcessing", "Z_Transform", "Inverse"],
1.81 - [("#Given" ,["filterExpression (X_eq::bool)"]),
1.82 - ("#Find" ,["stepResponse (n_eq::bool)"])],
1.83 + [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.84 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.85 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.86 errpats = [], nrls = Rule.e_rls},
1.87 @{thm inverse_ztransform.simps}
1.88 @@ -142,8 +137,8 @@
1.89 setup \<open>KEStore_Elems.add_mets
1.90 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.91 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.92 - [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
1.93 - ("#Find" ,["stepResponse n_eq"])],
1.94 + [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.95 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.96 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
1.97 srls = Rule.Rls {id="srls_partial_fraction",
1.98 preconds = [], rew_ord = ("termlessI",termlessI),
1.99 @@ -165,7 +160,7 @@
1.100 eval_factors_from_solution "#factors_from_solution")
1.101 ], scr = Rule.EmptyScr},
1.102 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
1.103 - @{thm simplify.simps}
1.104 + @{thm inverse_ztransform2.simps}
1.105 (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.106 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.107 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.108 @@ -182,6 +177,9 @@
1.109 " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.110 " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.111 \<close>
1.112 +ML \<open>
1.113 +\<close> ML \<open>
1.114 +\<close>
1.115
1.116 end
1.117