1 (* Title: "Minisubpbl/600-postcond-NEXT_STEP.sml"
2 Author: Walther Neuper 200121
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
7 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
8 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
11 ("Test", ["sqroot-test", "univariate", "equation", "test"],
12 ["Test", "squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
14 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac;
15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac;
16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac;
17 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;
19 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
20 = "([], [], empty, NONE, \n??.empty, ORundef, false, false)"
21 then () else error "pstate changed after ([], Met)";
23 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
25 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
26 = "([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
27 then () else error "pstate changed after ([1], Frm)"; (*this shall be corrected ... \<up> \<up> \<up> : a tac has been found !!!*)
29 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac;
31 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
32 = "([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [R, L, R, L, L, R, R], empty, SOME e_e, \nx + 1 + - 1 * 2 = 0, ORundef, true, false)"
33 then () else error "pstate changed after ([1], Res)"; (*this shall be corrected ............................. \<up> \<up> \<up> *)
35 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "Test_simplify" = tac;
37 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
38 = "([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [R, L, R, L, R, R], empty, SOME e_e, \n- 1 + x = 0, ORundef, true, false)"
39 then () else error "pstate changed after ([2], Res)"; (*this shall be corrected ................... \<up> \<up> \<up> *)
41 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = tac;
43 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
44 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [R, R, D, L, R], empty, NONE, \nSubproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test''), ORundef, true, false)"
45 then () else error "pstate changed after ([3], Pbl)";
47 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac;
48 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac;
49 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["LINEAR", "univariate", "equation", "test"] = tac;
50 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["Test", "solve_linear"] = tac;
52 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
53 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [R, R, D, L, R], empty, NONE, \nSubproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test''), ORundef, true, false)"
54 then () else error "pstate changed after ([3], Pbl)";
56 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["Test", "solve_linear"] = tac;
58 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
59 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
60 then () else error "pstate changed after ([3, 1], Frm)";
62 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;
64 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
65 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * - 1, ORundef, true, false)"
66 then () else error "pstate changed after ([3, 1], Res)";
68 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "Test_simplify" = tac;
70 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
71 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, R], empty, SOME e_e, \nx = 1, ORundef, true, false)"
72 then () else error "pstate changed after ([3, 2], Res)";
74 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_Postcond ["LINEAR", "univariate", "equation", "test"] = tac;
76 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
77 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\"], [R, R, D, L, R], empty, NONE, \n[x = 1], ORundef, true, false)"
78 then () else error "pstate changed after ([3], Res)";
80 (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_elementwise "Assumptions" = tac;
82 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
83 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\", \"\n(L_L, [x = 1])\"], [R, R, D, R, D], empty, NONE, \n[x = 1], ORundef, true, false)"
84 then () else error "pstate changed after ([4], Res)";
86 (*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_Postcond ["sqroot-test", "univariate", "equation", "test"] = tac;
88 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
89 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\", \"\n(L_L, [x = 1])\"], [R, R, D, R, D], empty, NONE, \n[x = 1], ORundef, true, false)"
90 then () else error "pstate changed after ([], Res)";
92 val return_me_Check_Postcond_sqroot_test = Step.do_next p ((pt, e_pos'), []);
93 (*//------------------ step into me_Check_Postcond_sqroot_test -----------------------------\\*)
94 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));
95 val pIopt = Ctree.get_pblID (pt, ip);
96 (*if*) ip = ([], Pos.Res) (*else*);
97 val _ = (*case*) tacis (*of*);
98 val SOME _ = (*case*) pIopt (*of*);
99 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
101 Step_Solve.do_next (pt, ip);
102 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
103 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
104 val thy' = get_obj g_domID pt (par_pblobj pt p);
105 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
107 (*+*)Istate.string_of ctxt ist
108 = "Pstate ([\"\n(e_e, - 1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], empty, NONE, \n[x = 1],"
109 ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)
111 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
112 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
113 = (sc, (pt, pos), ist, ctxt);
115 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
116 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) = ((prog, (ptp, ctxt)), (Pstate ist));
117 (*if*) path = [] (*else*);
120 go_scan_up (prog, cc) (trans_scan_up ist);
121 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
122 = ((prog, cc), (trans_scan_up ist));
123 (*if*) 1 < length path (*then*);
126 scan_up pcc (ist |> path_up) (go_up ctxt path sc);
127 "~~~~~ and scan_up , args:"; val (pcc, ist, (Abs _(*2*))) = (pcc, (ist |> path_up), (go_up ctxt path sc));
131 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
133 (*if*) 1 < length path (*then*);
137 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Let\<close>(*3*),_) $ _ $ (Abs _)))
138 = (pcc, (ist |> path_up), (go_up ctxt path sc));
139 (*\\------------------ step into me_Check_Postcond_sqroot_test -----------------------------//*)
140 val ("end-of-calculation", _) = return_me_Check_Postcond_sqroot_test;
142 (*/--------------------- final test ---------------------------------------------------------\\*)
144 = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\", \"\n(L_L, [x = 1])\"], [R, R, D], empty, NONE, \n[x = 1],"^
145 " ORundef, true, false)"
146 then () else error "";
148 (*ctxt* )Proof_Context.theory_of (Ctree.get_ctxt pt p);( *ctxt CANNOT BE RETRIEVED*)