1 (* Title: "Knowledge/partial_fractions.sml"
2 partial fraction decomposition
4 (c) due to copyright terms
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 "----------- why helpless here ? ------------------------";
11 "----------- why not nxt = Model_Problem here ? ---------";
12 "----------- fun factors_from_solution ------------------";
13 "----------- Logic.unvarify_global ----------------------";
14 "----------- eval_drop_questionmarks --------------------";
15 "----------- = me for met_partial_fraction --------------";
16 "----------- autoCalculate for met_partial_fraction -----";
17 "----------- progr.vers.2: check erls for multiply_ansatz";
18 "----------- progr.vers.2: improve program --------------";
19 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
20 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
23 "--------------------------------------------------------";
26 "----------- why helpless here ? ------------------------";
27 "----------- why helpless here ? ------------------------";
28 "----------- why helpless here ? ------------------------";
29 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))",
30 "functionName X_z", "stepResponse (x[n::real]::bool)"];
31 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
32 ["SignalProcessing", "Z_Transform", "Inverse"]);
33 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
40 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))";
41 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)))";
42 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
43 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
45 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
46 (p, ((pt, e_pos'),[]));
47 val pIopt = get_pblID (pt,ip);
48 ip = ([],Res); "false";
50 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
51 member op = [Pbl,Met] p_ ; "false";
52 (*Step_Solve.do_next (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
53 THIS MEANS: replace no_meth by [no_meth] in Program.*)
54 (*WAS val ("helpless",_) = Step.do_next p ((pt, e_pos'),[]) *)
55 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
57 "----------- why not nxt = Model_Problem here ? ---------";
58 "----------- why not nxt = Model_Problem here ? ---------";
59 "----------- why not nxt = Model_Problem here ? ---------";
60 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
61 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
62 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p);
64 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
65 (p, ((pt, e_pos'),[]));
66 val pIopt = get_pblID (pt,ip);
67 ip = ([],Res); " = false";
69 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
70 member op = [Pbl,Met] p_; " = false";
71 (* \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^ leads into
72 Step_Solve.do_next, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
73 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without implicit_take.
77 "----------- fun factors_from_solution ------------------";
78 "----------- fun factors_from_solution ------------------";
79 "----------- fun factors_from_solution ------------------";
80 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
81 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = - 1 / 4]";
82 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
84 "factors_from_solution [z = 1 / 2, z = - 1 / 4] = (z - 1 / 2) * (z - - 1 / 4)"
85 then () else error "factors_from_solution broken";
87 "----------- Logic.unvarify_global ----------------------";
88 "----------- Logic.unvarify_global ----------------------";
89 "----------- Logic.unvarify_global ----------------------";
90 val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
91 val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
93 val denom1 = parseNEW ctxt "(z + - 1 * (1 / 2))::real" |> the;
94 val denom2 = parseNEW ctxt "(z + - 1 * (- 1 / 4))::real" |> the;
96 val test = HOLogic.mk_binop \<^const_name>\<open>plus\<close>
97 (HOLogic.mk_binop \<^const_name>\<open>divide\<close> (A_var, denom1),
98 HOLogic.mk_binop \<^const_name>\<open>divide\<close> (B_var, denom2));
100 if UnparseC.term test = "?A / (z + - 1 * (1 / 2)) + ?B / (z + - 1 * (- 1 / 4))" then ()
101 else error "HOLogic.mk_binop broken ?";
103 (* Logic.unvarify_global test
104 ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
105 thus we need another fun var2free in termC.sml*)
107 "----------- = me for met_partial_fraction --------------";
108 "----------- = me for met_partial_fraction --------------";
109 "----------- = me for met_partial_fraction --------------";
111 ["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))",
112 "solveFor z", "decomposedFunction p_p"];
114 ("Partial_Fractions",
115 ["partial_fraction", "rational", "simplification"],
116 ["simplification", "of_rationals", "to_partial_fraction"]);
117 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) =
118 CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
119 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))")*)
120 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
121 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)
122 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)
124 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)
125 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
126 (*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
127 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)
128 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
130 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)
131 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + - 2 * z + 8 * z \<up> 2 = 0)")*)
132 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
133 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)
134 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)
136 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
137 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
138 (*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
139 (*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
140 (*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)
142 (*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)
143 (*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)
144 (*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
145 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - - 1 / 4))")*)
146 (*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)
148 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - - 1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - - 1 / 4)")*)
149 (*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)
150 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - - 1 / 4) + BB * (z - 1 / 2)"*)
151 (*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
152 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
153 (*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac_Knowledge", ["normalise", "polynomial", "univariate", "equation"]*)
155 (*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
156 (*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
157 (*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
158 (*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
159 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac_Knowledge"*)
161 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
162 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
163 (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
164 (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
165 (*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
167 (*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
168 (*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac_Knowledge", ["degree_1", "polynomial", "univariate", "equation"])*)
169 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
170 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
171 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
173 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
174 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
175 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
176 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
177 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
179 (*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
180 (*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
181 (*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
182 (*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
183 (*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
185 (*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
186 (*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
187 (*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
188 (*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
189 (*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
191 (*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
192 (*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
193 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
194 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
195 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
197 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
198 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
199 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
200 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
201 (*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
203 (*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
204 (*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
205 (*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
206 (*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
207 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
209 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
210 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
211 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
212 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
213 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
215 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
216 (*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
217 (*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
218 (*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
219 (*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
221 (*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
222 (*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
223 (*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)
224 (*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
226 (*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - - 1 / 4)"*)
228 (*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)
229 (*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)
230 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
233 (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" then ()
234 else error "= me .. met_partial_fraction f changed"
235 | _ => error "= me .. met_partial_fraction nxt changed";
237 Test_Tool.show_pt_tac pt; (**)
239 "----------- autoCalculate for met_partial_fraction -----";
240 "----------- autoCalculate for met_partial_fraction -----";
241 "----------- autoCalculate for met_partial_fraction -----";
244 ["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))",
245 "solveFor z", "decomposedFunction p_p"];
246 val (dI', pI', mI') =
247 ("Partial_Fractions",
248 ["partial_fraction", "rational", "simplification"],
249 ["simplification", "of_rationals", "to_partial_fraction"]);
250 CalcTree [(fmz, (dI' ,pI' ,mI'))];
253 autoCalculate 1 CompleteCalc;
255 val ((pt,p),_) = States.get_calc 1; val ip = States.get_pos 1 1;
256 if p = ip andalso ip = ([], Res) then ()
257 else error "autoCalculate for met_partial_fraction changed: final pos'";
259 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
260 if UnparseC.term f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" andalso
261 UnparseC.terms_short asms =
262 "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^
263 "lhs (- 1 + - 2 * z + 8 * z \<up> 2 = 0) has_degree_in z = 2," ^
264 "lhs (- 1 + - 2 * z + 8 * z \<up> 2 = 0) is_poly_in z,z = 1 / 2,z = - 1 / 4,z is_polyexp]"
265 then case tac of NONE => ()
266 | _ => error "me for met_partial_fraction changed: final result 1"
267 else error "me for met_partial_fraction changed: final result 2"
269 Test_Tool.show_pt pt; (**)
271 "----------- progr.vers.2: check erls for multiply_ansatz";
272 "----------- progr.vers.2: check erls for multiply_ansatz";
273 "----------- progr.vers.2: check erls for multiply_ansatz";
274 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
275 val t = TermC.parse_test @{context} "(3 / ((- 1 + - 2 * z + 8 * z \<up> 2) *3/24)) = (3 / ((z - 1 / 2) * (z - - 1 / 4)))";
276 val SOME (t', _) = rewrite_set_ @{theory Isac_Knowledge} true ansatz_rls t;
277 UnparseC.term t' = "3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - - 1 / 4)";
279 val SOME (t'', _) = rewrite_set_ @{theory Isac_Knowledge} true multiply_ansatz t'; (*true*)
280 UnparseC.term t'' = "(z - 1 / 2) * (z - - 1 / 4) * 3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n" ^
281 "?A * (z - - 1 / 4) + ?B * (z - 1 / 2)"; (*true*)
283 val SOME (t''', _) = rewrite_set_ @{theory Isac_Knowledge} true norm_Rational t'';
284 if UnparseC.term t''' = "3 = (AA + - 2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
285 else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
287 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
288 val xxx = Rule_Set.append_rules "multiply_ansatz_erls" norm_Rational
289 [Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")];
291 val multiply_ansatz = prep_rls @{theory} (
292 Rule_Set.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
294 srls = Rule_Set.Empty, calc = [], errpatts = [],
296 [Thm ("multiply_2nd_order",ThmC.numerals_to_Free @{thm multiply_2nd_order})
298 scr = Empty_Prog}:rls);
300 rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
301 rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)
303 "----------- progr.vers.2: improve program --------------";
304 "----------- progr.vers.2: improve program --------------";
305 "----------- progr.vers.2: improve program --------------";
306 (*WN120318 stopped due to much effort with the test above*)
307 "Program PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z)), zzz: z*)
308 " (let f_f = Take f_f; " ^
309 " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
310 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (- 1 + - 2 * z + 8 * z \<up> 2)*)
311 " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
312 " (denom::real) = get_denominator f_f; " ^(*denom: - 1 + - 2 * z + 8 * z \<up> 2*)
313 " (equ::bool) = (denom = (0::real)); " ^(*equ: - 1 + - 2 * z + 8 * z \<up> 2 = 0*)
314 " (L_L::bool list) = (SubProblem (PolyEqX, " ^
315 " [abcFormula, degree_2, polynomial, univariate, equation], " ^
316 " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = - 1 / 4]*)
317 " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - - 1 / 4)*)
318 " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - - 1 / 4)) *)
319 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - - 1 / 4)*)
320 " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - - 1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - - 1 / 4)*)
321 (*this has been tested below by rewrite_set_
322 " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
323 " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
324 " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - - 1 / 4) + ?B * (z - 1 / 2)*)
325 NEXT try to outcomment the very next line..*)
326 " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - - 1 / 4) + ?B * (z - 1 / 2)*)
327 " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*)
328 " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
329 " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: - 1 / 4*)
330 " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*)
331 " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - - 1 / 4) + B * (1 / 2 - 1 / 2)*)
332 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
333 " (sol_a::bool list) = " ^
334 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
335 " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
336 " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
337 " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*)
338 " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
339 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
340 " (sol_b::bool list) = " ^
341 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
342 " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
343 " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
344 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - - 1 / 4)*)
345 " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - - 1 / 4)*)
346 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - - 1 / 4)*)
349 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
350 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
351 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
352 val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
353 (["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", "solveFor z",
354 "decomposedFunction p_p'''"],
355 ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"],
356 ["simplification", "of_rationals", "to_partial_fraction"]))
357 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz_from_Subproblem_of_Inverse_sub)];
358 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
359 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
360 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
361 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
362 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
363 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
364 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
365 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
366 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
367 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
368 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
372 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
373 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
374 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
375 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
376 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
377 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
378 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
379 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
380 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
381 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
382 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
383 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
384 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
385 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
386 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
387 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
388 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
389 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
392 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
400 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
401 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
402 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
403 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
405 if fst nxt = "End_Proof'" andalso f2str f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" then ()
406 else error "--- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---";
409 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
410 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
411 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
413 (*val PblObj {fmz_from_Subproblem_of_Inverse_sub, ...} = get_obj I pt (fst p)
414 see --- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";*)
416 val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
417 (["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", "solveFor z",
418 "decomposedFunction p_p'''"],
419 ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"],
420 ["simplification", "of_rationals", "to_partial_fraction"]));
421 CalcTree [fmz_from_Subproblem_of_Inverse_sub];
425 autoCalculate 1 CompleteCalc;
426 exception Empty raised (line 429 of "library.ML") TODO during lucin: *)
429 LItool.trace_on := true;
431 @@@ program ["simplification", "of_rationals", "to_partial_fraction"]
433 (f_f, 3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", "
435 @@@ next leaf 'Take f_f' ---> Program.Tac 'Take (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))'