1 (* Title: "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
2 Author: Walther Neuper 1911
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
7 "----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
8 "----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
10 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
12 ("Test", ["sqroot-test","univariate","equation","test"],
13 ["Test","squ-equ-test-subpbl1"]);
14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Model_Problem*)
16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Theory*)
17 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
18 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
19 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
20 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
21 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
22 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*)
23 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
24 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
25 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
26 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
27 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
28 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
29 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
31 (*+*)if ((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]"
32 (*+*)then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed asms";
34 (*+*)case tac of Rewrite_Set "Test_simplify" => (
35 (*+*) if p = ([3, 2], Res) then (
36 (*+*) if pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n"
37 (*+*) then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed pt"
38 (*+*) ) else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed p")
39 (*+*)| _ => error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed tac";
41 (*+*)if (get_ctxt pt p |> Proof_Context.theory_of |> theory2str) = "Test" then ()
42 (*+*)else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed ctxt";
44 (*[4], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =(**) step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
46 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
47 val pIopt = get_pblID (pt,ip);
48 (*if*) ip = ([], Pos.Res) (*else*);
49 val _ = (*case*) tacis (*of*);
50 (*if*) ip = p (*else*);
51 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
53 do_solve_step (pt, ip);
54 "~~~~~ and do_solve_step , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
55 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
56 val thy' = get_obj g_domID pt (par_pblobj pt p);
57 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
59 determine_next_tactic sc (pt, pos) ist ctxt;
60 "~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
61 = (sc, (pt, pos), ist, ctxt);
63 (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
64 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
65 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
66 (*if*) path = [] (*else*);
68 go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_);
69 "~~~~~ fun go_scan_up2 , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, finish, ...}))
70 = ((prog, cc), (trans_scan_up2 ist |> set_appy Skip_));
71 (*if*) 1 < length path (*then*);
73 scan_up2 pcc (ist |> path_up) (go_up path sc);
74 "~~~~~ and scan_up2 , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
75 = (pcc, (ist |> path_up), (go_up path sc));
78 "~~~~~ fun go_scan_up2 , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, finish, ...}))
80 (*if*) 1 < length path (*then*);
82 scan_up2 pcc (ist |> path_up) (go_up path sc);
83 "~~~~~ and scan_up2 , args:"; val ((pcc as (_, cc)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))
84 = (pcc, (ist |> path_up), (go_up path sc));
86 (*case*) scan_dn2 cc (ist |> path_down [R]) e (*of*);
87 "~~~~~ fun scan_dn2 , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
88 = (cc, (ist |> path_down [R]), e);
89 (*============== stopped, when all worked ===================*)
92 (*[], Res*)val (_, ([(Check_elementwise "Assumptions", _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(**)
93 (*[], Res*)val (_, ([(Check_Postcond ["sqroot-test", "univariate", "equation", "test"], _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
95 (*+*)val (res, asm) = (get_obj g_result pt (fst p));
96 (*+*)if p = ([], Res) andalso
97 (*+*) term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
98 (*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";