1.1 --- a/src/Tools/isac/Build_Isac.thy Sat Nov 19 12:10:19 2022 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sat Nov 19 15:30:52 2022 +0100
1.3 @@ -172,7 +172,8 @@
1.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
1.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
1.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
1.7 -(*ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"*)
1.8 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
1.9 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
1.10 ML \<open>
1.11 \<close> ML \<open>
1.12 \<close> ML \<open>
1.13 @@ -195,569 +196,209 @@
1.14 ["Test", "squ-equ-test-subpbl1"]);
1.15 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
1.16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
1.17 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
1.18 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
1.19 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
1.20 +(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.21 +(*[1], Res*)val (_, ([(tac''', _, _)], _, (pt''', p'''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
1.22
1.23 -\<close> ML \<open>
1.24 -(*[], Pbl*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
1.25 -
1.26 -\<close> ML \<open> (*//----------- step into Model_Problem ---------------------------------------------\\*)
1.27 -(*//------------------ step into Model_Problem ---------------------------------------------\\*)
1.28 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.29 - = (p, ((pt, e_pos'), []));
1.30 +(*//------------------ step into Apply_Method ----------------------------------------------\\*)
1.31 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.32 + = (p ,((pt, e_pos'), []));
1.33 (*if*) Pos.on_calc_end ip (*else*);
1.34 val (_, probl_id, _) = Calc.references (pt, p);
1.35 val _ =
1.36 (*case*) tacis (*of*);
1.37 (*if*) probl_id = Problem.id_empty (*else*);
1.38
1.39 -\<close> ML \<open>
1.40 Step.switch_specify_solve p_ (pt, ip);
1.41 -\<close> ML \<open>
1.42 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.43 - (*if*) Pos.on_specification ([], state_pos) (*then*);
1.44 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
1.45 + = (p_, (pt, ip));
1.46 + (*if*) Pos.on_specification ([], state_pos) (*else*);
1.47
1.48 -\<close> ML \<open>
1.49 - Step.specify_do_next (pt, input_pos);
1.50 -\<close> ML \<open>
1.51 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.52 + LI.do_next (pt, input_pos);
1.53 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
1.54 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.55 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
1.56 +val LI.Next_Step (ist, ctxt, tac) =
1.57 + (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.58
1.59 -\<close> ML \<open>
1.60 - val (_, (p_', tac)) =
1.61 - Specify.find_next_step ptp;
1.62 -\<close> ML \<open>
1.63 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
1.64 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1.65 - spec = refs, ...} = Calc.specify_data (pt, pos);
1.66 - val ctxt = Ctree.get_ctxt pt pos;
1.67 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1.68 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
1.69 +"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
1.70 + = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
1.71 + val pos = next_in_prog' pos
1.72
1.73 -\<close> ML \<open>
1.74 - Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
1.75 -\<close> ML \<open>
1.76 -"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
1.77 - = (ctxt, oris, (o_refs, refs), (pbl, met));
1.78 - val cpI = if pI = Problem.id_empty then pI' else pI;
1.79 - val cmI = if mI = MethodC.id_empty then mI' else mI;
1.80 - val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
1.81 - val {model = mpc, ...} = MethodC.from_store ctxt cmI
1.82 + val (pos', c, _, pt) =
1.83 +Solve_Step.add_general tac_ ic (pt, pos);
1.84 +"~~~~~ fun add_general , args:"; val (tac, ic, cs)
1.85 + = (tac_, ic, (pt, pos));
1.86 + (*if*) Tactic.for_specify' tac (*else*);
1.87
1.88 -\<close> ML \<open>
1.89 - val (preok, _) =
1.90 - Pre_Conds.check ctxt where_rls where_ pbl 0;
1.91 -\<close> ML \<open>
1.92 -"~~~~~ fun check , args:"; val (where_rls, pres, pbl, _) = (where_rls, where_, pbl, 0);
1.93 - val env = I_Model.environment pbl;
1.94 - val pres' = map (TermC.subst_atomic_all env) pres;
1.95 - val evals = map (Pre_Conds.eval ctxt where_rls) pres';
1.96 +Solve_Step.add tac ic cs;
1.97 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
1.98 + = (tac, ic, cs);
1.99 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
1.100 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
1.101 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.102
1.103 -\<close> ML \<open>
1.104 - Pre_Conds.eval;
1.105 -\<close> ML \<open>
1.106 -"~~~~~ fun eval , args:"; val (ctxt, where_rls, (true, where_) ) = (ctxt, where_rls, hd pres');
1.107 -(*-------------------- stop step into Model_Problem ------------------------------------------*)
1.108 -(*\\------------------ step into Model_Problem ---------------------------------------------//*)
1.109 -\<close> ML \<open> (*\\----------- step into Model_Problem ---------------------------------------------//*)
1.110 +val return =
1.111 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
1.112 +(*-------------------- stop step into Apply_Method -------------------------------------------*)
1.113 +(*\\------------------ step into Apply_Method ----------------------------------------------//*)
1.114
1.115 -\<close> ML \<open> (*/------------ step into Specify_Theory ---------------------------------------------\*)
1.116 -(*/------------------- step into Specify_Theory ---------------------------------------------\*)
1.117 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p''''', ((pt''''', e_pos'), []));
1.118 - val pIopt = Ctree.get_pblID (pt, ip);
1.119 - (*if*) ip = ([], Pos.Res) (*else*);
1.120 - val _ = (*case*) tacis (*of*);
1.121 - val SOME _ = (*case*) pIopt (*of*);
1.122 +(*[2], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p''' ((pt''', e_pos'), []);(*Rewrite_Set "Test_simplify"*)
1.123
1.124 -(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
1.125 - Step.switch_specify_solve p_ (pt, ip);
1.126 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.127 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
1.128 -
1.129 -(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
1.130 - Step.specify_do_next (pt, input_pos);
1.131 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.132 -
1.133 -(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
1.134 - val (_, (_(*p_'*), _(*tac*))) =
1.135 -Specify.find_next_step ptp;
1.136 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = ptp;
1.137 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1.138 - spec = refs, ...} = Calc.specify_data (pt, pos);
1.139 - val ctxt = Ctree.get_ctxt pt pos;
1.140 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1.141 - (*if*) p_ = Pos.Pbl (*then*);
1.142 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
1.143 - Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
1.144 -(*\--------- step into Specify_Theory --------------------------------------------------------/*)
1.145 -\<close> ML \<open>(*\--- step into Specify_Theory --------------------------------------------------------/*)
1.146 -
1.147 -\<close> ML \<open>
1.148 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
1.149 -\<close> ML \<open>
1.150 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
1.151 -\<close> ML \<open>
1.152 -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.153 -\<close> ML \<open>
1.154 -(*[1], Res*)val (_, ([(tac''', _, _)], _, (pt''', p'''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
1.155 -\<close> ML \<open> (*//----------- step into Apply_Method ----------------------------------------------\\*)
1.156 -(*//------------------ step into Apply_Method ----------------------------------------------\\*)
1.157 -\<close> ML \<open>
1.158 +(*//------------------ step into Rewrite_Set -----------------------------------------------\\*)
1.159 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.160 - = (p ,((pt, e_pos'), []));
1.161 -\<close> ML \<open>
1.162 + = (p''', ((pt''', e_pos'), []));
1.163 (*if*) Pos.on_calc_end ip (*else*);
1.164 -\<close> ML \<open>
1.165 val (_, probl_id, _) = Calc.references (pt, p);
1.166 -\<close> ML \<open>
1.167 val _ =
1.168 (*case*) tacis (*of*);
1.169 -\<close> ML \<open>
1.170 (*if*) probl_id = Problem.id_empty (*else*);
1.171 -\<close> ML \<open>
1.172 - Step.switch_specify_solve p_ (pt, ip)
1.173 -\<close> ML \<open>
1.174 +
1.175 + Step.switch_specify_solve p_ (pt, ip);
1.176 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
1.177 = (p_, (pt, ip));
1.178 -\<close> ML \<open>
1.179 (*if*) Pos.on_specification ([], state_pos) (*else*);
1.180 -\<close> ML \<open>
1.181 - LI.do_next (pt, input_pos)
1.182 -\<close> ML \<open>
1.183 +
1.184 + LI.do_next (pt, input_pos);
1.185 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
1.186 -\<close> ML \<open>
1.187 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.188 -\<close> ML \<open>
1.189 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
1.190 -\<close> ML \<open>
1.191 -val LI.Next_Step (ist, ctxt, tac) =
1.192 - (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.193 -\<close> ML \<open>
1.194 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
1.195 -\<close> ML \<open>
1.196 -"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
1.197 - = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
1.198 -\<close> ML \<open>
1.199 - val pos = next_in_prog' pos
1.200 -\<close> ML \<open>
1.201 - val (pos', c, _, pt) =
1.202 -Solve_Step.add_general tac_ ic (pt, pos);
1.203 -\<close> ML \<open>
1.204 -"~~~~~ fun add_general , args:"; val (tac, ic, cs)
1.205 - = (tac_, ic, (pt, pos));
1.206 -\<close> ML \<open>
1.207 - (*if*) Tactic.for_specify' tac (*else*);
1.208 -\<close> ML \<open>
1.209 -Solve_Step.add tac ic cs
1.210 -\<close> ML \<open>
1.211 -"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
1.212 - = (tac, ic, cs);
1.213 -\<close> ML \<open>
1.214 - val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
1.215 - (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
1.216 -\<close> ML \<open>
1.217 - val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.218 -\<close> ML \<open>
1.219 -val return =
1.220 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
1.221 -(*-------------------- stop step into Apply_Method -------------------------------------------*)
1.222 -\<close> ML \<open> (*------------- stop step into Apply_Method -------------------------------------------*)
1.223 -(*\\------------------ step into Apply_Method ----------------------------------------------//*)
1.224 -\<close> ML \<open> (*\\----------- step into Apply_Method ----------------------------------------------//*)
1.225 -\<close> ML \<open>
1.226 -\<close> text \<open>
1.227 -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = Step.do_next p''' ((pt''', e_pos'), []);(*Rewrite_Set "Test_simplify"*)
1.228 -\<close> ML \<open> (*//----------- step into Rewrite_Set -----------------------------------------------\\*)
1.229 -(*//------------------ step into Rewrite_Set -----------------------------------------------\\*)
1.230 -\<close> ML \<open>
1.231 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.232 - = (p''', ((pt''', e_pos'), []));
1.233 -\<close> ML \<open>
1.234 - (*if*) Pos.on_calc_end ip (*else*);
1.235 -\<close> ML \<open>
1.236 - val (_, probl_id, _) = Calc.references (pt, p);
1.237 -\<close> ML \<open>
1.238 -val _ =
1.239 - (*case*) tacis (*of*);
1.240 -\<close> ML \<open>
1.241 - (*if*) probl_id = Problem.id_empty (*else*);
1.242 -\<close> text \<open>
1.243 - Step.switch_specify_solve p_ (pt, ip);
1.244 -\<close> ML \<open>
1.245 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
1.246 - = (p_, (pt, ip));
1.247 -\<close> ML \<open>
1.248 - (*if*) Pos.on_specification ([], state_pos) (*else*);
1.249 -\<close> text \<open>
1.250 - LI.do_next (pt, input_pos)
1.251 -\<close> ML \<open>
1.252 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
1.253 -\<close> ML \<open>
1.254 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
1.255 -\<close> ML \<open>
1.256 - val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
1.257 -\<close> text \<open>
1.258 +
1.259 (*case*)
1.260 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
1.261 -\<close> ML \<open>
1.262 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt)
1.263 = (sc, (pt, pos), ist, ctxt);
1.264 -\<close> text \<open>
1.265 +
1.266 (*case*)
1.267 LI.scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
1.268 -\<close> ML \<open>
1.269 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
1.270 = ((prog, (ptp, ctxt)), (Istate.Pstate ist) );
1.271 -\<close> ML \<open>
1.272 (*if*) path = [] (*else*);
1.273 -\<close> text \<open>
1.274 +
1.275 LI.go_scan_up (prog, cc) (Istate.trans_scan_up ist);
1.276 -\<close> ML \<open>
1.277 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
1.278 = ((prog, cc), (Istate.trans_scan_up ist));
1.279 -\<close> ML \<open>
1.280 (*if*) path = [R] (*root of the program body*) (*else*);
1.281 -\<close> text \<open>
1.282 +
1.283 LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc);
1.284 -\<close> ML \<open>
1.285 "~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _))
1.286 -= (pcc, (ist |> Istate.path_up), (go_up path sc));
1.287 -\<close> text \<open>
1.288 - LI.go_scan_up pcc ist
1.289 -\<close> ML \<open>
1.290 + = (pcc, (ist |> Istate.path_up), (go_up path sc));
1.291 +
1.292 + LI.go_scan_up pcc ist;
1.293 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
1.294 = (pcc, ist);
1.295 -\<close> ML \<open>
1.296 (*if*) path = [R] (*root of the program body*) (*else*);
1.297 -\<close> text \<open>
1.298 +
1.299 LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc);
1.300 -\<close> ML \<open>
1.301 "~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _))
1.302 = (pcc, (ist |> Istate.path_up), (go_up path sc));
1.303 -\<close> ML \<open>
1.304 - val e2 = LI.check_Seq_up ist sc
1.305 -\<close> text \<open>
1.306 + val e2 = LI.check_Seq_up ist sc;
1.307 +
1.308 (*case*)
1.309 LI.scan_dn cc (ist |> Istate.path_up_down [R]) e2 (*of*);
1.310 -\<close> ML \<open>
1.311 "~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e))
1.312 = (cc, (ist |> Istate.path_up_down [R]), e2 );
1.313 -\<close> text \<open>
1.314 +
1.315 (*case*)
1.316 LI.scan_dn cc (ist |> Istate.path_down [R]) e (*of*);
1.317 -\<close> ML \<open>
1.318 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*))
1.319 = (cc, (ist |> Istate.path_down [R]), e);
1.320 -\<close> ML \<open>
1.321 (*if*) Tactical.contained_in t (*else*);
1.322 -\<close> ML \<open>
1.323 val (Program.Tac prog_tac, form_arg) =
1.324 (*case*) LItool.check_leaf "next " ctxt eval (Istate.get_subst ist) t (*of*);
1.325 -\<close> text \<open>
1.326 +
1.327 LI.check_tac cc ist (prog_tac, form_arg);
1.328 -\<close> ML \<open>
1.329 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
1.330 = (cc, ist, (prog_tac, form_arg));
1.331 -\<close> ML \<open>
1.332 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
1.333 -\<close> ML \<open>
1.334 val _ =
1.335 (*case*) m (*of*);
1.336 -\<close> text \<open>
1.337 +
1.338 (*case*)
1.339 Solve_Step.check m (pt, p) (*of*);
1.340 -\<close> ML \<open>
1.341 "~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, pos)) )
1.342 = (m, (pt, p));
1.343 -\<close> ML \<open>
1.344 val ctxt = Ctree.get_loc pt pos |> snd
1.345 val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
1.346 val f = Calc.current_formula cs;
1.347 -\<close> text \<open>
1.348 - (*case*)
1.349 +
1.350 +(*+*)val ctxt = Config.put rewrite_trace true ctxt;
1.351 +val SOME (f', asm) = (*case*)
1.352 Rewrite.rewrite_set_ ctxt false (get_rls ctxt rls) f (*of*);
1.353 +(*+*)val ctxt = Config.put rewrite_trace false ctxt;
1.354 +(*
1.355 +@# rls: Test_simplify on: x + 1 + - 1 * 2 = 0
1.356 +@## try thm: "real_diff_minus"
1.357 +@## try thm: "radd_mult_distrib2"
1.358 +@## try thm: "rdistr_right_assoc"
1.359 +@## try thm: "rdistr_right_assoc_p"
1.360 +@## try thm: "rdistr_div_right"
1.361 +@## try thm: "rbinom_power_2"
1.362 +@## try thm: "radd_commute"
1.363 +@### eval asms: "x + 1 + - 1 * 2 = - 1 * 2 + (x + 1)"
1.364 +@## not >: "x + 1 + - 1 * 2" > "- 1 * 2 + (x + 1)"
1.365 +@### eval asms: "x + 1 = 1 + x"
1.366 +@## rewrites to: "1 + x + - 1 * 2 = 0"
1.367 +@## try thm: "radd_commute"
1.368 +@### eval asms: "1 + x + - 1 * 2 = - 1 * 2 + (1 + x)"
1.369 +@## not >: "1 + x + - 1 * 2" > "- 1 * 2 + (1 + x)"
1.370 +@### eval asms: "1 + x = x + 1"
1.371 +@## not >: "1 + x" > "x + 1"
1.372 +@## try thm: "radd_left_commute"
1.373 +@## try thm: "add.assoc"
1.374 +@### eval asms: "1 + x + - 1 * 2 = 1 + (x + - 1 * 2)"
1.375 +@## rewrites to: "1 + (x + - 1 * 2) = 0"
1.376 +@## try thm: "add.assoc"
1.377 +@## try thm: "rmult_commute"
1.378 +@### eval asms: "- 1 * 2 = 2 * - 1"
1.379 +@## not >: "- 1 * 2" > "2 * - 1"
1.380 +@## try thm: "rmult_left_commute"
1.381 +@## try thm: "rmult_assoc"
1.382 +@## try thm: "radd_real_const_eq"
1.383 +@## try thm: "radd_real_const"
1.384 +@## try calc: "Groups.plus_class.plus"
1.385 +@## try calc: "Groups.times_class.times"
1.386 +-------------------------------------------- ME_Isa: thy "Isac_Knowledge" not in system
1.387 +@### eval asms: "- 1 * 2 = - 2"
1.388 +@## calc. to: 1 + (x + - 2) = 0
1.389 +@## try calc: "Groups.times_class.times"
1.390 +@## try calc: "Rings.divide_class.divide"
1.391 +@## try calc: "BaseDefinitions.realpow"
1.392 +:
1.393 +*)
1.394 +(*-------------------- stop step into Rewrite_Set --------------------------------------------*)
1.395 +(*\\------------------ step into Rewrite_Set -----------------------------------------------//*)
1.396 +
1.397 +(* final test ... ----------------------------------------------------------------------------*)
1.398 +(*+*)val ([2], Res) = p''''';
1.399 +Test_Tool.show_pt_tac pt'''''; (*[
1.400 +([], Frm), solve (x + 1 = 2, x)
1.401 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
1.402 +([1], Frm), x + 1 = 2
1.403 +. . . . . . . . . . Rewrite_Set "norm_equation",
1.404 +([1], Res), x + 1 + - 1 * 2 = 0
1.405 +. . . . . . . . . . Rewrite_Set "Test_simplify",
1.406 +([2], Res), - 1 + x = 0
1.407 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
1.408 +*)
1.409 +
1.410 +\<close> ML \<open>
1.411 \<close> ML \<open>
1.412 -"~~~~~ fun rewrite_set_ , args:"; val (ctxt, bool, rls, term)
1.413 - = (ctxt, false, (get_rls ctxt rls), f);
1.414 -\<close> text \<open>
1.415 - Rewrite.rewrite__set_ ctxt 1 bool [] rls term
1.416 \<close> ML \<open>
1.417 -"~~~~~ and rewrite__set_ , args:"; val ((*3*)ctxt, i, put_asm, bdv, rls, ct)
1.418 - = (ctxt, 1, bool, [], rls, term);
1.419 \<close> ML \<open>
1.420 -val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
1.421 -
1.422 -fun trace1 ctxt i str =
1.423 - if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
1.424 - then tracing (idt "#" (i + 1) ^ str) else ()
1.425 -fun trace_in1 ctxt i str thmid =
1.426 - trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
1.427 -fun trace_in2 ctxt i str t =
1.428 - trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"");
1.429 -fun trace_in3 ctxt i str pairopt =
1.430 - trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
1.431 -fun msg call ctxt op_ thmC t =
1.432 - call ^ ": \n" ^
1.433 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^
1.434 - "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
1.435 -
1.436 - datatype switch = Appl | Noap;
1.437 - fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.438 - | rew_once (*2*)ruls asm ct Appl [] =
1.439 - (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
1.440 - | Rule_Set.Sequence _ => (ct, asm)
1.441 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
1.442 - | rew_once (*3*)ruls asm ct apno (rul :: thms) =
1.443 - case rul of
1.444 - Rule.Thm (thmid, thm) =>
1.445 - (trace_in1 ctxt i "try thm" thmid;
1.446 - case Rewrite.rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.447 - ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct of
1.448 - NONE => rew_once ruls asm ct apno thms
1.449 - | SOME (ct', asm') =>
1.450 - (trace_in2 ctxt i "rewrites to" ct';
1.451 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.452 - (* once again try the same rule, e.g. associativity against "()"*)
1.453 - | Rule.Eval (cc as (op_, _)) =>
1.454 - let val _ = trace_in1 ctxt i "try calc" op_;
1.455 - in case Eval.adhoc_thm ctxt cc ct of
1.456 - NONE => rew_once ruls asm ct apno thms
1.457 - | SOME (_, thm') =>
1.458 - let
1.459 - val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.460 - ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
1.461 - val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct)
1.462 - val _ = trace_in3 ctxt i "calc. to" pairopt;
1.463 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.464 - end
1.465 - | Rule.Cal1 (cc as (op_, _)) =>
1.466 - let val _ = trace_in1 ctxt i "try cal1" op_;
1.467 - in case Eval.adhoc_thm1_ ctxt cc ct of
1.468 - NONE => (ct, asm)
1.469 - | SOME (_, thm') =>
1.470 - let
1.471 - val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.472 - ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
1.473 - val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
1.474 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
1.475 - val _ = trace_in3 ctxt i "cal1. to" pairopt;
1.476 - in the pairopt end
1.477 - end
1.478 - | Rule.Rls_ rls' =>
1.479 - (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
1.480 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.481 - | NONE => rew_once ruls asm ct apno thms)
1.482 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
1.483 -
1.484 \<close> ML \<open>
1.485 - val ruls = (#rules o Rule_Set.rep) rls;
1.486 \<close> ML \<open>
1.487 - val _ = trace_eq1 ctxt i "rls" rls ct
1.488 -\<close> text \<open>
1.489 - val (ct', asm') =
1.490 - rew_once ruls [] ct Noap ruls;
1.491 \<close> ML \<open>
1.492 -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms))
1.493 - = (ruls, [], ct, Noap, ruls);
1.494 \<close> ML \<open>
1.495 -val Rule.Thm (thmid, thm) =
1.496 - (*case*) rul (*of*);
1.497 \<close> ML \<open>
1.498 -val NONE =
1.499 - (*case*) rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.500 - ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*);
1.501 -\<close> text \<open>
1.502 - rew_once ruls asm ct apno thms;
1.503 \<close> ML \<open>
1.504 -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms))
1.505 - = (ruls, asm, ct, apno, thms);
1.506 -\<close> ML \<open>
1.507 -(*+*) val Rule.Thm (thmid, thm)= nth 5 thms; (*fst thm rewriting to SOME*)
1.508 -\<close> text \<open>
1.509 - (*case*)
1.510 - rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.511 - ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*);
1.512 -\<close> ML \<open>
1.513 -"~~~~~ fun rewrite__ , args:"; val (ctxt, i, bdv, tless, rls, put_asm, thm, ct)
1.514 - = (ctxt, (i + 1), bdv:Subst.T, ((snd o #rew_ord o Rule_Set.rep) rls),
1.515 - ((#asm_rls o Rule_Set.rep) rls), put_asm, thm, ct);
1.516 -\<close> ML \<open>
1.517 -(* ------------------------------------------^^^.., id = "tval_rls" (*o*)
1.518 -rls =
1.519 - Repeat
1.520 - {asm_rls =
1.521 - Repeat
1.522 - {asm_rls = Repeat {asm_rls = Empty, calc = [], errpatts = [], id = "empty", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("dummy_ord", fn), rules = []}, calc = [], errpatts = [], id =
1.523 - "testerls", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("termlessI", fn), rules =
1.524 - [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \<le> ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"),
1.525 - Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"),
1.526 - Thm ("and_commute", "(?a \<and> ?b) = (?b \<and> ?a)"), Thm ("or_commute", "(?a \<or> ?b) = (?b \<or> ?a)"), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.matches", fn), Eval ("Groups.plus_class.plus", fn),
1.527 - Eval ("Groups.times_class.times", fn), Eval ("BaseDefinitions.realpow", fn), Eval ("Orderings.ord_class.less", fn), Eval ("Orderings.ord_class.less_eq", fn), Eval ("Prog_Expr.ident", fn)]},
1.528 - calc = [], errpatts = [], id = "tval_rls", preconds = [], prog_rls =
1.529 - Repeat {asm_rls = Empty, calc = [], errpatts = [], id = "empty", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("dummy_ord", fn), rules = []}, program = Empty_Prog, rew_ord =
1.530 - ("sqrt_right", fn), rules =
1.531 - [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \<le> ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"),
1.532 - Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("and_commute", "(?a \<and> ?b) = (?b \<and> ?a)"),
1.533 - Thm ("or_commute", "(?a \<or> ?b) = (?b \<or> ?a)"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"), Thm ("root_ge0", "0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True"),
1.534 - Thm ("root_add_ge0", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> (0 \<le> sqrt ?a + sqrt ?b) = True"), Thm ("root_ge0_1", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> 0 \<le> ?c \<Longrightarrow> (0 \<le> ?a * sqrt ?b + sqrt ?c) = True"),
1.535 - Thm ("root_ge0_2", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> 0 \<le> ?c \<Longrightarrow> (0 \<le> sqrt ?a + ?b * sqrt ?c) = True"), Eval ("Prog_Expr.is_num", fn), Eval ("Test.contains_root", fn), Eval ("Prog_Expr.matches", fn),
1.536 - Eval ("Test.contains_root", fn), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.times_class.times", fn), Eval ("NthRoot.sqrt", fn), Eval ("BaseDefinitions.realpow", fn),
1.537 - Eval ("Orderings.ord_class.less", fn), Eval ("Orderings.ord_class.less_eq", fn), Eval ("Prog_Expr.ident", fn)]}
1.538 -*)
1.539 -\<close> ML \<open>
1.540 -\<close> text \<open>
1.541 - val (t', asms, _(*lrd*), rew) =
1.542 - Rewrite.rew_sub ctxt i bdv tless rls put_asm ([]: TermC.path)
1.543 - (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
1.544 -\<close> ML \<open>
1.545 -"~~~~~ and rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
1.546 - = (ctxt, i, bdv, tless, rls, put_asm, ([]: TermC.path),
1.547 - (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
1.548 -\<close> ML \<open>
1.549 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.550 -\<close> ML \<open>
1.551 -(* inhibit exn NO_REWRITE
1.552 - val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
1.553 - (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.554 - handle Pattern.MATCH => raise NO_REWRITE
1.555 -*)
1.556 -(*+*) UnparseC.term_in_ctxt ctxt t = "x + 1 + - 1 * 2 = 0";
1.557 -\<close> ML \<open>
1.558 -val t1 $ t2 =
1.559 - (*case*) t (*of*);
1.560 -\<close> ML \<open>
1.561 -val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.562 -\<close> ML \<open>
1.563 - (*if*) rew2 (*else*);
1.564 -\<close> text \<open>
1.565 -val (t1', asm1, lrd, rew1) =
1.566 - rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.567 -\<close> ML \<open>
1.568 -"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
1.569 - = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.L]), r, t1);
1.570 -\<close> ML \<open>
1.571 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.572 -\<close> ML \<open>
1.573 -(* inhibit exn NO_REWRITE
1.574 - val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
1.575 - (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.576 - handle Pattern.MATCH => raise NO_REWRITE
1.577 -*)
1.578 -(*+*) UnparseC.term_in_ctxt ctxt t = "(=) (x + 1 + - 1 * 2)";
1.579 -\<close> ML \<open>
1.580 -val t1 $ t2 =
1.581 - (*case*) t (*of*);
1.582 -\<close> text \<open>
1.583 -val (t2', asm2, lrd, rew2) =
1.584 - rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.585 -\<close> ML \<open>
1.586 -"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
1.587 - = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.R]), r, t2);
1.588 -\<close> ML \<open>
1.589 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.590 -\<close> ML \<open>
1.591 - val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
1.592 - (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.593 - handle Pattern.MATCH => raise NO_REWRITE
1.594 -\<close> ML \<open>
1.595 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.596 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.597 -\<close> ML \<open>
1.598 -(*+*) UnparseC.term_in_ctxt ctxt t' = "- 1 * 2 + (x + 1)";
1.599 -\<close> ML \<open>
1.600 - val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls
1.601 -\<close> ML \<open>
1.602 - (*if*) nofalse (*then*);
1.603 -\<close> ML \<open>
1.604 - val (t'', p'') = (t', simpl_p')
1.605 -\<close> text \<open>
1.606 - (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t));
1.607 -\<close> text \<open>
1.608 - (tless bdv (t', t))
1.609 -\<close> ML \<open>
1.610 -(*+*)tless; (*vvv--- found (*o*) tval_rls*)
1.611 -(*+*) val sqrt_right = tval_rls |> (snd o #rew_ord o Rule_Set.rep);
1.612 -\<close> ML \<open>
1.613 -"~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), (ts, us))
1.614 - = (false, @{theory}(*?!*), bdv, (t', t));
1.615 -\<close> text \<open> -- hidden by "local" -- delete
1.616 - (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
1.617 -\<close> ML \<open>
1.618 -\<close> ML \<open>
1.619 -\<close> ML \<open>
1.620 -\<close> ML \<open>
1.621 -\<close> ML \<open>
1.622 -\<close> ML \<open>
1.623 -\<close> ML \<open>
1.624 -\<close> ML \<open>
1.625 -\<close> ML \<open>
1.626 -\<close> ML \<open>
1.627 -\<close> ML \<open>
1.628 -\<close> ML \<open>
1.629 -\<close> ML \<open>
1.630 -(*keep for continuing Rewrite_Set*)
1.631 -\<close> ML \<open> (*------------- continuing Rewrite_Set ------------------------------------------------*)
1.632 -(*-------------------- continuing Rewrite_Set ------------------------------------------------*)
1.633 -(*kept for continuing XXXXX*)
1.634 -(*-------------------- stop step into Rewrite_Set --------------------------------------------*)
1.635 -\<close> ML \<open> (*------------- stop step into Rewrite_Set --------------------------------------------*)
1.636 -(*\\------------------ step into Rewrite_Set -----------------------------------------------//*)
1.637 -\<close> ML \<open> (*\\----------- step into Rewrite_Set -----------------------------------------------//*)
1.638 -
1.639 -\<close> text \<open>
1.640 -(*/--------- investigate Rewrite_Set "Test_simplify" -----------------------------------------\*)
1.641 -(*+*)val form = get_obj g_res pt (fst p);
1.642 -(*+*)UnparseC.term form = "x + 1 + - 1 * 2 = 0"; (*isa*)
1.643 -(*+*)UnparseC.term form = "x + 1 + -1 * 2 = 0"; (*isa2*)
1.644 -\<close> text \<open>
1.645 -
1.646 -val Rewrite_Set "Test_simplify" = tac;
1.647 -
1.648 -val res = get_obj g_res pt''''' (fst p''''');
1.649 -(*+* )UnparseC.term res = "1 + (x + - 2) = 0"; ( *isa*)
1.650 -(*+*)if UnparseC.term res = "- 1 + x = 0" (*isa2*) then () else error "Test_simplify CHANGED";
1.651 -
1.652 -\<close> text \<open>
1.653 -val SOME (form', _) = rewrite_set_ ctxt true Test_simplify form;
1.654 -
1.655 -(*+* )UnparseC.term form' = "1 + (x + - 2) = 0"; ( *isa*)
1.656 -(*+*)if UnparseC.term form' = "- 1 + x = 0" (*isa2*) then () else error "Test_simplify CHANGED";
1.657 -(*\--------- investigate Rewrite_Set "Test_simplify" -----------------------------------------/*)
1.658 -\<close> text \<open>
1.659 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(* Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
1.660 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
1.661 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
1.662 -
1.663 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
1.664 -(*[3], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
1.665 -(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
1.666 -(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
1.667 -
1.668 -val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;
1.669 -
1.670 -\<close> text \<open>
1.671 -if p = ([3, 1], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) = "x = 0 + - 1 * - 1"
1.672 -then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()
1.673 - | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"
1.674 -else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"
1.675 -
1.676 -Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
1.677 -\<close> ML \<open>
1.678 -\<close> ML \<open>
1.679 -\<close> ML \<open>
1.680 -\<close> ML \<open>
1.681 -\<close> ML \<open>
1.682 -\<close> ML \<open>
1.683 -\<close> ML \<open>
1.684 -\<close> ML \<open>
1.685 -\<close> ML \<open>
1.686 -\<close> ML \<open>
1.687 -\<close> text \<open>
1.688 -M_Match.match_oris':
1.689 -(* vvvvvvvvvvvvv thy in MODEL_MATCH*)
1.690 - Proof.context -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
1.691 - bool * (I_Model.T * Pre_Conds.T)
1.692 \<close> ML \<open>
1.693 \<close> ML \<open>
1.694 \<close>
1.695 -(*----------------------- exclude in TEST_BASE ----------------------------------------(**)
1.696 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
1.697 +(*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
1.698 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
1.699 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
1.700 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
1.701 @@ -775,7 +416,7 @@
1.702 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
1.703 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
1.704 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
1.705 -(**)----------------------- exclude in TEST_BASE ----------------------------------------*)
1.706 +(**)\----- outcomment in order to intermediately check with Test_Isac.thy --------------/*)
1.707
1.708
1.709 text \<open>