1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 07 16:50:20 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 07 17:22:20 2019 +0100
1.3 @@ -150,7 +150,6 @@
1.4 (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \<comment> \<open>---\<close>
1.5 (eq::bool) = Take (eql = eqr); \<comment> \<open>Maybe possible to use HOLogic.mk_eq ??\<close>
1.6 eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \<comment> \<open>---\<close>
1.7 - eq = drop_questionmarks eq;
1.8 (z1::real) = (rhs (NTH 1 L_L)); \<comment> \<open>prepare equation for a - eq_a therefor substitute z with solution 1 - z1\<close>
1.9 (z2::real) = (rhs (NTH 2 L_L)); \<comment> \<open>---\<close>
1.10 (eq_a::bool) = Take eq;
1.11 @@ -169,14 +168,11 @@
1.12 [''univariate'',''equation''],[''no_met''])
1.13 [BOOL eq_b, REAL (B::real)]);
1.14 (b::real) = (rhs(NTH 1 sol_b)); \<comment> \<open>---\<close>
1.15 - eqr = drop_questionmarks eqr;
1.16 (pbz::real) = Take eqr;
1.17 pbz = ((Substitute [A=a, B=b]) pbz); \<comment> \<open>---\<close>
1.18 pbz = Rewrite ''ruleYZ'' False pbz;
1.19 - pbz = drop_questionmarks pbz; \<comment> \<open>---\<close>
1.20 (X_z::bool) = Take (X_z = pbz);
1.21 - (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z;
1.22 - n_eq = drop_questionmarks n_eq
1.23 + (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z
1.24 in n_eq)"
1.25 *)
1.26 setup \<open>KEStore_Elems.add_mets
1.27 @@ -216,7 +212,6 @@
1.28 (*Maybe possible to use HOLogic.mk_eq ??*)
1.29 " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^
1.30
1.31 - " eq = drop_questionmarks eq; "^
1.32 " (z1::real) = (rhs (NTH 1 L_L)); "^
1.33 (*
1.34 * prepare equation for a - eq_a
1.35 @@ -242,16 +237,13 @@
1.36 " [BOOL eq_b, REAL (B::real)]); "^
1.37 " (b::real) = (rhs(NTH 1 sol_b)); "^
1.38
1.39 - " eqr = drop_questionmarks eqr; "^
1.40 " (pbz::real) = Take eqr; "^
1.41 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1.42
1.43 " pbz = Rewrite ''ruleYZ'' False pbz; "^
1.44 - " pbz = drop_questionmarks pbz; "^
1.45
1.46 " (X_z::bool) = Take (X_z = pbz); "^
1.47 - " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z; "^
1.48 - " n_eq = drop_questionmarks n_eq "^
1.49 + " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z "^
1.50 "in n_eq)")]
1.51 \<close>
1.52 (* same error as in inverse_ztransform2
1.53 @@ -280,14 +272,11 @@
1.54 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.55 pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
1.56 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.57 - pbz_eq = drop_questionmarks pbz_eq;
1.58 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.59 (X_zeq::bool) = Take (X_z = rhs pbz_eq);
1.60 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.61 - n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq;
1.62 + n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
1.63 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.64 - n_eq = drop_questionmarks n_eq
1.65 -(*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.66 in n_eq) "
1.67 *)
1.68 setup \<open>KEStore_Elems.add_mets
1.69 @@ -313,9 +302,8 @@
1.70 Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
1.71 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
1.72 Rule.Calc ("Partial_Fractions.factors_from_solution",
1.73 - eval_factors_from_solution "#factors_from_solution"),
1.74 - Rule.Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
1.75 - scr = Rule.EmptyScr},
1.76 + eval_factors_from_solution "#factors_from_solution")
1.77 + ], scr = Rule.EmptyScr},
1.78 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
1.79 (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
1.80 "Script InverseZTransform (X_eq::bool) = "^
1.81 @@ -341,13 +329,11 @@
1.82 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.83 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^
1.84 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.85 - " pbz_eq = drop_questionmarks pbz_eq; "^
1.86 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.87 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
1.88 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.89 - " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq; "^
1.90 + " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^
1.91 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.92 - " n_eq = drop_questionmarks n_eq "^
1.93 (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.94 "in n_eq)")]
1.95 \<close>