diff -r 17db21aa9aed -r 73ee61385493 test/Tools/isac/Interpret/error-pattern.sml --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Apr 19 20:44:18 2021 +0200 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Apr 20 16:58:44 2021 +0200 @@ -377,10 +377,10 @@ val p = ([],Pbl); val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]", - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, (a/2) \ 2 + (b/2) \ 2 = r \ 2]", + "relations [A=a*b, (a/2) \ 2 + (b/2) \ 2 = r \ 2]", "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]", - (*^^^ these are the elements for the root-problem (in variants)*) + (* \ these are the elements for the root-problem (in variants)*) (*vvv these are elements required for subproblems*) "boundVariable a", "boundVariable b", "boundVariable alpha", "interval {x::real. 0 <= x & x <= 2*r}", @@ -431,14 +431,14 @@ Relate ["relations [A=a*b, a/2=r*sin alpha, \ \b/2=r*cos alpha]"]], Pbl, References.empty); val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; - if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*) + if ocalhd2str ocalhd = ------------ \ \ \ ^ missing !!!*) (*this input is complete in variant 1 (variant 3 does not work yet)*) val (b,pt''''',ocalhd) = input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], Find ["maximum A", "valuesFor [a,b]"], Relate ["relations [A=a*b, \ - \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], + \(a/2) \ 2 + (b/2) \ 2 = r \ 2]"]], Pbl, References.empty); val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; @@ -474,7 +474,7 @@ val ifo = "solve(x+1=2,x)"; val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)"; (* - This trick ^^^^^^^^^ micked input of ^^^^^^^^^^^^^^^^^ in the front-end. + This trick \ \ \ micked input of \ \ \ \ \ ^^ in the front-end. The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore (TODO hg bisect ?) and raises the ERROR Undefined fact: "xfoldr_Nil". @@ -637,7 +637,7 @@ "--------- Take as 1st tac, start with (CAS input) ---------"; "--------- Take as 1st tac, start with (CAS input) ---------"; "--------- Take as 1st tac, start with (CAS input) ---------"; -val t = TermC.str2term "Diff (x^^^2 + x + 1, x)"; +val t = TermC.str2term "Diff (x \ 2 + x + 1, x)"; case t of Const ("Diff.Diff", _) $ _ => () | _ => raise error "diff.sml behav.changed for CAS Diff (..., x)"; @@ -648,7 +648,7 @@ (*3>*)Iterator 1;moveActiveRoot 1; "----- here the Headline has been finished"; (*4>*)moveActiveFormula 1 ([],Pbl); -(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)"; +(*5>*)replaceFormula 1 "Diff (x \ 2 + x + 1, x)"; val ((pt,_),_) = get_calc 1; val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; val (SOME istate, NONE) = loc; @@ -679,12 +679,12 @@ ["diff", "differentiate_on_R"]) : spec*) writeln (I_Model.to_string ctxt probl); (*[ -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) writeln (I_Model.to_string ctxt meth); (*[ -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) writeln"-----------------------------------------------------------"; @@ -694,8 +694,9 @@ val ((pt,p),_) = get_calc 1; val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; + if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then () -else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)"; +else error "diff.sml behav.changed for Diff (x \ 2 + x + 1, x)"; DEconstrCalcTree 1; "--------- Take as 1st tac, start from exp -----------------------"; @@ -704,7 +705,7 @@ (*the following input is copied from BridgeLog Java <==> SML, omitting unnecessary inputs*) (*1>*)reset_states (); -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))]; +(*2>*)CalcTree [(["functionTerm (x \ 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))]; (*3>*)Iterator 1; moveActiveRoot 1; (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; @@ -722,12 +723,12 @@ ["diff", "differentiate_on_R"]) : spec*) writeln (I_Model.to_string ctxt probl); (*[ -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) writeln (I_Model.to_string ctxt meth); (*[ -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) writeln"-----------------------------------------------------------"; @@ -735,8 +736,8 @@ autoCalculate 1 (Steps 1); val ((pt,p),_) = get_calc 1; val Form res = (#1 o ME_Misc.pt_extract) (pt, p); -if UnparseC.term res = "d_d x (x ^^^ 2 + x + 1)" then () -else error "diff.sml Diff (x^2 + x + 1, x) from exp"; +if UnparseC.term res = "d_d x (x \ 2 + x + 1)" then () +else error "diff.sml Diff (x \ 2 + x + 1, x) from exp"; DEconstrCalcTree 1; "--------- implicit_take, start with (CAS input) ---------------"; @@ -945,30 +946,30 @@ "--------- build fun check_for' ?bdv -------------------------"; "--------- build fun check_for' ?bdv -------------------------"; val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst; -val t = TermC.str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))"; +val t = TermC.str2term "d_d x (x \ 2 + sin (x \ 4))"; val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t; -if UnparseC.term t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then () +if UnparseC.term t = "2 * x + cos (x \ 4) * 4 * x \ 3" then () else error "build fun check_for' ?bdv changed 1"; val rls = norm_diff val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; -val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x ^^^ 4))", TermC.str2term "2 * x + cos (4 * x ^^^ 3)"); +val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \ 4))", TermC.str2term "2 * x + cos (4 * x \ 3)"); val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; -if UnparseC.term res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then () +if UnparseC.term res' = "2 * x + cos (d_d x (x \ 4))" andalso rewritten then () else error "build fun check_for' ?bdv changed 2"; val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of NONE => res' | SOME (norm_res, _) => norm_res; -if UnparseC.term norm_res = "2 * x + cos (4 * x ^^^ 3)" then () +if UnparseC.term norm_res = "2 * x + cos (4 * x \ 3)" then () else error "build fun check_for' ?bdv changed 3"; val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of NONE => inf | SOME (norm_inf, _) => norm_inf; -if UnparseC.term norm_inf = "2 * x + cos (4 * x ^^^ 3)" then () +if UnparseC.term norm_inf = "2 * x + cos (4 * x \ 3)" then () else error "build fun check_for' ?bdv changed 4"; res' = inf; @@ -982,8 +983,8 @@ "--------- build fun check_for ------------------------"; "--------- build fun check_for ------------------------"; val (res, inf) = - (TermC.str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))", - TermC.str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"); + (TermC.str2term "d_d x (x \ 2) + d_d x (sin (x \ 4))", + TermC.str2term "d_d x (x \ 2) + cos (4 * x \ 3)"); val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"] val env = [(TermC.str2term "v_v", TermC.str2term "x")]; @@ -992,7 +993,7 @@ ("chain-rule-diff-both", [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", - TermC.parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)", + TermC.parse_patt @{theory} "d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1)", TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @@ -1006,16 +1007,16 @@ "--------- embed fun check_for ------------------------"; reset_states (); CalcTree -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], +[(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*) +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) +(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ \ 4)*) -"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)"); +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \ 2) + cos (4 * x \ 3)"); "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo); val cs = get_calc cI val pos = get_pos cI 1; @@ -1043,13 +1044,13 @@ {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog) | _ => error "inform: uncovered case of MethodC.from_store" ; -(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]" +(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (E_ \ ?u) = E_ \ ?u * d_d ?x ?u\"]]" (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3"; val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate ; -(*+*)if UnparseC.term f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso -(*+*) UnparseC.term f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)" +(*+*)if UnparseC.term f_pred = "d_d x (x \ 2) + d_d x (sin (x \ 4))" andalso +(*+*) UnparseC.term f_in = "d_d x (x \ 2) + cos (4 * x \ 3)" (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2"; val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*); @@ -1066,14 +1067,14 @@ "--------- embed fun find_fill_patterns ---------------------------"; reset_states (); CalcTree -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], +[(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) +appendFormula 1 "d_d x (x \ 2) + cos (4 * x \ 3)" (*|> Future.join*); (* error pattern #chain-rule-diff-both# *) (*or no derivation found *) @@ -1096,7 +1097,7 @@ case map (Error_Pattern.fill_from_store subst f_curr errpatID) errpatthms |> flat of ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm = - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" + "d_d x (x \ 2) + d_d x (sin (x \ 4)) =\nd_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" then () else error "find_fill_patterns changed 1a" | _ => error "find_fill_patterns changed 1b" @@ -1110,7 +1111,7 @@ case some |> filter is_some |> map the of ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm = - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" + "d_d x (x \ 2) + d_d x (sin (x \ 4)) =\nd_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" then () else error "find_fill_patterns changed 2a" | _ => error "find_fill_patterns changed 2b" @@ -1120,7 +1121,7 @@ val (form', _, _, rewritten) = rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; -if UnparseC.term form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then () +if UnparseC.term form' = "d_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" then () else error "find_fill_patterns changed 3"; "~~~~~ to findFillpatterns return val:"; val (fillpats) = @@ -1130,16 +1131,16 @@ val msg = "fill patterns " ^ ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_); msg = - "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^ - "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ - " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^ - "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^ - "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^ - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^ - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#"; -"^^^--- dropped this code WN120730"; + "fill patterns #fill-d_d-arg#d_d x (x \ 2) + d_d x (sin (x \ 4))" ^ + " =\nd_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" ^ + "#fill-both-args#d_d x (x \ 2) + d_d x (sin (x \ 4))" ^ + " =\nd_d x (x \ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^ + "#fill-d_d#d_d x (x \ 2) + d_d x (sin (x \ 4))" ^ + " =\nd_d x (x \ 2) + cos (x \ 4) * ?_dummy_1 x (x \ 4)" ^ + "#fill-inner-deriv#d_d x (x \ 2) + d_d x (sin (x \ 4))" ^ + " =\nd_d x (x \ 2) + cos (x \ 4) * ?_dummy_1" ^ + "#fill-all#d_d x (x \ 2) + d_d x (sin (x \ 4)) = d_d x (x \ 2) + ?_dummy_1#"; +" \ --- dropped this code WN120730"; if (map #1 fillpats) = ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"] @@ -1151,23 +1152,23 @@ "--------- build fun is_exactly_equal, inputFillFormula ----------"; reset_states (); CalcTree -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], +[(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalcHead; autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*) +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) +appendFormula 1 "d_d x (x \ 2) + cos (4 * x \ 3)" (*|> Future.join*); (*<<<<<<<=========================*) (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. + would recognize "cos (4 * x \ (4 - 1)) + 2 * x" as well. results in error pattern #chain-rule-diff-both# instead of no derivation found *) val ((pt,pos), _) = get_calc 1; val p = get_pos 1 1; val (Form f, _, asms) = ME_Misc.pt_extract (pt, p); - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", thm)) => if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () @@ -1176,13 +1177,13 @@ else error "embed fun fill_form changed 13"; findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*) -(* fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) +(* fill patterns #fill-d_d-arg#d_d x (x \ 2) + d_d x (sin (x \ 4)) = + d_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) val ((pt,pos),_) = get_calc 1; val p = get_pos 1 1; val (Form f, _, asms) = ME_Misc.pt_extract (pt, p); - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", thm)) => if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () @@ -1196,7 +1197,7 @@ val p = get_pos 1 1; val (Form f, _, asms) = ME_Misc.pt_extract (pt, p); if p = ([1], Res) andalso existpt [2] pt - andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" + andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", thm)) => if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () @@ -1210,7 +1211,7 @@ the respective thm is in the ctree ................ *) "~~~~~ fun inputFillFormula, args:"; val (cI, ifo) = - (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"); + (1, "d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ 4)"); val ((pt, _), _) = get_calc cI val pos = get_pos cI 1; @@ -1234,7 +1235,7 @@ val ((pt, _),_) = get_calc 1; val p = get_pos 1 1; val (Form f, _, asms) = ME_Misc.pt_extract (pt, p); - if p = ([2], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" + if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ 4)" then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", thm)) => if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then () @@ -1307,7 +1308,7 @@ ------------------------------------------------------------------------------ 1. "5 * x / (x - 2) - x / (x + 2) = 4" ... -4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalise", "poly".. +4. "12 * x + 4 * x \ 2 = 4 * (-4 + x \ 2)",Subproblem["normalise", "poly".. ... 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate".. ... @@ -1322,14 +1323,14 @@ ------------------------------------------------------------------------------ -"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)"; +"Schalk I s.87 Bsp 55b (x/(x \ 2 - 6*x+9) - 1/(x \ 2 - 3*x) =1/x)"; ------------------------------------------------------------------------------ -1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x" +1. "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) = 1 / x" ... -4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))" +4. "(3 + (-1 * x + x \ 2)) * x = 1 * (9 * x + (x \ 3 + -6 * x \ 2))" Subproblem["normalise", "polynomial", "univariate".. ... -4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. +4.4. "-6 * x + 5 * x \ 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. ... 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" 4.4.5. "[x = 0, x = 6 / 5]" @@ -1351,10 +1352,9 @@ 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" Subproblem["sq", "rootX", "univariate", "equation"] ... -6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2" +6.6. "144 + 288 * x + 144 * x \ 2 = 144 + x \ 2 + 288 * x + 143 * x \ 2" Subproblem["normalise", "polynomial", "univariate", "equation"] -... -6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"] +...6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"] ... Or_to_List 6.6.3.2 "UniversalList" ------------------------------------------------------------------------------