1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 20:02:16 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Jul 15 20:09:44 2021 +0200
1.3 @@ -187,7 +187,7 @@
1.4 ML_file "BaseDefinitions/calcelems.sml"
1.5 ML_file "BaseDefinitions/termC.sml"
1.6 ML_file "BaseDefinitions/substitution.sml"
1.7 -(** )ML_file "BaseDefinitions/contextC.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.8 + ML_file "BaseDefinitions/contextC.sml"
1.9 ML_file "BaseDefinitions/environment.sml"
1.10 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.12 @@ -200,7 +200,7 @@
1.13 ML_file "ProgLang/program.sml"
1.14 ML_file "ProgLang/prog_tac.sml"
1.15 ML_file "ProgLang/tactical.sml"
1.16 -(** )ML_file "ProgLang/auto_prog.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.17 + ML_file "ProgLang/auto_prog.sml"
1.18 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.19 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.20
1.21 @@ -254,706 +254,14 @@
1.22 ML_file "Interpret/error-pattern.sml"
1.23 ML_file "Interpret/li-tool.sml"
1.24 ML_file "Interpret/lucas-interpreter.sml"
1.25 -ML \<open>
1.26 -\<close> ML \<open>
1.27 -(* Title: "Interpret/lucas-interpreter.sml"
1.28 - Author: Walther Neuper
1.29 - (c) due to copyright terms
1.30 -*)
1.31 -
1.32 -"-----------------------------------------------------------------------------------------------";
1.33 -"table of contents -----------------------------------------------------------------------------";
1.34 -"-----------------------------------------------------------------------------------------------";
1.35 -"----------- Take as 1st stac in program -------------------------------------------------------";
1.36 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
1.37 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
1.38 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.39 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
1.40 -"-----------------------------------------------------------------------------------------------";
1.41 -"-----------------------------------------------------------------------------------------------";
1.42 -"-----------------------------------------------------------------------------------------------";
1.43 -
1.44 -"----------- Take as 1st stac in program -------------------------------------------------------";
1.45 -"----------- Take as 1st stac in program -------------------------------------------------------";
1.46 -"----------- Take as 1st stac in program -------------------------------------------------------";
1.47 -"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
1.48 -val p = e_pos'; val c = [];
1.49 -val (p,_,f,nxt,_,pt) =
1.50 - CalcTreeTEST
1.51 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
1.52 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
1.53 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
1.54 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.55 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.56 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.58 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.60 -case nxt of (Apply_Method ["diff", "integration"]) => ()
1.61 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
1.62 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
1.63 -
1.64 -"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
1.65 -"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
1.66 -val Applicable.Yes m = Step.check tac (pt, p);
1.67 - (*if*) Tactic.for_specify' m; (*false*)
1.68 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
1.69 -
1.70 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
1.71 - = (m, (pt, pos));
1.72 - val {srls, ...} = MethodC.from_store mI;
1.73 - val itms = case get_obj I pt p of
1.74 - PblObj {meth=itms, ...} => itms
1.75 - | _ => error "solve Apply_Method: uncovered case get_obj"
1.76 - val thy' = get_obj g_domID pt p;
1.77 - val thy = ThyC.get_theory thy';
1.78 - val srls = LItool.get_simplifier (pt, pos)
1.79 - val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
1.80 - (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
1.81 - | _ => error "solve Apply_Method: uncovered case init_pstate";
1.82 -(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
1.83 - val ini = LItool.implicit_take sc env;
1.84 - val p = lev_dn p;
1.85 -
1.86 - val NONE = (*case*) ini (*of*);
1.87 - val Next_Step (is', ctxt', m') =
1.88 - LI.find_next_step sc (pt, (p, Res)) is ctxt;
1.89 -(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
1.90 - val Safe_Step (_, _, Take' _) = (*case*)
1.91 - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
1.92 -"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
1.93 - = (sc, (pt, (p, Res)), is', ctxt', m');
1.94 -
1.95 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
1.96 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
1.97 - = ((prog, (cstate, ctxt, tac)), istate);
1.98 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
1.99 -
1.100 - val Accept_Tac1 (_, _, Take' _) =
1.101 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
1.102 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
1.103 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
1.104 -
1.105 -(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
1.106 -
1.107 - (*case*)
1.108 - scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
1.109 - (*======= end of scanning tacticals, a leaf =======*)
1.110 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
1.111 - = (xxx, (ist |> path_down [L, R]), e);
1.112 -val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
1.113 -
1.114 -
1.115 -
1.116 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
1.117 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
1.118 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
1.119 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.120 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.121 - ["Test", "squ-equ-test-subpbl1"]);
1.122 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.123 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.124 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.125 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.126 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.127 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.128 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.129 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
1.130 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
1.131 -
1.132 -(*//------------------ begin step into ------------------------------------------------------\\*)
1.133 -(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
1.134 -
1.135 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
1.136 -
1.137 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
1.138 - Step.by_tactic tac (pt,p) (*of*);
1.139 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
1.140 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
1.141 - (*if*) Tactic.for_specify' m; (*false*)
1.142 -
1.143 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
1.144 -Step_Solve.by_tactic m ptp;
1.145 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
1.146 -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
1.147 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
1.148 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.149 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
1.150 -
1.151 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
1.152 -"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
1.153 - = (sc, (pt, po), (fst is), (snd is), m);
1.154 - val srls = get_simplifier cstate;
1.155 -
1.156 - (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
1.157 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
1.158 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
1.159 - = ((prog, (cstate, ctxt, tac)), istate);
1.160 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
1.161 -
1.162 - (** )val xxxxx_xx = ( **)
1.163 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
1.164 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
1.165 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
1.166 -
1.167 - (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
1.168 -"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
1.169 - = (xxx, (ist |> path_down [L, R]), e);
1.170 -
1.171 - (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
1.172 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
1.173 - = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
1.174 -
1.175 - (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
1.176 - (*======= end of scanning tacticals, a leaf =======*)
1.177 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
1.178 - = (xxx, (ist |> path_down [R]), e);
1.179 - val (Program.Tac stac, a') =
1.180 - (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
1.181 - val LItool.Associated (m, v', ctxt) =
1.182 - (*case*) associate pt ctxt (m, stac) (*of*);
1.183 -
1.184 - Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
1.185 -"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
1.186 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
1.187 -
1.188 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
1.189 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
1.190 - (*if*) LibraryC.assoc (*then*);
1.191 -
1.192 - Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
1.193 -"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
1.194 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
1.195 -
1.196 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
1.197 - val (p'', _, _,pt') =
1.198 - Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
1.199 - (*in*)
1.200 -
1.201 - ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
1.202 - [(*ctree NOT cut*)], (pt', p''))) (*return value*);
1.203 -"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
1.204 - = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
1.205 - [(*ctree NOT cut*)], (pt', p'')));
1.206 -
1.207 -"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
1.208 - val (_, ts) =
1.209 - (case Step.do_next p ((pt, Pos.e_pos'), []) of
1.210 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
1.211 - | ("helpless", _) => ("helpless: cannot propose tac", [])
1.212 - | ("no-fmz-spec", _) => error "no-fmz-spec"
1.213 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
1.214 - | _ => error "me: uncovered case")
1.215 - handle ERROR msg => raise ERROR msg
1.216 - val tac =
1.217 - case ts of
1.218 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.219 - | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
1.220 -
1.221 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
1.222 -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
1.223 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
1.224 -
1.225 -(*//--------------------- check results from modified me ----------------------------------\\*)
1.226 -if p = ([2], Res) andalso
1.227 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
1.228 -then
1.229 - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
1.230 - | _ => error "")
1.231 -else error "check results from modified me CHANGED";
1.232 -(*\\--------------------- check results from modified me ----------------------------------//*)
1.233 -
1.234 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
1.235 -(*\\------------------ end step into --------------------------------------------------------//*)
1.236 -
1.237 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
1.238 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
1.239 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
1.240 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
1.241 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
1.242 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
1.243 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
1.244 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
1.245 -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.246 -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
1.247 -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
1.248 -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
1.249 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
1.250 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
1.251 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
1.252 -
1.253 -(*/--------------------- final test ----------------------------------\\*)
1.254 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
1.255 - ". ----- pblobj -----\n" ^
1.256 - "1. x + 1 = 2\n" ^
1.257 - "2. x + 1 + - 1 * 2 = 0\n" ^
1.258 - "3. ----- pblobj -----\n" ^
1.259 - "3.1. - 1 + x = 0\n" ^
1.260 - "3.2. x = 0 + - 1 * - 1\n" ^
1.261 - "4. [x = 1]\n"
1.262 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
1.263 -else error "re-build: fun locate_input_tactic changed 2";
1.264 -
1.265 -
1.266 -\<close> ML \<open>
1.267 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
1.268 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
1.269 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
1.270 -(*cp from -- try fun applyTactics ------- *)
1.271 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
1.272 - "normalform N"],
1.273 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.274 - ["simplification", "for_polynomials", "with_minus"]))];
1.275 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.276 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.277 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.278 -\<close> ML \<open>
1.279 -f
1.280 -\<close> ML \<open>
1.281 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
1.282 -\<close> ML \<open>
1.283 -(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
1.284 -\<close> ML \<open>
1.285 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
1.286 -
1.287 -\<close> ML \<open>
1.288 -(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f
1.289 -\<close> ML \<open>
1.290 -\<close> ML \<open> (*GOON*)
1.291 -map Tactic.input_to_string (specific_from_prog pt p)
1.292 -\<close> ML \<open>
1.293 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
1.294 - ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
1.295 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
1.296 - then () else error "specific_from_prog ([1], Res) CHANGED";
1.297 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.298 -
1.299 -\<close> ML \<open>
1.300 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
1.301 - ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
1.302 - "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
1.303 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
1.304 - then () else error "specific_from_prog ([1], Res) CHANGED";
1.305 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.306 -
1.307 -\<close> ML \<open>
1.308 -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
1.309 -(** )val ("ok", (_, _, ptp as (pt, p))) =( **)
1.310 - Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
1.311 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
1.312 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
1.313 - (*if*) Tactic.for_specify' m; (*false*)
1.314 -
1.315 -Step_Solve.by_tactic m (pt, p);
1.316 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
1.317 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.318 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.319 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
1.320 -
1.321 - (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
1.322 -"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
1.323 - = (sc, (pt, po), (fst is), (snd is), m);
1.324 - val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
1.325 -
1.326 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
1.327 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
1.328 - = ((prog, (cstate, ctxt, tac)), istate);
1.329 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
1.330 -
1.331 - go_scan_up1 (prog, cctt) ist;
1.332 -"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
1.333 - = ((prog, cctt), ist);
1.334 - (*if*) 1 < length path (*then*);
1.335 -
1.336 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
1.337 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
1.338 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
1.339 -
1.340 - go_scan_up1 pcct ist;
1.341 -"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
1.342 - = (pcct, ist);
1.343 - (*if*) 1 < length path (*then*);
1.344 -
1.345 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
1.346 -"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
1.347 - (Const ("Tactical.Chain"(*3*), _) $ _ ))
1.348 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
1.349 - val e2 = check_Seq_up ist prog
1.350 -;
1.351 - (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
1.352 -"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2))
1.353 - = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
1.354 -
1.355 - (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
1.356 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
1.357 - = (cct, (ist |> path_down [L, R]), e1);
1.358 -
1.359 - (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
1.360 - (*======= end of scanning tacticals, a leaf =======*)
1.361 -"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
1.362 - = (cct, (ist |> path_down [R]), e);
1.363 - (*if*) Tactical.contained_in t (*else*);
1.364 - val (Program.Tac prog_tac, form_arg) = (*case*)
1.365 - LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
1.366 -
1.367 - check_tac1 cct ist (prog_tac, form_arg);
1.368 -"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
1.369 - (cct, ist, (prog_tac, form_arg));
1.370 -val LItool.Not_Associated = (*case*)
1.371 - LItool.associate pt ctxt (tac, prog_tac) (*of*);
1.372 - val _(*ORundef*) = (*case*) or (*of*);
1.373 - val Applicable.Yes m' =
1.374 - (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
1.375 -
1.376 - Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
1.377 - (*return from check_tac1*);
1.378 -"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
1.379 - (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
1.380 -
1.381 -(*/----- original before child of 7e314dd233fd -------------------------------------------------\* )
1.382 - val (Program.Tac prog_tac, form_arg) = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
1.383 - val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
1.384 - val ORundef = (*case*) or (*of*);
1.385 - val Applicable.No "norm_equation not applicable" =
1.386 - (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (pt, p) (*of*);
1.387 -
1.388 - (Term_Val1 act_arg) (* return value *);
1.389 -
1.390 -val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
1.391 - t, (res, asm)) = m;
1.392 -
1.393 -if pstate2str ist =
1.394 - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], empty, SOME t_t, \n" ^
1.395 - "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, true, false)"
1.396 -andalso
1.397 - UnparseC.term t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
1.398 -andalso
1.399 - UnparseC.term res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
1.400 -andalso
1.401 - UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
1.402 -then () else error "locate_input_tactic Helpless, but applicable CHANGED";
1.403 -( *\----- original before child of 7e314dd233fd -------------------------------------------------/*)
1.404 -
1.405 -
1.406 -\<close> ML \<open>
1.407 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.408 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.409 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
1.410 -val fmz = ["Term (a + a ::real)", "normalform n_n"];
1.411 -val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
1.412 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.413 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
1.414 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
1.415 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
1.416 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
1.417 -(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
1.418 -(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
1.419 -
1.420 - Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
1.421 -\<close> ML \<open>
1.422 -(*//------------------ go into 1 ------------------------------------------------------------\\*)
1.423 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.424 - = (p, ((pt, e_pos'), []));
1.425 - val pIopt = Ctree.get_pblID (pt, ip);
1.426 - (*if*) ip = ([], Res) (*else*);
1.427 - val _ = (*case*) tacis (*of*);
1.428 - val SOME _ = (*case*) pIopt (*of*);
1.429 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
1.430 -
1.431 -val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
1.432 -Step_Solve.do_next (pt, ip);
1.433 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.434 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.435 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.436 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
1.437 -
1.438 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
1.439 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.440 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
1.441 - = (sc, (pt, pos), ist, ctxt);
1.442 -
1.443 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
1.444 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
1.445 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
1.446 - = ((prog, (ptp, ctxt)), (Pstate ist));
1.447 - (*if*) path = [] (*then*);
1.448 -
1.449 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
1.450 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
1.451 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
1.452 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
1.453 - (*if*) Tactical.contained_in t (*else*);
1.454 - val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
1.455 -
1.456 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
1.457 - check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
1.458 -"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
1.459 - = (check_tac cc ist (prog_tac, form_arg));
1.460 -
1.461 - Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
1.462 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
1.463 - = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
1.464 -
1.465 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
1.466 -"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
1.467 - = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
1.468 -(*\\------------------ end of go into 1 -----------------------------------------------------//*)
1.469 -
1.470 -(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
1.471 -
1.472 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
1.473 -(*//------------------ go into 2 ------------------------------------------------------------\\*)
1.474 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.475 - = (p''''', ((pt''''', e_pos'), []));
1.476 - val pIopt = Ctree.get_pblID (pt, ip);
1.477 - (*if*) ip = ([], Res) (*else*);
1.478 - val _ = (*case*) tacis (*of*);
1.479 - val SOME _ = (*case*) pIopt (*of*);
1.480 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
1.481 -
1.482 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
1.483 -Step_Solve.do_next (pt, ip);
1.484 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
1.485 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.486 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.487 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
1.488 -
1.489 - (** )val End_Program (ist, tac) =
1.490 - ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.491 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
1.492 - = (sc, (pt, pos), ist, ctxt);
1.493 -
1.494 -(* val Term_Val (Const ("Groups.times_class.times", _) $ Free ("2", _) $ Free ("a", _))*)
1.495 - (** )val Term_Val prog_result =
1.496 - ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
1.497 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
1.498 - = ((prog, (ptp, ctxt)), (Pstate ist));
1.499 - (*if*) path = [] (*else*);
1.500 -
1.501 - go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
1.502 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
1.503 - = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
1.504 - (*if*) path = [R] (*then*);
1.505 - (*if*) found_accept = true (*then*);
1.506 -
1.507 - Term_Val act_arg (*return from go_scan_up*);
1.508 -"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
1.509 -
1.510 - Term_Val prog_result (*return from scan_to_tactic*);
1.511 -"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
1.512 - val (true, p', _) = (*case*) parent_node pt p (*of*);
1.513 - val (_, pblID, _) = get_obj g_spec pt p';
1.514 -
1.515 - End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
1.516 - (*return from find_next_step*);
1.517 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
1.518 - = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
1.519 - val _ = (*case*) tac (*of*);
1.520 -
1.521 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
1.522 - = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
1.523 -"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
1.524 - = (LI.by_tactic tac (ist, ctxt) ptp);
1.525 -(*\\------------------ end of go into 2 -----------------------------------------------------//*)
1.526 -
1.527 -(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
1.528 -
1.529 -Test_Tool.show_pt_tac pt; (*[
1.530 -([], Frm), Simplify (a + a)
1.531 -. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
1.532 -([1], Frm), a + a
1.533 -. . . . . . . . . . Rewrite_Set "norm_Poly",
1.534 -([1], Res), 2 * a
1.535 -. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
1.536 -([], Res), 2 * a]*)
1.537 -
1.538 -(*/--- final test ---------------------------------------------------------------------------\\*)
1.539 -val (res, asm) = (get_obj g_result pt (fst p));
1.540 -if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
1.541 -andalso p = ([], Und) andalso msg = "end-of-calculation"
1.542 -andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
1.543 -then
1.544 - case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
1.545 - | _ => error "re-build: fun find_next_step, mini 1"
1.546 -else error "re-build: fun find_next_step, mini 2"
1.547 -
1.548 -
1.549 -\<close> ML \<open>
1.550 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
1.551 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
1.552 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
1.553 -(*cp from inform.sml
1.554 - ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
1.555 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.556 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.557 - ["Test", "squ-equ-test-subpbl1"]);
1.558 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.559 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.560 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.561 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.562 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.563 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.564 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.565 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
1.566 -
1.567 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
1.568 -(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
1.569 -
1.570 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
1.571 -(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
1.572 -
1.573 -Test_Tool.show_pt_tac pt; (*[
1.574 -([], Frm), solve (x + 1 = 2, x)
1.575 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.576 -([1], Frm), x + 1 = 2
1.577 -. . . . . . . . . . Rewrite_Set "norm_equation",
1.578 -([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
1.579 -
1.580 -(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
1.581 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
1.582 - val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
1.583 - val pos = (*get_pos cI 1*) p
1.584 -
1.585 -(*+*)val ptp''''' = (pt, p);
1.586 -(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
1.587 -(*+*)Test_Tool.show_pt_tac pt; (*[
1.588 -(*+*)([], Frm), solve (x + 1 = 2, x)
1.589 -(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.590 -(*+*)([1], Frm), x + 1 = 2
1.591 -(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
1.592 -(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
1.593 -
1.594 - val ("ok", cs' as (_, _, ptp')) =
1.595 - (*case*) Step.do_next pos cs (*of*);
1.596 -
1.597 -val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
1.598 - Step_Solve.by_term ptp' (encode ifo) (*of*);
1.599 -"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
1.600 - = (ptp', (encode ifo));
1.601 - val SOME f_in =
1.602 - (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
1.603 - val f_in = Thm.term_of f_in
1.604 - val pos_pred = lev_back(*'*) pos
1.605 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
1.606 - val f_succ = Ctree.get_curr_formula (pt, pos);
1.607 - (*if*) f_succ = f_in (*else*);
1.608 - val NONE =
1.609 - (*case*) CAS_Cmd.input f_in (*of*);
1.610 -
1.611 -(*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
1.612 -(*old*) val {scr = prog, ...} = MethodC.from_store metID
1.613 -(*old*) val istate = get_istate_LI pt pos
1.614 -(*old*) val ctxt = get_ctxt pt pos
1.615 - val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
1.616 - LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
1.617 -"~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
1.618 - = (prog, (pt, pos), istate, ctxt, f_in);
1.619 -( *old*)
1.620 -
1.621 -(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
1.622 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
1.623 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.624 -
1.625 - val ("ok", (_, _, cstate as (pt', pos'))) =
1.626 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
1.627 -
1.628 -(*old* )
1.629 - Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
1.630 -( *old*)
1.631 -(*NEW*) Found_Step cstate (*return from locate_input_term*);
1.632 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
1.633 -"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
1.634 - = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
1.635 -
1.636 - ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
1.637 -"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
1.638 - = ("ok", ([], [], ptp));
1.639 -
1.640 -(*fun me requires nxt...*)
1.641 - Step.do_next p''''' (ptp''''', []);
1.642 - val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
1.643 - (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
1.644 -(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
1.645 -
1.646 -(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
1.647 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
1.648 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
1.649 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
1.650 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
1.651 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
1.652 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
1.653 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
1.654 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
1.655 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.656 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
1.657 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
1.658 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
1.659 -( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
1.660 -
1.661 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
1.662 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
1.663 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
1.664 -
1.665 -(*/--- final test ---------------------------------------------------------------------------\\*)
1.666 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
1.667 - ". ----- pblobj -----\n" ^
1.668 - "1. x + 1 = 2\n" ^
1.669 - "2. x + 1 + - 1 * 2 = 0\n" ^
1.670 - "3. ----- pblobj -----\n" ^
1.671 - "3.1. - 1 + x = 0\n" ^
1.672 - "3.2. x = 0 + - 1 * - 1\n" ^
1.673 - "3.2.1. x = 0 + - 1 * - 1\n" ^
1.674 - "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
1.675 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
1.676 -else error "re-build: fun locate_input_term CHANGED 2";
1.677 -
1.678 -Test_Tool.show_pt_tac pt; (*[
1.679 -([], Frm), solve (x + 1 = 2, x)
1.680 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.681 -([1], Frm), x + 1 = 2
1.682 -. . . . . . . . . . Rewrite_Set "norm_equation",
1.683 -([1], Res), x + 1 + - 1 * 2 = 0
1.684 -. . . . . . . . . . Rewrite_Set "Test_simplify",
1.685 -([2], Res), - 1 + x = 0
1.686 -. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
1.687 -([3], Pbl), solve (- 1 + x = 0, x)
1.688 -. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
1.689 -([3,1], Frm), - 1 + x = 0
1.690 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
1.691 -([3,1], Res), x = 0 + - 1 * - 1
1.692 -. . . . . . . . . . Derive Test_simplify,
1.693 -([3,2,1], Frm), x = 0 + - 1 * - 1
1.694 -. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
1.695 -([3,2,1], Res), x = 0 + 1
1.696 -. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
1.697 -([3,2,2], Res), x = 1
1.698 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
1.699 -([3,2], Res), x = 1
1.700 -. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
1.701 -([3], Res), [x = 1]
1.702 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
1.703 -([], Res), [x = 1]]*)
1.704 -
1.705 -\<close> ML \<open>
1.706 -\<close> ML \<open>
1.707 -\<close> ML \<open>
1.708 -\<close> ML \<open>
1.709 -\<close> ML \<open>
1.710 -\<close> ML \<open>
1.711 -\<close> ML \<open>
1.712 -\<close> ML \<open>
1.713 -\<close> ML \<open>
1.714 -\<close>
1.715 ML_file "Interpret/step-solve.sml"
1.716
1.717 -ML_file "MathEngine/me-misc.sml"
1.718 + ML_file "MathEngine/me-misc.sml"
1.719 ML_file "MathEngine/fetch-tactics.sml"
1.720 -(** )ML_file "MathEngine/solve.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.721 + ML_file "MathEngine/solve.sml"
1.722 ML_file "MathEngine/step.sml"
1.723 -(** )
1.724 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
1.725 - ( *loops with eliminate ThmC.numerals_to_Free*)
1.726 -ML_file "MathEngine/messages.sml"
1.727 + ML_file "MathEngine/messages.sml"
1.728 ML_file "MathEngine/states.sml"
1.729
1.730 ML_file "BridgeLibisabelle/thy-present.sml"
1.731 @@ -1012,8 +320,8 @@
1.732 ML_file "Knowledge/biegelinie-1.sml"
1.733 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
1.734 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
1.735 -(** )ML_file "Knowledge/biegelinie-4.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.736 -(** )ML_file "Knowledge/algein.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.737 + ML_file "Knowledge/biegelinie-4.sml"
1.738 + ML_file "Knowledge/algein.sml"
1.739 ML_file "Knowledge/diophanteq.sml"
1.740 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
1.741 ML_file "Knowledge/inssort.sml"