1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -91,17 +91,17 @@
1.4 errpats = [], nrls = Rule.e_rls},
1.5 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
1.6 " (let X = Take X_eq;" ^
1.7 - " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
1.8 - " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
1.9 + " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
1.10 + " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
1.11 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
1.12 - " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
1.13 + " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*)
1.14 " equ = (denom = (0::real));" ^
1.15 " fun_arg = Take (lhs X');" ^
1.16 - " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
1.17 + " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*)
1.18 " (L_L::bool list) = " ^
1.19 - " (SubProblem (Test', " ^
1.20 - " [LINEAR,univariate,equation,test]," ^
1.21 - " [Test,solve_linear]) " ^
1.22 + " (SubProblem (''Test'', " ^
1.23 + " [''LINEAR'',''univariate'',''equation'',''test'']," ^
1.24 + " [''Test'',''solve_linear'']) " ^
1.25 " [BOOL equ, REAL z]) " ^
1.26 " in X)")]
1.27 \<close>
1.28 @@ -115,10 +115,10 @@
1.29 "Script InverseZTransform (X_eq::bool) = "^
1.30 (*(1/z) instead of z ^^^ -1*)
1.31 "(let X = Take X_eq; "^
1.32 - " X' = Rewrite ruleZY False X; "^
1.33 + " X' = Rewrite ''ruleZY'' False X; "^
1.34 (*z * denominator*)
1.35 " (num_orig::real) = get_numerator (rhs X'); "^
1.36 - " X' = (Rewrite_Set norm_Rational False) X'; "^
1.37 + " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^
1.38 (*simplify*)
1.39 " (X'_z::real) = lhs X'; "^
1.40 " (zzz::real) = argument_in X'_z; "^
1.41 @@ -129,9 +129,9 @@
1.42 " (num::real) = get_numerator funterm; "^
1.43 (*get_numerator*)
1.44 " (equ::bool) = (denom = (0::real)); "^
1.45 - " (L_L::bool list) = (SubProblem (PolyEq', "^
1.46 - " [abcFormula,degree_2,polynomial,univariate,equation], "^
1.47 - " [no_met]) "^
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); "^
1.54 @@ -140,7 +140,7 @@
1.55
1.56 " (eq::bool) = Take (eql = eqr); "^
1.57 (*Maybe possible to use HOLogic.mk_eq ??*)
1.58 - " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
1.59 + " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^
1.60
1.61 " eq = drop_questionmarks eq; "^
1.62 " (z1::real) = (rhs (NTH 1 L_L)); "^
1.63 @@ -154,17 +154,17 @@
1.64 " eq_a = (Substitute [zzz=z1]) eq; "^
1.65 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1.66 " (sol_a::bool list) = "^
1.67 - " (SubProblem (Isac', "^
1.68 - " [univariate,equation],[no_met]) "^
1.69 + " (SubProblem (''Isac'', "^
1.70 + " [''univariate'',''equation''],[''no_met'']) "^
1.71 " [BOOL eq_a, REAL (A::real)]); "^
1.72 " (a::real) = (rhs(NTH 1 sol_a)); "^
1.73
1.74 " (eq_b::bool) = Take eq; "^
1.75 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1.76 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1.77 + " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^
1.78 " (sol_b::bool list) = "^
1.79 - " (SubProblem (Isac', "^
1.80 - " [univariate,equation],[no_met]) "^
1.81 + " (SubProblem (''Isac'', "^
1.82 + " [''univariate'',''equation''],[''no_met'']) "^
1.83 " [BOOL eq_b, REAL (B::real)]); "^
1.84 " (b::real) = (rhs(NTH 1 sol_b)); "^
1.85
1.86 @@ -172,11 +172,11 @@
1.87 " (pbz::real) = Take eqr; "^
1.88 " pbz = ((Substitute [A=a, B=b]) pbz); "^
1.89
1.90 - " pbz = Rewrite ruleYZ False pbz; "^
1.91 + " pbz = Rewrite ''ruleYZ'' False pbz; "^
1.92 " pbz = drop_questionmarks pbz; "^
1.93
1.94 " (X_z::bool) = Take (X_z = pbz); "^
1.95 - " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1.96 + " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z; "^
1.97 " n_eq = drop_questionmarks n_eq "^
1.98 "in n_eq)")]
1.99 \<close>
1.100 @@ -212,7 +212,7 @@
1.101 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
1.102 "(let X = Take X_eq; "^
1.103 (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.104 - " X' = Rewrite ruleZY False X; "^
1.105 + " X' = Rewrite ''ruleZY'' False X; "^
1.106 (* ?X' z*)
1.107 " (X'_z::real) = lhs X'; "^
1.108 (* z *)
1.109 @@ -220,22 +220,22 @@
1.110 (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
1.111 " (funterm::real) = rhs X'; "^
1.112
1.113 - " (pbz::real) = (SubProblem (Isac', "^
1.114 - " [partial_fraction,rational,simplification], "^
1.115 - " [simplification,of_rationals,to_partial_fraction]) "^
1.116 + " (pbz::real) = (SubProblem (''Isac'', "^
1.117 + " [''partial_fraction'',''rational'',''simplification''], "^
1.118 + " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
1.119 (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.120 " [REAL funterm, REAL zzz]); "^
1.121
1.122 (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.123 " (pbz_eq::bool) = Take (X'_z = pbz); "^
1.124 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
1.125 - " pbz_eq = Rewrite ruleYZ False pbz_eq; "^
1.126 + " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^
1.127 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.128 " pbz_eq = drop_questionmarks pbz_eq; "^
1.129 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
1.130 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
1.131 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
1.132 - " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^
1.133 + " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq; "^
1.134 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
1.135 " n_eq = drop_questionmarks n_eq "^
1.136 (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)