(* Title:  "MathEngine/step.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- survey on istate, context ----- ---------------------------------------------------";

"----------- embed fun Step.inconsistent -------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- survey on istate, context ----- ---------------------------------------------------";

"----------- survey on istate, context ----- ---------------------------------------------------";

"----------- survey on istate, context ----- ---------------------------------------------------";

(* run this ---vvv code * )

"----------- fun me_trace all Minisubpbl -------------------------------------------------------";

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"]);

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test","squ-equ-test-subpbl1"]*)

(*[1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "norm_equation"*)

(*[2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Pbl*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3], Met*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;

(*[3, 1], Frm*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Apply_Method ["Test","solve_linear"]*)

(*[3, 1], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")*)

(*[3, 2], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Rewrite_Set "Test_simplify"*)

(*[3], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["LINEAR","univariate","equation","test"]*)

(*[4], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_elementwise "Assumptions"*)

(*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*Check_Postcond ["sqroot-test","univariate","equation","test"]*)

(*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*End_Proof'*)

( * run this ---^^^code *)

(* for this output:

========= ([], Pbl)========= Step.by_tactic: Model_Problem  ================================== 

Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),

... ctxt:    []) , 

Res .....  NONE) 

--------- ([], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (x + 1 = 2)---------------------------------- 

========= ([], Met)========= Step.by_tactic: Apply_Method ["Test","squ-equ-test-subpbl1"] ================================== 

Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["precond_rootmet x"]) , 

Res .....  NONE) 

--------- ([1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set "norm_equation"---------------------------------- 

Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["precond_rootmet x"]) , 

Res .....  SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], Rule_Set.empty, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, false),

... ctxt:    ["precond_rootmet x"]) ) 

========= ([1], Frm)========= Step.by_tactic: Rewrite_Set "norm_equation" ================================== 

Frm ..... (SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["precond_rootmet x"]) , 

Res .....  SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,L,R,R], Rule_Set.empty, SOME e_e, x + 1 + -1 * 2 = 0, ORundef, true, true),

... ctxt:    ["precond_rootmet x"]) ) 

--------- ([1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"---------------------------------- 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, -1 + x = 0, ORundef, true, false),

... ctxt:    ["precond_rootmet x"]) ) 

========= ([1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ================================== 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, x + 1 = 2),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, -1 + x = 0, ORundef, true, false),

... ctxt:    ["precond_rootmet x"]) ) 

--------- ([2], Res)--------- Step.do_next \<rightarrow> Subproblem (Test, ["LINEAR","univariate","equation","test"])---------------------------------- 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem

 (''Test'',

  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''

   ''test''), ORundef, true, false),

... ctxt:    ["precond_rootmet x"]) , 

Res .....  NONE) 

========= ([2], Res)========= Step.by_tactic: Subproblem (Test, ["LINEAR","univariate","equation","test"]) ================================== 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem

 (''Test'',

  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''

   ''test''), ORundef, true, true),

... ctxt:    []) , 

Res .....  NONE) 

--------- ([3], Pbl)--------- Step.do_next \<rightarrow> Model_Problem ---------------------------------- 

========= ([3], Pbl)========= Step.by_tactic: Model_Problem  ================================== 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem

 (''Test'',

  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''

   ''test''), ORundef, true, true),

... ctxt:    []) , 

Res .....  NONE) 

--------- ([3], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (-1 + x = 0)---------------------------------- 

========= ([3], Met)========= Step.by_tactic: Apply_Method ["Test","solve_linear"] ================================== 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 

Res .....  NONE) 

--------- ([3,1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")---------------------------------- 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, false),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 

========= ([3,1], Frm)========= Step.by_tactic: Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv") ================================== 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 

--------- ([3,1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"---------------------------------- 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 

========= ([3,1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ================================== 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 

--------- ([3,2], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["LINEAR","univariate","equation","test"]---------------------------------- 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem

 (''Test'',

  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''

   ''test''), ORundef, true, true),

... ctxt:    []) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

========= ([3,2], Res)========= Step.by_tactic: Check_Postcond ["LINEAR","univariate","equation","test"] ================================== 

Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem

 (''Test'',

  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''

   ''test''), ORundef, true, true),

... ctxt:    []) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

--------- ([3], Res)--------- Step.do_next \<rightarrow> Check_elementwise "Assumptions"---------------------------------- 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, false),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

========= ([3], Res)========= Step.by_tactic: Check_elementwise "Assumptions" ================================== 

Frm .....  (NONE, 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

--------- ([4], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["sqroot-test","univariate","equation","test"]---------------------------------- 

Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),

... ctxt:    []) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

========= ([4], Res)========= Step.by_tactic: Check_Postcond ["sqroot-test","univariate","equation","test"] ================================== 

Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),

... ctxt:    []) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

--------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'---------------------------------- 

========= ([], Res)========= Step.by_tactic: input End_Proof' ================================== 

Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),

... ctxt:    []) , 

Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),

... ctxt:    ["matches (?a = ?b) (-1 + x = 0)","x = 1"]) ) 

--------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'---------------------------------- 

*)

"--------- embed fun Step.inconsistent -------------------";

"--------- embed fun Step.inconsistent -------------------";

"--------- embed fun Step.inconsistent -------------------";

reset_states ();

CalcTree

[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 

  ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Steps 1);

autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)

appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);

(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),

  would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.

  results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>

  instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)

(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

findFillpatterns 1 "chain-rule-diff-both";

(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =

  d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)

"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =

  (1, ("chain-rule-diff-both", "fill-both-args"));

    val ((pt, _), _) = get_calc cI

		    val pos as (p, _) = get_pos cI 1;

    val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;

if pos = ([1], Res) then () else error "Step.inconsistent changed 1";

 val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o 

        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;

"~~~~~ fun Step.inconsistent, args:";

  val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =

    ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);

    val f = get_curr_formula (pt, pos);

    val pos' as (p', _) = (lev_on p, Res);

if pos = ([1], Res) then () else error "Step.inconsistent changed 2a";

if UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"

  then () else error "Step.inconsistent changed 2b";

    val (pt,c) = 

      case subs_opt of

        NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f

          (Rewrite thm') (f', []) Inconsistent

      | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f

          (Rewrite_Inst (subs, thm')) (f', []) Inconsistent

    val pt = update_branch pt p' TransitiveB;

if get_obj g_tac pt p' = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))

  andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]

then () else error "Step.inconsistent changed 3";

"~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');

(*val (pt, pos') = Step.inconsistent (sube_opt, thm'_of_thm thm)

            (fillform, []) (get_loc pt pos) pos' pt*)

upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';

"~~~~~ final check:";

val ((pt, _),_) = get_calc 1;

val p = get_pos 1 1;

val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

if p = ([2], Res) andalso 

  get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso

  UnparseC.term f =

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"

  (*WAS with old findFillpatterns:

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"

  WN120731 replaced 

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"

  WN120804 replaced

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_1 * d_d x ?_dummy_2"*)

then () else error "Step.inconsistent changed: fill-formula?";

Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)