(* Title:  "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"

   Author: Walther Neuper 1911

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";

"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";

"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";

val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

val (dI',pI',mI') =

  ("Test", ["sqroot-test", "univariate", "equation", "test"],

   ["Test", "squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)

(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)

(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

(*+*)if ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]"

(*+*)then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed asms";

(*+*)case tac of Rewrite_Set "Test_simplify" => (

(*+*)  if p = ([3, 2], Res) then (

(*+*)    if pr_ctree ctxt 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"

(*+*)    then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed pt"

(*+*)  ) else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed p") 

(*+*)| _ => error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed tac";

(*+*)if (get_ctxt pt p |> Proof_Context.theory_of |> Context.theory_name) = "Test" then ()

(*+*)else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed ctxt";

(*[4], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =(**) Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));

    val pIopt = get_pblID (pt,ip);

    (*if*) ip = ([], Pos.Res) (*else*);

      val _ = (*case*) tacis (*of*);

          (*if*) ip = p (*else*);

      (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);

           LI.do_next (pt, ip);

"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));

    (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

        val thy' = get_obj g_domID pt (par_pblobj pt p);

	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

           LI.find_next_step sc (pt, pos) ist ctxt;

"~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)

  = (sc, (pt, pos), ist, ctxt);

  (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Istate.Pstate ist));

  (*if*) path = [] (*else*);

           go_scan_up (prog, cc) (trans_scan_up ist |> set_found);

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = ((prog, cc), (trans_scan_up ist |> set_found));

    (*if*) 1 < length path (*then*);

           scan_up pcc (ist |> path_up) (go_up path sc);

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))

  = (pcc, (ist |> path_up), (go_up path sc));

           go_scan_up pcc ist;

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = (pcc, ist);

    (*if*) 1 < length path (*then*);

           scan_up pcc (ist |> path_up) (go_up path sc);

"~~~~~ and scan_up , args:"; val ((pcc as (_, cc)), ist, (Const (\<^const_name>\<open>Repeat\<close>(*2*), _) $ e))

= (pcc, (ist |> path_up), (go_up path sc));

  (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);

"~~~~~ fun scan_dn , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _)) 

  = (cc, (ist |> path_down [R]), e);

(*============== stopped, when all worked ===================*)

(*[], Res*)val (_, ([(Check_elementwise "Assumptions", _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(**)

(*[], Res*)val (_, ([(Check_Postcond ["sqroot-test", "univariate", "equation", "test"], _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)

(*+*)val (res, asm) = (get_obj g_result pt (fst p));

(*+*)if p = ([], Res) andalso

(*+*)  UnparseC.term res = "[x = 1]" andalso 

(*+*)  map UnparseC.term asm = []

(*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";

Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)