|
neuper@42289
|
1 |
(* Title: partial fraction decomposition
|
|
neuper@42289
|
2 |
Author: Jan Rocnik
|
|
neuper@42289
|
3 |
(c) due to copyright terms
|
|
neuper@42289
|
4 |
*)
|
|
neuper@42289
|
5 |
|
|
neuper@42289
|
6 |
"--------------------------------------------------------";
|
|
neuper@42289
|
7 |
"table of contents --------------------------------------";
|
|
neuper@42289
|
8 |
"--------------------------------------------------------";
|
|
neuper@42305
|
9 |
"----------- why helpless here ? ------------------------";
|
|
neuper@42310
|
10 |
"----------- why not nxt = Model_Problem here ? ---------";
|
|
neuper@42359
|
11 |
"----------- fun factors_from_solution ------------------";
|
|
neuper@42359
|
12 |
"----------- Logic.unvarify_global ----------------------";
|
|
neuper@42359
|
13 |
"----------- eval_drop_questionmarks --------------------";
|
|
neuper@42376
|
14 |
"----------- = me for met_partial_fraction --------------";
|
|
neuper@42289
|
15 |
"--------------------------------------------------------";
|
|
neuper@42289
|
16 |
"--------------------------------------------------------";
|
|
neuper@42289
|
17 |
"--------------------------------------------------------";
|
|
neuper@42289
|
18 |
|
|
neuper@42289
|
19 |
|
|
neuper@42305
|
20 |
"----------- why helpless here ? ------------------------";
|
|
neuper@42305
|
21 |
"----------- why helpless here ? ------------------------";
|
|
neuper@42305
|
22 |
"----------- why helpless here ? ------------------------";
|
|
neuper@42305
|
23 |
val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
|
|
neuper@42305
|
24 |
"stepResponse (x[n::real]::bool)"];
|
|
neuper@42305
|
25 |
val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
|
|
neuper@42305
|
26 |
["SignalProcessing","Z_Transform","inverse"]);
|
|
neuper@42305
|
27 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
|
|
neuper@42305
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
|
|
neuper@42305
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
|
|
neuper@42305
|
30 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
|
|
neuper@42305
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
|
|
neuper@42305
|
32 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
|
|
neuper@42305
|
33 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
|
|
neuper@42315
|
34 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
|
|
neuper@42315
|
35 |
val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
|
|
neuper@42305
|
36 |
"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
|
|
neuper@42305
|
37 |
val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
|
|
neuper@42305
|
38 |
val (pt, p) = ptp;
|
|
neuper@42305
|
39 |
"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
|
|
neuper@42305
|
40 |
(p, ((pt, e_pos'),[]));
|
|
neuper@42305
|
41 |
val pIopt = get_pblID (pt,ip);
|
|
neuper@42305
|
42 |
ip = ([],Res); "false";
|
|
neuper@42305
|
43 |
tacis; " = []";
|
|
neuper@42305
|
44 |
pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
|
|
neuper@42305
|
45 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
|
|
neuper@42305
|
46 |
(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
|
|
neuper@42305
|
47 |
THIS MEANS: replace no_meth by [no_meth] in Script.*)
|
|
neuper@42305
|
48 |
(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
|
|
neuper@42305
|
49 |
(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
|
|
neuper@42289
|
50 |
|
|
neuper@42310
|
51 |
"----------- why not nxt = Model_Problem here ? ---------";
|
|
neuper@42310
|
52 |
"----------- why not nxt = Model_Problem here ? ---------";
|
|
neuper@42310
|
53 |
"----------- why not nxt = Model_Problem here ? ---------";
|
|
neuper@42313
|
54 |
val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
|
|
neuper@42313
|
55 |
"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
|
|
neuper@42313
|
56 |
val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
|
|
neuper@42313
|
57 |
val (pt, p) = ptp;
|
|
neuper@42313
|
58 |
"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
|
|
neuper@42313
|
59 |
(p, ((pt, e_pos'),[]));
|
|
neuper@42313
|
60 |
val pIopt = get_pblID (pt,ip);
|
|
neuper@42313
|
61 |
ip = ([],Res); " = false";
|
|
neuper@42313
|
62 |
tacis; " = []";
|
|
neuper@42313
|
63 |
pIopt (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*);
|
|
neuper@42313
|
64 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
|
|
neuper@42313
|
65 |
(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
|
|
neuper@42313
|
66 |
nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
|
|
neuper@42313
|
67 |
This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
|
|
neuper@42313
|
68 |
See TODO.txt
|
|
neuper@42313
|
69 |
*)
|
|
neuper@42310
|
70 |
|
|
neuper@42359
|
71 |
"----------- fun factors_from_solution ------------------";
|
|
neuper@42359
|
72 |
"----------- fun factors_from_solution ------------------";
|
|
neuper@42359
|
73 |
"----------- fun factors_from_solution ------------------";
|
|
neuper@42359
|
74 |
val ctxt = ProofContext.init_global @{theory Isac};
|
|
jan@42352
|
75 |
val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
|
|
jan@42352
|
76 |
val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
|
|
jan@42352
|
77 |
if term2str t' =
|
|
neuper@42376
|
78 |
"factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
|
|
jan@42352
|
79 |
then () else error "factors_from_solution broken";
|
|
jan@42352
|
80 |
|
|
neuper@42359
|
81 |
"----------- Logic.unvarify_global ----------------------";
|
|
neuper@42359
|
82 |
"----------- Logic.unvarify_global ----------------------";
|
|
neuper@42359
|
83 |
"----------- Logic.unvarify_global ----------------------";
|
|
neuper@42359
|
84 |
val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
|
|
neuper@42359
|
85 |
val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
|
|
jan@42352
|
86 |
|
|
neuper@42359
|
87 |
val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
|
|
neuper@42359
|
88 |
val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
|
|
neuper@42359
|
89 |
|
|
neuper@42359
|
90 |
val test = HOLogic.mk_binop "Groups.plus_class.plus"
|
|
neuper@42359
|
91 |
(HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
|
|
neuper@42359
|
92 |
HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
|
|
neuper@42359
|
93 |
|
|
neuper@42359
|
94 |
if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
|
|
neuper@42359
|
95 |
else error "HOLogic.mk_binop broken ?";
|
|
neuper@42359
|
96 |
|
|
neuper@42359
|
97 |
(* Logic.unvarify_global test
|
|
neuper@42359
|
98 |
---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
|
|
neuper@42359
|
99 |
thus we need another fun var2free in termC.sml*)
|
|
neuper@42359
|
100 |
|
|
neuper@42359
|
101 |
"----------- eval_drop_questionmarks --------------------";
|
|
neuper@42359
|
102 |
"----------- eval_drop_questionmarks --------------------";
|
|
neuper@42359
|
103 |
"----------- eval_drop_questionmarks --------------------";
|
|
neuper@42359
|
104 |
if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))"
|
|
neuper@42359
|
105 |
then () else error "test setup (ctxt!) probably changed";
|
|
neuper@42359
|
106 |
|
|
neuper@42359
|
107 |
val t = Const ("Partial_Fractions.drop_questionmarks", HOLogic.realT --> HOLogic.realT) $ test;
|
|
neuper@42359
|
108 |
|
|
neuper@42359
|
109 |
val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
|
|
neuper@42359
|
110 |
if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
|
|
neuper@42359
|
111 |
"\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
|
|
neuper@42359
|
112 |
then () else error "eval_drop_questionmarks broken";
|
|
neuper@42359
|
113 |
|
|
neuper@42376
|
114 |
"----------- = me for met_partial_fraction --------------";
|
|
neuper@42376
|
115 |
"----------- = me for met_partial_fraction --------------";
|
|
neuper@42376
|
116 |
"----------- = me for met_partial_fraction --------------";
|
|
neuper@42376
|
117 |
val fmz =
|
|
neuper@42376
|
118 |
["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
|
|
neuper@42376
|
119 |
"solveFor z", "decomposedFunction p_p"];
|
|
neuper@42376
|
120 |
val (dI',pI',mI') =
|
|
neuper@42376
|
121 |
("Partial_Fractions",
|
|
neuper@42376
|
122 |
["partial_fraction", "rational", "simplification"],
|
|
neuper@42376
|
123 |
["simplification","of_rationals","to_partial_fraction"]);
|
|
neuper@42376
|
124 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@42376
|
125 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
126 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
127 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
132 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
133 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
134 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
135 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
136 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
147 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
149 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
150 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
151 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
152 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
154 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
159 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
160 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
161 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
163 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
164 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
165 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
166 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
167 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
168 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
169 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
170 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
174 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
177 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
178 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
179 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
182 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
183 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
185 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
186 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
187 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
188 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
189 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
191 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
192 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
193 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
194 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
195 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
196 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
197 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
198 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
200 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
202 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
203 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
204 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
206 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
208 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
209 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
210 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
211 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
213 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
214 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
215 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
216 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
neuper@42376
|
217 |
|
|
neuper@42376
|
218 |
show_pt pt;
|
|
neuper@42376
|
219 |
if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
|
|
neuper@42376
|
220 |
else error "= me .. met_partial_fraction broken";
|
|
neuper@42376
|
221 |
|