1.1 --- a/test/Tools/isac/Test_Isac.thy Thu Oct 20 10:23:38 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Oct 20 10:47:52 2022 +0200
1.3 @@ -317,1638 +317,6 @@
1.4
1.5 section \<open>further tests additional to src/.. files\<close>
1.6 ML_file "BridgeLibisabelle/use-cases.sml"
1.7 -ML \<open>
1.8 -\<close> ML \<open>
1.9 -\<close> ML \<open>
1.10 -(* Title: tests the interface of isac's SML-kernel in accordance to
1.11 - java-tests/isac.bridge.
1.12 - Author: Walther Neuper
1.13 - (c) copyright due to lincense terms.
1.14 -
1.15 -Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.
1.16 -Some tests are outcommented since "eliminate ThmC.numerals_to_Free";
1.17 -these are considered irrelevant for Isabelle/Isac.
1.18 -
1.19 -WN050707 ... if true, the test ist marked with a \label referring
1.20 -to the same UC in isac-docu.tex as the JUnit testcase.
1.21 -WN120210?not ME: added some labels, which are not among the above,
1.22 -repaired lost \label (s).
1.23 -
1.24 -theory Test_Some imports Isac.Build_Thydata begin
1.25 -ML {* KEStore_Elems.set_ref_thy @{theory};
1.26 - fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
1.27 -ML_file "Frontend/use-cases.sml"
1.28 -*)
1.29 -
1.30 -"--------------------------------------------------------";
1.31 -"table of contents --------------------------------------";
1.32 -"--------------------------------------------------------";
1.33 -"within struct ------------------------------------------";
1.34 -"--------------------------------------------------------";
1.35 -"--------- encode ^ -> ^^ ------------------------------";
1.36 -"--------------------------------------------------------";
1.37 -"exported from struct -----------------------------------";
1.38 -"--------------------------------------------------------";
1.39 -(*"--------- empty rootpbl --------------------------------";*)
1.40 -"--------- solve_linear as rootpbl FE -------------------";
1.41 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.42 -"--------- miniscript with mini-subpbl ------------------";
1.43 -"--------- mini-subpbl AUTOCALCULATE Steps 1 ------------";
1.44 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.45 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.46 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.47 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.48 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.49 -"--------- setContext..Thy ------------------------------";
1.50 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.51 -"--------- rat-eq + subpbl: no_met, NO solution dropped - WITH fun me IN test/../solve.sml";
1.52 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.53 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.54 -"--------- maximum-example, UC: Modeling an example -----";
1.55 -"--------- solve_linear from pbl-hierarchy --------------";
1.56 -"--------- solve_linear as in an algebra system (CAS)----";
1.57 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.58 -"--------- getTactic, fetchApplicableTactics ------------";
1.59 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.60 -"--------- arbitrary combinations of steps --------------";
1.61 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.62 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.63 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.64 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.65 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.66 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.67 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.68 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.69 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.70 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.71 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.72 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.73 -"--------------------------------------------------------";
1.74 -
1.75 -"within struct ---------------------------------------------------";
1.76 -"within struct ---------------------------------------------------";
1.77 -"within struct ---------------------------------------------------";
1.78 -(*==================================================================
1.79 -
1.80 -==================================================================*)
1.81 -"exported from struct --------------------------------------------";
1.82 -"exported from struct --------------------------------------------";
1.83 -"exported from struct --------------------------------------------";
1.84 -
1.85 -
1.86 -(*------------ set at startup of the Kernel ----------------------*)
1.87 -States.reset (); (*resets all state information in Kernel *)
1.88 -(*----------------------------------------------------------------*)
1.89 -
1.90 -(*---------------------------------------------------- postpone to Outer_Syntax..Example -----
1.91 -"--------- empty rootpbl --------------------------------";
1.92 -"--------- empty rootpbl --------------------------------";
1.93 -"--------- empty rootpbl --------------------------------";
1.94 - CalcTree @{context} [([], ("", [], []))];
1.95 - Iterator 1;
1.96 - moveActiveRoot 1;
1.97 - refFormula 1 (States.get_pos 1 1);
1.98 -(*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
1.99 -DEconstrCalcTree 1;
1.100 ------------------------------------------------------- postpone to Outer_Syntax..Example -----*)
1.101 -
1.102 -"--------- solve_linear as rootpbl FE -------------------";
1.103 -"--------- solve_linear as rootpbl FE -------------------";
1.104 -"--------- solve_linear as rootpbl FE -------------------";
1.105 -States.reset ();
1.106 -
1.107 - CalcTree @{context} (*start of calculation, return No.1*)
1.108 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.109 - ("Test",
1.110 - ["LINEAR", "univariate", "equation", "test"],
1.111 - ["Test", "solve_linear"]))];
1.112 - Iterator 1; (*create an active Iterator on CalcTree @{context} No.1*)
1.113 -
1.114 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree @{context} No.1*);
1.115 - refFormula 1 (States.get_pos 1 1) (*gets CalcHead; model is still empty*);
1.116 -
1.117 -
1.118 -(*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
1.119 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
1.120 - autoCalculate 1 (Steps 1);
1.121 - refFormula 1 (States.get_pos 1 1) (*model contains descriptions for all items*);
1.122 - autoCalculate 1 (Steps 1);
1.123 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.124 -(*2*) fetchProposedTactic 1;
1.125 - setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
1.126 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*equality added*);
1.127 -
1.128 -(*3*) fetchProposedTactic 1;
1.129 - setNextTactic 1 (Add_Given "solveFor x");
1.130 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.131 -
1.132 -(*4*) fetchProposedTactic 1;
1.133 - setNextTactic 1 (Add_Find "solutions L");
1.134 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.135 -
1.136 -(*5*) fetchProposedTactic 1;
1.137 - setNextTactic 1 (Specify_Theory "Test");
1.138 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.139 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.140 -
1.141 -(*6*) fetchProposedTactic 1;
1.142 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
1.143 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.144 -(*-------------------------------------------------------------------------*)
1.145 -(*7*) fetchProposedTactic 1;
1.146 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.147 -
1.148 - setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
1.149 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.150 -
1.151 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.152 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.153 -
1.154 -(*-------------------------------------------------------------------------*)
1.155 -(*8*) fetchProposedTactic 1;
1.156 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.157 -
1.158 -(*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
1.159 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
1.160 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
1.161 - SpecificationC.is_complete ptp;
1.162 - References.are_complete ptp;
1.163 -
1.164 -(*8*) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*<---------------------- orig. test code*)
1.165 -
1.166 - val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
1.167 -(*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
1.168 -andalso Istate.string_of (get_istate_LI pt p)
1.169 - = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
1.170 -then () else error "refFormula = 1 + - 1 * 2 + x = 0 changed";
1.171 -(*-------------------------------------------------------------------------*)
1.172 -
1.173 -(*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)
1.174 -(*+\\------------------------------------------ isa == REP -----------------------------------//* )
1.175 -(*+//========================================== isa <> REP (1) ===============================\\*)
1.176 -(*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
1.177 -
1.178 -"~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
1.179 - val ((pt'''''_', _), _) = States.get_calc cI
1.180 - val ip'''''_' = States.get_pos cI 1;
1.181 -
1.182 - val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
1.183 -(*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
1.184 - Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
1.185 -
1.186 -(*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
1.187 -Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
1.188 -if Istate.string_of istate
1.189 - = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.190 -then () else error "from Step.by_tactic return --- changed 1";
1.191 -
1.192 -if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
1.193 - = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.194 -then () else error "from Step.by_tactic return --- changed 2";
1.195 -(*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
1.196 -
1.197 -"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
1.198 - val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
1.199 - (*if*) Tactic.for_specify' m; (*false*)
1.200 -
1.201 -Step_Solve.by_tactic m (pt, p);
1.202 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
1.203 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
1.204 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.205 - val (is, sc) = LItool.resume_prog (p,p_) pt;
1.206 - val Safe_Step (istate, _, tac) =
1.207 - (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
1.208 -
1.209 -(*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
1.210 -(********************* locate_input_tactic returns cstate * istate * Proof.context *************)
1.211 -(*+*)if Istate.string_of istate
1.212 -(*+isa*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.213 -then case m of Rewrite_Set_Inst' _ => ()
1.214 -else error "from locate_input_tactic return --- changed";
1.215 -
1.216 -val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
1.217 -"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
1.218 -(*\\=========================================== isa <> REP (1) ===============================//*)
1.219 -(*//=========================================== isa <> REP (2) ===============================\\*)
1.220 -(*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
1.221 -( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)
1.222 -
1.223 -"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
1.224 - val pold = States.get_pos cI 1;
1.225 - val xxx = (States.get_calc cI);
1.226 -(*isa*) val (**)xxxx(**) (**) = (**)
1.227 - (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
1.228 -"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
1.229 - (*if*) s <= 1; (*then*)
1.230 - (*val (str, (_, c', ptp)) =*)
1.231 -
1.232 -Step.do_next ip cs;
1.233 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
1.234 -
1.235 -(*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
1.236 - Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
1.237 -(*+*)if pos' = ([1], Res) andalso Istate.string_of istate
1.238 - = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.239 -then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
1.240 -
1.241 - val pIopt = get_pblID (pt,ip);
1.242 - (*if*) ip = ([], Pos.Res);(*else*)
1.243 - val (_::_) = (*case*) tacis (*of*);
1.244 -(*isa==REP*) (*if*) ip = p;(*then*)
1.245 - (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
1.246 -(*//------------------------------------- final test -----------------------------------------\\*)
1.247 -val ("ok", [], ptp as (pt, p)) = xxxx;
1.248 -
1.249 -if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> \<up> \<up> \<up> \<up> ^*)
1.250 -(*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
1.251 -then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
1.252 -
1.253 -"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
1.254 -(*\\=========================================== isa <> REP (2) ===============================//*)
1.255 -
1.256 -(*10*) fetchProposedTactic 1;
1.257 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.258 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.259 -
1.260 -(*11*) fetchProposedTactic 1;
1.261 - setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
1.262 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.263 -
1.264 -(*======= final test ==================================================*)
1.265 - val ((pt,_),_) = States.get_calc 1;
1.266 - val ip = States.get_pos 1 1;
1.267 -
1.268 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
1.269 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.270 - if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
1.271 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.272 -
1.273 -
1.274 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.275 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.276 -"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
1.277 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
1.278 -(*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
1.279 - moveActiveRoot 1;
1.280 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
1.281 - moveActiveDown 1;
1.282 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
1.283 - moveActiveDown 1 ;
1.284 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
1.285 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
1.286 - moveActiveDown 1 ; refFormula 1 ([2],Res);
1.287 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.288 - moveActiveDown 1;
1.289 - moveActiveDown 1;
1.290 - moveActiveDown 1;
1.291 - if States.get_pos 1 1 = ([2], Res) then () else
1.292 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
1.293 - moveActiveDown 1; refFormula 1 ([], Res);
1.294 - if States.get_pos 1 1 = ([], Res) then () else
1.295 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
1.296 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.297 -DEconstrCalcTree 1;
1.298 -------------------------------------------------------------------------------------------------*)
1.299 -
1.300 -"--------- miniscript with mini-subpbl ------------------";
1.301 -"--------- miniscript with mini-subpbl ------------------";
1.302 -"--------- miniscript with mini-subpbl ------------------";
1.303 -(*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
1.304 -"=== this sequence of fun-calls resembles fun me ===";
1.305 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.306 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.307 - ["Test", "squ-equ-test-subpbl1"]))];
1.308 - Iterator 1;
1.309 -
1.310 - moveActiveRoot 1;
1.311 - refFormula 1 (States.get_pos 1 1);
1.312 - fetchProposedTactic 1;
1.313 - setNextTactic 1 (Model_Problem);
1.314 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*gets ModSpec;model is still empty*)
1.315 -
1.316 - fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
1.317 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
1.318 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.319 -
1.320 - fetchProposedTactic 1;
1.321 - setNextTactic 1 (Add_Given "solveFor x");
1.322 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.323 -
1.324 - fetchProposedTactic 1;
1.325 - setNextTactic 1 (Add_Find "solutions L");
1.326 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.327 -
1.328 - fetchProposedTactic 1;
1.329 - setNextTactic 1 (Specify_Theory "Test");
1.330 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.331 -
1.332 - fetchProposedTactic 1;
1.333 - setNextTactic 1 (Specify_Problem
1.334 - ["sqroot-test", "univariate", "equation", "test"]);
1.335 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.336 -"1-----------------------------------------------------------------";
1.337 -
1.338 - fetchProposedTactic 1;
1.339 - setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
1.340 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.341 -
1.342 - fetchProposedTactic 1;
1.343 - setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
1.344 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.345 -
1.346 - fetchProposedTactic 1;
1.347 - setNextTactic 1 (Rewrite_Set "norm_equation");
1.348 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.349 -
1.350 - fetchProposedTactic 1;
1.351 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.352 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.353 -
1.354 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
1.355 - setNextTactic 1 (Subproblem ("Test",
1.356 - ["LINEAR", "univariate", "equation", "test"]));
1.357 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.358 -
1.359 - fetchProposedTactic 1;
1.360 - setNextTactic 1 (Model_Problem );
1.361 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.362 -
1.363 - fetchProposedTactic 1;
1.364 - setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
1.365 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.366 -
1.367 - fetchProposedTactic 1;
1.368 - setNextTactic 1 (Add_Given "solveFor x");
1.369 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.370 -
1.371 - fetchProposedTactic 1;
1.372 - setNextTactic 1 (Add_Find "solutions x_i");
1.373 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.374 -
1.375 - fetchProposedTactic 1;
1.376 - setNextTactic 1 (Specify_Theory "Test");
1.377 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.378 -
1.379 - fetchProposedTactic 1;
1.380 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
1.381 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.382 -"2-----------------------------------------------------------------";
1.383 -
1.384 - fetchProposedTactic 1;
1.385 - setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
1.386 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.387 -
1.388 - fetchProposedTactic 1;
1.389 - setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
1.390 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.391 -
1.392 - fetchProposedTactic 1;
1.393 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1.394 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.395 -
1.396 - fetchProposedTactic 1;
1.397 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.398 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.399 -
1.400 - fetchProposedTactic 1;
1.401 - setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
1.402 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.403 -
1.404 - fetchProposedTactic 1;
1.405 - setNextTactic 1 (Check_elementwise "Assumptions");
1.406 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.407 -
1.408 - val xml = fetchProposedTactic 1;
1.409 - setNextTactic 1 (Check_Postcond
1.410 - ["sqroot-test", "univariate", "equation", "test"]);
1.411 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.412 -
1.413 - val ((pt,_),_) = States.get_calc 1;
1.414 - val str = pr_ctree pr_short pt;
1.415 - writeln str;
1.416 - val ip = States.get_pos 1 1;
1.417 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
1.418 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.419 - if UnparseC.term f = "[x = 1]" then () else
1.420 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.421 -(**)-------------------------------------------------------------------------------------------*)
1.422 - DEconstrCalcTree 1;
1.423 -
1.424 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.425 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.426 -"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
1.427 -(*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
1.428 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.429 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.430 - ["Test", "squ-equ-test-subpbl1"]))];
1.431 - Iterator 1;
1.432 - moveActiveRoot 1;
1.433 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.434 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.435 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.436 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.437 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.438 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.439 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.440 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.441 - (*here the solve-phase starts*)
1.442 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.443 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.444 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.445 - (*------------------------------------*)
1.446 -(* (*default_print_depth 13*) States.get_calc 1;
1.447 - *)
1.448 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.449 - (*calc-head of subproblem*)
1.450 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.451 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.452 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.453 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.454 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.455 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.456 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.457 - (*solve-phase of the subproblem*)
1.458 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.459 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.460 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.461 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.462 - (*finish subproblem*)
1.463 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.464 - (*finish problem*)
1.465 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.466 -
1.467 - (*this checks the test for correctness..*)
1.468 - val ((pt,_),_) = States.get_calc 1;
1.469 - val p = States.get_pos 1 1;
1.470 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.471 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.472 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.473 - DEconstrCalcTree 1;
1.474 -
1.475 -
1.476 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.477 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.478 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.479 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.480 - CalcTree @{context}
1.481 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.482 - ("Test",
1.483 - ["LINEAR", "univariate", "equation", "test"],
1.484 - ["Test", "solve_linear"]))];
1.485 - Iterator 1;
1.486 - moveActiveRoot 1;
1.487 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
1.488 -
1.489 - autoCalculate 1 CompleteCalc;
1.490 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.491 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.492 -
1.493 - val ((pt,_),_) = States.get_calc 1;
1.494 - val p = States.get_pos 1 1;
1.495 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.496 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.497 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.498 -DEconstrCalcTree 1;
1.499 -
1.500 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.501 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.502 -"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
1.503 -(* ERROR: error in kernel ?? *)
1.504 - CalcTree @{context}
1.505 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.506 - ("Test",
1.507 - ["LINEAR", "univariate", "equation", "test"],
1.508 - ["Test", "solve_linear"]))];
1.509 - Iterator 1;
1.510 - moveActiveRoot 1;
1.511 -
1.512 - autoCalculate 1 CompleteCalcHead;
1.513 - refFormula 1 (States.get_pos 1 1);
1.514 - val ((pt,p),_) = States.get_calc 1;
1.515 -
1.516 - autoCalculate 1 CompleteCalc;
1.517 - val ((pt,p),_) = States.get_calc 1;
1.518 - if p=([], Res) then () else
1.519 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
1.520 -DEconstrCalcTree 1;
1.521 -
1.522 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.523 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.524 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.525 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.526 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.527 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.528 - ["Test", "squ-equ-test-subpbl1"]))];
1.529 - Iterator 1;
1.530 - moveActiveRoot 1;
1.531 - autoCalculate 1 CompleteCalc;
1.532 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.533 -(*
1.534 -getTactic 1 ([1],Frm);
1.535 -getTactic 1 ([1],Res);
1.536 -initContext 1 Ptool.Thy_ ([1],Res);
1.537 -*)
1.538 - (*... returns calcChangedEvent with*)
1.539 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.540 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
1.541 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.542 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.543 -
1.544 - val ((pt,_),_) = States.get_calc 1;
1.545 - val p = States.get_pos 1 1;
1.546 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.547 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.548 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.549 - DEconstrCalcTree 1;
1.550 -
1.551 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.552 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.553 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.554 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.555 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.556 - ["Test", "squ-equ-test-subpbl1"]))];
1.557 - Iterator 1;
1.558 - moveActiveRoot 1;
1.559 - autoCalculate 1 CompleteCalcHead;
1.560 -
1.561 -val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
1.562 - meth, probl,
1.563 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.564 - ["Test", "squ-equ-test-subpbl1"]),
1.565 - branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
1.566 - ([], Met)), []) = States.get_calc 1;
1.567 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.568 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.569 -DEconstrCalcTree 1;
1.570 -
1.571 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.572 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.573 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.574 -States.reset ();
1.575 - CalcTree @{context}
1.576 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.577 - ("Test",
1.578 - ["LINEAR", "univariate", "equation", "test"],
1.579 - ["Test", "solve_linear"]))];
1.580 - Iterator 1;
1.581 - moveActiveRoot 1;
1.582 - autoCalculate 1 CompleteModel;
1.583 - refFormula 1 (States.get_pos 1 1);
1.584 -
1.585 -setProblem 1 ["LINEAR", "univariate", "equation", "test"];
1.586 -val pos = States.get_pos 1 1;
1.587 -(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
1.588 - refFormula 1 (States.get_pos 1 1);
1.589 -
1.590 -setMethod 1 ["Test", "solve_linear"];
1.591 -(*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
1.592 - refFormula 1 (States.get_pos 1 1);
1.593 - val ((pt,_),_) = States.get_calc 1;
1.594 - if get_obj g_spec pt [] = (ThyC.id_empty,
1.595 - ["LINEAR", "univariate", "equation", "test"],
1.596 - ["Test", "solve_linear"]) then ()
1.597 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
1.598 -
1.599 - autoCalculate 1 CompleteCalcHead;
1.600 - refFormula 1 (States.get_pos 1 1);
1.601 - autoCalculate 1 CompleteCalc;
1.602 - moveActiveDown 1;
1.603 - moveActiveDown 1;
1.604 - moveActiveDown 1;
1.605 - refFormula 1 (States.get_pos 1 1);
1.606 - val ((pt,_),_) = States.get_calc 1;
1.607 - val p = States.get_pos 1 1;
1.608 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.609 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.610 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.611 - DEconstrCalcTree 1;
1.612 -
1.613 -"--------- setContext..Thy ------------------------------";
1.614 -"--------- setContext..Thy ------------------------------";
1.615 -"--------- setContext..Thy ------------------------------";
1.616 -States.reset ();
1.617 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.618 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.619 - ["Test", "squ-equ-test-subpbl1"]))];
1.620 - Iterator 1; moveActiveRoot 1;
1.621 - autoCalculate 1 CompleteCalcHead;
1.622 - autoCalculate 1 (Steps 1);
1.623 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
1.624 - (*
1.625 - setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
1.626 - autoCalculate 1 (Steps 1);
1.627 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.628 - *)
1.629 -"----- \<up> ^^ and vvvvv do the same -----";
1.630 -(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
1.631 - val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
1.632 -
1.633 - autoCalculate 1 (Steps 1);
1.634 -(*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
1.635 - val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.636 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.637 - if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
1.638 - then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
1.639 -
1.640 - autoCalculate 1 CompleteCalc;
1.641 - val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
1.642 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.643 -
1.644 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
1.645 - else error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.646 - DEconstrCalcTree 1;
1.647 -
1.648 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.649 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.650 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.651 -States.reset ();
1.652 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.653 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.654 - ["Test", "squ-equ-test-subpbl1"]))];
1.655 - Iterator 1; moveActiveRoot 1;
1.656 - autoCalculate 1 CompleteToSubpbl;
1.657 - refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
1.658 - val ((pt,_),_) = States.get_calc 1;
1.659 - val str = pr_ctree pr_short pt;
1.660 - writeln str;
1.661 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
1.662 - then () else
1.663 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl- 1";
1.664 -
1.665 - autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
1.666 - autoCalculate 1 CompleteToSubpbl;
1.667 - val ((pt,_),_) = States.get_calc 1;
1.668 - val str = pr_ctree pr_short pt;
1.669 - writeln str;
1.670 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.671 - val ((pt,_),_) = States.get_calc 1;
1.672 - val p = States.get_pos 1 1;
1.673 -
1.674 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.675 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.676 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.677 - DEconstrCalcTree 1;
1.678 -
1.679 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.680 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.681 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.682 -"--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
1.683 -(*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
1.684 - ---- rat-eq + subpbl: set_found in check_tac1 ----*)
1.685 - CalcTree @{context}
1.686 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
1.687 - ((** )"RatEq"( **)"PolyEq"(*required for "make_ratpoly_in"*),
1.688 - ["univariate", "equation"], ["no_met"]))];
1.689 - Iterator 1;
1.690 - moveActiveRoot 1;
1.691 - fetchProposedTactic 1;
1.692 -
1.693 - setNextTactic 1 (Model_Problem);
1.694 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.695 -
1.696 - setNextTactic 1 (Specify_Theory "RatEq");
1.697 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.698 - setNextTactic 1 (Specify_Problem ["rational", "univariate", "equation"]);
1.699 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.700 - setNextTactic 1 (Specify_Method ["RatEq", "solve_rat_equation"]);
1.701 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.702 - setNextTactic 1 (Apply_Method ["RatEq", "solve_rat_equation"]);
1.703 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.704 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.705 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.706 - setNextTactic 1 (Rewrite_Set "norm_Rational");
1.707 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.708 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.709 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.710 - (* __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)
1.711 - setNextTactic 1 (Subproblem ("PolyEq", ["normalise", "polynomial",
1.712 - "univariate", "equation"]));
1.713 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.714 - setNextTactic 1 (Model_Problem );
1.715 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.716 - setNextTactic 1 (Specify_Theory "PolyEq");
1.717 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.718 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.719 - "univariate", "equation"]);
1.720 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.721 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.722 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.723 - setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1.724 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.725 - setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
1.726 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.727 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
1.728 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.729 - (* __________ for "16 + 12 * x = 0"*)
1.730 - setNextTactic 1 (Subproblem ("PolyEq",
1.731 - ["degree_1", "polynomial", "univariate", "equation"]));
1.732 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.733 - setNextTactic 1 (Model_Problem );
1.734 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.735 - setNextTactic 1 (Specify_Theory "PolyEq");
1.736 - (*------------- some trials in the problem-hierarchy ---------------*)
1.737 - setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation"]);
1.738 - autoCalculate 1 (Steps 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.739 - setNextTactic 1 (Refine_Problem ["univariate", "equation"]);
1.740 - (*------------------------------------------------------------------*)
1.741 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.742 - setNextTactic 1 (Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1.743 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.744 - setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
1.745 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.746 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
1.747 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.748 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.749 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.750 - setNextTactic 1 Or_to_List;
1.751 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.752 - setNextTactic 1 (Check_elementwise "Assumptions");
1.753 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.754 - setNextTactic 1 (Check_Postcond ["degree_1", "polynomial",
1.755 - "univariate", "equation"]);
1.756 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.757 - setNextTactic 1 (Check_Postcond ["normalise", "polynomial",
1.758 - "univariate", "equation"]);
1.759 - autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.760 - setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
1.761 - val (ptp,_) = States.get_calc 1;
1.762 - val (Form t,_,_) = ME_Misc.pt_extract ptp;
1.763 - if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
1.764 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.765 - DEconstrCalcTree 1;
1.766 -
1.767 -
1.768 -\<close> ML \<open>
1.769 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.770 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.771 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.772 -(*{\bf\UC{Having \isac{} Refine the Problem
1.773 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.774 - * x \<up>2 + 4*x + 5 = 2
1.775 -see isac.bridge.TestSpecify#testMatchRefine*)
1.776 -States.reset ();
1.777 - CalcTree @{context}
1.778 - [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
1.779 - ("Isac_Knowledge",
1.780 - ["univariate", "equation"],
1.781 - ["no_met"]))];
1.782 - Iterator 1;
1.783 - moveActiveRoot 1;
1.784 -
1.785 - fetchProposedTactic 1;
1.786 - setNextTactic 1 (Model_Problem );
1.787 - (*..this tactic should be done 'tacitly', too !*)
1.788 -
1.789 -(*
1.790 -autoCalculate 1 CompleteCalcHead;
1.791 -checkContext 1 ([],Pbl) "pbl_equ_univ";
1.792 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1.793 -*)
1.794 -
1.795 - autoCalculate 1 (Steps 1);
1.796 -
1.797 - fetchProposedTactic 1;
1.798 - setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");
1.799 - autoCalculate 1 (Steps 1);
1.800 -
1.801 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.802 -(*initContext 1 Ptool.Pbl_ ([],Pbl);*)
1.803 -(* this would break if a calculation would be inserted before: CALCID...
1.804 - and pattern matching is not available in *.java.
1.805 -if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
1.806 -then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
1.807 -*)
1.808 -(*initContext 1 Ptool.Met_ ([],Pbl);*)
1.809 -(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
1.810 -
1.811 - "--------- this match will show some incomplete items: ---------";
1.812 -
1.813 -(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
1.814 -checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
1.815 -
1.816 -
1.817 - fetchProposedTactic 1;
1.818 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
1.819 -
1.820 - fetchProposedTactic 1;
1.821 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
1.822 -
1.823 - "--------- this is a matching model (all items correct): -------";
1.824 -(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);*)
1.825 - "--------- this is a NOT matching model (some 'false': ---------";
1.826 -(*checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)
1.827 -
1.828 - "--------- find out a matching problem: ------------------------";
1.829 - "--------- find out a matching problem (FAILING: no new pbl) ---";
1.830 - refineProblem 1 ([],Pbl)(Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"]);
1.831 -
1.832 - "--------- find out a matching problem (SUCCESSFUL) ------------";
1.833 - refineProblem 1 ([],Pbl) (Ptool.pblID2guh @{context} ["univariate", "equation"]);
1.834 -
1.835 - "--------- tryMatch, tryRefine did not change the calculation -";
1.836 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1.837 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.838 - "univariate", "equation"]);
1.839 - autoCalculate 1 (Steps 1);
1.840 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
1.841 - and Specify_Theory skipped in comparison to below --- \<up> -inserted *)
1.842 -(*------------vvv-inserted-----------------------------------------------*)
1.843 - fetchProposedTactic 1;
1.844 -(*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )
1.845 - setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
1.846 - "univariate", "equation"]);
1.847 - autoCalculate 1 (Steps 1);
1.848 -
1.849 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1.850 -
1.851 - fetchProposedTactic 1;
1.852 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.853 - autoCalculate 1 (Steps 1);
1.854 -
1.855 - fetchProposedTactic 1;
1.856 - setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
1.857 -
1.858 - autoCalculate 1 CompleteCalc;
1.859 -
1.860 - val ((pt,_),_) = States.get_calc 1;
1.861 - Test_Tool.show_pt pt;
1.862 - val p = States.get_pos 1 1;
1.863 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.864 - if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.865 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.866 -
1.867 -(*------------ \<up> -inserted-----------------------------------------------*)
1.868 -(*WN050904 the fetchProposedTactic's below may not have worked like that
1.869 - before, too, because there was no check*)
1.870 - fetchProposedTactic 1;
1.871 - setNextTactic 1 (Specify_Theory "PolyEq");
1.872 - autoCalculate 1 (Steps 1);
1.873 -
1.874 - fetchProposedTactic 1;
1.875 - setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
1.876 - autoCalculate 1 (Steps 1);
1.877 -
1.878 - fetchProposedTactic 1;
1.879 - "--------- now the calc-header is ready for enter 'solving' ----";
1.880 - autoCalculate 1 CompleteCalc;
1.881 -
1.882 - val ((pt,_),_) = States.get_calc 1;
1.883 - rootthy pt;
1.884 - Test_Tool.show_pt pt;
1.885 - val p = States.get_pos 1 1;
1.886 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.887 - if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
1.888 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.889 - DEconstrCalcTree 1;
1.890 -( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)
1.891 -
1.892 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.893 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.894 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.895 -States.reset ();
1.896 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.897 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.898 - ["Test", "squ-equ-test-subpbl1"]))];
1.899 - Iterator 1;
1.900 - moveActiveRoot 1;
1.901 -
1.902 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1.903 - "solve (x+1=2, x)",(*the headline*)
1.904 - [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
1.905 - P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
1.906 - Pbl,
1.907 - ("Test",
1.908 - ["sqroot-test", "univariate", "equation", "test"],
1.909 - ["Test", "squ-equ-test-subpbl1"]));
1.910 -
1.911 -val ((Nd (PblObj {fmz = (fm, tpm),
1.912 - loc = (SOME scrst_ctxt, NONE),
1.913 - ctxt,
1.914 - meth,
1.915 - spec = (thy,
1.916 - ["sqroot-test", "univariate", "equation", "test"],
1.917 - ["Test", "squ-equ-test-subpbl1"]),
1.918 - probl,
1.919 - branch = TransitiveB,
1.920 - origin,
1.921 - ostate = Incomplete,
1.922 - result},
1.923 - []),
1.924 - ([], Pbl)),
1.925 - []) = States.get_calc 1;
1.926 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
1.927 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1.928 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
1.929 -
1.930 -resetCalcHead 1;
1.931 -modelProblem 1;
1.932 -
1.933 -States.get_calc 1;
1.934 -val ((Nd (PblObj {fmz = (fm, tpm),
1.935 - loc = (SOME scrst_ctxt, NONE),
1.936 - ctxt,
1.937 - meth,
1.938 - spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
1.939 - probl,
1.940 - branch = TransitiveB,
1.941 - origin,
1.942 - ostate = Incomplete,
1.943 - result},
1.944 - []),
1.945 - ([], Pbl)),
1.946 - []) = States.get_calc 1;
1.947 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.948 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
1.949 -
1.950 -"--------- maximum-example, UC: Modeling an example -----";
1.951 -"--------- maximum-example, UC: Modeling an example -----";
1.952 -"--------- maximum-example, UC: Modeling an example -----";
1.953 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
1.954 -see isac.bridge.TestModel#testEditItems
1.955 -*)
1.956 - val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
1.957 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.958 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.959 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
1.960 - (* \<up> these are the elements for the root-problem (in variants)*)
1.961 - (*vvv these are elements required for subproblems*)
1.962 - "boundVariable a", "boundVariable b", "boundVariable alpha",
1.963 - "interval {x::real. 0 <= x & x <= 2*r}",
1.964 - "interval {x::real. 0 <= x & x <= 2*r}",
1.965 - "interval {x::real. 0 <= x & x <= pi}",
1.966 - "errorBound (eps=(0::real))"]
1.967 - (*specifying is not interesting for this example*)
1.968 - val spec = ("Diff_App", ["maximum_of", "function"],
1.969 - ["Diff_App", "max_by_calculus"]);
1.970 - (*the empty model with descriptions for user-guidance by Model_Problem*)
1.971 - val empty_model = [P_Spec.Given ["fixedValues []"],
1.972 - P_Spec.Find ["maximum", "valuesFor"],
1.973 - P_Spec.Relate ["relations []"]];
1.974 - DEconstrCalcTree 1;
1.975 -
1.976 -"#################################################################";
1.977 -States.reset ();
1.978 - CalcTree @{context} [(elems, spec)];
1.979 - Iterator 1;
1.980 - moveActiveRoot 1;
1.981 - refFormula 1 (States.get_pos 1 1);
1.982 - (*this gives a completely empty model*)
1.983 -
1.984 - fetchProposedTactic 1;
1.985 -(*fill the CalcHead with Descriptions...*)
1.986 - setNextTactic 1 (Model_Problem );
1.987 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.988 -
1.989 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1.990 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1.991 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
1.992 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
1.993 - "Problem (Diff_App.thy, [maximum_of, function])",
1.994 - (*the head-form \<up> is not used for input here*)
1.995 - [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
1.996 - P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
1.997 - P_Spec.Relate ["relations"]],
1.998 - (*input (Arbfix will dissappear soon)*)
1.999 - Pbl (*belongsto*),
1.1000 - References.empty (*no input to the specification*));
1.1001 -
1.1002 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
1.1003 - and asks what to do next*)
1.1004 - fetchProposedTactic 1;
1.1005 - (*the student follows the advice*)
1.1006 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1.1007 - autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
1.1008 -
1.1009 - (*this input completes the model*)
1.1010 - modifyCalcHead 1 (([],Pbl), "not used here",
1.1011 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1012 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1013 - P_Spec.Relate ["relations [A=a*b, \
1.1014 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);
1.1015 -
1.1016 - (*specification is not interesting and should be skipped by the dialogguide;
1.1017 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1.1018 - modifyCalcHead 1 (([],Pbl), "not used here",
1.1019 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1020 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1021 - P_Spec.Relate ["relations [A=a*b, \
1.1022 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1023 - ("Diff_App", Problem.id_empty, MethodC.id_empty));
1.1024 - modifyCalcHead 1 (([],Pbl), "not used here",
1.1025 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1026 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1027 - P_Spec.Relate ["relations [A=a*b, \
1.1028 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1029 - ("Diff_App", ["maximum_of", "function"],
1.1030 - MethodC.id_empty));
1.1031 - modifyCalcHead 1 (([],Pbl), "not used here",
1.1032 - [P_Spec.Given ["fixedValues [r=Arbfix]"],
1.1033 - P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.1034 - P_Spec.Relate ["relations [A=a*b, \
1.1035 - \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
1.1036 - ("Diff_App", ["maximum_of", "function"],
1.1037 - ["Diff_App", "max_by_calculus"]));
1.1038 - (*this final calcHead now has STATUS 'complete' !*)
1.1039 - DEconstrCalcTree 1;
1.1040 -
1.1041 -(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
1.1042 -"--------- solve_linear from pbl-hierarchy --------------";
1.1043 -"--------- solve_linear from pbl-hierarchy --------------";
1.1044 -"--------- solve_linear from pbl-hierarchy --------------";
1.1045 -States.reset ();
1.1046 - val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
1.1047 - CalcTree @{context} [(fmz, sp)];
1.1048 - Iterator 1; moveActiveRoot 1;
1.1049 - refFormula 1 (States.get_pos 1 1);
1.1050 - modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
1.1051 - [P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
1.1052 - P_Spec.Find ["solutions L"]],
1.1053 - Pbl,
1.1054 - ("Test", ["LINEAR", "univariate", "equation", "test"],
1.1055 - ["Test", "solve_linear"]));
1.1056 - autoCalculate 1 CompleteCalc;
1.1057 - refFormula 1 (States.get_pos 1 1);
1.1058 - val ((pt,_),_) = States.get_calc 1;
1.1059 - val p = States.get_pos 1 1;
1.1060 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1061 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.1062 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
1.1063 - DEconstrCalcTree 1;
1.1064 -
1.1065 -"--------- solve_linear as in an algebra system (CAS)----";
1.1066 -"--------- solve_linear as in an algebra system (CAS)----";
1.1067 -"--------- solve_linear as in an algebra system (CAS)----";
1.1068 -(*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
1.1069 -States.reset ();
1.1070 - val (fmz, sp) = ([], ("", [], []));
1.1071 - CalcTree @{context} [(fmz, sp)];
1.1072 - Iterator 1; moveActiveRoot 1;
1.1073 - modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
1.1074 - autoCalculate 1 CompleteCalc;
1.1075 - refFormula 1 (States.get_pos 1 1);
1.1076 - val ((pt,_),_) = States.get_calc 1;
1.1077 - val p = States.get_pos 1 1;
1.1078 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1079 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1.1080 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
1.1081 -DEconstrCalcTree 1;
1.1082 -*)
1.1083 -
1.1084 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1085 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1086 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.1087 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1088 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1089 - ["Test", "squ-equ-test-subpbl1"]))];
1.1090 - Iterator 1;
1.1091 - moveActiveRoot 1;
1.1092 - autoCalculate 1 CompleteCalc;
1.1093 - val ((pt,_),_) = States.get_calc 1;
1.1094 - Test_Tool.show_pt pt;
1.1095 -
1.1096 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1097 - interSteps 1 ([2],Res);
1.1098 - val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1.1099 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1.1100 - getFormulaeFromTo 1 unc gen 1 false;
1.1101 -
1.1102 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1103 - interSteps 1 ([3,2],Res);
1.1104 - val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1.1105 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1.1106 - getFormulaeFromTo 1 unc gen 1 false;
1.1107 -
1.1108 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1109 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
1.1110 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1.1111 - getFormulaeFromTo 1 unc gen 1 false;
1.1112 -
1.1113 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1114 - interSteps 1 ([],Res) (*no new steps in subproblems*);
1.1115 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1.1116 - getFormulaeFromTo 1 unc gen 1 false;
1.1117 -DEconstrCalcTree 1;
1.1118 -
1.1119 -"--------- getTactic, fetchApplicableTactics ------------";
1.1120 -"--------- getTactic, fetchApplicableTactics ------------";
1.1121 -"--------- getTactic, fetchApplicableTactics ------------";
1.1122 -(* compare test/../script.sml
1.1123 -"----------- fun from_prog ---------------------------------------";
1.1124 -*)
1.1125 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1126 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1127 - ["Test", "squ-equ-test-subpbl1"]))];
1.1128 - Iterator 1; moveActiveRoot 1;
1.1129 - autoCalculate 1 CompleteCalc;
1.1130 - val ((pt,_),_) = States.get_calc 1;
1.1131 - Test_Tool.show_pt pt;
1.1132 -
1.1133 - (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1.1134 -WN120210 not impl. in FE*)
1.1135 - getTactic 1 ([],Pbl);
1.1136 - getTactic 1 ([1],Res);
1.1137 - getTactic 1 ([3],Pbl);
1.1138 - getTactic 1 ([3,1],Frm);
1.1139 - getTactic 1 ([3],Res);
1.1140 - getTactic 1 ([],Res);
1.1141 -
1.1142 -(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.1143 - fetchApplicableTactics 1 99999 ([],Pbl);
1.1144 - fetchApplicableTactics 1 99999 ([1],Res);
1.1145 - fetchApplicableTactics 1 99999 ([3],Pbl);
1.1146 - fetchApplicableTactics 1 99999 ([3,1],Res);
1.1147 - fetchApplicableTactics 1 99999 ([3],Res);
1.1148 - fetchApplicableTactics 1 99999 ([],Res);
1.1149 -DEconstrCalcTree 1;
1.1150 -
1.1151 -(*SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\* )
1.1152 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1153 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1154 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1155 -States.reset ();
1.1156 -CalcTree @{context}
1.1157 -[(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
1.1158 - "solveFor x", "solutions L"],
1.1159 - ("RatEq",["univariate", "equation"],["no_met"]))];
1.1160 -Iterator 1; moveActiveRoot 1;
1.1161 -autoCalculate 1 CompleteCalc;
1.1162 -val ((pt,_),_) = States.get_calc 1;
1.1163 -val p = States.get_pos 1 1;
1.1164 -val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1165 -(*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
1.1166 -if map UnparseC.term asms =
1.1167 - ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
1.1168 - " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0",
1.1169 - "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
1.1170 - "lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2",
1.1171 - "9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"]
1.1172 -andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()
1.1173 -else error "TODO compare 2002-- 2011"; (*...data during test --- x / (x \<up> 2 - 6 * x + 9) - 1...*)
1.1174 -============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)
1.1175 -
1.1176 -if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
1.1177 -andalso map UnparseC.term asms = []
1.1178 -then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.1179 -
1.1180 -(*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1.1181 -getAssumptions 1 ([3], Res);
1.1182 -getAssumptions 1 ([5], Res);
1.1183 -(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1.1184 - WN0502 still without positions*)
1.1185 -getAccumulatedAsms 1 ([3], Res);
1.1186 -getAccumulatedAsms 1 ([5], Res);
1.1187 -DEconstrCalcTree 1;
1.1188 -( *SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//*)
1.1189 -
1.1190 -\<close> ML \<open>
1.1191 -"--------- arbitrary combinations of steps --------------";
1.1192 -"--------- arbitrary combinations of steps --------------";
1.1193 -"--------- arbitrary combinations of steps --------------";
1.1194 - CalcTree @{context} (*start of calculation, return No.1*)
1.1195 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
1.1196 - ("Test",
1.1197 - ["LINEAR", "univariate", "equation", "test"],
1.1198 - ["Test", "solve_linear"]))];
1.1199 - Iterator 1; moveActiveRoot 1;
1.1200 -
1.1201 - fetchProposedTactic 1;
1.1202 - (*ERROR States.get_calc 1 not existent*)
1.1203 - setNextTactic 1 (Model_Problem );
1.1204 - autoCalculate 1 (Steps 1);
1.1205 - fetchProposedTactic 1;
1.1206 - fetchProposedTactic 1;
1.1207 -
1.1208 - setNextTactic 1 (Add_Find "solutions L");
1.1209 - setNextTactic 1 (Add_Find "solutions L");
1.1210 -
1.1211 - autoCalculate 1 (Steps 1);
1.1212 - autoCalculate 1 (Steps 1);
1.1213 -
1.1214 - setNextTactic 1 (Specify_Theory "Test");
1.1215 - fetchProposedTactic 1;
1.1216 - autoCalculate 1 (Steps 1);
1.1217 -
1.1218 - autoCalculate 1 (Steps 1);
1.1219 - autoCalculate 1 (Steps 1);
1.1220 - autoCalculate 1 (Steps 1);
1.1221 - autoCalculate 1 (Steps 1);
1.1222 -(*------------------------- end calc-head*)
1.1223 -
1.1224 - fetchProposedTactic 1;
1.1225 - setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1.1226 - autoCalculate 1 (Steps 1);
1.1227 -
1.1228 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.1229 - fetchProposedTactic 1;
1.1230 - autoCalculate 1 (Steps 1);
1.1231 -
1.1232 - autoCalculate 1 CompleteCalc;
1.1233 - val ((pt,_),_) = States.get_calc 1;
1.1234 - val p = States.get_pos 1 1;
1.1235 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1236 - if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1.1237 - error "FE-interface.sml: diff.behav. in combinations of steps";
1.1238 -DEconstrCalcTree 1;
1.1239 -
1.1240 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1.1241 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1242 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1243 -States.reset ();
1.1244 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1245 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1246 - ["Test", "squ-equ-test-subpbl1"]))];
1.1247 - Iterator 1;
1.1248 - moveActiveRoot 1;
1.1249 - autoCalculate 1 CompleteCalcHead;
1.1250 - autoCalculate 1 (Steps 1);
1.1251 - autoCalculate 1 (Steps 1);
1.1252 - appendFormula 1 "- 1 + x = 0" (*|> Future.join*);
1.1253 - (*... returns calcChangedEvent with*)
1.1254 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1255 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1256 -
1.1257 - val ((pt,_),_) = States.get_calc 1;
1.1258 - val p = States.get_pos 1 1;
1.1259 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1260 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1261 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1.1262 -DEconstrCalcTree 1;
1.1263 -
1.1264 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1.1265 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1266 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1267 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1268 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1269 - ["Test", "squ-equ-test-subpbl1"]))];
1.1270 - Iterator 1;
1.1271 - moveActiveRoot 1;
1.1272 - autoCalculate 1 CompleteCalcHead;
1.1273 - autoCalculate 1 (Steps 1);
1.1274 - autoCalculate 1 (Steps 1);
1.1275 - appendFormula 1 "x - 1 = 0" (*|> Future.join*);
1.1276 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1277 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1278 - (*11 elements !!!*)
1.1279 -
1.1280 - val ((pt,_),_) = States.get_calc 1;
1.1281 - val p = States.get_pos 1 1;
1.1282 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1283 - if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1284 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1.1285 -DEconstrCalcTree 1;
1.1286 -
1.1287 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1.1288 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1289 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1290 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1291 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1292 - ["Test", "squ-equ-test-subpbl1"]))];
1.1293 - Iterator 1;
1.1294 - moveActiveRoot 1;
1.1295 - autoCalculate 1 CompleteCalcHead;
1.1296 - autoCalculate 1 (Steps 1);
1.1297 - autoCalculate 1 (Steps 1);
1.1298 - appendFormula 1 "x = 1" (*|> Future.join*);
1.1299 - (*... returns calcChangedEvent with*)
1.1300 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1.1301 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1302 - (*6 elements !!!*)
1.1303 -
1.1304 - val ((pt,_),_) = States.get_calc 1;
1.1305 - val p = States.get_pos 1 1;
1.1306 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1307 - if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.1308 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.1309 -DEconstrCalcTree 1;
1.1310 -
1.1311 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1.1312 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1313 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1314 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1315 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1316 - ["Test", "squ-equ-test-subpbl1"]))];
1.1317 - Iterator 1;
1.1318 - moveActiveRoot 1;
1.1319 - autoCalculate 1 CompleteCalcHead;
1.1320 - autoCalculate 1 (Steps 1);
1.1321 - autoCalculate 1 (Steps 1);
1.1322 - appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
1.1323 - (*... returns <ERROR> no derivation found </ERROR>*)
1.1324 -
1.1325 - val ((pt,_),_) = States.get_calc 1;
1.1326 - val p = States.get_pos 1 1;
1.1327 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1328 - if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
1.1329 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1.1330 -DEconstrCalcTree 1;
1.1331 -
1.1332 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1.1333 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1334 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1335 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1336 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1337 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1338 - ["Test", "squ-equ-test-subpbl1"]))];
1.1339 - Iterator 1;
1.1340 - moveActiveRoot 1;
1.1341 - autoCalculate 1 CompleteCalc;
1.1342 - moveActiveFormula 1 ([2],Res);
1.1343 - replaceFormula 1 "- 1 + x = 0" (*i.e. repeats input*);
1.1344 - (*... returns <ERROR> formula not changed </ERROR>*)
1.1345 -
1.1346 - val ((pt,_),_) = States.get_calc 1;
1.1347 - val p = States.get_pos 1 1;
1.1348 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1349 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1350 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1351 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.1352 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1353 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1354 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.1355 -
1.1356 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.1357 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1358 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1359 - ["Test", "squ-equ-test-subpbl1"]))];
1.1360 - Iterator 2; (*! ! ! 1 CalcTree @{context} inbetween States.reset (); *)
1.1361 - moveActiveRoot 2;
1.1362 - autoCalculate 2 CompleteCalc;
1.1363 - moveActiveFormula 2 ([2],Res);
1.1364 - replaceFormula 2 "- 1 + x = 0" (*i.e. repeats input*);
1.1365 - (*... returns <ERROR> formula not changed </ERROR>*)
1.1366 -
1.1367 - val ((pt,_),_) = States.get_calc 2;
1.1368 - val p = States.get_pos 2 1;
1.1369 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1370 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1371 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1372 - if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1.1373 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1374 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1375 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.1376 -DEconstrCalcTree 1;
1.1377 -
1.1378 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1.1379 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1380 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1381 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1382 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1383 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1384 - ["Test", "squ-equ-test-subpbl1"]))];
1.1385 - Iterator 1;
1.1386 - moveActiveRoot 1;
1.1387 - autoCalculate 1 CompleteCalc;
1.1388 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1389 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1.1390 - (*... returns calcChangedEvent with*)
1.1391 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1.1392 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1393 -
1.1394 - val ((pt,_),_) = States.get_calc 1;
1.1395 - Test_Tool.show_pt pt;
1.1396 - val p = States.get_pos 1 1;
1.1397 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1398 - if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1399 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1.1400 -(* for getting the list in whole length ...
1.1401 -(*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1.1402 - *)
1.1403 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.1404 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1405 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1.1406 - ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
1.1407 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1.1408 -DEconstrCalcTree 1;
1.1409 -
1.1410 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1.1411 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1412 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1413 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1414 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1415 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1416 - ["Test", "squ-equ-test-subpbl1"]))];
1.1417 - Iterator 1;
1.1418 - moveActiveRoot 1;
1.1419 - autoCalculate 1 CompleteCalc;
1.1420 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1421 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1.1422 - (*... returns calcChangedEvent with ...*)
1.1423 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1.1424 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1425 - (*9 elements !!!*)
1.1426 -
1.1427 - val ((pt,_),_) = States.get_calc 1;
1.1428 - Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
1.1429 - val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
1.1430 - if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1.1431 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1.1432 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1433 - ([3,2],Res)] then () else
1.1434 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1.1435 -
1.1436 - val p = States.get_pos 1 1;
1.1437 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1438 - if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1.1439 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1.1440 -DEconstrCalcTree 1;
1.1441 -
1.1442 -\<close> ML \<open>
1.1443 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1.1444 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1445 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1446 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1447 - CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.1448 - ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.1449 - ["Test", "squ-equ-test-subpbl1"]))];
1.1450 - Iterator 1;
1.1451 - moveActiveRoot 1;
1.1452 - autoCalculate 1 CompleteCalc;
1.1453 - moveActiveFormula 1 ([2],Res); (*there is "- 1 + x = 0"*)
1.1454 - replaceFormula 1 "x - 4711 = 0";
1.1455 - (*... returns <ERROR> no derivation found </ERROR>*)
1.1456 -
1.1457 - val ((pt,_),_) = States.get_calc 1;
1.1458 - Test_Tool.show_pt pt;
1.1459 - val p = States.get_pos 1 1;
1.1460 - val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1.1461 - if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
1.1462 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.1463 - DEconstrCalcTree 1;
1.1464 -
1.1465 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1466 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1467 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1468 -CalcTree @{context}
1.1469 -[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.1470 - ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.1471 -Iterator 1;
1.1472 -moveActiveRoot 1;
1.1473 -autoCalculate 1 CompleteCalcHead;
1.1474 -autoCalculate 1 (Steps 1);
1.1475 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
1.1476 -appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.1477 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.1478 - would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1.1479 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.1480 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.1481 - val ((pt,pos), _) = States.get_calc 1;
1.1482 - val p = States.get_pos 1 1;
1.1483 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1484 -
1.1485 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.1486 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1.1487 - ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
1.1488 - | _ => error "embed fun fill_form changed 1"
1.1489 -else error "embed fun fill_form changed 2";
1.1490 -
1.1491 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.1492 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.1493 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
1.1494 - d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.1495 - val ((pt,pos),_) = States.get_calc 1;
1.1496 - val p = States.get_pos 1 1;
1.1497 -
1.1498 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1499 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
1.1500 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1.1501 - then ()
1.1502 - else error "embed fun fill_form changed 2";
1.1503 -
1.1504 -(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1.1505 - and the last has no gaps, then the number of fill-patterns would suffice
1.1506 - for the DialogGuide to select appropriately. *)
1.1507 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.1508 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.1509 - val ((pt,pos),_) = States.get_calc 1;
1.1510 - val p = States.get_pos 1 1;
1.1511 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1512 - if p = ([1], Res) andalso existpt [2] pt andalso
1.1513 - UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
1.1514 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
1.1515 - then () else error "embed fun fill_form changed 3";
1.1516 -
1.1517 -inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
1.1518 - val ((pt, _),_) = States.get_calc 1;
1.1519 - val p = States.get_pos 1 1;
1.1520 - val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1521 - if p = ([2], Res) andalso
1.1522 - UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
1.1523 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
1.1524 - then () else error "inputFillFormula changed 11";
1.1525 -
1.1526 -autoCalculate 1 CompleteCalc;
1.1527 -
1.1528 -"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1.1529 -val ((pt, _),_) = States.get_calc 1;
1.1530 -val p = States.get_pos 1 1;
1.1531 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.1532 -if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
1.1533 -then () else error "inputFillFormula changed 12";
1.1534 -Test_Tool.show_pt pt;
1.1535 -(*[
1.1536 -(([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),
1.1537 -(([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),
1.1538 -(([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),
1.1539 -(([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)), (*<<<<<<<=====*)
1.1540 -(([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1.1541 -(([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
1.1542 -(([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),
1.1543 -(([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)
1.1544 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1.1545 -DEconstrCalcTree 1;
1.1546 -
1.1547 -\<close> ML \<open>
1.1548 -(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
1.1549 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1550 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1551 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1552 -(*cp from BridgeLog Java <=> SML*)
1.1553 -CalcTree @{context} [([], References.empty)];
1.1554 -Iterator 1;
1.1555 -moveActiveRoot 1;
1.1556 -moveActiveFormula 1 ([],Pbl);
1.1557 -replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1.1558 -autoCalculate 1 CompleteCalcHead;
1.1559 -autoCalculate 1 (Steps 1);
1.1560 -appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
1.1561 -(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1.1562 ---- but in BridgeLog Java <=> SML:
1.1563 -<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1.1564 -DEconstrCalcTree 1;
1.1565 ------------------------------------------------------------------------------------------------*)
1.1566 -
1.1567 -\<close> ML \<open>
1.1568 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1569 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1570 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1571 -(*TODO*)
1.1572 -CalcTree @{context}
1.1573 -[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1.1574 - "differentiateFor x", "derivative f_f'"],
1.1575 - ("Isac_Knowledge", ["derivative_of", "function"],
1.1576 - ["diff", "differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1.1577 -Iterator 1;
1.1578 -moveActiveRoot 1;
1.1579 -autoCalculate 1 CompleteCalc;
1.1580 -val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.1581 -DEconstrCalcTree 1;
1.1582 -
1.1583 -\<close> ML \<open>
1.1584 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1585 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1586 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1587 -CalcTree @{context}
1.1588 -[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
1.1589 - "differentiateFor x", "derivative f_f'"],
1.1590 - ("Isac_Knowledge", ["derivative_of", "function"],
1.1591 - ["diff", "after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1.1592 -Iterator 1;
1.1593 -moveActiveRoot 1;
1.1594 -autoCalculate 1 CompleteCalcHead;
1.1595 -autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.1596 -autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1.1597 -(*
1.1598 -<NEXTTAC>
1.1599 - <CALCID> 1 </CALCID>
1.1600 - <TACTICERRORPATTERNS>
1.1601 - <STRINGLIST>
1.1602 - <STRING> chain-rule-diff-both </STRING>
1.1603 - <STRING> cancel </STRING>
1.1604 - </STRINGLIST>
1.1605 - <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1.1606 - <RULESET> norm_diff </RULESET>
1.1607 - <SUBSTITUTION>
1.1608 - <PAIR>
1.1609 - <VARIABLE>
1.1610 - <MATHML>
1.1611 - <ISA> bdv </ISA>
1.1612 - </MATHML>
1.1613 - </VARIABLE>
1.1614 - <VALUE>
1.1615 - <MATHML>
1.1616 - <ISA> x </ISA>
1.1617 - </MATHML>
1.1618 - </VALUE>
1.1619 - </PAIR>
1.1620 - </SUBSTITUTION>
1.1621 - </REWRITESETINSTTACTIC>
1.1622 - </TACTICERRORPATTERNS>
1.1623 -</NEXTTAC>
1.1624 -
1.1625 -
1.1626 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1627 -stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1.1628 -stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1.1629 -(* then --- UC errpat, fillpat by input ---*)
1.1630 -*)
1.1631 -autoCalculate 1 CompleteCalc;
1.1632 -val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.1633 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1634 -DEconstrCalcTree 1;
1.1635 -
1.1636 -\<close> ML \<open>
1.1637 -\<close> ML \<open>
1.1638 -\<close>
1.1639
1.1640 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.1641 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>