1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -377,10 +377,10 @@
1.4
1.5 val p = ([],Pbl);
1.6 val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
1.7 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.8 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.9 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.10 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.11 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
1.12 - (*^^^ these are the elements for the root-problem (in variants)*)
1.13 + (* \<up> these are the elements for the root-problem (in variants)*)
1.14 (*vvv these are elements required for subproblems*)
1.15 "boundVariable a", "boundVariable b", "boundVariable alpha",
1.16 "interval {x::real. 0 <= x & x <= 2*r}",
1.17 @@ -431,14 +431,14 @@
1.18 Relate ["relations [A=a*b, a/2=r*sin alpha, \
1.19 \b/2=r*cos alpha]"]], Pbl, References.empty);
1.20 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
1.21 - if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
1.22 + if ocalhd2str ocalhd = ------------ \<up> \<up> \<up> ^ missing !!!*)
1.23
1.24 (*this input is complete in variant 1 (variant 3 does not work yet)*)
1.25 val (b,pt''''',ocalhd) =
1.26 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
1.27 Find ["maximum A", "valuesFor [a,b]"],
1.28 Relate ["relations [A=a*b, \
1.29 - \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
1.30 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]],
1.31 Pbl, References.empty);
1.32 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
1.33
1.34 @@ -474,7 +474,7 @@
1.35 val ifo = "solve(x+1=2,x)";
1.36 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
1.37 (*
1.38 - This trick ^^^^^^^^^ micked input of ^^^^^^^^^^^^^^^^^ in the front-end.
1.39 + This trick \<up> \<up> \<up> micked input of \<up> \<up> \<up> \<up> \<up> ^^ in the front-end.
1.40 The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore
1.41 (TODO hg bisect ?) and raises the ERROR Undefined fact: "xfoldr_Nil".
1.42
1.43 @@ -637,7 +637,7 @@
1.44 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.45 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.46 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.47 -val t = TermC.str2term "Diff (x^^^2 + x + 1, x)";
1.48 +val t = TermC.str2term "Diff (x \<up> 2 + x + 1, x)";
1.49 case t of Const ("Diff.Diff", _) $ _ => ()
1.50 | _ => raise
1.51 error "diff.sml behav.changed for CAS Diff (..., x)";
1.52 @@ -648,7 +648,7 @@
1.53 (*3>*)Iterator 1;moveActiveRoot 1;
1.54 "----- here the Headline has been finished";
1.55 (*4>*)moveActiveFormula 1 ([],Pbl);
1.56 -(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
1.57 +(*5>*)replaceFormula 1 "Diff (x \<up> 2 + x + 1, x)";
1.58 val ((pt,_),_) = get_calc 1;
1.59 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
1.60 val (SOME istate, NONE) = loc;
1.61 @@ -679,12 +679,12 @@
1.62 ["diff", "differentiate_on_R"]) : spec*)
1.63 writeln (I_Model.to_string ctxt probl);
1.64 (*[
1.65 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.66 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
1.67 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.68 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.69 writeln (I_Model.to_string ctxt meth);
1.70 (*[
1.71 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.72 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
1.73 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.74 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.75 writeln"-----------------------------------------------------------";
1.76 @@ -694,8 +694,9 @@
1.77 val ((pt,p),_) = get_calc 1;
1.78 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
1.79 Test_Tool.show_pt pt;
1.80 +
1.81 if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
1.82 -else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
1.83 +else error "diff.sml behav.changed for Diff (x \<up> 2 + x + 1, x)";
1.84 DEconstrCalcTree 1;
1.85
1.86 "--------- Take as 1st tac, start from exp -----------------------";
1.87 @@ -704,7 +705,7 @@
1.88 (*the following input is copied from BridgeLog Java <==> SML,
1.89 omitting unnecessary inputs*)
1.90 (*1>*)reset_states ();
1.91 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))];
1.92 +(*2>*)CalcTree [(["functionTerm (x \<up> 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))];
1.93 (*3>*)Iterator 1; moveActiveRoot 1;
1.94
1.95 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.96 @@ -722,12 +723,12 @@
1.97 ["diff", "differentiate_on_R"]) : spec*)
1.98 writeln (I_Model.to_string ctxt probl);
1.99 (*[
1.100 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.101 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
1.102 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.103 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.104 writeln (I_Model.to_string ctxt meth);
1.105 (*[
1.106 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.107 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
1.108 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.109 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.110 writeln"-----------------------------------------------------------";
1.111 @@ -735,8 +736,8 @@
1.112 autoCalculate 1 (Steps 1);
1.113 val ((pt,p),_) = get_calc 1;
1.114 val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
1.115 -if UnparseC.term res = "d_d x (x ^^^ 2 + x + 1)" then ()
1.116 -else error "diff.sml Diff (x^2 + x + 1, x) from exp";
1.117 +if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
1.118 +else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
1.119 DEconstrCalcTree 1;
1.120
1.121 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
1.122 @@ -945,30 +946,30 @@
1.123 "--------- build fun check_for' ?bdv -------------------------";
1.124 "--------- build fun check_for' ?bdv -------------------------";
1.125 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
1.126 -val t = TermC.str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
1.127 +val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))";
1.128 val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
1.129 -if UnparseC.term t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
1.130 +if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
1.131 else error "build fun check_for' ?bdv changed 1";
1.132
1.133 val rls = norm_diff
1.134 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
1.135 -val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x ^^^ 4))", TermC.str2term "2 * x + cos (4 * x ^^^ 3)");
1.136 +val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
1.137
1.138 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
1.139 rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
1.140 -if UnparseC.term res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
1.141 +if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
1.142 else error "build fun check_for' ?bdv changed 2";
1.143
1.144 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
1.145 NONE => res'
1.146 | SOME (norm_res, _) => norm_res;
1.147 -if UnparseC.term norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
1.148 +if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then ()
1.149 else error "build fun check_for' ?bdv changed 3";
1.150
1.151 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
1.152 NONE => inf
1.153 | SOME (norm_inf, _) => norm_inf;
1.154 -if UnparseC.term norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
1.155 +if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then ()
1.156 else error "build fun check_for' ?bdv changed 4";
1.157
1.158 res' = inf;
1.159 @@ -982,8 +983,8 @@
1.160 "--------- build fun check_for ------------------------";
1.161 "--------- build fun check_for ------------------------";
1.162 val (res, inf) =
1.163 - (TermC.str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
1.164 - TermC.str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
1.165 + (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
1.166 + TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.167 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"]
1.168
1.169 val env = [(TermC.str2term "v_v", TermC.str2term "x")];
1.170 @@ -992,7 +993,7 @@
1.171 ("chain-rule-diff-both",
1.172 [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
1.173 TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
1.174 - TermC.parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
1.175 + TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
1.176 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
1.177 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.178 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
1.179 @@ -1006,16 +1007,16 @@
1.180 "--------- embed fun check_for ------------------------";
1.181 reset_states ();
1.182 CalcTree
1.183 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.184 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.185 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.186 Iterator 1;
1.187 moveActiveRoot 1;
1.188 autoCalculate 1 CompleteCalcHead;
1.189 autoCalculate 1 (Steps 1);
1.190 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.191 -(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
1.192 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.193 +(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> \<up> 4)*)
1.194
1.195 -"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
1.196 +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.197 "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
1.198 val cs = get_calc cI
1.199 val pos = get_pos cI 1;
1.200 @@ -1043,13 +1044,13 @@
1.201 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
1.202 | _ => error "inform: uncovered case of MethodC.from_store"
1.203 ;
1.204 -(*+*)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\"]]"
1.205 +(*+*)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 \<up> ?n) = ?n * ?u \<up> (?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 \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (E_ \<up> ?u) = E_ \<up> ?u * d_d ?x ?u\"]]"
1.206 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
1.207
1.208 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
1.209 ;
1.210 -(*+*)if UnparseC.term f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.211 -(*+*) UnparseC.term f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
1.212 +(*+*)if UnparseC.term f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.213 +(*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
1.214 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
1.215
1.216 val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
1.217 @@ -1066,14 +1067,14 @@
1.218 "--------- embed fun find_fill_patterns ---------------------------";
1.219 reset_states ();
1.220 CalcTree
1.221 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.222 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.223 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.224 Iterator 1;
1.225 moveActiveRoot 1;
1.226 autoCalculate 1 CompleteCalcHead;
1.227 autoCalculate 1 (Steps 1);
1.228 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.229 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
1.230 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.231 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*);
1.232 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
1.233 (*or
1.234 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
1.235 @@ -1096,7 +1097,7 @@
1.236
1.237 case map (Error_Pattern.fill_from_store subst f_curr errpatID) errpatthms |> flat of
1.238 ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm =
1.239 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
1.240 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.241 then () else error "find_fill_patterns changed 1a"
1.242 | _ => error "find_fill_patterns changed 1b"
1.243
1.244 @@ -1110,7 +1111,7 @@
1.245
1.246 case some |> filter is_some |> map the of
1.247 ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
1.248 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
1.249 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
1.250 then () else error "find_fill_patterns changed 2a"
1.251 | _ => error "find_fill_patterns changed 2b"
1.252
1.253 @@ -1120,7 +1121,7 @@
1.254 val (form', _, _, rewritten) =
1.255 rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
1.256
1.257 -if UnparseC.term form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
1.258 +if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
1.259 else error "find_fill_patterns changed 3";
1.260
1.261 "~~~~~ to findFillpatterns return val:"; val (fillpats) =
1.262 @@ -1130,16 +1131,16 @@
1.263 val msg = "fill patterns " ^
1.264 ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
1.265 msg =
1.266 - "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.267 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
1.268 - "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.269 - " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
1.270 - "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.271 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
1.272 - "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
1.273 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
1.274 - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
1.275 -"^^^--- dropped this code WN120730";
1.276 + "fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.277 + " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" ^
1.278 + "#fill-both-args#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.279 + " =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
1.280 + "#fill-d_d#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.281 + " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1 x (x \<up> 4)" ^
1.282 + "#fill-inner-deriv#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
1.283 + " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1" ^
1.284 + "#fill-all#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) = d_d x (x \<up> 2) + ?_dummy_1#";
1.285 +" \<up> --- dropped this code WN120730";
1.286
1.287 if (map #1 fillpats) =
1.288 ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
1.289 @@ -1151,23 +1152,23 @@
1.290 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.291 reset_states ();
1.292 CalcTree
1.293 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.294 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.295 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.296 Iterator 1;
1.297 moveActiveRoot 1;
1.298 autoCalculate 1 CompleteCalcHead;
1.299 autoCalculate 1 (Steps 1);
1.300 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.301 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.302 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.303 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.304 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.305 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1.306 + would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1.307 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.308 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.309 val ((pt,pos), _) = get_calc 1;
1.310 val p = get_pos 1 1;
1.311 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.312
1.313 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
1.314 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.315 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.316 ("diff_sum", thm)) =>
1.317 if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.318 @@ -1176,13 +1177,13 @@
1.319 else error "embed fun fill_form changed 13";
1.320
1.321 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.322 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1.323 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.324 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
1.325 + d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.326 val ((pt,pos),_) = get_calc 1;
1.327 val p = get_pos 1 1;
1.328
1.329 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.330 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
1.331 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.332 case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.333 ("diff_sum", thm)) =>
1.334 if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.335 @@ -1196,7 +1197,7 @@
1.336 val p = get_pos 1 1;
1.337 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.338 if p = ([1], Res) andalso existpt [2] pt
1.339 - andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1.340 + andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.341 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.342 ("diff_sum", thm)) =>
1.343 if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
1.344 @@ -1210,7 +1211,7 @@
1.345 the respective thm is in the ctree ................
1.346 *)
1.347 "~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
1.348 - (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
1.349 + (1, "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)");
1.350 val ((pt, _), _) = get_calc cI
1.351 val pos = get_pos cI 1;
1.352
1.353 @@ -1234,7 +1235,7 @@
1.354 val ((pt, _),_) = get_calc 1;
1.355 val p = get_pos 1 1;
1.356 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.357 - if p = ([2], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
1.358 + if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
1.359 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.360 ("diff_sin_chain", thm)) =>
1.361 if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
1.362 @@ -1307,7 +1308,7 @@
1.363 ------------------------------------------------------------------------------
1.364 1. "5 * x / (x - 2) - x / (x + 2) = 4"
1.365 ...
1.366 -4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalise", "poly"..
1.367 +4. "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)",Subproblem["normalise", "poly"..
1.368 ...
1.369 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
1.370 ...
1.371 @@ -1322,14 +1323,14 @@
1.372
1.373
1.374 ------------------------------------------------------------------------------
1.375 -"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
1.376 +"Schalk I s.87 Bsp 55b (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)";
1.377 ------------------------------------------------------------------------------
1.378 -1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
1.379 +1. "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x"
1.380 ...
1.381 -4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
1.382 +4. "(3 + (-1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))"
1.383 Subproblem["normalise", "polynomial", "univariate"..
1.384 ...
1.385 -4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
1.386 +4.4. "-6 * x + 5 * x \<up> 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
1.387 ...
1.388 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.389 4.4.5. "[x = 0, x = 6 / 5]"
1.390 @@ -1351,10 +1352,9 @@
1.391 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1.392 Subproblem["sq", "rootX", "univariate", "equation"]
1.393 ...
1.394 -6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1.395 +6.6. "144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"
1.396 Subproblem["normalise", "polynomial", "univariate", "equation"]
1.397 -...
1.398 -6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
1.399 +...6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
1.400 ... Or_to_List
1.401 6.6.3.2 "UniversalList"
1.402 ------------------------------------------------------------------------------