617 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
617 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
618 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); |
618 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); |
619 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
619 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
620 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); |
620 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); |
621 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
621 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
622 setNextTactic 1 (Rewrite ("all_left", @{thm all_left})); |
622 setNextTactic 1 (Rewrite ("all_left", num_str @{thm all_left})); |
623 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
623 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
624 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in")); |
624 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in")); |
625 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
625 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
626 (* __________ for "16 + 12 * x = 0"*) |
626 (* __________ for "16 + 12 * x = 0"*) |
627 setNextTactic 1 (Subproblem ("PolyEq", |
627 setNextTactic 1 (Subproblem ("PolyEq", |
1346 show_pt pt; |
1346 show_pt pt; |
1347 val p = get_pos 1 1; |
1347 val p = get_pos 1 1; |
1348 val (Form f, tac, asms) = pt_extract (pt, p); |
1348 val (Form f, tac, asms) = pt_extract (pt, p); |
1349 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else |
1349 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else |
1350 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; |
1350 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; |
1351 DEconstrCalcTree 1; |
1351 DEconstrCalcTree 1; |
1352 |
1352 |
1353 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1353 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1354 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1354 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1355 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1355 "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; |
1356 CalcTree |
1356 CalcTree |
1368 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *) |
1368 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *) |
1369 val ((pt,pos), _) = get_calc 1; |
1369 val ((pt,pos), _) = get_calc 1; |
1370 val p = get_pos 1 1; |
1370 val p = get_pos 1 1; |
1371 val (Form f, _, asms) = pt_extract (pt, p); |
1371 val (Form f, _, asms) = pt_extract (pt, p); |
1372 |
1372 |
1373 if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" |
1373 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" |
1374 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"], |
1374 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"], |
1375 ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0" |
1375 ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0" |
1376 | _ => error "embed fun get_fillform changed 1" |
1376 | _ => error "embed fun get_fillform changed 1" |
1377 else error "embed fun get_fillform changed 2"; |
1377 else error "embed fun get_fillform changed 2"; |
1378 ============ inhibit exn WN161019 TODO ========================================================*) |
|
1379 |
1378 |
1380 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== |
1379 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== |
1381 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*) |
1380 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*) |
1382 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = |
1381 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = |
1383 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) |
1382 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) |
1435 |
1434 |
1436 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1435 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1437 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1436 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1438 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1437 "--------- UC errpat add-fraction, fillpat by input --------------"; |
1439 (*cp from BridgeLog Java <=> SML*) |
1438 (*cp from BridgeLog Java <=> SML*) |
1440 =CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; |
1439 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; |
1441 Iterator 1; |
1440 Iterator 1; |
1442 moveActiveRoot 1; |
1441 moveActiveRoot 1; |
1443 moveActiveFormula 1 ([],Pbl); |
1442 moveActiveFormula 1 ([],Pbl); |
1444 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))"; |
1443 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))"; |
1445 autoCalculate 1 CompleteCalcHead; |
1444 autoCalculate 1 CompleteCalcHead; |
1452 |
1451 |
1453 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1452 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1454 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1453 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1455 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1454 "--------- UC errpat, fillpat step to Rewrite --------------------"; |
1456 (*TODO*) |
1455 (*TODO*) |
1457 =CalcTree |
1456 CalcTree |
1458 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))", |
1457 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))", |
1459 "differentiateFor x", "derivative f_f'"], |
1458 "differentiateFor x", "derivative f_f'"], |
1460 ("Isac", ["derivative_of","function"], |
1459 ("Isac", ["derivative_of","function"], |
1461 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*) |
1460 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*) |
1462 Iterator 1; |
1461 Iterator 1; |