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 "--------------------------------------------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
24 "----------- why helpless here ? ------------------------";
25 "----------- why helpless here ? ------------------------";
26 "----------- why helpless here ? ------------------------";
27 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
28 "stepResponse (x[n::real]::bool)"];
29 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
30 ["SignalProcessing","Z_Transform","Inverse"]);
31 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
38 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))";
39 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)))";
40 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
41 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
43 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
44 (p, ((pt, e_pos'),[]));
45 val pIopt = get_pblID (pt,ip);
46 ip = ([],Res); "false";
48 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
49 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
50 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
51 THIS MEANS: replace no_meth by [no_meth] in Script.*)
52 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
53 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
55 "----------- why not nxt = Model_Problem here ? ---------";
56 "----------- why not nxt = Model_Problem here ? ---------";
57 "----------- why not nxt = Model_Problem here ? ---------";
58 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
59 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
60 val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
62 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
63 (p, ((pt, e_pos'),[]));
64 val pIopt = get_pblID (pt,ip);
65 ip = ([],Res); " = false";
67 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
68 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
69 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
70 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
71 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
75 "----------- fun factors_from_solution ------------------";
76 "----------- fun factors_from_solution ------------------";
77 "----------- fun factors_from_solution ------------------";
78 val ctxt = Proof_Context.init_global @{theory Isac};
79 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
80 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
82 "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
83 then () else error "factors_from_solution broken";
85 "----------- Logic.unvarify_global ----------------------";
86 "----------- Logic.unvarify_global ----------------------";
87 "----------- Logic.unvarify_global ----------------------";
88 val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
89 val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
91 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
92 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
94 val test = HOLogic.mk_binop "Groups.plus_class.plus"
95 (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),
96 HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));
98 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
99 else error "HOLogic.mk_binop broken ?";
101 (* Logic.unvarify_global test
102 ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
103 thus we need another fun var2free in termC.sml*)
105 "----------- = me for met_partial_fraction --------------";
106 "----------- = me for met_partial_fraction --------------";
107 "----------- = me for met_partial_fraction --------------";
109 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
110 "solveFor z", "decomposedFunction p_p"];
112 ("Partial_Fractions",
113 ["partial_fraction", "rational", "simplification"],
114 ["simplification","of_rationals","to_partial_fraction"]);
115 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) =
116 CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
117 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)
118 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
119 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)
120 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)
122 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)
123 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
124 (*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
125 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)
126 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
128 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)
129 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
130 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
131 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)
132 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)
134 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
135 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
136 (*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
137 (*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
138 (*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)
140 (*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)
141 (*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)
142 (*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
143 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)
144 (*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)
146 (*[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)")*)
147 (*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)
148 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
149 (*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
150 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
151 (*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)
153 (*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
154 (*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
155 (*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
156 (*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
157 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)
159 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
160 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
161 (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
162 (*[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)"))*)
163 (*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
165 (*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
166 (*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)
167 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
168 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
169 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
171 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
172 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
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 = *)
177 (*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
178 (*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
179 (*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
180 (*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
181 (*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
183 (*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
184 (*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
185 (*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
186 (*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
187 (*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
189 (*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
190 (*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
191 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
192 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
193 (*[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 = *)
196 (*[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], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
201 (*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
202 (*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
203 (*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
204 (*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
205 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
207 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
208 (*[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 = *)
213 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
214 (*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
215 (*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
216 (*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
217 (*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
219 (*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
220 (*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
221 (*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)
222 (*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
224 (*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)
226 (*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)
227 (*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)
228 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
231 (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then ()
232 else error "= me .. met_partial_fraction f changed"
233 | _ => error "= me .. met_partial_fraction nxt changed";
237 (''Partial_Fractions'',
238 ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
240 . . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
241 ([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
242 . . . . . . . . . . Rewrite_Set "norm_Rational",
243 ([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
244 . . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
245 ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
246 . . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
247 ([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
248 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
249 ([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
250 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
251 . . . . . . . . . . Rewrite_Set "polyeq_simplify",
252 ([2,2], Res), z = 1 / 2 \<or> z = -1 / 4
253 . . . . . . . . . . Or_to_List ,
254 ([2,3], Res), [z = 1 / 2, z = -1 / 4]
255 . . . . . . . . . . Check_elementwise "Assumptions",
256 ([2,4], Res), [z = 1 / 2, z = -1 / 4]
257 . . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
258 ([2], Res), [z = 1 / 2, z = -1 / 4]
259 . . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
260 ([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
261 . . . . . . . . . . Rewrite_Set "ansatz_rls",
262 ([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
263 . . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
264 ([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
265 . . . . . . . . . . Rewrite_Set "equival_trans",
266 ([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
267 . . . . . . . . . . Substitute ["z = 1 / 2"],
268 ([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
269 . . . . . . . . . . Rewrite_Set "norm_Rational",
270 ([6], Res), 3 = 3 * AA / 4
271 . . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
272 ([7], Pbl), solve (3 = 3 * AA / 4, AA)
273 . . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
274 ([7,1], Frm), 3 = 3 * AA / 4
275 . . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
276 ([7,1], Res), 3 - 3 * AA / 4 = 0
277 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
278 ([7,2], Res), 3 / 1 + -3 / 4 * AA = 0
279 . . . . . . . . . . Rewrite_Set "polyeq_simplify",
280 ([7,3], Res), 3 + -3 / 4 * AA = 0
281 . . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
282 ([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)
283 . . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
284 ([7,4,1], Frm), 3 + -3 / 4 * AA = 0
285 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),
286 ([7,4,1], Res), AA = -1 * 3 / (-3 / 4)
287 . . . . . . . . . . Rewrite_Set "polyeq_simplify",
288 ([7,4,2], Res), AA = -3 / (-3 / 4)
289 . . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
290 ([7,4,3], Res), AA = 4
291 . . . . . . . . . . Or_to_List ,
292 ([7,4,4], Res), [AA = 4]
293 . . . . . . . . . . Check_elementwise "Assumptions",
294 ([7,4,5], Res), [AA = 4]
295 . . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
296 ([7,4], Res), [AA = 4]
297 . . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
299 . . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
300 ([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
301 . . . . . . . . . . Substitute ["z = -1 / 4"],
302 ([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)
303 . . . . . . . . . . Rewrite_Set "norm_Rational",
304 ([9], Res), 3 = -3 * BB / 4
305 . . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
306 ([10], Pbl), solve (3 = -3 * BB / 4, BB)
307 . . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
308 ([10,1], Frm), 3 = -3 * BB / 4
309 . . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
310 ([10,1], Res), 3 - -3 * BB / 4 = 0
311 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),
312 ([10,2], Res), 3 / 1 + 3 / 4 * BB = 0
313 . . . . . . . . . . Rewrite_Set "polyeq_simplify",
314 ([10,3], Res), 3 + 3 / 4 * BB = 0
315 . . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
316 ([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)
317 . . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
318 ([10,4,1], Frm), 3 + 3 / 4 * BB = 0
319 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),
320 ([10,4,1], Res), BB = -1 * 3 / (3 / 4)
321 . . . . . . . . . . Rewrite_Set "polyeq_simplify",
322 ([10,4,2], Res), BB = -3 / (3 / 4)
323 . . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
324 ([10,4,3], Res), BB = -4
325 . . . . . . . . . . Or_to_List ,
326 ([10,4,4], Res), [BB = -4]
327 . . . . . . . . . . Check_elementwise "Assumptions",
328 ([10,4,5], Res), [BB = -4]
329 . . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
330 ([10,4], Res), [BB = -4]
331 . . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
332 ([10], Res), [BB = -4]
333 . . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",
334 ([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)
335 . . . . . . . . . . Substitute ["AA = 4","BB = -4"],
336 ([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
337 . . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],
338 ([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)]
342 "----------- autoCalculate for met_partial_fraction -----";
343 "----------- autoCalculate for met_partial_fraction -----";
344 "----------- autoCalculate for met_partial_fraction -----";
347 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
348 "solveFor z", "decomposedFunction p_p"];
349 val (dI', pI', mI') =
350 ("Partial_Fractions",
351 ["partial_fraction", "rational", "simplification"],
352 ["simplification","of_rationals","to_partial_fraction"]);
353 CalcTree [(fmz, (dI' ,pI' ,mI'))];
356 autoCalculate 1 CompleteCalc;
358 val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
359 if p = ip andalso ip = ([], Res) then ()
360 else error "autoCalculate for met_partial_fraction changed: final pos'";
362 val (Form f, tac, asms) = pt_extract (pt, p);
363 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
365 "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^
366 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
367 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
368 then case tac of NONE => ()
369 | _ => error "me for met_partial_fraction changed: final result 1"
370 else error "me for met_partial_fraction changed: final result 2"
374 (([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
375 (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
376 (([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
377 (([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
378 (([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
379 (([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
380 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
381 (([2,2], Res), z = 1 / 2 | z = -1 / 4),
382 (([2,3], Res), [z = 1 / 2, z = -1 / 4]),
383 (([2,4], Res), [z = 1 / 2, z = -1 / 4]),
384 (([2], Res), [z = 1 / 2, z = -1 / 4]),
385 (([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
386 (([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
387 (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
388 (([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
389 (([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
390 (([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
391 (([6], Res), 3 = 3 * A / 4),
392 (([7], Pbl), solve (3 = 3 * A / 4, A)),
393 (([7,1], Frm), 3 = 3 * A / 4),
394 (([7,1], Res), 3 - 3 * A / 4 = 0),
395 (([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
396 (([7,3], Res), 3 + -3 / 4 * A = 0),
397 (([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
398 (([7,4,1], Frm), 3 + -3 / 4 * A = 0),
399 (([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
400 (([7,4,2], Res), A = -3 / (-3 / 4)),
401 (([7,4,3], Res), A = 4),
402 (([7,4,4], Res), [A = 4]),
403 (([7,4,5], Res), [A = 4]),
404 (([7,4], Res), [A = 4]),
405 (([7], Res), [A = 4]),
406 (([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
407 (([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
408 (([9], Res), 3 = -3 * B / 4),
409 (([10], Pbl), solve (3 = -3 * B / 4, B)),
410 (([10,1], Frm), 3 = -3 * B / 4),
411 (([10,1], Res), 3 - -3 * B / 4 = 0),
412 (([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
413 (([10,3], Res), 3 + 3 / 4 * B = 0),
414 (([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
415 (([10,4,1], Frm), 3 + 3 / 4 * B = 0),
416 (([10,4,1], Res), B = -1 * 3 / (3 / 4)),
417 (([10,4,2], Res), B = -3 / (3 / 4)),
418 (([10,4,3], Res), B = -4),
419 (([10,4,4], Res), [B = -4]),
420 (([10,4,5], Res), [B = -4]),
421 (([10,4], Res), [B = -4]),
422 (([10], Res), [B = -4]),
423 (([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
424 (([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
425 (([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
427 "----------- progr.vers.2: check erls for multiply_ansatz";
428 "----------- progr.vers.2: check erls for multiply_ansatz";
429 "----------- progr.vers.2: check erls for multiply_ansatz";
430 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
431 val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
432 val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
433 term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
435 val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
436 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
437 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
439 val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
440 if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
441 else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
443 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
444 val xxx = append_rls "multiply_ansatz_erls" norm_Rational
445 [Calc ("HOL.eq",eval_equal "#equal_")];
447 val multiply_ansatz = prep_rls @{theory} (
448 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
450 srls = Erls, calc = [], errpatts = [],
452 [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
454 scr = EmptyScr}:rls);
456 rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
457 rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)
459 "----------- progr.vers.2: improve program --------------";
460 "----------- progr.vers.2: improve program --------------";
461 "----------- progr.vers.2: improve program --------------";
462 (*WN120318 stopped due to much effort with the test above*)
463 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
464 " (let f_f = Take f_f; " ^
465 " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
466 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
467 " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
468 " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
469 " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
470 " (L_L::bool list) = (SubProblem (PolyEqX, " ^
471 " [abcFormula, degree_2, polynomial, univariate, equation], " ^
472 " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
473 " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
474 " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
475 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
476 " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
477 (*this has been tested below by rewrite_set_
478 " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
479 " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
480 " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
481 NEXT try to outcomment the very next line..*)
482 " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
483 " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
484 " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
485 " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
486 " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
487 " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
488 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
489 " (sol_a::bool list) = " ^
490 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
491 " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
492 " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
493 " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
494 " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
495 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
496 " (sol_b::bool list) = " ^
497 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
498 " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
499 " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
500 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
501 " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
502 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)