1.1 --- a/test/Tools/isac/Frontend/interface.sml Wed Jul 20 13:05:48 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Wed Jul 20 14:55:29 2011 +0200
1.3 @@ -581,20 +581,219 @@
1.4 states:=[];
1.5 CalcTree
1.6 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
1.7 - ("RatEq",
1.8 + ("RatEq", ["univariate","equation"], ["no_met"]))];
1.9 + Iterator 1;
1.10 + moveActiveRoot 1;
1.11 + fetchProposedTactic 1;
1.12
1.13 - val (Form f, tac, asms) = pt_extract (pt, p);
1.14 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.15 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.16 + setNextTactic 1 (Model_Problem);
1.17 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.18
1.19 + setNextTactic 1 (Specify_Theory "RatEq");
1.20 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.21 + setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.22 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.23 + setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.24 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.25 + setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.26 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.27 + setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.28 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.29 + setNextTactic 1 (Rewrite_Set "norm_Rational");
1.30 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.31 + setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.32 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.33 + (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.34 + setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
1.35 + "univariate","equation"]));
1.36 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.37 + setNextTactic 1 (Model_Problem );
1.38 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.39 + setNextTactic 1 (Specify_Theory "PolyEq");
1.40 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.41 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.42 + "univariate","equation"]);
1.43 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.44 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.45 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.46 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.47 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.48 + setNextTactic 1 (Rewrite ("all_left",""));
1.49 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.50 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.51 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.52 + (* __________ for "16 + 12 * x = 0"*)
1.53 + setNextTactic 1 (Subproblem ("PolyEq",
1.54 + ["degree_1","polynomial","univariate","equation"]));
1.55 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.56 + setNextTactic 1 (Model_Problem );
1.57 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.58 + setNextTactic 1 (Specify_Theory "PolyEq");
1.59 + (*------------- some trials in the problem-hierarchy ---------------*)
1.60 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
1.61 + autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.62 + setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.63 + (*------------------------------------------------------------------*)
1.64 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.65 + setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.66 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.67 + setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.68 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.69 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.70 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.71 + setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.72 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.73 + (*==================================================================*)
1.74 + setNextTactic 1 Or_to_List;
1.75 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.76 +(* setNextTactic 1 (Check_elementwise "Assumptions");
1.77 + WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.78 +"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
1.79 +val ((pt, _), _) = get_calc cI;
1.80 +val ip = get_pos cI 1;
1.81 +(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.82 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
1.83 +val (mI,m) = mk_tac'_ tac;
1.84 +val Appl m = applicable_in p pt m;
1.85 +member op = specsteps mI (*false*);
1.86 +(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.87 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
1.88 +(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.89 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.90 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.91 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.92 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.93 + val d = e_rls;
1.94 +(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.95 + WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
1.96 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
1.97 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
1.98 + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
1.99 +val thy = assoc_thy thy';
1.100 +l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
1.101 +(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
1.102 + ... Assoc ... is correct*)
1.103 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
1.104 + ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.105 +1 < length l (*true*);
1.106 +val up = drop_last l;
1.107 + term2str (go up sc);
1.108 + (go up sc);
1.109 +(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
1.110 + ... ???? ... is correct*)
1.111 +"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
1.112 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
1.113 + val l = drop_last l; (*comes from e, goes to Abs*)
1.114 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.115 + val i = mk_Free (i, T);
1.116 + val E = upd_env E (i, v);
1.117 +(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
1.118 +val [(tac_, mout, ptree, pos', xxx)] = ss;
1.119 +val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
1.120 +(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
1.121 + ... Assoc ... is correct*)
1.122 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
1.123 + ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
1.124 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
1.125 + val ctxt = get_ctxt pt (p,p_)
1.126 + val p' = lev_on p : pos;
1.127 +(* WAS val NotAss = assod pt d m stac
1.128 + ... Ass ... is correct*)
1.129 +"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
1.130 + (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
1.131 +consts = consts' (*WAS false*);
1.132 +(*========== inhibit exn 110719 ================================================
1.133 +========== inhibit exn 110719 =============================================*)
1.134 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.135 + setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
1.136 + "univariate","equation"]);
1.137 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.138 + setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.139 + "univariate","equation"]);
1.140 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.141
1.142 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.143 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.144 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.145 - states:=[];
1.146 +(*** exception TYPE raised (line 460 of "old_goals.ML"):
1.147 +*** Type error in application: Incompatible operand type
1.148 +***
1.149 +*** Operator: equality :: bool => una
1.150 +*** Operand: [((x * 3) = -4)] :: bool list
1.151 +***
1.152 +*** bool => una
1.153 +*** bool list
1.154 +*** equality
1.155 +*** [x * 3 = -4]*)
1.156 +
1.157 +(*========== inhibit exn 110719 ================================================
1.158 + setNextTactic 1 (Check_elementwise "Assumptions");
1.159 +============ inhibit exn 110719 ==============================================*)
1.160 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.161 + setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
1.162 + val (ptp,_) = get_calc 1;
1.163 + val (Form t,_,_) = pt_extract ptp;
1.164 + if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.165 + else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.166 +
1.167 +
1.168 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.169 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.170 +"--------- tryMatchProblem, tryRefineProblem ------------";
1.171 +(*{\bf\UC{Having \isac{} Refine the Problem
1.172 + * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.173 + * x^^^2 + 4*x + 5 = 2
1.174 +see isac.bridge.TestSpecify#testMatchRefine*)
1.175 + DEconstrCalcTree 1;
1.176 CalcTree
1.177 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
1.178 - ("RatEq", ["univariate","equation"], ["no_met"]))];
1.179 + [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
1.180 + ("Isac",
1.181 + ["univariate","equation"],
1.182 + ["no_met"]))];
1.183 + Iterator 1;
1.184 + moveActiveRoot 1;
1.185 +
1.186 + fetchProposedTactic 1;
1.187 + setNextTactic 1 (Model_Problem );
1.188 + (*..this tactic should be done 'tacitly', too !*)
1.189 +
1.190 +(*
1.191 +autoCalculate 1 CompleteCalcHead;
1.192 +checkContext 1 ([],Pbl) "pbl_equ_univ";
1.193 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.194 +*)
1.195 +
1.196 + autoCalculate 1 (Step 1);
1.197 +
1.198 + fetchProposedTactic 1;
1.199 + setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
1.200 + autoCalculate 1 (Step 1);
1.201 +
1.202 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.203 +initContext 1 Pbl_ ([],Pbl);
1.204 +initContext 1 Met_ ([],Pbl);
1.205 +
1.206 + "--------- this match will show some incomplete items: ---------";
1.207 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.208 +checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.209 +
1.210 +
1.211 + fetchProposedTactic 1;
1.212 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
1.213 +
1.214 + fetchProposedTactic 1;
1.215 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
1.216 +
1.217 + "--------- this is a matching model (all items correct): -------";
1.218 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.219 + "--------- this is a NOT matching model (some 'false': ---------";
1.220 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
1.221 +
1.222 + "--------- find out a matching problem: ------------------------";
1.223 + "--------- find out a matching problem (FAILING: no new pbl) ---";
1.224 + refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
1.225 +
1.226 + "--------- find out a matching problem (SUCCESSFUL) ------------";
1.227 + refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
1.228 +
1.229 + "--------- tryMatch, tryRefine di [univariate,equation], [no_met]))]";
1.230 Iterator 1;
1.231 moveActiveRoot 1;
1.232 fetchProposedTactic 1;
1.233 @@ -727,211 +926,8 @@
1.234 *** equality
1.235 *** [x * 3 = -4]*)
1.236
1.237 + setNextTactic 1 (Check_elementwise "Assumptions");
1.238 (*========== inhibit exn 110719 ================================================
1.239 - setNextTactic 1 (Check_elementwise "Assumptions");
1.240 -============ inhibit exn 110719 ==============================================*)
1.241 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.242 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
1.243 - val (ptp,_) = get_calc 1;
1.244 - val (Form t,_,_) = pt_extract ptp;
1.245 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.246 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.247 -
1.248 -
1.249 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.250 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.251 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.252 -(*{\bf\UC{Having \isac{} Refine the Problem
1.253 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.254 - * x^^^2 + 4*x + 5 = 2
1.255 -see isac.bridge.TestSpecify#testMatchRefine*)
1.256 - DEconstrCalcTree 1;
1.257 - CalcTree
1.258 - [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
1.259 - ("Isac",
1.260 - ["univariate","equation"],
1.261 - ["no_met"]))];
1.262 - Iterator 1;
1.263 - moveActiveRoot 1;
1.264 -
1.265 - fetchProposedTactic 1;
1.266 - setNextTactic 1 (Model_Problem );
1.267 - (*..this tactic should be done 'tacitly', too !*)
1.268 -
1.269 -(*
1.270 -autoCalculate 1 CompleteCalcHead;
1.271 -checkContext 1 ([],Pbl) "pbl_equ_univ";
1.272 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.273 -*)
1.274 -
1.275 - autoCalculate 1 (Step 1);
1.276 -
1.277 - fetchProposedTactic 1;
1.278 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
1.279 - autoCalculate 1 (Step 1);
1.280 -
1.281 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.282 -initContext 1 Pbl_ ([],Pbl);
1.283 -initContext 1 Met_ ([],Pbl);
1.284 -
1.285 - "--------- this match will show some incomplete items: ---------";
1.286 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.287 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.288 -
1.289 -
1.290 - fetchProposedTactic 1;
1.291 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
1.292 -
1.293 - fetchProposedTactic 1;
1.294 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
1.295 -
1.296 - "--------- this is a matching model (all items correct): -------";
1.297 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.298 - "--------- this is a NOT matching model (some 'false': ---------";
1.299 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
1.300 -
1.301 - "--------- find out a matching problem: ------------------------";
1.302 - "--------- find out a matching problem (FAILING: no new pbl) ---";
1.303 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
1.304 -
1.305 - "--------- find out a matching problem (SUCCESSFUL) ------------";
1.306 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
1.307 -
1.308 - "--------- tryMatch, tryRefine di ["univariate","equation"], ["no_met"]))];
1.309 - Iterator 1;
1.310 - moveActiveRoot 1;
1.311 - fetchProposedTactic 1;
1.312 -
1.313 -(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
1.314 - setNextTactic 1 (Model_Problem );
1.315 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.316 -
1.317 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.318 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
1.319 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.320 - setNextTactic 1 (Add_Given "solveFor x");
1.321 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.322 - setNextTactic 1 (Add_Find "solutions L");
1.323 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.324 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.325 - setNextTactic 1 (Specify_Theory "RatEq");
1.326 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.327 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.328 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.329 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.330 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.331 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.332 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.333 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.334 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.335 - setNextTactic 1 (Rewrite_Set "norm_Rational");
1.336 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.337 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.338 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.339 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.340 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
1.341 - "univariate","equation"]));
1.342 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.343 - setNextTactic 1 (Model_Problem );
1.344 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.345 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.346 - setNextTactic 1 (Add_Given
1.347 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
1.348 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.349 - setNextTactic 1 (Add_Given "solveFor x");
1.350 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.351 - setNextTactic 1 (Add_Find "solutions x_i");
1.352 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.353 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.354 - setNextTactic 1 (Specify_Theory "PolyEq");
1.355 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.356 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.357 - "univariate","equation"]);
1.358 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.359 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.360 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.361 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.362 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.363 - setNextTactic 1 (Rewrite ("all_left",""));
1.364 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.365 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.366 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.367 - (* __________ for "16 + 12 * x = 0"*)
1.368 - setNextTactic 1 (Subproblem ("PolyEq",
1.369 - ["degree_1","polynomial","univariate","equation"]));
1.370 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.371 - setNextTactic 1 (Model_Problem );
1.372 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.373 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.374 - setNextTactic 1 (Add_Given
1.375 - "equality (16 + 12 * x = 0)");
1.376 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.377 - setNextTactic 1 (Add_Given "solveFor x");
1.378 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.379 - setNextTactic 1 (Add_Find "solutions x_i");
1.380 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.381 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.382 - setNextTactic 1 (Specify_Theory "PolyEq");
1.383 - (*------------- some trials in the problem-hierarchy ---------------*)
1.384 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
1.385 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.386 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.387 - (*------------------------------------------------------------------*)
1.388 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.389 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.390 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.391 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.392 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.393 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.394 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.395 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.396 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.397 - (*==================================================================*)
1.398 - setNextTactic 1 Or_to_List;
1.399 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.400 -(* setNextTactic 1 (Check_elementwise "Assumptions");
1.401 - WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.402 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
1.403 -val ((pt, _), _) = get_calc cI;
1.404 -val ip = get_pos cI 1;
1.405 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.406 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
1.407 -val (mI,m) = mk_tac'_ tac;
1.408 -val Appl m = applicable_in p pt m;
1.409 -member op = specsteps mI (*false*);
1.410 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.411 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
1.412 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
1.413 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.414 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.415 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.416 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.417 - val d = e_rls;
1.418 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.419 - WAS: exception Match raised (line 1218 of ".../script.sml"*)
1.420 -(*========== inhibit exn 110719 ================================================
1.421 -========== inhibit exn 110719 XXX=============================================*)
1.422 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.423 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
1.424 - "univariate","equation"]);
1.425 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.426 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.427 - "univariate","equation"]);
1.428 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.429 -
1.430 -(*** exception TYPE raised (line 460 of "old_goals.ML"):
1.431 -*** Type error in application: Incompatible operand type
1.432 -***
1.433 -*** Operator: equality :: bool => una
1.434 -*** Operand: [((x * 3) = -4)] :: bool list
1.435 -***
1.436 -*** bool => una
1.437 -*** bool list
1.438 -*** equality
1.439 -*** [x * 3 = -4]*)
1.440 -
1.441 -(*========== inhibit exn 110719 ================================================
1.442 - setNextTactic 1 (Check_elementwise "Assumptions");
1.443 ============ inhibit exn 110719 ==============================================*)
1.444 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.445 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);