7 val thy = @{theory "Isac"}; |
7 val thy = @{theory "Isac"}; |
8 val ctxt = ProofContext.init_global thy; |
8 val ctxt = ProofContext.init_global thy; |
9 print_depth 5; |
9 print_depth 5; |
10 *} |
10 *} |
11 ML {* (*==================*) |
11 ML {* (*==================*) |
12 *} |
12 store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID |
13 ML {* |
13 (["SignalProcessing", "Z_Transform", "Inverse_sub"], |
14 *} |
14 [("#Given" ,["filterExpression X_eq"]), |
15 ML {* (*==================*) |
15 ("#Find" ,["stepResponse n_eq"])], |
|
16 {rew_ord'="tless_true", |
|
17 rls'= e_rls, calc = [], |
|
18 srls = Rls {id="srls_partial_fraction", |
|
19 preconds = [], |
|
20 rew_ord = ("termlessI",termlessI), |
|
21 erls = append_rls "erls_in_srls_partial_fraction" e_rls |
|
22 [(*for asm in NTH_CONS ...*) |
|
23 Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
|
24 (*2nd NTH_CONS pushes n+-1 into asms*) |
|
25 Calc("Groups.plus_class.plus", eval_binop "#add_")], |
|
26 srls = Erls, calc = [], |
|
27 rules = [ |
|
28 Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
|
29 Calc("Groups.plus_class.plus", eval_binop "#add_"), |
|
30 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
|
31 Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
|
32 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
|
33 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), |
|
34 Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), |
|
35 Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
|
36 Calc("Partial_Fractions.factors_from_solution", |
|
37 eval_factors_from_solution "#factors_from_solution"), |
|
38 Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")], |
|
39 scr = EmptyScr}, |
|
40 prls = e_rls, crls = e_rls, nrls = norm_Rational}, |
|
41 "Script InverseZTransform (X_eq::bool) = "^ |
|
42 (*(1/z) instead of z ^^^ -1*) |
|
43 "(let X = Take X_eq; "^ |
|
44 " X' = Rewrite ruleZY False X; "^ |
|
45 (*z * denominator*) |
|
46 " (num_orig::real) = get_numerator (rhs X'); "^ |
|
47 " X' = (Rewrite_Set norm_Rational False) X'; "^ |
|
48 (*simplify*) |
|
49 " (X'_z::real) = lhs X'; "^ |
|
50 " (zzz::real) = argument_in X'_z; "^ |
|
51 " (funterm::real) = rhs X'; "^ |
|
52 (*drop X' z = for equation solving*) |
|
53 " (denom::real) = get_denominator funterm; "^ |
|
54 (*get_denominator*) |
|
55 " (num::real) = get_numerator funterm; "^ |
|
56 (*get_numerator*) |
|
57 " (equ::bool) = (denom = (0::real)); "^ |
|
58 " (L_L::bool list) = (SubProblem (PolyEq', "^ |
|
59 " [abcFormula,degree_2,polynomial,univariate,equation], "^ |
|
60 " [no_met]) "^ |
|
61 " [BOOL equ, REAL zzz]); "^ |
|
62 " (facs::real) = factors_from_solution L_L; "^ |
|
63 " (eql::real) = Take (num_orig / facs); "^ |
|
64 |
|
65 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^ |
|
66 |
|
67 " (eq::bool) = Take (eql = eqr); "^ |
|
68 (*Maybe possible to use HOLogic.mk_eq ??*) |
|
69 " eq = (Try (Rewrite_Set equival_trans False)) eq; "^ |
|
70 |
|
71 " eq = drop_questionmarks eq; "^ |
|
72 " (z1::real) = (rhs (NTH 1 L_L)); "^ |
|
73 (* |
|
74 * prepare equation for a - eq_a |
|
75 * therefor substitute z with solution 1 - z1 |
|
76 *) |
|
77 " (z2::real) = (rhs (NTH 2 L_L)); "^ |
|
78 |
|
79 " (eq_a::bool) = Take eq; "^ |
|
80 " eq_a = (Substitute [zzz=z1]) eq; "^ |
|
81 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^ |
|
82 " (sol_a::bool list) = "^ |
|
83 " (SubProblem (Isac', "^ |
|
84 " [univariate,equation],[no_met]) "^ |
|
85 " [BOOL eq_a, REAL (A::real)]); "^ |
|
86 " (a::real) = (rhs(NTH 1 sol_a)); "^ |
|
87 |
|
88 " (eq_b::bool) = Take eq; "^ |
|
89 " eq_b = (Substitute [zzz=z2]) eq_b; "^ |
|
90 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^ |
|
91 " (sol_b::bool list) = "^ |
|
92 " (SubProblem (Isac', "^ |
|
93 " [univariate,equation],[no_met]) "^ |
|
94 " [BOOL eq_b, REAL (B::real)]); "^ |
|
95 " (b::real) = (rhs(NTH 1 sol_b)); "^ |
|
96 |
|
97 " eqr = drop_questionmarks eqr; "^ |
|
98 " (pbz::real) = Take eqr; "^ |
|
99 " pbz = ((Substitute [A=a, B=b]) pbz); "^ |
|
100 |
|
101 " pbz = Rewrite ruleYZ False pbz; "^ |
|
102 " pbz = drop_questionmarks pbz; "^ |
|
103 |
|
104 " (X_z::bool) = Take (X_z = pbz); "^ |
|
105 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^ |
|
106 " n_eq = drop_questionmarks n_eq "^ |
|
107 "in n_eq)" |
|
108 )); |
|
109 |
|
110 *} |
|
111 ML {* |
|
112 get_met ["SignalProcessing", "Z_Transform", "Inverse_sub"]; |
|
113 *} |
|
114 ML {* |
|
115 *} |
|
116 ML {* |
|
117 *} |
|
118 ML {* |
|
119 *} |
|
120 ML {* (*==================*) |
|
121 "----------- test [SignalProcessing,Z_Transform,inverse] me = ----"; |
|
122 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", |
|
123 "stepResponse (x[n::real]::bool)"]; |
|
124 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], |
|
125 ["SignalProcessing", "Z_Transform", "Inverse_sub"]); |
|
126 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*) |
|
127 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*) |
|
128 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = *) |
|
129 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*) |
|
130 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*) |
|
131 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*) |
|
132 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method *) |
|
133 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; |
|
134 (*([1], Frm)*) |
|
135 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb="?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; |
|
136 (*([1], Res)*) |
|
137 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([2], Res) Subproblem --- why NOT solve ?!?*) |
|
138 f2str fb = "?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)"; |
|
139 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*([3], Res)Model_Problem*) |
|
140 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*) |
|
141 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*) |
|
142 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "solutions z_i"*) |
|
143 *} |
|
144 ML {* |
|
145 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory ?!? Empty_Tac |
|
146 ..., Given = [Correct "equality (get_denominator (24 / (-1 + -2 * z + 8 * z ^^^ 2)) = 0)" |
|
147 ^^^^^^^^^^^^^^^ why not evaluated ?*) |
|
148 *} |
|
149 ML {* |
|
150 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem*) |
|
151 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method*) |
|
152 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method*) |
|
153 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0"; |
|
154 (*([3, 1], Frm)*) |
|
155 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / "^ |
|
156 "(2 * 8) |\nz = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)"; |
|
157 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; f2str fb = "z = 1 / 2 | z = -1 / 4"; |
|
158 (*([3, 2], Res)*) |
|
159 if f2str fb = "z = 1 / 2 | z = -1 / 4" andalso p = ([3, 2], Res) |
|
160 then () else error "begin of 'inv Z', exp 1 me changed"; |
|
161 show_pt pt; |
|
162 (*[ |
|
163 (([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])), |
|
164 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))), |
|
165 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), |
|
166 (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)), |
|
167 (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)), |
|
168 (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0)] |
|
169 (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) | |
|
170 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)), |
|
171 (([3,2], Res), z = 1 / 2 | z = -1 / 4)] *) |
|
172 |
|
173 *} |
|
174 ML {* (*==================*) |
|
175 *} |
|
176 ML {* |
|
177 *} |
|
178 ML {* |
16 *} |
179 *} |
17 ML {* |
180 ML {* |
18 *} |
181 *} |
19 ML {* (*==================*) |
182 ML {* (*==================*) |
20 "~~~~~ fun , args:"; val () = (); |
183 "~~~~~ fun , args:"; val () = (); |