1 (* Title: Knowledge/eqsystem-1a.sml
2 author: Walther Neuper 050826,
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "Knowledge/eqsystem-1.sml";
9 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
10 "----------- problems -----------------------------------------------------------equsystem-1.sml";
11 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
12 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
15 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
17 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
18 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
19 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
20 "Knowledge/eqsystem-1a.sml";
21 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
22 "Knowledge/eqsystem-2.sml";
23 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
24 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
25 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
26 "-----------------------------------------------------------------------------------------------";
27 "-----------------------------------------------------------------------------------------------";
28 "-----------------------------------------------------------------------------------------------";
31 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
32 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
33 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
34 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
35 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
36 "solveForVars [c, c_2]", "solution LL"];
38 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
39 ["EqSystem", "normalise", "2x2"]);
40 val p = e_pos'; val c = [];
41 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
42 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
43 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
44 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
45 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
46 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
47 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
49 val (p,_,f,nxt,_,pt) = me nxt p c pt;
50 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
53 "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^
54 " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";
55 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt) =
56 "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)";
58 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
59 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
61 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt
62 val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;
63 (*+*)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)"
64 = (Ctree.get_istate_LI pt p |> Istate.string_of ctxt)
66 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
67 val (p,_,f,nxt,_,pt) = me nxt p c pt;
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
70 (*ERROR type_of: type mismatch in application * real * real list (#) [c]*)
71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 (*+*)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)"
77 = (Ctree.get_istate_LI pt p |> Istate.string_of ctxt)
79 val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;
80 (*/------------------- step into me Apply_Method -------------------------------------------\*)
81 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
82 val (pt'''', p'''') = (* keep for continuation*)
83 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
84 case Step.by_tactic nxt (pt, p) of
85 ("ok", (_, _, ptp)) => ptp;
86 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (nxt, (pt, p));
88 (*+isa==isa2*)val ([5], Met) = p;
89 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);
90 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)" =
91 (*+isa==isa2*)is1 |> Istate.string_of ctxt;
92 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)" =
93 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
96 Step.check tac (pt, p) (*of*);
97 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );
99 (*+*)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)" =
100 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
102 (*if*) Tactic.for_specify tac (*else*);
103 val Applicable.Yes xxx =
105 Solve_Step.check tac (ctree, pos);
107 (*+*)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)" =
108 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
110 "~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);
111 (*if*) Tactic.for_specify' tac' (*else*);
113 Step_Solve.by_tactic tac' ptp;;
114 "~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))
117 (*+*)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)" =
118 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
120 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
121 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
122 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
123 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
124 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
125 => (itms, oris, probl, o_spec, spec)
126 | _ => raise ERROR "LI.by_tactic: no PblObj"
127 val (_, pI', _) = References.select_input o_spec spec
128 val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
129 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
130 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
131 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
132 val ini = LItool.implicit_take ctxt prog env;
133 val pos = start_new_level pos
137 val (tac''', ist''', ctxt''') =
138 case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
139 Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
141 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_top_down_2x2, NONE, \nc_2 = 0, ORundef, true, false)"
142 = ist''' |> Istate.string_of ctxt;
143 (*------------------------------------------------------------------------------------------------------^v^v^v^v^v^v^v^v^v^
144 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)" =
145 (*+isa==isa2*)ist''' |> Istate.string_of ctxt;
147 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
148 = (prog ,(pt, (lev_dn p, Res)), is, ctxt);
150 (Take' ttt, iii, _) =
151 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
153 (*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term @{context});
154 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_top_down_2x2, NONE, \nc_2 = 0, ORundef, true, false)"
155 = (Pstate iii |> Istate.string_of ctxt);
156 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
157 = ((prog, (ptp, ctxt)), (Pstate ist));
158 (*if*) path = [] (*then*);
160 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
161 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
162 = (cc, (trans_scan_dn ist), (Program.body_of prog));
164 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
165 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
166 = (cc ,(ist |> path_down [L, R]), e);
168 (*if*) Tactical.contained_in t (*else*);
170 LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
171 "~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)
172 = ("next ", ctxt, eval, (get_subst ist), t);
175 Prog_Tac.eval_leaf E a v t (*of*);
176 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))
180 (Program.Tac (subst_atomic E t), NONE:term option);
181 "~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;
182 val stac' = Rewrite.eval_prog_expr ctxt prog_rls
183 (subst_atomic (Env.update_opt E (a, v)) stac)
186 (Program.Tac stac', a');
187 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;
189 check_tac cc ist (prog_tac, form_arg);
190 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
191 = (cc, ist, (prog_tac, form_arg));
192 val m = LItool.tac_from_prog (pt, p) prog_tac
194 (*case*) m (*of*); (*tac as string/input*)
198 Solve_Step.check m (pt, p) (*of*);
199 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));
202 check_tac cc ist (prog_tac, form_arg)
204 (*+*)val xxx = (Pstate ist |> Istate.string_of ctxt);
206 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";
207 val (Accept_Tac (tac, ist, ctxt)) = return;
209 (*+*)val xxx = (Pstate ist |> Istate.string_of ctxt)
212 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);
213 "~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;
214 val (tac', ist', ctxt') = (tac, ist, ctxt)
216 (*case*) tac' (*of*);
217 val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
219 (*+isa==isa2*)pos; (*from check_tac*)
220 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];
221 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)" =
222 (*+isa==isa2*)is1 |> Istate.string_of ctxt;
223 (*+*)val xxx = (ist' |> Istate.string_of ctxt)
224 (*-------------------- stop step into me Apply_Method ----------------------------------------*)
225 (*+isa==isa2*)val "c_2 = 0" = f2str f;
226 (*+*)val xxx = (Ctree.get_istate_LI pt''' p''' |> Istate.string_of ctxt)
227 (*\\------------------- step into me Apply_Method ------------------------------------------//*)
229 val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;
231 (*+isa==isa2*)val ([5, 1], Frm) = p'''';
232 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;
233 (*+isa<>isa2*)val (** )Check_Postcond ["triangular", "2x2", "LINEAR", "system"]( **)
234 Substitute ["c_2 = 0"](**) = nxt'''';
235 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');
236 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)" =
237 (*+isa==isa2*)is1 |> Istate.string_of ctxt;
238 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)" =
239 (*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of ctxt;
241 (*//------------------ step into me Take ---------------------------------------------------\\*)
242 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
244 val (pt, p) = (* keep for continuation*)
245 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
247 case Step.by_tactic tac (pt, p) of
248 ("ok", (_, _, ptp)) => ptp;
250 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)" =
251 (*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of ctxt;
254 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
255 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
256 (*if*) Pos.on_calc_end ip (*else*);
257 val (_, probl_id, _) = Calc.references (pt, p);
259 (*case*) tacis (*of*);
260 (*if*) probl_id = Problem.id_empty (*else*);
262 switch_specify_solve p_ (pt, ip);
263 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
264 (*if*) Pos.on_specification ([], state_pos) (*else*);
266 LI.do_next (pt, input_pos);
267 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
268 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
269 val thy' = get_obj g_domID pt (par_pblobj pt p);
270 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
272 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)" =
273 (*+isa==isa2*)ist |> Istate.string_of ctxt;
276 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
277 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
278 = (sc, (pt, pos), ist, ctxt);
280 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
281 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
282 = ((prog, (ptp, ctxt)), (Pstate ist));
283 (*if*) path = [] (*else*);
285 go_scan_up (prog, cc) (trans_scan_up ist);
286 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
287 = ((prog, cc), (trans_scan_up ist));
289 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)" =
290 (*+isa==isa2*)Pstate ist |> Istate.string_of ctxt;
291 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term @{context};
293 (*if*) path = [R] (*root of the program body*) (*else*);
295 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
296 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
297 = (pcc, (ist |> path_up), (go_up ctxt path sc));
298 val (i, body) = check_Let_up ctxt ist sc;
300 (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
301 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
302 = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
305 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
306 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))
307 = (cc, (ist |> path_down [L, R]), e);
309 (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
310 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
311 = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
312 (*if*) Tactical.contained_in t (*else*);
315 LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
316 "~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)
317 = ("next ", ctxt, eval, (get_subst ist), t);
318 val (Program.Tac stac, a') =
319 (*case*) Prog_Tac.eval_leaf E a v t (*of*);
320 val stac' = Rewrite.eval_prog_expr ctxt prog_rls
321 (subst_atomic (Env.update_opt E (a, v)) stac)
323 (*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term @{context};
326 (Program.Tac stac', a');
327 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))
330 check_tac cc ist (prog_tac, form_arg);
331 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
332 = (cc, ist, (prog_tac, form_arg));
333 val m = LItool.tac_from_prog (pt, p) prog_tac
338 Solve_Step.check m (pt, p) (*of*);
339 "~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))
341 val pp = Ctree.par_pblobj pt p
342 val ctxt = Ctree.get_loc pt pos |> snd
343 val thy = Proof_Context.theory_of ctxt
344 val f = Calc.current_formula cs;
345 val {rew_ord, asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
346 val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube
347 val ro = get_rew_ord ctxt rew_ord;
348 (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);
350 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term @{context}
351 (*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map (UnparseC.term @{context})
354 (*case*) Rewrite.rewrite_terms_ ctxt ro asm_rls subte f (*of*);
355 (*-------------------- stop step into me Take ------------------------------------------------*)
356 (*\\------------------ step into me Take ---------------------------------------------------//*)
358 val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;
360 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
361 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
363 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
364 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
366 (*+*)val (** )"L * c + c_2 = q_0 * L \<up> 2 / 2"( **)
367 "[c = L * q_0 / 2, c_2 = 0]"(**) = f2str f;
368 (*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)" =*)
369 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)" =
370 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
373 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
374 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
375 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
376 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
378 (* final test ... ----------------------------------------------------------------------------*)
379 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
380 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
384 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
386 Test_Tool.show_pt pt (*[
387 (([], Frm), solveSystem
388 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
389 [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
391 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
392 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
393 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
394 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
395 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
396 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
397 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
398 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
400 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
401 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
402 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
403 (([5, 4], Res), c = L * q_0 / 2),
404 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
405 (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
406 (([5], Res), [c = L * q_0 / 2, c_2 = 0]),
407 (([], Res), [c = L * q_0 / 2, c_2 = 0])]