(* Title:  "Minisubpbl/790-complete-NEXT_STEP.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

"----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

"----------- Minisubpbl/790-complete-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, e_pos'), []); val Model_Problem = tac;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)

(* there are questionable assumptions either --------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)

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

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"precond_rootmet 1\"]";(*REP*)

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

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"precond_rootmet 1\"]";(*REP*)

(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)

(*/--------------------- final test ----------------------------------\\*)

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

if UnparseC.term @{context} res = "[x = 1]" andalso

  map (UnparseC.term @{context}) asm = []    (* assumptions have gone to the ctxt *)

then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_step CHANGED";

if p = ([], Und)

then

  case get_obj g_tac pt (fst p) of

    Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()

  | _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"

else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1";

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