(* Title:  "MathEngine/step.sml"

   Author: Walther Neuper

*)

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

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

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

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

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

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

"----------- maximum example with Step.specify_do_next -----------------------------------------";

(*"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";*)

(*"----------- maximum example with 'specify', fmz = [] ------------------------------------------";*)

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

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

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

"----------- 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) = Test_Code.init_calc @{context} [(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 --- \<up> 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 -------------------";

States.reset ();

CalcTree @{context}

[(["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 \<up> 2) + d_d x (sin (x \<up> 4))*)

;

         @{term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" }

;

appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";

  (*WAS ERROR: Inner syntax error \n Failed to parse term: "d_d x (x ^ 2) + cos (4 * x ^ 3)"

    -----------------------------------------------------------------\<up>-----------------\<up>*)

(*/------------------- locate ERROR within appendFormula more precisely ---------------------\*)

"~~~~~ fun appendFormula , args:"; val (cI, ifo) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");

    val cs = States.get_calc cI

    val pos = States.get_pos cI 1

val ("ok", (_, _, ptp)) =

    (*case*) Step.do_next pos cs (*of*);

  (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*WAS ERROR: Inner syntax error \n Failed to parse term*)

(*\------------------- locate ERROR within appendFormula more precisely ---------------------/*)

(* the check for errpat is maximally liberal (whole term modulo "rew_rls" 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 \<up> 2) + d_d x (sin (x \<up> 4)) =

  d_d x (x \<up> 2) + cos (x \<up> 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, _), _) = States.get_calc cI

		    val pos as (p, _) = States.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 @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 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*)

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

"~~~~~ final check:";

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

val p = States.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 @{context} f =

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

  (*WAS with old findFillpatterns:

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

  WN120731 replaced 

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

  WN120804 replaced

  "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 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! ==================*)

(*** maximum example with Step.specify_do_next ============================================= ***);

"----------- maximum example with Step.specify_do_next -----------------------------------------";

"----------- maximum example with Step.specify_do_next -----------------------------------------";

val c = []:cid;

val fmz = [

  "fixedValues [r=Arbfix]", "maximum A",

  "valuesFor [a,b::real]",

  "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",

  "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",

  "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",

  "boundVariable a", "boundVariable b", "boundVariable alpha",

  "interval {x::real. 0 <= x & x <= 2*r}",

  "interval {x::real. 0 <= x & x <= 2*r}",

  "interval {x::real. 0 <= x & x <= pi}",

  "errorBound (eps=(0::real))"];

val (dI',pI',mI') = ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);

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

(*** stepwise Specification: Problem model================================================= ***)

val ("ok", ([(Model_Problem, Model_Problem' (["maximum_of", "function"], _, _), _)], _, ptp))

  = Step.specify_do_next (pt, p);

val ("ok", ([(Add_Given "fixedValues [r = Arbfix]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Find "maximum A", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Find "valuesFor [a]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Find "valuesFor [a, b]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Relation "relations [A = a * b]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

(*** Problem model is complete ============================================================ ***)

val PblObj {probl, ...} = get_obj I (fst ptp) [];

val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt

(*** Specification of References ========================================================== ***)

val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp))

  = Step.specify_do_next ptp;

(*** stepwise Specification: MethodC model ================================================ ***)

val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp))

  = Step.specify_do_next ptp;

Step.specify_do_next ptp;

val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val PblObj {meth, ...} = get_obj I (fst ptp) [];

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS boundVariable a , pen2str, Position.T)), \n(9, [1, 2], true ,#Given, (Cor_POS interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str, Position.T)), \n(11, [1, 2, 3], true ,#Given, (Cor_POS errorBound (eps = 0) , pen2str, Position.T))]"

 = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt

(*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)

(*  Step.specify_do_next ptp;

ERROR

---------------------------------------------------------------------- 

actual arg(s) missing for '["(#Find, (maxArgument, v_0))"]' i.e. should be 'copy-named' by '*_._'

*)

(*------------------------------------------------------ after specify --> Step.specify_find_next

"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";

"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";

"----------- maximum example with 'specify', fmz <> [] -----------------------------------------";

val fmz =

    ["fixedValues [r=Arbfix]", "maximum A",

     "valuesFor [a,b]",

     "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

     "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

     "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",

     "boundVariable a", "boundVariable b", "boundVariable alpha",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= pi}",

     "errorBound (eps=(0::real))"];

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

  ("Diff_App",["maximum_of", "function"],

   ["Diff_App", "max_by_calculus"]);

val c = []:cid;

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

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt e_pos' [] pt;

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "maximum (A::bool)" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Relation "relations [A = a * b]" *)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)

(*---------------------------- FIXXXXME.me !!! partial Add-Relation !!!

  Step_Specify.by_tactic_input <> specify ?!

if nxt<>(Add_Relation 

 "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]")

then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

------------------------------ FIXXXXME.me !!! ---*)

(*val nxt = Specify_Theory "Diff_App" : tac*)

val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms);

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Problem ["maximum_of", "function"]*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Method ("Diff_App", "max_by_calculus")*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "boundVariable a" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "errorBound (eps = #0)" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)

case nxt of (Apply_Method ["Diff_App", "max_by_calculus"]) => ()

| _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";

"----------- maximum example with 'specify', fmz = [] ------------------------------------------";

"----------- maximum example with 'specify', fmz = [] ------------------------------------------";

"----------- maximum example with 'specify', fmz = [] ------------------------------------------";

val fmz = [];

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

val c = []:cid;

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

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt e_pos' [] 

  EmptyPtree;

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Theory ThyC.id_empty : tac*)

val nxt = Specify_Theory "Diff_App";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Problem Problem.id_empty : tac*)

val nxt = Specify_Problem ["maximum_of", "function"];

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "fixedValues" : tac*)

val nxt = Add_Given "fixedValues [r=Arbfix]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "maximum" : tac*)

val nxt = Add_Find "maximum A";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor" : tac*)

val nxt = Add_Find "valuesFor [a]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Relation "relations" --- 

  --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)

(*========== inhibit exn 010830 =======================================================*)

(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

if nxt<>(Add_Relation "relations []")

then error "test specify, fmz <> []: nxt <> Add_Relation.." 

else (); (*different with show_types !!!*)

*)

(*========== inhibit exn 010830 =======================================================*)

val nxt = Add_Relation "relations [(A=a+b)]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*)

val nxt = Specify_Method ["Diff_App", "max_by_calculus"];

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "boundVariable" : tac*)

val nxt = Add_Given "boundVariable alpha";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "interval" : tac*)

val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "errorBound" : tac*)

val nxt = Add_Given "errorBound (eps=999)";

val nxt = tac2tac_ pt p nxt; 

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Apply_Method ("Diff_App", "max_by_calculus") *)

(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

if nxt<>(Apply_Method ("Diff_App", "max_by_calculus"))

then error "test specify, fmz <> []: nxt <> Add_Relation.." 

else ();

*)

(* 2.4.00 nach Transfer specify -> hard_gen

val nxt = Apply_Method ("Diff_App", "max_by_calculus");

val(p,_, Test_Out.PpcKF model, nxt,_,pt) = specify nxt p [] pt; *)

(*val nxt = Empty_Tac : tac*)

------------------------------------------------------ after specify --> Step.specify_find_next *)