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