1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Fri May 04 08:51:42 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri May 04 17:33:31 2012 +0200
1.3 @@ -297,9 +297,9 @@
1.4 mathauthors: string list,(*copyright *)
1.5 init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
1.6 rew_ord' : rew_ord', (*for rules in Detail
1.7 - TODO.WN0509 store fun itself, see 'type pbt'*)
1.8 + TODO.WN0509 store fun itself, see 'type pbt'*)
1.9 erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
1.10 - instead erls in "fun prep_met" *)
1.11 + instead erls in "fun prep_met" *)
1.12 srls : rls, (*for evaluating list expressions in scr *)
1.13 prls : rls, (*for evaluating predicates in modelpattern *)
1.14 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
2.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri May 04 08:51:42 2012 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri May 04 17:33:31 2012 +0200
2.3 @@ -134,7 +134,7 @@
2.4 {
2.5 rew_ord'="tless_true",
2.6 rls'= e_rls, calc = [],
2.7 - srls = srls,
2.8 + srls = srls_partial_fraction,
2.9 prls = e_rls,
2.10 crls = e_rls, nrls = e_rls
2.11 },
3.1 --- a/src/Tools/isac/Knowledge/Isac.thy Fri May 04 08:51:42 2012 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Fri May 04 17:33:31 2012 +0200
3.3 @@ -21,6 +21,6 @@
3.4 RatPolyEq RatRootEq etc.
3.5 *}
3.6
3.7 -ML {* val version_isac = "isac version 120503 17:32"; *}
3.8 +ML {* val version_isac = "isac version 120504 15:33"; *}
3.9
3.10 end
4.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri May 04 08:51:42 2012 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri May 04 17:33:31 2012 +0200
4.3 @@ -198,7 +198,7 @@
4.4
4.5 text {* rule set for functions called in the Script *}
4.6 ML {*
4.7 - val srls = Rls {id="srls_partial_fraction",
4.8 + val srls_partial_fraction = Rls {id="srls_partial_fraction",
4.9 preconds = [],
4.10 rew_ord = ("termlessI",termlessI),
4.11 erls = append_rls "erls_in_srls_partial_fraction" e_rls
4.12 @@ -242,7 +242,7 @@
4.13 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
4.14 ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
4.15 ("#Find" ,["decomposedFunction p_p"])],
4.16 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls,
4.17 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
4.18 crls = e_rls, nrls = e_rls},
4.19 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
4.20 " (let f_f = Take f_f; " ^
5.1 --- a/src/Tools/isac/ROOT.ML Fri May 04 08:51:42 2012 +0200
5.2 +++ b/src/Tools/isac/ROOT.ML Fri May 04 17:33:31 2012 +0200
5.3 @@ -4,7 +4,7 @@
5.4 $ ls -l /home/neuper/.isabelle/heaps/polyml-5.4.0_x86-linux/Isac
5.5
5.6 Knowledge/Isac.thy
5.7 -ML {* val version_isac = "isac version 120503 17:32"; *}
5.8 +ML {* val version_isac = "isac version 120504 15:33"; *}
5.9 *)
5.10
5.11 use_thys ["Build_Isac"];
6.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Fri May 04 08:51:42 2012 +0200
6.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Fri May 04 17:33:31 2012 +0200
6.3 @@ -1,4 +1,4 @@
6.4 -(* Title: inverse_z_transform
6.5 +(* Title: Knowledge/Inverse_Z_Transform/inverse_z_transform.sml
6.6 Author: Jan Rocnik
6.7 (c) copyright due to lincense terms.
6.8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6.9 @@ -36,10 +36,12 @@
6.10 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
6.11 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method *)
6.12 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
6.13 + (*([1], Frm)*)
6.14 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
6.15 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem --- DIFFERENCE TO ERROR*)
6.16 + (*([1], Res)*)
6.17 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Subproblem --- why NOT solve ?!?*)
6.18 f2str fb = "?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
6.19 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
6.20 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res)Model_Problem*)
6.21 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
6.22 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
6.23 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions z_i"*)
6.24 @@ -47,11 +49,26 @@
6.25 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
6.26 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
6.27 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method*)
6.28 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
6.29 -(*
6.30 -if f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0" andalso p = ([3, 1], Frm)
6.31 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0";
6.32 + (*([3, 1], Frm)*)
6.33 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / "^
6.34 + "(2 * 8) |\nz = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)";
6.35 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = 1 / 2 | z = -1 / 4";
6.36 + (*([3, 2], Res)*)
6.37 +if f2str fb = "z = 1 / 2 | z = -1 / 4" andalso p = ([3, 2], Res)
6.38 then () else error "begin of 'inv Z', exp 1 me changed"
6.39 -*)
6.40 +show_pt pt;
6.41 +(*[
6.42 +(([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
6.43 +(([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
6.44 +(([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
6.45 +(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
6.46 +(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
6.47 +(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)]
6.48 +(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
6.49 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
6.50 +(([3,2], Res), z = 1 / 2 | z = -1 / 4)] *)
6.51 +
6.52
6.53 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
6.54 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
6.55 @@ -136,7 +153,10 @@
6.56 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
6.57 (*====================================================================
6.58 (* Below are _all_ steps from BridgeLog; _superfluous_ ones and output are text.
6.59 - THE ERROR RESULTED FROM
6.60 + REASON FOR THE ERROR: Inverse_Z_Transform.thy did not contain final version of method.
6.61 +
6.62 +[[to sml: theory TTY_Communication imports Isac begin
6.63 +ML {* states := []; *}
6.64 *)
6.65 ML {* CalcTree [(["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
6.66 "stepResponse (x[n::real]::bool)"],("Isac",["Inverse","Z_Transform","SignalProcessing"],
7.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Fri May 04 08:51:42 2012 +0200
7.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri May 04 17:33:31 2012 +0200
7.3 @@ -12,6 +12,7 @@
7.4 "----------- Logic.unvarify_global ----------------------";
7.5 "----------- eval_drop_questionmarks --------------------";
7.6 "----------- = me for met_partial_fraction --------------";
7.7 +"----------- autoCalculate for met_partial_fraction -----";
7.8 "----------- progr.vers.2: check erls for multiply_ansatz";
7.9 "----------- progr.vers.2: improve program --------------";
7.10 "--------------------------------------------------------";
7.11 @@ -221,6 +222,94 @@
7.12 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
7.13 else error "= me .. met_partial_fraction broken";
7.14
7.15 +"----------- autoCalculate for met_partial_fraction -----";
7.16 +"----------- autoCalculate for met_partial_fraction -----";
7.17 +"----------- autoCalculate for met_partial_fraction -----";
7.18 +states:= [];
7.19 + val fmz =
7.20 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
7.21 + "solveFor z", "decomposedFunction p_p"];
7.22 + val (dI', pI', mI') =
7.23 + ("Partial_Fractions",
7.24 + ["partial_fraction", "rational", "simplification"],
7.25 + ["simplification","of_rationals","to_partial_fraction"]);
7.26 +CalcTree [(fmz, (dI' ,pI' ,mI'))];
7.27 +Iterator 1;
7.28 +moveActiveRoot 1;
7.29 +autoCalculate 1 CompleteCalc;
7.30 +
7.31 +val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
7.32 +if p = ip andalso ip = ([], Res) then ()
7.33 + else error "autoCalculate for met_partial_fraction changed: final pos'";
7.34 +
7.35 +val (Form f, tac, asms) = pt_extract (pt, p);
7.36 +if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
7.37 + tac = NONE andalso
7.38 + terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^
7.39 + "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
7.40 + "B is_polyexp,A is_polyexp," ^
7.41 + "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^
7.42 + "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
7.43 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
7.44 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z ~= 0,z is_polyexp]"
7.45 +then ()
7.46 + else error "autoCalculate for met_partial_fraction changed: final result"
7.47 +
7.48 +show_pt pt;
7.49 +(*[
7.50 +(([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
7.51 +(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
7.52 +(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
7.53 +(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
7.54 +(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
7.55 +(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
7.56 +z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
7.57 +(([2,2], Res), z = 1 / 2 | z = -1 / 4),
7.58 +(([2,3], Res), [z = 1 / 2, z = -1 / 4]),
7.59 +(([2,4], Res), [z = 1 / 2, z = -1 / 4]),
7.60 +(([2], Res), [z = 1 / 2, z = -1 / 4]),
7.61 +(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
7.62 +(([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
7.63 +(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
7.64 +(([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
7.65 +(([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
7.66 +(([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
7.67 +(([6], Res), 3 = 3 * A / 4),
7.68 +(([7], Pbl), solve (3 = 3 * A / 4, A)),
7.69 +(([7,1], Frm), 3 = 3 * A / 4),
7.70 +(([7,1], Res), 3 - 3 * A / 4 = 0),
7.71 +(([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
7.72 +(([7,3], Res), 3 + -3 / 4 * A = 0),
7.73 +(([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
7.74 +(([7,4,1], Frm), 3 + -3 / 4 * A = 0),
7.75 +(([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
7.76 +(([7,4,2], Res), A = -3 / (-3 / 4)),
7.77 +(([7,4,3], Res), A = 4),
7.78 +(([7,4,4], Res), [A = 4]),
7.79 +(([7,4,5], Res), [A = 4]),
7.80 +(([7,4], Res), [A = 4]),
7.81 +(([7], Res), [A = 4]),
7.82 +(([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
7.83 +(([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
7.84 +(([9], Res), 3 = -3 * B / 4),
7.85 +(([10], Pbl), solve (3 = -3 * B / 4, B)),
7.86 +(([10,1], Frm), 3 = -3 * B / 4),
7.87 +(([10,1], Res), 3 - -3 * B / 4 = 0),
7.88 +(([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
7.89 +(([10,3], Res), 3 + 3 / 4 * B = 0),
7.90 +(([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
7.91 +(([10,4,1], Frm), 3 + 3 / 4 * B = 0),
7.92 +(([10,4,1], Res), B = -1 * 3 / (3 / 4)),
7.93 +(([10,4,2], Res), B = -3 / (3 / 4)),
7.94 +(([10,4,3], Res), B = -4),
7.95 +(([10,4,4], Res), [B = -4]),
7.96 +(([10,4,5], Res), [B = -4]),
7.97 +(([10,4], Res), [B = -4]),
7.98 +(([10], Res), [B = -4]),
7.99 +(([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
7.100 +(([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
7.101 +(([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
7.102 +
7.103 "----------- progr.vers.2: check erls for multiply_ansatz";
7.104 "----------- progr.vers.2: check erls for multiply_ansatz";
7.105 "----------- progr.vers.2: check erls for multiply_ansatz";
8.1 --- a/test/Tools/isac/Test_Isac.thy Fri May 04 08:51:42 2012 +0200
8.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 04 17:33:31 2012 +0200
8.3 @@ -164,7 +164,7 @@
8.4 use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
8.5 use "Knowledge/partial_fractions.sml"
8.6 use "Knowledge/polyeq.sml"
8.7 -(*use "Knowledge/rlang.sml" much to clean up, not urgent due to other tests *)
8.8 +(*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
8.9 use "Knowledge/calculus.sml"
8.10 use "Knowledge/trig.sml"
8.11 (*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
9.1 --- a/test/Tools/isac/Test_Some.thy Fri May 04 08:51:42 2012 +0200
9.2 +++ b/test/Tools/isac/Test_Some.thy Fri May 04 17:33:31 2012 +0200
9.3 @@ -9,10 +9,173 @@
9.4 print_depth 5;
9.5 *}
9.6 ML {* (*==================*)
9.7 +store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
9.8 + (["SignalProcessing", "Z_Transform", "Inverse_sub"],
9.9 + [("#Given" ,["filterExpression X_eq"]),
9.10 + ("#Find" ,["stepResponse n_eq"])],
9.11 + {rew_ord'="tless_true",
9.12 + rls'= e_rls, calc = [],
9.13 + srls = Rls {id="srls_partial_fraction",
9.14 + preconds = [],
9.15 + rew_ord = ("termlessI",termlessI),
9.16 + erls = append_rls "erls_in_srls_partial_fraction" e_rls
9.17 + [(*for asm in NTH_CONS ...*)
9.18 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
9.19 + (*2nd NTH_CONS pushes n+-1 into asms*)
9.20 + Calc("Groups.plus_class.plus", eval_binop "#add_")],
9.21 + srls = Erls, calc = [],
9.22 + rules = [
9.23 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
9.24 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
9.25 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
9.26 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
9.27 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
9.28 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
9.29 + Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
9.30 + Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
9.31 + Calc("Partial_Fractions.factors_from_solution",
9.32 + eval_factors_from_solution "#factors_from_solution"),
9.33 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
9.34 + scr = EmptyScr},
9.35 + prls = e_rls, crls = e_rls, nrls = norm_Rational},
9.36 + "Script InverseZTransform (X_eq::bool) = "^
9.37 + (*(1/z) instead of z ^^^ -1*)
9.38 + "(let X = Take X_eq; "^
9.39 + " X' = Rewrite ruleZY False X; "^
9.40 + (*z * denominator*)
9.41 + " (num_orig::real) = get_numerator (rhs X'); "^
9.42 + " X' = (Rewrite_Set norm_Rational False) X'; "^
9.43 + (*simplify*)
9.44 + " (X'_z::real) = lhs X'; "^
9.45 + " (zzz::real) = argument_in X'_z; "^
9.46 + " (funterm::real) = rhs X'; "^
9.47 + (*drop X' z = for equation solving*)
9.48 + " (denom::real) = get_denominator funterm; "^
9.49 + (*get_denominator*)
9.50 + " (num::real) = get_numerator funterm; "^
9.51 + (*get_numerator*)
9.52 + " (equ::bool) = (denom = (0::real)); "^
9.53 + " (L_L::bool list) = (SubProblem (PolyEq', "^
9.54 + " [abcFormula,degree_2,polynomial,univariate,equation], "^
9.55 + " [no_met]) "^
9.56 + " [BOOL equ, REAL zzz]); "^
9.57 + " (facs::real) = factors_from_solution L_L; "^
9.58 + " (eql::real) = Take (num_orig / facs); "^
9.59 +
9.60 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
9.61 +
9.62 + " (eq::bool) = Take (eql = eqr); "^
9.63 + (*Maybe possible to use HOLogic.mk_eq ??*)
9.64 + " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
9.65 +
9.66 + " eq = drop_questionmarks eq; "^
9.67 + " (z1::real) = (rhs (NTH 1 L_L)); "^
9.68 + (*
9.69 + * prepare equation for a - eq_a
9.70 + * therefor substitute z with solution 1 - z1
9.71 + *)
9.72 + " (z2::real) = (rhs (NTH 2 L_L)); "^
9.73 +
9.74 + " (eq_a::bool) = Take eq; "^
9.75 + " eq_a = (Substitute [zzz=z1]) eq; "^
9.76 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
9.77 + " (sol_a::bool list) = "^
9.78 + " (SubProblem (Isac', "^
9.79 + " [univariate,equation],[no_met]) "^
9.80 + " [BOOL eq_a, REAL (A::real)]); "^
9.81 + " (a::real) = (rhs(NTH 1 sol_a)); "^
9.82 +
9.83 + " (eq_b::bool) = Take eq; "^
9.84 + " eq_b = (Substitute [zzz=z2]) eq_b; "^
9.85 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
9.86 + " (sol_b::bool list) = "^
9.87 + " (SubProblem (Isac', "^
9.88 + " [univariate,equation],[no_met]) "^
9.89 + " [BOOL eq_b, REAL (B::real)]); "^
9.90 + " (b::real) = (rhs(NTH 1 sol_b)); "^
9.91 +
9.92 + " eqr = drop_questionmarks eqr; "^
9.93 + " (pbz::real) = Take eqr; "^
9.94 + " pbz = ((Substitute [A=a, B=b]) pbz); "^
9.95 +
9.96 + " pbz = Rewrite ruleYZ False pbz; "^
9.97 + " pbz = drop_questionmarks pbz; "^
9.98 +
9.99 + " (X_z::bool) = Take (X_z = pbz); "^
9.100 + " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
9.101 + " n_eq = drop_questionmarks n_eq "^
9.102 + "in n_eq)"
9.103 + ));
9.104 +
9.105 +*}
9.106 +ML {*
9.107 +get_met ["SignalProcessing", "Z_Transform", "Inverse_sub"];
9.108 +*}
9.109 +ML {*
9.110 +*}
9.111 +ML {*
9.112 *}
9.113 ML {*
9.114 *}
9.115 ML {* (*==================*)
9.116 +"----------- test [SignalProcessing,Z_Transform,inverse] me = ----";
9.117 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
9.118 + "stepResponse (x[n::real]::bool)"];
9.119 +val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
9.120 + ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
9.121 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
9.122 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
9.123 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *)
9.124 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
9.125 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
9.126 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
9.127 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method *)
9.128 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
9.129 + (*([1], Frm)*)
9.130 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
9.131 + (*([1], Res)*)
9.132 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Subproblem --- why NOT solve ?!?*)
9.133 + f2str fb = "?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
9.134 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res)Model_Problem*)
9.135 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
9.136 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
9.137 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions z_i"*)
9.138 +*}
9.139 +ML {*
9.140 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory ?!? Empty_Tac
9.141 + ..., Given = [Correct "equality (get_denominator (24 / (-1 + -2 * z + 8 * z ^^^ 2)) = 0)"
9.142 + ^^^^^^^^^^^^^^^ why not evaluated ?*)
9.143 +*}
9.144 +ML {*
9.145 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*)
9.146 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*)
9.147 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method*)
9.148 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0";
9.149 + (*([3, 1], Frm)*)
9.150 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / "^
9.151 + "(2 * 8) |\nz = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)";
9.152 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = 1 / 2 | z = -1 / 4";
9.153 + (*([3, 2], Res)*)
9.154 +if f2str fb = "z = 1 / 2 | z = -1 / 4" andalso p = ([3, 2], Res)
9.155 + then () else error "begin of 'inv Z', exp 1 me changed";
9.156 +show_pt pt;
9.157 +(*[
9.158 +(([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
9.159 +(([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
9.160 +(([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
9.161 +(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
9.162 +(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
9.163 +(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)]
9.164 +(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
9.165 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
9.166 +(([3,2], Res), z = 1 / 2 | z = -1 / 4)] *)
9.167 +
9.168 +*}
9.169 +ML {* (*==================*)
9.170 +*}
9.171 +ML {*
9.172 +*}
9.173 +ML {*
9.174 *}
9.175 ML {*
9.176 *}