(* Title:  "Minisubpbl/200-start-method-NEXT_STEP.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

val ctxt = Proof_Context.init_global @{theory}

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) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

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

(*/--------- step into Specify_Theory --------------------------------------------------------\*)

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

    val pIopt = Ctree.get_pblID (pt, ip);

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

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

      val SOME _ = (*case*) pIopt (*of*);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

           switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

           specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)

    val (_, (_(*p_'*), _(*tac*))) =

Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = ptp;

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

    (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

    (*if*) p_ = Pos.Pbl (*then*);

"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =

        Specify.for_problem_PIDE ctxt oris (o_refs, refs) (pbl, met);

(*\--------- step into Specify_Theory --------------------------------------------------------/*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', 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"]*)

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

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

(*/--------- investigate Rewrite_Set "Test_simplify" -----------------------------------------\*)

(*+*)val form = get_obj g_res pt (fst p);

(*+*)UnparseC.term form = "x + 1 + - 1 * 2 = 0"; (*isa*)

(*+*)UnparseC.term form = "x + 1 + -1 * 2 = 0"; (*isa2*)

val Rewrite_Set "Test_simplify" = tac;

val res = get_obj g_res pt''''' (fst p''''');

(*+* )UnparseC.term res = "1 + (x + - 2) = 0"; ( *isa*)

(*+*)if UnparseC.term res = "- 1 + x = 0" (*isa2*) then () else error "Test_simplify CHANGED";

val SOME (form', _) = rewrite_set_ ctxt true Test_simplify form;

(*+* )UnparseC.term form' = "1 + (x + - 2) = 0"; ( *isa*)

(*+*)if UnparseC.term form' = "- 1 + x = 0" (*isa2*) then () else error "Test_simplify CHANGED";

(*\--------- investigate 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], Met*)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")*)

val  Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;

if p = ([3, 1], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) = "x = 0 + - 1 * - 1"

then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()

  | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"

else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"

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