1 theory Test_Some imports Isac.Build_Thydata
4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
5 (* these vvv test, if funs are intermediately opened in structure
6 in case of errors here consider ~~/./xtest-to-coding.sh *)
8 open Math_Engine; CalcTreeTEST;
10 open Inform; cas_input;
11 open Rtools; trtas2str;
12 open Chead; pt_extract;
13 open Generate; (* NONE *)
14 open Ctree; append_problem;
15 open Specify; show_ptyps;
16 open Applicable; mk_set;
17 open Solve; (* NONE *)
19 open Stool; transfer_asms_from_to;
21 open Model; (* NONE *)
22 open LTool; rule2stac;
27 open Rule; string_of_thm;
29 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31 ML_file "Knowledge/biegelinie-3.sml"
33 section \<open>code for copy & paste ===============================================================\<close>
35 "~~~~~ fun xxx , args:"; val () = ();
36 "~~~~~ and xxx , args:"; val () = ();
38 "~~~~~ to xxx return val:"; val () = ();
42 declare [[show_types]]
43 declare [[show_sorts]]
44 find_theorems "?a <= ?a"
50 ML_command \<open>Pretty.writeln prt\<close>
51 declare [[ML_print_depth = 999]]
52 declare [[ML_exception_trace]]
55 (*========== inhibit exn WN130909 TODO =========================================================
56 ============ inhibit exn WN130909 TODO ========================================================*)
57 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
58 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
61 section \<open>===================================================================================\<close>
63 "~~~~~ fun xxx , args:"; val () = ();
67 "~~~~~ fun xxx , args:"; val () = ();
70 section \<open>================= "Knowledge/partial_fractions.sml" ============================\<close>
72 "~~~~~ fun xxx , args:"; val () = ();
74 (* Title: partial fraction decomposition
76 (c) due to copyright terms
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 "--------------------------------------------------------";
96 "----------- why helpless here ? ------------------------";
97 "----------- why helpless here ? ------------------------";
98 "----------- why helpless here ? ------------------------";
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))];
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";
111 (*CURRENT*)(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse"])*)
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.
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]"]*)
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)))";
124 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
125 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
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";
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";*)
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);
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";
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.
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;
168 "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
169 then () else error "factors_from_solution broken";
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
178 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
179 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
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));
185 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
186 else error "HOLogic.mk_binop broken ?";
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*)
193 "----------- = me for met_partial_fraction --------------";
194 "----------- = me for met_partial_fraction --------------";
195 "----------- = me for met_partial_fraction --------------";
197 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
198 "solveFor z", "decomposedFunction p_p"];
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")*)
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"]))*)
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")*)
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")*)
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")*)
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"]*)
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"*)
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")*)
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"*)
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 = *)
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 = *)
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 = *)
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 = *)
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 = *)
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 = *)
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 = *)
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 = *)
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"]*)
312 (*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)
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'*)
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";
325 (''Partial_Fractions'',
326 ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
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"],
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)]
430 "----------- autoCalculate for met_partial_fraction -----";
431 "----------- autoCalculate for met_partial_fraction -----";
432 "----------- autoCalculate for met_partial_fraction -----";
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'))];
444 autoCalculate 1 CompleteCalc;
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'";
450 val (Form f, tac, asms) = pt_extract (pt, p);
451 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
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"
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))] *)
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)";
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*)
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";
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_")];
536 val multiply_ansatz = prep_rls @{theory} (
537 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
539 srls = Erls, calc = [], errpatts = [],
541 [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
543 scr = EmptyScr}:rls);
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?*)
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)*)
596 "~~~~~ fun xxx , args:"; val () = ();
599 section \<open>=============== "Knowledge/biegelinie-3.sml" ===============================\<close>
601 "~~~~~ fun xxx , args:"; val () = ();
603 (* "Knowledge/biegelinie-3.sml"
604 author: Walther Neuper 190515
605 (c) due to copyright terms
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 "-----------------------------------------------------------------";
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*)
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 ----------------------------------------//*)
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"*)
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"]"
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]"]*)
670 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
672 (*locatetac is here for testing by me; step would suffice in me*)
673 case locatetac tac (pt,p) of
674 ("ok", (_, _, ptp)) => ptp
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'''"])]
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*)
693 loc_solve_ (mI,m) ptp;
694 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
696 Solve.solve m (pt, pos);
697 "~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
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;
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*);
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'''"])]
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));
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*);
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] *)
748 | _ => error ("assy: call by " ^ pos'2str (p,p_));
749 val Ass (m,v') = (*case*) assod pt d m stac (*of*);
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')) =
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);
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 *)
775 (*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
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*)
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); (*[]*)
809 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
811 (*locatetac is here for testing by me; step would suffice in me*)
812 case locatetac tac (pt,p) of
813 ("ok", (_, _, ptp)) => ptp
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*)
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;
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
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
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''']))] *)
856 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
858 if mI' = ["Biegelinien", "ausBelastung"]
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", [])]))] )))]
869 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
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"}] )))]
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", [])]))] )))]
890 if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
891 (*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
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;
933 (**)val (p,_,f,nxt,_,pt) = me nxt p c pt;
935 (*CURRENT*)if p = ([2, 1], Pbl) andalso
936 (*CURRENT*) f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
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";
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)")*)
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;
984 ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
988 {Find = [Incompl "solution []"], Given =
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";
997 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
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"]);
1013 CalcTree [(fmz, (dI',pI',mI'))];
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 *)
1041 val ((pt,_),_) = get_calc 1;
1042 val ip = get_pos 1 1;
1043 val (Form f, tac, asms) = pt_extract (pt, ip);
1045 if ip = ([2, 1, 1], Frm) andalso
1046 term2str f = "hd []"
1049 SOME Empty_Tac => ()
1050 | _ => error "ERROR biegel.7.70 changed 1"
1051 else error "ERROR biegel.7.70 changed 2";
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]"
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";
1064 "~~~~~ fun xxx , args:"; val () = ();
1067 section \<open>===================================================================================\<close>
1069 "~~~~~ fun xxx , args:"; val () = ();
1073 "~~~~~ fun xxx , args:"; val () = ();
1076 section \<open>code for copy & paste ===============================================================\<close>
1078 "~~~~~ fun xxx , args:"; val () = ();
1079 "~~~~~ and xxx , args:"; val () = ();
1081 "~~~~~ to xxx return val:"; val () = ();