106 \<close> ML \<open> |
107 \<close> ML \<open> |
107 \<close> ML \<open> |
108 \<close> ML \<open> |
108 \<close> ML \<open> |
109 \<close> ML \<open> |
109 \<close> |
110 \<close> |
110 |
111 |
111 section \<open>===================================================================================\<close> |
112 section \<open>========= test/../Knowlegde/equsystem-1a.sml ======================================\<close> |
112 ML \<open> |
113 ML \<open> |
113 \<close> ML \<open> |
114 \<close> ML \<open> |
114 \<close> ML \<open> |
115 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; |
|
116 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; |
|
117 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; |
|
118 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\ |
|
119 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", |
|
120 "solveForVars [c, c_2]", "solution LL"]; |
|
121 val (dI',pI',mI') = |
|
122 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"], |
|
123 ["EqSystem", "normalise", "2x2"]); |
|
124 val p = e_pos'; val c = []; |
|
125 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
126 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
127 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
128 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
130 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => () |
|
131 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; |
|
132 |
|
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
134 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
135 |
|
136 (*+*)if f2str f = |
|
137 "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^ |
|
138 " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error ""; |
|
139 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) = |
|
140 "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)"; |
|
141 |
|
142 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
143 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
144 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
145 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
146 |
|
147 (*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f; |
|
148 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)" = |
|
149 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); |
|
150 |
|
151 case nxt of |
|
152 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
|
153 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem"; |
|
154 |
|
155 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
156 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
157 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
158 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
159 case nxt of |
|
160 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
|
161 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
|
162 |
|
163 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
164 |
|
165 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
166 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); |
|
167 |
|
168 val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f; |
|
169 (*/------------------- step into me Apply_Method -------------------------------------------\*) |
|
170 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); |
|
171 \<close> ML \<open> |
|
172 val (pt'''', p'''') = (* keep for continuation*) |
|
173 (*Step.by_tactic is here for testing by me; do_next would suffice in me*) |
|
174 |
|
175 case Step.by_tactic tac (pt, p) of |
|
176 ("ok", (_, _, ptp)) => ptp; |
|
177 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
|
178 |
|
179 (*+isa==isa2*)val ([5], Met) = p; |
|
180 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p); |
|
181 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
182 (*+isa==isa2*)is1 |> Istate.string_of; |
|
183 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
184 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); |
|
185 |
|
186 (*case*) |
|
187 Step.check tac (pt, p) (*of*); |
|
188 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) ); |
|
189 |
|
190 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
191 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of); |
|
192 |
|
193 (*if*) Tactic.for_specify tac (*else*); |
|
194 val Applicable.Yes xxx = |
|
195 |
|
196 Solve_Step.check tac (ctree, pos); |
|
197 |
|
198 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
199 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of); |
|
200 |
|
201 "~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx); |
|
202 (*if*) Tactic.for_specify' tac' (*else*); |
|
203 |
|
204 Step_Solve.by_tactic tac' ptp;; |
|
205 "~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p))) |
|
206 = (tac', ptp); |
|
207 |
|
208 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
209 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); |
|
210 |
|
211 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp; |
|
212 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) |
|
213 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp); |
|
214 val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*) |
|
215 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) |
|
216 val {ppc, ...} = MethodC.from_store ctxt mI; |
|
217 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc |
|
218 val srls = LItool.get_simplifier (pt, pos) |
|
219 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of |
|
220 (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr) |
|
221 |
|
222 (*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" = |
|
223 (*+isa==isa2*)is |> Istate.string_of |
|
224 |
|
225 val ini = LItool.implicit_take prog env; |
|
226 val pos = start_new_level pos |
|
227 val NONE = |
|
228 (*case*) ini (*of*); |
|
229 val (tac''', ist''', ctxt''') = |
|
230 case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of |
|
231 Next_Step (ist, ctxt, tac) => (tac, ist, ctxt) |
|
232 |
|
233 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = |
|
234 (*+isa==isa2*)ist''' |> Istate.string_of; |
|
235 |
|
236 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) |
|
237 = (prog ,(pt, (lev_dn p, Res)), is, ctxt); |
|
238 val Accept_Tac |
|
239 (Take' ttt, iii, _) = |
|
240 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); |
|
241 |
|
242 (*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term); |
|
243 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = |
|
244 (*+isa==isa2*)(Pstate iii |> Istate.string_of); |
|
245 |
|
246 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) |
|
247 = ((prog, (ptp, ctxt)), (Pstate ist)); |
|
248 (*if*) path = [] (*then*); |
|
249 |
|
250 scan_dn cc (trans_scan_dn ist) (Program.body_of prog); |
|
251 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) |
|
252 = (cc, (trans_scan_dn ist), (Program.body_of prog)); |
|
253 |
|
254 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*); |
|
255 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) |
|
256 = (cc ,(ist |> path_down [L, R]), e); |
|
257 |
|
258 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" = |
|
259 (*+isa==isa2*)(Pstate ist |> Istate.string_of); |
|
260 |
|
261 (*if*) Tactical.contained_in t (*else*); |
|
262 |
|
263 (*case*) |
|
264 LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); |
|
265 "~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t) |
|
266 = ("next ", ctxt, eval, (get_subst ist), t); |
|
267 |
|
268 (*case*) |
|
269 Prog_Tac.eval_leaf E a v t (*of*); |
|
270 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _))) |
|
271 = (E, a, v, t); |
|
272 |
|
273 val return = |
|
274 (Program.Tac (subst_atomic E t), NONE:term option); |
|
275 "~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return; |
|
276 val stac' = Rewrite.eval_prog_expr ctxt srls |
|
277 (subst_atomic (Env.update_opt E (a, v)) stac) |
|
278 |
|
279 val return = |
|
280 (Program.Tac stac', a'); |
|
281 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return; |
|
282 |
|
283 check_tac cc ist (prog_tac, form_arg); |
|
284 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) |
|
285 = (cc, ist, (prog_tac, form_arg)); |
|
286 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac |
|
287 val _ = |
|
288 (*case*) m (*of*); (*tac as string/input*) |
|
289 |
|
290 (*case*) |
|
291 Solve_Step.check m (pt, p) (*of*); |
|
292 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p)); |
|
293 |
|
294 val return = |
|
295 check_tac cc ist (prog_tac, form_arg) |
|
296 |
|
297 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" = |
|
298 (*+isa==isa2*)(Pstate ist |> Istate.string_of); |
|
299 |
|
300 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; |
|
301 val (Accept_Tac (tac, ist, ctxt)) = return; |
|
302 |
|
303 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = |
|
304 (*+isa==isa2*)(Pstate ist |> Istate.string_of) |
|
305 |
|
306 val return = |
|
307 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac); |
|
308 "~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return; |
|
309 val (tac', ist', ctxt') = (tac, ist, ctxt) |
|
310 val Tactic.Take' t = |
|
311 (*case*) tac' (*of*); |
|
312 val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt'); |
|
313 |
|
314 (*+isa==isa2*)pos; (*from check_tac*) |
|
315 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5]; |
|
316 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = |
|
317 (*+isa==isa2*)is1 |> Istate.string_of; |
|
318 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = |
|
319 (*+isa==isa2*)(ist' |> Istate.string_of) |
|
320 (*-------------------- stop step into me Apply_Method ----------------------------------------*) |
|
321 (*+isa==isa2*)val "c_2 = 0" = f2str f; |
|
322 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = |
|
323 (*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of) |
|
324 (*\\------------------- step into me Apply_Method ------------------------------------------//*) |
|
325 |
|
326 \<close> ML \<open> |
|
327 val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f; |
|
328 \<close> ML \<open> |
|
329 (*+isa==isa2*)val ([5, 1], Frm) = p''''; |
|
330 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f; |
|
331 (*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** ) |
|
332 Substitute ["c_2 = 0"]( **) = nxt''''; |
|
333 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p''''); |
|
334 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" = |
|
335 (*+isa==isa2*)is1 |> Istate.string_of; |
|
336 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" = |
|
337 (*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of; |
|
338 \<close> ML \<open> (*//----------- step into me Take ---------------------------------------------------\\*) |
|
339 (*//------------------ step into me Take ---------------------------------------------------\\*) |
|
340 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt'''); |
|
341 \<close> ML \<open> |
|
342 val (pt, p) = (* keep for continuation*) |
|
343 (*Step.by_tactic is here for testing by me; do_next would suffice in me*) |
|
344 |
|
345 case Step.by_tactic tac (pt, p) of |
|
346 ("ok", (_, _, ptp)) => ptp; |
|
347 \<close> ML \<open> |
|
348 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" = |
|
349 (*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of; |
|
350 \<close> ML \<open> |
|
351 (*case*) |
|
352 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
353 \<close> ML \<open> |
|
354 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); |
|
355 \<close> ML \<open> |
|
356 (*if*) Pos.on_calc_end ip (*else*); |
|
357 \<close> ML \<open> |
|
358 val (_, probl_id, _) = Calc.references (pt, p); |
|
359 \<close> ML \<open> |
|
360 val _ = |
|
361 (*case*) tacis (*of*); |
|
362 \<close> ML \<open> |
|
363 (*if*) probl_id = Problem.id_empty (*else*); |
|
364 \<close> ML \<open> |
|
365 switch_specify_solve p_ (pt, ip); |
|
366 \<close> ML \<open> |
|
367 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
368 \<close> ML \<open> |
|
369 (*if*) Pos.on_specification ([], state_pos) (*else*); |
|
370 \<close> ML \<open> |
|
371 LI.do_next (pt, input_pos); |
|
372 \<close> ML \<open> |
|
373 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); |
|
374 \<close> ML \<open> |
|
375 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
|
376 \<close> ML \<open> |
|
377 val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
378 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt; |
|
379 \<close> ML \<open> |
|
380 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" = |
|
381 (*+isa==isa2*)ist |> Istate.string_of; |
|
382 \<close> ML \<open> |
|
383 (*case*) |
|
384 LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
|
385 \<close> ML \<open> |
|
386 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) |
|
387 = (sc, (pt, pos), ist, ctxt); |
|
388 \<close> ML \<open> |
|
389 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); |
|
390 \<close> ML \<open> |
|
391 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) |
|
392 = ((prog, (ptp, ctxt)), (Pstate ist)); |
|
393 \<close> ML \<open> |
|
394 (*if*) path = [] (*else*); |
|
395 \<close> ML \<open> |
|
396 go_scan_up (prog, cc) (trans_scan_up ist); |
|
397 \<close> ML \<open> |
|
398 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) |
|
399 = ((prog, cc), (trans_scan_up ist)); |
|
400 \<close> ML \<open> |
|
401 val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" = |
|
402 (*+isa==isa2*)Pstate ist |> Istate.string_of; |
|
403 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term; |
|
404 \<close> ML \<open> |
|
405 (*if*) path = [R] (*root of the program body*) (*else*); |
|
406 \<close> ML \<open> |
|
407 scan_up pcc (ist |> path_up) (go_up path sc); |
|
408 \<close> ML \<open> |
|
409 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _)) |
|
410 = (pcc, (ist |> path_up), (go_up path sc)); |
|
411 \<close> ML \<open> |
|
412 val (i, body) = check_Let_up ist sc |
|
413 \<close> ML \<open> |
|
414 (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*); |
|
415 \<close> ML \<open> |
|
416 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) |
|
417 = (cc, (ist |> path_up_down [R, D] |> upd_env i), body); |
|
418 \<close> ML \<open> |
|
419 val goback = |
|
420 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*); |
|
421 \<close> ML \<open> |
|
422 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a)) |
|
423 = (cc, (ist |> path_down [L, R]), e); |
|
424 \<close> ML \<open> |
|
425 (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*); |
|
426 \<close> ML \<open> |
|
427 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) |
|
428 = (cc, (ist |> path_down_form ([L, L, R], a)), e1); |
|
429 \<close> ML \<open> |
|
430 (*if*) Tactical.contained_in t (*else*); |
|
431 \<close> ML \<open> |
|
432 (*case*) |
|
433 LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); |
|
434 \<close> ML \<open> |
|
435 "~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t) |
|
436 = ("next ", ctxt, eval, (get_subst ist), t); |
|
437 \<close> ML \<open> |
|
438 val (Program.Tac stac, a') = |
|
439 (*case*) Prog_Tac.eval_leaf E a v t (*of*); |
|
440 \<close> ML \<open> |
|
441 val stac' = Rewrite.eval_prog_expr ctxt srls |
|
442 (subst_atomic (Env.update_opt E (a, v)) stac) |
|
443 \<close> ML \<open> |
|
444 (*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term; |
|
445 \<close> ML \<open> |
|
446 val return = |
|
447 (Program.Tac stac', a') |
|
448 \<close> ML \<open> |
|
449 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg)) |
|
450 = (return); |
|
451 \<close> ML \<open> |
|
452 check_tac cc ist (prog_tac, form_arg); |
|
453 \<close> ML \<open> |
|
454 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) |
|
455 = (cc, ist, (prog_tac, form_arg)); |
|
456 \<close> ML \<open> |
|
457 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac |
|
458 \<close> ML \<open> |
|
459 val _ = |
|
460 (*case*) m (*of*); |
|
461 \<close> ML \<open> |
|
462 (*case*) |
|
463 Solve_Step.check m (pt, p) (*of*); |
|
464 \<close> ML \<open> |
|
465 "~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _)))) |
|
466 = (m, (pt, p)); |
|
467 \<close> ML \<open> |
|
468 val pp = Ctree.par_pblobj pt p |
|
469 val ctxt = Ctree.get_loc pt pos |> snd |
|
470 val thy = Proof_Context.theory_of ctxt |
|
471 val f = Calc.current_formula cs; |
|
472 val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) |
|
473 val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*) |
|
474 val ro = get_rew_ord ctxt rew_ord' |
|
475 \<close> ML \<open> |
|
476 (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*); |
|
477 \<close> ML \<open> |
|
478 (*+isa==isa2*)sube : TermC.as_string list |
|
479 \<close> ML \<open> |
|
480 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term |
|
481 \<close> ML \<open> |
|
482 (*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term |
|
483 \<close> ML \<open> |
|
484 val SOME ttt = |
|
485 (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*); |
|
486 \<close> ML \<open> |
|
487 \<close> ML \<open> (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*) |
|
488 (*//------------------ build new fun XXXXX -------------------------------------------------\\*) |
|
489 \<close> ML \<open> |
|
490 fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs; |
|
491 \<close> ML \<open> |
|
492 input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs |
|
493 \<close> ML \<open> |
|
494 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type*) |
|
495 fun input_to_terms ctxt strs = strs |
|
496 |> map (TermC.parse ctxt) |
|
497 |> map (Model_Pattern.adapt_term_to_type ctxt) |
|
498 \<close> ML \<open> |
|
499 \<close> ML \<open> |
|
500 \<close> ML \<open> |
|
501 \<close> ML \<open> |
|
502 (*\\------------------ build new fun XXXXX -------------------------------------------------//*) |
|
503 \<close> ML \<open> (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*) |
|
504 \<close> ML \<open> |
|
505 \<close> ML \<open> |
|
506 \<close> ML \<open> |
|
507 \<close> ML \<open> |
|
508 \<close> ML \<open> |
|
509 \<close> ML \<open> |
|
510 \<close> ML \<open> |
|
511 \<close> ML \<open> |
|
512 \<close> text \<open> |
|
513 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_up , return:"; val (Accept_Tac ict) = (goback); |
|
514 \<close> text \<open> |
|
515 "~~~~~ from fun scan_up \<longrightarrow>fun go_scan_up" ^ |
|
516 " \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt)) |
|
517 = (Accept_Tac ict); |
|
518 \<close> ML \<open> |
|
519 \<close> ML \<open> |
|
520 \<close> ML \<open> |
|
521 \<close> ML \<open> |
|
522 \<close> ML \<open> |
|
523 \<close> ML \<open> |
|
524 \<close> ML \<open> |
|
525 \<close> ML \<open> |
|
526 (*-------------------- stop step into me Take ------------------------------------------------*) |
|
527 \<close> ML \<open> (*------------- stop step into me Take ------------------------------------------------*) |
|
528 (*\\------------------ step into me Take ---------------------------------------------------//*) |
|
529 \<close> ML \<open> (*\\----------- step into me Take ---------------------------------------------------//*) |
|
530 \<close> ML \<open> |
|
531 val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f; |
|
532 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
533 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
535 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
537 \<close> ML \<open> |
|
538 (*+*)val (**)"L * c + c_2 = q_0 * L \<up> 2 / 2"(** ) |
|
539 "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f; |
|
540 \<close> ML \<open> |
|
541 val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" = |
|
542 (*val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =*) |
|
543 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) |
|
544 \<close> text \<open> |
|
545 case nxt of |
|
546 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
|
547 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; |
|
548 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
549 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
550 |
|
551 (* final test ... ----------------------------------------------------------------------------*) |
|
552 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () |
|
553 else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; |
|
554 |
|
555 case nxt of |
|
556 (End_Proof') => () |
|
557 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
|
558 \<close> ML \<open> |
|
559 Test_Tool.show_pt pt (*[ |
|
560 (([], Frm), solveSystem |
|
561 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2], |
|
562 [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]] |
|
563 [[c], [c_2]]), |
|
564 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2, |
|
565 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]), |
|
566 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]), |
|
567 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]), |
|
568 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]), |
|
569 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]), |
|
570 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]), |
|
571 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2), |
|
572 |
|
573 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2), |
|
574 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2), |
|
575 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L), |
|
576 (([5, 4], Res), c = L * q_0 / 2), |
|
577 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), |
|
578 (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), |
|
579 (([5], Res), [c = L * q_0 / 2, c_2 = 0]), |
|
580 (([], Res), [c = L * q_0 / 2, c_2 = 0])] |
|
581 *) |
115 \<close> ML \<open> |
582 \<close> ML \<open> |
116 \<close> |
583 \<close> |
117 |
584 |
118 section \<open>===================================================================================\<close> |
585 section \<open>===================================================================================\<close> |
119 ML \<open> |
586 ML \<open> |