65 \<close> ML \<open> |
65 \<close> ML \<open> |
66 \<close> ML \<open> |
66 \<close> ML \<open> |
67 "~~~~~ fun xxx , args:"; val () = (); |
67 "~~~~~ fun xxx , args:"; val () = (); |
68 \<close> |
68 \<close> |
69 |
69 |
70 section \<open>===================================================================================\<close> |
70 section \<open>================= "Knowledge/partial_fractions.sml" ============================\<close> |
71 ML \<open> |
71 ML \<open> |
72 "~~~~~ fun xxx , args:"; val () = (); |
72 "~~~~~ fun xxx , args:"; val () = (); |
73 \<close> ML \<open> |
73 \<close> ML \<open> |
|
74 (* Title: partial fraction decomposition |
|
75 Author: Jan Rocnik |
|
76 (c) due to copyright terms |
|
77 *) |
|
78 |
|
79 "--------------------------------------------------------"; |
|
80 "table of contents --------------------------------------"; |
|
81 "--------------------------------------------------------"; |
|
82 "----------- why helpless here ? ------------------------"; |
|
83 "----------- why not nxt = Model_Problem here ? ---------"; |
|
84 "----------- fun factors_from_solution ------------------"; |
|
85 "----------- Logic.unvarify_global ----------------------"; |
|
86 "----------- eval_drop_questionmarks --------------------"; |
|
87 "----------- = me for met_partial_fraction --------------"; |
|
88 "----------- autoCalculate for met_partial_fraction -----"; |
|
89 "----------- progr.vers.2: check erls for multiply_ansatz"; |
|
90 "----------- progr.vers.2: improve program --------------"; |
|
91 "--------------------------------------------------------"; |
|
92 "--------------------------------------------------------"; |
|
93 "--------------------------------------------------------"; |
|
94 |
|
95 |
|
96 "----------- why helpless here ? ------------------------"; |
|
97 "----------- why helpless here ? ------------------------"; |
|
98 "----------- why helpless here ? ------------------------"; |
|
99 \<close> ML \<open> |
|
100 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", |
|
101 "stepResponse (x[n::real]::bool)"]; |
|
102 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], |
|
103 ["SignalProcessing","Z_Transform","Inverse"]); |
|
104 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; |
|
105 \<close> ML \<open> |
|
106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given"; |
|
107 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find"; |
|
108 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory"; |
|
109 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem"; |
|
110 \<close> ML \<open> |
|
111 (*CURRENT*)(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse"])*) |
|
112 \<close> ML \<open> |
|
113 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method"; |
|
114 (*CURRENT*)(*ERROR in creating the environment from formal args. of partial_function "HOL.eq" |
|
115 and the actual args., ie. items of the guard of "["SignalProcessing","Z_Transform","Inverse"]" by "assoc_by_type": |
|
116 formal arg "TYPE('a)" doesn't mach an actual arg. |
|
117 with: |
|
118 3 formal args: ["TYPE('a)","X_eq","z"] |
|
119 2 actual args: ["X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))","x [n]"]*) |
|
120 \<close> ML \<open> |
|
121 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))"; |
|
122 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)))"; |
|
123 \<close> ML \<open> |
|
124 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); |
|
125 val ("ok", (_, _, ptp)) = locatetac tac (pt,p) |
|
126 val (pt, p) = ptp; |
|
127 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
|
128 (p, ((pt, e_pos'),[])); |
|
129 val pIopt = get_pblID (pt,ip); |
|
130 ip = ([],Res); "false"; |
|
131 tacis; " = []"; |
|
132 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*) |
|
133 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false"; |
|
134 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'" |
|
135 THIS MEANS: replace no_meth by [no_meth] in Script.*) |
|
136 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *) |
|
137 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*) |
|
138 |
|
139 \<close> ML \<open> |
|
140 "----------- why not nxt = Model_Problem here ? ---------"; |
|
141 "----------- why not nxt = Model_Problem here ? ---------"; |
|
142 "----------- why not nxt = Model_Problem here ? ---------"; |
|
143 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; |
|
144 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); |
|
145 val ("ok", (_, _, ptp)) = locatetac tac (pt,p); |
|
146 val (pt, p) = ptp; |
|
147 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
|
148 (p, ((pt, e_pos'),[])); |
|
149 val pIopt = get_pblID (pt,ip); |
|
150 ip = ([],Res); " = false"; |
|
151 tacis; " = []"; |
|
152 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*); |
|
153 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false"; |
|
154 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into |
|
155 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD). |
|
156 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form. |
|
157 See TODO.txt |
|
158 *) |
|
159 |
|
160 \<close> ML \<open> |
|
161 "----------- fun factors_from_solution ------------------"; |
|
162 "----------- fun factors_from_solution ------------------"; |
|
163 "----------- fun factors_from_solution ------------------"; |
|
164 val ctxt = Proof_Context.init_global @{theory Isac}; |
|
165 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]"; |
|
166 val SOME (_, t') = eval_factors_from_solution "" 0 t thy; |
|
167 if term2str t' = |
|
168 "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)" |
|
169 then () else error "factors_from_solution broken"; |
|
170 |
|
171 \<close> ML \<open> |
|
172 "----------- Logic.unvarify_global ----------------------"; |
|
173 "----------- Logic.unvarify_global ----------------------"; |
|
174 "----------- Logic.unvarify_global ----------------------"; |
|
175 val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global |
|
176 val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global |
|
177 |
|
178 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the; |
|
179 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the; |
|
180 |
|
181 val test = HOLogic.mk_binop "Groups.plus_class.plus" |
|
182 (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1), |
|
183 HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2)); |
|
184 |
|
185 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then () |
|
186 else error "HOLogic.mk_binop broken ?"; |
|
187 |
|
188 (* Logic.unvarify_global test |
|
189 ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z" |
|
190 thus we need another fun var2free in termC.sml*) |
|
191 |
|
192 \<close> ML \<open> |
|
193 "----------- = me for met_partial_fraction --------------"; |
|
194 "----------- = me for met_partial_fraction --------------"; |
|
195 "----------- = me for met_partial_fraction --------------"; |
|
196 val fmz = |
|
197 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", |
|
198 "solveFor z", "decomposedFunction p_p"]; |
|
199 val (dI',pI',mI') = |
|
200 ("Partial_Fractions", |
|
201 ["partial_fraction", "rational", "simplification"], |
|
202 ["simplification","of_rationals","to_partial_fraction"]); |
|
203 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = |
|
204 CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*) |
|
205 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*) |
|
206 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*) |
|
207 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*) |
|
208 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*) |
|
209 (*05*) |
|
210 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*) |
|
211 (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*) |
|
212 (*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*) |
|
213 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*) |
|
214 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*) |
|
215 (*10*) |
|
216 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*) |
|
217 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*) |
|
218 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*) |
|
219 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*) |
|
220 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*) |
|
221 (*[2], Pbl*)(*15*) |
|
222 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*) |
|
223 (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*) |
|
224 (*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*) |
|
225 (*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*) |
|
226 (*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*) |
|
227 (*20*) |
|
228 (*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*) |
|
229 (*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*) |
|
230 (*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*) |
|
231 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*) |
|
232 (*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*) |
|
233 (*25*) |
|
234 (*[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)")*) |
|
235 (*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*) |
|
236 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*) |
|
237 (*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*) |
|
238 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*) |
|
239 (*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*) |
|
240 (*30+1*) |
|
241 (*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*) |
|
242 (*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*) |
|
243 (*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*) |
|
244 (*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*) |
|
245 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*) |
|
246 (*35*) |
|
247 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*) |
|
248 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*) |
|
249 (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*) |
|
250 (*[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)"))*) |
|
251 (*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*) |
|
252 (*40*) |
|
253 (*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*) |
|
254 (*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*) |
|
255 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) |
|
256 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*) |
|
257 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*) |
|
258 (*45*) |
|
259 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
260 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
261 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
262 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
263 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
264 (*50*) |
|
265 (*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
266 (*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
267 (*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
268 (*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
269 (*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
270 (*55*) |
|
271 (*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
272 (*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
273 (*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
274 (*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
275 (*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
276 (*60*) |
|
277 (*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
278 (*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
279 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
280 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
281 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
282 (*65*) |
|
283 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
284 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
285 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
286 (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
287 (*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
288 (*70*) |
|
289 (*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
290 (*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
291 (*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
292 (*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
293 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
294 (*75*) |
|
295 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
296 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
297 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
298 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
299 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
300 (*80*) |
|
301 (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
302 (*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
303 (*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
304 (*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
305 (*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
306 (*85*) |
|
307 (*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) |
|
308 (*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*) |
|
309 (*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*) |
|
310 (*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*) |
|
311 |
|
312 (*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*) |
|
313 (*90*) |
|
314 (*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*) |
|
315 (*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*) |
|
316 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) |
|
317 |
|
318 case nxt of |
|
319 (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then () |
|
320 else error "= me .. met_partial_fraction f changed" |
|
321 | _ => error "= me .. met_partial_fraction nxt changed"; |
|
322 |
|
323 show_pt_tac pt; (*[ |
|
324 ([], Frm), Problem |
|
325 (''Partial_Fractions'', |
|
326 ??.\<^const>String.char.Char ''partial_fraction'' ''rational'' |
|
327 ''simplification'') |
|
328 . . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"], |
|
329 ([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) |
|
330 . . . . . . . . . . Rewrite_Set "norm_Rational", |
|
331 ([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2) |
|
332 . . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]), |
|
333 ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z) |
|
334 . . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"], |
|
335 ([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0 |
|
336 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"), |
|
337 ([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or> |
|
338 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
|
339 . . . . . . . . . . Rewrite_Set "polyeq_simplify", |
|
340 ([2,2], Res), z = 1 / 2 \<or> z = -1 / 4 |
|
341 . . . . . . . . . . Or_to_List , |
|
342 ([2,3], Res), [z = 1 / 2, z = -1 / 4] |
|
343 . . . . . . . . . . Check_elementwise "Assumptions", |
|
344 ([2,4], Res), [z = 1 / 2, z = -1 / 4] |
|
345 . . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"], |
|
346 ([2], Res), [z = 1 / 2, z = -1 / 4] |
|
347 . . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))", |
|
348 ([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) |
|
349 . . . . . . . . . . Rewrite_Set "ansatz_rls", |
|
350 ([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4) |
|
351 . . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)", |
|
352 ([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4) |
|
353 . . . . . . . . . . Rewrite_Set "equival_trans", |
|
354 ([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2) |
|
355 . . . . . . . . . . Substitute ["z = 1 / 2"], |
|
356 ([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2) |
|
357 . . . . . . . . . . Rewrite_Set "norm_Rational", |
|
358 ([6], Res), 3 = 3 * AA / 4 |
|
359 . . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]), |
|
360 ([7], Pbl), solve (3 = 3 * AA / 4, AA) |
|
361 . . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"], |
|
362 ([7,1], Frm), 3 = 3 * AA / 4 |
|
363 . . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"), |
|
364 ([7,1], Res), 3 - 3 * AA / 4 = 0 |
|
365 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"), |
|
366 ([7,2], Res), 3 / 1 + -3 / 4 * AA = 0 |
|
367 . . . . . . . . . . Rewrite_Set "polyeq_simplify", |
|
368 ([7,3], Res), 3 + -3 / 4 * AA = 0 |
|
369 . . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]), |
|
370 ([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA) |
|
371 . . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"], |
|
372 ([7,4,1], Frm), 3 + -3 / 4 * AA = 0 |
|
373 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"), |
|
374 ([7,4,1], Res), AA = -1 * 3 / (-3 / 4) |
|
375 . . . . . . . . . . Rewrite_Set "polyeq_simplify", |
|
376 ([7,4,2], Res), AA = -3 / (-3 / 4) |
|
377 . . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized", |
|
378 ([7,4,3], Res), AA = 4 |
|
379 . . . . . . . . . . Or_to_List , |
|
380 ([7,4,4], Res), [AA = 4] |
|
381 . . . . . . . . . . Check_elementwise "Assumptions", |
|
382 ([7,4,5], Res), [AA = 4] |
|
383 . . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"], |
|
384 ([7,4], Res), [AA = 4] |
|
385 . . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"], |
|
386 ([7], Res), [AA = 4] |
|
387 . . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)", |
|
388 ([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2) |
|
389 . . . . . . . . . . Substitute ["z = -1 / 4"], |
|
390 ([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2) |
|
391 . . . . . . . . . . Rewrite_Set "norm_Rational", |
|
392 ([9], Res), 3 = -3 * BB / 4 |
|
393 . . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]), |
|
394 ([10], Pbl), solve (3 = -3 * BB / 4, BB) |
|
395 . . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"], |
|
396 ([10,1], Frm), 3 = -3 * BB / 4 |
|
397 . . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"), |
|
398 ([10,1], Res), 3 - -3 * BB / 4 = 0 |
|
399 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"), |
|
400 ([10,2], Res), 3 / 1 + 3 / 4 * BB = 0 |
|
401 . . . . . . . . . . Rewrite_Set "polyeq_simplify", |
|
402 ([10,3], Res), 3 + 3 / 4 * BB = 0 |
|
403 . . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]), |
|
404 ([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB) |
|
405 . . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"], |
|
406 ([10,4,1], Frm), 3 + 3 / 4 * BB = 0 |
|
407 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"), |
|
408 ([10,4,1], Res), BB = -1 * 3 / (3 / 4) |
|
409 . . . . . . . . . . Rewrite_Set "polyeq_simplify", |
|
410 ([10,4,2], Res), BB = -3 / (3 / 4) |
|
411 . . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized", |
|
412 ([10,4,3], Res), BB = -4 |
|
413 . . . . . . . . . . Or_to_List , |
|
414 ([10,4,4], Res), [BB = -4] |
|
415 . . . . . . . . . . Check_elementwise "Assumptions", |
|
416 ([10,4,5], Res), [BB = -4] |
|
417 . . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"], |
|
418 ([10,4], Res), [BB = -4] |
|
419 . . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"], |
|
420 ([10], Res), [BB = -4] |
|
421 . . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)", |
|
422 ([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4) |
|
423 . . . . . . . . . . Substitute ["AA = 4","BB = -4"], |
|
424 ([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4) |
|
425 . . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"], |
|
426 ([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)] |
|
427 val it = (): unit |
|
428 *) |
|
429 |
|
430 "----------- autoCalculate for met_partial_fraction -----"; |
|
431 "----------- autoCalculate for met_partial_fraction -----"; |
|
432 "----------- autoCalculate for met_partial_fraction -----"; |
|
433 reset_states (); |
|
434 val fmz = |
|
435 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", |
|
436 "solveFor z", "decomposedFunction p_p"]; |
|
437 val (dI', pI', mI') = |
|
438 ("Partial_Fractions", |
|
439 ["partial_fraction", "rational", "simplification"], |
|
440 ["simplification","of_rationals","to_partial_fraction"]); |
|
441 CalcTree [(fmz, (dI' ,pI' ,mI'))]; |
|
442 Iterator 1; |
|
443 moveActiveRoot 1; |
|
444 autoCalculate 1 CompleteCalc; |
|
445 |
|
446 val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1; |
|
447 if p = ip andalso ip = ([], Res) then () |
|
448 else error "autoCalculate for met_partial_fraction changed: final pos'"; |
|
449 |
|
450 val (Form f, tac, asms) = pt_extract (pt, p); |
|
451 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso |
|
452 terms2str' asms = |
|
453 "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^ |
|
454 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^ |
|
455 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]" |
|
456 then case tac of NONE => () |
|
457 | _ => error "me for met_partial_fraction changed: final result 1" |
|
458 else error "me for met_partial_fraction changed: final result 2" |
|
459 |
|
460 show_pt pt; |
|
461 (*[ |
|
462 (([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])), |
|
463 (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))), |
|
464 (([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)), |
|
465 (([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)), |
|
466 (([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0), |
|
467 (([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) | |
|
468 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)), |
|
469 (([2,2], Res), z = 1 / 2 | z = -1 / 4), |
|
470 (([2,3], Res), [z = 1 / 2, z = -1 / 4]), |
|
471 (([2,4], Res), [z = 1 / 2, z = -1 / 4]), |
|
472 (([2], Res), [z = 1 / 2, z = -1 / 4]), |
|
473 (([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))), |
|
474 (([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)), |
|
475 (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)), |
|
476 (([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)), |
|
477 (([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)), |
|
478 (([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)), |
|
479 (([6], Res), 3 = 3 * A / 4), |
|
480 (([7], Pbl), solve (3 = 3 * A / 4, A)), |
|
481 (([7,1], Frm), 3 = 3 * A / 4), |
|
482 (([7,1], Res), 3 - 3 * A / 4 = 0), |
|
483 (([7,2], Res), 3 / 1 + -3 / 4 * A = 0), |
|
484 (([7,3], Res), 3 + -3 / 4 * A = 0), |
|
485 (([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)), |
|
486 (([7,4,1], Frm), 3 + -3 / 4 * A = 0), |
|
487 (([7,4,1], Res), A = -1 * 3 / (-3 / 4)), |
|
488 (([7,4,2], Res), A = -3 / (-3 / 4)), |
|
489 (([7,4,3], Res), A = 4), |
|
490 (([7,4,4], Res), [A = 4]), |
|
491 (([7,4,5], Res), [A = 4]), |
|
492 (([7,4], Res), [A = 4]), |
|
493 (([7], Res), [A = 4]), |
|
494 (([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)), |
|
495 (([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)), |
|
496 (([9], Res), 3 = -3 * B / 4), |
|
497 (([10], Pbl), solve (3 = -3 * B / 4, B)), |
|
498 (([10,1], Frm), 3 = -3 * B / 4), |
|
499 (([10,1], Res), 3 - -3 * B / 4 = 0), |
|
500 (([10,2], Res), 3 / 1 + 3 / 4 * B = 0), |
|
501 (([10,3], Res), 3 + 3 / 4 * B = 0), |
|
502 (([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)), |
|
503 (([10,4,1], Frm), 3 + 3 / 4 * B = 0), |
|
504 (([10,4,1], Res), B = -1 * 3 / (3 / 4)), |
|
505 (([10,4,2], Res), B = -3 / (3 / 4)), |
|
506 (([10,4,3], Res), B = -4), |
|
507 (([10,4,4], Res), [B = -4]), |
|
508 (([10,4,5], Res), [B = -4]), |
|
509 (([10,4], Res), [B = -4]), |
|
510 (([10], Res), [B = -4]), |
|
511 (([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)), |
|
512 (([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)), |
|
513 (([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *) |
|
514 |
|
515 \<close> ML \<open> |
|
516 "----------- progr.vers.2: check erls for multiply_ansatz"; |
|
517 "----------- progr.vers.2: check erls for multiply_ansatz"; |
|
518 "----------- progr.vers.2: check erls for multiply_ansatz"; |
|
519 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*) |
|
520 val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))"; |
|
521 val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t; |
|
522 term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)"; |
|
523 |
|
524 val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*) |
|
525 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^ |
|
526 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*) |
|
527 |
|
528 val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; |
|
529 if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then () |
|
530 else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; |
|
531 |
|
532 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*) |
|
533 val xxx = append_rls "multiply_ansatz_erls" norm_Rational |
|
534 [Calc ("HOL.eq",eval_equal "#equal_")]; |
|
535 |
|
536 val multiply_ansatz = prep_rls @{theory} ( |
|
537 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
|
538 erls = xxx, |
|
539 srls = Erls, calc = [], errpatts = [], |
|
540 rules = |
|
541 [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order}) |
|
542 ], |
|
543 scr = EmptyScr}:rls); |
|
544 |
|
545 rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*) |
|
546 rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*) |
|
547 |
|
548 "----------- progr.vers.2: improve program --------------"; |
|
549 "----------- progr.vers.2: improve program --------------"; |
|
550 "----------- progr.vers.2: improve program --------------"; |
|
551 (*WN120318 stopped due to much effort with the test above*) |
|
552 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*) |
|
553 " (let f_f = Take f_f; " ^ |
|
554 " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*) |
|
555 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*) |
|
556 " (numer::real) = get_numerator f_f; " ^(*numer: 24*) |
|
557 " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*) |
|
558 " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*) |
|
559 " (L_L::bool list) = (SubProblem (PolyEqX, " ^ |
|
560 " [abcFormula, degree_2, polynomial, univariate, equation], " ^ |
|
561 " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*) |
|
562 " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*) |
|
563 " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *) |
|
564 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*) |
|
565 " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*) |
|
566 (*this has been tested below by rewrite_set_ |
|
567 " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**) |
|
568 " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**) |
|
569 " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*) |
|
570 NEXT try to outcomment the very next line..*) |
|
571 " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*) |
|
572 " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
573 " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*) |
|
574 " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*) |
|
575 " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
576 " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*) |
|
577 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*) |
|
578 " (sol_a::bool list) = " ^ |
|
579 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^ |
|
580 " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*) |
|
581 " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*) |
|
582 " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*) |
|
583 " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *) |
|
584 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *) |
|
585 " (sol_b::bool list) = " ^ |
|
586 " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^ |
|
587 " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*) |
|
588 " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*) |
|
589 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*) |
|
590 " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*) |
|
591 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) |
|
592 " in pbz)" |
|
593 |
|
594 \<close> ML \<open> |
|
595 \<close> ML \<open> |
|
596 "~~~~~ fun xxx , args:"; val () = (); |
|
597 \<close> |
|
598 |
|
599 section \<open>=============== "Knowledge/biegelinie-3.sml" ===============================\<close> |
|
600 ML \<open> |
|
601 "~~~~~ fun xxx , args:"; val () = (); |
|
602 \<close> ML \<open> |
|
603 (* "Knowledge/biegelinie-3.sml" |
|
604 author: Walther Neuper 190515 |
|
605 (c) due to copyright terms |
|
606 *) |
|
607 "table of contents -----------------------------------------------"; |
|
608 "-----------------------------------------------------------------"; |
|
609 "----------- see biegelinie-1.sml---------------------------------"; |
|
610 (* problems with generalised handling of meths which extend the model of a probl |
|
611 since 98298342fb6d: wait for review of whole model-specify phase *) |
|
612 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----"; |
|
613 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---"; |
|
614 "-----------------------------------------------------------------"; |
|
615 "-----------------------------------------------------------------"; |
|
616 "-----------------------------------------------------------------"; |
|
617 |
|
618 \<close> ML \<open> |
|
619 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----"; |
|
620 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----"; |
|
621 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----"; |
|
622 "----- Bsp 7.70 with me"; |
|
623 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
|
624 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", |
|
625 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", |
|
626 "AbleitungBiegelinie dy"]; |
|
627 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], |
|
628 ["IntegrierenUndKonstanteBestimmen2"]); |
|
629 val p = e_pos'; val c = []; |
|
630 (*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*) |
|
631 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*) |
|
632 |
|
633 (*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p); |
|
634 (*+*)writeln (oris2str oris); (*[ |
|
635 (1, ["1"], #Given,Traegerlaenge, ["L"]), |
|
636 (2, ["1"], #Given,Streckenlast, ["q_0"]), |
|
637 (3, ["1"], #Find,Biegelinie, ["y"]), |
|
638 (4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]), |
|
639 (5, ["1"], #undef,FunktionsVariable, ["x"]), |
|
640 (6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]), |
|
641 (7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*) |
|
642 (*+*)itms2str_ @{context} probl = "[]"; |
|
643 (*+*)itms2str_ @{context} meth = "[]"; |
|
644 (*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*) |
|
645 |
|
646 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*) |
|
647 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*) |
|
648 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*) |
|
649 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*) |
|
650 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*) |
|
651 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*) |
|
652 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*) |
|
653 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*) |
|
654 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*) |
|
655 (*----------- 10 -----------*) |
|
656 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*) |
|
657 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*) |
|
658 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*) |
|
659 |
|
660 (*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*) |
|
661 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*) |
|
662 (*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script" |
|
663 and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type": |
|
664 formal arg. "b" type-matches with several...actual args. "["dy","y"]" |
|
665 selected "dy" |
|
666 with |
|
667 formals: ["l","q","v","b","s","vs","id_abl"] |
|
668 actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*) |
|
669 |
|
670 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt); |
|
671 val (pt''', p''') = |
|
672 (*locatetac is here for testing by me; step would suffice in me*) |
|
673 case locatetac tac (pt,p) of |
|
674 ("ok", (_, _, ptp)) => ptp |
|
675 ; |
|
676 (*+*)p = ([], Met); |
|
677 (*+*)p''' = ([1], Pbl); |
|
678 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p'''); |
|
679 (*+*)(*MISSING after locatetac:*) |
|
680 (*+*)writeln (oris2str oris); (*[ |
|
681 (1, ["1"], #Given,Streckenlast, ["q_0"]), |
|
682 (2, ["1"], #Given,FunktionsVariable, ["x"]), |
|
683 (3, ["1"], #Find,Funktionen, ["funs'''"])] |
|
684 MISSING: |
|
685 Biegelinie |
|
686 AbleitungBiegelinie |
|
687 *) |
|
688 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); |
|
689 val (mI, m) = Solve.mk_tac'_ tac; |
|
690 val Appl m = (*case*) Applicable.applicable_in p pt m (*of*); |
|
691 (*if*) member op = Solve.specsteps mI = false; (*else*) |
|
692 |
|
693 loc_solve_ (mI,m) ptp; |
|
694 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp); |
|
695 |
|
696 Solve.solve m (pt, pos); |
|
697 "~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) = |
|
698 (m, (pt, pos)); |
|
699 val {srls, ...} = Specify.get_met mI; |
|
700 val itms = case get_obj I pt p of |
|
701 PblObj {meth=itms, ...} => itms |
|
702 | _ => error "solve Apply_Method: uncovered case get_obj" |
|
703 val thy' = get_obj g_domID pt p; |
|
704 val thy = Celem.assoc_thy thy'; |
|
705 val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of |
|
706 (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc) |
|
707 | _ => error "solve Apply_Method: uncovered case init_scrstate" |
|
708 val ini = Lucin.init_form thy sc env; |
|
709 val p = lev_dn p; |
|
710 val NONE = (*case*) ini (*of*); |
|
711 val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); |
|
712 val d = Rule.e_rls (*FIXME: get simplifier from domID*); |
|
713 val Steps (_, ss as (_, _, pt', p', c') :: _) = |
|
714 (*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*); |
|
715 |
|
716 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p'); |
|
717 (*+*)(*MISSING after locate_gen:*) |
|
718 (*+*)writeln (oris2str oris); (*[ |
|
719 (1, ["1"], #Given,Streckenlast, ["q_0"]), |
|
720 (2, ["1"], #Given,FunktionsVariable, ["x"]), |
|
721 (3, ["1"], #Find,Funktionen, ["funs'''"])] |
|
722 MISSING: |
|
723 Biegelinie |
|
724 AbleitungBiegelinie |
|
725 *) |
|
726 "~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p), |
|
727 (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) = |
|
728 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); |
|
729 val thy = Celem.assoc_thy thy'; |
|
730 (*if*) l = [] orelse ( |
|
731 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*) |
|
732 (assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc)); |
|
733 |
|
734 "~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = |
|
735 ((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc)); |
|
736 (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*); |
|
737 |
|
738 "~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) = |
|
739 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e); |
|
740 val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*); |
|
741 (*+*)writeln (term2str stac); (*SubProblem |
|
742 (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''], |
|
743 [''Biegelinien'', ''ausBelastung'']) |
|
744 [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *) |
|
745 val p' = |
|
746 case p_ of Frm => p |
|
747 | Res => lev_on p |
|
748 | _ => error ("assy: call by " ^ pos'2str (p,p_)); |
|
749 val Ass (m,v') = (*case*) assod pt d m stac (*of*); |
|
750 |
|
751 "~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)), |
|
752 (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $ |
|
753 dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) = |
|
754 (pt, d, m, stac); |
|
755 val dI = HOLogic.dest_string dI'; |
|
756 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt); |
|
757 val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string; |
|
758 val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string; |
|
759 val ags = TermC.isalist2list ags'; |
|
760 (*if*) mI = ["no_met"] = false; (*else*) |
|
761 (* val (pI, pors, mI) = *) |
|
762 (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags) |
|
763 handle ERROR "actual args do not match formal args" |
|
764 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI); |
|
765 "~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags); |
|
766 (*+*)pbt; |
|
767 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_) |
|
768 val pbt' = filter_out is_copy_named pbt |
|
769 val cy = filter is_copy_named pbt |
|
770 val oris' = matc thy pbt' ags [] |
|
771 val cy' = map (cpy_nam pbt' oris') cy |
|
772 val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *) |
|
773 |
|
774 (*+*)val c = []; |
|
775 (*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*) |
|
776 |
|
777 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*) |
|
778 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*) |
|
779 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*) |
|
780 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*) |
|
781 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*) |
|
782 (*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*) |
|
783 (*----------- 20 -----------*) |
|
784 (*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*) |
|
785 (*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*) |
|
786 ERROR itms2args: 'Biegelinie' not in itms*) |
|
787 |
|
788 (*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _) |
|
789 [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl] |
|
790 ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*) |
|
791 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p'''''); |
|
792 (*+*)if oris2str oris = |
|
793 (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]" |
|
794 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris"; |
|
795 writeln (oris2str oris); (*[ |
|
796 (1, ["1"], #Given,Streckenlast, ["q_0"]), |
|
797 (2, ["1"], #Given,FunktionsVariable, ["x"]), |
|
798 (3, ["1"], #Find,Funktionen, ["funs'''"])]*) |
|
799 (*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]" |
|
800 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl"; |
|
801 writeln (itms2str_ @{context} probl); (*[ |
|
802 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), |
|
803 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), |
|
804 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*) |
|
805 (*+*)if itms2str_ @{context} meth = "[]" |
|
806 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth"; |
|
807 writeln (itms2str_ @{context} meth); (*[]*) |
|
808 |
|
809 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt'''''); |
|
810 (* val (pt, p) = *) |
|
811 (*locatetac is here for testing by me; step would suffice in me*) |
|
812 case locatetac tac (pt,p) of |
|
813 ("ok", (_, _, ptp)) => ptp |
|
814 ; |
|
815 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); |
|
816 val (mI, m) = Solve.mk_tac'_ tac; |
|
817 val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); |
|
818 (*if*) member op = Solve.specsteps mI = true; (*then*) |
|
819 |
|
820 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*) |
|
821 "~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp); |
|
822 (* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt; |
|
823 |
|
824 "~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt); |
|
825 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of |
|
826 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} => |
|
827 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) |
|
828 val {ppc, pre, prls,...} = Specify.get_met mID |
|
829 val thy = Celem.assoc_thy dI |
|
830 val dI'' = if dI = Rule.e_domID then dI' else dI |
|
831 val pI'' = if pI = Celem.e_pblID then pI' else pI |
|
832 ; |
|
833 (*+*)writeln (oris2str oris); (*[ |
|
834 (1, ["1"], #Given,Streckenlast, ["q_0"]), |
|
835 (2, ["1"], #Given,FunktionsVariable, ["x"]), |
|
836 (3, ["1"], #Find,Funktionen, ["funs'''"])]*) |
|
837 (*+*)writeln (pats2str' ppc); |
|
838 (*["(#Given, (Streckenlast, q__q)) |
|
839 ","(#Given, (FunktionsVariable, v_v)) |
|
840 ","(#Given, (Biegelinie, id_fun)) |
|
841 ","(#Given, (AbleitungBiegelinie, id_abl)) |
|
842 ","(#Find, (Funktionen, fun_s))"]*) |
|
843 (*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI)); |
|
844 (*["(#Given, (Streckenlast, q_q)) |
|
845 ","(#Given, (FunktionsVariable, v_v)) |
|
846 ","(#Find, (Funktionen, funs'''))"]*) |
|
847 val oris = Specify.add_field' thy ppc oris |
|
848 val met = if met = [] then pbl else met |
|
849 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris |
|
850 ; |
|
851 (*+*)writeln (itms2str_ @{context} itms); (*[ |
|
852 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), |
|
853 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), |
|
854 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *) |
|
855 |
|
856 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*) |
|
857 val itms = |
|
858 if mI' = ["Biegelinien", "ausBelastung"] |
|
859 then itms @ |
|
860 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])), |
|
861 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]), |
|
862 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])), |
|
863 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))), |
|
864 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])), |
|
865 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]), |
|
866 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])), |
|
867 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))] |
|
868 else itms |
|
869 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*) |
|
870 |
|
871 val itms' = itms @ |
|
872 [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"}, |
|
873 [@{term "y::real \<Rightarrow> real"}]), |
|
874 (@{term "id_fun::real \<Rightarrow> real"}, |
|
875 [@{term "y::real \<Rightarrow> real"}] ))), |
|
876 (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"}, |
|
877 [@{term "dy::real \<Rightarrow> real"}]), |
|
878 (@{term "id_abl::real \<Rightarrow> real"}, |
|
879 [@{term "dy::real \<Rightarrow> real"}] )))] |
|
880 val itms'' = itms @ |
|
881 [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])), |
|
882 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]), |
|
883 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])), |
|
884 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))), |
|
885 (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])), |
|
886 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]), |
|
887 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])), |
|
888 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))] |
|
889 ; |
|
890 if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN"; |
|
891 (*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*) |
|
892 |
|
893 val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; |
|
894 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
895 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
896 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
897 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
898 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
899 (*----------- 30 -----------*) |
|
900 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
901 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
902 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
903 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
904 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
905 (*----------- 40 -----------*) |
|
906 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
907 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
908 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
909 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
910 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
911 (*----------- 50 -----------*) |
|
912 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
913 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
914 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
915 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
916 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
917 (*----------- 60 -----------*) |
|
918 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
919 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
920 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
921 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
922 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
923 (*----------- 70 -----------*) |
|
924 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
925 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
926 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
927 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
928 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
929 (*----------- 80 -----------*) |
|
930 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
931 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
932 \<close> ML \<open> |
|
933 (**)val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
934 \<close> ML \<open> |
|
935 (*CURRENT*)if p = ([2, 1], Pbl) andalso |
|
936 (*CURRENT*) f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []}) |
|
937 (*CURRENT*)then |
|
938 (*CURRENT*) case nxt of |
|
939 (*CURRENT*) ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*)) |
|
940 (*CURRENT*) | _ => error "me biegelinie changed 1" |
|
941 (*CURRENT*)else error "me biegelinie changed 2"; |
|
942 \<close> ML \<open> |
|
943 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
944 (*CURRENT*)nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*) |
|
945 \<close> ML \<open> |
|
946 (*----- due to "switch from Script to partial_function" 4035ec339062 ? |
|
947 OR ?due to "failed trial to generalise handling of meths which extend the model of a probl " 98298342fb6d |
|
948 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
949 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
950 (*----------- 90 -----------*) |
|
951 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
952 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
953 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
954 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
955 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
956 (*---------- 100 -----------*) |
|
957 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
958 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
959 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
960 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
961 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
962 (*---------- 110 -----------*) |
|
963 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
964 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
965 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
966 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
967 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
968 (*---------- 120 -----------*) |
|
969 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
970 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
971 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
972 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
973 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
974 (*---------- 130 -----------*) |
|
975 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
976 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
977 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
978 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
979 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
980 |
|
981 if p = ([3], Pbl) |
|
982 then |
|
983 case nxt of |
|
984 ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") => |
|
985 (case f of |
|
986 PpcKF |
|
987 (Problem [], |
|
988 {Find = [Incompl "solution []"], Given = |
|
989 [Correct |
|
990 "equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]", |
|
991 Incompl "solveForVars [c]"], |
|
992 Relate = [], Where = [], With = []}) => () |
|
993 | _ => error "Bsp.7.70 me changed 1") |
|
994 | _ => error "Bsp.7.70 me changed 2" |
|
995 else error "Bsp.7.70 me changed 3"; |
|
996 -----*) |
|
997 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *) |
|
998 |
|
999 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---"; |
|
1000 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---"; |
|
1001 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---"; |
|
1002 (* the error in this test might be independent from introduction of y, dy |
|
1003 as arguments in IntegrierenUndKonstanteBestimmen2, |
|
1004 rather due to so far untested use of "auto" *) |
|
1005 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
|
1006 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", |
|
1007 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", |
|
1008 "AbleitungBiegelinie dy"]; |
|
1009 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], |
|
1010 ["IntegrierenUndKonstanteBestimmen2"]); |
|
1011 |
|
1012 reset_states (); |
|
1013 CalcTree [(fmz, (dI',pI',mI'))]; |
|
1014 Iterator 1; |
|
1015 moveActiveRoot 1; |
|
1016 |
|
1017 (*[], Met*)autoCalculate 1 CompleteCalcHead; |
|
1018 (*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *) |
|
1019 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**) |
|
1020 (*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *) |
|
1021 (*[2], Res*)autoCalculate 1 CompleteSubpbl; |
|
1022 (*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *) |
|
1023 (*[3], Met*)autoCalculate 1 CompleteCalcHead; |
|
1024 (*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1025 (*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*) |
|
1026 (*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1027 (*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1028 (*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1029 (*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1030 (*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1031 (*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1032 (*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1033 (*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1034 (*[3, 8], Met*)autoCalculate 1 CompleteCalcHead; |
|
1035 (*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1036 (*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *) |
|
1037 (*(**)autoCalculate 1 (Step 1); |
|
1038 *** generate1: not impl.for Empty_Tac_ |
|
1039 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *) |
|
1040 |
|
1041 val ((pt,_),_) = get_calc 1; |
|
1042 val ip = get_pos 1 1; |
|
1043 val (Form f, tac, asms) = pt_extract (pt, ip); |
|
1044 |
|
1045 if ip = ([2, 1, 1], Frm) andalso |
|
1046 term2str f = "hd []" |
|
1047 then |
|
1048 case tac of |
|
1049 SOME Empty_Tac => () |
|
1050 | _ => error "ERROR biegel.7.70 changed 1" |
|
1051 else error "ERROR biegel.7.70 changed 2"; |
|
1052 |
|
1053 (*----- this state has been reached shortly after 98298342fb6d: |
|
1054 if ip = ([3, 8, 1], Res) andalso |
|
1055 term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]" |
|
1056 then |
|
1057 case tac of |
|
1058 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => () |
|
1059 | _ => error "ERROR biegel.7.70 changed 1" |
|
1060 else error "ERROR biegel.7.70 changed 2"; |
|
1061 *) |
74 \<close> ML \<open> |
1062 \<close> ML \<open> |
75 \<close> ML \<open> |
1063 \<close> ML \<open> |
76 "~~~~~ fun xxx , args:"; val () = (); |
1064 "~~~~~ fun xxx , args:"; val () = (); |
77 \<close> |
1065 \<close> |
78 |
1066 |