1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -56,13 +56,6 @@
1.4 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
1.5 [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
1.6
1.7 -subsection \<open>Define Name and Signature for the Method\<close>
1.8 -consts
1.9 - InverseZTransform1 :: "[bool, bool] => bool"
1.10 - ("((Script InverseZTransform1 (_ =))// (_))" 9)
1.11 - InverseZTransform2 :: "[bool, real, bool] => bool"
1.12 - ("((Script InverseZTransform2 (_ _ =))// (_))" 9)
1.13 -
1.14 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
1.15 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
1.16 setup \<open>KEStore_Elems.add_mets
1.17 @@ -99,22 +92,7 @@
1.18 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.19 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.20 errpats = [], nrls = Rule.e_rls},
1.21 - @{thm inverse_ztransform.simps}
1.22 - (*"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.23 - " (let X = Take X_eq;" ^
1.24 - " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
1.25 - " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
1.26 - " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
1.27 - " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*)
1.28 - " equ = (denom = (0::real));" ^
1.29 - " fun_arg = Take (lhs X');" ^
1.30 - " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*)
1.31 - " (L_L::bool list) = " ^
1.32 - " (SubProblem (''Test'', " ^
1.33 - " [''LINEAR'',''univariate'',''equation'',''test'']," ^
1.34 - " [''Test'',''solve_linear'']) " ^
1.35 - " [BOOL equ, REAL z]) " ^
1.36 - " in X)"*))]
1.37 + @{thm inverse_ztransform.simps})]
1.38 \<close>
1.39
1.40 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.41 @@ -160,22 +138,7 @@
1.42 eval_factors_from_solution "#factors_from_solution")
1.43 ], scr = Rule.EmptyScr},
1.44 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
1.45 - @{thm inverse_ztransform2.simps}
1.46 - (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.47 - " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.48 - " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.49 - " (X'_z::real) = lhs X'; "^ (* ?X' z*)
1.50 - " (zzz::real) = argument_in X'_z; "^ (* z *)
1.51 - " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.52 - " (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.53 - " [''partial_fraction'',''rational'',''simplification''], "^
1.54 - " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
1.55 - " [REAL funterm, REAL zzz]); "^
1.56 - " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.57 - " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.58 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.59 - " 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.60 - " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.61 + @{thm inverse_ztransform2.simps})]
1.62 \<close>
1.63 ML \<open>
1.64 \<close> ML \<open>