1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Feb 15 16:52:05 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Feb 19 19:35:12 2019 +0100
1.3 @@ -82,6 +82,20 @@
1.4 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.5 errpats = [], nrls = Rule.e_rls}, "empty_script")]
1.6 \<close>
1.7 +partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool"
1.8 + where
1.9 +"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
1.10 + (let X = Take X_eq;
1.11 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
1.12 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
1.13 + funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
1.14 + denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
1.15 + equ = (denom = (0::real));
1.16 + fun_arg = Take (lhs X');
1.17 + arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
1.18 + L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
1.19 + [''Test'',''solve_linear'']) [BOOL equ, STRING ''z''] \<comment> \<open>PROG string\<close>
1.20 + in X) "
1.21 setup \<open>KEStore_Elems.add_mets
1.22 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.23 (["SignalProcessing", "Z_Transform", "Inverse"],
1.24 @@ -105,6 +119,64 @@
1.25 " [BOOL equ, REAL z]) " ^
1.26 " in X)")]
1.27 \<close>
1.28 +(*
1.29 +Type unification failed: Clash of types "bool" and "_ itself"
1.30 +Type error in application: incompatible operand type
1.31 +Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b
1.32 +Operand:
1.33 + \<lambda>X. let X' = Rewrite ''ruleZY'' ...
1.34 +:
1.35 +:partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> bool"
1.36 + where
1.37 +"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
1.38 + (let X = Take X_eq;
1.39 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
1.40 + (num_orig::real) = get_numerator (rhs X');
1.41 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
1.42 + (X'_z::real) = lhs X';
1.43 + (zzz::real) = argument_in X'_z;
1.44 + (funterm::real) = rhs X'; \<comment> \<open>drop X' z = for equation solving\<close>
1.45 + (denom::real) = get_denominator funterm; \<comment> \<open>get_denominator\<close>
1.46 + (num::real) = get_numerator funterm; \<comment> \<open>get_numerator\<close>
1.47 + (equ::bool) = (denom = (0::real));
1.48 + (L_L::bool list) = (SubProblem (''PolyEq'',
1.49 + [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''],
1.50 + [''no_met''])
1.51 + [BOOL equ, REAL zzz]);
1.52 + (facs::real) = factors_from_solution L_L;
1.53 + (eql::real) = Take (num_orig / facs); \<comment> \<open>---\<close>
1.54 + (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \<comment> \<open>---\<close>
1.55 + (eq::bool) = Take (eql = eqr); \<comment> \<open>Maybe possible to use HOLogic.mk_eq ??\<close>
1.56 + eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \<comment> \<open>---\<close>
1.57 + eq = drop_questionmarks eq;
1.58 + (z1::real) = (rhs (NTH 1 L_L)); \<comment> \<open>prepare equation for a - eq_a therefor substitute z with solution 1 - z1\<close>
1.59 + (z2::real) = (rhs (NTH 2 L_L)); \<comment> \<open>---\<close>
1.60 + (eq_a::bool) = Take eq;
1.61 + eq_a = (Substitute [zzz=z1]) eq;
1.62 + eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
1.63 + (sol_a::bool list) =
1.64 + (SubProblem (''Isac'',
1.65 + [''univariate'',''equation''],[''no_met''])
1.66 + [BOOL eq_a, REAL (A::real)]);
1.67 + (a::real) = (rhs(NTH 1 sol_a)); \<comment> \<open>---\<close>
1.68 + (eq_b::bool) = Take eq;
1.69 + eq_b = (Substitute [zzz=z2]) eq_b;
1.70 + eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b;
1.71 + (sol_b::bool list) =
1.72 + (SubProblem (''Isac'',
1.73 + [''univariate'',''equation''],[''no_met''])
1.74 + [BOOL eq_b, REAL (B::real)]);
1.75 + (b::real) = (rhs(NTH 1 sol_b)); \<comment> \<open>---\<close>
1.76 + eqr = drop_questionmarks eqr;
1.77 + (pbz::real) = Take eqr;
1.78 + pbz = ((Substitute [A=a, B=b]) pbz); \<comment> \<open>---\<close>
1.79 + pbz = Rewrite ''ruleYZ'' False pbz;
1.80 + pbz = drop_questionmarks pbz; \<comment> \<open>---\<close>
1.81 + (X_z::bool) = Take (X_z = pbz);
1.82 + (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z;
1.83 + n_eq = drop_questionmarks n_eq
1.84 +in n_eq)"
1.85 +*)
1.86 setup \<open>KEStore_Elems.add_mets
1.87 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.88 (["SignalProcessing", "Z_Transform", "Inverse"],
1.89 @@ -180,6 +252,42 @@
1.90 " n_eq = drop_questionmarks n_eq "^
1.91 "in n_eq)")]
1.92 \<close>
1.93 +(* same error as in inverse_ztransform2
1.94 +:partial_function (tailrec) inverse_ztransform3 :: "bool \<Rightarrow> bool"
1.95 + where
1.96 +"inverse_ztransform X_eq =
1.97 +(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.98 +(let X = Take X_eq;
1.99 +(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.100 + X' = Rewrite ''ruleZY'' False X;
1.101 +(* ?X' z*)
1.102 + (X'_z::real) = lhs X';
1.103 +(* z *)
1.104 + (zzz::real) = argument_in X'_z;
1.105 +(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.106 + (funterm::real) = rhs X';
1.107 +(*-----*)
1.108 + (pbz::real) = (SubProblem (''Isac'',
1.109 + [''partial_fraction'',''rational'',''simplification''],
1.110 + [''simplification'',''of_rationals'',''to_partial_fraction''])
1.111 +(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.112 + [REAL funterm, REAL zzz]);
1.113 +(*-----*)
1.114 +(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.115 + (pbz_eq::bool) = Take (X'_z = pbz);
1.116 +(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.117 + pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
1.118 +(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.119 + pbz_eq = drop_questionmarks pbz_eq;
1.120 +(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.121 + (X_zeq::bool) = Take (X_z = rhs pbz_eq);
1.122 +(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.123 + n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq;
1.124 +(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.125 + n_eq = drop_questionmarks n_eq
1.126 +(*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.127 +in n_eq) "
1.128 +*)
1.129 setup \<open>KEStore_Elems.add_mets
1.130 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.131 (["SignalProcessing", "Z_Transform", "Inverse_sub"],